mrwulf
172a1d0653
Round-4 verdicts: Claude reviewer — nothing blocks the freeze, no remaining findings; GPT-5.6 — approve after minor documentation fixes, attestation scoped to the mechanized model. This round is those fixes; no Lean surface changed. - 218/59 → 222/61 everywhere, and STRUCTURALLY: check.sh Phase 3c asserts the audit counts (STATEMENT-MAP + README vs allowlist/CONES) and the four fidelity pins (STATEMENT-MAP vs run_fidelity.py constants) on every run — stale-count drift is a red button now (R4-1, third recurrence of the class). - Gap 14 reworded to evidence-vs-inference (the invariant "is assumed", not "transfers"), witnesses cited (paper §5.3/§5.4; pacta sthstore.py/logclient.py — outside the fidelity target). New gap 15: deployment refinement invariant unmechanized (GPT's principal finding, split out because it carries the deployed-soundness claim). - Runbook: A1 marked done (both approvals on SD); B2 gains the REQUIRED scoped attestation wording (GPT §11) as a gate condition — entry 13 cannot claim "deployed verifier formally verified". - run_bare.sh fail-closes on Lean version AND commit (rejection path tested with a fake toolchain: FATAL, exit 1). - Harness: "consistency baseline family" line (GPT §8); gap 14 says "fixed offsets n−1/n+1/n+7" (R4-5). - RESPONSE round 5, incl. refutation of GPT §7 (the target tarball demonstrably contains MANIFEST.sha256 + TARGET-PROVENANCE.md; the round-5 kit also ships both unpacked as a courtesy). check.sh exit 0 ATTESTATION GREEN (Phases 0-4 incl. new 3c); selftest exit 0, 9/9 + control. Live LTL untouched (12 leaves, bcd15f9d…). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
4 KiB
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: FROZEN for external review (corpus complete)
All paper-§10 mechanization targets are kernel-checked; the audit surface
is defined and green (verification/check.sh, exit 0). See
STATEMENT-MAP.md for the paper↔Lean review surface and
KNOWN-GAPS.md for the honest scope ledger.
Revised across four external review rounds (GPT-5.6 + a second Claude,
adversarial; zero broken theorems in any round; both approved after
round 4). The audit surface is an environment-derived inventory
(Proofs/Inventory.lean + pinned allowlist — 222 constants,
61 human-reviewed cones, self-tested by selftest_audit.sh); the review
kit is push-button reproducible (run_bare.sh, self-contained fidelity
target); acceptIncl/acceptCons_sound route the theorems through the
named acceptance predicates; fidelity = agreement over pinned families
(230,271 + 230,016 baseline; 73,573 lied-size boundary cases with
3,867 expected one-sided divergences — KNOWN-GAPS gaps 14/15, not
extensional equality). Doc counts are asserted by check.sh Phase 3c.
The finished certificates' attestation into the LTL is a separate,
explicitly-authorized operator decision, scoped per the runbook.
| 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 | inclusion completeness (Theorem 1) + named acceptance acceptIncl |
done (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) |
| L4 | frontier binding content (Lemma 2) | done as specializations — inlined in the extractor walk (extractIncl), whole-tree (extractMTH), ConsRec (consRecBinding); the standalone Root receipt-uniqueness instance was deleted with the vacuous root_binding in S3.5 and deliberately NOT restored (optional, unused — KNOWN-GAPS gap 3) |
| L5 | inclusion soundness = EXPLICIT extractor extractIncl (Theorem 2) |
done, non-vacuous |
| L6a | descent extractor extractMTH (Theorem 3 step 3 = Lemma 2, whole-tree instance) |
done, non-vacuous |
| L6b | Theorem 3 (consistency soundness): consRecBinding (steps 1–2) + extractCons/extractCons_correct (+ _paper at the paper's exact quantifiers; acceptCons_sound routes it through the named acceptCons predicate, size bound derived from acceptance via consRec_some_le) |
done, non-vacuous |
| L6c | pin-store state machine safety (Proposition 1): pinAccept_monotone, pin_prefix_correct, fork_distinct |
done, non-vacuous (per-step; multi-step chain = gap 7) |
Discipline (identical to the subject corpora)
verification/Proofs/contains ZEROaxiomdeclarations; the single sanctioned axiom site isverification/gen/— here, one opaque function: SHA-256. The theorems are constructive collision extractors, so collision resistance is never assumed, only interpreted.verification/check.shis THE button: compiles every file throughlean-guard(memory cap, core pinning, timeout, single-flight lock) and axiom-audits every certificate against its documented exact cone.- Reviewers without the operator toolchain:
verification/run_bare.shcompiles, axiom-audits, and inventory-gates the corpus with a plain publiclean(version pinned inverification/lean-toolchain); the operator path is overridable viaAENEAS_ENV. - Expected boundary:
propext, Classical.choice, Quot.soundplusLTLAcc.sha256for hash-touching certificates — documented per certificate incheck.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.