From db920373114e9e67e6e74a585357a866ebd34ca5 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 13:55:00 +0100 Subject: [PATCH 01/63] fix(proofs): tropical-session Lean proof compiles under Lean 4.13.0 Two minimal edits, no change to the proofs' content: - drop a redundant `simp` ("no goals to be solved") in the eval_recv case of tropical_session_soundness; - insert `simp only [TropicalBudget] at *` before the three `omega` calls in budget_strictly_bounds_billing, so omega sees through the `abbrev TropicalBudget := Nat` (4.13.0 no longer unfolds the abbrev for omega, which otherwise reports "No usable constraints found"). No sorry/admit/axiom/native_decide. `lean TropicalSessionTypes.lean` now exits 0. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../tropical-session-types/TropicalSessionTypes.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/docs/academic/tropical-session-types/TropicalSessionTypes.lean b/docs/academic/tropical-session-types/TropicalSessionTypes.lean index cb2b9fe5..8c9bd93d 100644 --- a/docs/academic/tropical-session-types/TropicalSessionTypes.lean +++ b/docs/academic/tropical-session-types/TropicalSessionTypes.lean @@ -104,7 +104,6 @@ theorem tropical_session_soundness (s : Session) (c : TropicalBudget) | eval_recv _ ih => unfold tropicalGrade tropicalSeq rw [ih] - simp | eval_spec _ _ ih1 ih2 => unfold tropicalGrade tropicalPar rw [ih1, ih2] @@ -136,12 +135,17 @@ theorem budget_strictly_bounds_billing (s : Session) : simp [tropicalGrade, linearBilling] | send s' ih => unfold tropicalGrade tropicalSeq linearBilling + -- `TropicalBudget` is an abbrev for `Nat`; unfold it everywhere so that + -- omega sees a uniform set of `Nat` atoms in the goal and the IH. + simp only [TropicalBudget] at * omega | recv s' ih => unfold tropicalGrade tropicalSeq linearBilling + simp only [TropicalBudget] at * omega | spec_branch s1 s2 ih1 ih2 => unfold tropicalGrade tropicalPar linearBilling + simp only [TropicalBudget] at * -- Lean 4's Presburger arithmetic solver automatically proves that -- max(A, B) ≤ A + B for all natural numbers. omega From ca2b51430951a8ea8783c8e932062eeef97c6a84 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 13:55:17 +0100 Subject: [PATCH 02/63] proof(solo-core): mechanise reduction + prove progress (Track F1) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the call-by-value reduction relation and the progress half of Solo-core soundness; preservation remains (?todo_preservation). - Subst.idr (new): de Bruijn shift + single-variable substitution (subst0), structurally total, no assert_total. - Soundness.idr: Step now has its CBV constructors (beta/let/case/ projection redexes + evaluation-context congruences, per spec §4.2-4.3); progress proven by induction on the typing derivation with canonical-forms reasoning inlined; StepsTo's reduct is erased. - ContextLemmas.idr (new): IsZero predicate + Empty/scale inversions. - Typing.idr: encoding-only reformulation needed to *prove* (not just *state*) the metatheory in Idris2 — split contexts of T-App/Pair/ Case/Let are explicit (Idris2 erases indices, so they must be runtime to be analysed) and the all-zero context of T-Var/T-Unit uses the analysable IsZero premise instead of the non-invertible computed index ctxZero g. The typing *relation* is unchanged. No believe_me/assert_total/postulate; idris2 --check Soundness.idr exits 0; progress is total and hole-free. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../solo-core/ContextLemmas.idr | 72 ++++++ .../solo-core/Soundness.idr | 205 +++++++++++++++++- .../formal-verification/solo-core/Subst.idr | 94 ++++++++ .../formal-verification/solo-core/Typing.idr | 57 +++-- 4 files changed, 397 insertions(+), 31 deletions(-) create mode 100644 docs/academic/formal-verification/solo-core/ContextLemmas.idr create mode 100644 docs/academic/formal-verification/solo-core/Subst.idr diff --git a/docs/academic/formal-verification/solo-core/ContextLemmas.idr b/docs/academic/formal-verification/solo-core/ContextLemmas.idr new file mode 100644 index 00000000..468548e6 --- /dev/null +++ b/docs/academic/formal-verification/solo-core/ContextLemmas.idr @@ -0,0 +1,72 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Context-level lemmas supporting the Solo-core soundness proofs. +-- +-- Two design notes, both forced by mechanising (rather than merely +-- *stating*) the meta-theory in Idris2: +-- +-- 1. `IsZero g` replaces the bare index `ctxZero g0` that the +-- week-1-2 statement-only `Typing.idr` used for the all-zero +-- context in T-Var / T-Unit. A computed index such as +-- `ctxZero g0` is not invertible by unification, so a derivation +-- cannot be pattern-matched against a *concrete* context (e.g. +-- `Empty`). `IsZero` is the same information as an analysable, +-- inductive premise: `IsZero g` holds exactly when every entry +-- of `g` carries quantity `Zero`, i.e. iff `g = ctxZero g`. +-- +-- 2. The pointwise inversions below take their contexts as explicit +-- (runtime) arguments. Idris2 erases data-type indices, so the +-- split contexts threaded through T-App / T-Pair / T-Case / +-- T-Let must be available at run time to be analysed at all; the +-- reformulated `Typing.idr` therefore passes them explicitly. +-- +-- None of this changes the typing *relation* — the set of derivable +-- `Has g t a` judgements is identical to the statement-only version. + +module ContextLemmas + +import Quantity +import Syntax +import Context + +%default total + +------------------------------------------------------------ +-- The "every entry is Zero" predicate +------------------------------------------------------------ + +||| `IsZero g` witnesses that every binding in `g` has quantity +||| `Zero`. This is the analysable form of "`g` is an all-zero +||| context" (`g = ctxZero g`), used by T-Var and T-Unit. +public export +data IsZero : Ctx -> Type where + IZEmpty : IsZero Empty + IZSnoc : IsZero g -> IsZero (Snoc g a Zero) + +||| `ctxZero g` is always a zero context. +public export +ctxZeroIsZero : (g : Ctx) -> IsZero (ctxZero g) +ctxZeroIsZero Empty = IZEmpty +ctxZeroIsZero (Snoc g a q) = IZSnoc (ctxZeroIsZero g) + +------------------------------------------------------------ +-- Inversions: when does a combination collapse to `Empty`? +------------------------------------------------------------ + +||| If two contexts add to `Empty`, both were `Empty`. Contexts are +||| explicit so the proof can case-split them (indices are erased). +public export +addEmptyInv : (x, y : Ctx) -> ctxAdd x y = Just Empty -> (x = Empty, y = Empty) +addEmptyInv Empty Empty _ = (Refl, Refl) +addEmptyInv Empty (Snoc _ _ _) Refl impossible +addEmptyInv (Snoc _ _ _) Empty Refl impossible +addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) prf with (ctxAdd g1 g2) + addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) Refl | Nothing impossible + addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) Refl | (Just _) impossible + +||| Scaling a context to `Empty` means it was already `Empty`. +public export +scaleEmptyInv : (q : Q) -> (g : Ctx) -> ctxScale q g = Empty -> g = Empty +scaleEmptyInv q Empty _ = Refl +scaleEmptyInv q (Snoc _ _ _) Refl impossible diff --git a/docs/academic/formal-verification/solo-core/Soundness.idr b/docs/academic/formal-verification/solo-core/Soundness.idr index 112272ab..c6b3a683 100644 --- a/docs/academic/formal-verification/solo-core/Soundness.idr +++ b/docs/academic/formal-verification/solo-core/Soundness.idr @@ -15,7 +15,9 @@ module Soundness import Quantity import Syntax import Context +import ContextLemmas import Typing +import Subst %default total @@ -42,22 +44,114 @@ data Value : Tm -> Type where -- reduction. They are introduced alongside the progress / -- preservation proofs in weeks 3-6. +||| Call-by-value, left-to-right small-step reduction. The redex +||| rules (beta, projection, case, let) mirror `docs/spec.md` §4.3; +||| the congruence rules implement the evaluation contexts of +||| §4.2 (function before argument, left of a pair before right, +||| inside an injection, scrutinee before branch selection). We do +||| NOT reduce under a binder, so every `Lam` is a value. public export data Step : Tm -> Tm -> Type where - -- Constructors intentionally omitted until week 3. - -- This keeps the *statements* below well-typed without - -- prematurely committing to a specific operational-semantics - -- formulation. The constructors will mirror the reference - -- interpreter in `lib/interp.ml` (call-by-value, left-to-right). + + ------------------------------------------------------------ + -- beta / redex rules + ------------------------------------------------------------ + + ||| (fn(q x:a) => body) v → body[0 ↦ v] + SBeta : Value v + -> Step (App (Lam q a body) v) (subst0 body v) + + ||| fst (v1, v2) → v1 + SFstBeta : Value v1 -> Value v2 + -> Step (Fst (Pair v1 v2)) v1 + + ||| snd (v1, v2) → v2 + SSndBeta : Value v1 -> Value v2 + -> Step (Snd (Pair v1 v2)) v2 + + ||| case (inl v) of {l; r} → l[0 ↦ v] + SCaseL : Value v + -> Step (Case (Inl b v) tL tR) (subst0 tL v) + + ||| case (inr v) of {l; r} → r[0 ↦ v] + SCaseR : Value v + -> Step (Case (Inr a v) tL tR) (subst0 tR v) + + ||| let (q x) = v in body → body[0 ↦ v] + SLetBeta : Value v + -> Step (Let q v body) (subst0 body v) + + ------------------------------------------------------------ + -- congruence rules (evaluation contexts) + ------------------------------------------------------------ + + SApp1 : Step t1 t1' -> Step (App t1 t2) (App t1' t2) + SApp2 : Value v1 -> Step t2 t2' -> Step (App v1 t2) (App v1 t2') + SPair1 : Step t1 t1' -> Step (Pair t1 t2) (Pair t1' t2) + SPair2 : Value v1 -> Step t2 t2' -> Step (Pair v1 t2) (Pair v1 t2') + SFst : Step t t' -> Step (Fst t) (Fst t') + SSnd : Step t t' -> Step (Snd t) (Snd t') + SInl : Step t t' -> Step (Inl b t) (Inl b t') + SInr : Step t t' -> Step (Inr a t) (Inr a t') + SCase : Step s s' -> Step (Case s tL tR) (Case s' tL tR) + SLet1 : Step e e' -> Step (Let q e body) (Let q e' body) ------------------------------------------------------------ -- Existential wrapper (no dependent pair imports needed) ------------------------------------------------------------ -||| Simple Sigma to avoid bringing in `Data.DPair` right now. +||| Simple Sigma to avoid bringing in `Data.DPair` right now. The +||| reduct `t'` is erased (`0`): `StepsTo t` is the proposition +||| "there exists `t'` with `t` ⟶ `t'`", and the proofs never need +||| to compute the reduct as run-time data. public export data StepsTo : Tm -> Type where - MkStepsTo : (t' : Tm) -> Step t t' -> StepsTo t + MkStepsTo : (0 t' : Tm) -> Step t t' -> StepsTo t + +------------------------------------------------------------ +-- Inversions used by progress +------------------------------------------------------------ + +||| The empty context binds no variables. +noEmptyVar : HasVar Empty n a -> Void +noEmptyVar (HVHere _ _) impossible +noEmptyVar (HVThere _ _) impossible + +||| Elimination forms are never values. +notValApp : Value (App x y) -> Void +notValApp VUnit impossible +notValApp VLam impossible +notValApp (VPair _ _) impossible +notValApp (VInl _) impossible +notValApp (VInr _) impossible + +notValFst : Value (Fst x) -> Void +notValFst VUnit impossible +notValFst VLam impossible +notValFst (VPair _ _) impossible +notValFst (VInl _) impossible +notValFst (VInr _) impossible + +notValSnd : Value (Snd x) -> Void +notValSnd VUnit impossible +notValSnd VLam impossible +notValSnd (VPair _ _) impossible +notValSnd (VInl _) impossible +notValSnd (VInr _) impossible + +notValCase : Value (Case s l r) -> Void +notValCase VUnit impossible +notValCase VLam impossible +notValCase (VPair _ _) impossible +notValCase (VInl _) impossible +notValCase (VInr _) impossible + +notValLet : Value (Let q e b) -> Void +notValLet VUnit impossible +notValLet VLam impossible +notValLet (VPair _ _) impossible +notValLet (VInl _) impossible +notValLet (VInr _) impossible ------------------------------------------------------------ -- Progress @@ -66,12 +160,101 @@ data StepsTo : Tm -> Type where ||| Progress: a closed, well-typed Solo term is either a value ||| or can take a step. ||| -||| "Closed" means typed in the empty context — there are no -||| free de Bruijn indices because `Empty` has no `HVHere` / -||| `HVThere` inhabitants. +||| "Closed" means typed in the empty context — `Empty` has no +||| `HasVar` inhabitants (`noEmptyVar`), so there are no free de +||| Bruijn indices. The proof is by induction on the typing +||| derivation; the splitting rules first invert their context +||| equation to learn that every sub-derivation is itself closed, +||| then recurse left-to-right per the call-by-value strategy. public export progress : Has Empty t a -> Either (Value t) (StepsTo t) -progress _ = ?todo_progress + +progress (THVar v) = absurd (noEmptyVar v) + +progress (THUnit _) = Left VUnit + +progress (THLam _) = Left VLam + +progress (THInl d) = case progress d of + Right (MkStepsTo _ st) => Right (MkStepsTo _ (SInl st)) + Left dval => Left (VInl dval) + +progress (THInr d) = case progress d of + Right (MkStepsTo _ st) => Right (MkStepsTo _ (SInr st)) + Left dval => Left (VInr dval) + +progress (THApp g1 g2 q f x prf) = + let (e1, esc) = addEmptyInv g1 (ctxScale q g2) prf + e2 = scaleEmptyInv q g2 esc in + case (e1, e2) of + (Refl, Refl) => case progress f of + Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SApp1 st1)) + Left fval => case progress x of + Right (MkStepsTo _ st2) => Right (MkStepsTo _ (SApp2 fval st2)) + Left xval => case f of + THLam _ => Right (MkStepsTo _ (SBeta xval)) + THVar v => absurd (noEmptyVar v) + THApp _ _ _ _ _ _ => absurd (notValApp fval) + THFst _ => absurd (notValFst fval) + THSnd _ => absurd (notValSnd fval) + THCase _ _ _ _ _ _ => absurd (notValCase fval) + THLet _ _ _ _ _ _ => absurd (notValLet fval) + +progress (THPair g1 g2 p1 p2 prf) = + let (e1, e2) = addEmptyInv g1 g2 prf in + case (e1, e2) of + (Refl, Refl) => case progress p1 of + Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SPair1 st1)) + Left v1 => case progress p2 of + Right (MkStepsTo _ st2) => Right (MkStepsTo _ (SPair2 v1 st2)) + Left v2 => Left (VPair v1 v2) + +progress (THFst d) = case progress d of + Right (MkStepsTo _ st) => Right (MkStepsTo _ (SFst st)) + Left dval => case d of + THPair _ _ _ _ _ => case dval of + VPair v1 v2 => Right (MkStepsTo _ (SFstBeta v1 v2)) + THVar v => absurd (noEmptyVar v) + THApp _ _ _ _ _ _ => absurd (notValApp dval) + THFst _ => absurd (notValFst dval) + THSnd _ => absurd (notValSnd dval) + THCase _ _ _ _ _ _ => absurd (notValCase dval) + THLet _ _ _ _ _ _ => absurd (notValLet dval) + +progress (THSnd d) = case progress d of + Right (MkStepsTo _ st) => Right (MkStepsTo _ (SSnd st)) + Left dval => case d of + THPair _ _ _ _ _ => case dval of + VPair v1 v2 => Right (MkStepsTo _ (SSndBeta v1 v2)) + THVar v => absurd (noEmptyVar v) + THApp _ _ _ _ _ _ => absurd (notValApp dval) + THFst _ => absurd (notValFst dval) + THSnd _ => absurd (notValSnd dval) + THCase _ _ _ _ _ _ => absurd (notValCase dval) + THLet _ _ _ _ _ _ => absurd (notValLet dval) + +progress (THCase g1 g2 s l r prf) = + let (e1, e2) = addEmptyInv g1 g2 prf in + case (e1, e2) of + (Refl, Refl) => case progress s of + Right (MkStepsTo _ st) => Right (MkStepsTo _ (SCase st)) + Left sval => case s of + THInl _ => case sval of VInl v => Right (MkStepsTo _ (SCaseL v)) + THInr _ => case sval of VInr v => Right (MkStepsTo _ (SCaseR v)) + THVar v => absurd (noEmptyVar v) + THApp _ _ _ _ _ _ => absurd (notValApp sval) + THFst _ => absurd (notValFst sval) + THSnd _ => absurd (notValSnd sval) + THCase _ _ _ _ _ _ => absurd (notValCase sval) + THLet _ _ _ _ _ _ => absurd (notValLet sval) + +progress (THLet g1 g2 q d1 d2 prf) = + let (esc, e2) = addEmptyInv (ctxScale q g1) g2 prf + e1 = scaleEmptyInv q g1 esc in + case (e1, e2) of + (Refl, Refl) => case progress d1 of + Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SLet1 st1)) + Left v1 => Right (MkStepsTo _ (SLetBeta v1)) ------------------------------------------------------------ -- Preservation diff --git a/docs/academic/formal-verification/solo-core/Subst.idr b/docs/academic/formal-verification/solo-core/Subst.idr new file mode 100644 index 00000000..9b912c31 --- /dev/null +++ b/docs/academic/formal-verification/solo-core/Subst.idr @@ -0,0 +1,94 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- De Bruijn shifting and single-variable substitution for the Solo +-- core. These are the term-level operations that the small-step +-- reduction relation (Soundness.idr) uses in its beta/let/case rules, +-- and that the substitution lemma (SubstLemma.idr) proves type-safe. +-- +-- The formulation is the standard call-by-value de Bruijn one +-- (cf. TAPL ch. 6): `shift c t` lifts every free variable index >= c +-- by one; `subst j s t` replaces variable `j` by `s` inside `t`, +-- decrementing the free variables above `j` and lifting `s` past each +-- binder it crosses. `subst0` is the index-0 instance used by every +-- beta reduction. Everything is structurally recursive, so `%default +-- total` holds with no `assert_total`. + +module Subst + +import Syntax + +%default total + +------------------------------------------------------------ +-- Variable shifting +------------------------------------------------------------ + +||| `shiftVar c k` lifts a single de Bruijn index: indices `< c` are +||| left alone (they are bound by binders crossed since the cutoff), +||| indices `>= c` are incremented (they are free past the cutoff). +public export +shiftVar : (c : Nat) -> (k : Nat) -> Nat +shiftVar Z k = S k +shiftVar (S c) Z = Z +shiftVar (S c) (S k) = S (shiftVar c k) + +||| `shift c t` lifts every free variable of `t` whose index is `>= c`. +||| The cutoff increases by one under each binder. +public export +shift : (c : Nat) -> Tm -> Tm +shift c (Var k) = Var (shiftVar c k) +shift c UnitT = UnitT +shift c (Lam q a t) = Lam q a (shift (S c) t) +shift c (App t1 t2) = App (shift c t1) (shift c t2) +shift c (Pair t1 t2) = Pair (shift c t1) (shift c t2) +shift c (Fst t) = Fst (shift c t) +shift c (Snd t) = Snd (shift c t) +shift c (Inl b t) = Inl b (shift c t) +shift c (Inr a t) = Inr a (shift c t) +shift c (Case s l r) = Case (shift c s) (shift (S c) l) (shift (S c) r) +shift c (Let q e b) = Let q (shift c e) (shift (S c) b) + +------------------------------------------------------------ +-- Single-variable substitution +------------------------------------------------------------ + +||| `substVar j k s` is the variable case of substitution: replace +||| index `k` while substituting for index `j` with `s`. +||| +||| * `k < j` — a more recently bound variable, unchanged. +||| * `k = j` — the substituted variable; yields `s` lifted past the +||| `j` binders crossed to reach this occurrence. +||| * `k > j` — a free variable above the hole, decremented by one +||| (its binder is gone). +||| +||| The single `shift 0` in the `S j / S k` case threads the +||| past-binder lifting through the recursion, so callers of `subst` +||| do *not* pre-shift `s` when descending under a binder. +public export +substVar : (j : Nat) -> (k : Nat) -> (s : Tm) -> Tm +substVar Z Z s = s +substVar Z (S k) s = Var k +substVar (S j) Z s = Var Z +substVar (S j) (S k) s = shift 0 (substVar j k s) + +||| `subst j s t` replaces the free variable `j` in `t` by `s`. +public export +subst : (j : Nat) -> (s : Tm) -> Tm -> Tm +subst j s (Var k) = substVar j k s +subst j s UnitT = UnitT +subst j s (Lam q a t) = Lam q a (subst (S j) s t) +subst j s (App t1 t2) = App (subst j s t1) (subst j s t2) +subst j s (Pair t1 t2) = Pair (subst j s t1) (subst j s t2) +subst j s (Fst t) = Fst (subst j s t) +subst j s (Snd t) = Snd (subst j s t) +subst j s (Inl b t) = Inl b (subst j s t) +subst j s (Inr a t) = Inr a (subst j s t) +subst j s (Case sc l r) = Case (subst j s sc) (subst (S j) s l) (subst (S j) s r) +subst j s (Let q e b) = Let q (subst j s e) (subst (S j) s b) + +||| Substitute for the most-recently-bound variable (index 0). This is +||| the operation performed by every beta-style reduction. +public export +subst0 : Tm -> Tm -> Tm +subst0 body v = subst Z v body diff --git a/docs/academic/formal-verification/solo-core/Typing.idr b/docs/academic/formal-verification/solo-core/Typing.idr index 5aa9036a..4a00dfdc 100644 --- a/docs/academic/formal-verification/solo-core/Typing.idr +++ b/docs/academic/formal-verification/solo-core/Typing.idr @@ -7,11 +7,6 @@ -- context `g`, with `g`'s quantities exactly accounting for the -- uses of each bound variable inside `t`. -- --- These are the RULES, stated as data constructors. The meta- --- theorems (progress, preservation, affine-preservation) are --- stated in `Soundness.idr` and will be proved in weeks 3-12 of --- Track F1. --- -- Source of truth for the rule shapes: -- * docs/spec.md §3.1, §3.6 (T-Var, T-Lam, T-App, T-Let) -- * lib/quantity.ml — semiring operations and the "linear must @@ -26,12 +21,28 @@ -- formulation for which progress + preservation are provable, -- and is equivalent to the implementation's usage-walk for the -- Solo fragment. An explicit equivalence lemma is future work. +-- +-- ENCODING NOTE (week-3 mechanisation, vs. the week-1-2 statement +-- form): two purely-presentational changes were needed to make the +-- judgement *provable* in Idris2, neither of which alters the set of +-- derivable judgements: +-- +-- * The split contexts of T-App / T-Pair / T-Case / T-Let are now +-- **explicit** arguments (`(g1, g2 : Ctx) -> ...`). Idris2 erases +-- data-type indices, so without this the sub-contexts could not +-- be analysed inside the soundness proofs at all. +-- +-- * The all-zero context of T-Var / T-Unit is expressed by the +-- analysable premise `IsZero g` (from ContextLemmas) rather than +-- the non-invertible computed index `ctxZero g0`. `IsZero g` +-- holds iff `g = ctxZero g`, so the rule is unchanged in meaning. module Typing import Quantity import Syntax import Context +import ContextLemmas %default total @@ -41,15 +52,17 @@ import Context ------------------------------------------------------------ ||| `HasVar g n a` says the de Bruijn variable `n` has type `a` -||| in `g`, where `g` is a context that assigns quantity `One` -||| to position `n` and quantity `Zero` to every other position. -||| This is the T-Var rule in QTT: "using a variable once uses -||| it exactly once, and uses nothing else". +||| in `g`, where `g` assigns quantity `One` to position `n` and +||| quantity `Zero` to every other position. This is the T-Var +||| rule in QTT: "using a variable once uses it exactly once, and +||| uses nothing else". public export data HasVar : Ctx -> Nat -> Ty -> Type where - HVHere : HasVar (Snoc (ctxZero g) a One) Z a - HVThere : HasVar g n a - -> HasVar (Snoc g b Zero) (S n) a + ||| The variable is the most recently bound one: it sits at + ||| quantity `One` on top of an all-zero context. + HVHere : (g : Ctx) -> IsZero g -> HasVar (Snoc g a One) Z a + ||| Skip a more recent binding, which must be unused (`Zero`). + HVThere : (g : Ctx) -> HasVar g n a -> HasVar (Snoc g b Zero) (S n) a ------------------------------------------------------------ -- The typing judgement @@ -65,8 +78,9 @@ data Has : Ctx -> Tm -> Ty -> Type where THVar : HasVar g n a -> Has g (Var n) a - ||| T-Unit: the unit term types in the all-zero context. - THUnit : Has (ctxZero g) UnitT TUnit + ||| T-Unit: the unit term types in any all-zero context. + THUnit : IsZero g + -> Has g UnitT TUnit ||| T-Lam: introduce a binding with quantity `q` and type `a`, ||| type the body in the extended context. The resulting @@ -78,13 +92,15 @@ data Has : Ctx -> Tm -> Ty -> Type where ||| scaled by the function's parameter quantity `q`, and the ||| whole application is typed in the pointwise sum ||| `g1 + q * g2`. - THApp : Has g1 t1 (TArr q a b) + THApp : (g1, g2 : Ctx) -> (q : Q) + -> Has g1 t1 (TArr q a b) -> Has g2 t2 a -> ctxAdd g1 (ctxScale q g2) = Just g -> Has g (App t1 t2) b ||| T-Pair: product introduction splits the context additively. - THPair : Has g1 t1 a + THPair : (g1, g2 : Ctx) + -> Has g1 t1 a -> Has g2 t2 b -> ctxAdd g1 g2 = Just g -> Has g (Pair t1 t2) (TPair a b) @@ -107,9 +123,9 @@ data Has : Ctx -> Tm -> Ty -> Type where ||| T-Case: the scrutinee is typed in `g1`; each branch binds ||| the injected value with quantity One and is typed in `g2` ||| extended with that binder. Branches must agree on `g2` and - ||| on the result type. The whole `case` is typed in - ||| `g1 + g2`. - THCase : Has g1 t (TSum a b) + ||| on the result type. The whole `case` is typed in `g1 + g2`. + THCase : (g1, g2 : Ctx) + -> Has g1 t (TSum a b) -> Has (Snoc g2 a One) tL c -> Has (Snoc g2 b One) tR c -> ctxAdd g1 g2 = Just g @@ -120,7 +136,8 @@ data Has : Ctx -> Tm -> Ty -> Type where ||| to `g2` (the body's context). This is the usual QTT let ||| rule and matches how `lib/typecheck.ml` threads quantities ||| through `let` bindings. - THLet : Has g1 t1 a + THLet : (g1, g2 : Ctx) -> (q : Q) + -> Has g1 t1 a -> Has (Snoc g2 a q) t2 b -> ctxAdd (ctxScale q g1) g2 = Just g -> Has g (Let q t1 t2) b From 4c03522240138083a856b09e0cfd865216172bba Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 14:02:40 +0100 Subject: [PATCH 03/63] tooling(proofs): add proof-check harness + just recipes Backs the `just proof-check-{idris2,lean,agda,all}` recipes (referenced by the PROOF-STATUS templates but never implemented) with tools/check-proofs.sh. Each stage re-runs the proof against its assistant and fails on a type error or any dangerous escape hatch (believe_me / assert_total / postulate / sorry / axiom / native_decide / idris_crash); unfinished Idris2 `?` holes are reported as a warning. Coverage: Solo-core QTT metatheory (Idris2), tropical session types (Lean 4), and the 23 echo-boundary certificates (Agda). The Agda stage needs AFFINESCRIPT_ECHO_TYPES_DIR + AGDA_STDLIB (the certificates import the external echo-types proofs + agda-stdlib) and skips with a clear message when either is unset, so the harness still runs hermetically. Verified: idris2/lean stages PASS; agda stage PASSES all 23 proofs with the env vars set and SKIPs cleanly without them. Co-Authored-By: Claude Opus 4.8 (1M context) --- justfile | 23 ++++++++ tools/check-proofs.sh | 131 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 154 insertions(+) create mode 100755 tools/check-proofs.sh diff --git a/justfile b/justfile index 28801b80..8e732784 100644 --- a/justfile +++ b/justfile @@ -104,6 +104,29 @@ guard: doc-truth-bless: ./tools/check-doc-truthing.sh --update +# ── Proofs ───────────────────────────────────────────────────────────────────── +# Re-check the mechanised proofs against their proof assistants and fail on any +# dangerous escape hatch (believe_me / assert_total / postulate / sorry / axiom). +# Unfinished Idris2 `?` holes are reported as a warning, not a failure. + +# Check the Solo-core QTT metatheory (Idris2). +proof-check-idris2: + ./tools/check-proofs.sh --idris2 + +# Check the tropical-session-types proof (Lean 4). +proof-check-lean: + ./tools/check-proofs.sh --lean + +# Check the echo-boundary certificates (Agda). Needs AFFINESCRIPT_ECHO_TYPES_DIR +# and AGDA_STDLIB; skips with a message if either is unset (the proofs import +# modules from the external echo-types repo + agda-stdlib). +proof-check-agda: + ./tools/check-proofs.sh --agda + +# Check every mechanised proof in the repo. +proof-check-all: + ./tools/check-proofs.sh --all + # ── Compiler subcommands ────────────────────────────────────────────────────── # Run the lexer on a file diff --git a/tools/check-proofs.sh b/tools/check-proofs.sh new file mode 100755 index 00000000..1d0ebfb0 --- /dev/null +++ b/tools/check-proofs.sh @@ -0,0 +1,131 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell +# +# Proof-check harness for the AffineScript repository. +# +# Re-runs every mechanised proof in-tree against its proof assistant and +# fails on (a) a type-check error or (b) any "dangerous" escape hatch +# (believe_me / assert_total / postulate / sorry / axiom / native_decide +# / idris_crash). Unfinished proofs (Idris2 `?` holes) are reported as a +# WARNING, not a failure, so the harness can run during development. +# +# This is the backing for the `just proof-check-*` recipes referenced by +# the PROOF-STATUS templates; before this script those recipes had no +# implementation. Run from anywhere; it cd's to the repo root. +# +# Coverage: +# --idris2 Solo-core QTT metatheory (docs/academic/formal-verification/solo-core) +# --lean Tropical session types (docs/academic/tropical-session-types) +# --agda Echo-boundary certificates (proposals/**), iff the external +# echo-types proofs + agda-stdlib are reachable (see env vars). +# --all all of the above (default) +# +# Agda external dependencies (the proofs import modules that live OUTSIDE +# this repo, so they cannot be checked hermetically here): +# AFFINESCRIPT_ECHO_TYPES_DIR -> /proofs/agda +# AGDA_STDLIB -> /src (matching the agda in PATH) +# If either is unset/missing the Agda stage SKIPS with a clear message +# (exit-neutral), it does not fail the run. + +set -uo pipefail + +cd "$(dirname "$0")/.." +REPO="$(pwd)" + +GREEN=$'\033[32m'; RED=$'\033[31m'; YEL=$'\033[33m'; DIM=$'\033[2m'; RST=$'\033[0m' +pass=0; fail=0; skip=0 + +ok () { printf '%s PASS%s %s\n' "$GREEN" "$RST" "$1"; pass=$((pass+1)); } +bad () { printf '%s FAIL%s %s\n' "$RED" "$RST" "$1"; fail=$((fail+1)); } +warn () { printf '%s WARN%s %s\n' "$YEL" "$RST" "$1"; } +note () { printf '%s SKIP%s %s\n' "$DIM" "$RST" "$1"; skip=$((skip+1)); } + +# Dangerous escape hatches that must never appear in a finished proof. +# Comment lines (-- … / // … / -- in Agda, Idris, Lean) are stripped first. +DANGER='believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|\bsorry\b|\baxiom\b|native_decide' + +scan_danger () { # ; prints offending lines, returns 1 if any + local root="$1"; shift + local found=0 f hits + while IFS= read -r f; do + # strip whole-line comments (Idris/Agda --, Lean --) before scanning + hits=$(grep -nE "$DANGER" "$f" 2>/dev/null | grep -vE ':\s*(--|//)' || true) + if [ -n "$hits" ]; then echo " $f:"; echo "$hits" | sed 's/^/ /'; found=1; fi + done < <(for e in "$@"; do find "$root" -name "*.$e" 2>/dev/null; done) + return $found +} + +# ───────────────────────────────────────────────────────────────────────────── +check_idris2 () { + local dir="$REPO/docs/academic/formal-verification/solo-core" + command -v idris2 >/dev/null 2>&1 || { note "Idris2 (idris2 not on PATH)"; return; } + echo "── Idris2: Solo-core QTT metatheory ──" + # Soundness.idr transitively builds Quantity/Syntax/Context/ContextLemmas/Typing/Subst. + if ( cd "$dir" && idris2 --check Soundness.idr ) >/tmp/.pc_idris 2>&1; then + ok "idris2 --check Soundness.idr (+ all imports)" + else + bad "idris2 --check Soundness.idr"; sed 's/^/ /' /tmp/.pc_idris | tail -25 + fi + if scan_danger "$dir" idr; then ok "no dangerous primitives (Idris2)"; else bad "dangerous primitive in Idris2 proof"; fi + # holes are incompleteness, not unsoundness → warn only + local holes + holes=$(grep -rnE '\?[a-zA-Z_][a-zA-Z0-9_]*' "$dir"/*.idr 2>/dev/null | grep -vE ':\s*--' || true) + [ -n "$holes" ] && { warn "unfinished holes remain:"; echo "$holes" | sed 's/^/ /'; } +} + +# ───────────────────────────────────────────────────────────────────────────── +check_lean () { + local dir="$REPO/docs/academic/tropical-session-types" + command -v lean >/dev/null 2>&1 || { note "Lean (lean not on PATH)"; return; } + echo "── Lean 4: Tropical session types ──" + if ( cd "$dir" && lean TropicalSessionTypes.lean ) >/tmp/.pc_lean 2>&1; then + ok "lean TropicalSessionTypes.lean" + else + bad "lean TropicalSessionTypes.lean"; sed 's/^/ /' /tmp/.pc_lean | tail -25 + fi + if scan_danger "$dir" lean; then ok "no dangerous tactics (Lean)"; else bad "dangerous tactic in Lean proof"; fi +} + +# ───────────────────────────────────────────────────────────────────────────── +check_agda () { + command -v agda >/dev/null 2>&1 || { note "Agda (agda not on PATH)"; return; } + local echo_dir="${AFFINESCRIPT_ECHO_TYPES_DIR:-}" + local stdlib="${AGDA_STDLIB:-}" + echo "── Agda: echo-boundary certificates ──" + if [ -z "$echo_dir" ] || [ ! -d "$echo_dir" ]; then + note "Agda (set AFFINESCRIPT_ECHO_TYPES_DIR to /proofs/agda)"; return; fi + if [ -z "$stdlib" ] || [ ! -f "$stdlib/Data/Nat/Base.agda" ]; then + note "Agda (set AGDA_STDLIB to the agda-stdlib 'src' dir)"; return; fi + local self="$REPO/proposals/echo-types" + export AGDA_DIR; AGDA_DIR="$(mktemp -d)"; trap 'rm -rf "$AGDA_DIR"' RETURN + # only delete .agdai we create + local snap; snap="$(mktemp)" + find "$REPO/proposals" "$echo_dir" "$stdlib" -name '*.agdai' 2>/dev/null | sort >"$snap" + local agda_fail=0 f dir + while IFS= read -r f; do + dir="$(dirname "$f")" + if agda --no-libraries -i "$stdlib" -i "$echo_dir" -i "$self" -i "$dir" "$f" >/dev/null 2>&1; then :; else + echo " FAIL $f"; agda_fail=1; fi + done < <( { echo "$REPO/proposals/echo-types/EchoEncodingFaithfulness.agda"; + find "$REPO/proposals/nextgen-evangelist/echo-boundary/samples" -name '*.agda'; + find "$REPO/proposals/idaptik/migrated" -name '*Boundary.agda'; } | sort -u ) + [ "$agda_fail" -eq 0 ] && ok "all in-repo .agda boundary proofs type-check" || bad "an Agda boundary proof failed" + if scan_danger "$REPO/proposals" agda; then ok "no dangerous primitives (Agda)"; else bad "dangerous primitive in Agda proof"; fi + find "$REPO/proposals" "$echo_dir" "$stdlib" -name '*.agdai' 2>/dev/null | sort >"$snap.after" + comm -13 "$snap" "$snap.after" | while IFS= read -r a; do [ -n "$a" ] && rm -f "$a"; done + rm -f "$snap" "$snap.after" +} + +# ───────────────────────────────────────────────────────────────────────────── +case "${1:---all}" in + --idris2) check_idris2 ;; + --lean) check_lean ;; + --agda) check_agda ;; + --all) check_idris2; echo; check_lean; echo; check_agda ;; + *) echo "usage: $0 [--idris2|--lean|--agda|--all]" >&2; exit 2 ;; +esac + +echo +printf '%s passed, %s failed, %s skipped\n' "$pass" "$fail" "$skip" +[ "$fail" -eq 0 ] From 9fb25f34f1a643dde3f0fd78a7d6d311296eef5e Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 17:19:40 +0100 Subject: [PATCH 04/63] proof(solo-core): prove progress + AFFINE preservation (Track F1 complete) Completes the Solo-core soundness metatheory. progress and preservation are fully mechanised: idris2 --check Soundness.idr exits 0, every definition is total, and there is NO believe_me / assert_total / really_believe_me / postulate / ? hole. What is proved: * progress : Has Empty t a -> Either (Value t) (StepsTo t) * preservation: Has g t a -> Step t t' -> (g' ** (Weaker g' g, Has g' t' a)) * affinePreservation: same. The substitution-lemma infrastructure (ContextLemmas.idr AddCtx algebra, SubstLemma.idr substGen/substLemma0, Subst.idr de Bruijn shift/subst) was produced by a parallel proof search and re-verified locally. Mechanisation finding + owner decision (2026-06-15): The original statement asked for the reduct in the SAME context. That is FALSE for the Solo core as designed -- TPair introduces multiplicatively (split context) but is eliminated by Fst/Snd projections, so e.g. "Snd (Pair x y) steps to y" (x linear) drops x's resources, leaving a strictly smaller context. Every beta-rule preserves the context exactly (via the substitution lemma); only the projections shrink it. Resolved the AFFINE way (AffineScript is affine: lib/quantity.ml's q_le permits under-use): the language is unchanged (split product + projections + eager CBV kept) and preservation is restated affinely (reduct in a Weaker sub-context, g' <= g pointwise, same shape/types). See dev-notes/2026-06-15-affinescript-solo-core-preservation/. Typing.idr encoding note: split contexts of T-App/Pair/Case/Let are explicit AddCtx premises and T-Var/T-Unit use an IsZero premise -- an encoding change (Idris2 erases data indices) that leaves the set of derivable judgements unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../solo-core/ContextLemmas.idr | 764 +++++++++++++++++- .../formal-verification/solo-core/README.adoc | 102 ++- .../solo-core/Soundness.idr | 474 ++++++----- .../formal-verification/solo-core/Subst.idr | 143 ++-- .../solo-core/SubstLemma.idr | 478 +++++++++++ .../formal-verification/solo-core/Typing.idr | 102 ++- 6 files changed, 1680 insertions(+), 383 deletions(-) create mode 100644 docs/academic/formal-verification/solo-core/SubstLemma.idr diff --git a/docs/academic/formal-verification/solo-core/ContextLemmas.idr b/docs/academic/formal-verification/solo-core/ContextLemmas.idr index 468548e6..4ad643e1 100644 --- a/docs/academic/formal-verification/solo-core/ContextLemmas.idr +++ b/docs/academic/formal-verification/solo-core/ContextLemmas.idr @@ -1,28 +1,25 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- --- Context-level lemmas supporting the Solo-core soundness proofs. +-- Context algebra for the Solo-core preservation proof. -- --- Two design notes, both forced by mechanising (rather than merely --- *stating*) the meta-theory in Idris2: +-- The friction in `Context.idr` is that `ctxAdd` is Maybe-valued (a +-- pointwise add only makes sense on equal-shape contexts) and does +-- not track type agreement. For the QTT substitution lemma we need a +-- *type-tracking, total, analysable* notion of "g is the pointwise +-- sum of g1 and g2". We therefore work with the inductive relation +-- `AddCtx g1 g2 g`, which: -- --- 1. `IsZero g` replaces the bare index `ctxZero g0` that the --- week-1-2 statement-only `Typing.idr` used for the all-zero --- context in T-Var / T-Unit. A computed index such as --- `ctxZero g0` is not invertible by unification, so a derivation --- cannot be pattern-matched against a *concrete* context (e.g. --- `Empty`). `IsZero` is the same information as an analysable, --- inductive premise: `IsZero g` holds exactly when every entry --- of `g` carries quantity `Zero`, i.e. iff `g = ctxZero g`. +-- * forces g1, g2, g to share their spine AND their per-position +-- types (the `a` in `ACSnoc` is shared); +-- * records the per-position quantity sum (`qAdd q1 q2`); +-- * is Maybe-free, so all the semiring algebra is equational, +-- reusing the proven `Quantity.idr` laws via `cong`. -- --- 2. The pointwise inversions below take their contexts as explicit --- (runtime) arguments. Idris2 erases data-type indices, so the --- split contexts threaded through T-App / T-Pair / T-Case / --- T-Let must be available at run time to be analysed at all; the --- reformulated `Typing.idr` therefore passes them explicitly. --- --- None of this changes the typing *relation* — the set of derivable --- `Has g t a` judgements is identical to the statement-only version. +-- A bridge to `Context.ctxAdd` is provided (`addCtxToAdd`) so the +-- relation can be related back to the original `Just`-valued +-- definition where wanted; the typing rules in `Typing.idr` use +-- `AddCtx` directly. module ContextLemmas @@ -33,40 +30,731 @@ import Context %default total ------------------------------------------------------------ --- The "every entry is Zero" predicate +-- The type-tracking additive splitting relation ------------------------------------------------------------ -||| `IsZero g` witnesses that every binding in `g` has quantity -||| `Zero`. This is the analysable form of "`g` is an all-zero -||| context" (`g = ctxZero g`), used by T-Var and T-Unit. +||| `AddCtx g1 g2 g` : `g` is the pointwise quantity-sum of `g1` and +||| `g2`, which must share spine and types. +||| +||| `ACSnoc` stores the per-position type and the two summand +||| quantities as RUNTIME arguments. This lets the metatheory rebuild +||| the actual summand contexts from an `AddCtx` value alone — the +||| typed indices `g1`, `g2`, `g` are erased, so without these the +||| decomposition lemmas could not run. +public export +data AddCtx : Ctx -> Ctx -> Ctx -> Type where + ACEmpty : AddCtx Empty Empty Empty + ACSnoc : (a : Ty) -> (q1 : Q) -> (q2 : Q) + -> AddCtx g1 g2 g + -> AddCtx (Snoc g1 a q1) (Snoc g2 a q2) (Snoc g a (qAdd q1 q2)) + +||| Bridge: `AddCtx` implies the partial `ctxAdd` succeeds with the +||| same result. (Kept for cross-checking against `Context.idr`.) +public export +addCtxToAdd : AddCtx g1 g2 g -> ctxAdd g1 g2 = Just g +addCtxToAdd ACEmpty = Refl +addCtxToAdd (ACSnoc _ _ _ ac) = rewrite addCtxToAdd ac in Refl + +------------------------------------------------------------ +-- Typed-shape relation (same length AND same per-position types) +------------------------------------------------------------ + +||| `ShapeEq g1 g2` : the two contexts have the same spine and the +||| same type at every position (quantities free). The per-position +||| type/quantities are ERASED indices — `mkAdd` reads the actual +||| quantities from the (runtime) contexts instead, so `shapeScale` +||| does not need the scaling quantity at runtime. +public export +data ShapeEq : Ctx -> Ctx -> Type where + SEEmpty : ShapeEq Empty Empty + SESnoc : ShapeEq g1 g2 -> ShapeEq (Snoc g1 a q1) (Snoc g2 a q2) + +||| The two summands of an additive split share a typed shape. +public export +shapeSummands : AddCtx g1 g2 g -> ShapeEq g1 g2 +shapeSummands ACEmpty = SEEmpty +shapeSummands (ACSnoc a q1 q2 ac) = SESnoc (shapeSummands ac) + +||| The left summand shares a typed shape with the result. +public export +shapeLeftResult : AddCtx g1 g2 g -> ShapeEq g1 g +shapeLeftResult ACEmpty = SEEmpty +shapeLeftResult (ACSnoc a q1 q2 ac) = SESnoc (shapeLeftResult ac) + +||| Scaling preserves the typed shape (the scaling quantity is erased). +public export +shapeScale : {0 q : Q} -> (g : Ctx) -> ShapeEq g (ctxScale q g) +shapeScale Empty = SEEmpty +shapeScale (Snoc g a e) = SESnoc (shapeScale g) + +||| `ShapeEq` is symmetric. +public export +shapeSym : ShapeEq g1 g2 -> ShapeEq g2 g1 +shapeSym SEEmpty = SEEmpty +shapeSym (SESnoc se) = SESnoc (shapeSym se) + +||| `ShapeEq` is transitive. +public export +shapeTrans : ShapeEq g1 g2 -> ShapeEq g2 g3 -> ShapeEq g1 g3 +shapeTrans SEEmpty SEEmpty = SEEmpty +shapeTrans (SESnoc s1) (SESnoc s2) = SESnoc (shapeTrans s1 s2) + +||| Build the additive sum of two same-shaped contexts, reading the +||| quantities from the (runtime) contexts. The first context's type +||| is used at each position (matching `AddCtx`'s convention). +public export +mkAdd : (g1, g2 : Ctx) -> ShapeEq g1 g2 -> (g : Ctx ** AddCtx g1 g2 g) +mkAdd Empty Empty SEEmpty = (Empty ** ACEmpty) +mkAdd (Snoc g1 a q1) (Snoc g2 _ q2) (SESnoc se) = + let (g ** ac) = mkAdd g1 g2 se in + (Snoc g a (qAdd q1 q2) ** ACSnoc a q1 q2 ac) +mkAdd Empty (Snoc _ _ _) SEEmpty impossible +mkAdd (Snoc _ _ _) Empty SEEmpty impossible + +||| `AddCtx` is deterministic in its result. +public export +addDet : AddCtx g1 g2 ga -> AddCtx g1 g2 gb -> ga = gb +addDet ACEmpty ACEmpty = Refl +addDet (ACSnoc a q1 q2 ac1) (ACSnoc _ _ _ ac2) = + cong (\w => Snoc w a (qAdd q1 q2)) (addDet ac1 ac2) + +||| Determinism modulo propositional equality of the summands. +public export +addDetEq : AddCtx a b ga -> AddCtx a' b' gb -> a = a' -> b = b' -> ga = gb +addDetEq ac1 ac2 Refl Refl = addDet ac1 ac2 + +||| A split whose result is `Empty` has both summands `Empty`. +public export +addEmptyInv : AddCtx g1 g2 Empty -> (g1 = Empty, g2 = Empty) +addEmptyInv ACEmpty = (Refl, Refl) + +||| Scaling to `Empty` forces the context to be `Empty`. +public export +scaleEmptyInv : (g : Ctx) -> ctxScale q g = Empty -> g = Empty +scaleEmptyInv Empty _ = Refl +scaleEmptyInv (Snoc _ _ _) Refl impossible + + +------------------------------------------------------------ +-- IsZero (analysable "everything erased") +------------------------------------------------------------ + +||| `IsZero g` witnesses that every quantity in `g` is `Zero`. +||| `HasVar`'s `HVHere` carries one so the substitution proof can +||| analyse the surrounding context. public export data IsZero : Ctx -> Type where IZEmpty : IsZero Empty IZSnoc : IsZero g -> IsZero (Snoc g a Zero) -||| `ctxZero g` is always a zero context. +||| The canonical all-zero context built by `ctxZero` is zero. public export ctxZeroIsZero : (g : Ctx) -> IsZero (ctxZero g) ctxZeroIsZero Empty = IZEmpty ctxZeroIsZero (Snoc g a q) = IZSnoc (ctxZeroIsZero g) +||| Invert a zero `Snoc`: the tail is zero and the head quantity is +||| `Zero`. +public export +isZeroSnocInv : IsZero (Snoc g a q) -> (IsZero g, q = Zero) +isZeroSnocInv (IZSnoc iz) = (iz, Refl) + +||| Scaling a zero context by anything keeps it zero. +public export +isZeroScale : (q : Q) -> IsZero g -> IsZero (ctxScale q g) +isZeroScale q IZEmpty = IZEmpty +isZeroScale q (IZSnoc iz) = rewrite qMulZeroR q in IZSnoc (isZeroScale q iz) + ------------------------------------------------------------ --- Inversions: when does a combination collapse to `Empty`? +-- Scaling laws (pure functions, equational) ------------------------------------------------------------ -||| If two contexts add to `Empty`, both were `Empty`. Contexts are -||| explicit so the proof can case-split them (indices are erased). +||| Scaling by `One` is the identity. +public export +scaleOne : (g : Ctx) -> ctxScale One g = g +scaleOne Empty = Refl +scaleOne (Snoc g a q) = rewrite scaleOne g in rewrite qMulOneL q in Refl + +||| Scaling by `Zero` produces a manifestly-zero context — namely +||| `ctxZero g`. +public export +scaleZero : (g : Ctx) -> ctxScale Zero g = ctxZero g +scaleZero Empty = Refl +scaleZero (Snoc g a q) = rewrite scaleZero g in Refl + +||| Scaling ANY context by `Zero` yields a zero context. +public export +scaleZeroIsZero : (g : Ctx) -> IsZero (ctxScale Zero g) +scaleZeroIsZero g = rewrite scaleZero g in ctxZeroIsZero g + +||| Scaling associates with quantity multiplication. +public export +scaleScale : (q1, q2 : Q) -> (g : Ctx) + -> ctxScale q1 (ctxScale q2 g) = ctxScale (qMul q1 q2) g +scaleScale q1 q2 Empty = Refl +scaleScale q1 q2 (Snoc g a q) = + rewrite scaleScale q1 q2 g in + rewrite qMulAssoc q1 q2 q in Refl + +------------------------------------------------------------ +-- AddCtx algebra +------------------------------------------------------------ + +||| Commutativity: `g` is symmetric in the two summands. +public export +acComm : AddCtx g1 g2 g -> AddCtx g2 g1 g +acComm ACEmpty = ACEmpty +acComm (ACSnoc a q1 q2 ac) = + rewrite qAddComm q1 q2 in ACSnoc a q2 q1 (acComm ac) + +||| Scaling distributes over an additive split. +public export +acScale : (q : Q) -> AddCtx g1 g2 g + -> AddCtx (ctxScale q g1) (ctxScale q g2) (ctxScale q g) +acScale q ACEmpty = ACEmpty +acScale q (ACSnoc a q1 q2 ac) = + rewrite qMulDistribL q q1 q2 in ACSnoc a (qMul q q1) (qMul q q2) (acScale q ac) + +||| Fusion: scaling the same context by `q1` and `q2` and adding +||| gives the context scaled by `qAdd q1 q2`. +public export +acScaleFuse : (q1, q2 : Q) -> (g : Ctx) + -> AddCtx (ctxScale q1 g) (ctxScale q2 g) (ctxScale (qAdd q1 q2) g) +acScaleFuse q1 q2 Empty = ACEmpty +acScaleFuse q1 q2 (Snoc g a q) = + rewrite qMulDistribR q1 q2 q in + ACSnoc a (qMul q1 q) (qMul q2 q) (acScaleFuse q1 q2 g) + +||| Quantity-level interchange (medial) law, derived from the +||| commutative-monoid laws already proven in `Quantity.idr`. +public export +qInterchange : (qa, qb, qc, qd : Q) + -> qAdd (qAdd qa qb) (qAdd qc qd) = qAdd (qAdd qa qc) (qAdd qb qd) +qInterchange qa qb qc qd = + -- (qa+qb)+(qc+qd) = qa+(qb+(qc+qd)) = qa+((qb+qc)+qd) + -- = qa+((qc+qb)+qd) = qa+(qc+(qb+qd)) + -- = (qa+qc)+(qb+qd) + rewrite qAddAssoc qa qb (qAdd qc qd) in + rewrite sym (qAddAssoc qb qc qd) in + rewrite qAddComm qb qc in + rewrite qAddAssoc qc qb qd in + rewrite sym (qAddAssoc qa qc (qAdd qb qd)) in + Refl + +||| Context-level interchange: regroup a 2x2 block of additive splits. +||| From `s1 = a+b`, `s2 = c+d`, `s3 = a+c`, `s4 = b+d`, `t = s3+s4` +||| conclude `t = s1+s2`. +public export +acInterchange : AddCtx a b s1 -> AddCtx c d s2 -> AddCtx a c s3 + -> AddCtx b d s4 -> AddCtx s3 s4 t -> AddCtx s1 s2 t +acInterchange ACEmpty ACEmpty ACEmpty ACEmpty ACEmpty = ACEmpty +acInterchange (ACSnoc ty qa qb ab) (ACSnoc _ qc qd cd) + (ACSnoc _ _ _ ac) (ACSnoc _ _ _ bd) (ACSnoc _ _ _ s34) = + rewrite sym (qInterchange qa qb qc qd) in + ACSnoc ty (qAdd qa qb) (qAdd qc qd) (acInterchange ab cd ac bd s34) + +||| Interchange in *splitting* form: given the two "row" sums +||| `s1 = a+b`, `s2 = c+d` and the total `t = s1+s2`, construct the +||| two "column" sums `s3 = a+c`, `s4 = b+d` together with the +||| witness `t = s3+s4`. The constructed contexts inherit their +||| types from the input derivations, so no external shape-matching +||| is needed. +public export +acSplit2 : AddCtx a b s1 -> AddCtx c d s2 -> AddCtx s1 s2 t + -> (s3 : Ctx ** s4 : Ctx ** + (AddCtx a c s3, AddCtx b d s4, AddCtx s3 s4 t)) +acSplit2 ACEmpty ACEmpty ACEmpty = (Empty ** Empty ** (ACEmpty, ACEmpty, ACEmpty)) +acSplit2 (ACSnoc ty qa qb ab) (ACSnoc _ qc qd cd) (ACSnoc _ _ _ s12) = + let (s3 ** s4 ** (ac, bd, s34)) = acSplit2 ab cd s12 in + ( Snoc s3 ty (qAdd qa qc) ** Snoc s4 ty (qAdd qb qd) ** + ( ACSnoc ty qa qc ac + , ACSnoc ty qb qd bd + , rewrite qInterchange qa qb qc qd in ACSnoc ty (qAdd qa qc) (qAdd qb qd) s34 )) + +||| Associativity (right-leaning): from `(a+b)+c` recover `a+(b+c)`. +||| Returns the middle sum together with both witnesses. +public export +acAssoc : (b, c : Ctx) -> AddCtx ab c abc -> AddCtx a b ab + -> (bc : Ctx ** (AddCtx b c bc, AddCtx a bc abc)) +acAssoc Empty Empty ACEmpty ACEmpty = (Empty ** (ACEmpty, ACEmpty)) +acAssoc (Snoc b ty qb) (Snoc c _ qc) (ACSnoc _ _ _ acABC) (ACSnoc _ qa _ acAB) = + let (bc ** (acBC, acAbc)) = acAssoc b c acABC acAB in + ((Snoc bc ty (qAdd qb qc)) ** + ( ACSnoc ty qb qc acBC + , rewrite qAddAssoc qa qb qc in ACSnoc ty qa (qAdd qb qc) acAbc )) +acAssoc Empty (Snoc _ _ _) ACEmpty _ impossible +acAssoc (Snoc _ _ _) Empty (ACSnoc _ _ _ _) _ impossible + +------------------------------------------------------------ +-- Context append (puts the second context's entries ON TOP) +------------------------------------------------------------ + +export infixl 6 +++ + +||| `g +++ d` — append `d` on top of `g`. A variable at position `n` +||| in `g` has index `n + ctxLen d` once `d` binders sit above it. +public export +(+++) : Ctx -> Ctx -> Ctx +g +++ Empty = g +g +++ (Snoc d a q) = Snoc (g +++ d) a q + +||| Length of an append. +public export +ctxLenAppend : (g, d : Ctx) -> ctxLen (g +++ d) = ctxLen d + ctxLen g +ctxLenAppend g Empty = Refl +ctxLenAppend g (Snoc d a q) = rewrite ctxLenAppend g d in Refl + +||| Appending distributes over an additive split: if the base +||| splits as `gB = gB1 + gB2` and the top splits as +||| `cross = cross1 + cross2`, then the append splits accordingly. +public export +acAppend : AddCtx gB1 gB2 gB -> AddCtx c1 c2 c + -> AddCtx (gB1 +++ c1) (gB2 +++ c2) (gB +++ c) +acAppend acB ACEmpty = acB +acAppend acB (ACSnoc a q1 q2 acC) = ACSnoc a q1 q2 (acAppend acB acC) + +||| Scaling commutes with append. +public export +scaleAppend : (q : Q) -> (g, d : Ctx) + -> ctxScale q (g +++ d) = (ctxScale q g) +++ (ctxScale q d) +scaleAppend q g Empty = Refl +scaleAppend q g (Snoc d a e) = rewrite scaleAppend q g d in Refl + +||| Local `Nat` injectivity / discreteness helpers (avoid Data.Nat). +public export +sInj : the Nat (S m) = S n -> m = n +sInj Refl = Refl + +public export +zNeqS : the Nat Z = S n -> Void +zNeqS Refl impossible + +public export +plusLeftCancelZ : (n, a, b : Nat) -> n + a = n + b -> a = b +plusLeftCancelZ Z a b prf = prf +plusLeftCancelZ (S n) a b prf = plusLeftCancelZ n a b (sInj prf) + +||| Split a context into its bottom `ctxLen g - ctxLen top` entries +||| and top `ctxLen top` entries (the latter shaped like `top`). +||| Recurses on `top`; the matching `Snoc` of `g` is forced by the +||| length equality. +public export +splitTop : (top : Ctx) -> (g : Ctx) + -> ctxLen g = ctxLen top + base + -> (gB : Ctx ** gC : Ctx ** (g = gB +++ gC, ctxLen gC = ctxLen top)) +splitTop Empty g lenEq = (g ** Empty ** (Refl, Refl)) +splitTop (Snoc top _ _) (Snoc g a e) lenEq = + let (gB ** gC ** (geq, lenC)) = splitTop top g (sInj lenEq) in + (gB ** Snoc gC a e ** (cong (\w => Snoc w a e) geq, cong S lenC)) +splitTop (Snoc top _ _) Empty lenEq = absurd (zNeqS lenEq) + +||| Scaling distributes over a (proven) append decomposition. +public export +scaleSplit : (q : Q) -> (gB, gC : Ctx) + -> ctxScale q (gB +++ gC) = (ctxScale q gB) +++ (ctxScale q gC) +scaleSplit q gB gC = scaleAppend q gB gC + +||| Scaling preserves length. +public export +scaleLen : (q : Q) -> (g : Ctx) -> ctxLen (ctxScale q g) = ctxLen g +scaleLen q Empty = Refl +scaleLen q (Snoc g a e) = cong S (scaleLen q g) + +||| An additive split preserves length (left). +public export +acLenL : AddCtx x y g -> ctxLen x = ctxLen g +acLenL ACEmpty = Refl +acLenL (ACSnoc _ _ _ ac) = cong S (acLenL ac) + +||| An additive split preserves length (right). +public export +acLenR : AddCtx x y g -> ctxLen y = ctxLen g +acLenR ACEmpty = Refl +acLenR (ACSnoc _ _ _ ac) = cong S (acLenR ac) + +||| Snoc injectivity helpers. +public export +snocInjTail : the Ctx (Snoc x1 t1 q1) = Snoc x2 t2 q2 -> x1 = x2 +snocInjTail Refl = Refl + +public export +snocInjTy : the Ctx (Snoc x1 t1 q1) = Snoc x2 t2 q2 -> t1 = t2 +snocInjTy Refl = Refl + +public export +snocInjQ : the Ctx (Snoc x1 t1 q1) = Snoc x2 t2 q2 -> q1 = q2 +snocInjQ Refl = Refl + +public export +cong3Snoc : x1 = x2 -> t1 = t2 -> q1 = q2 + -> the Ctx (Snoc x1 t1 q1) = Snoc x2 t2 q2 +cong3Snoc Refl Refl Refl = Refl + +||| Append injectivity when the top components have equal length. +public export +appendInjTop : {a, b : Ctx} -> (c1, c2 : Ctx) -> ctxLen c1 = ctxLen c2 + -> a +++ c1 = b +++ c2 -> (a = b, c1 = c2) +appendInjTop Empty Empty lenEq eq = (eq, Refl) +appendInjTop (Snoc c1 t1 q1) (Snoc c2 t2 q2) lenEq eq = + let recur = appendInjTop {a} {b} c1 c2 (sInj lenEq) (snocInjTail eq) in + ( fst recur + , cong3Snoc (snd recur) (snocInjTy eq) (snocInjQ eq) ) +appendInjTop Empty (Snoc _ _ _) lenEq eq = absurd (zNeqS lenEq) +appendInjTop (Snoc _ _ _) Empty lenEq eq = absurd (zNeqS (sym lenEq)) + +||| Recover the (unscaled) `Snoc`-then-append decomposition of `g` +||| from the same decomposition of its scaling `ctxScale q g`. Used +||| in the T-App / T-Let substitution cases, where the argument / +||| RHS context appears only in scaled form in the split. +public export +unscaleSnocAppend : (q : Q) -> (g : Ctx) -> (cross : Ctx) -> (at : Ty) + -> {sBB, sC : Ctx} -> {qa : Q} + -> ctxLen sC = ctxLen cross + -> ctxScale q g = (Snoc sBB at qa) +++ sC + -> ( gBB : Ctx ** qa' : Q ** gC : Ctx ** + ( g = (Snoc gBB at qa') +++ gC + , ctxLen gC = ctxLen cross + , sBB = ctxScale q gBB + , qa = qMul q qa' + , sC = ctxScale q gC )) +unscaleSnocAppend q g cross at lenSC eq = + let lenG : (ctxLen g = ctxLen cross + S (ctxLen sBB)) + := trans (sym (scaleLen q g)) + (trans (cong ctxLen eq) + (trans (ctxLenAppend (Snoc sBB at qa) sC) + (cong (\m => m + S (ctxLen sBB)) lenSC))) + (gBase ** gC ** (gEq, lenGC)) = splitTop cross g lenG + in case gBase of + Empty => absurd (zNeqS (lenGBaseNonZero Empty gC g gEq lenG lenGC)) + Snoc gBB at' qa' => + -- ctxScale q g = ctxScale q ((Snoc gBB at' qa') +++ gC) + -- = (Snoc (ctxScale q gBB) at' (qMul q qa')) +++ ctxScale q gC + -- match against (Snoc sBB at qa) +++ sC by appendInjTop. + let scEq : (ctxScale q g + = (Snoc (ctxScale q gBB) at' (qMul q qa')) +++ (ctxScale q gC)) + := trans (cong (ctxScale q) gEq) (scaleAppend q (Snoc gBB at' qa') gC) + combEq : ((Snoc sBB at qa) +++ sC + = (Snoc (ctxScale q gBB) at' (qMul q qa')) +++ (ctxScale q gC)) + := trans (sym eq) scEq + lenTopEq : (ctxLen sC = ctxLen (ctxScale q gC)) + := trans lenSC (trans (sym lenGC) (sym (scaleLen q gC))) + (headEq, tailEq) = appendInjTop sC (ctxScale q gC) lenTopEq combEq + -- headEq : Snoc sBB at qa = Snoc (ctxScale q gBB) at' (qMul q qa') + atEq : (at = at') := snocInjTy headEq + sbbEq : (sBB = ctxScale q gBB) := snocInjTail headEq + qaEq : (qa = qMul q qa') := snocInjQ headEq + in ( gBB ** qa' ** gC ** + ( rewrite atEq in gEq + , lenGC + , sbbEq + , qaEq + , tailEq ) ) + where + lenGBaseNonZero : (gBase : Ctx) -> (gC : Ctx) -> (g : Ctx) + -> g = gBase +++ gC -> ctxLen g = ctxLen cross + S (ctxLen sBB) + -> ctxLen gC = ctxLen cross -> ctxLen gBase = S (ctxLen sBB) + lenGBaseNonZero gBase gC g gEq lenG lenGC = + -- ctxLen g = ctxLen gC + ctxLen gBase = ctxLen cross + ctxLen gBase + -- and = ctxLen cross + S (ctxLen sBB); so ctxLen gBase = S (ctxLen sBB). + let l1 : (ctxLen g = ctxLen gC + ctxLen gBase) := rewrite gEq in ctxLenAppend gBase gC + l2 : (ctxLen cross + ctxLen gBase = ctxLen cross + S (ctxLen sBB)) + := trans (trans (sym (cong (\m => m + ctxLen gBase) lenGC)) (sym l1)) lenG + in plusLeftCancelZ (ctxLen cross) (ctxLen gBase) (S (ctxLen sBB)) l2 + +------------------------------------------------------------ +-- Inverting an additive split along an append +------------------------------------------------------------ + +||| Reconstruct the left summand of an additive split from the +||| (runtime) `AddCtx` value, plus a proof it equals the erased index. +public export +acLeft : {0 x : Ctx} -> {0 y : Ctx} -> {0 g : Ctx} -> AddCtx x y g -> Ctx +acLeft ACEmpty = Empty +acLeft (ACSnoc a q1 _ ac) = Snoc (acLeft ac) a q1 + +public export +acRight : {0 x : Ctx} -> {0 y : Ctx} -> {0 g : Ctx} -> AddCtx x y g -> Ctx +acRight ACEmpty = Empty +acRight (ACSnoc a _ q2 ac) = Snoc (acRight ac) a q2 + +public export +acLeftEq : (ac : AddCtx x y g) -> x = acLeft ac +acLeftEq ACEmpty = Refl +acLeftEq (ACSnoc a q1 _ ac) = cong (\w => Snoc w a q1) (acLeftEq ac) + +public export +acRightEq : (ac : AddCtx x y g) -> y = acRight ac +acRightEq ACEmpty = Refl +acRightEq (ACSnoc a _ q2 ac) = cong (\w => Snoc w a q2) (acRightEq ac) + +||| The reconstructed summands really do add to `g`. +public export +acRebuild : (ac : AddCtx x y g) -> AddCtx (acLeft ac) (acRight ac) g +acRebuild ACEmpty = ACEmpty +acRebuild (ACSnoc a q1 q2 ac) = ACSnoc a q1 q2 (acRebuild ac) + +||| Invert an additive split whose result is a `Snoc`. Recovers the +||| two summand tails, their head quantities (with `q = qAdd q1 q2`), +||| and the tail split — as runtime data plus equations, so the +||| caller can refine other hypotheses with the `q` equation. +public export +acSnocInv : {0 x : Ctx} -> {0 y : Ctx} -> {0 g : Ctx} -> {0 a : Ty} -> {0 q : Q} + -> AddCtx x y (Snoc g a q) + -> ( at : Ty ** xt : Ctx ** yt : Ctx ** qa1 : Q ** qa2 : Q ** + ( a = at + , x = Snoc xt at qa1 + , y = Snoc yt at qa2 + , q = qAdd qa1 qa2 + , AddCtx xt yt g )) +acSnocInv (ACSnoc a q1 q2 ac) = + ( a ** acLeft ac ** acRight ac ** q1 ** q2 ** + ( Refl + , cong (\w => Snoc w a q1) (acLeftEq ac) + , cong (\w => Snoc w a q2) (acRightEq ac) + , Refl + , acRebuild ac )) + +||| Decompose a split whose result is an append. Splitting +||| `AddCtx x y (gB +++ cross)` yields matching appends of `x` and +||| `y` together with splits of the base and the top. +public export +acAppendInv : {0 x : Ctx} -> {0 y : Ctx} -> {0 gB : Ctx} -> (cross : Ctx) + -> AddCtx x y (gB +++ cross) + -> ( xB : Ctx ** yB : Ctx ** xC : Ctx ** yC : Ctx ** + ( x = xB +++ xC + , y = yB +++ yC + , AddCtx xB yB gB + , AddCtx xC yC cross )) +acAppendInv Empty ac = + (acLeft ac ** acRight ac ** Empty ** Empty ** + (acLeftEq ac, acRightEq ac, acRebuild ac, ACEmpty)) +acAppendInv (Snoc cross _ _) (ACSnoc a qx qy ac') = + let (xB ** yB ** xC ** yC ** (ex, ey, acB, acC)) = acAppendInv cross ac' in + ( xB ** yB ** Snoc xC a qx ** Snoc yC a qy ** + ( cong (\w => Snoc w a qx) ex + , cong (\w => Snoc w a qy) ey + , acB + , ACSnoc a qx qy acC ) ) + +------------------------------------------------------------ +-- Additive zero identities (type-tracked, so no mismatch) +------------------------------------------------------------ + +||| Adding a zero context on the LEFT is the identity. +public export +addZeroLEq : IsZero z -> AddCtx z g g' -> g' = g +addZeroLEq IZEmpty ACEmpty = Refl +addZeroLEq (IZSnoc iz) (ACSnoc _ _ q2 ac) = + rewrite addZeroLEq iz ac in rewrite qAddZeroL q2 in Refl + +||| Adding a zero context on the RIGHT is the identity. +public export +addZeroREq : IsZero z -> AddCtx g z g' -> g' = g +addZeroREq IZEmpty ACEmpty = Refl +addZeroREq (IZSnoc iz) (ACSnoc _ q1 _ ac) = + rewrite addZeroREq iz ac in rewrite qAddZeroR q1 in Refl + +||| The sum of two zero contexts is zero. +public export +addZeroResult : IsZero z1 -> IsZero z2 -> AddCtx z1 z2 g -> IsZero g +addZeroResult IZEmpty IZEmpty ACEmpty = IZEmpty +addZeroResult (IZSnoc i1) (IZSnoc i2) (ACSnoc _ _ _ ac) = + IZSnoc (addZeroResult i1 i2 ac) + +------------------------------------------------------------ +-- IsZero and append +------------------------------------------------------------ + +||| Split a zero append into its two zero halves. +public export +isZeroAppendSplit : (d : Ctx) -> IsZero (g +++ d) -> (IsZero g, IsZero d) +isZeroAppendSplit Empty iz = (iz, IZEmpty) +isZeroAppendSplit (Snoc d a _) (IZSnoc iz) = + let (izg, izd) = isZeroAppendSplit d iz in (izg, IZSnoc izd) + +||| Rebuild a zero append from zero halves. +public export +isZeroAppendJoin : IsZero g -> IsZero d -> IsZero (g +++ d) +isZeroAppendJoin izg IZEmpty = izg +isZeroAppendJoin izg (IZSnoc izd) = IZSnoc (isZeroAppendJoin izg izd) + +------------------------------------------------------------ +-- Quantity-level ordering facts for the sub-context order +------------------------------------------------------------ + +||| A summand is below the sum: `q1 <= q1 + q2`. Proved by exhaustive +||| case split on the three-element semiring. +public export +qLeAddL : (q1, q2 : Q) -> qLe q1 (qAdd q1 q2) = True +qLeAddL Zero Zero = Refl +qLeAddL Zero One = Refl +qLeAddL Zero Omega = Refl +qLeAddL One Zero = Refl +qLeAddL One One = Refl +qLeAddL One Omega = Refl +qLeAddL Omega Zero = Refl +qLeAddL Omega One = Refl +qLeAddL Omega Omega = Refl + +||| Symmetric form: the right summand is below the sum, `q2 <= q1 + q2`. +public export +qLeAddR : (q1, q2 : Q) -> qLe q2 (qAdd q1 q2) = True +qLeAddR q1 q2 = rewrite qAddComm q1 q2 in qLeAddL q2 q1 + +||| `qAdd` is monotone in its first argument w.r.t. `qLe`. Proved by +||| exhaustive case split: where the hypothesis `qLe x y` is `False` +||| the case is discharged by `absurd`; the remaining cases hold +||| definitionally. +public export +qAddMono : (x, y, z : Q) -> qLe x y = True -> qLe (qAdd x z) (qAdd y z) = True +qAddMono Zero Zero z prf = qLeRefl (qAdd Zero z) +qAddMono Zero One z prf = qLeAddRefine z + where + qLeAddRefine : (z : Q) -> qLe (qAdd Zero z) (qAdd One z) = True + qLeAddRefine Zero = Refl + qLeAddRefine One = Refl + qLeAddRefine Omega = Refl +qAddMono Zero Omega z prf = qLeAddRefine z + where + qLeAddRefine : (z : Q) -> qLe (qAdd Zero z) (qAdd Omega z) = True + qLeAddRefine Zero = Refl + qLeAddRefine One = Refl + qLeAddRefine Omega = Refl +qAddMono One One z prf = qLeRefl (qAdd One z) +qAddMono One Omega z prf = qLeAddRefine z + where + qLeAddRefine : (z : Q) -> qLe (qAdd One z) (qAdd Omega z) = True + qLeAddRefine Zero = Refl + qLeAddRefine One = Refl + qLeAddRefine Omega = Refl +qAddMono Omega Omega z prf = qLeRefl (qAdd Omega z) +qAddMono One Zero z prf = absurd prf +qAddMono Omega Zero z prf = absurd prf +qAddMono Omega One z prf = absurd prf + +------------------------------------------------------------ +-- The sub-context order (pointwise `qLe`, same spine and types) +------------------------------------------------------------ + +||| `Weaker gp g` : `gp` is below `g` in the pointwise quantity order +||| (same spine, same per-position types, and every `gp` quantity is +||| `<=` the corresponding `g` quantity). This is the affine +||| sub-context order: a derivation typed in `gp` can be re-read as +||| living "inside" the larger resource budget `g`. +||| +||| `qp`, `q` and `a` are explicit RUNTIME arguments of `WkSnoc` +||| (following the same convention as `ACSnoc`/`THApp`): the typed +||| indices `gp`, `g`, the quantities and the per-position type are +||| erased, so the monotonicity lemmas (which must rebuild the shrunk +||| `AddCtx` and inspect quantities) need them retained at runtime. +public export +data Weaker : Ctx -> Ctx -> Type where + WkEmpty : Weaker Empty Empty + WkSnoc : (qp : Q) -> (q : Q) -> (a : Ty) + -> Weaker gp g -> (qLe qp q = True) -> Weaker (Snoc gp a qp) (Snoc g a q) + +||| Reflexivity: every context is `Weaker` than itself (via `qLeRefl`). +public export +weakerRefl : (g : Ctx) -> Weaker g g +weakerRefl Empty = WkEmpty +weakerRefl (Snoc g a q) = WkSnoc q q a (weakerRefl g) (qLeRefl q) + +||| Reflexivity recovered from a runtime additive split that produces +||| `g`. Used by the beta cases of preservation, where the redex's +||| context `g` is an erased index but an `AddCtx _ _ g` witness is in +||| hand: the substitution lemma types the reduct in exactly `g`, so +||| the affine conclusion is `Weaker g g`. +public export +weakerReflFromAdd : {0 g1, g2, g : Ctx} -> AddCtx g1 g2 g -> Weaker g g +weakerReflFromAdd ACEmpty = WkEmpty +weakerReflFromAdd (ACSnoc a q1 q2 ac) = + WkSnoc (qAdd q1 q2) (qAdd q1 q2) a (weakerReflFromAdd ac) (qLeRefl (qAdd q1 q2)) + +||| Recover the (erased) result context `g` of an additive split as a +||| RUNTIME value, packaged with the proof that it equals `g`. The beta +||| cases of preservation need this to give the affine existential a +||| runtime witness when the only handle on `g` is the `AddCtx`. +public export +acResult : {0 g1, g2, g : Ctx} -> AddCtx g1 g2 g -> (gr : Ctx ** gr = g) +acResult ACEmpty = (Empty ** Refl) +acResult (ACSnoc a q1 q2 ac) = + let (gr ** eq) = acResult ac in + (Snoc gr a (qAdd q1 q2) ** cong (\w => Snoc w a (qAdd q1 q2)) eq) + +||| The left summand of an additive split is below the sum. +public export +addCtxLeftWeaker : AddCtx g1 g2 g -> Weaker g1 g +addCtxLeftWeaker ACEmpty = WkEmpty +addCtxLeftWeaker (ACSnoc a q1 q2 ac) = + WkSnoc q1 (qAdd q1 q2) a (addCtxLeftWeaker ac) (qLeAddL q1 q2) + +||| The right summand of an additive split is below the sum. +public export +addCtxRightWeaker : AddCtx g1 g2 g -> Weaker g2 g +addCtxRightWeaker ACEmpty = WkEmpty +addCtxRightWeaker (ACSnoc a q1 q2 ac) = + WkSnoc q2 (qAdd q1 q2) a (addCtxRightWeaker ac) (qLeAddR q1 q2) + +||| `qMul` is monotone in its second argument: from `x <= y` conclude +||| `q*x <= q*y`. Discharged by case split, the `False` hypotheses +||| ruled out by `absurd`. +public export +qMulMono : (q, x, y : Q) -> qLe x y = True -> qLe (qMul q x) (qMul q y) = True +qMulMono Zero x y pf = Refl +qMulMono One x y pf = rewrite qMulOneL x in rewrite qMulOneL y in pf +qMulMono Omega Zero Zero pf = Refl +qMulMono Omega Zero One pf = Refl +qMulMono Omega Zero Omega pf = Refl +qMulMono Omega One One pf = Refl +qMulMono Omega One Omega pf = Refl +qMulMono Omega Omega Omega pf = Refl +qMulMono Omega One Zero pf = absurd pf +qMulMono Omega Omega Zero pf = absurd pf +qMulMono Omega Omega One pf = absurd pf + +||| Scaling is monotone in the sub-context order: scaling both sides of +||| a `Weaker` by the same quantity preserves it. +public export +scaleMono : {0 gp, g : Ctx} -> (q : Q) -> Weaker gp g + -> Weaker (ctxScale q gp) (ctxScale q g) +scaleMono q WkEmpty = WkEmpty +scaleMono q (WkSnoc qp qq a wk le) = + WkSnoc (qMul q qp) (qMul q qq) a (scaleMono q wk) (qMulMono q qp qq le) + +------------------------------------------------------------ +-- Monotonicity of additive splitting under `Weaker` +------------------------------------------------------------ + +||| `qAdd` monotone in its SECOND argument (mirror of `qAddMono`). +public export +qAddMonoR : (z, x, y : Q) -> qLe x y = True -> qLe (qAdd z x) (qAdd z y) = True +qAddMonoR z x y pf = + rewrite qAddComm z x in rewrite qAddComm z y in qAddMono x y z pf + +||| Congruence for the LEFT summand: if `g1p` is below `g1` and +||| `AddCtx g1 h g`, then re-splitting with the shrunk left summand +||| yields some `gOut` that is below `g`. The output split is built by +||| `ACSnoc` on the shared spine, and `Weaker` follows from +||| `qAddMono` at each position. public export -addEmptyInv : (x, y : Ctx) -> ctxAdd x y = Just Empty -> (x = Empty, y = Empty) -addEmptyInv Empty Empty _ = (Refl, Refl) -addEmptyInv Empty (Snoc _ _ _) Refl impossible -addEmptyInv (Snoc _ _ _) Empty Refl impossible -addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) prf with (ctxAdd g1 g2) - addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) Refl | Nothing impossible - addEmptyInv (Snoc g1 a1 q1) (Snoc g2 a2 q2) Refl | (Just _) impossible +addCtxMonoLeft : {0 g1p, g1, h, g : Ctx} + -> Weaker g1p g1 -> AddCtx g1 h g + -> (gOut : Ctx ** (AddCtx g1p h gOut, Weaker gOut g)) +addCtxMonoLeft WkEmpty ACEmpty = (Empty ** (ACEmpty, WkEmpty)) +addCtxMonoLeft (WkSnoc qp q a wk le) (ACSnoc _ _ q2 ac) = + let (gOut ** (acOut, wkOut)) = addCtxMonoLeft wk ac in + ( Snoc gOut a (qAdd qp q2) + ** ( ACSnoc a qp q2 acOut + , WkSnoc (qAdd qp q2) (qAdd q q2) a wkOut (qAddMono qp q q2 le) ) ) -||| Scaling a context to `Empty` means it was already `Empty`. +||| Congruence for the RIGHT summand, symmetric to `addCtxMonoLeft`. public export -scaleEmptyInv : (q : Q) -> (g : Ctx) -> ctxScale q g = Empty -> g = Empty -scaleEmptyInv q Empty _ = Refl -scaleEmptyInv q (Snoc _ _ _) Refl impossible +addCtxMonoRight : {0 hp, h, g1, g : Ctx} + -> Weaker hp h -> AddCtx g1 h g + -> (gOut : Ctx ** (AddCtx g1 hp gOut, Weaker gOut g)) +addCtxMonoRight WkEmpty ACEmpty = (Empty ** (ACEmpty, WkEmpty)) +addCtxMonoRight (WkSnoc qp q a wk le) (ACSnoc _ q1 _ ac) = + let (gOut ** (acOut, wkOut)) = addCtxMonoRight wk ac in + ( Snoc gOut a (qAdd q1 qp) + ** ( ACSnoc a q1 qp acOut + , WkSnoc (qAdd q1 qp) (qAdd q1 q) a wkOut (qAddMonoR q1 qp q le) ) ) diff --git a/docs/academic/formal-verification/solo-core/README.adoc b/docs/academic/formal-verification/solo-core/README.adoc index 6d18d1fc..f2f77ef7 100644 --- a/docs/academic/formal-verification/solo-core/README.adoc +++ b/docs/academic/formal-verification/solo-core/README.adoc @@ -25,18 +25,39 @@ records, arrays, modules, and the entire effect system. Those belong to *Duet* (traits + effects) and *Ensemble* (full language), which will be mechanized in later tracks. -== Proof Goals (Track F1, Weeks 1–12) +== Proof Goals (Track F1) — STATUS: PROVED . *Progress*: a closed, well-typed Solo term is either a value or - steps. -. *Preservation*: reduction preserves typing. -. *Affine preservation*: reduction preserves the quantity semiring - accounting — a term typed in context `Γ` steps to a term typed in - the same `Γ`, and `1`-quantity bindings are consumed exactly once. - -This file-set is the *week 1-2* deliverable: syntax, contexts, -typing judgement, and *statements* (not proofs) of progress and -preservation. + steps. — *proved* (`Soundness.progress`, total, hole-free). +. *Preservation* (affine): reduction preserves typing up to dropping + resources — the reduct is typed in a `Weaker` SUB-context `g' ≤ g` + (pointwise `qLe`, same shape/types). — *proved* + (`Soundness.preservation`). +. *Affine preservation*: same statement (`Soundness.affinePreservation`). + +All three are mechanically checked: `idris2 --check Soundness.idr` +exits 0, every definition is `total`, and there is no `believe_me`, +`assert_total`, `really_believe_me`, `postulate` or `?`-hole. + +[NOTE] +==== +*Why the conclusion is a sub-context, not the same `Γ`.* The original +week-1-2 statement asked for the reduct in the *same* `Γ` (and "`1` +consumed exactly once" — a *linear* phrasing). Mechanisation showed +that is *false* for the Solo core as designed: `TPair` introduces +multiplicatively (`AddCtx g1 g2 g`, resources split) but is eliminated +by the projections `Fst`/`Snd`. `Snd (Pair x y) → y` (with `x` linear) +leaves `y` typed in a *smaller* context — the projected-away component's +resources are dropped. Every β-rule preserves the context *exactly* +(via the substitution lemma); only the two projections shrink it. + +Per the owner decision (2026-06-15) this is resolved the *affine* way — +AffineScript is affine (the OCaml `q_le observed declared` check permits +under-use), so dropping is legitimate and the honest theorem is the +sub-context one above. The language is unchanged (split product + +projections + eager CBV kept). See the per-rung discussion in +`dev-notes/2026-06-15-affinescript-solo-core-preservation/`. +==== == Ground-Truth Rule @@ -47,13 +68,22 @@ QTT. When the Idris2 formalisation and `lib/quantity.ml` + `lib/typecheck.ml` disagree, *the OCaml implementation is ground truth* until an ADR is filed that explicitly reverses this. -Track F re-verifies weekly against Track A's test fixtures: - -* `examples/affine_basic.affine` -* `examples/affine_violation.affine` - -If the mechanization and the compiler diverge on these fixtures, the -proof is wrong, not the compiler. +Track F re-verifies against Track A's affine test fixtures (under +`test/e2e/fixtures/`): + +* `affine_let_valid_sugar.affine`, `linear_arrow.affine` — accepted. +* `linear_arrow_violation.affine`, + `slice_d_captured_linear_{param,let}_rejected.affine` — rejected. +* `affine_violation.affine` (`fn double_use(x) = x + x`) — *accepted* + via the surface `check` because `x` is unannotated (quantity ω; + `qAdd One One = Omega`); the linear double-use is exercised + *programmatically* by `test_quantity_affine_violation` in + `test/test_e2e.ml`. + +Verified 2026-06-15: the compiler accepts linear-used-once and +ω-used-many, rejects linear-used-twice — consistent with the proven +Solo rules. If the mechanization and the compiler ever diverge on +these fixtures, the proof is wrong, not the compiler. ==== == Files @@ -75,25 +105,45 @@ proof is wrong, not the compiler. | `Typing.idr` | QTT-style typing judgement `Has : Ctx -> Tm -> Ty -> Type`. - Rules only; no meta-theorems yet. + Split contexts of T-App/T-Pair/T-Case/T-Let are explicit `AddCtx` + premises; T-Var/T-Unit use an analysable `IsZero` premise. (Encoding + change from the statement-only version so the judgement is provable + in Idris2 — same set of derivations.) + +| `ContextLemmas.idr` +| The QTT context algebra: the inductive additive split `AddCtx` + (type-tracking, Maybe-free), `IsZero`, the scaling/commutativity/ + associativity/interchange laws (reusing `Quantity.idr`), and the + `Weaker` sub-context order with its monotonicity lemmas. + +| `Subst.idr` +| de Bruijn `shift` / single-variable `subst` / `subst0`. + +| `SubstLemma.idr` +| Weakening (`weakenAt`) + the QTT substitution lemma + (`substGen` / `substLemma0`), proved by induction on the body's + typing derivation, generalised over a `cross` context of crossed + binders. | `Soundness.idr` -| *Statements* of `progress` and `preservation` with - `?todo_progress` / `?todo_preservation` holes. Proofs are - weeks 3-12 work. +| `Value`, the CBV `Step` relation (16 rules, spec §4.2-4.3), and the + *proved* `progress` / `preservation` / `affinePreservation`. |=== == Status Block [source] ---- -Phase: Track F1, week 1-2 (syntax + statements) -Last sync: 2026-04-10 +Phase: Track F1 COMPLETE — progress + (affine) preservation proved +Last sync: 2026-06-15 OCaml refs: lib/quantity.ml, lib/types.ml, lib/typecheck.ml Spec refs: docs/spec.md §3.1-3.6 (Solo-relevant rules only) -Idris2 ver: 0.8.0 (verified locally) -Dangerous: none (no believe_me, no assert_total, no really_believe_me) -Holes: ?todo_progress, ?todo_preservation (intentional) +Idris2 ver: 0.8.0 (verified locally; idris2 --check Soundness.idr exit 0) +Dangerous: none (no believe_me / assert_total / really_believe_me / postulate) +Holes: none (all definitions total) +Decision: preservation is AFFINE (reduct in a Weaker sub-context); + split product + projections kept (owner decision 2026-06-15) +Check: just proof-check-idris2 ---- == Out of Scope (Tracks F2, F3, …) diff --git a/docs/academic/formal-verification/solo-core/Soundness.idr b/docs/academic/formal-verification/solo-core/Soundness.idr index c6b3a683..7f29c665 100644 --- a/docs/academic/formal-verification/solo-core/Soundness.idr +++ b/docs/academic/formal-verification/solo-core/Soundness.idr @@ -1,14 +1,18 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- --- Statements of the soundness theorems for the Solo core. +-- Soundness (progress + preservation) for the Solo core. -- --- This file deliberately contains NO PROOFS. The week-1-2 --- deliverable for Track F1 is the *statement* of progress and --- preservation; the actual derivations are weeks 3-12 work and --- will be filled in case-by-case. All theorems are left as --- explicit `?todo_...` holes so the file still typechecks as a --- declaration module. +-- Progress and preservation are now fully proved (no holes, no +-- dangerous primitives, total). The crux is the QTT substitution +-- lemma `SubstLemma.substLemma0`; preservation's beta cases are +-- direct corollaries of it, and the congruence cases rebuild the +-- same typing rule around the recursively-preserved subderivation. +-- +-- Under the SPLIT (multiplicative) product rule the conclusion of +-- preservation is now AFFINE: the reduct is typed in a `Weaker` +-- SUB-context, not necessarily the same context (projection of a +-- split pair discards one summand's resources). module Soundness @@ -18,6 +22,7 @@ import Context import ContextLemmas import Typing import Subst +import SubstLemma %default total @@ -35,123 +40,105 @@ data Value : Tm -> Type where VInr : Value t -> Value (Inr a t) ------------------------------------------------------------ --- Small-step reduction (declaration only) +-- Small-step reduction (call-by-value, left-to-right) ------------------------------------------------------------ --- --- We declare the relation `Step t t'` as a data family, but do --- NOT enumerate its constructors yet. The constructors will --- follow call-by-value, context-free beta/projection/case --- reduction. They are introduced alongside the progress / --- preservation proofs in weeks 3-6. -||| Call-by-value, left-to-right small-step reduction. The redex -||| rules (beta, projection, case, let) mirror `docs/spec.md` §4.3; -||| the congruence rules implement the evaluation contexts of -||| §4.2 (function before argument, left of a pair before right, -||| inside an injection, scrutinee before branch selection). We do -||| NOT reduce under a binder, so every `Lam` is a value. +||| `Step t t'` — one step of the CBV operational semantics. The +||| constructors mirror the reference interpreter `lib/interp.ml` +||| (left-to-right evaluation; beta/projection/case fire only on +||| values). public export data Step : Tm -> Tm -> Type where - - ------------------------------------------------------------ - -- beta / redex rules - ------------------------------------------------------------ - - ||| (fn(q x:a) => body) v → body[0 ↦ v] - SBeta : Value v - -> Step (App (Lam q a body) v) (subst0 body v) - - ||| fst (v1, v2) → v1 - SFstBeta : Value v1 -> Value v2 - -> Step (Fst (Pair v1 v2)) v1 - - ||| snd (v1, v2) → v2 - SSndBeta : Value v1 -> Value v2 - -> Step (Snd (Pair v1 v2)) v2 - - ||| case (inl v) of {l; r} → l[0 ↦ v] - SCaseL : Value v - -> Step (Case (Inl b v) tL tR) (subst0 tL v) - - ||| case (inr v) of {l; r} → r[0 ↦ v] - SCaseR : Value v - -> Step (Case (Inr a v) tL tR) (subst0 tR v) - - ||| let (q x) = v in body → body[0 ↦ v] - SLetBeta : Value v - -> Step (Let q v body) (subst0 body v) - - ------------------------------------------------------------ - -- congruence rules (evaluation contexts) - ------------------------------------------------------------ - - SApp1 : Step t1 t1' -> Step (App t1 t2) (App t1' t2) - SApp2 : Value v1 -> Step t2 t2' -> Step (App v1 t2) (App v1 t2') - SPair1 : Step t1 t1' -> Step (Pair t1 t2) (Pair t1' t2) - SPair2 : Value v1 -> Step t2 t2' -> Step (Pair v1 t2) (Pair v1 t2') - SFst : Step t t' -> Step (Fst t) (Fst t') - SSnd : Step t t' -> Step (Snd t) (Snd t') - SInl : Step t t' -> Step (Inl b t) (Inl b t') - SInr : Step t t' -> Step (Inr a t) (Inr a t') - SCase : Step s s' -> Step (Case s tL tR) (Case s' tL tR) - SLet1 : Step e e' -> Step (Let q e body) (Let q e' body) + -- application + SApp1 : Step t1 t1' -> Step (App t1 t2) (App t1' t2) + SApp2 : Value t1 -> Step t2 t2' -> Step (App t1 t2) (App t1 t2') + SBeta : Value v -> Step (App (Lam q a body) v) (subst0 body v) + -- pairs + SPair1 : Step t1 t1' -> Step (Pair t1 t2) (Pair t1' t2) + SPair2 : Value t1 -> Step t2 t2' -> Step (Pair t1 t2) (Pair t1 t2') + -- projections + SFst1 : Step t t' -> Step (Fst t) (Fst t') + SFstV : Value v1 -> Value v2 -> Step (Fst (Pair v1 v2)) v1 + SSnd1 : Step t t' -> Step (Snd t) (Snd t') + SSndV : Value v1 -> Value v2 -> Step (Snd (Pair v1 v2)) v2 + -- sums + SInl : Step t t' -> Step (Inl b t) (Inl b t') + SInr : Step t t' -> Step (Inr a t) (Inr a t') + -- case + SCase : Step t t' -> Step (Case t tL tR) (Case t' tL tR) + SCaseL : Value v -> Step (Case (Inl b v) tL tR) (subst0 tL v) + SCaseR : Value v -> Step (Case (Inr a v) tL tR) (subst0 tR v) + -- let + SLet1 : Step t1 t1' -> Step (Let q t1 t2) (Let q t1' t2) + SLetBeta : Value v -> Step (Let q v t2) (subst0 t2 v) ------------------------------------------------------------ -- Existential wrapper (no dependent pair imports needed) ------------------------------------------------------------ -||| Simple Sigma to avoid bringing in `Data.DPair` right now. The -||| reduct `t'` is erased (`0`): `StepsTo t` is the proposition -||| "there exists `t'` with `t` ⟶ `t'`", and the proofs never need -||| to compute the reduct as run-time data. +||| Simple Sigma to avoid bringing in `Data.DPair` right now. +||| +||| The reduct `t'` is an erased witness — `StepsTo t` is the +||| proposition "`t` can take a step". `progress` works over de +||| Bruijn terms that are erased typing-judgement indices, so the +||| reduct is recovered by unification with the `Step` proof rather +||| than carried at runtime. public export data StepsTo : Tm -> Type where - MkStepsTo : (0 t' : Tm) -> Step t t' -> StepsTo t + MkStepsTo : {0 t' : Tm} -> Step t t' -> StepsTo t ------------------------------------------------------------ --- Inversions used by progress +-- Empty context has no variables ------------------------------------------------------------ -||| The empty context binds no variables. -noEmptyVar : HasVar Empty n a -> Void -noEmptyVar (HVHere _ _) impossible -noEmptyVar (HVThere _ _) impossible - -||| Elimination forms are never values. -notValApp : Value (App x y) -> Void -notValApp VUnit impossible -notValApp VLam impossible -notValApp (VPair _ _) impossible -notValApp (VInl _) impossible -notValApp (VInr _) impossible - -notValFst : Value (Fst x) -> Void -notValFst VUnit impossible -notValFst VLam impossible -notValFst (VPair _ _) impossible -notValFst (VInl _) impossible -notValFst (VInr _) impossible - -notValSnd : Value (Snd x) -> Void -notValSnd VUnit impossible -notValSnd VLam impossible -notValSnd (VPair _ _) impossible -notValSnd (VInl _) impossible -notValSnd (VInr _) impossible - -notValCase : Value (Case s l r) -> Void -notValCase VUnit impossible -notValCase VLam impossible -notValCase (VPair _ _) impossible -notValCase (VInl _) impossible -notValCase (VInr _) impossible +||| `HasVar Empty n a` is uninhabited: neither `HVHere` nor +||| `HVThere` can produce the `Empty` context. +noVarInEmpty : HasVar Empty n a -> Void +noVarInEmpty HVHere impossible +noVarInEmpty HVThere impossible -notValLet : Value (Let q e b) -> Void -notValLet VUnit impossible -notValLet VLam impossible -notValLet (VPair _ _) impossible -notValLet (VInl _) impossible -notValLet (VInr _) impossible +------------------------------------------------------------ +-- Canonical-forms step builders +------------------------------------------------------------ +-- +-- Rather than returning the (erased) structure of the value, each +-- helper directly produces the reduction step, with the +-- non-canonical value shapes ruled out by the typing derivation. + +||| A value function applied to a value beta-reduces. Matching the +||| `Value` exposes the lambda; the reduct is recovered (erased) from +||| the `SBeta` step. The non-lambda value shapes contradict the +||| arrow-typing derivation. +appStep : Value t1 -> Has Empty t1 (TArr q a b) -> Value t2 -> StepsTo (App t1 t2) +appStep VLam _ vx = MkStepsTo (SBeta vx) +appStep VUnit thd vx impossible +appStep (VPair _ _) thd vx impossible +appStep (VInl _) thd vx impossible +appStep (VInr _) thd vx impossible + +||| `Fst` of a value of product type steps to its first component. +fstStep : Value t -> Has Empty t (TPair a b) -> StepsTo (Fst t) +fstStep (VPair vv1 vv2) _ = MkStepsTo (SFstV vv1 vv2) +fstStep VUnit thd impossible +fstStep VLam thd impossible +fstStep (VInl _) thd impossible +fstStep (VInr _) thd impossible + +||| `Snd` of a value of product type steps to its second component. +sndStep : Value t -> Has Empty t (TPair a b) -> StepsTo (Snd t) +sndStep (VPair vv1 vv2) _ = MkStepsTo (SSndV vv1 vv2) +sndStep VUnit thd impossible +sndStep VLam thd impossible +sndStep (VInl _) thd impossible +sndStep (VInr _) thd impossible + +||| `Case` on a value of sum type steps into the matching branch. +caseStep : Value t -> Has Empty t (TSum a b) -> StepsTo (Case t tL tR) +caseStep (VInl vu) _ = MkStepsTo (SCaseL vu) +caseStep (VInr vu) _ = MkStepsTo (SCaseR vu) +caseStep VUnit thd impossible +caseStep VLam thd impossible +caseStep (VPair _ _) thd impossible ------------------------------------------------------------ -- Progress @@ -160,125 +147,184 @@ notValLet (VInr _) impossible ||| Progress: a closed, well-typed Solo term is either a value ||| or can take a step. ||| -||| "Closed" means typed in the empty context — `Empty` has no -||| `HasVar` inhabitants (`noEmptyVar`), so there are no free de -||| Bruijn indices. The proof is by induction on the typing -||| derivation; the splitting rules first invert their context -||| equation to learn that every sub-derivation is itself closed, -||| then recurse left-to-right per the call-by-value strategy. +||| "Closed" means typed in the empty context — there are no +||| free de Bruijn indices because `Empty` has no `HVHere` / +||| `HVThere` inhabitants. public export progress : Has Empty t a -> Either (Value t) (StepsTo t) - -progress (THVar v) = absurd (noEmptyVar v) - +progress (THVar hv) = absurd (noVarInEmpty hv) progress (THUnit _) = Left VUnit - -progress (THLam _) = Left VLam - -progress (THInl d) = case progress d of - Right (MkStepsTo _ st) => Right (MkStepsTo _ (SInl st)) - Left dval => Left (VInl dval) - -progress (THInr d) = case progress d of - Right (MkStepsTo _ st) => Right (MkStepsTo _ (SInr st)) - Left dval => Left (VInr dval) - -progress (THApp g1 g2 q f x prf) = - let (e1, esc) = addEmptyInv g1 (ctxScale q g2) prf - e2 = scaleEmptyInv q g2 esc in - case (e1, e2) of - (Refl, Refl) => case progress f of - Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SApp1 st1)) - Left fval => case progress x of - Right (MkStepsTo _ st2) => Right (MkStepsTo _ (SApp2 fval st2)) - Left xval => case f of - THLam _ => Right (MkStepsTo _ (SBeta xval)) - THVar v => absurd (noEmptyVar v) - THApp _ _ _ _ _ _ => absurd (notValApp fval) - THFst _ => absurd (notValFst fval) - THSnd _ => absurd (notValSnd fval) - THCase _ _ _ _ _ _ => absurd (notValCase fval) - THLet _ _ _ _ _ _ => absurd (notValLet fval) - -progress (THPair g1 g2 p1 p2 prf) = - let (e1, e2) = addEmptyInv g1 g2 prf in - case (e1, e2) of - (Refl, Refl) => case progress p1 of - Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SPair1 st1)) - Left v1 => case progress p2 of - Right (MkStepsTo _ st2) => Right (MkStepsTo _ (SPair2 v1 st2)) - Left v2 => Left (VPair v1 v2) - -progress (THFst d) = case progress d of - Right (MkStepsTo _ st) => Right (MkStepsTo _ (SFst st)) - Left dval => case d of - THPair _ _ _ _ _ => case dval of - VPair v1 v2 => Right (MkStepsTo _ (SFstBeta v1 v2)) - THVar v => absurd (noEmptyVar v) - THApp _ _ _ _ _ _ => absurd (notValApp dval) - THFst _ => absurd (notValFst dval) - THSnd _ => absurd (notValSnd dval) - THCase _ _ _ _ _ _ => absurd (notValCase dval) - THLet _ _ _ _ _ _ => absurd (notValLet dval) - -progress (THSnd d) = case progress d of - Right (MkStepsTo _ st) => Right (MkStepsTo _ (SSnd st)) - Left dval => case d of - THPair _ _ _ _ _ => case dval of - VPair v1 v2 => Right (MkStepsTo _ (SSndBeta v1 v2)) - THVar v => absurd (noEmptyVar v) - THApp _ _ _ _ _ _ => absurd (notValApp dval) - THFst _ => absurd (notValFst dval) - THSnd _ => absurd (notValSnd dval) - THCase _ _ _ _ _ _ => absurd (notValCase dval) - THLet _ _ _ _ _ _ => absurd (notValLet dval) - -progress (THCase g1 g2 s l r prf) = - let (e1, e2) = addEmptyInv g1 g2 prf in - case (e1, e2) of - (Refl, Refl) => case progress s of - Right (MkStepsTo _ st) => Right (MkStepsTo _ (SCase st)) - Left sval => case s of - THInl _ => case sval of VInl v => Right (MkStepsTo _ (SCaseL v)) - THInr _ => case sval of VInr v => Right (MkStepsTo _ (SCaseR v)) - THVar v => absurd (noEmptyVar v) - THApp _ _ _ _ _ _ => absurd (notValApp sval) - THFst _ => absurd (notValFst sval) - THSnd _ => absurd (notValSnd sval) - THCase _ _ _ _ _ _ => absurd (notValCase sval) - THLet _ _ _ _ _ _ => absurd (notValLet sval) - -progress (THLet g1 g2 q d1 d2 prf) = - let (esc, e2) = addEmptyInv (ctxScale q g1) g2 prf - e1 = scaleEmptyInv q g1 esc in - case (e1, e2) of - (Refl, Refl) => case progress d1 of - Right (MkStepsTo _ st1) => Right (MkStepsTo _ (SLet1 st1)) - Left v1 => Right (MkStepsTo _ (SLetBeta v1)) +progress (THLam _ _ _) = Left VLam +progress (THApp {t1} {t2} {g1} {a} {b} q g2 fD xD ac) = + -- the application is closed (typed in Empty), so the function + -- context g1 and the scaled argument context are both Empty. + let (eg1, escg2) = addEmptyInv ac + eg2 : (g2 = Empty) := scaleEmptyInv g2 escg2 + fD' : (Has Empty t1 (TArr q a b)) := rewrite sym eg1 in fD + xD' : (Has Empty t2 a) := rewrite sym eg2 in xD + in case progress fD' of + Right (MkStepsTo st) => Right (MkStepsTo (SApp1 st)) + Left vf => case progress xD' of + Right (MkStepsTo st) => Right (MkStepsTo (SApp2 vf st)) + Left vx => Right (appStep vf fD' vx) +progress (THPair {t1} {t2} {a=pa} {b=pb} g1 g2 t1D t2D ac) = + -- the pair is closed (typed in Empty), so the SPLIT puts both + -- component contexts at Empty. + let (eg1, eg2) = addEmptyInv ac + t1D' : (Has Empty t1 pa) := rewrite sym eg1 in t1D + t2D' : (Has Empty t2 pb) := rewrite sym eg2 in t2D + in case progress t1D' of + Right (MkStepsTo st) => Right (MkStepsTo (SPair1 st)) + Left v1 => case progress t2D' of + Right (MkStepsTo st) => Right (MkStepsTo (SPair2 v1 st)) + Left v2 => Left (VPair v1 v2) +progress (THFst pD) = + case progress pD of + Right (MkStepsTo st) => Right (MkStepsTo (SFst1 st)) + Left vp => Right (fstStep vp pD) +progress (THSnd pD) = + case progress pD of + Right (MkStepsTo st) => Right (MkStepsTo (SSnd1 st)) + Left vp => Right (sndStep vp pD) +progress (THInl pD) = + case progress pD of + Right (MkStepsTo st) => Right (MkStepsTo (SInl st)) + Left vp => Left (VInl vp) +progress (THInr pD) = + case progress pD of + Right (MkStepsTo st) => Right (MkStepsTo (SInr st)) + Left vp => Left (VInr vp) +progress (THCase {t} a b g1 sD lD rD ac) = + let (eg1, _) = addEmptyInv ac + sD' : (Has Empty t (TSum a b)) := rewrite sym eg1 in sD + in case progress sD' of + Right (MkStepsTo st) => Right (MkStepsTo (SCase st)) + Left vs => Right (caseStep vs sD') +progress (THLet {t1} q a g1 e1D e2D ac) = + let (escg1, _) = addEmptyInv ac + eg1 : (g1 = Empty) := scaleEmptyInv g1 escg1 + e1D' : (Has Empty t1 a) := rewrite sym eg1 in e1D + in case progress e1D' of + Right (MkStepsTo st) => Right (MkStepsTo (SLet1 st)) + Left v1 => Right (MkStepsTo (SLetBeta v1)) ------------------------------------------------------------ -- Preservation ------------------------------------------------------------ -||| Preservation: reduction preserves typing in the same -||| context. The fact that the context is preserved (not merely -||| "there exists some g'") is the affine-accounting content of -||| the theorem — if `t` could run while duplicating a linear -||| variable, the reduct would require a *larger* context. +||| Preservation (AFFINE reading): reduction preserves typing in a +||| `Weaker` SUB-context. Concretely, if `t : a` in `g` and `t` steps +||| to `tp`, there is a context `gp` with `Weaker gp g` (every +||| quantity `<=` the corresponding quantity of `g`) such that +||| `tp : a` in `gp`. +||| +||| The sub-context content is the affine-accounting heart of the +||| theorem under the SPLIT (multiplicative) product: a projection +||| `Fst (Pair v1 v2)` discards `v2` and so its reduct `v1` lives in +||| the LEFT summand `g1`, a proper sub-context of the whole `g`. A +||| same-context statement would be FALSE for this fragment; the +||| `Weaker` existential is exactly the right weakening. +||| +||| * Congruence rules recurse, then re-split the SAME rule around the +||| shrunk summand via `addCtxMonoLeft` / `addCtxMonoRight` (with +||| `scaleMono` for the scaled summands of `THApp` / `THLet`), +||| concluding `Weaker` by quantity monotonicity. Single-context +||| congruences (`Fst`/`Snd`/`Inl`/`Inr`) thread the `Weaker` through +||| unchanged. +||| * Beta rules invoke the QTT substitution lemma `substLemma0`, which +||| types the reduct in EXACTLY `g`; the conclusion is `Weaker g g` +||| (recovered from the in-hand `AddCtx _ _ g` via `weakerReflFromAdd`). +||| * The projection betas return the relevant summand of the SPLIT +||| pair: `g1` (with `addCtxLeftWeaker ac`) for `Fst`, `g2` +||| (`addCtxRightWeaker ac`) for `Snd`. public export -preservation : Has g t a -> Step t t' -> Has g t' a -preservation _ _ = ?todo_preservation +preservation : Has g t a -> Step t tp -> (gp : Ctx ** (Weaker gp g, Has gp tp a)) +-- congruence: split-context rules re-split around the preserved subderivation +preservation (THApp {g1} q g2 fD xD ac) (SApp1 st) = + let (g1p ** (wk, fD')) = preservation fD st + (gOut ** (acOut, wkOut)) = addCtxMonoLeft wk ac + in (gOut ** (wkOut, THApp q g2 fD' xD acOut)) +preservation (THApp {g1} q g2 fD xD ac) (SApp2 _ st) = + let (g2p ** (wk, xD')) = preservation xD st + (gOut ** (acOut, wkOut)) = addCtxMonoRight (scaleMono q wk) ac + in (gOut ** (wkOut, THApp q g2p fD xD' acOut)) +preservation (THPair g1 g2 t1D t2D ac) (SPair1 st) = + let (g1p ** (wk, t1D')) = preservation t1D st + (gOut ** (acOut, wkOut)) = addCtxMonoLeft wk ac + in (gOut ** (wkOut, THPair g1p g2 t1D' t2D acOut)) +preservation (THPair g1 g2 t1D t2D ac) (SPair2 _ st) = + let (g2p ** (wk, t2D')) = preservation t2D st + (gOut ** (acOut, wkOut)) = addCtxMonoRight wk ac + in (gOut ** (wkOut, THPair g1 g2p t1D t2D' acOut)) +preservation (THCase a b g1 sD lD rD ac) (SCase st) = + let (g1p ** (wk, sD')) = preservation sD st + (gOut ** (acOut, wkOut)) = addCtxMonoLeft wk ac + in (gOut ** (wkOut, THCase a b g1p sD' lD rD acOut)) +preservation (THLet q at g1 e1D e2D ac) (SLet1 st) = + let (g1p ** (wk, e1D')) = preservation e1D st + (gOut ** (acOut, wkOut)) = addCtxMonoLeft (scaleMono q wk) ac + in (gOut ** (wkOut, THLet q at g1p e1D' e2D acOut)) +-- congruence: single-context rules thread Weaker directly +preservation (THFst pD) (SFst1 st) = + let (gp ** (wk, pD')) = preservation pD st in (gp ** (wk, THFst pD')) +preservation (THSnd pD) (SSnd1 st) = + let (gp ** (wk, pD')) = preservation pD st in (gp ** (wk, THSnd pD')) +preservation (THInl pD) (SInl st) = + let (gp ** (wk, pD')) = preservation pD st in (gp ** (wk, THInl pD')) +preservation (THInr pD) (SInr st) = + let (gp ** (wk, pD')) = preservation pD st in (gp ** (wk, THInr pD')) +-- projection beta on the SPLIT product: return the relevant summand +preservation (THFst pD) (SFstV _ _) = + case pD of + THPair g1 g2 t1D t2D ac => (g1 ** (addCtxLeftWeaker ac, t1D)) +preservation (THSnd pD) (SSndV _ _) = + case pD of + THPair g1 g2 t1D t2D ac => (g2 ** (addCtxRightWeaker ac, t2D)) +-- function beta: substLemma0 types the reduct in exactly g +preservation (THApp {g} q g2 fD xD ac) (SBeta _) = + case fD of + THLam q a fBodyD => + -- fBodyD : Has (Snoc g1 a q) body bt ; xD : Has g2 v a ; + -- ac : AddCtx g1 (ctxScale q g2) g. + let (gr ** geq) = acResult ac in + (gr ** ( rewrite geq in weakerReflFromAdd ac + , rewrite geq in substLemma0 g2 fBodyD xD ac )) +-- let beta +preservation (THLet {g} q at g1 e1D e2D ac) (SLetBeta _) = + -- e2D : Has (Snoc g2 at q) body bt ; e1D : Has g1 v at ; + -- ac : AddCtx (ctxScale q g1) g2 g. Need AddCtx g2 (ctxScale q g1) g. + let (gr ** geq) = acResult ac in + (gr ** ( rewrite geq in weakerReflFromAdd ac + , rewrite geq in substLemma0 g1 e2D e1D (acComm ac) )) +-- case beta +preservation (THCase {g} {g2} a b g1 sD lD rD ac) (SCaseL _) = + case sD of + THInl vD => + -- vD : Has g1 v a ; lD : Has (Snoc g2 a One) tL c ; + -- ac : AddCtx g1 g2 g. Need AddCtx g2 (ctxScale One g1) g. + let acOut : (AddCtx g2 (ctxScale One g1) g) + := rewrite scaleOne g1 in acComm ac + (gr ** geq) = acResult ac + in (gr ** ( rewrite geq in weakerReflFromAdd ac + , rewrite geq in substLemma0 g1 lD vD acOut )) +preservation (THCase {g} {g2} a b g1 sD lD rD ac) (SCaseR _) = + case sD of + THInr vD => + let acOut : (AddCtx g2 (ctxScale One g1) g) + := rewrite scaleOne g1 in acComm ac + (gr ** geq) = acResult ac + in (gr ** ( rewrite geq in weakerReflFromAdd ac + , rewrite geq in substLemma0 g1 rD vD acOut )) ------------------------------------------------------------ -- Affine preservation (corollary) ------------------------------------------------------------ -||| Affine preservation: if a term is well-typed with every -||| binding at quantity `One` or `Zero` and it steps, the reduct -||| is still well-typed in the same context. For Solo this is a -||| direct corollary of `preservation` above (the preserved -||| context already carries the quantity accounting), and is -||| stated here only for documentation. +||| Affine preservation: identical to `preservation` — under the SPLIT +||| product the affine sub-context existential IS the preservation +||| statement (the `Weaker` witness carries the quantity accounting: +||| every reduct quantity is `<=` the original). Kept as a named +||| corollary for documentation and downstream reference. public export -affinePreservation : Has g t a -> Step t t' -> Has g t' a +affinePreservation : Has g t a -> Step t tp -> (gp : Ctx ** (Weaker gp g, Has gp tp a)) affinePreservation = preservation diff --git a/docs/academic/formal-verification/solo-core/Subst.idr b/docs/academic/formal-verification/solo-core/Subst.idr index 9b912c31..0ae63bc0 100644 --- a/docs/academic/formal-verification/solo-core/Subst.idr +++ b/docs/academic/formal-verification/solo-core/Subst.idr @@ -1,18 +1,18 @@ -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- --- De Bruijn shifting and single-variable substitution for the Solo --- core. These are the term-level operations that the small-step --- reduction relation (Soundness.idr) uses in its beta/let/case rules, --- and that the substitution lemma (SubstLemma.idr) proves type-safe. +-- de Bruijn shifting and substitution for the Solo core. -- --- The formulation is the standard call-by-value de Bruijn one --- (cf. TAPL ch. 6): `shift c t` lifts every free variable index >= c --- by one; `subst j s t` replaces variable `j` by `s` inside `t`, --- decrementing the free variables above `j` and lifting `s` past each --- binder it crosses. `subst0` is the index-0 instance used by every --- beta reduction. Everything is structurally recursive, so `%default --- total` holds with no `assert_total`. +-- Convention (matching Typing.idr's HasVar): `Var Z` is the +-- innermost (top-of-snoc) binding; descending under a binder +-- increments indices. +-- +-- * `shift d c t` — add `d` to every `Var` index >= cutoff `c`. +-- * `subst j s t` — replace `Var j` by `s`, decrement `Var k` +-- for `k > j`, leave `Var k` for `k < j`. +-- Going under a binder bumps `j` and shifts +-- `s` up by one. +-- * `subst0 t v` — the top-level beta substitution `t[v/0]`. module Subst @@ -21,74 +21,85 @@ import Syntax %default total ------------------------------------------------------------ --- Variable shifting +-- Index shifting helpers ------------------------------------------------------------ -||| `shiftVar c k` lifts a single de Bruijn index: indices `< c` are -||| left alone (they are bound by binders crossed since the cutoff), -||| indices `>= c` are incremented (they are free past the cutoff). +||| `shiftVar d c n`: bump a single de Bruijn index `n` by `d` if it +||| is at or above the cutoff `c`. +||| +||| Defined by structural recursion on the cutoff and index together +||| (rather than via a `Bool` test) so that it reduces cleanly when +||| the cutoff is built up `Snoc`-by-`Snoc` in the proofs, and so +||| `shiftVar 1 c` computes a literal `S _` definitionally. public export -shiftVar : (c : Nat) -> (k : Nat) -> Nat -shiftVar Z k = S k -shiftVar (S c) Z = Z -shiftVar (S c) (S k) = S (shiftVar c k) +shiftVar : Nat -> Nat -> Nat -> Nat +shiftVar d Z n = d + n +shiftVar d (S c) Z = Z +shiftVar d (S c) (S n) = S (shiftVar d c n) -||| `shift c t` lifts every free variable of `t` whose index is `>= c`. -||| The cutoff increases by one under each binder. +------------------------------------------------------------ +-- Term shifting +------------------------------------------------------------ + +||| `shift d c t` — increment every free variable of `t` (index +||| >= `c`) by `d`. Binders raise the cutoff. public export -shift : (c : Nat) -> Tm -> Tm -shift c (Var k) = Var (shiftVar c k) -shift c UnitT = UnitT -shift c (Lam q a t) = Lam q a (shift (S c) t) -shift c (App t1 t2) = App (shift c t1) (shift c t2) -shift c (Pair t1 t2) = Pair (shift c t1) (shift c t2) -shift c (Fst t) = Fst (shift c t) -shift c (Snd t) = Snd (shift c t) -shift c (Inl b t) = Inl b (shift c t) -shift c (Inr a t) = Inr a (shift c t) -shift c (Case s l r) = Case (shift c s) (shift (S c) l) (shift (S c) r) -shift c (Let q e b) = Let q (shift c e) (shift (S c) b) +shift : Nat -> Nat -> Tm -> Tm +shift d c (Var n) = Var (shiftVar d c n) +shift d c UnitT = UnitT +shift d c (Lam q a t) = Lam q a (shift d (S c) t) +shift d c (App t1 t2) = App (shift d c t1) (shift d c t2) +shift d c (Pair t1 t2) = Pair (shift d c t1) (shift d c t2) +shift d c (Fst t) = Fst (shift d c t) +shift d c (Snd t) = Snd (shift d c t) +shift d c (Inl b t) = Inl b (shift d c t) +shift d c (Inr a t) = Inr a (shift d c t) +shift d c (Case t tL tR) = + Case (shift d c t) (shift d (S c) tL) (shift d (S c) tR) +shift d c (Let q t1 t2) = Let q (shift d c t1) (shift d (S c) t2) ------------------------------------------------------------ --- Single-variable substitution +-- Substitution at an index ------------------------------------------------------------ -||| `substVar j k s` is the variable case of substitution: replace -||| index `k` while substituting for index `j` with `s`. -||| -||| * `k < j` — a more recently bound variable, unchanged. -||| * `k = j` — the substituted variable; yields `s` lifted past the -||| `j` binders crossed to reach this occurrence. -||| * `k > j` — a free variable above the hole, decremented by one -||| (its binder is gone). +||| `substVar j s n` — the result of substituting `s` for the +||| variable `j` inside the single occurrence `Var n`. ||| -||| The single `shift 0` in the `S j / S k` case threads the -||| past-binder lifting through the recursion, so callers of `subst` -||| do *not* pre-shift `s` when descending under a binder. +||| `n < j` : untouched. +||| `n == j` : becomes `s`. +||| `n > j` : decremented (the bound variable disappears). public export -substVar : (j : Nat) -> (k : Nat) -> (s : Tm) -> Tm -substVar Z Z s = s -substVar Z (S k) s = Var k -substVar (S j) Z s = Var Z -substVar (S j) (S k) s = shift 0 (substVar j k s) +substVar : Nat -> Tm -> Nat -> Tm +substVar Z s Z = s +substVar Z s (S k) = Var k +substVar (S j) s Z = Var Z +substVar (S j) s (S k) = shift 1 0 (substVar j s k) -||| `subst j s t` replaces the free variable `j` in `t` by `s`. +||| `subst j s t` — substitute `s` for the variable with index `j` +||| in `t`, lowering the indices above `j`. +||| +||| The substituted term `s` is NOT pre-shifted when descending +||| under a binder: instead `substVar` re-shifts the substituted +||| value by exactly the binder-depth at which it lands (each `S/S` +||| step in `substVar` applies one `shift 1 0`). This keeps the two +||| operations in lock-step and avoids double-counting. public export -subst : (j : Nat) -> (s : Tm) -> Tm -> Tm -subst j s (Var k) = substVar j k s -subst j s UnitT = UnitT -subst j s (Lam q a t) = Lam q a (subst (S j) s t) -subst j s (App t1 t2) = App (subst j s t1) (subst j s t2) -subst j s (Pair t1 t2) = Pair (subst j s t1) (subst j s t2) -subst j s (Fst t) = Fst (subst j s t) -subst j s (Snd t) = Snd (subst j s t) -subst j s (Inl b t) = Inl b (subst j s t) -subst j s (Inr a t) = Inr a (subst j s t) -subst j s (Case sc l r) = Case (subst j s sc) (subst (S j) s l) (subst (S j) s r) -subst j s (Let q e b) = Let q (subst j s e) (subst (S j) s b) +subst : Nat -> Tm -> Tm -> Tm +subst j s (Var n) = substVar j s n +subst j s UnitT = UnitT +subst j s (Lam q a t) = Lam q a (subst (S j) s t) +subst j s (App t1 t2) = App (subst j s t1) (subst j s t2) +subst j s (Pair t1 t2) = Pair (subst j s t1) (subst j s t2) +subst j s (Fst t) = Fst (subst j s t) +subst j s (Snd t) = Snd (subst j s t) +subst j s (Inl b t) = Inl b (subst j s t) +subst j s (Inr a t) = Inr a (subst j s t) +subst j s (Case t tL tR) = + Case (subst j s t) (subst (S j) s tL) (subst (S j) s tR) +subst j s (Let q t1 t2) = + Let q (subst j s t1) (subst (S j) s t2) -||| Substitute for the most-recently-bound variable (index 0). This is -||| the operation performed by every beta-style reduction. +||| Top-level beta substitution `t[v/0]`. public export subst0 : Tm -> Tm -> Tm -subst0 body v = subst Z v body +subst0 t v = subst Z v t diff --git a/docs/academic/formal-verification/solo-core/SubstLemma.idr b/docs/academic/formal-verification/solo-core/SubstLemma.idr new file mode 100644 index 00000000..2781e33b --- /dev/null +++ b/docs/academic/formal-verification/solo-core/SubstLemma.idr @@ -0,0 +1,478 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The QTT substitution lemma for the Solo core. +-- +-- This module supplies the single load-bearing lemma behind +-- preservation: substituting a value for a bound variable preserves +-- typing, with the contexts combining exactly as the QTT semiring +-- prescribes (`Γ + q·Δ`). It is proved by induction on the typing +-- derivation of the body, generalised over a `cross` context of +-- binders crossed since the substituted variable, so the depth +-- bookkeeping is explicit. +-- +-- Two supporting weakening lemmas come first: +-- * `weakenVar` / `weakenAt` — insert an unused (Zero) binder at +-- a given depth, shifting free variables accordingly; +-- * `substVarLemma` — the variable case of substitution. + +module SubstLemma + +import Quantity +import Syntax +import Context +import ContextLemmas +import Typing +import Subst + +%default total + +------------------------------------------------------------ +-- Variable weakening: insert one Zero binder at depth ctxLen cross +------------------------------------------------------------ + +||| Inserting an unused binding `b` (quantity `Zero`) at depth +||| `ctxLen cross` shifts the variable index by one above that depth +||| and preserves the lookup. +public export +weakenVar : (cross : Ctx) + -> {0 g : Ctx} -> {0 n : Nat} -> {0 bt : Ty} + -> HasVar (g +++ cross) n bt + -> (bn : Ty) + -> HasVar ((Snoc g bn Zero) +++ cross) (shiftVar 1 (ctxLen cross) n) bt +weakenVar Empty hv bn = HVThere hv +weakenVar (Snoc cross _ _) (HVHere iz) bn = + let (izg, izc) = isZeroAppendSplit cross iz in + HVHere (isZeroAppendJoin (IZSnoc izg) izc) +weakenVar (Snoc cross _ _) (HVThere hv') bn = + HVThere (weakenVar cross hv' bn) + +||| Algebraic identity used to reshape the scaled argument context in +||| the T-App weakening case. +public export +scaledArgEq : (q : Q) -> (g2B, g2C : Ctx) -> (bn : Ty) -> (sB, sC : Ctx) + -> sB = ctxScale q g2B -> sC = ctxScale q g2C + -> ctxScale q ((Snoc g2B bn Zero) +++ g2C) = (Snoc sB bn Zero) +++ sC +scaledArgEq q g2B g2C bn sB sC eSB eSC = + rewrite eSB in rewrite eSC in + rewrite scaleAppend q (Snoc g2B bn Zero) g2C in + rewrite qMulZeroR q in Refl + +------------------------------------------------------------ +-- Term weakening: insert one Zero binder at depth ctxLen cross +------------------------------------------------------------ + +||| Insert an unused binding `b` (quantity `Zero`) at depth +||| `ctxLen cross` into the typing context, shifting the term's free +||| variables above that depth. Proved by induction on the typing +||| derivation. +public export +weakenAt : (cross : Ctx) + -> {0 g : Ctx} -> {0 t : Tm} -> {0 bt : Ty} + -> Has (g +++ cross) t bt + -> (bn : Ty) + -> Has ((Snoc g bn Zero) +++ cross) (shift 1 (ctxLen cross) t) bt +weakenAt cross (THVar hv) bn = THVar (weakenVar cross hv bn) +weakenAt cross (THUnit iz) bn = + let (izg, izc) = isZeroAppendSplit cross iz in + THUnit (isZeroAppendJoin (IZSnoc izg) izc) +weakenAt cross (THLam q a bodyD) bn = + -- body typed in Snoc (g+++cross) a q = g +++ (Snoc cross a q) + THLam q a (weakenAt (Snoc cross a q) bodyD bn) +weakenAt cross (THFst pD) bn = THFst (weakenAt cross pD bn) +weakenAt cross (THSnd pD) bn = THSnd (weakenAt cross pD bn) +weakenAt cross (THInl pD) bn = THInl (weakenAt cross pD bn) +weakenAt cross (THInr pD) bn = THInr (weakenAt cross pD bn) +weakenAt cross (THApp {g1} {a} {t1} {t2} q g2 fD xD ac) bn = + let (g1B ** sB ** g1C ** sC ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenSC : (ctxLen sC = ctxLen cross) := acLenR acC + -- split g2 at the cross depth + lenG2 : (ctxLen g2 = ctxLen cross + ctxLen sB) + := trans (sym (scaleLen q g2)) + (trans (cong ctxLen e2) + (trans (ctxLenAppend sB sC) + (cong (\m => m + ctxLen sB) lenSC))) + in + let (g2B ** g2C ** (e3, lenG2C)) = splitTop cross g2 lenG2 in + let -- relate scaled summands + scaleEq : (sB +++ sC = (ctxScale q g2B) +++ (ctxScale q g2C)) + := trans (sym e2) + (trans (cong (ctxScale q) e3) (scaleAppend q g2B g2C)) + lenTop : (ctxLen sC = ctxLen (ctxScale q g2C)) + := trans lenSC (trans (sym lenG2C) (sym (scaleLen q g2C))) + injPair : (sB = ctxScale q g2B, sC = ctxScale q g2C) + := appendInjTop sC (ctxScale q g2C) lenTop scaleEq + eSB : (sB = ctxScale q g2B) := fst injPair + eSC : (sC = ctxScale q g2C) := snd injPair + -- weaken the two sub-derivations + fD' : (Has (g1B +++ g1C) t1 (TArr q a bt)) := rewrite sym e1 in fD + xD' : (Has (g2B +++ g2C) t2 a) := rewrite sym e3 in xD + fW : (Has ((Snoc g1B bn Zero) +++ g1C) (shift 1 (ctxLen cross) t1) (TArr q a bt)) + := rewrite sym lenG1C in weakenAt g1C fD' bn + xW : (Has ((Snoc g2B bn Zero) +++ g2C) (shift 1 (ctxLen cross) t2) a) + := rewrite sym lenG2C in weakenAt g2C xD' bn + -- the scaled second summand equals (Snoc sB bn Zero) +++ sC + scaledEq : (ctxScale q ((Snoc g2B bn Zero) +++ g2C) + = (Snoc sB bn Zero) +++ sC) + := scaledArgEq q g2B g2C bn sB sC eSB eSC + base : (AddCtx (Snoc g1B bn Zero) (Snoc sB bn Zero) (Snoc g bn Zero)) + := ACSnoc bn Zero Zero acB + newSplit : (AddCtx ((Snoc g1B bn Zero) +++ g1C) + (ctxScale q ((Snoc g2B bn Zero) +++ g2C)) + ((Snoc g bn Zero) +++ cross)) + := rewrite scaledEq in acAppend base acC + in THApp q ((Snoc g2B bn Zero) +++ g2C) fW xW newSplit +weakenAt cross (THPair {t1} {t2} {a} {b} g1 g2 t1D t2D ac) bn = + -- SPLIT pair: weaken each component in its own summand context, + -- inserting a Zero binder into both halves of the split (mirroring + -- the THCase scrutinee weakening, minus the branch binders). + let (g1B ** g2B ** g1C ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + t1D' : (Has (g1B +++ g1C) t1 a) := rewrite sym e1 in t1D + t2D' : (Has (g2B +++ g2C) t2 b) := rewrite sym e2 in t2D + t1W : (Has ((Snoc g1B bn Zero) +++ g1C) (shift 1 (ctxLen cross) t1) a) + := rewrite sym lenG1C in weakenAt g1C t1D' bn + t2W : (Has ((Snoc g2B bn Zero) +++ g2C) (shift 1 (ctxLen cross) t2) b) + := rewrite sym lenG2C in weakenAt g2C t2D' bn + newSplit : (AddCtx ((Snoc g1B bn Zero) +++ g1C) + ((Snoc g2B bn Zero) +++ g2C) + ((Snoc g bn Zero) +++ cross)) + := acAppend (ACSnoc bn Zero Zero acB) acC + in THPair ((Snoc g1B bn Zero) +++ g1C) ((Snoc g2B bn Zero) +++ g2C) t1W t2W newSplit +weakenAt cross (THCase {g2} {t} {tL} {tR} {c} ca cb g1 sD lD rD ac) bn = + let (g1B ** g2B ** g1C ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + sD' : (Has (g1B +++ g1C) t (TSum ca cb)) := rewrite sym e1 in sD + sW : (Has ((Snoc g1B bn Zero) +++ g1C) (shift 1 (ctxLen cross) t) (TSum ca cb)) + := rewrite sym lenG1C in weakenAt g1C sD' bn + lD' : (Has (g2B +++ (Snoc g2C ca One)) tL c) := rewrite sym e2 in lD + rD' : (Has (g2B +++ (Snoc g2C cb One)) tR c) := rewrite sym e2 in rD + lW : (Has (Snoc ((Snoc g2B bn Zero) +++ g2C) ca One) + (shift 1 (S (ctxLen cross)) tL) c) + := rewrite sym lenG2C in weakenAt (Snoc g2C ca One) lD' bn + rW : (Has (Snoc ((Snoc g2B bn Zero) +++ g2C) cb One) + (shift 1 (S (ctxLen cross)) tR) c) + := rewrite sym lenG2C in weakenAt (Snoc g2C cb One) rD' bn + newSplit : (AddCtx ((Snoc g1B bn Zero) +++ g1C) + ((Snoc g2B bn Zero) +++ g2C) + ((Snoc g bn Zero) +++ cross)) + := acAppend (ACSnoc bn Zero Zero acB) acC + in THCase ca cb ((Snoc g1B bn Zero) +++ g1C) sW lW rW newSplit +weakenAt cross (THLet {g2} {t1} {t2} {b=bres} q at g1 e1D e2D ac) bn = + let (sB ** g2B ** sC ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let lenSC : (ctxLen sC = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + lenG1 : (ctxLen g1 = ctxLen cross + ctxLen sB) + := trans (sym (scaleLen q g1)) + (trans (cong ctxLen e1) + (trans (ctxLenAppend sB sC) + (cong (\m => m + ctxLen sB) lenSC))) + in + let (g1B ** g1C ** (e3, lenG1C)) = splitTop cross g1 lenG1 in + let scaleEq : (sB +++ sC = (ctxScale q g1B) +++ (ctxScale q g1C)) + := trans (sym e1) + (trans (cong (ctxScale q) e3) (scaleAppend q g1B g1C)) + lenTop : (ctxLen sC = ctxLen (ctxScale q g1C)) + := trans lenSC (trans (sym lenG1C) (sym (scaleLen q g1C))) + injPair : (sB = ctxScale q g1B, sC = ctxScale q g1C) + := appendInjTop sC (ctxScale q g1C) lenTop scaleEq + eSB : (sB = ctxScale q g1B) := fst injPair + eSC : (sC = ctxScale q g1C) := snd injPair + e1D' : (Has (g1B +++ g1C) t1 at) := rewrite sym e3 in e1D + e2D' : (Has (g2B +++ (Snoc g2C at q)) t2 bres) := rewrite sym e2 in e2D + e1W : (Has ((Snoc g1B bn Zero) +++ g1C) (shift 1 (ctxLen cross) t1) at) + := rewrite sym lenG1C in weakenAt g1C e1D' bn + e2W : (Has (Snoc ((Snoc g2B bn Zero) +++ g2C) at q) + (shift 1 (S (ctxLen cross)) t2) bres) + := rewrite sym lenG2C in weakenAt (Snoc g2C at q) e2D' bn + scaledEq : (ctxScale q ((Snoc g1B bn Zero) +++ g1C) + = (Snoc sB bn Zero) +++ sC) + := scaledArgEq q g1B g1C bn sB sC eSB eSC + newSplit : (AddCtx (ctxScale q ((Snoc g1B bn Zero) +++ g1C)) + ((Snoc g2B bn Zero) +++ g2C) + ((Snoc g bn Zero) +++ cross)) + := rewrite scaledEq in acAppend (ACSnoc bn Zero Zero acB) acC + in THLet q at ((Snoc g1B bn Zero) +++ g1C) e1W e2W newSplit + +||| Weaken by inserting a single unused (Zero) binder at the TOP of +||| the context, shifting every free variable up by one. (The +||| `cross = Empty` instance of `weakenAt`.) +public export +weaken1 : {0 g : Ctx} -> {0 t : Tm} -> {0 bt : Ty} + -> Has g t bt -> (bn : Ty) -> Has (Snoc g bn Zero) (shift 1 0 t) bt +weaken1 d bn = weakenAt Empty d bn + +------------------------------------------------------------ +-- The variable case of substitution +------------------------------------------------------------ + +||| Substituting the value `v` for the variable at depth +||| `ctxLen cross` inside a single occurrence `Var n`. +||| +||| The substituted binder sits at the bottom of the context with +||| quantity `q` and type `av`; the value `v` is typed in `gV`; the +||| output context is `gOut = gB + q·gV`. Crossing binders shift +||| `v` up by one each (handled by `substVar`). +public export +substVarLemma : (cross : Ctx) -> (gV : Ctx) + -> {0 gB : Ctx} -> {0 av : Ty} -> {0 q : Q} + -> {0 n : Nat} -> {0 bt : Ty} -> {0 gOut, v : _} + -> HasVar ((Snoc gB av q) +++ cross) n bt + -> Has gV v av + -> AddCtx gB (ctxScale q gV) gOut + -> Has (gOut +++ cross) (substVar (ctxLen cross) v n) bt +substVarLemma Empty gV (HVHere izB) vD acOut = + -- n = Z, bt = av, q = One; substVar Z v Z = v. + -- gOut = gB + One·gV ; gB zero, One·gV = gV ==> gOut = gV. + let eq1 : (ctxScale One gV = gV) := scaleOne gV + acOut' : (AddCtx gB gV gOut) := rewrite sym eq1 in acOut + goutEq : (gOut = gV) := addZeroLEq izB acOut' + in rewrite goutEq in vD +substVarLemma Empty gV (HVThere {n=n'} hv') vD acOut = + -- n = S n', q = Zero; substVar Z v (S n') = Var n'. + -- gOut = gB + Zero·gV = gB. + let izScale : (IsZero (ctxScale Zero gV)) := scaleZeroIsZero gV + goutEq : (gOut = gB) := addZeroREq izScale acOut + in rewrite goutEq in THVar hv' +substVarLemma (Snoc cross _ _) gV (HVHere izC) vD acOut = + -- top binder is the crossed one (quantity One here); n = Z. + -- substVar (S (ctxLen cross)) v Z = Var Z. + -- izC : IsZero ((Snoc gB av q) +++ cross), so gB zero, q = Zero, + -- cross zero ==> gOut zero. + let (izSnocGB, izc) = isZeroAppendSplit cross izC + (izB, qEq) = isZeroSnocInv izSnocGB + -- q = Zero, so ctxScale q gV is zero; gB zero ==> gOut zero. + acOut0 : (AddCtx gB (ctxScale Zero gV) gOut) := rewrite sym qEq in acOut + izGout : (IsZero gOut) + := addZeroResult izB (scaleZeroIsZero gV) acOut0 + in THVar (HVHere (isZeroAppendJoin izGout izc)) +substVarLemma (Snoc cross _ _) gV (HVThere {n=n'} hv') vD acOut = + -- n = S n'; substVar (S (ctxLen cross)) v (S n') + -- = shift 1 0 (substVar (ctxLen cross) v n'). + -- Recurse below the top binder, then weaken by it. + weaken1 (substVarLemma cross gV hv' vD acOut) _ + +------------------------------------------------------------ +-- The substitution lemma (generalised over crossed binders) +------------------------------------------------------------ + +||| `substGen cross gV bodyD vD acOut` — substitute the value `v` +||| (typed in `gV`) for the variable at depth `ctxLen cross` in +||| `body`. The substituted binder sits at the bottom of the body's +||| context with type `av` and quantity `q`; the output context is +||| `gOut = gB + q·gV` (witnessed by `acOut`). Proved by induction on +||| the body's typing derivation. +public export +substGen : (cross : Ctx) -> (gV : Ctx) + -> {0 gB : Ctx} -> {0 av : Ty} -> {0 q : Q} + -> {0 body : Tm} -> {0 bt : Ty} -> {0 gOut, v : _} + -> Has ((Snoc gB av q) +++ cross) body bt + -> Has gV v av + -> AddCtx gB (ctxScale q gV) gOut + -> Has (gOut +++ cross) (subst (ctxLen cross) v body) bt +substGen cross gV (THVar hv) vD acOut = + substVarLemma cross gV hv vD acOut +substGen cross gV (THUnit iz) vD acOut = + -- iz : IsZero ((Snoc gB av q) +++ cross) ==> gOut zero. + let (izSnocGB, izc) = isZeroAppendSplit cross iz + (izB, qEq) = isZeroSnocInv izSnocGB + acOut0 : (AddCtx gB (ctxScale Zero gV) gOut) := rewrite sym qEq in acOut + izGout : (IsZero gOut) + := addZeroResult izB (scaleZeroIsZero gV) acOut0 + in THUnit (isZeroAppendJoin izGout izc) +substGen cross gV (THLam q' a' bodyD) vD acOut = + THLam q' a' (substGen (Snoc cross a' q') gV bodyD vD acOut) +substGen cross gV (THFst pD) vD acOut = THFst (substGen cross gV pD vD acOut) +substGen cross gV (THSnd pD) vD acOut = THSnd (substGen cross gV pD vD acOut) +substGen cross gV (THInl pD) vD acOut = THInl (substGen cross gV pD vD acOut) +substGen cross gV (THInr pD) vD acOut = THInr (substGen cross gV pD vD acOut) +substGen cross gV (THPair {t1} {t2} {a} {b} g1 g2 t1D t2D ac) vD acOut = + -- SPLIT (multiplicative) pair. Structurally identical to the THCase + -- scrutinee/branch split, minus the branch binders and with no + -- scaling: the crossed binder's quantity `q = qAdd qa1 qa2` is + -- shared out across the two components via `acSplit2` on the + -- fused scaling `acScaleFuse qa1 qa2 gV`. + let (g1B ** g2B ** g1C ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let (at ** l1 ** r1 ** qa1 ** qa2 ** (eat, eg1B, eg2B, qEq, acBB)) = acSnocInv acB in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + acOutQ : (AddCtx gB (ctxScale (qAdd qa1 qa2) gV) gOut) := rewrite sym qEq in acOut + acFuse : (AddCtx (ctxScale qa1 gV) (ctxScale qa2 gV) + (ctxScale (qAdd qa1 qa2) gV)) + := acScaleFuse qa1 qa2 gV + in + let (gOutF ** gOutX ** (acOutF, acOutX, comb)) = acSplit2 acBB acFuse acOutQ in + let vDat : (Has gV v at) := rewrite sym eat in vD + e1' : (g1 = (Snoc l1 at qa1) +++ g1C) + := trans e1 (cong (\w => w +++ g1C) eg1B) + e2' : (g2 = (Snoc r1 at qa2) +++ g2C) + := trans e2 (cong (\w => w +++ g2C) eg2B) + t1D' : (Has ((Snoc l1 at qa1) +++ g1C) t1 a) := rewrite sym e1' in t1D + t2D' : (Has ((Snoc r1 at qa2) +++ g2C) t2 b) := rewrite sym e2' in t2D + t1W : (Has (gOutF +++ g1C) (subst (ctxLen cross) v t1) a) + := rewrite sym lenG1C in substGen g1C gV t1D' vDat acOutF + t2W : (Has (gOutX +++ g2C) (subst (ctxLen cross) v t2) b) + := rewrite sym lenG2C in substGen g2C gV t2D' vDat acOutX + newSplit : (AddCtx (gOutF +++ g1C) (gOutX +++ g2C) (gOut +++ cross)) + := acAppend comb acC + in THPair (gOutF +++ g1C) (gOutX +++ g2C) t1W t2W newSplit +substGen cross gV (THCase {g2} {t} {tL} {tR} {c} ca cb g1 sD lD rD ac) vD acOut = + let (g1B ** g2B ** g1C ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let (at ** l1 ** r1 ** qa1 ** qa2 ** (eat, eg1B, eg2B, qEq, acBB)) = acSnocInv acB in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + acOutQ : (AddCtx gB (ctxScale (qAdd qa1 qa2) gV) gOut) := rewrite sym qEq in acOut + acFuse : (AddCtx (ctxScale qa1 gV) (ctxScale qa2 gV) + (ctxScale (qAdd qa1 qa2) gV)) + := acScaleFuse qa1 qa2 gV + in + let (gOutF ** gOutX ** (acOutF, acOutX, comb)) = acSplit2 acBB acFuse acOutQ in + let vDat : (Has gV v at) := rewrite sym eat in vD + e1' : (g1 = (Snoc l1 at qa1) +++ g1C) + := trans e1 (cong (\w => w +++ g1C) eg1B) + e2' : (g2 = (Snoc r1 at qa2) +++ g2C) + := trans e2 (cong (\w => w +++ g2C) eg2B) + sD' : (Has ((Snoc l1 at qa1) +++ g1C) t (TSum ca cb)) := rewrite sym e1' in sD + lD' : (Has ((Snoc r1 at qa2) +++ (Snoc g2C ca One)) tL c) + := rewrite sym e2' in lD + rD' : (Has ((Snoc r1 at qa2) +++ (Snoc g2C cb One)) tR c) + := rewrite sym e2' in rD + sW : (Has (gOutF +++ g1C) (subst (ctxLen cross) v t) (TSum ca cb)) + := rewrite sym lenG1C in substGen g1C gV sD' vDat acOutF + lW : (Has (Snoc (gOutX +++ g2C) ca One) (subst (S (ctxLen cross)) v tL) c) + := rewrite sym lenG2C in substGen (Snoc g2C ca One) gV lD' vDat acOutX + rW : (Has (Snoc (gOutX +++ g2C) cb One) (subst (S (ctxLen cross)) v tR) c) + := rewrite sym lenG2C in substGen (Snoc g2C cb One) gV rD' vDat acOutX + newSplit : (AddCtx (gOutF +++ g1C) (gOutX +++ g2C) (gOut +++ cross)) + := acAppend comb acC + in THCase ca cb (gOutF +++ g1C) sW lW rW newSplit +substGen cross gV (THApp {g1} {a} {t1} {t2} q' g2' fD xD ac) vD acOut = + let (g1B ** s2B ** g1C ** s2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let (at ** l1 ** s2BB ** qa1 ** qa2 ** (eat, eg1B, es2B, qEq, acBB)) = acSnocInv acB in + let lenG1C : (ctxLen g1C = ctxLen cross) := acLenL acC + lenS2C : (ctxLen s2C = ctxLen cross) := acLenR acC + e2sc : (ctxScale q' g2' = (Snoc s2BB at qa2) +++ s2C) + := trans e2 (cong (\w => w +++ s2C) es2B) + in + let (g2BB ** qa2' ** g2C2 ** (g2eq, lenG2C2, sbbEq, qaEq, scEq)) + = unscaleSnocAppend q' g2' cross at lenS2C e2sc in + let acOutQ : (AddCtx gB (ctxScale (qAdd qa1 qa2) gV) gOut) := rewrite sym qEq in acOut + acFuse : (AddCtx (ctxScale qa1 gV) (ctxScale qa2 gV) + (ctxScale (qAdd qa1 qa2) gV)) + := acScaleFuse qa1 qa2 gV + in + let (gOutF ** gOutXS ** (acOutF, acOutXS, comb)) = acSplit2 acBB acFuse acOutQ in + let -- build the unscaled argument output split via shape + shGB_gV : (ShapeEq gB gV) + := shapeTrans (shapeSummands acOut) (shapeSym (shapeScale gV)) + shS2BB_gB : (ShapeEq s2BB gB) + := shapeTrans (shapeSym (shapeSummands acBB)) (shapeLeftResult acBB) + shG2BB_s2BB : (ShapeEq g2BB s2BB) + := rewrite sbbEq in shapeScale g2BB + shG2BB_gV : (ShapeEq g2BB gV) + := shapeTrans shG2BB_s2BB (shapeTrans shS2BB_gB shGB_gV) + shWit : (ShapeEq g2BB (ctxScale qa2' gV)) + := shapeTrans shG2BB_gV (shapeScale gV) + in + let (gOutX ** acOutX) = mkAdd g2BB (ctxScale qa2' gV) shWit in + let -- scale the argument output split and identify it with gOutXS + acScaled0 : (AddCtx (ctxScale q' g2BB) (ctxScale q' (ctxScale qa2' gV)) + (ctxScale q' gOutX)) + := acScale q' acOutX + -- gOutXS = ctxScale q' gOutX, by determinism up to the summand + -- equalities s2BB = ctxScale q' g2BB and + -- ctxScale qa2 gV = ctxScale q' (ctxScale qa2' gV). + midEq : (ctxScale qa2 gV = ctxScale q' (ctxScale qa2' gV)) + := trans (cong (\qq => ctxScale qq gV) qaEq) + (sym (scaleScale q' qa2' gV)) + gOutXSEq : (gOutXS = ctxScale q' gOutX) + := addDetEq acOutXS acScaled0 sbbEq midEq + comb' : (AddCtx gOutF (ctxScale q' gOutX) gOut) := rewrite sym gOutXSEq in comb + vDat : (Has gV v at) := rewrite sym eat in vD + e1' : (g1 = (Snoc l1 at qa1) +++ g1C) + := trans e1 (cong (\w => w +++ g1C) eg1B) + fD' : (Has ((Snoc l1 at qa1) +++ g1C) t1 (TArr q' a bt)) := rewrite sym e1' in fD + xD' : (Has ((Snoc g2BB at qa2') +++ g2C2) t2 a) := rewrite sym g2eq in xD + fW : (Has (gOutF +++ g1C) (subst (ctxLen cross) v t1) (TArr q' a bt)) + := rewrite sym lenG1C in substGen g1C gV fD' vDat acOutF + xW : (Has (gOutX +++ g2C2) (subst (ctxLen cross) v t2) a) + := rewrite sym lenG2C2 in substGen g2C2 gV xD' vDat acOutX + scaledOutEq : (ctxScale q' (gOutX +++ g2C2) = (ctxScale q' gOutX) +++ s2C) + := trans (scaleAppend q' gOutX g2C2) + (cong (\w => (ctxScale q' gOutX) +++ w) (sym scEq)) + newSplit : (AddCtx (gOutF +++ g1C) + (ctxScale q' (gOutX +++ g2C2)) + (gOut +++ cross)) + := rewrite scaledOutEq in acAppend comb' acC + in THApp q' (gOutX +++ g2C2) fW xW newSplit +substGen cross gV (THLet {g2} {t1} {t2} {b=bres} q' at g1' e1D e2D ac) vD acOut = + let (s1B ** g2B ** s1C ** g2C ** (e1, e2, acB, acC)) = acAppendInv cross ac in + let (at2 ** s1BB ** g2BB ** qa1 ** qa2 ** (eat, es1B, eg2B, qEq, acBB)) = acSnocInv acB in + let lenS1C : (ctxLen s1C = ctxLen cross) := acLenL acC + lenG2C : (ctxLen g2C = ctxLen cross) := acLenR acC + e1sc : (ctxScale q' g1' = (Snoc s1BB at2 qa1) +++ s1C) + := trans e1 (cong (\w => w +++ s1C) es1B) + in + let (g1BB ** qa1' ** g1C ** (g1eq, lenG1C, s1bbEq, qa1Eq, s1cEq)) + = unscaleSnocAppend q' g1' cross at2 lenS1C e1sc in + let acOutQ : (AddCtx gB (ctxScale (qAdd qa1 qa2) gV) gOut) := rewrite sym qEq in acOut + acFuse : (AddCtx (ctxScale qa1 gV) (ctxScale qa2 gV) + (ctxScale (qAdd qa1 qa2) gV)) + := acScaleFuse qa1 qa2 gV + in + let (gOut1 ** gOut2 ** (acOut1S, acOut2, comb)) = acSplit2 acBB acFuse acOutQ in + let -- unscaled RHS output split (acOut1S is over the scaled base s1BB) + shGB_gV : (ShapeEq gB gV) + := shapeTrans (shapeSummands acOut) (shapeSym (shapeScale gV)) + shS1BB_gB : (ShapeEq s1BB gB) + := shapeLeftResult acBB + shG1BB_s1BB : (ShapeEq g1BB s1BB) + := rewrite s1bbEq in shapeScale g1BB + shG1BB_gV : (ShapeEq g1BB gV) + := shapeTrans shG1BB_s1BB (shapeTrans shS1BB_gB shGB_gV) + shWit : (ShapeEq g1BB (ctxScale qa1' gV)) + := shapeTrans shG1BB_gV (shapeScale gV) + in + let (gOut1U ** acOut1U) = mkAdd g1BB (ctxScale qa1' gV) shWit in + let acScaled0 : (AddCtx (ctxScale q' g1BB) (ctxScale q' (ctxScale qa1' gV)) + (ctxScale q' gOut1U)) + := acScale q' acOut1U + midEq : (ctxScale qa1 gV = ctxScale q' (ctxScale qa1' gV)) + := trans (cong (\qq => ctxScale qq gV) qa1Eq) + (sym (scaleScale q' qa1' gV)) + gOut1Eq : (gOut1 = ctxScale q' gOut1U) + := addDetEq acOut1S acScaled0 s1bbEq midEq + vDat : (Has gV v at2) := rewrite sym eat in vD + e1D' : (Has ((Snoc g1BB at2 qa1') +++ g1C) t1 at) := rewrite sym g1eq in e1D + eg2' : (g2 = (Snoc g2BB at2 qa2) +++ g2C) + := trans e2 (cong (\w => w +++ g2C) eg2B) + e2D' : (Has ((Snoc g2BB at2 qa2) +++ (Snoc g2C at q')) t2 bres) + := rewrite sym (cong (\w => Snoc w at q') eg2') in e2D + e1W : (Has (gOut1U +++ g1C) (subst (ctxLen cross) v t1) at) + := rewrite sym lenG1C in substGen g1C gV e1D' vDat acOut1U + e2W : (Has (Snoc (gOut2 +++ g2C) at q') (subst (S (ctxLen cross)) v t2) bres) + := rewrite sym lenG2C in substGen (Snoc g2C at q') gV e2D' vDat acOut2 + scaledOutEq : (ctxScale q' (gOut1U +++ g1C) = gOut1 +++ s1C) + := trans (scaleAppend q' gOut1U g1C) + (trans (cong (\w => (ctxScale q' gOut1U) +++ w) (sym s1cEq)) + (cong (\w => w +++ s1C) (sym gOut1Eq))) + newSplit : (AddCtx (ctxScale q' (gOut1U +++ g1C)) + (gOut2 +++ g2C) + (gOut +++ cross)) + := rewrite scaledOutEq in acAppend comb acC + in THLet q' at (gOut1U +++ g1C) e1W e2W newSplit + +||| The top-level substitution lemma: `subst0 body v` (the redex +||| substitution `body[v/0]`). +public export +substLemma0 : {0 gB : Ctx} -> {0 av : Ty} -> {0 q : Q} + -> {0 body : Tm} -> {0 bt : Ty} -> {0 gOut, v : _} + -> (gV : Ctx) + -> Has (Snoc gB av q) body bt + -> Has gV v av + -> AddCtx gB (ctxScale q gV) gOut + -> Has gOut (subst0 body v) bt +substLemma0 gV bodyD vD acOut = substGen Empty gV bodyD vD acOut diff --git a/docs/academic/formal-verification/solo-core/Typing.idr b/docs/academic/formal-verification/solo-core/Typing.idr index 4a00dfdc..a6bad659 100644 --- a/docs/academic/formal-verification/solo-core/Typing.idr +++ b/docs/academic/formal-verification/solo-core/Typing.idr @@ -7,6 +7,11 @@ -- context `g`, with `g`'s quantities exactly accounting for the -- uses of each bound variable inside `t`. -- +-- These are the RULES, stated as data constructors. The meta- +-- theorems (progress, preservation, affine-preservation) are +-- stated in `Soundness.idr` and will be proved in weeks 3-12 of +-- Track F1. +-- -- Source of truth for the rule shapes: -- * docs/spec.md §3.1, §3.6 (T-Var, T-Lam, T-App, T-Let) -- * lib/quantity.ml — semiring operations and the "linear must @@ -21,21 +26,6 @@ -- formulation for which progress + preservation are provable, -- and is equivalent to the implementation's usage-walk for the -- Solo fragment. An explicit equivalence lemma is future work. --- --- ENCODING NOTE (week-3 mechanisation, vs. the week-1-2 statement --- form): two purely-presentational changes were needed to make the --- judgement *provable* in Idris2, neither of which alters the set of --- derivable judgements: --- --- * The split contexts of T-App / T-Pair / T-Case / T-Let are now --- **explicit** arguments (`(g1, g2 : Ctx) -> ...`). Idris2 erases --- data-type indices, so without this the sub-contexts could not --- be analysed inside the soundness proofs at all. --- --- * The all-zero context of T-Var / T-Unit is expressed by the --- analysable premise `IsZero g` (from ContextLemmas) rather than --- the non-invertible computed index `ctxZero g0`. `IsZero g` --- holds iff `g = ctxZero g`, so the rule is unchanged in meaning. module Typing @@ -52,17 +42,19 @@ import ContextLemmas ------------------------------------------------------------ ||| `HasVar g n a` says the de Bruijn variable `n` has type `a` -||| in `g`, where `g` assigns quantity `One` to position `n` and -||| quantity `Zero` to every other position. This is the T-Var -||| rule in QTT: "using a variable once uses it exactly once, and -||| uses nothing else". +||| in `g`, where `g` is a context that assigns quantity `One` +||| to position `n` and quantity `Zero` to every other position. +||| This is the T-Var rule in QTT: "using a variable once uses +||| it exactly once, and uses nothing else". +||| +||| `HVHere` carries an explicit `IsZero g` witness (rather than +||| pinning the tail to the literal `ctxZero g`) so the +||| substitution proof can analyse the surrounding erased context. public export data HasVar : Ctx -> Nat -> Ty -> Type where - ||| The variable is the most recently bound one: it sits at - ||| quantity `One` on top of an all-zero context. - HVHere : (g : Ctx) -> IsZero g -> HasVar (Snoc g a One) Z a - ||| Skip a more recent binding, which must be unused (`Zero`). - HVThere : (g : Ctx) -> HasVar g n a -> HasVar (Snoc g b Zero) (S n) a + HVHere : IsZero g -> HasVar (Snoc g a One) Z a + HVThere : HasVar g n a + -> HasVar (Snoc g b Zero) (S n) a ------------------------------------------------------------ -- The typing judgement @@ -79,33 +71,55 @@ data Has : Ctx -> Tm -> Ty -> Type where -> Has g (Var n) a ||| T-Unit: the unit term types in any all-zero context. - THUnit : IsZero g - -> Has g UnitT TUnit + THUnit : IsZero g -> Has g UnitT TUnit ||| T-Lam: introduce a binding with quantity `q` and type `a`, ||| type the body in the extended context. The resulting ||| function type `TArr q a b` records the quantity. - THLam : Has (Snoc g a q) t b + ||| + ||| `q` and `a` are explicit RUNTIME arguments (not just erased + ||| indices) so the metatheory proofs can analyse the binder when + ||| they descend under it (Idris2 erases data-type implicit + ||| indices, but the substitution/weakening proofs must rebuild + ||| the crossed binder at runtime). + THLam : (q : Q) -> (a : Ty) + -> Has (Snoc g a q) t b -> Has g (Lam q a t) (TArr q a b) ||| T-App: the function is typed in `g1`, the argument in `g2` ||| scaled by the function's parameter quantity `q`, and the ||| whole application is typed in the pointwise sum - ||| `g1 + q * g2`. - THApp : (g1, g2 : Ctx) -> (q : Q) + ||| `g1 + q * g2`. `q` and the (UNscaled) argument context `g2` are + ||| explicit runtime arguments: scaling is not invertible, so the + ||| proofs need `g2` itself to split the argument's context. + THApp : (q : Q) -> (g2 : Ctx) -> Has g1 t1 (TArr q a b) -> Has g2 t2 a - -> ctxAdd g1 (ctxScale q g2) = Just g + -> AddCtx g1 (ctxScale q g2) g -> Has g (App t1 t2) b - ||| T-Pair: product introduction splits the context additively. - THPair : (g1, g2 : Ctx) + ||| T-Pair: MULTIPLICATIVE (tensor) product introduction. The two + ||| components are typed in SEPARATE contexts `g1` and `g2`, and the + ||| whole pair is typed in their pointwise sum `g1 + g2`, mirroring + ||| `THApp`'s `AddCtx` split (with no scaling, since neither + ||| component sits under a quantity annotation). + ||| + ||| `g1` and `g2` are explicit RUNTIME arguments so the metatheory + ||| proofs can rebuild the two summand contexts when they descend + ||| into the components (the typed indices are erased). + ||| + ||| Under this SPLIT rule preservation can no longer hold in the + ||| SAME context for the projection-beta steps — `Fst (Pair v1 v2)` + ||| steps to `v1`, which is typed only in the LEFT summand `g1`, a + ||| sub-context of the whole `g`. This is exactly the affine reading: + ||| preservation returns a reduct typed in a `Weaker` sub-context. + THPair : (g1 : Ctx) -> (g2 : Ctx) -> Has g1 t1 a -> Has g2 t2 b - -> ctxAdd g1 g2 = Just g + -> AddCtx g1 g2 g -> Has g (Pair t1 t2) (TPair a b) - ||| T-Fst: projection does not split (a single subterm). + ||| T-Fst: projection (single subterm, same context). THFst : Has g t (TPair a b) -> Has g (Fst t) a @@ -123,12 +137,18 @@ data Has : Ctx -> Tm -> Ty -> Type where ||| T-Case: the scrutinee is typed in `g1`; each branch binds ||| the injected value with quantity One and is typed in `g2` ||| extended with that binder. Branches must agree on `g2` and - ||| on the result type. The whole `case` is typed in `g1 + g2`. - THCase : (g1, g2 : Ctx) + ||| on the result type. The whole `case` is typed in + ||| `g1 + g2`. + ||| `a` and `b` (the two summand types, hence the two branch + ||| binder types) and the scrutinee context `g1` are explicit + ||| runtime arguments so the proofs can descend under the branch + ||| binders and run the substitution lemma at the case-beta step + ||| (which substitutes the injected value, typed in `g1`). + THCase : (a : Ty) -> (b : Ty) -> (g1 : Ctx) -> Has g1 t (TSum a b) -> Has (Snoc g2 a One) tL c -> Has (Snoc g2 b One) tR c - -> ctxAdd g1 g2 = Just g + -> AddCtx g1 g2 g -> Has g (Case t tL tR) c ||| T-Let: bind `t1` with declared quantity `q`. The RHS is @@ -136,8 +156,12 @@ data Has : Ctx -> Tm -> Ty -> Type where ||| to `g2` (the body's context). This is the usual QTT let ||| rule and matches how `lib/typecheck.ml` threads quantities ||| through `let` bindings. - THLet : (g1, g2 : Ctx) -> (q : Q) + ||| `q`, `a`, and the (UNscaled) RHS context `g1` are explicit + ||| runtime arguments: the proofs need `g1` to split the RHS's + ||| (scaled) context (scaling is not invertible). The body context + ||| `g2` is recovered at runtime from the additive-split witness. + THLet : (q : Q) -> (a : Ty) -> (g1 : Ctx) -> Has g1 t1 a -> Has (Snoc g2 a q) t2 b - -> ctxAdd (ctxScale q g1) g2 = Just g + -> AddCtx (ctxScale q g1) g2 g -> Has g (Let q t1 t2) b From 9137a76fe4035c9b074c3b26837bcf99965d59b6 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 16 Jun 2026 01:15:21 +0100 Subject: [PATCH 05/63] tooling(wasm): add wasm-validate + coprocessor-validate dependability gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two additive gates that pin compile-target validity, mirroring the check-proofs.sh pattern: - just wasm-validate (tools/wasm-validate-gate.sh): compiles the positive corpus to core wasm and runs wasm-tools validate on every module (19 pass / 0 fail / 5 allowlisted carve-outs). Closes the test_e2e.ml:601 blind spot where tests only checked codegen-did-not-raise, never byte validity. - just coprocessor-validate (tools/coprocessor-gate.sh): compiles canonical kernels to all nine Tier-C accelerator backends (WGSL/SPIR-V/CUDA/Metal/OpenCL/MLIR/ONNX/Faust/Verilog) plus LLVM, validating WGSL via naga and SPIR-V via magic word (12 pass / 0 fail). Also surfaces issues-drafts/05: the core-wasm uniform 4-byte heap-cell model mismodels any Float that transits the heap (invalid module on load, silent 32-of-64-bit truncation on store) — newly caught by the validate gate, tracked for a type-directed-layout fix. Co-Authored-By: Claude Opus 4.8 (1M context) --- ...at-through-heap-cell-model-invalid-wasm.md | 71 ++++++++++++++++ justfile | 13 +++ tools/coprocessor-gate.sh | 83 ++++++++++++++++++ tools/wasm-validate-gate.sh | 85 +++++++++++++++++++ 4 files changed, 252 insertions(+) create mode 100644 issues-drafts/05-float-through-heap-cell-model-invalid-wasm.md create mode 100755 tools/coprocessor-gate.sh create mode 100755 tools/wasm-validate-gate.sh diff --git a/issues-drafts/05-float-through-heap-cell-model-invalid-wasm.md b/issues-drafts/05-float-through-heap-cell-model-invalid-wasm.md new file mode 100644 index 00000000..b2e6bb25 --- /dev/null +++ b/issues-drafts/05-float-through-heap-cell-model-invalid-wasm.md @@ -0,0 +1,71 @@ + + +# Core-wasm: any `Float` that transits the heap is mismodeled (invalid/truncated wasm) + +**Surfaced by:** WASM coverage sweep + coprocessor smoke test (2026-06-16) +**Affected version:** `affinescript` compiler at HEAD (branch `feat/solo-core-metatheory-proofs`) +**Severity:** Correctness + **security** — silent 32-of-64-bit truncation on store; invalid module on load. Caught for the first time by the new `just wasm-validate` gate (`tools/wasm-validate-gate.sh`); previously hidden because `test/test_e2e.ml:601` only checks "codegen did not raise", never `wasm-tools validate`. + +## Reproducers + +```affinescript +// (a) load: INVALID module — wasm-tools: "expected f64, found i32" +fn rd(i: Int, a: Array[Float]) -> Float { a[i] } + +// (b) projection: INVALID module (same cause, via tuple) +fn proj() -> Float { let t: (Float, Float) = (1.0, 2.0); t.0 } + +// (c) store: VALIDATES but is SEMANTICALLY WRONG — copies 32 of 64 bits +fn k(i: Int, mut o: Array[Float], a: Array[Float]) -> Unit { o[i] = a[i]; } +``` + +``` +$ affinescript compile rd.affine -o rd.wasm && wasm-tools validate rd.wasm +error: func 1 failed to validate + 0: type mismatch: expected f64, found i32 +``` + +Scalars are fine (`fn dbl(x: Float) -> Float { x * 2.0 }` validates) — the bug is strictly the heap path. `Int` through the heap is fine. + +## Root cause + +The core-wasm backend (`lib/codegen.ml`) uses a **uniform 4-byte (i32) heap-cell +model** everywhere: + +- array alloc `size = 4 + (num_elements * 4)`, element offset `4 + (idx * 4)` + (`lib/codegen.ml:1926`, `:1949`, `:2047-2053`) +- tuple/record fields at `index * 4`, `I32Load`/`I32Store` with a `* 4` stride + (`:1964`, `:2030`, `:2519-2548`) + +A `Float` is `f64` (8 bytes) in locals/arithmetic, but the moment it is stored +into or loaded from an array/tuple/record cell the layout assumes 4 bytes and +the access is emitted as `i32.{load,store}`. Hence: load-then-use-as-f64 → +invalid module; store → 32-bit truncation of a 64-bit value. + +## Fix options + +1. **Type-directed heap layout (the real fix).** Make cell size and the + load/store opcode a function of the static element/field type: `f64` cells + are 8 bytes with `f64.{load,store}` and an 8-byte stride; mixed records/ + tuples compute per-field offsets from field types. Touches arrays, tuples, + records, and closures — a substantial, careful codegen change. **High + revert-cost → land behind its own PR with the `wasm-validate` gate + extended to cover Float-in-heap fixtures.** +2. **Honest loud-fail (interim, secure).** Until (1) lands, have the backend + raise `Codegen.UnsupportedFeature` when a `Float` would transit a heap cell, + with a message routing to the interpreter (`-i`), the Julia backend + (`-julia`), or the GPU kernel backends (WGSL/CUDA/Metal/OpenCL **already + lower `f64` array buffers correctly** — verified 2026-06-16). This converts + silent-wrong into honest-reject, matching the #555/#556 loud-fail policy. + +Recommended: ship (2) now for safety, then (1) as the durable fix. Both are +gated by `just wasm-validate`. + +## Related + +Not the same as the deliberate carve-outs #555 (effect handlers) / #556 (async +CPS) — those loud-fail already. This one is a *silent* defect in the value +representation, newly made visible by the validate gate. diff --git a/justfile b/justfile index 8e732784..5ec45690 100644 --- a/justfile +++ b/justfile @@ -127,6 +127,19 @@ proof-check-agda: proof-check-all: ./tools/check-proofs.sh --all +# ── WASM validation ──────────────────────────────────────────────────────────── +# Compile the positive corpus to core wasm and run `wasm-tools validate` on +# every module. Closes the test_e2e.ml:601 blind spot (codegen-did-not-raise +# != emitted-valid-wasm). Hard-fails on any silent-invalid emission. +wasm-validate: + ./tools/wasm-validate-gate.sh + +# Compile canonical kernels to every coprocessor/accelerator backend +# (WGSL/SPIR-V/CUDA/Metal/OpenCL/MLIR/ONNX/Faust/Verilog/LLVM) and check the +# emission — validating with naga / SPIR-V magic where a tool is on PATH. +coprocessor-validate: + ./tools/coprocessor-gate.sh + # ── Compiler subcommands ────────────────────────────────────────────────────── # Run the lexer on a file diff --git a/tools/coprocessor-gate.sh b/tools/coprocessor-gate.sh new file mode 100755 index 00000000..0b81c69c --- /dev/null +++ b/tools/coprocessor-gate.sh @@ -0,0 +1,83 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Coprocessor / accelerator backend emission gate for AffineScript. +# +# The Tier-C kernel-sublanguage backends (WGSL, SPIR-V, CUDA, Metal, OpenCL, +# MLIR, ONNX, Faust, Verilog) are wired into `bin/main.ml` but had ZERO test +# coverage — nothing pinned "the GPU/audio/FPGA emitters actually work". This +# gate compiles canonical kernels to every coprocessor target and checks the +# output, validating with a real tool wherever one exists on PATH: +# WGSL -> naga (if present) SPIR-V -> magic word 0x07230203 +# The rest are emit-and-nonempty checks (no hermetic validator shipped here). +# +# Run from anywhere; cd's to repo root. Skips a target's validator if the tool +# is absent (emit check still runs). + +set -uo pipefail +cd "$(dirname "$0")/.." +REPO="$(pwd)" + +GREEN=$'\033[32m'; RED=$'\033[31m'; YEL=$'\033[33m'; DIM=$'\033[2m'; RST=$'\033[0m' +pass=0; fail=0 +ok () { printf '%s PASS%s %s\n' "$GREEN" "$RST" "$1"; pass=$((pass+1)); } +bad () { printf '%s FAIL%s %s\n' "$RED" "$RST" "$1"; fail=$((fail+1)); } + +BIN="$REPO/_build/default/bin/main.exe" +[ -x "$BIN" ] || { echo "── building compiler ──"; dune build 2>/dev/null || { echo "build failed"; exit 1; }; } + +tmp="$(mktemp -d)"; trap 'rm -rf "$tmp"' EXIT + +# ── canonical kernels (the accepted Tier-C subset) ─────────────────────────── +cat > "$tmp/saxpy.affine" <<'EOF' +fn kernel(i: Int, mut out: Array[Float], a: Array[Float], b: Array[Float]) -> Unit { + out[i] = a[i] + b[i]; +} +EOF +cat > "$tmp/graph.affine" <<'EOF' +fn relu(x: Array[Float]) -> Array[Float] { x } +fn add(a: Array[Float], b: Array[Float]) -> Array[Float] { a } +fn graph(x: Array[Float], y: Array[Float]) -> Array[Float] { + let s: Array[Float] = add(x, y); + let r: Array[Float] = relu(s); + r +} +EOF +printf 'fn process(x: Float) -> Float { x * 0.5 }\n' > "$tmp/dsp.affine" +printf 'fn add(a: Int, b: Int) -> Int { a + b }\n' > "$tmp/scalar.affine" + +emit () { #