diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc new file mode 100644 index 0000000..8b4d6a4 --- /dev/null +++ b/AFFIRMATION.adoc @@ -0,0 +1,87 @@ +// SPDX-License-Identifier: MPL-2.0 +// Owner: Jonathan D.A. Jewell +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += 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) +| 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) +|=== diff --git a/docs/STATUS.adoc b/docs/STATUS.adoc new file mode 100644 index 0000000..07f358d --- /dev/null +++ b/docs/STATUS.adoc @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: MPL-2.0 +// Owner: Jonathan D.A. Jewell +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += 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). diff --git a/docs/handoff/NEXT-SESSION.md b/docs/handoff/NEXT-SESSION.md new file mode 100644 index 0000000..79ebc88 --- /dev/null +++ b/docs/handoff/NEXT-SESSION.md @@ -0,0 +1,73 @@ + + + + +# 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). diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index 944239c..c684860 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -689,15 +689,15 @@ 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 => @@ -705,7 +705,7 @@ hvSubst TEmpty g a dg q UEmpty Z b du u hlen hv hu = 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,12 +730,12 @@ 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, @@ -743,3 +743,66 @@ hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) (S n0) b du u hlen hv hu = 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))