saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-04 20:03:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
ltl-accumulator-verified/verification/Proofs/AxiomCheck.lean

66 lines
2.1 KiB
Text
Raw Normal View History

L1+L2: hashing shapes, domain separation, MTH/Root/ConsRec with termination Accumulator pyramid layers 1-2, mechanizing paper SS5.3/SS6 groundwork: - gen/LTLAcc/HashExternal.lean: the single sanctioned axiom, opaque sha256 (no properties assumed - the soundness theorems downstream are constructive collision extractors). - Proofs/Basic.lean: hleaf/hnode (0x00/0x01 domain stamps); Lemma 1 (domsep) proven AXIOM-FREE; kbelow (largest power of two below n) with pos/lt/le-two bound lemmas; MTH, Root (Option = rejection), ConsRec (four cases, b-flag, pinned anchor) - all with kernel-checked termination via the kbelow bounds. - check.sh: estate discipline (stub audit, axiom-smuggling gate, lean-guard compilation, boundary-exact per-certificate cone audit). All green; observed cones pinned exactly. Zero contact with the live LTL: no appends, no server, accumulator frozen at 12 leaves throughout this project. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-10 21:58:00 +00:00
/- Axiom-cone observation for the audit (Phase 3 of check.sh). -/
import Proofs.Basic
L3: Theorem 1 (inclusion completeness) kernel-checked Path (prover-side inclusion path, paper SS5.3) with termination via the kbelow bounds; self-contained list lemmas (getD_take, getD_drop - no stdlib-name dependence); equation lemmas MTH_single/MTH_split/Root_one/ Root_left/Root_right (Option.map form; matcher side conditions closed explicitly); Theorem 1 by functional induction on Path with a k-fold discipline against the let-bound split point. incl_complete cone: [propext, Classical.choice, LTLAcc.sha256, Quot.sound] - pinned exactly in check.sh alongside Path. THE button green end to end. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 10:06:20 +00:00
import Proofs.Completeness
S3.5: explicit collision extractor — Theorem 2 made non-vacuous, vacuous forms removed The S3 Socratic re-audit found incl_sound was kernel-perfect but VACUOUS: its '... ∨ HasCollision' disjunct (∃ x y, x≠y ∧ sha256 x = sha256 y) is provable by pigeonhole ALONE (sha256: infinite List UInt8 → finite 32-byte Hash), so the theorem said nothing about forgeries. Even a data-carrying {p // IsCollision p} disjunct fails (Classical.choice inhabits it). The only faithful rendering of the paper's 'explicit algorithm 𝓔' is a NAMED FUNCTION whose correctness is a claim about ITS OUTPUT. - extractIncl (m D d P): total function that walks the honest tree and returns the concrete colliding preimage pair at the first divergence (a node preimage pair, or the leaf preimage pair at the bottom). - extractIncl_correct: d ≠ D[m] ∧ accepting-receipt → IsCollision (extractIncl …).1 (extractIncl …).2. A statement ABOUT the fixed function's output; pigeonhole cannot discharge it. ADVERSARIAL CHECK (probe, since removed): proved ¬ IsCollision (extractIncl 0 [[7]] [7] []) — i.e. on a NON-forgery input the output is provably NOT a collision, so the conclusion is genuinely false for some inputs ⇒ non-vacuous, choice-proof. - Removed the vacuous theorems entirely (incl_sound, root_binding, hnode/hleaf_inj_or_collision, HasCollision def) so no hollow statement survives in a corpus destined for the log. Kept the real building blocks (hnode_preimage_inj [propext]; eq_dropLast helper moved to Completeness; Binding.lean deleted). extractIncl_correct cone [propext, Classical.choice, LTLAcc.sha256, Quot.sound]. THE button green (14 certs). Fable statement-audit passed. LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 13:31:21 +00:00
import Proofs.Extract
S4: descent extractor extractMTH (Theorem 3 step 3 + F2 restoration), non-vacuous The 'descend' step of the paper's Theorem 3, built extractor-first per the S3.5 lesson (never a bare '∨ collision'): - extractMTH (D D'): total function that, given two equal-length leaf lists sharing a Merkle root, walks the common-shape tree to the first divergence and returns the concrete colliding preimage pair (a node pair, or a leaf pair at the bottom). - extractMTH_correct: |D|=|D'| ∧ D≠D' ∧ MTH D = MTH D' → IsCollision (extractMTH D D'). Proven by functional induction on extractMTH; composite case uses MTH_split + append_inj (fixed-width Hash) to split node preimages or exhibit the node collision. - extractMTH_nonvacuous: equal lists → output NOT a collision (pinned), so the conclusion is false for some inputs ⇒ choice-proof. This also RESTORES, in explicit non-vacuous form, the receipt-uniqueness content of Lemma 2 deleted in the S3.5 cleanup (re-audit F2): the honest Merkle fold is injective up to a collision. 18 certs green. Fable statement-audit passed (matches paper Thm 3 step 3 verbatim). LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 14:46:58 +00:00
import Proofs.Descent
S5 stage 1: consistency infrastructure (kbelow prefix-split + list surgery) Theorem 3's binding (steps 1-2) turns on one non-obvious arithmetic fact, isolated and proven here before the main proof: - pow2_exp_unique / kbelow_eq_of_pow2_between: kbelow is pinned by its three defining inequalities (power-of-two, k<n≤2k), so a prefix that spills past the left subtree splits at the SAME point. - kbelow_prefix_eq: with k=kbelow n, 2≤n, k<n₀≤n ⇒ kbelow n₀ = k (the fact the n₀>k recursion branch needs to align MTH(D₁.take n₀) with the fold). - take_take_le, take_drop_prefix: the list-surgery identities relating (D.take n₀) to D.take k and (D.drop k).take (n₀-k). Cones pinned; 21 certs green. Deliberate honest checkpoint — binding + extractCons assembly is the next stage. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 15:53:43 +00:00
import Proofs.Consistency
S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) The single hardest proof in the corpus is complete, no sorry. Under the value-equality invariant y = MTH D₁, an accepting ConsRec fold either makes extractConsNode output a genuine collision or its first component is the honest prefix root MTH(D₁.take n₀). - ConsRec base changed from list-match to decidable if (if C=[] / if C.length=1) — same root-cause fix as Root, avoids WF-unfold exhaustiveness obligations; more faithful to the deployed Python. Whole chain (Basic..Consistency) rebuilt clean. - consRecBinding by ConsRec.induct (10 cases): 4 base/singleton, 3 rejection/none contradictions, 2 recursive (n₀≤k, n₀>k). The n₀>k none-branch is where all S5.1 infrastructure interlocks: kbelow_prefix_eq (prefix splits at same k) + take_take_le + take_drop_prefix assemble x = hnode s xx into MTH(D₁.take n₀). The collision branches use append_inj (fixed-width Hash) + MTH_split. - take_all helper (take-whole-list). Cone [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — single hash axiom. 24 certs green. Fable statement-audit: matches paper Thm 3 steps 1-2. LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 17:18:26 +00:00
import Proofs.Binding3
S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) Re-derived S5.3 (all done under an Opus switch) from zero. consRecBinding STATEMENT re-confirmed faithful to paper Thm 3 steps 1-2 (y=MTH D₁ = the hash-fold condition; some=>collision / none=>x=MTH(D₁.take n₀) = the two Lemma-2 outcomes); non-vacuous (some-branch is a SPECIFIC-pair IsCollision, not pigeonhole-provable; none-branch a real equality needing hcons). FINDING + FIX: Opus changed ConsRec's base definition (list-match → decidable if) with only 'recompiled clean' as evidence — a definition that mirrors the deployed verifier. Now machine-checked: consRec_base_ false_eq / consRec_base_true_eq prove the decidable-if base EQUALS the exact list-match forms it replaced. Kept as PERMANENT cone-audited theorems (F1 discipline: keep the evidence), not a throwaway probe. QUEUED for S5.4: extractCons_correct (Theorem 3 endpoint) MUST carry a permanent non-vacuity witness like extractIncl_nonvacuous/extractMTH_ nonvacuous. S7 must re-confirm the NEW ConsRec base vs Python. 26 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 17:25:04 +00:00
import Proofs.Refactor
S5.4: THEOREM 3 COMPLETE — extractCons assembly + non-vacuity witness The paper's hardest theorem is fully kernel-checked. extractCons joins the two proven halves: extractConsNode's collision (via consRecBinding, steps 1-2) or the descent extractMTH D₀ (D₁.take n₀) (step 3, S4). - extractCons_correct: acceptance ConsRec n₀ |D₁| C ⊤ (MTH D₀) = some (MTH D₀, MTH D₁) with D₀ ≠ D₁.take n₀ (and |D₀| = n₀ ≤ |D₁|, 0 < n₀) ⇒ IsCollision of THIS function's output. Statement matches paper Thm 3 verbatim (the n₀ = 0 escape is vacuous there: [] is always the real prefix). Compiled on first attempt — the pre-verified skeleton held exactly. - extractCons_nonvacuous (queued requirement honored): on a non-rewrite input the output is provably NOT a collision — choice-proof. Cones: extractCons_correct [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — single hash axiom, no collision-resistance assumed anywhere. 29 certs green. Fable statement-audit passed. LTL untouched (12 leaves, bcd15f9d). Corpus now holds kernel-checked: Lemma 1, Theorem 1, Theorem 2, Theorem 3 (+ whole-tree Lemma 2). Remaining: Prop 1 (S6), fidelity harness (S7), freeze (S8). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 18:07:20 +00:00
import Proofs.Theorem3
S6: Proposition 1 (pin-store safety) — the last theorem, Merkle-layer share The consumer pin store (§5.4) as a transition predicate; the paper's Prop 1(1) fully mechanized: - pinAccept: same-size ⇒ root match; smaller ⇒ reject (rollback); larger ⇒ consistency proof verifies. Mirrors sthstore.py. - pinAccept_monotone: an accepted step never shrinks the pin (definitional). - pin_prefix_correct: an honest advance where D is NOT the prefix of D' makes pinExtract output a genuine collision — same-size routes to extractMTH (whole-tree Lemma 2), grow routes to extractCons (Theorem 3). Explicit named-extractor form ⇒ non-vacuous (pin_prefix_nonvacuous pinned). - fork_distinct: the Merkle share of Prop 1(2) — different roots at equal size commit to different content. EUF-CMA transferable-evidence is signature-layer, OUT OF SCOPE and documented in the file header (not smuggled). Cones: single hash axiom (pin_prefix_correct adds Classical.choice via functional induction downstream). 33 certs green. Fable statement-audit: matches paper Prop 1(1); Prop 1(2) scope-bounded honestly. LTL untouched. Every §6 statement is now kernel-checked: Lemma 1, Theorems 1-3, whole-tree Lemma 2, Proposition 1. Remaining: S7 fidelity, S8 freeze. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 18:23:49 +00:00
import Proofs.PinStore
L1+L2: hashing shapes, domain separation, MTH/Root/ConsRec with termination Accumulator pyramid layers 1-2, mechanizing paper SS5.3/SS6 groundwork: - gen/LTLAcc/HashExternal.lean: the single sanctioned axiom, opaque sha256 (no properties assumed - the soundness theorems downstream are constructive collision extractors). - Proofs/Basic.lean: hleaf/hnode (0x00/0x01 domain stamps); Lemma 1 (domsep) proven AXIOM-FREE; kbelow (largest power of two below n) with pos/lt/le-two bound lemmas; MTH, Root (Option = rejection), ConsRec (four cases, b-flag, pinned anchor) - all with kernel-checked termination via the kbelow bounds. - check.sh: estate discipline (stub audit, axiom-smuggling gate, lean-guard compilation, boundary-exact per-certificate cone audit). All green; observed cones pinned exactly. Zero contact with the live LTL: no appends, no server, accumulator frozen at 12 leaves throughout this project. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-10 21:58:00 +00:00
#print axioms LTLAcc.domsep
#print axioms LTLAcc.kbelow_pos
#print axioms LTLAcc.kbelow_lt
#print axioms LTLAcc.le_two_kbelow
S2 Fable-5 re-audit: close the kbelow/RFC-fidelity gap (kbelow_pow2) Adversarial statement-level re-verification of everything S2 shipped, against paper SS5.3 and the deployed Python verifier: Path recursion, Root_left/Root_right fold shapes (none exactly where the deployed code rejects), incl_complete as Theorem 1 verbatim (getD default unreachable under m < |D|), MTH([]) = H(epsilon) per RFC. All faithful. One genuine gap found and closed: the kbelow lemmas bounded k but never established k is a power of two, leaving 'our split point = the RFC split point' as by-construction folklore. kbelow_pow2 (cone: propext, Quot.sound) now pins it: 2^j = k < n <= 2k = 2^(j+1) uniquely determines the RFC 9162 split. THE button green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 10:26:04 +00:00
#print axioms LTLAcc.kbelow_pow2
L1+L2: hashing shapes, domain separation, MTH/Root/ConsRec with termination Accumulator pyramid layers 1-2, mechanizing paper SS5.3/SS6 groundwork: - gen/LTLAcc/HashExternal.lean: the single sanctioned axiom, opaque sha256 (no properties assumed - the soundness theorems downstream are constructive collision extractors). - Proofs/Basic.lean: hleaf/hnode (0x00/0x01 domain stamps); Lemma 1 (domsep) proven AXIOM-FREE; kbelow (largest power of two below n) with pos/lt/le-two bound lemmas; MTH, Root (Option = rejection), ConsRec (four cases, b-flag, pinned anchor) - all with kernel-checked termination via the kbelow bounds. - check.sh: estate discipline (stub audit, axiom-smuggling gate, lean-guard compilation, boundary-exact per-certificate cone audit). All green; observed cones pinned exactly. Zero contact with the live LTL: no appends, no server, accumulator frozen at 12 leaves throughout this project. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-10 21:58:00 +00:00
#print axioms LTLAcc.MTH
#print axioms LTLAcc.Root
#print axioms LTLAcc.ConsRec
L3: Theorem 1 (inclusion completeness) kernel-checked Path (prover-side inclusion path, paper SS5.3) with termination via the kbelow bounds; self-contained list lemmas (getD_take, getD_drop - no stdlib-name dependence); equation lemmas MTH_single/MTH_split/Root_one/ Root_left/Root_right (Option.map form; matcher side conditions closed explicitly); Theorem 1 by functional induction on Path with a k-fold discipline against the let-bound split point. incl_complete cone: [propext, Classical.choice, LTLAcc.sha256, Quot.sound] - pinned exactly in check.sh alongside Path. THE button green end to end. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 10:06:20 +00:00
#print axioms LTLAcc.Path
#print axioms LTLAcc.incl_complete
S3/L4-L5: root binding (Lemma 2, Path instance) + Theorem 2, constructive The crux layer — the statement whose HAND proof once carried the frontier coverage bug is now kernel-checked. - gen: hash outputs refactored to Hash = {l : List UInt8 // l.length = 32}. MECHANIZATION FINDING: the paper's pair-coincidence step ('equal hnode values of distinct argument pairs are a collision') is load-bearing on FIXED-WIDTH outputs — with unconstrained byte strings x++s = X++Y does not split. hnode_preimage_inj (cone: propext) makes this explicit via List.append_inj on equal-length components. Queued as a half-sentence for the paper's next cycle. - HasCollision := ∃ x y, x ≠ y ∧ sha256 x = sha256 y — appears ONLY as a conclusion, never a hypothesis (no collision-resistance assumed). - hnode_inj_or_collision / hleaf_inj_or_collision: the per-node dichotomy. - root_binding: any accepting reconstruction from (v,P) to the honest root either IS the honest receipt (leaf hash AND full path P = Path m D — case (ii) pinning every consumed sibling) or exhibits a collision. Motive quantifies (v,P); induction on Path; k-fold discipline. - incl_sound (Theorem 2, position binding): accepting a wrong leaf at m yields a collision. Cone [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — the single hash axiom, pinned in check.sh. ALL GREEN. Also: Root n=1 branch changed from list-match to decidable 'if P = []' (well-founded unfolding generated a spurious exhaustiveness obligation); Root_one_cons added. Fable-5 statement-audit passed. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 11:21:17 +00:00
#print axioms LTLAcc.hnode_preimage_inj
S3.5: explicit collision extractor — Theorem 2 made non-vacuous, vacuous forms removed The S3 Socratic re-audit found incl_sound was kernel-perfect but VACUOUS: its '... ∨ HasCollision' disjunct (∃ x y, x≠y ∧ sha256 x = sha256 y) is provable by pigeonhole ALONE (sha256: infinite List UInt8 → finite 32-byte Hash), so the theorem said nothing about forgeries. Even a data-carrying {p // IsCollision p} disjunct fails (Classical.choice inhabits it). The only faithful rendering of the paper's 'explicit algorithm 𝓔' is a NAMED FUNCTION whose correctness is a claim about ITS OUTPUT. - extractIncl (m D d P): total function that walks the honest tree and returns the concrete colliding preimage pair at the first divergence (a node preimage pair, or the leaf preimage pair at the bottom). - extractIncl_correct: d ≠ D[m] ∧ accepting-receipt → IsCollision (extractIncl …).1 (extractIncl …).2. A statement ABOUT the fixed function's output; pigeonhole cannot discharge it. ADVERSARIAL CHECK (probe, since removed): proved ¬ IsCollision (extractIncl 0 [[7]] [7] []) — i.e. on a NON-forgery input the output is provably NOT a collision, so the conclusion is genuinely false for some inputs ⇒ non-vacuous, choice-proof. - Removed the vacuous theorems entirely (incl_sound, root_binding, hnode/hleaf_inj_or_collision, HasCollision def) so no hollow statement survives in a corpus destined for the log. Kept the real building blocks (hnode_preimage_inj [propext]; eq_dropLast helper moved to Completeness; Binding.lean deleted). extractIncl_correct cone [propext, Classical.choice, LTLAcc.sha256, Quot.sound]. THE button green (14 certs). Fable statement-audit passed. LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 13:31:21 +00:00
#print axioms LTLAcc.IsCollision
#print axioms LTLAcc.extractIncl
#print axioms LTLAcc.extractIncl_correct
S3.5 Fable re-audit: permanent non-vacuity witness + honest ledger Adversarial re-derivation of S3.5 (drill after harness switch). Core verdict CONFIRMED: extractIncl_correct is faithful and non-vacuous. Three methodical flaws found and resolved: - F1: the non-vacuity proof existed only as a deleted probe — evidence discarded. Now permanent: extractIncl_nonvacuous proves the extractor's output on a NON-forgery input is NOT a collision, so the correctness conclusion is false for some inputs and cannot be discharged by pigeonhole/choice. Guards against future drift back into vacuity. Cone pinned. - F2 (queued for S4): deleting root_binding discarded the receipt- uniqueness content of Lemma 2 (left disjunct: P = Path m D) along with its vacuous disjunct. To be restored in extractor form during S4; the S4 consistency walk inlines the same argument regardless. - F3: README still claimed 'root_binding done' — a deleted theorem advertised as delivered. Ledger corrected. 15 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 14:38:34 +00:00
#print axioms LTLAcc.extractIncl_nonvacuous
S4: descent extractor extractMTH (Theorem 3 step 3 + F2 restoration), non-vacuous The 'descend' step of the paper's Theorem 3, built extractor-first per the S3.5 lesson (never a bare '∨ collision'): - extractMTH (D D'): total function that, given two equal-length leaf lists sharing a Merkle root, walks the common-shape tree to the first divergence and returns the concrete colliding preimage pair (a node pair, or a leaf pair at the bottom). - extractMTH_correct: |D|=|D'| ∧ D≠D' ∧ MTH D = MTH D' → IsCollision (extractMTH D D'). Proven by functional induction on extractMTH; composite case uses MTH_split + append_inj (fixed-width Hash) to split node preimages or exhibit the node collision. - extractMTH_nonvacuous: equal lists → output NOT a collision (pinned), so the conclusion is false for some inputs ⇒ choice-proof. This also RESTORES, in explicit non-vacuous form, the receipt-uniqueness content of Lemma 2 deleted in the S3.5 cleanup (re-audit F2): the honest Merkle fold is injective up to a collision. 18 certs green. Fable statement-audit passed (matches paper Thm 3 step 3 verbatim). LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 14:46:58 +00:00
#print axioms LTLAcc.extractMTH
#print axioms LTLAcc.extractMTH_correct
#print axioms LTLAcc.extractMTH_nonvacuous
S5 stage 1: consistency infrastructure (kbelow prefix-split + list surgery) Theorem 3's binding (steps 1-2) turns on one non-obvious arithmetic fact, isolated and proven here before the main proof: - pow2_exp_unique / kbelow_eq_of_pow2_between: kbelow is pinned by its three defining inequalities (power-of-two, k<n≤2k), so a prefix that spills past the left subtree splits at the SAME point. - kbelow_prefix_eq: with k=kbelow n, 2≤n, k<n₀≤n ⇒ kbelow n₀ = k (the fact the n₀>k recursion branch needs to align MTH(D₁.take n₀) with the fold). - take_take_le, take_drop_prefix: the list-surgery identities relating (D.take n₀) to D.take k and (D.drop k).take (n₀-k). Cones pinned; 21 certs green. Deliberate honest checkpoint — binding + extractCons assembly is the next stage. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 15:53:43 +00:00
#print axioms LTLAcc.kbelow_prefix_eq
#print axioms LTLAcc.take_take_le
#print axioms LTLAcc.take_drop_prefix
S5 stage 2: extractConsNode extractor defined (consistency, Theorem 3 steps 1-2) The consistency collision extractor: walks the ConsRec new-root fold in parallel with the honest size-n tree of D₁ and returns the concrete colliding node preimage pair at the first level where the fold's hnode argument pair diverges from the honest node — or none if the fold is genuine all the way down (binding holds). Both branches verified faithful to ConsRec's hnode argument order (n₀≤k: y' left / s right; n₀>k: s left / y' right). Termination via kbelow bounds. Deliberate honest checkpoint: the DEFINITION compiles and is cone-audited [propext, LTLAcc.sha256, Quot.sound]; the binding CORRECTNESS proof — the single hardest object in the corpus — is stage 3, kept for a fresh session rather than a rushed long turn. 22 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 15:55:51 +00:00
#print axioms LTLAcc.extractConsNode
S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) The single hardest proof in the corpus is complete, no sorry. Under the value-equality invariant y = MTH D₁, an accepting ConsRec fold either makes extractConsNode output a genuine collision or its first component is the honest prefix root MTH(D₁.take n₀). - ConsRec base changed from list-match to decidable if (if C=[] / if C.length=1) — same root-cause fix as Root, avoids WF-unfold exhaustiveness obligations; more faithful to the deployed Python. Whole chain (Basic..Consistency) rebuilt clean. - consRecBinding by ConsRec.induct (10 cases): 4 base/singleton, 3 rejection/none contradictions, 2 recursive (n₀≤k, n₀>k). The n₀>k none-branch is where all S5.1 infrastructure interlocks: kbelow_prefix_eq (prefix splits at same k) + take_take_le + take_drop_prefix assemble x = hnode s xx into MTH(D₁.take n₀). The collision branches use append_inj (fixed-width Hash) + MTH_split. - take_all helper (take-whole-list). Cone [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — single hash axiom. 24 certs green. Fable statement-audit: matches paper Thm 3 steps 1-2. LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 17:18:26 +00:00
#print axioms LTLAcc.take_all
#print axioms LTLAcc.consRecBinding
S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) Re-derived S5.3 (all done under an Opus switch) from zero. consRecBinding STATEMENT re-confirmed faithful to paper Thm 3 steps 1-2 (y=MTH D₁ = the hash-fold condition; some=>collision / none=>x=MTH(D₁.take n₀) = the two Lemma-2 outcomes); non-vacuous (some-branch is a SPECIFIC-pair IsCollision, not pigeonhole-provable; none-branch a real equality needing hcons). FINDING + FIX: Opus changed ConsRec's base definition (list-match → decidable if) with only 'recompiled clean' as evidence — a definition that mirrors the deployed verifier. Now machine-checked: consRec_base_ false_eq / consRec_base_true_eq prove the decidable-if base EQUALS the exact list-match forms it replaced. Kept as PERMANENT cone-audited theorems (F1 discipline: keep the evidence), not a throwaway probe. QUEUED for S5.4: extractCons_correct (Theorem 3 endpoint) MUST carry a permanent non-vacuity witness like extractIncl_nonvacuous/extractMTH_ nonvacuous. S7 must re-confirm the NEW ConsRec base vs Python. 26 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 17:25:04 +00:00
#print axioms LTLAcc.consRec_base_false_eq
#print axioms LTLAcc.consRec_base_true_eq
S5.4: THEOREM 3 COMPLETE — extractCons assembly + non-vacuity witness The paper's hardest theorem is fully kernel-checked. extractCons joins the two proven halves: extractConsNode's collision (via consRecBinding, steps 1-2) or the descent extractMTH D₀ (D₁.take n₀) (step 3, S4). - extractCons_correct: acceptance ConsRec n₀ |D₁| C ⊤ (MTH D₀) = some (MTH D₀, MTH D₁) with D₀ ≠ D₁.take n₀ (and |D₀| = n₀ ≤ |D₁|, 0 < n₀) ⇒ IsCollision of THIS function's output. Statement matches paper Thm 3 verbatim (the n₀ = 0 escape is vacuous there: [] is always the real prefix). Compiled on first attempt — the pre-verified skeleton held exactly. - extractCons_nonvacuous (queued requirement honored): on a non-rewrite input the output is provably NOT a collision — choice-proof. Cones: extractCons_correct [propext, Classical.choice, LTLAcc.sha256, Quot.sound] — single hash axiom, no collision-resistance assumed anywhere. 29 certs green. Fable statement-audit passed. LTL untouched (12 leaves, bcd15f9d). Corpus now holds kernel-checked: Lemma 1, Theorem 1, Theorem 2, Theorem 3 (+ whole-tree Lemma 2). Remaining: Prop 1 (S6), fidelity harness (S7), freeze (S8). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 18:07:20 +00:00
#print axioms LTLAcc.extractCons
#print axioms LTLAcc.extractCons_correct
#print axioms LTLAcc.extractCons_nonvacuous
S6: Proposition 1 (pin-store safety) — the last theorem, Merkle-layer share The consumer pin store (§5.4) as a transition predicate; the paper's Prop 1(1) fully mechanized: - pinAccept: same-size ⇒ root match; smaller ⇒ reject (rollback); larger ⇒ consistency proof verifies. Mirrors sthstore.py. - pinAccept_monotone: an accepted step never shrinks the pin (definitional). - pin_prefix_correct: an honest advance where D is NOT the prefix of D' makes pinExtract output a genuine collision — same-size routes to extractMTH (whole-tree Lemma 2), grow routes to extractCons (Theorem 3). Explicit named-extractor form ⇒ non-vacuous (pin_prefix_nonvacuous pinned). - fork_distinct: the Merkle share of Prop 1(2) — different roots at equal size commit to different content. EUF-CMA transferable-evidence is signature-layer, OUT OF SCOPE and documented in the file header (not smuggled). Cones: single hash axiom (pin_prefix_correct adds Classical.choice via functional induction downstream). 33 certs green. Fable statement-audit: matches paper Prop 1(1); Prop 1(2) scope-bounded honestly. LTL untouched. Every §6 statement is now kernel-checked: Lemma 1, Theorems 1-3, whole-tree Lemma 2, Proposition 1. Remaining: S7 fidelity, S8 freeze. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 18:23:49 +00:00
#print axioms LTLAcc.pinAccept_monotone
#print axioms LTLAcc.pin_prefix_correct
#print axioms LTLAcc.fork_distinct
#print axioms LTLAcc.pin_prefix_nonvacuous
S7 Fable re-audit: close the cone-audit COVERAGE gap (52/52), verify button by exit code Re-derived S7 as Fable, practicing the standing rule (check exit code + ALL GREEN, not tail). Confirmed committed button genuinely exits 0. FINDING: the cone audit had a COVERAGE gap — 34 of 52 proven objects were pinned; 18 (incl. core defs kbelow/hleaf/hnode and the pin-store defs pinAccept/pinExtract/acceptCons, plus intermediate lemmas) were never cone-audited. Transitively safe (Phase 1 forbids axiom under Proofs/, Phase 2 forbids sorry, universally) — but 'transitively covered' is not good enough for an externally-reviewed corpus. Closed: every proven theorem/def now has its EXACT cone pinned, read from #print axioms (not guessed). Coverage now 52/52, empty unaudited list. Cones of note: hleaf/hnode = [LTLAcc.sha256] only; kbelow and the pure arithmetic/list helpers = no hash axiom; the def-level objects that touch MTH carry the single sha256 boundary. No surprise axioms anywhere. Button verified: EXIT 0, ALL GREEN, FIDELITY GREEN, 164,479/164,224 pinned. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 18:56:17 +00:00
#print axioms LTLAcc.MTH_single
#print axioms LTLAcc.MTH_split
#print axioms LTLAcc.Root_left
#print axioms LTLAcc.Root_one
#print axioms LTLAcc.Root_one_cons
#print axioms LTLAcc.Root_right
#print axioms LTLAcc.acceptCons
#print axioms LTLAcc.eq_dropLast_append_of_getLast?
#print axioms LTLAcc.exists_singleton_of_length_one
#print axioms LTLAcc.getD_drop
#print axioms LTLAcc.getD_take
#print axioms LTLAcc.hleaf
#print axioms LTLAcc.hnode
#print axioms LTLAcc.kbelow
#print axioms LTLAcc.kbelow_eq_of_pow2_between
#print axioms LTLAcc.pinAccept
#print axioms LTLAcc.pinExtract
#print axioms LTLAcc.pow2_exp_unique
#print axioms LTLAcc.take_append_drop
S7 drill (2nd pass): pin the load-bearing gen/ instance cones; document audit surface Audit-of-the-coverage-audit. Its 18 added cone values re-verified against the observed #print outputs (all match). Methodology blind spots found: abbrev Bytes (bare alias, no cone content — excluded by nature) and the two ANONYMOUS gen/ instances, which are silently load-bearing (DecidableEq Hash powers ConsRec's 'if C = []' and pinAccept's root compare; Inhabited Hash powers every getD default). Transitivity covered them, but no hand-waves before external review: cones read and pinned — instInhabitedHash = [propext], instDecidableEqHash = AXIOM-FREE. The audit-surface definition is now documented in check.sh itself. Button verified by exit code: EXIT 0, ALL GREEN, FIDELITY GREEN. 54 pinned cones. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 19:07:08 +00:00
#print axioms LTLAcc.instInhabitedHash
#print axioms LTLAcc.instDecidableEqHash
Reference in a new issue Copy permalink