ltl-accumulator-verified/KNOWN-GAPS.md

# 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 (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` accepts strictly more than the
   mechanized `ConsRec` on lied-size inputs** (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 RFC 9162 iterative
   algorithm seeds the walk with the old root and uses the sizes only
   as bit-navigation state, so several size claims navigate one proof
   identically. 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). No pacta code change is
   made (deployed behavior matches upstream RFC 9162 implementations).
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.