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
ltl-accumulator-verified/KNOWN-GAPS.md

12 KiB
Raw Permalink Blame History

Known gaps and scope boundaries (honest ledger)

Numbering note (2026-07-19): "paper §N" references in this ledger use the archived system report's numbering ("The Lean Transparency Log", the v0.2 draft archived in the pacta repository's git history), which this corpus was built against. The current paper at /paper has a different structure; in particular its §5.3/§5.4 are unrelated to the §5.3/§5.4 cited in gap 14/15 below.

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 (within the 230,016-case consistency agreement with the deployed verifier).

  3. Lemma 2 is mechanized as specializations, not as one general theorem. The paper's Lemma 2 is a single statement quantified over an abstract hash-fold F and a connected subtree S. The corpus has no hash-fold datatype/predicate; it proves the needed instances directly — whole-tree (extractMTH_correct), ConsRec (consRecBinding), inclusion (extractIncl_correct), and the width fact (hnode_preimage_inj). These suffice for Theorems 2–3. Two consequences: (a) the abstract lemma itself is not a mechanized object; (b) the path-instance receipt-uniqueness for Root (removed with the vacuous root_binding) is not restored — optional, unused. Any paper claim that "Lemma 2 is mechanized" must read "its specializations sufficient for Theorems 2–3 are mechanized."

  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.

  9. Asymptotic cost not mechanized. Paper Theorems 2 and 3 assert the extractors run in O(n) / O(n₁) hash evaluations. The mechanization proves functional correctness of the named extractors only — no cost semantics, recurrence, or computability-after-hash-instantiation. (The extractors are noncomputable over the opaque sha256.)

  10. Pin-store initialization from the empty pin not modeled, and pin_prefix_correct assumes 0 < n. Trust-on-first-use / the size-0 initial state is a separate operation; the theorems cover transitions from a positive-size pin. (Related to gap 7's per-step scoping.)

  11. acceptIncl now named (was review F1). The consumer's inclusion acceptance m < n ∧ Root … = some r is now the Lean object acceptIncl, with acceptIncl_complete/acceptIncl_sound routing completeness/soundness through it, and the fidelity harness exercises the out-of-range families (m ≥ n). Root alone still accepts out-of-range m; that is by design (it is the reconstruction, not the accept predicate).

  12. Audit-gate lineage (candor; was round-2 GPT H1 / Claude NEW-1, both round-1 "fail-closed" claims were overclaims). The round-2 coverage gate enumerated declarations with a source regex and was evadable (attributes, indentation, private/protected, instance, nested-namespace basename collisions). Round 3 replaced it with an environment-derived inventory (Proofs/Inventory.lean + inventory-allowlist.txt, fully-qualified names, no filtering) and selftest_audit.sh, which runs the published evasion table plus a namespace collision, an axiom smuggle, a stale-entry case, and two unmanifested-module cases against the exact production gate. Residual honesty: the inventory sees what the compiled environment contains; it cannot see source that is never compiled (which the dead-file checks cover) or defeat a hostile Lean toolchain.

  13. Review-kit fidelity target was not self-contained in round 2 (GPT H2: missing load-time imports made run_fidelity.py unrunnable from the kit). Round 3 ships the complete stdlib-only import closure of pacta.transparency, content-addressed against pacta commit 3d81d53, plus the clean-extraction transcript with exit code.

  14. Deployed verify_consistency accepted lied-size proofs the mechanized ConsRec rejects — finite pinned family, no global inclusion relation claimed. [CLOSED 2026-07-23 — see closure note at the end of this item.] (round-3 Claude addendum F1*, reproduced by the operator against deployed pacta). Witness: for the honest proof P between sizes 2→3, verify_consistency(1, 3, R2, R3, P) returns True — a semantically false claim ("R2 is the root of a size-1 prefix") — while ConsRec rejects; 3,405 such divergences exist for n < 60, ALL one-sided (the mechanized model never accepts anything the deployed verifier rejects; inclusion shows zero divergences under identical abuse). Mechanism: when the claimed old size is a power of two, the deployed iterative verifier (an RFC 9162-style loop, but see root cause) seeds the walk with the old root and uses the sizes only as bit-navigation state, so several size claims navigate one proof identically. (Root cause, identified at closure: the deployed verifier omitted RFC 9162 §2.1.4.2 Step 7's terminal sn == 0 condition; see the closure note below.) Consequences: (a) fidelity between the two consistency verifiers is agreement over the pinned case families, NOT extensional equality — the harness's lied-size family pins the boundary (73,573 cases: lied old size exhaustive for n < 60, lied new size at fixed offsets n−1/n+1/n+7; 3,867 expected divergences, direction asserted one-sided per case); (b) Theorem 3 / acceptCons_sound cover the MECHANIZED accept set. The exhibited divergence is outside the intended pin-store input invariant; applying the mechanized soundness result to the deployed flow therefore additionally ASSUMES that the deployed state machine always binds each root to its authentic size and exposes no alternate invocation path — an invariant that is NOT mechanized in this corpus (gap 15). Where the invariant's witnesses live: paper §5.3 (the signed head binds (n₁, r₁) together under one signature) and §5.4 (the pin (n₀, r₀) comes from the consumer's own store, never from the peer), implemented in the pacta repo at src/pacta/sthstore.py and src/pacta/logclient.py — code OUTSIDE the supplied fidelity target (review R4-3/GPT-4). No exploitability against that flow is claimed or ruled out here; assessing it requires the signature/STH layer (gap 4).

CLOSURE (2026-07-23, pacta ddbb5a4). The earlier sentence "deployed behavior matches upstream RFC 9162 implementations" was incorrect: the deployed verify_consistency implemented the RFC 9162 §2.1.4.2 bit-navigation loop but omitted its Step 7 terminal condition that the new-size navigation counter reach zero (sn == 0). That omission — not any property of RFC 9162 — is the whole of the divergence: a faithful RFC verifier rejects the same lied-size family. Restoring the one conjunct removes every divergence in the pinned 73,573-case family, verified by a new three-way regression test_consistency_lied_size_three_way_agreement (deployed verifier / recursive ConsRec model / an independent faithful RFC 9162 transliteration) over both the honest and lied-size families. The divergence was originally surfaced by this corpus's own two-way fidelity harness; the missing third (RFC) oracle is what assigned blame to the deployed side rather than the model. The historical divergence remains truthfully recorded in public log entry 13 and is reproducible at the tagged pre-fix commit vulnerable/sn0-consistency-fd2f6ba; public entry 13, the attested accumulator commit 172a1d0, and the IACR submission PDF are all unchanged. Gap 15 (deployment refinement invariant) remains open. 15. Deployment refinement invariant unmechanized (round-4 GPT, its principal finding — split out from gap 14 because it carries the deployed-soundness claim). The corpus proves soundness of the mechanized acceptCons; it does NOT prove the refinement AuthenticPair(n₀,r₀,D₀) ∧ AuthenticPair(n₁,r₁,D₁) ∧ verify_consistency(…) → acceptCons(…). The operational invariant (authentic-size/root binding via the signed-head + pin-store flow) is relied upon but unverified, and the consumer flow implementing it is not in the supplied fidelity target. Consequently any attestation of this corpus must be scoped to the MECHANIZED model: "the deployed consistency verifier is formally verified" is NOT a claim this corpus supports. Closure paths (roadmap, operator decision, post paper-freeze): (A) make the deployed verifier adopt ConsRec-equivalent acceptance; or (B) mechanize the signed-head + pin-store state machine and prove the refinement; or (C) keep the boundary and this scoped claim permanently. 16. The statement binding covers identity, not meaning (added 2026-07-28 with check.sh Phase 3d). The coverage gate pins every constant's name, kind and axiom cone, both directions; Phase 3d additionally pins every constant's fully-elaborated TYPE and every definition's fully-elaborated BODY, digest committed as AUDIT-MANIFEST.txt. What that buys is that the corpus is the one that was reviewed. What it does NOT buy: (a) whether those statements say anything worth believing is a question a human reading STATEMENT-MAP.md answers, not the button; (b) an author who edits a definition and refreshes the digest in the same commit passes every phase — the defence is that both changes are visible in the diff at the pinned commit; (c) proof TERMS are deliberately not bound, by proof irrelevance, so a proof rewritten to a different term of the same statement and cone moves nothing. Worth recording plainly, because it was measured rather than reasoned: wrapping one branch of pinAccept's body in id (…) is definitionally equal, compiles, leaves name/kind/type/cone untouched, and the coverage gate reports GREEN. Only the digest sees it. That is the exact size of the gap Phase 3d closes, and selftest_statements.sh case 1 replays it.