Cairn Docs Claims Blog Packages
Contents

Evidence

Claims

Everything a person can do in a Cairn app is a claim, with an id that never changes, a promise, and a proof that the promise holds in every state.

A claim isn't a test that passed once. It is a statement Lean checks for every state the app can be in, under an id that tests, docs, reviews and agents can cite. Here is one running.

^202
^202
^203^202^204#1^205#1^206#1^208^209^210
^203^202^204#1^205#1^206#1^208^209^210
^203^202^204#1^205#1^206#1^204#2^205#2^206#2^208^209^210
Todo after flow ^216: milk checked, eggs active, 1 item left. Every control carries its claim id.
^203^202^204#1^205#1^206#1^204#2^205#2^206#2^208^209^210^211

^216 flow Add two todos and complete one

  1. Type “milk” edit ^202 (.insert "milk")
  2. Press Enter submit ^202
  3. Type “␣␣eggs␣” edit ^202 (.insert " eggs ")
  4. Press Enter submit ^202
  5. Check milk press ^204#1

Goal Two todos in order, eggs trimmed, milk completed, the field empty, 1 item left. proved reachable

^204 move Complete a todo

The todo is completed, or active again; the counter follows, and under a filter it leaves or joins the list. Nothing else changes.

proved in every state where it's offered

Todo running flow ^216, frame by frame: every control on screen carries its claim's id. The frames were drawn by the app's own Lean code. Point at a control to read its claim.

Each step of that run is a move with its own id, and each move promises what follows, in words for people and in a statement for Lean. The flow, ^216, is a claim too: Lean checks that every step is offered when it's taken and that the goal holds at the end. Change the app so that any of it stops being true, and it doesn't build.

What's in one

Here is the whole of Reset, in Counter. The two lines in green are for people; everything under them, in gold, is for the checker.

move1 ^22 reset (s : State)3 "Reset"4 in ^35 where  does "Press Reset."6  sees "The count is zero, and Reset disappears."  enabled7 := resetEnabled s8  on press9    apply := { s with count := 0 }10    post s' := s'.count = 0 ∧ resetEnabled s' = false11    sound := by12 intro s _13; exact ⟨rfl, rfl⟩14
  1. A move Something a person can do. Cairn's other claims are flows (a path through moves), invariants (always true) and places (where things show). Like a test step, except it's declared with the app instead of written after it.
  2. The id, ^2 Permanent: never renumbered or reused. Reviews, docs and agents cite it. A data-testid that can't drift, kept in a ledger (claims.lock).
  3. The input, s The app's whole state at the moment of the press. It's a variable, so everything below holds for any s.
  4. The title The button's label, as people see it.
  5. The place, ^3 Where the button lives. ^3 is a claim too, a place: Counter's window. The build checks that ^3 exists and is a place.
  6. What it does, in words does says what you do, sees what you'll see next: plain English for reviewers, shown on the claim's page. Lean checks the lines below, not these. Like the name in test('…').
  7. When it's offered Reset exists only while this is true. Cairn proves the button is on screen exactly then, in every state. Playwright's toBeVisible() checks one page load.
  8. A plain function The same Lean function the view calls to decide whether to draw the button, so the claim and the screen can't disagree. No selector to keep in sync.
  9. On press The contract for one press, as given, when, then: enabled is the given, apply the when, post the then. Given-When-Then, with a proof in place of a test run.
  10. The new state A copy of s with the count set to 0. Pure: nothing changes in place, and nothing is asked of the host. Like a Redux reducer.
  11. The promise About the new state s′: the count is 0, and (∧) Reset is gone. An expect(), stated for every state instead of asserted on one run.
  12. A proof begins by switches from stating to proving. sound is the claim that post always follows from apply.
  13. For any state Take any s where Reset is enabled: any s, not only the ones a test tried.
  14. Both halves hold rfl: true by computing, one for each side of the ∧. If either fails, the app doesn't build. Like Rust's assert_eq!, except the compiler settles it for every s instead of running it on one value.
Counter's Reset button, exactly as written in Counter.lean. Every line under sees is checked when the app builds.

What they buy you

Every state, not one run

A test drives the app down one path and checks where it lands. A claim's proof is about every state at once, including the ones nobody thought to try.

  • A test One run: the six states flow ^216 passes through. It says nothing about the other 394.
  • A proof Invariant ^212, “the counter shows the number of active todos, and ids are distinct”, holds in all 400, and in every state past them: 1,004 moves lead out of what was explored.
Todo's states, by how many moves they are from launch. The rings stop at 400 because the explorer did; the app doesn't, and neither does the proof.

Nothing happens without one

An event arrives

a click, a key, a timer

^N owns it

Its move runs, and its promise holds afterwards.

No claim owns it

The state is unchanged and nothing is asked of the host. update_unclaimed

An app's update is built only from its moves, so this holds for every Cairn app, proved once in the framework. Every effect an app asks for (a file write, a sound, a timer) comes from some move (update_effect). The list of claims is the list of what the app can do, with nothing hiding outside it.

One name, everywhere

The id is how everything else refers to the behaviour, and it means the same thing in all of them:

  • The codemove ^204 toggleTodo (s : State) (k : Nat) "Complete a todo"
  • Accessibilityidentifier "^204#1"the checkbox on milk, for VoiceOver and UI tests
  • A flowwitness … submit ^202, press ^204#1
  • Its page/packages/cairn_examples/claims/204/
  • Review^204 “Complete a todo”: meaning changed

A data-testid names an element and drifts when someone renames it. ^204 names a behaviour and can't be renamed: tests, docs, agents and bug reports that cite it stay right for as long as the app exists.

Meaning changes show up in review

Each package keeps a ledger of every id it has issued. A refactor that changes no promise passes quietly; one that changes what a claim says is flagged, and has to take a new id or be accepted in a commit someone reviews.

claims.lock cairn_examples, an excerpt

  1. 204moveactivebfb82886ecadd91cComplete a todo
  2. 212invariantactive8b1d23f718f063ecCounter and ids
  3. 213invariantretired-The list is the filter applied to the todosStyle gained an image field, which changed the statement: reissued as ^225
  4. 215moveretired-Back through filtersWeb only: the Mac app has no Back command
  5. 216flowactive059a40708193b6f5Add two todos and complete one
  6. 225invariantretiredcdded3b5839c217cThe list is the filter applied to the todosFieldView gained secure: reissued as ^226
  7. 226invariantactive5df0a26eadf00c3cThe list is the filter applied to the todos

What the build says

warning ^225 “The list is the filter applied to the todos”: meaning changed (statement cdded3b5839c217c → 5df0a26eadf00c3c): give it a new id or lake exe ledger update --accept

error ^215 move “Back through filters” is in claims.lock but gone from the code. Ids never disappear: retire it with retire ^215 move "Back through filters" because "…"

Every id a package ever issued, with a hash of what it promises. ^213 and ^225 kept their meaning and lost their id: a published claim keeps its statement, so a changed statement takes a new id. The two messages are the ledger's own, for a hash that changes and for an id deleted instead of retired.

A released claim is a promise to whoever relies on it, so retiring one needs a major version: semver for guarantees, checked by the build. Claims has the ledger's rules.

Six kinds

Moves are what people do. The other five say how moves fit together, what always holds, and what is taken on trust.

  • move

    Something a person can do: when it's offered, what it does, the promise afterwards and its proof.

    ^204 Complete a todo

  • flow

    A goal and a path of moves that reaches it. Lean checks every step is offered and the goal holds at the end.

    ^216 Add two todos and complete one

  • invariant

    A property every move keeps, proved once, so it holds in every state the app can reach.

    ^212 Counter and ids

  • assume

    What the proofs rely on and can't prove, mostly about the host. Recorded, checked by fuzzing, visible in every theorem that uses it.

    cairn^908 The host's clock is monotonic

  • place

    A region of the view where moves appear: a window, a menu, a panel. Claim pages are grouped by them.

    ^201 Todos window

  • retire

    A tombstone with a reason. The claim is gone, the id stays issued forever, and retiring a released claim is a breaking change.

    ^215 Back through filters

How sure we are

Each claim carries the evidence it has, not only the strongest. They rule out different things:

  1. ProvedA counterexample anywhere: every state, every key, every input.
  2. FuzzedA counterexample in the random sessions it ran, the claim checked after every step.
  3. TestedThe running app disagreeing with the proved model, on the sequences it drove.
  4. SeenA control that's never drawn, a flow that can't be clicked through.
  5. AssumedNothing by itself. Written down, so every proof that relies on it says so.

A proof still trusts that its statement says what you mean: post s' := True is easy to prove and promises nothing. How much to trust a claim says what each kind of evidence still takes on faith, with a bug the tests miss and the proof catches, and the evidence ladder says how the build computes them.

The registry's claim pages

Every package on the registry has claim pages: each version's claims, grouped by the place (window) they belong to, and a page for each claim with what you do and see, a flow's steps, its evidence theorems and where it's defined. They are rendered from the claims export that cairn publish sends with each version, checked by the registry against the version's claims.lock. Nothing on them is written by hand. You can also click through Todo's states, every control labelled with its claim.

Place What it covers
The trusted base the host's assumptions, cairn^7, cairn^214, ^9xx and ^10xx
Counter cairn_examples^1–^6: two moves, two flows and a retired claim
Basics cairn_examples^101–^109: a field, a keyed list and an invariant
TodoMVC cairn_examples^201–^226: the full TodoMVC spec
Clock cairn_examples^401–^409: time, timers and files
Tray cairn_examples^450–^462: a menu bar item, a submenu and an overlay panel
Gallery cairn_examples^501–^513: images and a grid that fits the window
Pairs pairs^1–^32: a deal of the pack, two cards up at most, and every game can be won
Sky sky^1–^36: sign in, the session, and a feed with no duplicates or gaps however its pages and refreshes race
cairn_atproto cairn_atproto^1–^16: the session machine, one refresh at a time, each call sent at most twice
Yap yap^301–^399: a menu bar menu, an overlay and the dictation machine

The pages show the evidence the export holds: proofs and their axioms, assumptions, flow witnesses, retired and moved ids. Fuzzing, conformance and screenshots need a build that runs the app, and a claim lists them as not shown yet until CI publishes them. A version published before the export existed shows its ledger alone.