How much to trust a claim

A claim's evidence says proved, fuzzed, tested, seen or assumed. This page says what each of those words buys you: what it rules out, and what you still have to trust when you rely on it. The evidence ladder says how the build computes them.

A claim keeps every kind it has, not just the strongest, because they cover different things. A proof is about the Lean model; only conformance runs the real app, and only the capture puts it on screen.

Proved

What is checked. Every theorem the claim names (a move's sound, a flow's live and reaches, an invariant's init and step) exists and was accepted by Lean's kernel. make check audits each one's axioms: only propext, Classical.choice and Quot.sound are allowed, so a sorry or a new axiom anywhere underneath shows up. A lint rejects the escape hatches that would skip the kernel (native_decide, implemented_by, debug.skipKernelTC), and every declaration is replayed through the kernel once more.

What it rules out. Every case, not a sample of them. A move's post holds in every state where the move is enabled, for every key and every text edit; an invariant holds in every state the app can reach. No test suite can say that.

What it still trusts.

• The statement. A proof shows that the formal statement holds, not that it says what you meant. post s' := True is easy to prove and promises nothing. Nothing checks that the does and sees prose says what post says; that is review's job. The API reference prints each claim's formal statement next to its words so a reader can compare them, and the ledger warns when a statement changes, so a weakened promise shows in review.
• Lean. Its kernel, which checks the proofs, and its compiler, which builds the code that actually runs. The proofs are about the definitions; the compiled code is trusted to behave like them. Banning implemented_by keeps the two the same code.
• Everything below the bytes. The proofs end at the frame Lean sends: the host, AppKit, Core Text, Metal and the GPU are the trusted base, each piece an assumption with its own checks.

Fuzzed

What is checked. cairn fuzz runs random sequences of moves against the Lean model and, after every step, checks each claim it can: a move's post, its control's presence and pressability, every invariant. For an assumption, the trusted-base fuzzer runs the real host code against Lean's proved code or another oracle. A failure prints the command that replays it.

What it rules out. A counterexample in the sequences it ran: 200 by default, and as many as you ask for. That is far more than a person writes by hand, and the fuzzer tries the odd orders people don't.

What it still trusts. That a bug is reachable in a short random walk. A case that needs a rare, long or precise setup can hide from it. For a move or an invariant, fuzzing is a cheap second opinion on what the proof already covers; for an assumption, which has no proof, it is the evidence.

Tested

What is checked. cairn conformance drives the real app (its Swift host, its compiled Lean) through its debug socket and compares every frame with what the Lean model says it should be.

What it rules out. The running app and the model disagreeing, on the sequences it ran. It is the only evidence that reaches through the host.

What it still trusts. The harness: events are injected at the view, not through the window server; keys are built as a US keyboard would produce them; no real input method runs; frames are compared through two JSON printers, one per language. And it says nothing about sequences it didn't run.

Seen

What is checked. The capture renders the app's frames with the real renderer and replays each flow's witness, clicking each step's control where it was laid out. A move is seen when its control is in a captured frame; a flow, when its whole witness replays. No capture runs today: it went with the example apps (#137), and nothing gathers this evidence until one comes back.

What it rules out. A control that is never drawn, and a flow that can't be clicked through. It is also the evidence a person can look at.

What it still trusts. That the model's frames are what the app shows: the capture renders Lean's frames, not the running window. Conformance is what ties the two together. Some rarer text operations (word movement, input-method composition) aren't replayed yet, so a flow that uses one is only partly seen.

Assumed

An assume claim states something the proofs rely on and can't prove, most often about the host: that the clock never goes backwards, that the host reports clicks where they happen. It always reads as assumed, even when fuzzed, so it never passes for a proof.

What it rules out. Nothing by itself. Its evidence is whatever checks it: Cairn's own assumptions each name a fuzz check (check "name") and are listed with their results on the trusted base page.

What it still trusts. Whoever wrote it. That is the next question.

Who checks an assume?

Cairn's checks are built to catch an honest author's mistakes, and they do that well. They are not a defence against an author who means to mislead you, and it is worth being exact about why.

Here is what the build does for an honest author:

• An assumption's formal statement is a definition, never an axiom: a theorem that relies on it takes it as a hypothesis, so the reliance is written in the theorem's own statement.
• Every assumption is a claim with an id, kind assume, in the package's ledger and its API reference. You can list them all.
• A claim's statement can't change quietly: the ledger hashes it, warns on a change, and needs ledger update --accept, which shows in review. Ids are never reused.

A hostile author has more room:

• An assume can state something false. Nothing proves it; only a check the author chose to write gathers evidence for it.
• A post can be weak, and does and sees can promise more than the formal statement does. The proof is real; it just proves less than the prose says.
• An app's own Swift code, such as a Metal shader it draws with, is outside the proofs.
• Cairn's lint, axiom audit and kernel replay run in Cairn's repository. An app in its own repository has no cairn check yet, and the package registry shows what the publisher sent (its ledger, and its claims with their proofs) without rebuilding it or re-running them.

So read a package you don't trust for its statements, not its green ticks. List its assume claims and decide whether you believe each one. Read each claim's formal statement beside its prose. Build it yourself and run the checks, so the evidence is your kernel's and not the publisher's report.

A bug the tests miss

The fixture, Cairn's own test app (test/fixture), gives each new item the id it keeps in its state and counts that id up. Invariant ^7 says every item's id is below the next one, so no two items can share an id:

/-- ^7's statement. -/
def Inv (s : State) : Prop := 0 < s.nextId ∧ ∀ i ∈ s.items, i.id < s.nextId

theorem add_inv {s : State} (h : Inv s) : Inv (add s) := by
  obtain ⟨hn, hb⟩ := h
  unfold add
  by_cases ht : trimmed s.field.text = []
  · simp only [ht, ↓reduceIte]; exact ⟨hn, hb⟩
  · simp only [ht, ↓reduceIte]
    refine ⟨Nat.succ_pos _, fun i hi => ?_⟩
    simp only [List.mem_append, List.mem_singleton] at hi
    rcases hi with hi | rfl
    · exact Nat.lt_succ_of_lt (hb i hi)
    · exact Nat.lt_succ_self _

add keeps it: the new item takes the next id, and the next id goes up by one.

/-- The field's text without leading and trailing whitespace. -/
def trimmed (t : List Char) : List Char :=
  ((t.dropWhile Char.isWhitespace).reverse.dropWhile Char.isWhitespace).reverse

/-- Add the field's trimmed text as a new item and clear the field; nothing when it's blank. -/
def add (s : State) : State :=
  if trimmed s.field.text = [] then s
  else
    { s with items := s.items ++ [{ id := s.nextId, text := String.ofList (trimmed s.field.text) }],
             nextId := s.nextId + 1, field := Text.Field.empty placeholder }

Here is the same function with one plausible slip. It works the next id out from how many items there are:

/-- `add`, except that it works out the next id from how many items there are, instead of
keeping it. -/
def addBuggy (s : State) : State :=
  if trimmed s.field.text = [] then s
  else
    let items := s.items ++ [{ id := s.nextId, text := String.ofList (trimmed s.field.text) }]
    { s with items, nextId := items.length + 1, field := Text.Field.empty placeholder }

The tests pass. As long as nothing is deleted before an add, the number of items is the number of ids handed out, so the slip gives the same ids. The fixture's own tests add two items, check one off and delete at the end; the same steps, on addBuggy:

/-- `s` with `t` typed into the New item field. -/
def typing (t : String) (s : State) : State := { s with field := { s.field with text := t.toList } }

def ids (s : State) : List Nat := s.items.map (·.id)

-- The fixture's tests: add milk, add eggs, check one off. Same ids, same next id as `add`.
#guard ids (addBuggy (typing "eggs" (addBuggy (typing "milk" {})))) == [1, 2]
#guard (addBuggy (typing "eggs" (addBuggy (typing "milk" {})))).nextId == 3
-- Blank text adds nothing, and deleting at the end leaves the rest.
#guard addBuggy (typing "  " {}) == typing "  " {}
#guard ids (delete 2 (addBuggy (typing "eggs" (addBuggy (typing "milk" {}))))) == [1]

The proof doesn't. ^7's step needs a proof that add keeps the invariant, and the one that works for add stops at the next id. This is that proof, written for addBuggy, with the message Lean gives. #guard_msgs makes the build check that the attempt fails with exactly this message:

/--
error: omega could not prove the goal:
a possible counterexample may satisfy the constraints
  c ≥ 0
  b ≥ 0
  b - c ≥ 2
  a ≥ 1
  a - b ≥ 0
where
 a := ↑s.nextId
 b := ↑i.id
 c := ↑s.items.length
-/
#guard_msgs in
/-- ^7's step for `addBuggy`, written like `add_inv`. It fails, and `#guard_msgs` checks that it
fails with exactly this message. -/
example {s : State} (h : Inv s) : Inv (addBuggy s) := by
  obtain ⟨hn, hb⟩ := h
  unfold addBuggy
  split
  · exact ⟨hn, hb⟩
  · refine ⟨Nat.succ_pos _, fun i hi => ?_⟩
    simp only [List.mem_append, List.mem_singleton, List.length_append,
      List.length_singleton] at hi ⊢
    have : i.id < s.nextId + 1 := by
      rcases hi with hi | rfl
      · exact Nat.lt_succ_of_lt (hb i hi)
      · exact Nat.lt_succ_self _
    omega

Read the constraints as a description of the bug. b is an item's id and c the number of items before the add; the new next id is c + 2, and b - c ≥ 2 says the item's id isn't below it. That needs an id at least two more than the number of items: more ids handed out than items left. So the failing case is an add after a delete. Lean didn't need a test to find it. It made it concrete, and it can be proved:

/-- Add milk and eggs, then delete milk: one item left, and the next id is 3. -/
def eggsLeft : State := { items := [⟨2, "eggs", false⟩], nextId := 3 }

/-- The state the failed proof asks about: more ids issued than items left. Adding bread to
`eggsLeft` with `addBuggy` gives it id 3 and sets the next id to 3, so ^7 no longer holds. -/
theorem addBuggy_breaks : Inv eggsLeft ∧ ¬ Inv (addBuggy (typing "bread" eggsLeft)) := by
  refine ⟨⟨by decide, fun i hi => ?_⟩, fun h => ?_⟩
  · simp only [eggsLeft, List.mem_singleton] at hi; subst hi; decide
  · have hid : ids (addBuggy (typing "bread" eggsLeft)) = [2, 3] := by decide
    have hn : (addBuggy (typing "bread" eggsLeft)).nextId = 3 := by decide
    have h3 : 3 ∈ ids (addBuggy (typing "bread" eggsLeft)) := by rw [hid]; decide
    obtain ⟨it, hit, he⟩ := List.mem_map.mp h3
    have := h.2 it hit
    omega

What the other evidence would have said. With the bug planted in the fixture, cairn fuzz with its defaults (100 random sequences from seed 0) failed ^7 in 27 of them, the first at step 23 of seed 4. Fuzzing would very likely have caught this one. Conformance and a capture would not have: the app would match its own buggy model, frame for frame, and the screenshots would look fine. The proof is the only evidence that guarantees the case is covered, rather than likely to have come up. And because the fixture's invariant is proved, make check fails before this change can merge.

Checking a claim yourself

1. Read the claim. Its entry in the API reference shows its does and sees, its formal statement, its proofs and its evidence. Check that the statement says what the prose does.
2. Look for assumptions. Find the package's assume claims among its claims, and read the trusted base. Every proof you rely on takes those as given.
3. Run the checks. Cairn's make check, or a package's own, builds every proof, audits its axioms, replays the kernel and runs the ledger; cairn fuzz and cairn conformance gather the rest. Evidence you built is evidence you don't have to take on anyone's word.