# Qed Remediation TODOs — Priority-Ordered

**Generated:** 2026-04-19
**Last revised:** 2026-04-20
**Companion:** `QED-NARRATIVE-2026-04-19.md` (prose context, what each path leads to)

Priority = tractability × impact, sorted per standing priority order
(dependability > security > interop > usability > performance > versatility > extension).

---

## Done (do not re-do)

- [x] **oblibeny/Interface.idr** — 2 `believe_me` discharged (commit `3aedee9`, 2026-04-20). `installReversible` + `doubleInstallIdempotent` now structural.
- [x] **cerro-torre/CryptoProofs.idr:81,90** — 2 `assert_total $ idris_crash` replaced with `partial + idris_crash`; partiality propagated (`25be6d7` + `83afc01` + `a71ac3b`, 2026-04-19).

---

## Live TODOs

### [ ] 1. Resolve my-lang dual-truth drift  — *one session, destructive*

- **Sites:** `developer-ecosystem/my-lang/proofs/verification/coq/Typing.v:173,182,192` (3 `Admitted.`).
- **Canonical:** `nextgen-languages/my-lang/Typing.v` — 745 lines, 0 Admitted.
- **Action:** delete the stale standalone clone, OR wire it as a submodule pointing at the canonical path.
- **Blocker:** destructive op — needs user confirmation.
- **Payoff:** 3 Admitted discharged at zero proof cost; eliminates a dual-truth hazard class.

### [ ] 2. Audit boj-server documented-axiomatic sites  — *cheap, ~30 min*

- **Sites:**
  - `boj-server/src/abi/Boj/SafetyLemmas.idr` — 3× `believe_me`
  - `boj-server/src/abi/Boj/SafeAPIKey.idr:152` — 1× `believe_me` (`logSafeBounded`)
- **Action:** verify each site's in-file documentation still matches the code. Cross-check against memory `boj-server-believe-me-sweep.md`. If drifted, either re-prove or update docs.
- **Payoff:** keeps the "documented axiomatic" category honest; flags backend-primitive drift early.

### [ ] 3. Refactor `verifyChain` to unblock `chainCommutative`  — *medium session*

- **Site:** `fleet-ecosystem/stapeln/container-stack/cerro-torre/verification/idris/SignatureProofs.idr :: chainCommutative` (currently `partial + idris_crash` postulate).
- **Action:** rewrite `verifyChain = allValid ∘ map verifyPair` with Bool-head pattern match. Re-prove `chainHeadValid` / `chainTailValid` / `chainImpliesIndividual` as a coupled set against the new shape. Remove the postulate; close with structural proof.
- **Reason:** with-abstraction is syntactic; current `verifyChain` shape keeps `verifyEd25519 …` off the goal at abstraction time.
- **Payoff:** regression closes; cerro-torre signature-chain soundness complete modulo the Ed25519 primitive itself.
- **Deferred-plan refs:** in-file diagnosis + `PROOF-NEEDS.md §"chainCommutative regression"`.

### [ ] 4. Close `ephapax/Semantics.v` preservation  — *multi-hour, budget a block*

- **Site:** `developer-ecosystem/nextgen-languages/ephapax/formal/Semantics.v:2948` — 1× `Admitted.` on preservation (S_Region_Exit case).
- **Action:** implement Option C TFun region-capture refactor (prototyped, deferred).
  - Add `free_regions : T → set region`.
  - Prove `expr_free_of_region` variant for TFun shape.
  - Prove `region_shrink_preserves_typing` variant.
  - Add `r ∉ free_regions T` premise to `T_Region` / `T_Region_Active`.
  - Close the S_Region_Exit branch.
- **Context:** Option B landed 2026-04-20 (branch `docs/vision-relocation-2026-04-17`); 2 narrow structural admits remain on region-env weakening.
- **Payoff:** end-to-end language soundness; downstream claims depending on preservation become theorems.

### [ ] 5. 007 canonical-suite `Parameter` audit  — *mechanical, high volume*

- **Scope:** 266 `Parameter` declarations across the suite.
- **Per memory:** v1.0 in-progress entries (M2, M3, M4, S3, S4, E1, E5) must not use the Parameter-axiom shortcut per `AI-WORK-007.md §3.1`. v1.1 entries (M11 pattern) allow it.
- **Action:** walk each listed v1.0 entry; flag any Parameter used as axiom-shortcut; either import/build the analytic layer (Stdlib.Reals, Coquelicot, mathcomp) or convert to explicit-predicate-arg.
- **Reference for Coquelicot gotchas:** memory `feedback_coquelicot_proof_gotchas.md`.
- **Payoff:** v1.0 label becomes a stronger claim than v1.1; no hidden shortcuts.

### [ ] 6. absolute-zero Axiom triage  — *review-only session*

- **Scope:** 175 `Axiom` declarations across physics modules.
- **Action:** per declaration, classify as {physics postulate, measurement primitive, owed-proof escape}. Tag in-file or in `.machine_readable/axiom-triage.a2ml`.
- **Urgency:** low (Axiom is Coq-legitimate). Volume: high.
- **Payoff:** external verification can weight claims by grounding strength rather than treating "Qed modulo 175 axioms" as an aggregate.

---

## Not-on-this-list (policy exclusions, for reference)

- `rescript/compiler/*` — 52 `Obj.magic`. Vendored upstream. Not ours.
- `developer-ecosystem/linguist/samples/Rocq Prover/JsCorrectness.v` — 71 `Admitted.`. GitHub Linguist detection corpus. Excluded.
- `echidna/AxiomCompleteness.idr` — banned tokens as string literals (detection table). Excluded by path.
- `hyperpolymath-archive/zotero-formbd/Journal.lean` — 2 `sorry`. Archived repo. Skipped.

---

## Audit-hygiene reminders

- Code-only grep: `^[^-|]*<pattern>` for Idris; equivalent per language.
- Deduplicate submodule shadows before counting.
- Check drift via `diff -q` between suspected dual copies.
- Exclude detection tables by path, not regex.
- `Axiom` / `Parameter` / `postulate` ≠ banned — but run their own discipline audit (items 5 + 6).
