# How much to trust a claim

> What each kind of evidence rules out, what it still takes on trust, and a bug that tests miss and a proof can't.

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](https://cairn.iamnbutler.workers.dev/docs/reference/evidence.md) says how the build computes them.

| Evidence | Rules out | Still trusts |
|---|---|---|
| **proved** | a counterexample anywhere: every state, every key, every input | that the statement says what you mean; Lean's kernel and compiler; the trusted base |
| **fuzzed** | a counterexample in the sequences the fuzzer ran | that the random sequences reach the case that matters |
| **tested** | the running app disagreeing with the model, on the sequences run | the conformance harness; nothing about sequences it didn't run |
| **seen** | a control that is never drawn, a flow that can't be clicked through | the capture, which renders the model's frames, not the running window |
| **assumed** | nothing | whoever wrote it, and the checks that gather evidence for it |

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](https://cairn.iamnbutler.workers.dev/docs/api/claims.html) 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](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md), 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](https://github.com/iamnbutler/cairn/issues/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](https://cairn.iamnbutler.workers.dev/docs/internals/trusted-base.md) 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:

```lean
/-- ^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 _
```

`test/fixture/lean/Fixture.lean`, lines 191–204

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

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

`test/fixture/lean/Fixture.lean`, lines 164–173

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

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

`test/fixture/lean/Fixture/Mutant.lean`, lines 11–17

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

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

`test/fixture/lean/Fixture/Mutant.lean`, lines 21–31

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

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

`test/fixture/lean/Fixture/Mutant.lean`, lines 35–63

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:

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

`test/fixture/lean/Fixture/Mutant.lean`, lines 67–80

**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](https://cairn.iamnbutler.workers.dev/docs/api/claims.html) 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.

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