From 505b590a5c3308faab8d6b4b7ab9868d2bce9dc0 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 26 May 2026 16:55:03 +0100 Subject: [PATCH] docs: seed docs/proof-debt.md per trusted-base policy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per the trusted-base reduction policy (hyperpolymath/standards#203), enumerate every soundness-relevant escape hatch in this repo with its disposition. Initial state: - §(a) DISCHARGED: none yet. - §(b) BUDGETED: none (ephapax's proofs are deductive, not property- tested at the working layer). - §(c) NECESSARY AXIOM: none (no funExt etc. introduced). - §(d) DEBT — 3 entries: - formal/Semantics.v:4924 — Admitted inside step_preserves_type - formal/Semantics.v:5983 — Admitted inside step_output_context_eq - formal/Semantics.v:6572 — Admitted inside preservation All three are within the preservation proof corpus and are already owned by the project_ephapax_preservation_closure_plan (6-9 day discharge plan; deadline 2026-09-01). This file is the per-repo schema the future scripts/check-trusted-base.sh will validate against (mirror of standards#201 check-licence-consistency.sh). Co-Authored-By: Claude Opus 4.7 (1M context) --- docs/proof-debt.md | 104 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 docs/proof-debt.md diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..8eef97c --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,104 @@ + + +# Proof Debt — ephapax + +**Schema**: [hyperpolymath/standards `TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) (standards#203). + +This file enumerates every soundness-relevant escape hatch in the ephapax +codebase and its disposition under the trusted-base policy. Markers without +an entry below count as undocumented debt and will be flagged by +`scripts/check-trusted-base.sh` once that lands. + +Markers in scope (from the 2026-05-26 estate proof-debt audit, +standards#195): +- Coq `Axiom`, `Admitted`, `admit.` +- Idris2 `believe_me`, `assert_total`, top-level `partial` +- `TODO PROOF` / `OWED:` / `FIXME PROOF` markers + +## (a) DISCHARGED in this repo + +*(None yet — entries move here when their proof lands.)* + +## (b) BUDGETED — tested with a refutation budget + +*(None — ephapax's proof targets are deductive, not property-tested. Items +in this section would belong here if/when we add adversarial-test budgets +for the Rust↔Idris2 ABI boundary code.)* + +## (c) NECESSARY AXIOM + +*(None — ephapax does not introduce any irreducible metatheoretic axioms +in the working Coq logic. If future work adds e.g. `funExt`, list it here +with a citation to its canonical formalisation.)* + +## (d) DEBT — actively to be closed + +### `formal/Semantics.v:4924` — `Admitted` inside `step_preserves_type` + +- **Lemma**: `step_preserves_type` (declared at `formal/Semantics.v:3615`). +- **Statement (informal)**: small-step semantics preserve typing. +- **Owner**: @hyperpolymath +- **Plan**: discharge as part of [project_ephapax_preservation_closure_plan](https://github.com/hyperpolymath/standards/blob/main/docs/audits/2026-05-26-estate-proof-debt.md). Estimated 6–9 days. ~40 goals split into sub-buckets A/B/C/D; start with A. +- **Deadline**: 2026-09-01 (per closure plan). + +### `formal/Semantics.v:5983` — `Admitted` inside `step_output_context_eq` + +- **Lemma**: `step_output_context_eq` (declared at `formal/Semantics.v:4944`). +- **Statement (informal)**: output context is preserved across a step + (modulo region marking). +- **Owner**: @hyperpolymath +- **Plan**: discharged as a corollary of the strengthened + `step_preserves_type` proof; depends on the preservation closure plan. +- **Deadline**: 2026-09-01. + +### `formal/Semantics.v:6572` — `Admitted` inside `preservation` + +- **Theorem**: `preservation` (declared at `formal/Semantics.v:5985`). +- **Statement (informal)**: the main preservation theorem for the ephapax + region-aware operational semantics. +- **Owner**: @hyperpolymath +- **Plan**: this is the top-level theorem the other two Admitteds feed + into. Discharge order: `step_preserves_type` first → then + `step_output_context_eq` → then `preservation` lands automatically + modulo wiring. +- **Deadline**: 2026-09-01. + +## Soundness-relevant escape hatches in non-Coq code + +The 2026-05-26 audit also surfaced: +- 1 `believe_me` reference (a comment in + `src/formal/Ephapax/Formal/RegionLinear.idr:127` explicitly stating + "This is a REAL proof — not (), not believe_me, not assert_total" — + no actual `believe_me` use; the comment is documentation about NOT + using it). +- 1 `partial` (Idris2 totality waiver) — TBD if real or comment artefact. +- 14 `TODO PROOF` / `OWED:` markers — these were not located in this + repo by the per-repo scan; they likely cluster around the same + Admitteds above. + +When `scripts/check-trusted-base.sh` lands, any genuine occurrence of +the above will require either a leading `TRUSTED:` / `AXIOM:` annotation +or a `§(d) DEBT` entry here. + +## How to update this file + +After each PR that closes one of the entries above: + +1. Move the entry from §(d) → §(a) DISCHARGED. +2. Update the closure plan referenced. +3. Run `git cliff --output CHANGELOG.md` to regenerate the changelog + (see [standards#206](https://github.com/hyperpolymath/standards/pull/206) for + the canonical workflow). + +## Companion documents + +- [standards#195](https://github.com/hyperpolymath/standards/pull/195) — estate proof-debt audit +- [standards#203](https://github.com/hyperpolymath/standards/pull/203) — trusted-base reduction policy (the schema this file follows) +- `project_ephapax_preservation_closure_plan` (maintainer memory) — 6–9 day discharge plan + +--- + +🤖 Initial seed by Claude Code, 2026-05-26.