From 6e56414fbc2f28cceb9ebdb96d2fb91a58b470c4 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 21:19:05 +0200 Subject: [PATCH] =?UTF-8?q?S8:=20CORPUS=20FROZEN=20for=20external=20review?= =?UTF-8?q?=20=E2=80=94=20statement=20map=20+=20known-gaps=20ledger?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - STATEMENT-MAP.md: the review surface — every paper §6/§10 item mapped to its Lean name, file, and cone; the named-extractor design invariant and the anti-pigeonhole guards explained; the audit surface stated. - KNOWN-GAPS.md: eight honest scope boundaries, including the process- history candor item (the guessed-pins/false-green episode and its fix). - README: frozen banner. Final sweeps: button EXIT 0 + ALL GREEN + FIDELITY GREEN; zero sorry; the only ∃-conclusions are content-bearing (kbelow_pow2) or hypothesis-guarded helpers — no collision existentials anywhere. Corpus: 54 pinned cones over a defined surface, single sha256 boundary, Lemma 1 axiom-free, Theorems 1-3 + Prop 1(1) + whole-tree Lemma 2 + fidelity 164,479/164,224. Frozen at this commit pending external review. LTL untouched (12 leaves, bcd15f9d). Co-Authored-By: Claude Fable 5 --- KNOWN-GAPS.md | 35 +++++++++++++++++++++++++++++++++++ README.md | 10 +++++++++- STATEMENT-MAP.md | 39 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 83 insertions(+), 1 deletion(-) create mode 100644 KNOWN-GAPS.md create mode 100644 STATEMENT-MAP.md diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md new file mode 100644 index 0000000..f327129 --- /dev/null +++ b/KNOWN-GAPS.md @@ -0,0 +1,35 @@ +# Known gaps and scope boundaries (honest ledger) + +Deliberate, documented, and none silent. Reviewers should verify this +list is COMPLETE, not merely that the items are acceptable. + +1. **SHA-256 is opaque** — the single boundary axiom (`LTLAcc.sha256`), + by design identical to the paper's posture: soundness theorems + construct collisions, never assume collision resistance. +2. **No consistency-completeness theorem** (honest ConsRec acceptance). + Matches the paper (its Theorem 1 is inclusion-only); honest + consistency behavior is covered by the fidelity harness's honest + cases (164,224-case agreement with the deployed verifier). +3. **Lemma 2, path instance not restored** — receipt-uniqueness for + `Root` (an accepting `(v,P)` is the honest receipt) was removed with + the vacuous `root_binding` and not re-proven in extractor form. + Optional: unused by Theorems 2–3 as assembled. +4. **Signature layer abstract** — Ed25519 EUF-CMA, the poison/evidence + retention state, and transferability of fork evidence (paper Prop + 1(2)) are not modeled; `fork_distinct` is the Merkle-layer share only. +5. **Transliteration bridge** — `fidelity/lean_defs.py` mirrors the Lean + definitions by quoted-source inspection (the Lean defs are + noncomputable over the opaque hash, so the bridge cannot be #eval'd + closed). Same inspection bridge the paper's own harness uses. +6. **Proposition 2 (verdict integrity) out of scope** — per paper §10's + mechanization list (i–v). It is a property of the consumer tooling's + construction, enforced and regression-tested in the pacta repo. +7. **Multi-step pin monotonicity** — mechanized per-step + (`pinAccept_monotone`); the paper's multi-step chain is its + reflexive-transitive iterate, not separately mechanized. +8. **Process history** (candor): three cone pins were guessed (not read) + during S5.3–S6 and the audit's failure went unnoticed until S7 + because green was claimed from tailed output rather than the exit + code. No theorem was affected (kernel-checked throughout); pins were + corrected, the audit surface defined, and the standing rule is now: + exit code + ALL GREEN, cones read from #print axioms only. diff --git a/README.md b/README.md index 48d0762..34d7cac 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,15 @@ Lean 4 mechanization of the security analysis (§6) of the paper 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) +## 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](STATEMENT-MAP.md) for the paper↔Lean review surface and +[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. No changes +until the external review round (second model instance + GPT + author) +completes. The finished certificates' attestation into the LTL is a +separate, explicitly-authorized operator decision. | layer | content | status | |---|---|---| diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md new file mode 100644 index 0000000..dce195b --- /dev/null +++ b/STATEMENT-MAP.md @@ -0,0 +1,39 @@ +# Statement map: paper §6 ↔ Lean corpus + +The kernel guarantees every proof below; what a reviewer must vet is the +**statements** — that each Lean theorem says what the paper's item says. +This map is the review surface. Paper = "The Lean Transparency Log" +(https://ltl.zkdefi.org/paper), §6 and §10 (which scopes the +mechanization to items i–v). + +| paper item | Lean name | file | cone | +|---|---|---|---| +| §5.3 split point k (RFC 9162) | `kbelow` + `kbelow_pos/lt`, `le_two_kbelow`, `kbelow_pow2` (2^j = k < n ≤ 2^{j+1} pins k uniquely) | Basic | no hash axiom | +| §5.3 MTH | `MTH` | Basic | sha256 | +| §5.3 Path | `Path` | Completeness | sha256 | +| §5.3 Root (App. B) | `Root` (Option = rejection) | Basic | sha256 | +| §5.3 ConsRec | `ConsRec` (+ machine-checked base-refactor equivalences `consRec_base_true_eq/false_eq`) | Basic, Refactor | sha256 | +| Lemma 1 (domain separation) | `domsep` | Basic | **axiom-free** | +| Theorem 1 (inclusion completeness) | `incl_complete` | Completeness | sha256 (+choice) | +| Lemma 2, width fact ("65-byte preimages") | `Hash` = length-32 subtype; `hnode_preimage_inj` | gen, Basic | propext | +| Lemma 2, whole-tree instance | `extractMTH` + `extractMTH_correct` | Descent | sha256 (+choice) | +| Lemma 2, ConsRec instance (Thm 3 steps 1–2) | `consRecBinding` | Binding3 | sha256 (+choice) | +| Theorem 2 (inclusion soundness, explicit 𝓔) | `extractIncl` + `extractIncl_correct` | Extract | sha256 (+choice) | +| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct` | Theorem3 | sha256 (+choice) | +| Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) | +| Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 | +| non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 | +| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 164,479 + 164,224 (paper's exact case set) | fidelity | (testing) | + +Design invariant of every soundness statement: the collision is the output +of a **named extractor function** and correctness is a claim about that +output. A bare `∃ x y, x ≠ y ∧ sha256 x = sha256 y` is provable by +pigeonhole alone (sha256 maps an infinite domain into the finite 32-byte +type), so it carries no cryptographic content; the guards above prove each +extractor's conclusion is *false* on honest inputs, hence not +choice-dischargeable. + +Audit surface (enforced by `verification/check.sh`, exit 0 = green): +every theorem/def under `Proofs/` (52) plus the two load-bearing `gen/` +instances; excluded by nature: the sanctioned axiom `sha256` (it *is* the +boundary) and `abbrev Bytes` (alias, no cone content).