swaits
47c0e4396e
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.
319 lines
14 KiB
Lean4
319 lines
14 KiB
Lean4
import Wanderbooks.Entry
|
|
|
|
/-!
|
|
# Documents are the subledgers of their control accounts (rules.md B-38)
|
|
|
|
Every ledger line may carry the document it belongs to (an invoice or a
|
|
bill: `Ledger.line_docs`, `arap::DocTag`). A document's figures are the
|
|
sum of its tagged lines; a control account's balance is the sum of every
|
|
line on it. Mirrors `Ledger::doc_state` (outstanding), `control_check`,
|
|
the control guard (`check_control_lines`: every line a command posts on a
|
|
control account carries its document) and `reverse_entry` (a mirror line
|
|
copies its original's tag).
|
|
|
|
The headline, `control_agrees`: for every account and any lines at all,
|
|
the account's balance is the sum over the documents of what each carries
|
|
on it, plus its untagged ("unattached") lines. Both sides sum the same
|
|
lines, so it is an identity, not a reconciliation, and it holds through
|
|
any date, since a date is a filter on the lines. A document is one `Nat`
|
|
here: an injective coding of `DocRef` (invoices and bills in one id
|
|
space), which is all the sums need. Then, over the commands:
|
|
a document step (an invoice, a bill, a payment, or any entry whose
|
|
control lines are tagged) never moves what is unattached; a reversal
|
|
moves each document, and what is unattached, by exactly the opposite of
|
|
the lines it mirrors (B-38 INVARIANT 3); so books built by these steps
|
|
alone have nothing unattached on a control account, ever
|
|
(`Reachable.unattached_zero`).
|
|
-/
|
|
|
|
namespace Wanderbooks.Documents
|
|
|
|
open Wanderbooks
|
|
|
|
/-- A posted line, its day, and the document it carries (`none`: none). -/
|
|
structure TLine where
|
|
line : Line
|
|
date : Nat
|
|
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
|
|
|
|
/-- Account `a`'s balance over some lines (the general ledger). -/
|
|
def gl (a : Nat) : List TLine → Int
|
|
| [] => 0
|
|
| l :: ls => onAcct a l + gl a ls
|
|
|
|
/-- What document `d`'s lines on account `a` sum to (`doc_lines`). -/
|
|
def docSum (a d : Nat) : List TLine → Int
|
|
| [] => 0
|
|
| l :: ls => (if l.doc = some d then onAcct a l else 0) + docSum a d ls
|
|
|
|
/-- Account `a`'s lines that carry no document. -/
|
|
def unattached (a : Nat) : List TLine → Int
|
|
| [] => 0
|
|
| l :: ls => (if l.doc = none then onAcct a l else 0) + unattached a ls
|
|
|
|
@[simp] theorem gl_nil (a : Nat) : gl a [] = 0 := rfl
|
|
@[simp] theorem docSum_nil (a d : Nat) : docSum a d [] = 0 := rfl
|
|
@[simp] theorem unattached_nil (a : Nat) : unattached a [] = 0 := rfl
|
|
|
|
theorem gl_append (a : Nat) (xs ys : List TLine) : gl a (xs ++ ys) = gl a xs + gl a ys := by
|
|
induction xs with
|
|
| nil => simp
|
|
| cons x xs ih => simp only [List.cons_append, gl, ih]; omega
|
|
|
|
theorem docSum_append (a d : Nat) (xs ys : List TLine) :
|
|
docSum a d (xs ++ ys) = docSum a d xs + docSum a d ys := by
|
|
induction xs with
|
|
| nil => simp
|
|
| cons x xs ih => simp only [List.cons_append, docSum, ih]; omega
|
|
|
|
theorem unattached_append (a : Nat) (xs ys : List TLine) :
|
|
unattached a (xs ++ ys) = unattached a xs + unattached a ys := by
|
|
induction xs with
|
|
| nil => simp
|
|
| cons x xs ih => simp only [List.cons_append, unattached, ih]; omega
|
|
|
|
/-- Every document some lines carry is among `ds`. -/
|
|
def Covers (ds : List Nat) (ls : List TLine) : Prop :=
|
|
∀ l ∈ ls, ∀ k, l.doc = some k → k ∈ ds
|
|
|
|
/-- **The control account agrees with its documents** (B-38 INVARIANT 1):
|
|
for any lines, any account, and any distinct document ids covering the
|
|
lines' tags, the balance is the documents' sum plus what is unattached. -/
|
|
theorem control_agrees (a : Nat) (ds : List Nat) (hd : Distinct ds) :
|
|
∀ ls : List TLine, Covers ds ls →
|
|
gl a ls = sumOver (fun d => docSum a d ls) ds + unattached a ls := by
|
|
intro ls
|
|
induction ls with
|
|
| nil => intro _; simp [sumOver_zero]
|
|
| cons l ls ih =>
|
|
intro hc
|
|
have hc' : Covers ds ls := fun m hm => hc m (List.mem_cons_of_mem _ hm)
|
|
simp only [gl, docSum, unattached]
|
|
rw [sumOver_add, ih hc']
|
|
cases h : l.doc with
|
|
| none =>
|
|
simp [sumOver_zero] <;> omega
|
|
| some k =>
|
|
have hk : k ∈ ds := hc l (List.mem_cons_self ..) k h
|
|
have e : sumOver (fun d => if some k = some d then onAcct a l else 0) ds
|
|
= sumOver (fun d => if k = d then onAcct a l else 0) ds :=
|
|
sumOver_congr _ _ ds (fun d _ => by simp)
|
|
simp only [e, sumOver_indicator k (onAcct a l) ds hd hk]
|
|
simp <;> omega
|
|
|
|
/-- The lines dated on or before day `D`. -/
|
|
def through (D : Nat) (ls : List TLine) : List TLine := ls.filter (fun l => decide (l.date ≤ D))
|
|
|
|
theorem Covers.through {ds : List Nat} {ls : List TLine} (h : Covers ds ls) (D : Nat) :
|
|
Covers ds (through D ls) := fun l hl => h l (List.mem_filter.1 hl).1
|
|
|
|
/-- **The same through any day**: GL(A, D) = Σ_docs outstanding(d, D) +
|
|
unattached(A, D). -/
|
|
theorem control_agrees_through (a : Nat) (ds : List Nat) (hd : Distinct ds) (ls : List TLine)
|
|
(hc : Covers ds ls) (D : Nat) :
|
|
gl a (through D ls) = sumOver (fun d => docSum a d (through D ls)) ds
|
|
+ unattached a (through D ls) :=
|
|
control_agrees a ds hd _ (hc.through D)
|
|
|
|
/-! ## The commands -/
|
|
|
|
/-- A line mirrored by a reversal: its side flipped, its day the
|
|
reversal's, its document kept (`reverse_entry_steps` copies the tag). -/
|
|
def mirror (D : Nat) (l : TLine) : TLine := { l with line := l.line.reverse, date := D }
|
|
|
|
theorem onAcct_mirror (a D : Nat) (l : TLine) : onAcct a (mirror D l) = -onAcct a l := by
|
|
unfold onAcct mirror
|
|
by_cases h : l.line.account = a
|
|
· simp [Line.reverse, h]
|
|
have := Line.reverse_signed l.line
|
|
simp [Line.reverse] at this
|
|
exact this
|
|
· simp [Line.reverse, h]
|
|
|
|
theorem docSum_mirror (a d D : Nat) (ls : List TLine) :
|
|
docSum a d (ls.map (mirror D)) = -docSum a d ls := by
|
|
induction ls with
|
|
| nil => simp
|
|
| cons l ls ih =>
|
|
simp only [List.map_cons, docSum, ih, onAcct_mirror]
|
|
have : (mirror D l).doc = l.doc := rfl
|
|
rw [this]
|
|
by_cases h : l.doc = some d <;> simp [h] <;> omega
|
|
|
|
theorem unattached_mirror (a D : Nat) (ls : List TLine) :
|
|
unattached a (ls.map (mirror D)) = -unattached a ls := by
|
|
induction ls with
|
|
| nil => simp
|
|
| cons l ls ih =>
|
|
simp only [List.map_cons, unattached, ih, onAcct_mirror]
|
|
have : (mirror D l).doc = l.doc := rfl
|
|
rw [this]
|
|
by_cases h : l.doc = none <;> simp [h] <;> omega
|
|
|
|
/-- Every line of `ls` on a control account carries a document: what the
|
|
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),
|
|
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
|
|
lines, mirror for mirror, each keeping its tag (`Step.reverse`), dated on
|
|
or after them (B-38, "Dating rules"); assigning a document role an
|
|
account all of whose lines are documents' (`Step.assign`:
|
|
`check_assign_role` SCENARIO 6 refuses one holding an untagged line); and
|
|
an account leaving the control accounts once it holds no document's line
|
|
(`Step.release`: an assigned role moved off an account no document posted
|
|
to; an account holding a document's line stays guarded,
|
|
`control_role_of`). -/
|
|
inductive Step : Books → Books → Prop
|
|
| document (B : Books) (e : List TLine) (h : Tagged B.control e) :
|
|
Step B { B with lines := B.lines ++ e }
|
|
| reverse (B : Books) (e : List TLine) (he : ∀ l ∈ e, l ∈ B.lines) (D : Nat) :
|
|
Step B { B with lines := B.lines ++ e.map (mirror D) }
|
|
| assign (B : Books) (c : Nat) (h : ∀ l ∈ B.lines, l.line.account = c → l.doc ≠ none) :
|
|
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. -/
|
|
theorem Step.document_unattached (B : Books) (e : List TLine) (h : Tagged B.control e)
|
|
(a : Nat) (ha : a ∈ B.control) : unattached a (B.lines ++ e) = unattached a B.lines := by
|
|
rw [unattached_append]
|
|
suffices unattached a e = 0 by omega
|
|
induction e with
|
|
| nil => rfl
|
|
| cons l ls ih =>
|
|
simp only [unattached]
|
|
rw [ih (fun m hm => h m (List.mem_cons_of_mem _ hm))]
|
|
by_cases hn : l.doc = none
|
|
· have hacc : l.line.account ≠ a := fun e => h l (List.mem_cons_self ..) (e ▸ ha) hn
|
|
simp [hn, onAcct, hacc]
|
|
· simp [hn]
|
|
|
|
/-- **A reversal moves each document by exactly the opposite of its lines
|
|
it mirrors** (B-38 INVARIANT 3), and what is unattached likewise: only
|
|
reversing a legacy hand line changes it. -/
|
|
theorem Step.reverse_moves (B : Books) (e : List TLine) (D a d : Nat) :
|
|
docSum a d (B.lines ++ e.map (mirror D)) = docSum a d B.lines - docSum a d e
|
|
∧ unattached a (B.lines ++ e.map (mirror D)) = unattached a B.lines - unattached a e := by
|
|
rw [docSum_append, docSum_mirror, unattached_append, unattached_mirror]
|
|
omega
|
|
|
|
/-- **Reversing a reversal restores every document** (B-10): the lines,
|
|
mirrored twice, sum as the originals did. -/
|
|
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, [], []⟩
|
|
| 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
|
|
induction r with
|
|
| empty => intro l hl; simp at hl
|
|
| step _ s ih =>
|
|
cases s with
|
|
| document e h =>
|
|
intro l hl hc
|
|
rcases List.mem_append.1 hl with hl | hl
|
|
· exact ih l hl hc
|
|
· exact h l hl hc
|
|
| reverse e he D =>
|
|
intro l hl hc
|
|
rcases List.mem_append.1 hl with hl | hl
|
|
· exact ih l hl hc
|
|
· obtain ⟨m, hm, rfl⟩ := List.mem_map.1 hl
|
|
exact ih m (he m hm) (by simpa [mirror, Line.reverse] using hc)
|
|
| assign c h =>
|
|
intro l hl hc
|
|
rcases List.mem_cons.1 hc with hc | hc
|
|
· exact h l hl hc
|
|
· exact ih l hl hc
|
|
| 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:
|
|
every control line is a document's. (Books an earlier version wrote, with
|
|
hand lines, are covered by the identity `control_agrees` alone; an
|
|
account becoming a control account by its first document, holding lines
|
|
from before, is outside the model: `control_check` lists those lines.) -/
|
|
theorem Reachable.unattached_zero {B : Books} (r : Reachable B) (a : Nat) (ha : a ∈ B.control)
|
|
(D : Nat) : unattached a (through D B.lines) = 0 := by
|
|
have ht := r.tagged
|
|
have : ∀ ls : List TLine, (∀ l ∈ ls, l ∈ B.lines) → unattached a ls = 0 := by
|
|
intro ls
|
|
induction ls with
|
|
| nil => intro _; rfl
|
|
| cons l ls ih =>
|
|
intro hs
|
|
simp only [unattached]
|
|
rw [ih (fun m hm => hs m (List.mem_cons_of_mem _ hm))]
|
|
by_cases hn : l.doc = none
|
|
· have hacc : l.line.account ≠ a :=
|
|
fun e => ht l (hs l (List.mem_cons_self ..)) (e ▸ ha) hn
|
|
simp [hn, onAcct, hacc]
|
|
· simp [hn]
|
|
exact this _ (fun l hl => (List.mem_filter.1 hl).1)
|
|
|
|
/-- **So the control account is its documents**, exactly, on every day:
|
|
GL(A, D) = Σ_docs outstanding(d, D). -/
|
|
theorem Reachable.control_is_documents {B : Books} (r : Reachable B) (a : Nat)
|
|
(ha : a ∈ B.control) (ds : List Nat) (hd : Distinct ds) (hc : Covers ds B.lines) (D : Nat) :
|
|
gl a (through D B.lines) = sumOver (fun d => docSum a d (through D B.lines)) ds := by
|
|
rw [control_agrees_through a ds hd B.lines hc D, r.unattached_zero a ha D]; omega
|
|
|
|
end Wanderbooks.Documents
|