From 47c0e4396ec04e7535d0ba72f0cf521a8b88e3df Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Tue, 27 Oct 2026 07:19:57 -0600 Subject: [PATCH] verify(lean): Step.markSent, a send moves no figure (P4b S5) AGENTS.md's formal-methods bar makes every new Ledger command a Lean Step with a preservation proof, so `Ledger::mark_sent` gets one even though the unit expected no Lean change (the As-built block records that). `Documents.lean`'s `Books` gains the sends recorded, and `Step.markSent` adds one on a document the lines carry. A send touches no line, so every control balance, every document's sum and what is unattached are unchanged through any day (`Step.markSent_changes_no_figure`, no axioms), and `Reachable.tagged` covers the new step. `Audit.lean` lists the theorem; rules.md B-38's model now covers the record side of a document's life as well as its figures. --- docs/verification.md | 18 +++++++++++ verify/lean/Audit.lean | 1 + verify/lean/Wanderbooks/Documents.lean | 44 ++++++++++++++++++++++++-- 3 files changed, 60 insertions(+), 3 deletions(-) diff --git a/docs/verification.md b/docs/verification.md index 9d03108..7762f45 100644 --- a/docs/verification.md +++ b/docs/verification.md @@ -504,6 +504,24 @@ come from the kernel: No Lean model: these are two arithmetic laws, not a new `Ledger` command (S4.1 adds fields to the existing document commands). +### Sent tracking (P4b S5) + +34. **A send changes no figure.** `Ledger::mark_sent` is a command, so it + is a `Step` in the model (AGENTS.md's formal-methods bar; the unit's + "no Lean change" phrase was overruled by it, and says so in its As + built block). `Documents.lean`'s `Books` gains `sends`, and + `Step.markSent` records one on a document the lines carry, touching + no line. Every control balance, every document's sum and what is + unattached are therefore the same before and after, through any day, + and `Reachable.tagged` (the control lines are all documents') covers + the new step; the engine's side is the same statement, checked by + `a_send_changes_no_figure` on the fixture book. + - Lean `Documents.Step.markSent_changes_no_figure` (no axioms) · + `Documents.Reachable.tagged`, `Documents.Reachable.control_is_documents` + cover the new step · tests `sends_replay_and_project`, + `a_send_changes_no_figure`, `mark_sent_on_void_refused`, + `mark_sent_waits_for_documents_v2` + ## What the proofs found The engine already had 190+ tests, property tests, mutation testing, diff --git a/verify/lean/Audit.lean b/verify/lean/Audit.lean index c015231..dd05949 100644 --- a/verify/lean/Audit.lean +++ b/verify/lean/Audit.lean @@ -94,5 +94,6 @@ open Wanderbooks #print axioms Documents.Step.document_unattached #print axioms Documents.Step.reverse_moves #print axioms Documents.reverse_twice +#print axioms Documents.Step.markSent_changes_no_figure #print axioms Documents.Reachable.unattached_zero #print axioms Documents.Reachable.control_is_documents diff --git a/verify/lean/Wanderbooks/Documents.lean b/verify/lean/Wanderbooks/Documents.lean index 4575fc3..17ed148 100644 --- a/verify/lean/Wanderbooks/Documents.lean +++ b/verify/lean/Wanderbooks/Documents.lean @@ -37,6 +37,15 @@ structure TLine where doc : Option Nat deriving DecidableEq +/-- A recorded send of an invoice (plan P4b S5, `Sent`, `invoice.sent`): +the invoice, the day, and a code for who sent it, how, to whom and the +channel's own reference. No figure reads it: a send moves no money. -/ +structure Send where + doc : Nat + day : Nat + code : Nat + deriving DecidableEq + /-- A line's signed amount on account `a` (zero on another account). -/ def onAcct (a : Nat) (l : TLine) : Int := if l.line.account = a then l.line.signed else 0 @@ -159,11 +168,17 @@ control guard requires of every entry a command posts. -/ def Tagged (control : List Nat) (ls : List TLine) : Prop := ∀ l ∈ ls, l.line.account ∈ control → l.doc ≠ none -/-- The books: the control accounts (the receivables and payables roles) -and every posted line, in order. -/ +/-- The books: the control accounts (the receivables and payables roles), +every posted line in order, and the sends recorded (each on its invoice; +plan P4b S5). -/ structure Books where control : List Nat lines : List TLine + sends : List Send + +/-- The documents some lines carry: the invoices a send can name. -/ +def Books.docs (B : Books) : List Nat := + B.lines.filterMap (fun l => l.doc) /-- What the engine allows (S1): a document command, or any entry whose control lines are all tagged (`Step.document`); a reversal of posted @@ -184,6 +199,11 @@ inductive Step : Books → Books → Prop Step B { B with control := c :: B.control } | release (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc = none) : Step B { B with control := B.control.erase c } + /-- `mark_sent` (`Ledger::mark_sent`, plan P4b S5): a send is recorded on + an invoice the books hold, and nothing else changes. It moves no line, + so every figure stays where it was. -/ + | markSent (B : Books) (s : Send) (h : s.doc ∈ B.docs) : + Step B { B with sends := s :: B.sends } /-- **A document step never moves what is unattached** on a control account: no command adds an untagged control line. -/ @@ -216,9 +236,24 @@ theorem reverse_twice (a d D D' : Nat) (e : List TLine) : docSum a d ((e.map (mirror D)).map (mirror D')) = docSum a d e := by rw [docSum_mirror, docSum_mirror]; omega +/-- **A send changes no figure** (plan P4b S5): recording one leaves every +control account's balance, every document's sum on it and what is +unattached exactly as they were, through any day. A send adds a record and +no line, so the engine's own statement (`Ledger::mark_sent`) that a +document's DocState is the same before and after is this, line for line. -/ +theorem Step.markSent_changes_no_figure (B : Books) (s : Send) (_h : s.doc ∈ B.docs) + (a d D : Nat) : + gl a (through D ({ B with sends := s :: B.sends } : Books).lines) + = gl a (through D B.lines) + ∧ docSum a d (through D ({ B with sends := s :: B.sends } : Books).lines) + = docSum a d (through D B.lines) + ∧ unattached a (through D ({ B with sends := s :: B.sends } : Books).lines) + = unattached a (through D B.lines) := by + exact ⟨rfl, rfl, rfl⟩ + /-- States reachable from books with no lines. -/ inductive Reachable : Books → Prop - | empty (control : List Nat) : Reachable ⟨control, []⟩ + | empty (control : List Nat) : Reachable ⟨control, [], []⟩ | step {B B' : Books} : Reachable B → Step B B' → Reachable B' theorem Reachable.tagged {B : Books} (r : Reachable B) : Tagged B.control B.lines := by @@ -245,6 +280,9 @@ theorem Reachable.tagged {B : Books} (r : Reachable B) : Tagged B.control B.line | release c h => intro l hl hc exact ih l hl (List.mem_of_mem_erase hc) + | markSent _ _ => + -- A send touches no line: the control lines are the ones it found. + exact ih /-- **Nothing is ever unattached on a control account** in books these steps build, through any day, roles assigned and released included: