Proving a claim

A claim's evidence comes at several strengths. The strongest is a proof that Lean's kernel has checked, using only the three standard axioms. This chapter shows the proofs a small app has, in the order you meet them.

The proof a move needs

A move's sound clause proves that its handler meets its post, for every state (and every key and text operation) where the move is enabled. For an item's checkbox, apply flips the item and post says the items are the old ones with that item flipped, so both sides compute to the same thing and rfl closes it:

move ^4 toggleItem (s : State) (k : Nat) "Toggle an item" in ^1 where
  does "Press an item's checkbox."
  sees "The item is marked done, or not done again."
  enabled := has s k
  on press
    apply := toggle k s
    post s' := s'.items = s.items.map (flip k)
    sound := by intro s k _; rfl

Most moves are like that: post restates apply in the terms a reader cares about, and the proof is rfl, a tuple of rfls, or a lemma about the model. When a proof needs real logic about a function the app calls, prove a lemma about that function next to it and cite it. The fixture's invariant does that for add:

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

Checks you get for free

Flows are proved by evaluation: decide runs the witness through the machine at compile time. You can do the same for any small fact with example … := by decide. The framework's own theorem update_unclaimed gives facts about every input at once: an action whose claim no move of the app has changes nothing and asks nothing of the host, so an app never has to prove that about a stray click.

Presence: the control is there exactly when the move is enabled

A move's enabled says when it is available. Whether its control is actually on screen is a question about the view, so the app proves it: the control's ref is among the view's controls exactly when the move is enabled. A counter proves it for a Reset button that is there only when the count is above zero.

The framework's layout and frame theorems (Frame.controls_ofLaid_layout) carry that through to every frame the running app shows: the accessibility tree of the frame, for any text measurements and any window size.

Pressable: a click at its centre presses it

Being in the tree isn't enough: another node could be painted over the control, or it could be laid out with no size. Hit testing is Lean, so this is a theorem too. For a rigid view (chapter 3) the framework reduces it to a condition on the view alone, FitsIn, proved once for every window above a minimum size. A view that isn't rigid, like the fixture's, is checked one concrete layout at a time: checkPressable decides it for a laid-out frame, and pressable_of_check turns that into the theorem. The fuzzer checks that each enabled move's control is pressable at its centre, in every state it reaches.

The runtime's own theorems take it from there: if the pointer reaches a control at its centre, a pointer down and up there deliver exactly a press of that control to update.

Invariants

An invariant's proof is the most work in a typical app: init for the starting state, then one obligation per handler, each saying that handler keeps the property. The chapter on moves and flows shows the shape. The fixture's ^7 needs three short lemmas, add_inv, toggle_inv and delete_inv, one per function that changes the items. A count of items left takes about thirty lines of ordinary list reasoning.

Runtime checks

Some things are easier to check by running than by proving. #guard runs code at compile time; the fixture's tests drive the real runtime, with clicks found by hit testing and frames through the real byte encoding:

def typed : List Event :=
  clickOn (run []) fieldRef ++ [.insertText "  milk ", .key .enter {}, .insertText "eggs"]
def two : List Event := typed ++ clickOn (run typed) addRef

#guard texts (st typed) == [(1, "milk", false)]
#guard texts (st two) == [(1, "milk", false), (2, "eggs", false)]
def toggled : List Event := two ++ clickOn (run two) (toggleRef 1)
#guard texts (st toggled) == [(1, "milk", true), (2, "eggs", false)]
#guard left (st toggled) == 1
def deleted : List Event := toggled ++ clickOn (run toggled) (deleteRef 2)
#guard texts (st deleted) == [(1, "milk", true)]
/-- The buttons under Flash: Top, End, Go to row, Hide rows, then Badge, Clear badge, Announce. -/
def moreRefs : List ControlRef :=
  [topRef, endButtonRef, goRowRef, hideRef, badgeRef, clearBadgeRef, announceRef]
-- Tab order: field, Add, Passcode, Flash, Add above, Add below, the buttons under them, then each
-- item's checkbox, delete button and ⋯, the posts' Like buttons and Refresh (and then the list's
-- rows, `notRow`).
#guard ((tabOrder (run two).laid).map (·.ref)).filter notRow ==
  [fieldRef, addRef, passRef, flashRef, addTopRef, addEndRef] ++ moreRefs ++
  [toggleRef 1, deleteRef 1, moreRef 1, toggleRef 2, deleteRef 2, moreRef 2, likeRef 1, likeRef 2,
   likeRef 3, likeRef 4, refreshRef]
-- Flash sets its timer; the note shows until it fires.
def flashed : List Event := clickOn (run []) flashRef
#guard (st flashed).flash
-- The frame through the v1 boundary carries the keyed controls.
#guard ((decodeFrame (frameBytes Frame.boundary (run two))).map fun f =>
  (f.ax.toList.filterMap (·.control)).filter notRow) ==
  some ([fieldRef, addRef, passRef, flashRef, addTopRef, addEndRef] ++ moreRefs ++
        [toggleRef 1, deleteRef 1, moreRef 1, toggleRef 2, deleteRef 2, moreRef 2, likeRef 1,
         likeRef 2, likeRef 3, likeRef 4, refreshRef])

The rules

These hold for every proof that counts as evidence, and make check enforces them:

• No sorry. An unfinished proof fails the build.
• Only the standard axioms: propext, Classical.choice and Quot.sound. The axiom audit looks at every theorem.
• No escape hatches: native_decide, bv_decide, implemented_by, debug.skipKernelTC and axiom are rejected by a lint, and every declaration is replayed through the kernel.

What a proof still leaves you to trust, and what the other kinds of evidence add, is on How much to trust a claim. For proofs about geometry, omega does most of the work, since layout is integers. For bounded enumerations, decide +kernel. For lists of nodes, write recursion structurally: children.map f makes a definition that rfl and decide can't see through.