Cairn.Claims.Move
lean/Cairn/Claims/Move.lean
Moves and the update they induce.
A move is one thing a person can do. It owns a claim id and answers the actions that name a
control of that claim (^5, or ^5#12 for the control with key 12). For each kind of action it
answers (press, edit, …) it has a handler: what happens (apply), what must follow
(post, a formal statement relating the state before and after), and a proof that the first
meets the second whenever the move is enabled.
dispatch is the only way a list of moves becomes an update, so an app cannot react to input
except through a move. The theorems at the end say so formally.
This module is pure and imports nothing from Lean: it is linked into the host. The commands
that build moves live in Cairn.Claims (compile time only).
Imports Cairn.Input, Cairn.Claim
Structures 2
Handler (S : Type) (enabled : S → Nat → Bool) : Type
How a move answers one kind of action. post relates the state before, the action, and the
state after; sound is the proof that apply meets post whenever the move is enabled for the
action's key. Built from the per-trigger forms below, so apply and post only ever look at the
key (and the text op for edit).
Move (S : Type) : Type
One thing a person can do: a claim, when it is available (enabled, per control key), and a
handler for each kind of action it answers.
Inductive types 1
Trigger : Type
The kind of an action, without its payload.
Definitions 15
name : Trigger → String
trigger : Action → Trigger
claim (a : Action) : ClaimId
The claim an action names.
key (a : Action) : Nat
The key of the control an action names (12 in ^5#12, 0 when there is one control).
op? : Action → Option TextOp
The text operation an edit carries.
simple {S : Type} {enabled : S → Nat → Bool} (t : Trigger)
(apply : S → Nat → S × List Effect) (post : S → Nat → S → Prop)
(sound : ∀ (s : S) (k : Nat), enabled s k = true → post s k (apply s k).fst) :
Handler S enabledA handler for an action that carries only its control (press, doublePress, submit,
cancel, blur, appear).
edit {S : Type} {enabled : S → Nat → Bool}
(apply : S → Nat → TextOp → S × List Effect) (post : S → Nat → TextOp → S → Prop)
(sound :
∀ (s : S) (k : Nat) (op : TextOp),
enabled s k = true → post s k op (apply s k op).fst) :
Handler S enabled
id {S : Type} (m : Move S) : ClaimId
triggers {S : Type} (m : Move S) : List TriggerThe triggers a move answers.
handler? {S : Type} (m : Move S) (t : Trigger) :
Option (Handler S m.enabled)The handler a move has for a trigger (the first, though the move command allows only one
per trigger).
find? {S : Type} (moves : List (Move S)) (id : ClaimId) : Option (Move S)The move a list of moves has for a claim id.
dispatch {S : Type} (moves : List (Move S)) (s : S) (a : Action) :
S × List EffectAnswer an action with the move that owns its claim, if that move has a handler for it and is enabled for the action's key. Anything else leaves the state alone and emits nothing.
accepts {S : Type} (moves : List (Move S)) (s : S) (a : Action) : BoolWhether some move answers the action: it owns the claim, has a handler for the trigger, and is enabled. Flows use this to check every step of a witness does something.
Preserves {S : Type} {en : S → Nat → Bool} (h : Handler S en)
(P : S → Prop) : PropThe handler keeps P whenever it runs.
Preserves {S : Type} (m : Move S) (P : S → Prop) : PropEvery handler of the move keeps P.
Theorems 20
find?_some {S : Type} {moves : List (Move S)} {id : ClaimId} {m : Move S}
(h : find? moves id = some m) : m ∈ moves ∧ m.id = id
find?_none {S : Type} {moves : List (Move S)} {id : ClaimId} :
find? moves id = none ↔ ∀ (m : Move S), m ∈ moves → m.id ≠ id
handler?_some {S : Type} {m : Move S} {t : Trigger} {h : Handler S m.enabled}
(e : m.handler? t = some h) : h ∈ m.handlers ∧ h.trigger = t
dispatch_eq {S : Type} {moves : List (Move S)} {s : S} {a : Action}
{m : Move S} {h : Handler S m.enabled} (hm : find? moves a.claim = some m)
(hh : m.handler? a.trigger = some h) (he : m.enabled s a.key = true) :
dispatch moves s a = h.apply s aDispatch. When the move found for the action's claim has a handler for its trigger and
is enabled, dispatch is that handler's apply.
dispatch_disabled {S : Type} {moves : List (Move S)} {s : S} {a : Action}
{m : Move S} (hm : find? moves a.claim = some m) (he : m.enabled s a.key = false) :
dispatch moves s a = (s, [])A disabled move leaves the state unchanged and emits nothing.
dispatch_unhandled {S : Type} {moves : List (Move S)} {s : S} {a : Action}
{m : Move S} (hm : find? moves a.claim = some m) (hh : m.handler? a.trigger = none) :
dispatch moves s a = (s, [])A move with no handler for the action's trigger leaves the state unchanged.
dispatch_unclaimed {S : Type} {moves : List (Move S)} {s : S} {a : Action}
(h : ∀ (m : Move S), m ∈ moves → m.id ≠ a.claim) : dispatch moves s a = (s, [])No behaviour without a claim. If no move owns the action's claim id, the state is unchanged and no effects are emitted.
dispatch_cases {S : Type} (moves : List (Move S)) (s : S) (a : Action) :
dispatch moves s a = (s, []) ∨
∃ m,
m ∈ moves ∧
∃ h,
h ∈ m.handlers ∧
m.id = a.claim ∧
h.trigger = a.trigger ∧
m.enabled s a.key = true ∧ dispatch moves s a = h.apply s aDispatch either leaves the state alone and emits nothing, or it is exactly one enabled handler of one move in the list that owns the action's claim and answers its trigger.
dispatch_effect {S : Type} {moves : List (Move S)} {s : S} {a : Action}
{e : Effect} (he : e ∈ (dispatch moves s a).snd) :
∃ m,
m ∈ moves ∧
∃ h,
h ∈ m.handlers ∧
m.id = a.claim ∧
h.trigger = a.trigger ∧ m.enabled s a.key = true ∧ e ∈ (h.apply s a).sndEvery effect comes from a move. Each effect dispatch emits was emitted by the apply
of an enabled handler of a move in the list that owns the action's claim.
dispatch_post {S : Type} {moves : List (Move S)} {s : S} {a : Action}
{m : Move S} {h : Handler S m.enabled} (hm : find? moves a.claim = some m)
(hh : m.handler? a.trigger = some h) (he : m.enabled s a.key = true) :
h.post s a (dispatch moves s a).fstMoves keep their promises. When dispatch runs an enabled handler, the new state meets
that handler's post.
accepts_iff {S : Type} {moves : List (Move S)} {s : S} {a : Action} :
accepts moves s a = true ↔
∃ m h,
find? moves a.claim = some m ∧
m.handler? a.trigger = some h ∧ m.enabled s a.key = trueaccepts is exactly "dispatch runs a handler".
dispatch_preserves {S : Type} {moves : List (Move S)} (P : S → Prop)
(hP :
∀ (m : Move S),
m ∈ moves →
∀ (h : Handler S m.enabled),
h ∈ m.handlers →
∀ (s : S) (a : Action),
h.trigger = a.trigger →
m.id = a.claim → m.enabled s a.key = true → P s → P (h.apply s a).fst)
(s : S) (a : Action) (hs : P s) : P (dispatch moves s a).fstA property every enabled handler preserves is preserved by dispatch. This is how an invariant is proved one move at a time.
all_nil {S : Type} {en : S → Nat → Bool} {P : S → Prop}
(h : Handler S en) : h ∈ [] → h.Preserves P
all_cons {S : Type} {en : S → Nat → Bool} {P : S → Prop}
{h : Handler S en} {hs : List (Handler S en)} (p : h.Preserves P)
(ps : ∀ (h : Handler S en), h ∈ hs → h.Preserves P) (x : Handler S en) :
x ∈ h :: hs → x.Preserves P
simple_preserves {S : Type} {en : S → Nat → Bool} {P : S → Prop}
{t : Trigger} {ap : S → Nat → S × List Effect} {po : S → Nat → S → Prop}
{so : ∀ (s : S) (k : Nat), en s k = true → po s k (ap s k).fst}
(hp : ∀ (s : S) (k : Nat), en s k = true → P s → P (ap s k).fst) :
(simple t ap po so).Preserves P
edit_preserves {S : Type} {en : S → Nat → Bool} {P : S → Prop}
{ap : S → Nat → TextOp → S × List Effect} {po : S → Nat → TextOp → S → Prop}
{so : ∀ (s : S) (k : Nat) (op : TextOp), en s k = true → po s k op (ap s k op).fst}
(hp : ∀ (s : S) (k : Nat) (op : TextOp), en s k = true → P s → P (ap s k op).fst) :
(edit ap po so).Preserves P
all_nil {S : Type} {P : S → Prop} (m : Move S) : m ∈ [] → m.Preserves P
all_cons {S : Type} {P : S → Prop} {m : Move S} {ms : List (Move S)}
(p : m.Preserves P) (ps : ∀ (m : Move S), m ∈ ms → m.Preserves P) (x : Move S) :
x ∈ m :: ms → x.Preserves P
dispatch_preserves_moves {S : Type} {moves : List (Move S)} {P : S → Prop}
(hm : ∀ (m : Move S), m ∈ moves → m.Preserves P) (s : S) (a : Action) (hs : P s) :
P (dispatch moves s a).fstInvariants one move at a time. If every move keeps P, dispatch keeps P.
simple_apply {S : Type} {en : S → Nat → Bool} {t : Trigger}
{ap : S → Nat → S × List Effect} {po : S → Nat → S → Prop}
{so : ∀ (s : S) (k : Nat), en s k = true → po s k (ap s k).fst} (s : S) (a : Action) :
(simple t ap po so).apply s a = ap s a.key
Instances 3
instReprTrigger : Repr Trigger
instDecidableEqTrigger : DecidableEq Trigger
instInhabitedTrigger : Inhabited Trigger
What dispatch guarantees
Preservation, one handler at a time
An invariant is preserved by dispatch when every handler of every move preserves it. The
move command generates name.preserves, which turns obligations stated in the move's own
terms (its apply, its binders) into Move.Preserves.