Moves and flows

Everything a person can do in a Cairn app is a move. A move is a claim: it has an id, a title, two sentences for people and a formal statement for Lean. The app's update is assembled from its moves and nothing else, so there is no behaviour without a claim. The framework proves that once, for every app: an action no move owns changes nothing and asks nothing of the host, and every effect an app asks for comes from an enabled move.

This chapter covers the claim kinds you write most: moves, flows and invariants. The claims reference has every clause.

A move

Here is the fixture's Add:

move ^3 addItem (s : State) "Add" in ^1 where
  does "Press Add."
  sees "The field's text, trimmed, is added at the end of the list and the field is cleared. Blank text changes nothing."
  on press
    apply := add s
    post s' := s' = add s
    sound := by intro s; rfl

Reading it top to bottom:

• move ^3 addItem (s : State) "Add" in ^1: the id, a Lean name, the state's name, the title, and the place the control appears in.
• does and sees: what a person does and what follows. Reviewers read these, and its claim pages show them. Both are required.
• on press: one block per kind of action the move answers. The triggers are press, doublePress, submit, cancel, blur and edit, which also binds the text operation.
• apply: the new state. Use emit instead when the move also asks the host to do something; it returns the new state and a list of effects.
• post s': what must be true of the new state s', stated against the old one, s.
• sound: the proof that apply meets post. A move without it doesn't compile.

A move can say when it is available with enabled. An item's delete button is only enabled for an item in the list, and the view only shows it then:

move ^5 deleteItem (s : State) (k : Nat) "Delete an item" in ^1 where
  does "Press an item's delete button."
  sees "The item is gone, and its checkbox and delete button with it."
  enabled := has s k
  on press
    apply := delete k s
    post s' := s'.items = s.items.filter (·.id ≠ k)
    sound := by intro s k _; rfl

With enabled, sound may assume it: the goal is "for every key and every enabled state, post holds after apply", which is why its proof takes three arguments (intro s k _).

Keyed moves: one control per item

A list shows one checkbox per item, and they are all the same move. A keyed move takes a key after the state, and each control carries it: ^4#12 is item 12's checkbox. Delete, above, is one too, and so is the checkbox:

move ^4 toggleItem (s : State) (k : Nat) "Toggle an item" in ^1 where
  does "Press an item's checkbox."
  sees "The item is marked done, or not done again."
  enabled := has s k
  on press
    apply := toggle k s
    post s' := s'.items = s.items.map (flip k)
    sound := by intro s k _; rfl

Text fields

A field's move answers edit with the text operation, and usually submit for Enter. The framework's Text.Field.apply does the editing (the caret, the selection, undo, input methods), and returns the effects an edit needs, such as a clipboard write for copy:

move ^2 typeItem (s : State) "Type a new item" in ^1 where
  does "Type in the New item field, and press Enter."
  sees "The text appears in the field; Enter adds it like Add does."
  on edit (op : TextOp)
    emit := ({ s with field := (Text.Field.apply op s.field).1 }, (Text.Field.apply op s.field).2)
    post s' := s'.field = (Text.Field.apply op s.field).1 ∧ s'.items = s.items ∧
      s'.nextId = s.nextId
    sound := by intro s op; exact ⟨rfl, rfl, rfl⟩
  on submit
    apply := add s
    post s' := s' = add s
    sound := by intro s; rfl

Flows

A flow is a goal and a path that reaches it: a list of actions, each naming a move. Lean runs the path through the machine at compile time and checks two things: that every step is answered by an enabled move (so the path isn't a run of no-ops), and that the end state meets the goal.

flow ^8 addAndFinish "Add two items and finish one" for machine where
  does "Type milk and press Enter, type eggs and press Add, then check milk."
  sees "Two items, milk done."
  goal s := s.items.map (·.text) = ["milk", "eggs"] ∧ s.items.map (·.done) = [true, false]
  witness edit ^2 (.insert "milk"), submit ^2, edit ^2 (.insert " eggs "), press ^3, press ^4#1

flow ^33 finishFromMenus "Finish items from their menus" for machine where
  does "Add milk and eggs, mark milk done and delete it from its menu, mark eggs done from its menu, then Clear Done in the app menu."
  sees "No items left."
  goal s := s.items.length = 0
  witness edit ^2 (.insert "milk"), submit ^2, edit ^2 (.insert "eggs"), press ^3, press ^26#1,
    press ^27#1, press ^26#2, press ^29

A witness step names a control: press ^3, press ^4#1, edit ^2 (.insert "milk"), submit ^2. Flows are also what the conformance driver replays against the running app.

Invariants

An invariant is a property that holds in every state the app can reach. You prove it holds at the start (init) and that every move keeps it (step). The commands then derive that it holds in every reachable state, and the runtime theorems carry that onto the screen. The fixture's says every item's id is below the id the next item gets, so a new item's id is never one already in the list:

invariant ^7 idsBelow "Item ids stay below the next id" for machine where
  does "Every item's id is positive and below the id the next item gets, in every reachable state."
  holds s := Inv s
  init := ⟨Nat.one_pos, fun _ h => by simp only [machine, List.not_mem_nil] at h⟩
  step := machine.preserves <|
    Move.all_cons (typeItem.preserves _ (fun _ _ h => h) fun _ h => add_inv h)
      (Move.all_cons (addItem.preserves _ fun _ h => add_inv h)
      (Move.all_cons (toggleItem.preserves _ fun _ k _ h => toggle_inv k h)
      (Move.all_cons (deleteItem.preserves _ fun _ k _ h => delete_inv k h)
      (Move.all_cons (flashMove.preserves _ fun _ h => h)
      (Move.all_cons (typePasscode.preserves _ (fun _ _ h => h) fun _ h => h)
      (Move.all_cons (selectRow.preserves _ fun _ _ _ h => h)
      (Move.all_cons (reachEnd.preserves _ fun _ h => h)
      (Move.all_cons (addTop.preserves _ fun _ h => h)
      (Move.all_cons (addEnd.preserves _ fun _ h => h)
      (Move.all_cons (like.preserves _ fun _ _ _ h => h)
      (Move.all_cons (refresh.preserves _ fun _ h => h)
      (Move.all_cons (menuToggle.preserves _ fun _ k _ h => toggle_inv k h)
      (Move.all_cons (menuDelete.preserves _ fun _ k _ h => delete_inv k h)
      (Move.all_cons (clearDoneMove.preserves _ fun _ _ h => clearDone_inv h)
      (Move.all_cons (firstRow.preserves _ fun _ h => h)
      (Move.all_cons (noRow.preserves _ fun _ _ h => h)
      (Move.all_cons (scrollTop.preserves _ fun _ _ h => h)
      (Move.all_cons (scrollEnd.preserves _ fun _ _ h => h)
      (Move.all_cons (scrollRow.preserves _ fun _ _ h => h)
      (Move.all_cons (hideRows.preserves _ fun _ h => h)
      (Move.all_cons (badgeMove.preserves _ fun _ h => h)
      (Move.all_cons (clearBadge.preserves _ fun _ h => h)
      (Move.all_cons (announceMove.preserves _ fun _ h => h) Move.all_nil)))))))))))))))))))))))
  receive := fun _ _ h => h

The step proof goes one move at a time: machine.preserves splits it, and each move's generated preserves lemma leaves one obligation per handler, stated over that handler's own apply. The lemmas it uses (add_inv, toggle_inv, delete_inv) are ordinary theorems in the same file. The fixture's machine also hears the world (Flash's timer), so the invariant has a third clause, receive: every message keeps it too. When the invariant is decidable, the command also makes it a runnable check, which the fuzzer runs after every step.

Places, assumptions and retired claims

Three more kinds complete the set:

• A place is a region of the view where moves appear: a window, a menu, a panel.
• An assumption (assume) is something the proofs rely on but can't prove, such as "the host reports clicks where they happen". It is recorded, never proved, and theorems that rely on it take it as a hypothesis, so every use shows.
• A retired claim is a tombstone. Its id stays issued forever, with the reason it went.

Every app relies on that one, so Cairn's trusted base declares it, and the host fuzzer gathers its evidence (check):

assume ^7 hostClicks "The host reports clicks where they happen" where
  does "The host sends a pointer down and up at the logical point the person clicked, in order."
  check "pointer.click"

A retired claim keeps its kind, its title and the reason it went. An invariant the state no longer has anything to say about is retired, not deleted, and its id is never used again.

Ids are the contract

An id is never renumbered or reused. claims.lock, at the root of the repository, records every id ever issued with a hash of its formal statement, and make check fails when an id disappears without being retired, comes back after it, or changes kind. When a claim's statement changes, the build warns: a new meaning needs a new id, or an explicit lake exe ledger update --accept that shows up in review.