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..284d8eb 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 ------------------------------------------------------------