Cairn.Claims.Machine
lean/Cairn/Claims/Machine.lean
A machine is an initial state and the moves that act on it. Its update is derived from the
moves by dispatch, so it inherits every guarantee in Cairn.Claims.Move. Flows and invariants
are stated against a machine.
A machine may also hear the outside world (docs/effects.md): receive takes the clock, timers,
replies and subscription events. An invariant must be kept by receive as well as by every
move, so it holds over any interleaving of a person's actions and the host's messages
(Invariant.reachableAll), and through the runtime (Cairn.Claims.steps_reachableAll).
Pure, and linked into the host, like Cairn.Claims.Move.
Imports Cairn.Claims.Move, Cairn.App
Structures 5
Machine (S : Type) : Type
init : S
moves : List (Move S)
receive : S × List Effect
What the outside world does to the state (App.receive); by default nothing.
Flow {S : Type} (M : Machine S) : TypeA goal reachable from the machine's initial state, with a witness: a sequence of actions, each answered by an enabled move, after which the goal holds.
Invariant {S : Type} (M : Machine S) : TypeA property of every reachable state: true initially, preserved by every update (so by
every move, see Machine.update) and by every message from the world (Machine.receive; for a
machine that ignores the world this is immediate).
info : ClaimInfo
holds : Prop
init : self.holds M.init
step : self.holds (M.update s a).fst
recv : self.holds (M.receive s m).fst
Assumption : Type
Something taken as given about the world. statement is recorded, never proved: theorems
that rely on it take it as a hypothesis, so it never becomes an axiom.
info : ClaimInfo
statement : Prop
Place : Type
A region of the view where moves appear.
info : ClaimInfo
Definitions 9
update {S : Type} (M : Machine S) (s : S) (a : Action) :
S × List EffectThe update an app gets from its moves.
run {S : Type} (M : Machine S) (s : S) (as : List Action) : SThe state after a sequence of actions.
live {S : Type} (M : Machine S) : S → List Action → BoolEvery action in the sequence is answered by an enabled move, in turn.
Reachable {S : Type} (M : Machine S) (s : S) : PropStates reachable from init.
feed {S : Type} (M : Machine S) (s : S) : Action ⊕ Msg → S
runAll {S : Type} (M : Machine S) (s : S) (xs : List (Action ⊕ Msg)) :
SThe state after a sequence of actions and messages.
ReachableAll {S : Type} (M : Machine S) (s : S) : PropStates reachable from init by actions and messages.
toApp {S : Type} (M : Machine S) (surfaces : List (Surface S))
(claims : List ClaimInfo) (initFocus : Option ControlRef := none) : App SAn app whose update is this machine's, showing surfaces (M1 apps: one window).
StateOf {S : Type} : Machine S → TypeThe state type of a machine. The flow and invariant commands use it to type the bodies they are given without asking for the state type again.
Theorems 11
all {S : Type} (M : Machine S) {s : S} (h : M.Reachable s) :
M.ReachableAll s
run_nil {S : Type} (M : Machine S) (s : S) : M.run s [] = s
run_cons {S : Type} (M : Machine S) (s : S) (a : Action)
(as : List Action) : M.run s (a :: as) = M.run (M.update s a).fst as
run_append {S : Type} (M : Machine S) (s : S) (as bs : List Action) :
M.run s (as ++ bs) = M.run (M.run s as) bs
update_unclaimed {S : Type} (M : Machine S) {s : S} {a : Action}
(h : ∀ (m : Move S), m ∈ M.moves → m.id ≠ a.claim) : M.update s a = (s, [])No behaviour without a claim, for a machine.
update_effect {S : Type} (M : Machine S) {s : S} {a : Action}
{e : Effect} (he : e ∈ (M.update s a).snd) :
∃ m,
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, for a machine.
preserves {S : Type} (M : Machine S) {P : S → Prop}
(hm : ∀ (m : Move S), m ∈ M.moves → m.Preserves P) (s : S) (a : Action) :
P s → P (M.update s a).fstInvariants one move at a time, for a machine: if every move keeps P, so does every
update. Pair with the name.preserves lemma each move generates.
run_preserves {S : Type} (M : Machine S) (P : S → Prop)
(step : ∀ (s : S) (a : Action), P s → P (M.update s a).fst) (as : List Action) (s : S) :
P s → P (M.run s as)A property true at s and preserved by every update holds after any sequence.
runAll_preserves {S : Type} (M : Machine S) (P : S → Prop)
(step : ∀ (s : S) (a : Action), P s → P (M.update s a).fst)
(recv : ∀ (s : S) (m : Msg), P s → P (M.receive s m).fst) (xs : List (Action ⊕ Msg))
(s : S) : P s → P (M.runAll s xs)A property true at s and kept by every update and every message holds after any sequence
of both.
reachable {S : Type} {M : Machine S} (i : Invariant M) {s : S}
(h : M.Reachable s) : i.holds s
reachableAll {S : Type} {M : Machine S} (i : Invariant M) {s : S}
(h : M.ReachableAll s) : i.holds s
Claims other than moves
Each structure pairs the claim's human half (ClaimInfo) with its formal half. The commands in
Cairn.Claims build them; the evidence is in the fields' proofs.