Cairn · module

Cairn.Claims.Deliver

lean/Cairn/Claims/Deliver.lean

The claim guarantees, carried through the runtime.

Cairn.Runtime.step_delivers_quiet says a runtime step passes App.update exactly the routed actions, via Runtime.deliver, for an app that ignores the world (every machine's toApp). For an app whose update is a machine's, the lemmas here say what that means for a whole batch of actions: every effect came from an enabled move handler answering one of the actions, and a batch that names no move's claim changes nothing.

Imports Cairn.Claims.Machine, Cairn.Runtime.Step, Cairn.Runtime.WorldProofs

Order

Theorems 5

theorem

Cairn.Claims.deliver_effect

provedlean/Cairn/Claims/Deliver.lean:38

deliver_effect {S : Type} (M : Machine S) {st : S} {acts : List Action}
  {e : Effect} (he : e ∈ (Runtime.deliver M.update st acts).snd) :
  ∃ a,
    a ∈ acts ∧
      ∃ s 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).snd

Every effect the runtime runs comes from a move. Each effect of delivering a batch of actions to a machine was emitted by an enabled handler of one of its moves, answering one of the actions (and owning its claim).

theorem

Cairn.Claims.deliver_unclaimed

provedlean/Cairn/Claims/Deliver.lean:62

deliver_unclaimed {S : Type} (M : Machine S) {st : S} {acts : List Action}
  (h : ∀ (a : Action), a ∈ acts → ∀ (m : Move S), m ∈ M.moves → m.id ≠ a.claim) :
  Runtime.deliver M.update st acts = (st, [])

No behaviour without a claim, through the runtime: a batch of actions none of which names a move's claim leaves the app state alone and runs no effects.

theorem

Cairn.Claims.deliver_run

provedlean/Cairn/Claims/Deliver.lean:75

deliver_run {S : Type} (M : Machine S) (st : S) (acts : List Action) :
  (Runtime.deliver M.update st acts).fst = M.run st acts

Delivering a batch of actions to a machine runs them in order.

theorem

Cairn.Claims.steps_reachable

provedlean/Cairn/Claims/Deliver.lean:81

steps_reachable {S : Type} (M : Machine S) (surfaces : List (Surface S))
  (claims : List ClaimInfo) (cfg : Runtime.Config) (size : Size) (scale : Nat)
  (es : List Event) (initFocus : Option ControlRef := none)
  (hq : ∀ (s : S) (m : Msg), (M.receive s m).fst = s := by intro _ _; rfl) :
  M.Reachable
    (Runtime.steps (M.toApp surfaces claims initFocus) cfg
          (Runtime.start (M.toApp surfaces claims initFocus) cfg size scale) es).fst.app

Invariants hold on screen. In an app whose update is a machine's, the app state of every runtime state reached from start by events is reachable in the machine, so every invariant (Invariant.reachable) holds in it.

theorem

Cairn.Claims.steps_reachableAll

provedlean/Cairn/Claims/Deliver.lean:109

steps_reachableAll {S : Type} (M : Machine S) (app : App S)
  (hi : app.init = M.init) (hu : app.update = M.update) (hr : app.receive = M.receive)
  (cfg : Runtime.Config) (size : Size) (scale : Nat) (es : List Event) :
  M.ReachableAll (Runtime.steps app cfg (Runtime.start app cfg size scale) es).fst.app

Invariants hold on screen, with the world. In any app whose start, update and receive are a machine's (M.toApp, possibly with subscriptions and init effects added), the app state of every runtime state reached from start by any events (input, the clock, timers, replies, subscription events) is reachable in the machine by actions and messages, so every invariant (Invariant.reachableAll) holds in it.