saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-03 19:53:48 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
No description
32 commits 1 branch 0 tags 2.7 MiB
Shell 54.1%
Lean 36%
Python 9.9%
Find a file
mrwulf bab1c8c737 Runbook round-6 normalization: release tuple, B0 preflight, candidate-inspection gate, 12→13 rehearsal 
Both round-6 reviewers' critical/high procedural findings:

- CRITICAL (both): runbook pinned the wrong commit (2da0a79 in the
  facts table, B1 checkout, A4) while the reviewed subject and the
  scoped-wording config live in 172a1d0. Re-pinned everywhere;
  remaining 2da0a79 mentions are explicitly historical. Added §2a
  release tuple (SUBJECT_COMMIT/PACTA_COMMIT/EXPECTED_OLD_SIZE/
  EXPECTED_OLD_ROOT/KEY_FINGERPRINT) that every Phase-B step consumes.
- A2: "14 entries" → 15, with the dynamic grep count and gap 15 called
  out as the claim-constraining one.
- GPT §10: new B0 — preflight the LIVE predecessor (size/root/STH-sig/
  witness-audit-under-real-key/live-service/mirror agreement/no partial
  entry 13/operational-state roots to bcd15f9d). An append-only system
  re-reads its predecessor; it does not trust a Facts table.
- GPT §4: new B1b — clone + checkout + clean-tree + green-suite the
  pinned PACTA_COMMIT; that is the only producer used.
- GPT §5 + both: new B2b candidate-leaf inspection gate (subject commit,
  61/61 proven+clean, scope.deployment_constraints carries the required
  wording and not the forbidden phrase, scope.exclusions complete) —
  inspect before you append a leaf you cannot take back.
- GPT §11: exact changed-path set + prefix immutability (entries
  0..11 byte-identical, one appended history line) instead of
  "exactly four paths" by description.
- GPT §7/§8: B6 binds sanitized evidence (subject/producer commits,
  config + candidate + fidelity-transcript digests, old/new roots,
  consistency + witness + pin results) so the leaf's fidelity clause
  points at a concrete object.

A4 redone as a structural 12→13 rehearsal (GPT Method B) — green:
predecessor copy roots to bcd15f9d, candidate 61/61 with scoped wording
IN THE LEAF, append→13, prefix immutability, consistency 12→13 accepted
by deployed AND mechanized model. Transcript on SD. Facts table:
pacta freeze lifted; producer = round-6 PACTA_COMMIT, not 3d81d53.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-16 15:29:20 +02:00
docs docs: optimistic-accountability essay (rollup ↔ LTL mapping + what the tree actually holds); wired into runbook B7 2026-07-14 11:27:30 +02:00
verification Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded 2026-07-15 09:40:20 +02:00
.gitignore Review round 4: F1* absorbed (lied-size boundary), acceptCons_sound, kit reproducibility 2026-07-12 15:07:57 +02:00
ATTESTATION-RUNBOOK.md Runbook round-6 normalization: release tuple, B0 preflight, candidate-inspection gate, 12→13 rehearsal 2026-07-16 15:29:20 +02:00
KNOWN-GAPS.md Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded 2026-07-15 09:40:20 +02:00
README.md Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded 2026-07-15 09:40:20 +02:00
RESPONSE-TO-REVIEWERS.md Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded 2026-07-15 09:40:20 +02:00
STATEMENT-MAP.md Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded 2026-07-15 09:40:20 +02:00

README.md

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 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.
  • Reviewers without the operator toolchain: verification/run_bare.sh compiles, axiom-audits, and inventory-gates the corpus with a plain public lean (version pinned in verification/lean-toolchain); the operator path is overridable via AENEAS_ENV.
  • 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.