From c641e267241dd43949985dc0af1697a66f77b25a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:49:21 +0000 Subject: [PATCH 1/4] =?UTF-8?q?proof(solo-core/idris):=20htSubst=20COMPLET?= =?UTF-8?q?E=20=E2=80=94=20all=205=20usage-splitting=20cases=20(toward=20#?= =?UTF-8?q?108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The QTT substitution lemma htSubst is now fully proved (all 15 cases, total, hole-free) on the Idris track, mirroring Coq ht_subst. The 5 usage-splitting cases land via the accounting algebra: - Tensor / LetPair / Case : usplit3 (USnoc-boundary split) x2 -> uaddSplitBoundary2 -> recurse -> substReassocMult -> uaddUappend - App / Let : the q-scaled variants via substReassocAdd + uscaleUappend (Let also needs uaddComm/qAddComm for the d1-scaled shape) - binder cases (LetPair/Case/Let) recurse with the prefix I extended and the body usage reshaped (USnoc..); Case unifies the two branch residuals (justInj' on the shared d2 split). Build green 8/8; the ONLY remaining hole in the whole solo-core is ?todo_preservation. Next: substLemma0 + subst2Lemma (corollaries) then the Step-induction closes preservation. --- .../idris/solo-core/Substitution.idr | 86 +++++++++++++++++-- 1 file changed, 81 insertions(+), 5 deletions(-) diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index c684860..b4b738a 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -779,7 +779,22 @@ 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 (App t1 t2) i g a dg q di du u hlen (THApp d1 d2 q' h1 h2 prf) hu = + let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i)) + (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t2 h2) (tappendLen (TSnoc g a) i)) + (hGadd, hqeq, hIadd) = + uaddSplitBoundary2 dg1 q1 di1 (uscale q' dg2) (qMul q' q2) (uscale q' di2) dg q di + (trans l1 (sym (trans (uscaleLen q' di2) l2))) (trans hlen (sym l1)) + (rewrite sym (uscaleUappend q' (USnoc dg2 q2) di2) in prf) + (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu + (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg2 q2 di2 du u l2 h2 hu + (dgr ** (hDgr, hcomb)) = substReassocAdd dg1 dgr1 dg2 dgr2 dg du q' q1 q2 hr1 hr2 hGadd + in (dgr ** (rewrite hqeq in hDgr, + THApp (uappend dgr1 di1) (uappend dgr2 di2) q' hht1 hht2 + (rewrite uscaleUappend q' dgr2 di2 in + uaddUappend di1 (uscale q' di2) di dgr1 (uscale q' dgr2) dgr hIadd hcomb))) 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 @@ -790,16 +805,77 @@ htSubst (Fst t1) i g a dg q di du u hlen (THFst h) hu = 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 (Tensor t1 t2) i g a dg q di du u hlen (THTensor d1 d2 h1 h2 prf) hu = + let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i)) + (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t2 h2) (tappendLen (TSnoc g a) i)) + (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di + (trans l1 (sym l2)) (trans hlen (sym l1)) prf + (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu + (dgr2 ** (hr2, hht2)) = htSubst t2 i g a dg2 q2 di2 du u l2 h2 hu + (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd + in (dgr ** (rewrite hqeq in hDgr, + THTensor (uappend dgr1 di1) (uappend dgr2 di2) hht1 hht2 + (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb))) +htSubst (LetPair t1 t2) i g a dg q di du u hlen (THLetPair d1 d2 aa bb h1 hb prf) hu = + let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i)) + (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i) + (trans (predEq' (predEq' + (shapeType (TSnoc (TSnoc (tappend (TSnoc g a) i) aa) bb) t2 hb))) + (tappendLen (TSnoc g a) i)) + (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di + (trans l1 (sym l2)) (trans hlen (sym l1)) prf + (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu + (dgr2 ** (hr2, hht2)) = htSubst t2 (TSnoc (TSnoc i aa) bb) g a dg2 q2 + (USnoc (USnoc di2 One) One) du u (cong S (cong S l2)) hb hu + (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd + in (dgr ** (rewrite hqeq in hDgr, + THLetPair (uappend dgr1 di1) (uappend dgr2 di2) aa bb hht1 hht2 + (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb))) 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 (Case t1 tL tR) i g a dg q di du u hlen (THCase d1 d2 aa bb h hL hR prf) hu = + let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t1 h) (tappendLen (TSnoc g a) i)) + (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i) + (trans (predEq' (shapeType (TSnoc (tappend (TSnoc g a) i) aa) tL hL)) + (tappendLen (TSnoc g a) i)) + (hGadd, hqeq, hIadd) = uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di + (trans l1 (sym l2)) (trans hlen (sym l1)) prf + (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h hu + (dgr2 ** (hr2, hhtL)) = htSubst tL (TSnoc i aa) g a dg2 q2 (USnoc di2 One) du u (cong S l2) hL hu + (dgr2' ** (hr2', hhtR)) = htSubst tR (TSnoc i bb) g a dg2 q2 (USnoc di2 One) du u (cong S l2) hR hu + (dgr ** (hDgr, hcomb)) = substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 hr1 hr2 hGadd + in (dgr ** (rewrite hqeq in hDgr, + THCase (uappend dgr1 di1) (uappend dgr2 di2) aa bb hht1 hhtL + (rewrite justInj' (trans (sym hr2) hr2') in hhtR) + (uaddUappend di1 di2 di dgr1 dgr2 dgr hIadd hcomb))) +htSubst (Let q' t1 t2) i g a dg q di du u hlen (THLet d1 d2 _ aa h1 h2 prf) hu = + let (dg1 ** q1 ** di1 ** (Refl, l1)) = usplit3 d1 (tlen g) (tlen i) + (trans (shapeType (tappend (TSnoc g a) i) t1 h1) (tappendLen (TSnoc g a) i)) + (dg2 ** q2 ** di2 ** (Refl, l2)) = usplit3 d2 (tlen g) (tlen i) + (trans (predEq' (shapeType (TSnoc (tappend (TSnoc g a) i) aa) t2 h2)) + (tappendLen (TSnoc g a) i)) + (hGadd, hqeq, hIadd) = + uaddSplitBoundary2 (uscale q' dg1) (qMul q' q1) (uscale q' di1) dg2 q2 di2 dg q di + (trans (uscaleLen q' di1) (trans l1 (sym l2))) + (trans hlen (sym (trans (uscaleLen q' di1) l1))) + (rewrite sym (uscaleUappend q' (USnoc dg1 q1) di1) in prf) + (dgr1 ** (hr1, hht1)) = htSubst t1 i g a dg1 q1 di1 du u l1 h1 hu + (dgr2 ** (hr2, hht2)) = htSubst t2 (TSnoc i aa) g a dg2 q2 (USnoc di2 q') du u (cong S l2) h2 hu + (dgr ** (hDgr, hcomb)) = substReassocAdd dg2 dgr2 dg1 dgr1 dg du q' q2 q1 hr2 hr1 + (trans (uaddComm dg2 (uscale q' dg1)) hGadd) + in (dgr ** (rewrite hqeq in rewrite qAddComm (qMul q' q1) q2 in hDgr, + THLet (uappend dgr1 di1) (uappend dgr2 di2) q' aa hht1 hht2 + (rewrite uscaleUappend q' dgr1 di1 in + uaddUappend (uscale q' di1) di2 di (uscale q' dgr1) dgr2 dgr hIadd + (trans (uaddComm (uscale q' dgr1) dgr2) hcomb)))) 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)) From 9c574690e2df7abdbb93072cf0b97ab07ef7a7a2 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:54:20 +0000 Subject: [PATCH 2/4] =?UTF-8?q?proof(solo-core/idris):=20substLemma0=20?= =?UTF-8?q?=E2=80=94=20subst0=20corollary=20of=20htSubst=20(toward=20#108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit substLemma0 = htSubst at the empty prefix (I = TEmpty): substitute the single top-of-context variable once, the workhorse the reduction rules S_App / S_CaseL / S_CaseR / S_Let consume. One-liner over the now-complete htSubst; build green. Layer 4c (the QTT substitution lemma) is now: htSubst COMPLETE (15/15) + substLemma0. Remaining for preservation (4d): uaddAssoc -> subst2Lemma (the two-variable LetPair substitution), then the Step-induction. --- .../verification/idris/solo-core/Substitution.idr | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index b4b738a..a41b392 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -882,3 +882,18 @@ htSubst (MkEcho m aE bE t1) i g a dg q di du u hlen (THEcho h) hu = 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)) + +------------------------------------------------------------ +-- 4c (cont). Operational corollaries of htSubst +------------------------------------------------------------ + +||| `subst0` corollary — `htSubst` at the empty prefix `I = TEmpty`: substitute +||| the single top-of-context variable once. (Mirrors Coq `subst_lemma0`.) +||| The reduction rules `S_App` / `S_CaseL` / `S_CaseR` / `S_Let` consume this. +public export +substLemma0 : (g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (t : Tm) + -> (du : Uvec) -> (u : Tm) + -> Has (TSnoc g a) (USnoc dg q) t b + -> Has g du u a + -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr, Has g dgr (subst0 u t) b)) +substLemma0 g a dg q t du u ht hu = htSubst t TEmpty g a dg q UEmpty du u Refl ht hu From 25a4f8b8915754efa0ecb47aff0d23b5b319ee93 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 20 Jun 2026 13:55:05 +0000 Subject: [PATCH 3/4] =?UTF-8?q?docs(proofs):=20update=20STATUS=20registry?= =?UTF-8?q?=20=E2=80=94=20htSubst=20complete=20+=20substLemma0=20(Idris=20?= =?UTF-8?q?#108)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Idris preservation row: foundation -> htSubst COMPLETE (15/15, b-erasure resolved) + substLemma0; only ?todo_preservation remains; subst2Lemma (via uaddAssoc) + the Step-induction are the documented remainder. --- proofs/STATUS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/STATUS.md b/proofs/STATUS.md index c3687f7..f434066 100644 --- a/proofs/STATUS.md +++ b/proofs/STATUS.md @@ -61,7 +61,7 @@ Last verified: 2026-06-14. | `progress` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free. Phase F1.3. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed. | | `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. **Re-proven over the SEPARATED context (`Tctx`/`Uvec`) + both products (`TWith`/`TTensor`, `LetPair`) in the 2026-06-15 F1.4 design migration** — closed-term inversions now massage only the usage vector (`uaddEmpty`/`uscaleEmpty`), since the shared type context stays `TEmpty` automatically; `:total progress` confirms totality. | | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). | -| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Foundation landed (2026-06-15): `Substitution.idr` (in the ipkg, hole-free) carries the append-context algebra (`tappend`/`uappend` + injectivity/split/boundary lemmas) and the shape invariant (`shapeVar`/`shapeType`), all `idris2 --build`-checked. The shift/subst/preservation layers thread `g`/`t` RELEVANTLY around Idris's index erasure (ADR-003) — heavier than the Coq original; PENDING.** | +| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Progress (2026-06-19): `Substitution.idr` (in the ipkg) now carries the append-context algebra, the shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift` (term weakening, all 14 cases), the substitution accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`), `hvSubst`, the FULL `htSubst` (the QTT substitution lemma — all 15 cases, total, hole-free), and `substLemma0` (the `subst0` corollary). The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` as an erased implicit in `hvSubst`/`htSubst`. `idris2 --build` exits 0; the ONLY remaining hole in the whole solo-core is `?todo_preservation`. REMAINING for `preservation`: `uaddAssoc` -> `subst2Lemma` (two-variable LetPair substitution) -> the `Step`-induction. PENDING (still NOT proved).** | | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. | | Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. | | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. | From ad50fb1a8ea7f8cbd2bd1cb2f832ea3a94236b7a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 02:25:26 +0000 Subject: [PATCH 4/4] =?UTF-8?q?proof(solo-core/idris):=20close=20preservat?= =?UTF-8?q?ion=20(#108)=20=E2=80=94=20total,=20hole-free?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Discharge the Idris twin's `preservation` (Phase F1.4), the last open normative MUST. The solo core is now hole-free on BOTH proof tracks. Substitution.idr: - add `uaddAssoc` (associativity of the partial `uadd`, existential form) and `subst2Lemma` (two-variable LetPair substitution), completing the substitution-lemma chain over the existing `htSubst` / `substLemma0`; - add a local `coeUsage` (retype along a usage equality) and export `justInj'`; - invert the module dependency: drop the unused `import Soundness` so Soundness can import Substitution (no cycle). Soundness.idr: - import Substitution; replace `?todo_preservation` with the full proof by induction on `Step`, mirroring the Coq twin `preservation`. The reduction cases consume `substLemma0` (App/Case/Let) and `subst2Lemma` (LetPair); the residual usage is realigned to `d` via uadd commutativity/associativity and `uscale One`; congruence cases recurse structurally; - take the reduct term explicitly (relevant), exactly as `progress` does, so the substitution lemmas receive the bound body + substituted value under Idris index erasure; `affinePreservation` follows as the corollary. Verified in-environment: - `idris2 --build solo-core.ipkg` exits 0 (8/8 modules); - `:total` confirms preservation, affinePreservation, subst2Lemma, uaddAssoc, substLemma0 are all total; no holes / postulates / believe_me / assert_total; - Coq twin re-compiled fresh and `Print Assumptions preservation` / `affine_pres` both report "Closed under the global context" (axiom-free). Docs: proofs/STATUS.md (Idris `preservation` -> locally-checked, solo core hole-free), docs/STATUS.adoc (MUST met), AFFIRMATION.adoc (revision 2), docs/handoff/NEXT-SESSION.md (redirected to the compilation axis); stale "hole" comments in both modules refreshed. Co-Authored-By: Claude Opus 4.8 (1M context) Claude-Session: https://claude.ai/code/session_01BwV2DWsjkBiNP3oscimMLV --- AFFIRMATION.adoc | 46 +++--- docs/STATUS.adoc | 16 +- docs/handoff/NEXT-SESSION.md | 69 +++++---- proofs/STATUS.md | 4 +- .../idris/solo-core/Soundness.idr | 118 +++++++++++--- .../idris/solo-core/Substitution.idr | 144 +++++++++++++++--- 6 files changed, 285 insertions(+), 112 deletions(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 8b4d6a4..8909ecc 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -4,8 +4,8 @@ = Affirmation :toc: preamble :sectnums: -:revdate: 2026-06-19T21:35:54Z -:revnumber: 1 +:revdate: 2026-06-21T02:22:08Z +:revnumber: 2 This AFFIRMATION records the standing of *my-lang* against the hyperpolymath standards and this project's own honesty discipline, at the timestamp below. @@ -29,12 +29,17 @@ Rust compiler. The normative obligation — the *must* — is that the language 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. +. *Soundness is mechanised, not asserted — now on BOTH tracks.* 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. The *Idris2 twin* + now also proves both `progress` and `preservation` (#108, discharged + 2026-06-21): total, hole-free functions under `%default total` with no + postulates — `:total preservation` confirms — via the QTT substitution + lemmas `htSubst` / `substLemma0` / `subst2Lemma` (with `uaddAssoc`). The + solo core is hole-free on both tracks. . *No overclaim.* Every proof hole is recorded as an obligation, never as a result (`proofs/STATUS.md` is authoritative and wins over any prose). @@ -56,20 +61,23 @@ To the verified state of this repository, I affirm: * 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. +* Idris2: `idris2 --build solo-core.ipkg` exits 0 under `%default total`, + no postulates / `believe_me` / `assert_total`; the solo core is HOLE-FREE + (`preservation`, `affinePreservation`, `htSubst`, `substLemma0`, + `subst2Lemma`, `uaddAssoc` all `:total`). * 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. +The normative *must* (a mechanised-sound core, coupled into the compiler) is +met on both proof tracks. What remains is *intends* and *wishes* +(`docs/STATUS.adoc`), affirmed as NOT done: making the QTT axis the *default* +in `checker.rs`; surface quantity syntax for real per-binder linearity; the +`wasm32` and `RISC-V` backend legs; the typed-wasm WasmGC verified leg +(blocked on `typed-wasm` / AffineScript / Ephapax being added to the session); +and Android / iOS via Tauri / Dioxus. The non-Solo dialect compilers (Duet / +Ensemble) are scaffold only. == Affirmation @@ -81,7 +89,7 @@ herein is described as proved that a proof assistant does not accept today. |=== | 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) +| Timestamp (UTC) | 2026-06-21T02:22:08Z +| Verified basis | `claude/dreamy-hypatia-O8XHo` (Idris `preservation` #108 discharged, solo core hole-free) atop `main` @ `a7765e7` (PR #116 `my-qtt`, PR #117 coupling step 2) | 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 index 07f358d..798c10e 100644 --- a/docs/STATUS.adoc +++ b/docs/STATUS.adoc @@ -18,11 +18,10 @@ 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`. +my-lang's normative must is met — the Coq metatheory is complete and +axiom-free, the verified usage-checker is merged into the Rust toolchain, and +the Idris twin's `preservation` (#108) is now DISCHARGED (total, hole-free; +`:total preservation`). The solo core is hole-free on both tracks. == MUST — my-lang itself (sound core, verified-coupled, compiling) @@ -38,7 +37,7 @@ locally at `acd29d6`. | 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` +| **Idris twin `preservation` (#108)** — full `htSubst` + `subst2Lemma` + `uaddAssoc`, `Step`-induction, total + hole-free | `[x]` | `claude/dreamy-hypatia-O8XHo` |=== == INTEND — planned next @@ -46,7 +45,6 @@ locally at `acd29d6`. [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 @@ -67,6 +65,6 @@ locally at `acd29d6`. == 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. +* Idris: `idris2 --build solo-core.ipkg` exits 0, `%default total`, no postulates / `believe_me` / `assert_total`; the solo core is HOLE-FREE (`preservation`, `affinePreservation`, `subst2Lemma`, `uaddAssoc`, `substLemma0`, `htSubst` all `:total`). * 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). +* Landed this programme increment: PR #116 (`my-qtt`), PR #117 (coupling step 2); `preservation` #108 discharged (this increment). diff --git a/docs/handoff/NEXT-SESSION.md b/docs/handoff/NEXT-SESSION.md index 79ebc88..58b03e0 100644 --- a/docs/handoff/NEXT-SESSION.md +++ b/docs/handoff/NEXT-SESSION.md @@ -10,38 +10,40 @@ 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 one open MUST is now CLOSED: 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): +The Coq metatheory is complete and axiom-free, and **the Idris twin's +`preservation` is now DISCHARGED** (2026-06-21): a total, hole-free function +by induction on `Step` in `proofs/verification/idris/solo-core/Soundness.idr`, +`:total preservation` confirmed, `%default total`, no postulates. The whole +solo core is HOLE-FREE on both tracks. `htSubst` (all 15 cases), `substLemma0`, +`subst2Lemma`, and `uaddAssoc` all land in `Substitution.idr` (the module +dependency was inverted: `Soundness` now imports `Substitution`). -- **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`. +### Where the normative work goes next (the compilation axis) +The sound core is done and coupled. The open items are *intends*/*wishes* in +`docs/STATUS.adoc`: +1. Make the QTT resource axis the **default** in `crates/my-lang/src/checker.rs` + (the bridge is opt-in today via `qtt_bridge::check_expr`). +2. Add surface **quantity syntax** so the bridge enforces real per-binder + linearity (`Param` has no quantity field; the bridge defaults to `One`). +3. **wasm32** via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`), + then **RISC-V** (`riscv64gc-unknown-linux-gnu`), then the **typed-wasm** + WasmGC verified leg (blocked until `typed-wasm` / AffineScript / Ephapax are + added to the working session). ### Load-bearing context (do NOT relitigate) +- **`preservation` takes the reduct term `t` explicitly** (relevant), exactly + as `progress` does. Idris erases the derivation's term/type indices, but the + substitution lemmas compute on the bound body + substituted value, so those + must come from a matched (relevant) term; `{g}`/`{d}` are relevant for the + same reason. `subst2Lemma`'s result type `c` is an erased implicit. +- **Per-clause pattern variables that unify** (the Lam/arrow quantity, the + Inl/Inr annotation vs the sum's summand, the Let quantity) must share ONE + name in the LHS — Idris rejects two names that provably unify. +- **`let`-block rule**: don't mix type-annotated bindings with dependent-pair + pattern bindings in one block (parse error). Use single-binding nested + `let … in let …`, or inline. - **`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 @@ -51,11 +53,12 @@ substitution lemma `htSubst`, which is now **structurally landed** (commit - **`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. +- Toolchain: if 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` + (exit 0), and check totality with `:total ` in the REPL. Discipline: + every edit ends with a compile; `%default total`; no postulates; pin + headline theorems where the repo convention does. ## The other axis: fundamentals -> compilation (see docs/STATUS.adoc) diff --git a/proofs/STATUS.md b/proofs/STATUS.md index f434066..20404d9 100644 --- a/proofs/STATUS.md +++ b/proofs/STATUS.md @@ -61,7 +61,7 @@ Last verified: 2026-06-14. | `progress` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free. Phase F1.3. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed. | | `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. **Re-proven over the SEPARATED context (`Tctx`/`Uvec`) + both products (`TWith`/`TTensor`, `LetPair`) in the 2026-06-15 F1.4 design migration** — closed-term inversions now massage only the usage vector (`uaddEmpty`/`uscaleEmpty`), since the shared type context stays `TEmpty` automatically; `:total progress` confirms totality. | | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). | -| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Progress (2026-06-19): `Substitution.idr` (in the ipkg) now carries the append-context algebra, the shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift` (term weakening, all 14 cases), the substitution accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`), `hvSubst`, the FULL `htSubst` (the QTT substitution lemma — all 15 cases, total, hole-free), and `substLemma0` (the `subst0` corollary). The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` as an erased implicit in `hvSubst`/`htSubst`. `idris2 --build` exits 0; the ONLY remaining hole in the whole solo-core is `?todo_preservation`. REMAINING for `preservation`: `uaddAssoc` -> `subst2Lemma` (two-variable LetPair substitution) -> the `Step`-induction. PENDING (still NOT proved).** | +| `preservation` | Idris2 `solo-core/Soundness` | **locally-checked** | **DISCHARGED 2026-06-21 (#108).** `preservation : (t : Tm) -> Has g d t a -> Step t t' -> Has g d t' a` is a total, hole-free function by induction on `Step` — `:total preservation` confirms; `%default total`, no `postulate`/`believe_me`/`assert_total`/`?hole`. Mirrors the Coq twin `preservation`: the β/projection/elimination cases consume the QTT substitution lemmas from `Substitution.idr` — `substLemma0` (App/Case/Let single-variable) and `subst2Lemma` (LetPair two-variable) — realigning the residual usage with `d` via `uadd` commutativity/associativity (`uaddAssoc`) and `uscale One`; congruence cases recurse structurally. Stated over the CORRECT design (separated context + genuine products) that made the same-usage statement sound (issue #93). The reduct term `t` is taken explicitly (relevant), exactly as `progress` does, because Idris erases the derivation's term/type indices while the substitution lemmas compute on the bound body + substituted value. `affinePreservation` follows as the Solo-kernel corollary (`:total` too). Supporting chain in `Substitution.idr` (all total, hole-free): append-context algebra, shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift`, the accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`/`uaddAssoc`), `hvSubst`, the FULL `htSubst` (all 15 cases), `substLemma0`, `subst2Lemma`. The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` erased. `idris2 --build solo-core.ipkg` exits 0; **the solo core is now HOLE-FREE**. CI: `proofs.yml` Idris job. | | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. | | Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. | | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. | @@ -86,7 +86,7 @@ Last verified: 2026-06-14. | Topic AS has | my-lang status | Plan phase | |--------------|----------------|-----------| | Mechanised QTT solo-core | **commenced** (this PR) | F1 | -| Mechanised progress/preservation | Coq **machine-checked** (axiom-free `Qed`, CI-guarded); Idris twin pending | F1.3 / F1.4 | +| Mechanised progress/preservation | Coq **machine-checked** (axiom-free `Qed`, CI-guarded); Idris twin **locally-checked** (both total + hole-free; `preservation` #108 discharged 2026-06-21) | F1.3 / F1.4 | | Algorithmic typing / decidable typecheck (static-split ≡ usage-walk) | Coq **machine-checked** (`check_correct`, axiom-free) — **overtakes AS** (states it as prose "future work" only) | F1.4 | | Surface→core elaboration correctness (`me` → `solo`) | Coq **machine-checked** (`me_wt_sound` over the WHOLE `me_tm` + `elab_data_check`, axiom-free, M1.1/M1.1b — M1 complete) — **overtakes AS** (solo-only; no `me`-like dialect, nothing analogous as surveyed (AS@main 2026-06-02)) | M1 | | Quantitative-types (dedicated doc) | folded into solo affine doc | F4 | diff --git a/proofs/verification/idris/solo-core/Soundness.idr b/proofs/verification/idris/solo-core/Soundness.idr index c2e0099..5969598 100644 --- a/proofs/verification/idris/solo-core/Soundness.idr +++ b/proofs/verification/idris/solo-core/Soundness.idr @@ -23,19 +23,18 @@ import EchoMode import Syntax import Context import Typing +import Substitution %default total --- NOTE (F1.4 staging): this module re-proves `progress` over the --- separated context + two products, and STATES `preservation` over the --- correct same-usage statement. The proof of `preservation` (the QTT --- substitution lemma) lands in the companion module Substitution.idr --- and is wired in here once discharged — until then `preservation` is a --- typed hole `?todo_preservation` and is NEVER described as proved --- (proofs/STATUS.md vocabulary). Phases 1-3 (this file) are the --- prerequisite: the OLD design (split-intro Pair + project-elim Fst/Snd) --- made the same-usage preservation literally UNSOUND, so the hole could --- not be honestly filled before this migration. +-- NOTE (F1.4): this module re-proves `progress` over the separated context +-- + two products, and PROVES `preservation` over the correct same-usage +-- statement (DISCHARGED 2026-06-21, #108). The QTT substitution lemmas it +-- consumes live in the companion module Substitution.idr (`substLemma0`, +-- `subst2Lemma`); the proof is by induction on `Step`, total and hole-free +-- (`:total preservation`). The OLD design (split-intro Pair + project-elim +-- Fst/Snd) made the same-usage preservation literally UNSOUND (issue #93), +-- so this could not be honestly filled before the 2026-06-15 migration. ------------------------------------------------------------ -- Values @@ -299,23 +298,94 @@ progress (Weaken t) (THWeaken d) = ||| affine-accounting content of the theorem — a reduct that duplicated a ||| linear variable would require a *larger* usage. ||| -||| OUTSTANDING (Phase F1.4): the proof needs a QTT substitution lemma -||| that respects usage splitting (the App/Let/Case computation cases -||| substitute a value for the bound variable; the LetPair case -||| substitutes two). Lands in Substitution.idr; wired in here once -||| discharged. Left as a typed hole; tracked in proofs/STATUS.md and -||| GitHub #108. NOT described as proved. +||| DISCHARGED (Phase F1.4) by induction on `Step` (mirrors the Coq twin +||| `preservation` in SoloCore.v). The β/projection/elimination cases +||| consume the QTT substitution lemmas from `Substitution.idr`: +||| `substLemma0` for the single-variable reductions (App/Case/Let), and +||| `subst2Lemma` for the two-variable `LetPair` reduction; each realigns +||| the residual usage with the original `d` via the `uadd` accounting +||| (commutativity / associativity / `uscale One`). The congruence cases +||| recurse structurally on the sub-step and rebuild the derivation. ||| -||| Stated over the CORRECT design now (separated context + genuine -||| products): with the old split-intro/project-elim `Pair`, this -||| same-usage statement was unsound (issue #93); the migration in this -||| file is what makes it provable. +||| Stated over the CORRECT design (separated context + genuine products): +||| with the old split-intro/project-elim `Pair`, this same-usage statement +||| was unsound (issue #93); the migration in this file is what makes it +||| provable. +||| +||| The reduct term `t` is taken EXPLICITLY (relevant), exactly as +||| `progress` does: Idris erases the derivation's term/type indices, so the +||| substitution lemmas — which compute on the bound variable's body and the +||| substituted value — need those sub-terms supplied relevantly from the +||| matched term; `g`/`d` are relevant for the same reason. This is a +||| presentation choice; the logical statement is the Coq twin's. public export -preservation : Has g d t a -> Step t t' -> Has g d t' a -preservation _ _ = ?todo_preservation +preservation : {g : Tctx} -> {d : Uvec} -> (t : Tm) + -> Has g d t a -> Step t t' -> Has g d t' a +preservation (App (Lam q' a0 tb) v) (THApp d1 d2 q' (THLam hb) h2 prf) (SApp vval) = + let (dgr ** (hadd, hht)) = substLemma0 g a0 d1 q' tb d2 v hb h2 + in coeUsage (justInj' (trans (sym hadd) prf)) hht +-- additive projections fire on a With value +preservation (Fst (With v1 v2)) (THFst (THWith h1 h2)) (SFst v1v v2v) = h1 +preservation (Snd (With v1 v2)) (THSnd (THWith h1 h2)) (SSnd v1v v2v) = h2 +-- sum elimination: substitute the injected value into the taken branch +preservation (Case (Inl bb v) tL tR) (THCase d1 d2 aa bb (THInl hv) hL hR prf) + (SCaseL vval) = + let (dgr ** (hadd, hht)) = substLemma0 g aa d2 One tL d1 v hL hv + in coeUsage + (justInj' (trans (sym (trans (uaddComm d1 d2) + (trans (sym (cong (uadd d2) (uscaleOne d1))) hadd))) prf)) + hht +preservation (Case (Inr aa v) tL tR) (THCase d1 d2 aa bb (THInr hv) hL hR prf) + (SCaseR vval) = + let (dgr ** (hadd, hht)) = substLemma0 g bb d2 One tR d1 v hR hv + in coeUsage + (justInj' (trans (sym (trans (uaddComm d1 d2) + (trans (sym (cong (uadd d2) (uscaleOne d1))) hadd))) prf)) + hht +-- let binding: substitute the bound value +preservation (Let q1 v t2) (THLet d1 d2 q1 aa h1 h2 prf) (SLet vval) = + let (dgr ** (hadd, hht)) = substLemma0 g aa d2 q1 t2 d1 v h2 h1 + in coeUsage + (justInj' (trans (sym (trans (uaddComm (uscale q1 d1) d2) hadd)) prf)) + hht +-- multiplicative let-pair: two-variable substitution of the tensor components +preservation (LetPair (Tensor v1 v2) body) + (THLetPair d1 d2 aa bb (THTensor dv1 dv2 hv1 hv2 prft) hb prf) + (SLetPair v1v v2v) = + subst2Lemma g aa bb d d1 d2 dv1 dv2 body v1 v2 hb hv1 hv2 prft prf +-- congruence: thread the sub-step and rebuild +preservation (App t1 t2) (THApp d1 d2 q h1 h2 prf) (SApp1 s1) = + THApp d1 d2 q (preservation t1 h1 s1) h2 prf +preservation (App v1 t2) (THApp d1 d2 q h1 h2 prf) (SApp2 v1v s2) = + THApp d1 d2 q h1 (preservation t2 h2 s2) prf +preservation (With t1 t2) (THWith h1 h2) (SWith1 s1) = + THWith (preservation t1 h1 s1) h2 +preservation (With v1 t2) (THWith h1 h2) (SWith2 v1v s2) = + THWith h1 (preservation t2 h2 s2) +preservation (Fst tt) (THFst h) (SFst1 s) = THFst (preservation tt h s) +preservation (Snd tt) (THSnd h) (SSnd1 s) = THSnd (preservation tt h s) +preservation (Tensor t1 t2) (THTensor d1 d2 h1 h2 prf) (STensor1 s1) = + THTensor d1 d2 (preservation t1 h1 s1) h2 prf +preservation (Tensor v1 t2) (THTensor d1 d2 h1 h2 prf) (STensor2 v1v s2) = + THTensor d1 d2 h1 (preservation t2 h2 s2) prf +preservation (LetPair t1 t2) (THLetPair d1 d2 aa bb h1 hb prf) (SLetPair1 s1) = + THLetPair d1 d2 aa bb (preservation t1 h1 s1) hb prf +preservation (Inl b0 tt) (THInl h) (SInl1 s) = THInl (preservation tt h s) +preservation (Inr a0 tt) (THInr h) (SInr1 s) = THInr (preservation tt h s) +preservation (Case tc tL tR) (THCase d1 d2 aa bb h hL hR prf) (SCase1 s) = + THCase d1 d2 aa bb (preservation tc h s) hL hR prf +preservation (Let q1 t1 t2) (THLet d1 d2 q1 aa h1 h2 prf) (SLet1 s1) = + THLet d1 d2 q1 aa (preservation t1 h1 s1) h2 prf +preservation (MkEcho m a0 b0 tt) (THEcho h) (SEcho1 s) = THEcho (preservation tt h s) +preservation (Weaken tt) (THWeaken h) (SWeaken1 s) = THWeaken (preservation tt h s) +-- echo weaken: a Linear echo value weakens to an Affine one +preservation (Weaken (MkEcho Linear a0 b0 v)) (THWeaken h) (SWeaken vval) = + case h of + THEcho hv => THEcho hv ||| Affine preservation: a direct corollary of `preservation` for the ||| Solo kernel (the preserved usage already carries the accounting). public export -affinePreservation : Has g d t a -> Step t t' -> Has g d t' a -affinePreservation = preservation +affinePreservation : {g : Tctx} -> {d : Uvec} -> (t : Tm) + -> Has g d t a -> Step t t' -> Has g d t' a +affinePreservation t = preservation t diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index a41b392..6c43191 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -1,33 +1,34 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- --- The QTT substitution lemma + preservation for the my-lang Solo core --- (Idris2 twin of the F1.4 section of SoloCore.v). Phase F1.4, Idris track. +-- The QTT substitution lemmas for the my-lang Solo core (Idris2 twin of the +-- F1.4 section of SoloCore.v). Phase F1.4, Idris track. -- --- This is the proof of `preservation` (Soundness.idr states it as the hole --- `?todo_preservation`). It rests on the standard open-context substitution --- lemma `htSubst`: substitution under binders shifts the substituted --- variable's index, so the lemma is generalised over a type-context prefix --- `I` (the binders crossed so far). The reduction rules only ever do --- `subst0` (one variable) and `subst2` (two), but the under-binder induction --- needs the general form. +-- These lemmas are what `Soundness.preservation` consumes (preservation +-- itself lives in Soundness.idr, which imports this module). The core is the +-- open-context substitution lemma `htSubst`: substitution under binders +-- shifts the substituted variable's index, so the lemma is generalised over +-- a type-context prefix `I` (the binders crossed so far). The reduction rules +-- only ever do `subst0` (one variable) and `subst2` (two), but the +-- under-binder induction needs the general form. -- --- Layers (mirroring the Coq twin): --- 4a append-context algebra (tappend/uappend + injectivity/split) [VERIFIED] --- 4b shape + shift (shapeType/hvShift/htShift [VERIFIED]; --- htShift0/weakeningAppend — PENDING) --- 4c substitution core (reassoc algebra, hvSubst, htSubst, --- substLemma0, subst2Lemma — PENDING) --- 4d preservation (consumes 4c; congruences recurse on Step --- — PENDING; Soundness.preservation stays --- the honest hole until 4d lands) +-- Layers (mirroring the Coq twin), all VERIFIED (total, hole-free): +-- 4a append-context algebra (tappend/uappend + injectivity/split) +-- 4b shape + shift (shapeType, hvShift, htShift, htShift0) +-- 4c substitution core (reassoc algebra, uaddAssoc, hvSubst, +-- htSubst [all 15 cases], substLemma0, +-- subst2Lemma) +-- 4d preservation (in Soundness.idr; consumes 4c, recurses +-- on Step — DISCHARGED 2026-06-21, #108) -- --- STATUS (Idris track, #108): HOLE-FREE for the layers it currently contains — --- 4a (append algebra), the shape invariant, `hvShift` (has_var weakening), --- the structural shift index `shiftIdx`/`shiftIdxCorrect`/`shiftVarLemma`, and --- `htShift` (term weakening, all 14 constructor cases, total) on top of its --- support lemmas (`unitInv`, `usplitLemma`, `uaddUshift`, `ushiftUscale`). --- It does NOT yet prove preservation (htSubst/subst2Lemma/preservation pending). +-- STATUS (Idris track, #108): the whole solo core is HOLE-FREE. This module +-- provides the append algebra, the shape invariant, the structural shift +-- index (`shiftIdx`/`shiftIdxCorrect`/`shiftVarLemma`), `htShift` (term +-- weakening, all 14 constructor cases), the accounting algebra +-- (`qReassoc`/`vecReassoc`/`substReassoc*`/`usplit3`/`uaddSplitBoundary2`/ +-- `uaddAssoc`), `hvSubst`, the FULL `htSubst`, `substLemma0`, and +-- `subst2Lemma` — all `%default total`, no postulates. `Soundness.preservation` +-- discharges the soundness obligation on top of them. -- -- ARCHITECTURAL BLOCKER on `htShift` — RESOLVED 2026-06-15 via Option A. -- `htShift` shifts under binders, so its binder cases extend the type context @@ -53,7 +54,6 @@ import EchoMode import Syntax import Context import Typing -import Soundness import Data.Nat %default total @@ -63,6 +63,7 @@ import Data.Nat ------------------------------------------------------------ -- (Context.idr's equivalents are not exported; restate locally.) +public export justInj' : Just x = Just y -> x = y justInj' Refl = Refl @@ -621,6 +622,43 @@ substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 h1 h2 h3 = (rewrite uscaleOne dg2 in h3) in (dgr ** (rewrite sym (qMulOneL q2) in ha, rewrite sym (uscaleOne dgr2) in hb)) +||| Addition is ASSOCIATIVE on the partial operation (mirrors Coq +||| `uadd_assoc`): if `(D1+D2)+D3` is defined, then `D2+D3` is defined and +||| `D1+(D2+D3)` agrees with `(D1+D2)+D3`. The existential reassociation +||| `subst2Lemma` uses to align the two-variable substitution accounting. +||| Structural recursion on the (lock-stepped) first two summands; the +||| heads reassociate via `qAddAssoc`. +public export +uaddAssoc : (d1, d2, d3, d12, d123 : Uvec) + -> uadd d1 d2 = Just d12 + -> uadd d12 d3 = Just d123 + -> (d23 : Uvec ** (uadd d2 d3 = Just d23, uadd d1 d23 = Just d123)) +uaddAssoc UEmpty UEmpty UEmpty d12 d123 h12 h123 = + case justInj' h12 of + Refl => case justInj' h123 of + Refl => (UEmpty ** (Refl, Refl)) +uaddAssoc UEmpty UEmpty (USnoc _ _) d12 d123 h12 h123 = + case justInj' h12 of + Refl => void (nothingNotJust' h123) +uaddAssoc UEmpty (USnoc _ _) d3 d12 d123 h12 h123 = void (nothingNotJust' h12) +uaddAssoc (USnoc _ _) UEmpty d3 d12 d123 h12 h123 = void (nothingNotJust' h12) +uaddAssoc (USnoc d1 q1) (USnoc d2 q2) UEmpty d12 d123 h12 h123 = + let (c12 ** (e12, hd12)) = uaddSnocSplit d1 d2 q1 q2 d12 h12 + in case hd12 of + Refl => void (nothingNotJust' h123) +uaddAssoc (USnoc d1 q1) (USnoc d2 q2) (USnoc d3 q3) d12 d123 h12 h123 = + let (c12 ** (e12, hd12)) = uaddSnocSplit d1 d2 q1 q2 d12 h12 + in case hd12 of + Refl => + let (c123 ** (e123, hd123)) = uaddSnocSplit c12 d3 (qAdd q1 q2) q3 d123 h123 + (c23 ** (e23, e1_23)) = uaddAssoc d1 d2 d3 c12 c123 e12 e123 + in (USnoc c23 (qAdd q2 q3) ** + ( trans (uaddUSnocReduce d2 d3 q2 q3) (cong (combMaybe (qAdd q2 q3)) e23) + , trans (trans (uaddUSnocReduce d1 c23 q1 (qAdd q2 q3)) + (cong (combMaybe (qAdd q1 (qAdd q2 q3))) e1_23)) + (trans (cong (\z => Just (USnoc c123 z)) (sym (qAddAssoc q1 q2 q3))) + (cong Just (sym hd123))) )) + ------------------------------------------------------------ -- 4c (cont). USnoc-headed boundary splitters + var arithmetic ------------------------------------------------------------ @@ -897,3 +935,59 @@ substLemma0 : (g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (t : Tm) -> Has g du u a -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr, Has g dgr (subst0 u t) b)) substLemma0 g a dg q t du u ht hu = htSubst t TEmpty g a dg q UEmpty du u Refl ht hu + +||| Retype a derivation along a usage equality (local; the analogous +||| `Soundness.coeUse` is private to that module). `subst2Lemma` uses it to +||| reshape the residual usages the two nested `substLemma0` calls produce. +public export +coeUsage : d = d' -> Has g d t b -> Has g d' t b +coeUsage Refl x = x + +||| Two-variable substitution lemma (mirrors Coq `subst2_lemma`): the +||| `LetPair` eliminator substitutes BOTH tensor components into the +||| two-binder body `t`. Proven as two nested `substLemma0` applications — +||| first the pre-shifted `u2` under the inner (type-`b`) binder, then `u1` +||| for the (now top) type-`a` binder — with the residual usages realigned +||| via `uaddAssoc` / `uaddComm`. `subst2 u1 u2 t` reduces definitionally to +||| `subst0 u1 (subst0 (shift 0 u2) t)`, exactly what the outer call yields. +||| The `S_LetPair` case of `preservation` consumes this. +public export +subst2Lemma : (g : Tctx) -> (a, b : Ty) -> (d, d1, d2, dv1, dv2 : Uvec) + -> (t, u1, u2 : Tm) -> {0 c : Ty} + -> Has (TSnoc (TSnoc g a) b) (USnoc (USnoc d2 One) One) t c + -> Has g dv1 u1 a + -> Has g dv2 u2 b + -> uadd dv1 dv2 = Just d1 + -> uadd d1 d2 = Just d + -> Has g d (subst2 u1 u2 t) c +subst2Lemma g a b d d1 d2 dv1 dv2 t u1 u2 ht hu1 hu2 hd1 hd = + -- inner substitution: (shift 0 u2) for the index-0, type-`b` binder + let (dr1 ** (hadd1, hht1)) = + substLemma0 (TSnoc g a) b (USnoc d2 One) One t (USnoc dv2 Zero) + (shift 0 u2) ht (htShift0 g a dv2 u2 hu2) in + -- the residual `dr1` reshapes to `USnoc dr1g One`, where `dr1g = D2 + Dv2` + let (dr1g ** hdr1g) = + uaddTotal d2 dv2 + (trans (predEq' (predEq' (shapeType (TSnoc (TSnoc g a) b) t ht))) + (sym (shapeType g u2 hu2))) in + let hht1' = coeUsage + (justInj' + (trans (sym (trans (sym (cong (uadd (USnoc d2 One)) + (uscaleOne (USnoc dv2 Zero)))) hadd1)) + (trans (uaddUSnocReduce d2 dv2 One Zero) + (trans (cong (combMaybe (qAdd One Zero)) hdr1g) + (cong (\z => Just (USnoc dr1g z)) (qAddZeroR One)))))) + hht1 in + -- outer substitution: u1 for the (now top) type-`a` binder + let (dr ** (hadd2, hht2)) = + substLemma0 g a dr1g One (subst0 (shift 0 u2) t) dv1 u1 hht1' hu1 in + -- realign `dr = d` via associativity: (Dv1+Dv2)+D2 = Dv1+(D2+Dv2) = Dv1+Dr1g = Dr + let (yz ** (hyz, hx)) = uaddAssoc dv1 dv2 d2 d1 d hd1 hd in + coeUsage + (sym (justInj' + (trans (sym hx) + (trans (cong (uadd dv1) + (justInj' (trans (sym (trans (sym (uaddComm dv2 d2)) hyz)) hdr1g))) + (trans (uaddComm dv1 dr1g) + (trans (sym (cong (uadd dr1g) (uscaleOne dv1))) hadd2)))))) + hht2