diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..1a5bf04 --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,148 @@ + + +# Proof Debt — betlang + +**Schema**: [`hyperpolymath/standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) +— the canonical estate-wide policy (standards#203). Companion to the +strategic narrative in [`../PROOF-NEEDS.md`](../PROOF-NEEDS.md). Detection +script: [`scripts/check-trusted-base.sh`](https://github.com/hyperpolymath/standards/blob/main/scripts/check-trusted-base.sh) +(standards#211). + +This file is the schema-conformant per-repo proof-debt index for +`hyperpolymath/betlang`. It enumerates every soundness-relevant escape +hatch in `proofs/BetLang.lean`. + +## Marker count (2026-05-27) + +`check-trusted-base.sh` reports **4 syntactic hits** under its Lean regex +(`\bsorry\b|^[[:space:]]*axiom[[:space:]]`); **1 is a real declaration** +and **3 are comment-line false positives** that the script's +`is_comment_line` heuristic strips. After comment-skip: **1 real marker** +— the single named axiom `substTop_preserves_typing`. + +| File:line | Raw token | Real? | Disposition | +|---|---|---|---| +| `proofs/BetLang.lean:19` | `sorry` (inside `-- All theorems are fully proved — no \`sorry\`.`) | false positive (comment) | n/a | +| `proofs/BetLang.lean:387` | `axiom` / `sorry` inside `-- IMPORTANT: This is NOT sorry — it is an axiom.` | false positive (comment) | n/a | +| `proofs/BetLang.lean:388` | `axioms` / `sorry` inside `-- axioms are explicit assumptions ... whereas sorry` | false positive (comment) | n/a | +| `proofs/BetLang.lean:392` | `axiom substTop_preserves_typing :` | **real** | §(d) DEBT | + +## (a) DISCHARGED in this repo + +*(None yet — entries move here when a marker is removed or replaced by a +total/proven counterpart.)* + +## (b) BUDGETED — tested with a refutation budget + +*(None. BetLang's proof file is pure Lean 4 metatheory; there is no +extraction-boundary surface needing a property-test budget.)* + +## (c) NECESSARY AXIOM + +*(None. The only real axiom in this repo (`substTop_preserves_typing`) +is **not** a metatheoretic assumption — it is a standard TAPL Ch.9 +substitution-preservation lemma with a known constructive discharge. +It is therefore classified as §(d) DEBT, not §(c) NECESSARY.)* + +## (d) DEBT — actively to be closed + +### `proofs/BetLang.lean:392` — `axiom substTop_preserves_typing` + +- **Statement**: `∀ (Γ : Ctx) (S T : Ty) (body v : Expr), HasType (S :: Γ) body T → HasType Γ v S → HasType Γ (substTop v body) T`. +- **Why it is §(d) and not §(c)**: this is the standard top-level + substitution-preservation lemma (Pierce, TAPL Ch.9). It is constructively + provable in Lean 4 by induction on the typing derivation, factored + through a generalised `substAt_preserves_typing` and three + context-insertion lookup lemmas. It does **not** encode a + metatheoretic assumption (no funExt, no choice, no UIP). It only + exists in the source because a full de Bruijn substitution calculus + would, per the inline doc-comment at L383-385, "triple the file size" + — a *cost* judgement, not a *necessity* judgement. +- **Owner**: @hyperpolymath +- **Plan** (verbatim from the discharge recipe in PR + [#27](https://github.com/hyperpolymath/betlang/pull/27) body, lightly + reformatted): + 1. **`Ctx.insertAt`** — define a context-insertion operator. (`Ctx` + is a `List Ty` `abbrev`, so dot-notation `Γ.insertAt` does not + resolve to anything useful; use a top-level + `def Ctx.insertAt (Γ : Ctx) (k : Nat) (U : Ty) : Ctx := + Γ.take k ++ U :: Γ.drop k`.) + 2. **Three lookup lemmas**, all needing the `k ≤ Γ.length` + hypothesis (without which they are false at empty Γ with k > 0): + - `lookup_ctxInsertAt_lt : n < k → Ctx.lookup (ctxInsertAt Γ k U) n = Ctx.lookup Γ n` + - `lookup_ctxInsertAt_eq : Ctx.lookup (ctxInsertAt Γ k U) k = some U` + - `lookup_ctxInsertAt_gt : n > k → Ctx.lookup (ctxInsertAt Γ k U) n = Ctx.lookup Γ (n - 1)` + 3. **`shift_preserves_typing`** (weakening at `amount = 1`): + `HasType Γ e T → ∀ k U, k ≤ Γ.length → HasType (ctxInsertAt Γ k U) (shift 1 k e) T`. + Induction on `HasType`; binder cases (`tLam`, `tLet`) bump `k` by 1 + and recurse. Variable case needs `Int.toNat (↑n + 1) = n + 1`. + 4. **`subst_preserves_typing`** (generalised): + `HasType (ctxInsertAt Γ k S) e T → HasType Γ v S → HasType (ctxInsertAt Γ k S) (subst k (shift (k+1 : Int) 0 v) e) T`. + Induction on `e`. Binder cases recurse with `k+1` after pulling in + the extra `shift 1 0`. + 5. **"No surviving var k" tracking lemma**: after `subst k v e`, define + a predicate `freeVarNotIn k e` and prove it holds. Then prove + `shift_down` preserves typing when this predicate holds. + 6. **Headline**: + `substTop_preserves_typing Γ S T body v hb hv := ...` combining the + chain. Then delete `axiom substTop_preserves_typing` at L392. + Verify `preservation` still typechecks. +- **Estimated size**: ~300-400 LoC of standard TAPL Ch.9 mechanisation. + The `Int.toNat` clamping in BetLang's `shift` (signed `amount`) adds + non-trivial arithmetic friction at every `var` case. +- **Status**: a partial implementation lives on the local working + branch `proofs/discharge-substTop-axiom-23` (commit `8fa128d` + "proofs: discharge substTop_preserves_typing axiom (closes #23)"), + not yet opened as a PR. Issue + [#23](https://github.com/hyperpolymath/betlang/issues/23) was closed + optimistically when PR #27 merged the build-fix half of the work; + the axiom itself remained in source. +- **Deadline**: INDEFINITE — single-maintainer repo; discharge is bounded + in scope but not currently scheduled. Re-open issue #23 (or file a + successor) when work resumes. + +## Cross-language survey (Idris2) + +The repo also contains Idris2 test scaffolding under `tests/idris2/**` +and `playground/tests/idris2/**`. `check-trusted-base.sh` finds **zero** +`believe_me` / `really_believe_me` / `assert_total` / top-level +`partial` markers in those files. No §(b)/(c)/(d) entries needed. + +## How to update this file + +When markers in `proofs/BetLang.lean` (or any future proof-bearing file) +change: + +1. Re-run `bash scripts/check-trusted-base.sh .` (the script is + delivered from `hyperpolymath/standards` and called from the + governance bundle). +2. If the count drops, move the resolved entries from §(d) → §(a). +3. If new markers appear, add them to §(d) with an owner + (possibly + INDEFINITE) deadline. +4. The `trusted-base` CI job (`governance-reusable.yml`, landed in + standards#211) will fail on un-annotated AND un-enumerated markers + — so every change in source MUST be reflected here. + +## Companion documents + +- [`../PROOF-NEEDS.md`](../PROOF-NEEDS.md) — the strategic proof-debt + narrative for betlang. +- [hyperpolymath/standards#203](https://github.com/hyperpolymath/standards/pull/203) + — the policy this file conforms to. +- [hyperpolymath/standards#211](https://github.com/hyperpolymath/standards/pull/211) + — `scripts/check-trusted-base.sh` and the `trusted-base` job. +- [hyperpolymath/standards#222](https://github.com/hyperpolymath/standards/pull/222) + — the fill-in PR for the policy doc. +- [hyperpolymath/betlang#23](https://github.com/hyperpolymath/betlang/issues/23) + — the (closed) tracking issue for discharging + `substTop_preserves_typing`. +- [hyperpolymath/betlang#27](https://github.com/hyperpolymath/betlang/pull/27) + — the merged PR whose body contains the canonical discharge recipe. + +--- + +Initial seed by Claude Code, 2026-05-27, applying the standards#203 +schema to betlang per the standards#222 per-repo triage pass. diff --git a/proofs/BetLang.lean b/proofs/BetLang.lean index 8dcd466..29a5a7d 100644 --- a/proofs/BetLang.lean +++ b/proofs/BetLang.lean @@ -389,6 +389,12 @@ theorem progress {e : Expr} {T : Ty} (ht : HasType [] e T) : is a proof hole. We could discharge this axiom by building the full shifting/substitution calculus, but that is orthogonal to the BetLang-specific content of this formalisation. -/ +-- AXIOM: substTop_preserves_typing — disposition §(d) DEBT (NOT §(c) necessary). +-- The axiom is standard TAPL Ch.9-style substitution preservation; a full +-- de Bruijn discharge has a known recipe (PR #27 body) and a partial +-- implementation on branch `proofs/discharge-substTop-axiom-23` (~300-400 LoC). +-- See docs/proof-debt.md §(d) entry "substTop_preserves_typing" for plan, +-- owner, and discharge recipe. axiom substTop_preserves_typing : ∀ (Γ : Ctx) (S T : Ty) (body v : Expr), HasType (S :: Γ) body T → HasType Γ v S → HasType Γ (substTop v body) T