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/README.md

37 lines
2.3 KiB
Markdown
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
# ltl-accumulator-verified
Lean 4 mechanization of the security analysis (§6) of the paper
"The Lean Transparency Log" (https://ltl.zkdefi.org/paper): the Merkle
accumulator's own correctness and soundness theorems, kernel-checked, in
the same discipline as the four `*-ed25519-verified` subject corpora.
## Status: layer scaffold (work in progress — honest ledger below)
| layer | content | status |
|---|---|---|
| L1 | bytes, hleaf/hnode, domain separation (Lemma 1) | **done** (domsep: axiom-free) |
| L2 | MTH, Root, ConsRec definitions + termination | **done** (cones: propext, LTLAcc.sha256, Quot.sound) |
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
| L3 | inclusion completeness (Theorem 1) | **done** (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) |
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
| L4 | frontier binding content (Lemma 2) | **inlined in the extractor walk** (extractIncl); standalone receipt-uniqueness theorem queued for S4 restoration in extractor form |
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
| L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** |
S4 Fable re-audit: correct a false ledger claim (F2 was NOT resolved) Adversarial re-derivation of S4. The mathematics HOLDS: extractMTH_correct is faithful to paper Theorem 3 step 3 (hypotheses, recursion, node/leaf collision cases all re-verified), sub-call length/difference obligations sound, non-vacuity witness valid. The defect was in the CLAIM: S4's commit/README stated extractMTH 'restores the receipt-uniqueness content of Lemma 2'. Wrong instance. Lemma 2 has three instantiations; the deleted root_binding was the PATH instance (uniqueness of accepting receipts (v,P) for Root, quantifying over adversarial paths); extractMTH is the WHOLE-TREE instance (MTH injective on equal-length leaf lists). Nothing in the corpus currently states path-uniqueness. Ledger corrected: whole-tree instance done; path instance honestly listed as deleted-and-not-restored (optional — not needed for Theorem 3 assembly). No Lean changes; 18 certs remain green. LTL untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 15:15:08 +00:00
| L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, WHOLE-TREE instance) **done, non-vacuous** |
| — | Lemma 2, PATH instance (receipt-uniqueness of `Root`): deleted with the vacuous `root_binding` in S3.5 and **not yet restored**; optional, not needed for Theorem 3 |
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
| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | pending (S5) |
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
| L6 | pin-store state machine safety (Proposition 1) | pending |
## Discipline (identical to the subject corpora)
- `verification/Proofs/` contains ZERO `axiom` declarations; the single
sanctioned axiom site is `verification/gen/` — here, one opaque
function: SHA-256. The theorems are constructive collision extractors,
so collision resistance is never assumed, only interpreted.
- `verification/check.sh` is THE button: compiles every file through
`lean-guard` (memory cap, core pinning, timeout, single-flight lock)
and axiom-audits every certificate against its documented exact cone.
- Expected boundary: `propext, Classical.choice, Quot.sound` plus
`LTLAcc.sha256` for hash-touching certificates — documented per
certificate in `check.sh`, audited both directions.
The finished certificates are destined for the LTL itself as attestation
leaves: the log carrying kernel-checked proofs of its own machinery.
Reference in a new issue Copy permalink