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

14 lines
413 B
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
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
Reference in a new issue Copy permalink