Claims

A claim is a statement about the app with a durable id, written ^N. Claims are a language feature: the commands below are Lean commands, and an app's update is built from its moves and nothing else. For an introduction, read Moves and flows.

Using the commands

The commands need Lean's compiler, which an app must not link (it would make the app about 100 MB). So an app file is a Lean module that imports the runtime and only meta imports the commands, which makes them available at compile time and absent from the binary:

• public import Cairn, which brings in everything an app links and meta-imports the commands; or, module by module, public import Cairn.Claims.Core (the claim types), meta import Cairn.Claims.Elab (the commands), public import Cairn.App and whatever else the app uses;
• @[expose] public section, so other modules' proofs can unfold the app's definitions.

The keywords (move, flow, invariant, assume, place, retire) aren't reserved words, so they stay usable as names elsewhere. Clauses are indented under where, one per line.

move

One thing a person can do.

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

• Header: the id, a Lean name, the state binder (s : State), optionally a key binder (k : Nat) for a keyed move (one control per item: ^5#12 is the control with key 12), the title, and optionally in ^P, the place it appears in.
• does, sees (required): what the person does, and what follows.
• enabled := b (optional; always, by default): when the move is available. A Prop is decided. Presence theorems are stated against it.
• on <trigger>, one block per trigger the move answers: press, doublePress, submit, cancel, blur, or edit (op : TextOp), which binds the text operation.
• In each block: apply := s', or emit := (s', effects) when it asks the host to do something; post s' := P, relating the state before (s), the key and operation if any, and the state after (s'); and sound := proof.

The sound goal is ∀ s, enabled s = true → post s (apply s), with the key and operation added for keyed and edit handlers, and without the enabled hypothesis when there's no enabled.

For a move named deleteItem, the command generates deleteItem.enabled, deleteItem.press.apply (and emit), deleteItem.press.post, deleteItem.press.sound, deleteItem.info (the human half), deleteItem : Move State, and deleteItem.preserves, which turns "every handler keeps P" into what an invariant's proof needs.

A field's move, with edit and submit:

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

machine, moves%, claims%

moves% is every move declared in the current namespace, and claims% every claim's ClaimInfo, retired ones included, in id order. A move declared after moves%, or a claim after claims%, in the same namespace is an error, because it would be silently left out.

def machine : Machine State := { init := {}, moves := moves%, receive }

def claimInfos : List ClaimInfo := claims%

machine.toApp surfaces claims makes the app; an optional last argument names the control focused at launch. A machine can also have a receive, for messages from the outside world (effects).

flow

A goal reachable through moves, with a checked path.

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

witness is a sequence of actions, each naming a move with a handler for that trigger: press ^1, press ^5#12, doublePress ^5#12, edit ^3 (.insert "milk"), edit ^3 .selectAll, submit ^3, cancel ^3, blur ^3. The command generates live (every step is answered by an enabled move) and reaches (the end state meets goal). Both are proved by decide unless you give reaches := proof.

invariant

A property that holds in every reachable state.

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

• holds s := P: the property.
• init: a proof that it holds for the machine's starting state.
• step: a proof that every action keeps it. machine.preserves with Move.all_cons splits it one move at a time.
• receive: for a machine that hears the outside world, a proof that every message keeps it too. Optional, and proved for you, when the machine ignores the world.

Generates reachable and reachableAll (it holds in every state reachable by actions, and by actions and messages), and, when the property is decidable, check, a runnable version the fuzzer calls after every step.

assume

Something the proofs rely on but can't prove.

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"

Optional clauses: statement := P, a formal statement (a definition, never an axiom: theorems that rely on it take it as a hypothesis), and check "name", naming the fuzz check that gathers evidence for it. See the trusted base.

place

A region of the view where moves appear: a window, a menu, a panel. Moves, flows and other places refer to it with in ^P.

place ^1 window "Fixture window" where
  does "The window: a heading, a paragraph, the New item field and Add, the Passcode field, Flash, the items and the count left."

retire

A tombstone. The claim is gone; its id stays issued. It needs the old kind, the old title, and a reason.

Retiring a released claim is a breaking change. A claim the last release had active can be retired only in a new major version, or a new minor version while at 0.x: Cairn at 0.1.2 can retire one in 0.2.0, not in 0.1.3. lake exe ledger check finds the last release from the git tags and fails otherwise. A claim added since then can go in any version.

For example, an invariant the runtime took over: retire ^6 invariant "Moves never leave a press in progress" because "…".

What the build checks

At compile time, in the commands:

Proved once, in the framework, for every app:

• No behaviour without a claim. An action whose control no move owns changes nothing and emits nothing (update_unclaimed).
• Every effect comes from a move: each effect was emitted by an enabled handler of the move that owns the action (update_effect).
• A disabled move, or one without a handler for the trigger, changes nothing.
• An invariant holds in every state the running app reaches, whatever events arrive (steps_reachableAll).

Scopes

Claim ids are scoped by package. Cairn's own are cairn^N. An app in its own repository sets its scope once, in its lakefile's cairn.claims.scope option (cairn new does it for you), and with the scope notes, its ^311 is notes^311. In code, a bare ^N always means the module's own scope: in ^P and a flow's witness find only claims of that scope. Messages name claims in full, and each package keeps its own claims.lock. Frames and the running app still carry bare numbers, since an app's controls are always its own moves.

The scope defaults to cairn, so an app that forgets to set it collides with Cairn's ids at compile time instead of shipping with them. When claims move with an app to its own package, the lock they left marks them moved:<scope>, so the ids stay issued there and can't come back.

The ledger

claims.lock, at the root of the package, has one line per id ever issued: its kind, its status (active, retired, or moved:<scope> for an id that left with an app), a hash of its formal statement, and its title. Tools write it; never edit it by hand. lake exe ledger check runs in make check:

• it fails when an id in the lock is gone from the code without being retired, an id is reused for another kind, a retired id comes back, the code issues an id twice, a claim has no does, or the code has an id the lock doesn't;
• it warns when a claim's statement or title changed. A new meaning needs a new id; to keep the id, run lake exe ledger update --accept, and the change shows in review.

lake exe ledger update appends new ids and marks retired ones. It never removes a line.

The hash covers the claim's formal statement and the definitions it uses, followed into Cairn's own modules. Names of bound variables, apply and proofs don't count, so refactoring a handler doesn't flag the claim, and changing what it promises does.

What isn't checked

• Prose. Nothing proves that sees says what post says. That is what review is for.
• Effects in post. A move's post constrains the state, not which effects it emits.
• Presence and pressability aren't generated: they depend on the view, and each app proves them (Proving a claim).
• Ids are unique only as far as imports reach. Each package's ledger imports everything in that package, which is how it catches two of its apps using the same id. Two packages may both issue ^301, because their scopes differ.