# Claims

> Every claim kind, its clauses, what it generates, and what the build checks.

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](https://cairn.iamnbutler.workers.dev/docs/guide/moves-and-flows.md).

## 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 import`s 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.

```lean
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
```

`test/fixture/lean/Fixture.lean`, lines 266–273

- **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`:

```lean
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
```

`test/fixture/lean/Fixture.lean`, lines 230–241

## `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.

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

`test/fixture/lean/Fixture.lean`, line 516

```lean
def claimInfos : List ClaimInfo := claims%
```

`test/fixture/lean/Fixture.lean`, line 610

`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](https://cairn.iamnbutler.workers.dev/docs/guide/effects.md)).

## `flow`

A goal reachable through moves, with a checked path.

```lean
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
```

`test/fixture/lean/Fixture.lean`, lines 595–606

`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.

```lean
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
```

`test/fixture/lean/Fixture.lean`, lines 520–549

- **`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.

```lean
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"
```

`lean/Cairn/Fuzz/Trusted/Claims.lean`, lines 254–256

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](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md).

## `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`.

```lean
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."
```

`test/fixture/lean/Fixture.lean`, lines 225–226

## `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:

| Check | Error |
|---|---|
| an id is issued once among everything imported | `claim id cairn^N is already issued: …` |
| a move says what the person does and what follows | `missing does "…"`, `missing sees "…"` |
| `in ^P` names a place that exists and isn't retired | `unknown place ^P`, `^P is not a place` |
| a move has at least one handler, at most one per trigger, each with `apply` or `emit`, `post` and `sound` | `missing sound`, and so on |
| a flow's witness names moves with a handler for each step's trigger | `a witness step names a move, and ^P is not one` |
| a flow's witness is live and reaches its goal | the `decide`, or your proof, fails |
| a retired claim says why | `a retired claim says why it was retired` |

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](https://cairn.iamnbutler.workers.dev/docs/guide/proving.md)).
- **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.

From https://cairn.iamnbutler.workers.dev/docs/reference/claims/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt