Idris htSubst structure (b-erasure solved, 10/15) + AFFIRMATION & status docs

AFFIRMATION.adoc

@@ -0,0 +1,87 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Affirmation
+:toc: preamble
+:sectnums:
+:revdate: 2026-06-19T21:35:54Z
+:revnumber: 1
+
+This AFFIRMATION records the standing of *my-lang* against the hyperpolymath
+standards and this project's own honesty discipline, at the timestamp below.
+It follows the AFFIRMATION convention of the hyperpolymath `standards`
+repository (governance + Hypatia); that guidance could not be read in the
+session that authored this file, so it is followed *in spirit*, per the RSR
+(Rhodium Standard Repository) discipline this repo consumes. Refine against
+the canonical template when `standards` is in scope.
+
+This is a point-in-time affirmation, not a perpetual claim: it is true of the
+verified state at `:revdate:` and is superseded by the next dated affirmation.
+
+== Scope of affirmation
+
+my-lang is the QTT (quantitative type theory) multi-dialect language with a
+mechanised solo-core proved on *dual tracks* (Coq + Idris2) and an AI-first
+Rust compiler. The normative obligation — the *must* — is that the language be
+*sound*, and that its soundness *live in the compiler* and not merely on paper.
+
+== Affirmed true at this timestamp
+
+To the verified state of this repository, I affirm:
+
+. *Soundness is mechanised, not asserted.* The Coq solo-core proves
+  `progress`, `preservation`, and `affine_pres`; the algorithmic checker
+  (`check`, R5) and the affine decision (`aff_type_dec`, R5b); the
+  `me -> solo` elaboration adequacy (M1); the session-pi metatheory through
+  S3c.3; and the echo residue-measure seam (E4). All are real `Qed`,
+  *axiom-free* (`Print Assumptions` closed), and CI-gated.
+
+. *No overclaim.* Every proof hole is recorded as an obligation, never as a
+  result (`proofs/STATUS.md` is authoritative and wins over any prose).
+  Honest-scope and matched-negative discipline is kept throughout the
+  formalisation.
+
+. *The coupling is real.* The machine-checked usage-walk is now executed by
+  the compiler, not re-implemented ad hoc: `crates/my-qtt` is a faithful Rust
+  port of the Coq R5/R5b algorithm (checked against that algorithm's own
+  `reflexivity` examples), and `crates/my-lang/src/qtt_bridge.rs` lowers the
+  running compiler's real `ast::Expr` onto it. The proofs and the
+  implementation are no longer disconnected universes.
+
+. *Provenance is honoured.* MPL-2.0 throughout; SPDX headers on files; sole
+  -maintainer governance (`GOVERNANCE.adoc`); RSR-consumer status; no
+  postulates, no `--safe` weakening, no escape pragmas in the trusted base.
+
+== Integrity basis
+
+* Coq: `.github/workflows/proofs.yml` compiles the solo-core and asserts the
+  headline theorems are axiom-free on every PR touching `proofs/verification/**`.
+* Idris2: `idris2 --build` under `%default total`; the only open marker is
+  `?todo_preservation` plus the five `htSubst` usage-splitting holes.
+* Rust: `cargo test -p my-qtt` and `cargo test -p my-lang qtt_bridge` green;
+  `my-qtt` carries the R5/R5b oracle tests.
+
+== Affirmed NOT done (the honest boundary)
+
+The Idris twin's `preservation` (`#108`) is *not* proved. The QTT substitution
+lemma `htSubst` is structurally landed (10 of 15 cases; the `b`-index erasure
+resolved) and committed locally; the five usage-splitting cases, the
+`substLemma0` / `subst2Lemma` corollaries, and `preservation` itself remain
+open. This is the single outstanding *must*. The wasm / RISC-V / mobile /
+typed-wasm legs are *intends* and *wishes* (`docs/STATUS.adoc`), not affirmed
+as done.
+
+== Affirmation
+
+I affirm the above as a true account of this repository's verified standing at
+the timestamp recorded, and I stand behind its honesty discipline: nothing
+herein is described as proved that a proof assistant does not accept today.
+
+[cols="1,3"]
+|===
+| Affirmed by | Jonathan D.A. Jewell (@hyperpolymath) <j.d.a.jewell@open.ac.uk>
+| Repository  | hyperpolymath/my-lang
+| Timestamp (UTC) | 2026-06-19T21:35:54Z
+| Verified basis | `main` @ `a7765e7` (merged: PR #116 `my-qtt`, PR #117 coupling step 2); dev `acd29d6` (`htSubst` structure)
+| Authority | `proofs/STATUS.md` (proofs) · `docs/STATUS.adoc` (programme) · `.machine_readable/contractiles/Mustfile.a2ml` (invariants)
+|===

docs/STATUS.adoc

@@ -0,0 +1,72 @@
+// SPDX-License-Identifier: MPL-2.0
+// Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= my-lang — Status: Musts / Intends / Wishes
+:toc:
+:sectnums:
+:revdate: 2026-06-19
+
+Snapshot of where my-lang stands, grouped by contractile priority — *Must*
+(hard normative obligation; see `.machine_readable/contractiles/Mustfile.a2ml`),
+*Intend* (roadmap; `Intentfile.a2ml`), *Wish* (stretch / blocked). The
+**normative must is my-lang itself**: the language being sound, and that
+soundness living in the compiler rather than only on paper.
+
+Status legend: `[x]` done / merged · `[~]` in progress · `[ ]` not started ·
+`[!]` blocked. The authoritative proof registry is `proofs/STATUS.md`; this
+file is the priority-grouped programme view.
+
+== Position (one line)
+
+my-lang's normative must is essentially met — the Coq metatheory is complete
+and axiom-free, and the verified usage-checker is merged into the Rust
+toolchain. The single open must is the Idris twin's `preservation`,
+structurally landed (10/15 `htSubst` cases, `b`-erasure solved), committed
+locally at `acd29d6`.
+
+== MUST — my-lang itself (sound core, verified-coupled, compiling)
+
+[cols="4,1,2",options="header"]
+|===
+| Item | Status | Where
+| QTT core soundness (Coq): `progress` / `preservation` / `affine_pres`, axiom-free, CI-gated | `[x]` | `main`
+| Algorithmic checker `check` (R5) + affine decision `aff_type_dec` (R5b), Coq | `[x]` | `main`
+| `me -> solo` elaboration adequacy (M1), Coq | `[x]` | `main`
+| Session-pi soundness S1–S3c.3 (Ensemble / Duet by projection), Coq | `[x]` | `main`
+| Echo residue-measure seam (E4), Coq | `[x]` | `main`
+| Verified usage-checker IN the compiler — `my-qtt` (faithful R5/R5b port) | `[x]` | `main` (PR #116)
+| Surface -> core coupling (named engine + real `ast::Expr` bridge) | `[x]` | `main` (PR #117)
+| Idris twin `progress` (total, hole-free) | `[x]` | `main`
+| Working compiler pipeline parse->HIR->MIR->LLVM->native (x86_64 / aarch64) | `[x]` | `main`
+| **Idris twin `preservation` (#108)** — `htSubst` structure + `b`-erasure solved | `[~]` 10/15 cases | local `acd29d6`
+|===
+
+== INTEND — planned next
+
+[cols="4,1,3",options="header"]
+|===
+| Item | Status | Note
+| Close Idris `preservation`: 5 `htSubst` split cases -> `substLemma0` / `subst2Lemma` | `[~]` next | consumes the landed `usplit3` / `uaddSplitBoundary2` / `substReassocAdd` / `substReassocMult`
+| Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[ ]` | the QTT bridge is opt-in (`qtt_bridge::check_expr`) today
+| Surface *quantity syntax* so the bridge enforces real per-binder linearity | `[ ]` | `Param` has no quantity field; bridge defaults to `One`
+| `wasm32` via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`) | `[ ]` | fastest target leg; backend already emits objects
+| `RISC-V` (`riscv64gc-unknown-linux-gnu`) via LLVM | `[ ]` | near-free once `wasm32` target wiring exists
+|===
+
+== WISH — stretch / blocked
+
+[cols="4,1,3",options="header"]
+|===
+| Item | Status | Note
+| typed-wasm WasmGC verified leg | `[!]` blocked | needs `typed-wasm` / AffineScript / Ephapax added to the working session; gated upstream on WasmGC recursive types
+| Android / iOS via Tauri 2.0+ / Dioxus | `[ ]` | policy-documented, no integration code
+| Duet / Ensemble dialect compilers | `[ ]` | scaffold only; Solo is the live dialect
+| Full surface coverage in the bridge (binary / `match` / records / AI exprs) | `[ ]` | resource fragment only today (the rest returns `Unsupported`)
+|===
+
+== Provenance
+
+* Coq: axiom-free (`Print Assumptions` closed), CI-gated (`.github/workflows/proofs.yml`), no `Admitted`/`Axiom` in the trusted base.
+* Idris: `idris2 --build`-checked, `%default total`, no postulates; only `?todo_preservation` and the 5 `htSubst` split holes open.
+* Rust: `cargo test -p my-qtt` (20 tests incl. the R5/R5b `reflexivity` oracle tests + the surface-coupling tests) and `cargo test -p my-lang qtt_bridge` (6 tests) green.
+* Landed this programme increment: PR #116 (`my-qtt`), PR #117 (coupling step 2); local `acd29d6` (`htSubst` structure).

docs/handoff/NEXT-SESSION.md

@@ -0,0 +1,73 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+<!-- Handoff prompt — paste to the next Claude working on my-lang. Dated 2026-06-19. -->
+
+# Next-session prompt — my-lang (paste this to the next Claude)
+
+You are continuing work on **my-lang** (the QTT multi-dialect language with a
+mechanised Coq + Idris2 solo-core and an AI-first Rust compiler). Develop on
+branch `claude/dreamy-hypatia-O8XHo`; commit green slices; push and open a
+**draft** PR when a slice is complete. Read `docs/STATUS.adoc` (musts/intends/
+wishes) and `proofs/STATUS.md` (authoritative proof registry) first.
+
+## The one open MUST: close Idris `preservation` (#108)
+
+The Coq metatheory is complete and axiom-free. The Idris twin's `progress` is
+done; **`preservation` is the last normative obligation** (`?todo_preservation`
+in `proofs/verification/idris/solo-core/Soundness.idr`). It rests on the QTT
+substitution lemma `htSubst`, which is now **structurally landed** (commit
+`acd29d6` on the dev branch, build green 8/8):
+
+- **10/15 `htSubst` cases proved**: Var, Unit, Lam, With, Fst, Snd, Inl, Inr,
+  MkEcho, Weaken.
+- **5 usage-splitting holes remain** in `Substitution.idr`:
+  `?htSubst_app`, `?htSubst_tensor`, `?htSubst_letpair`, `?htSubst_case`,
+  `?htSubst_let`.
+
+### Do this, in order
+1. Fill the 5 split holes. Each mirrors the Coq `ht_subst` case in
+   `proofs/verification/coq/solo-core/SoloCore.v` (≈ lines 1618–1889) and
+   **consumes already-landed lemmas**: `usplit3`, `uaddSplitBoundary2`,
+   `substReassocAdd` (additive, for App/Let), `substReassocMult` (for
+   Tensor/LetPair/Case), `uaddUappend`, `uscaleUappend`, `ushiftUscale`.
+   App splits `d1` and the `q`-scaled `d2`; Tensor/LetPair/Case split `d1`,`d2`;
+   Let scales `d1`. The binder cases (LetPair/Case/Let) recurse into bodies with
+   the prefix `I` extended (mirror the `hvSubst`/`htShift` binder pattern).
+2. Add `substLemma0` (the `I = TEmpty` corollary) and `subst2Lemma` (two-var,
+   for `LetPair`), mirroring Coq `subst_lemma0` / `subst2_lemma` (≈ 1893–1937).
+3. Fill `?todo_preservation` in `Soundness.idr` by induction on `Step`
+   (mirror Coq `preservation`, ≈ 1941–2036): reduction cases use
+   `substLemma0`/`subst2Lemma`; congruence cases recurse.
+4. Move the `preservation` row in `proofs/STATUS.md` to *machine-checked* and
+   update `docs/STATUS.adoc`.
+
+### Load-bearing context (do NOT relitigate)
+- **`b`-erasure is solved.** The result type `b` is a genuine type index, so
+  `hvSubst` and `htSubst` both carry it as an **erased implicit** (`{0 b}` /
+  auto-bound). Passing an *unrestricted* `b` (or an erased `b` to an
+  unrestricted param) gives "`{b}` is not accessible" — keep it erased on both.
+- **Let-clause quantity clash:** match `THLet`'s quantity field with `_` (the
+  term's `q'` forces it; two named patterns "unify with" each other otherwise).
+- **`THLet`/`THCase`/`THLetPair` carry explicit bound-type fields** (Option A,
+  already merged) — that is how the binder cases recover the body context under
+  erasure. Don't revert it.
+- Toolchain: Idris2 0.7.0 isn't preinstalled — bootstrap from source
+  (`make bootstrap SCHEME=chezscheme && make install`, ~10 min), then
+  `cd proofs/verification/idris/solo-core && idris2 --build solo-core.ipkg`.
+  Discipline: every edit ends with a compile; `--safe`/`%default total`; no
+  postulates; pin headline theorems where the repo convention does.
+
+## The other axis: fundamentals -> compilation (see docs/STATUS.adoc)
+
+The verified usage-checker is now in the compiler (`crates/my-qtt` =
+faithful R5/R5b port; `crates/my-lang/src/qtt_bridge.rs` lowers real
+`ast::Expr` and runs it). Next intends: make the QTT check the *default* in
+`checker.rs`; add surface **quantity syntax** so linearity is enforced for
+real; then **wasm32 via the existing LLVM backend** (`TargetSpec::wasm32` is
+defined but unwired — add the `wasm-ld` link path), then **RISC-V**, then the
+**typed-wasm** WasmGC verified leg (blocked until the `typed-wasm` /
+AffineScript / Ephapax repos are added to the session).
+
+## Don't reopen
+The merged `my-qtt` and coupling (PRs #116/#117); the `b`-erasure design; the
+Option-A bound-type fields; the Coq core (complete, axiom-free).

proofs/verification/idris/solo-core/Substitution.idr

@@ -689,23 +689,23 @@ substVarSucc k u n with (compare n k) proof eq
 ||| (mirrors Coq `hv_subst`); `htSubst`'s `Var` case is this lemma.
 public export
 hvSubst : (i, g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (di : Uvec)
-       -> (n : Nat) -> (b : Ty) -> (du : Uvec) -> (u : Tm)
+       -> (n : Nat) -> {0 b : Ty} -> (du : Uvec) -> (u : Tm)
        -> ulen di = tlen i
        -> HasVar (tappend (TSnoc g a) i) (uappend (USnoc dg q) di) n b
        -> Has g du u a
        -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr,
             Has (tappend g i) (uappend dgr di)
                 (substAt (tlen i) (shiftn (tlen i) u) (Var n)) b))
-hvSubst TEmpty g a dg q (USnoc _ _) n b du u hlen hv hu = void (sNotZ' hlen)
-hvSubst TEmpty g a dg q UEmpty Z b du u hlen hv hu =
+hvSubst TEmpty g a dg q (USnoc _ _) n du u hlen hv hu = void (sNotZ' hlen)
+hvSubst TEmpty g a dg q UEmpty Z du u hlen hv hu =
   case varInv hv of
     VIT hdq hn hv' => void (zNotS' hn)
     VIH hdq hn hb =>
       let (hdg, hq) = usnocInj hdq
       in (du ** (rewrite hdg in rewrite hq in rewrite uscaleOne du in
                    uaddZeroL g du (shapeType g u hu),
                  rewrite hb in hu))
-hvSubst TEmpty g a dg q UEmpty (S n0) b du u hlen hv hu =
+hvSubst TEmpty g a dg q UEmpty (S n0) du u hlen hv hu =
   case varInv hv of
     VIH hdq hn hb => void (sNotZ' hn)
     VIT hdq hn hv' =>
@@ -715,8 +715,8 @@ hvSubst TEmpty g a dg q UEmpty (S n0) b du u hlen hv hu =
       in (dg ** (rewrite hq in
                    uaddUscaleZeroR dg du (trans (shapeVar g hv'') (sym (shapeType g u hu))),
                  rewrite minusZeroRight n0 in THVar hv''))
-hvSubst (TSnoc i' c) g a dg q UEmpty n b du u hlen hv hu = void (zNotS' hlen)
-hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) Z b du u hlen hv hu =
+hvSubst (TSnoc i' c) g a dg q UEmpty n du u hlen hv hu = void (zNotS' hlen)
+hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) Z du u hlen hv hu =
   case varInv hv of
     VIT hdq hn hv' => void (zNotS' hn)
     VIH hdq hn hb =>
@@ -730,16 +730,79 @@ hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) Z b du u hlen hv hu =
              uaddUscaleZeroR (uzero g) du (trans (uzeroLen g) (sym (shapeType g u hu))),
            rewrite hb in rewrite hqd in rewrite hdi in
              rewrite sym (uzeroTappend g i') in THVar HVHere))
-hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) (S n0) b du u hlen hv hu =
+hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) (S n0) du u hlen hv hu =
   case varInv hv of
     VIH hdq hn hb => void (sNotZ' hn)
     VIT hdq hn hv' =>
       let (hd0, hqd) = usnocInj hdq
-          (dgr ** (hadd, hht)) = hvSubst i' g a dg q di' n0 b du u (predEq' hlen)
+          (dgr ** (hadd, hht)) = hvSubst i' g a dg q di' n0 du u (predEq' hlen)
                                    (rewrite hd0 in rewrite predEq' hn in hv') hu
       in (dgr **
           (hadd,
            rewrite hqd in
              rewrite substVarSucc (tlen i') u n0 in
              htShift0 (tappend g i') c (uappend dgr di')
                       (substAt (tlen i') (shiftn (tlen i') u) (Var n0)) hht))
+
+------------------------------------------------------------
+-- 4c (cont). The QTT substitution lemma: htSubst
+------------------------------------------------------------
+
+||| The QTT substitution lemma (mirrors Coq `ht_subst`): substitute `u` (typed
+||| at `du`) for the boundary variable of type `a` in a derivation of `t`, under
+||| a prefix `I` of crossed binders. Residual usage `dg + q·du`. The result type
+||| `b` is an ERASED (auto-bound) implicit — a genuine type index, never passed
+||| at runtime; `hvSubst` likewise erases its `b`, keeping the `Var` case's call
+||| erasure-consistent (ADR-003 index-erasure discipline).
+public export
+htSubst : (t : Tm) -> (i, g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q)
+       -> (di : Uvec) -> (du : Uvec) -> (u : Tm)
+       -> ulen di = tlen i
+       -> Has (tappend (TSnoc g a) i) (uappend (USnoc dg q) di) t b
+       -> Has g du u a
+       -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr,
+            Has (tappend g i) (uappend dgr di)
+                (substAt (tlen i) (shiftn (tlen i) u) t) b))
+htSubst (Var n) i g a dg q di du u hlen (THVar hv) hu =
+  hvSubst i g a dg q di n du u hlen hv hu
+htSubst UnitT i g a dg q di du u hlen h hu =
+  let (hd, hb)    = unitInv h
+      (hdgq, hdi) = uappendInj di (uzero i) (USnoc dg q) (USnoc (uzero g) Zero)
+                      (trans hlen (sym (uzeroLen i)))
+                      (trans hd (uzeroTappend (TSnoc g a) i))
+      (hdg, hq)   = usnocInj hdgq
+  in (uzero g **
+      (rewrite hdg in rewrite hq in
+         uaddUscaleZeroR (uzero g) du (trans (uzeroLen g) (sym (shapeType g u hu))),
+       rewrite hb in rewrite hdi in rewrite sym (uzeroTappend g i) in THUnit))
+htSubst (Lam q' tyL t1) i g a dg q di du u hlen (THLam bodyD) hu =
+  let (dgr ** (hadd, hht)) =
+        htSubst t1 (TSnoc i tyL) g a dg q (USnoc di q') du u (cong S hlen) bodyD hu
+  in (dgr ** (hadd, THLam hht))
+htSubst (App t1 t2) i g a dg q di du u hlen (THApp d1 d2 q' h1 h2 prf) hu = ?htSubst_app
+htSubst (With t1 t2) i g a dg q di du u hlen (THWith h1 h2) hu =
+  let (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg q di du u hlen h1 hu
+      (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg q di du u hlen h2 hu
+  in (dgr1 ** (hr1, THWith hht1 (rewrite justInj' (trans (sym hr1) hr2) in hht2)))
+htSubst (Fst t1) i g a dg q di du u hlen (THFst h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THFst hht))
+htSubst (Snd t1) i g a dg q di du u hlen (THSnd h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THSnd hht))
+htSubst (Tensor t1 t2) i g a dg q di du u hlen (THTensor d1 d2 h1 h2 prf) hu = ?htSubst_tensor
+htSubst (LetPair t1 t2) i g a dg q di du u hlen (THLetPair d1 d2 aa bb h1 hb prf) hu = ?htSubst_letpair
+htSubst (Inl b0 t1) i g a dg q di du u hlen (THInl h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THInl hht))
+htSubst (Inr a0 t1) i g a dg q di du u hlen (THInr h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THInr hht))
+htSubst (Case t1 tL tR) i g a dg q di du u hlen (THCase d1 d2 aa bb h hL hR prf) hu = ?htSubst_case
+htSubst (Let q' t1 t2) i g a dg q di du u hlen (THLet d1 d2 _ aa h1 h2 prf) hu = ?htSubst_let
+htSubst (MkEcho m aE bE t1) i g a dg q di du u hlen (THEcho h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THEcho hht))
+htSubst (Weaken t1) i g a dg q di du u hlen (THWeaken h) hu =
+  let (dgr ** (hr, hht)) = htSubst t1 i g a dg q di du u hlen h hu
+  in (dgr ** (hr, THWeaken hht))