Repository navigation
Seam walk: 3 prod panics + 10 unreachables + 28 TODOs + 6 proof holes (audit 2026-06-01) #41
Description
Background
Deep audit 2026-06-01 — companion to the verisimdb audit shape (verisimdb#77-#83). Records every soundness/completeness escape hatch in the codebase, classified by category. This is the seam-walk dimension.
Counts (excluding test code where noted)
| Category | Count | Notes |
|---|---|---|
panic! in production Rust |
1 | 47 of 48 panic!s in parser.rs are inside #[cfg(test)] test helpers. Real production panics: 1 in parser.rs, 2 in state.rs → 3 total |
unreachable! in production Rust |
10 | 6 in commands.rs, 1 each in quotes.rs, parser.rs, arith.rs; 1 in fuzz_targets/fuzz_state_machine.rs (intentional) |
unimplemented!() |
0 | |
TODO markers |
28 | Hot spots: src/functions.rs (6), tests/security_tests.rs (4), src/parser.rs (4), src/external.rs + src/audit_log.rs (2 each) |
FIXME / HACK / XXX |
0 | |
.unwrap() in production Rust |
424 | (not necessarily bugs — many are infallible by invariant. Triage by file: parser.rs / commands.rs / state.rs hotspots) |
.expect(…) in production Rust |
17 | |
Coq Admitted |
3 | proofs/coq/filesystem_composition.v:199 (single_op_reversible, OpRmdir branch) is the only documented one in ROADMAP |
Agda postulate |
3 | Down from 7 — 2026-04-03 closure session eliminated 4 |
Idris2 ?holes |
2 | RMO.idr:92 ?secureDeleteIrreversibleProof, RMO.idr:169 ?gdprDeletionCompliantProof |
Idris2 top-level partial |
10 | totality-check waived (in proofs/idris2/src/Filesystem/) |
Lean sorry / axiom |
0 |
Real production seam: 3 panics + 10 unreachables + 6 proof holes + 10 partial = 29 load-bearing escape hatches.
Top-5 findings (most load-bearing)
-
proofs/idris2/src/Filesystem/RMO.idr:92, :169— two holes (?secureDeleteIrreversibleProof,?gdprDeletionCompliantProof) at the GDPR / RMO core. These hold the entire "provably irreversible" claim. Without them, the marketing "mathematically irreversible secure deletion" is unfounded. -
proofs/coq/filesystem_composition.v:199—single_op_reversibleOpRmdirbranch isadmit.-ed. This is the only remaining Coq admit perdocs/PROOF_HOLES_AUDIT.md. Tied toobliterate_overwrites_all_blocks. -
impl/rust-cli/src/commands.rs— 6unreachable!sites in command dispatch. Each represents an assumed-impossible state in the FSM. If parser exposes any of these, we panic in production — needs taint analysis to verify which inputs can reach them. -
impl/rust-cli/src/audit_log.rsTODOs (2) +tests/security_tests.rs:338, :349— these are the append-only audit log and secure deletion stubs flagged inUNIMPLEMENTED_FEATURES.md. README's bullet "GDPR Compliance: Secure deletion (obliterate) + audit logging (stubs only)" is the audit footprint. -
impl/rust-cli/src/functions.rsTODOs (6) — Function-definition feature is documented as incomplete inCLAUDE.md("function nesting still incomplete"). The TODOs map directly to the gaps.
Resolution plan
- Phase 1 (1 PR each): close 2 Idris2 holes in RMO.idr + 1 Coq admit in filesystem_composition.v → unblocks the RMO/GDPR claim
- Phase 2: convert each
unreachable!to a typed-error return or document why genuinely unreachable; one-PR-per-file - Phase 3: implement secure_delete + audit_log per
UNIMPLEMENTED_FEATURES.md; close 2 of the highest-priority TODOs - Phase 4: tackle the 10 Idris2
partialmarkers — most are likely tractable now that totality landscape is well-understood (compare proven-stack patterns)
Companion issues: proof-inventory (next), test-expansion (next), docs-vs-standards (next).
References
docs/PROOF_HOLES_AUDIT.md— primary inventory (2026-04-12)UNIMPLEMENTED_FEATURES.md— stub cataloguedocs/tech-debt-2026-05-26.md— estate-scan baseline (9 markers; close-enough to this audit's count)
🤖 Filed by deep audit 2026-06-01
Activity
docs: max-out vs estate standards + fill INTENT.contractile + reconci…
hyperpolymath commentedon Jun 1, 2026
Phase 1 status (2026-06-01)
Idris2 side — finding from sub-agent sweep: the two
?holesatRMO.idr:92andRMO.idr:169cannot be honestly closed under their current type signatures.?secureDeleteIrreversibleProofclaimsrecovery fs = fs -> Voidfor an arbitraryrecoveryfunction.recovery = idsatisfies the premise without producingVoid, so no proof exists; this isn't a hole-to-fill, it's a theorem-shape bug.?gdprDeletionCompliantProofclaimsrecovery = idfor arbitraryrecovery : Filesystem -> Filesystem. Trivially refuted byrecovery = const empty.Per
MUST.contractile(nobelieve_me/assert_total/Admitted/sorry) and the no-fake-proofs policy, no PR was opened. Two redesign tickets filed instead:obliterate_not_injective)Coq side — closure attempt for
single_op_reversibleOpRmdir branch is in flight via a separate PR using theOpMkdirWithPermsvariant approach (path #2 of 3 documented in PR #47 Tier S F-2).Pre-existing blocker also surfaced:
proofs/idris2/src/Filesystem/Model.idrdoes not type-check under Idris2 0.8.0 (isJustundefined; missingEq Path/Eq (Path, FSEntry)instances at lines 103/108/135/152/169). There is nobuild-idris2Justfile target and no Idris2 CI job — the Idris2 "build oracle" referenced in policy doesn't yet exist for this repo. Will be addressed in a separate PR.Net: Phase 1 keystone closure is blocked on owner approval of #60/#61 redesigns + landing the Coq PR. Phases 2-4 unaffected.
proofs(coq): close single_op_reversible OpRmdir branch via OpMkdirWit…
proofs(idris2): make Filesystem.Model typecheck under Idris2 0.8.0 (#69)
feat(rust-cli): secure_delete + audit_log real impls + typed-error re…
chore: M2 ROADMAP + M3 doc-TODO sweep + M4 dep+action SHA refresh (#68)
hyperpolymath commentedon Jun 1, 2026
Sub-issue split filed (2026-06-01 Option 2 phase)
Per-category breakdown of the 29 load-bearing escape hatches:
Closed in this session: #41 Phase 1 Coq side (#67), Phase 1 practice gaps obliterate+audit_log (#72).
Still open: #60 / #61 — RMO.idr theorem-shape redesigns (Phase 1 Idris2 side).
hyperpolymath commentedon Jun 2, 2026
Status update 2026-06-02: sub-issues #45 / #60 / #61 / #70 / #89 closed by today's sweep. This umbrella remains open. See estate sweep memory entry for full PR list (#105/#106/#108/#109/#112/#113/#114/#115/#116).
docs: production charter — roadmap to v1.0.0 rewritten (owner ratific…