From 326d25f35ae35a153fe3e9c732a018319f559e1f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 22:52:37 +0000 Subject: [PATCH 01/11] proof(wager): Stage 8 freeze: open-typed terms, typing rules, 3 statements Stage 8 gives a term of the target a context of type variables. There is no quantifier, and the 79 checked modules of stages 1 to 7 do not change. Frozen before any proof: T8-Conv, T8-Inst, T8-Closed (Wager/Poly/Statements.agda). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK --- .../proofs/agda/Wager/Poly/Statements.agda | 40 +++++++++++ verification/proofs/agda/Wager/Poly/Term.agda | 70 +++++++++++++++++++ .../proofs/agda/Wager/Poly/Typing.agda | 68 ++++++++++++++++++ 3 files changed, 178 insertions(+) create mode 100644 verification/proofs/agda/Wager/Poly/Statements.agda create mode 100644 verification/proofs/agda/Wager/Poly/Term.agda create mode 100644 verification/proofs/agda/Wager/Poly/Typing.agda diff --git a/verification/proofs/agda/Wager/Poly/Statements.agda b/verification/proofs/agda/Wager/Poly/Statements.agda new file mode 100644 index 0000000..8be7401 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Statements.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The statements, frozen before their proofs. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature + +module Wager.Poly.Statements + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ) +open import Wager.L1.Syntax S +open import Wager.L1.Conversion S +open import Wager.L2.Typing S TS ops using (_▸_⊢_∶_) +open import Wager.Poly.Typing S TS ops + +-- T8-Conv. Conversion of types is stable under a substitution of types. +T8-Conv : Type +T8-Conv = ∀ {Δ Δ' k} (σ : TySub Δ' Δ) {A B : Ty Δ k} → + DefEq A B → DefEq (sub σ A) (sub σ B) + +-- T8-Inst. Each instance of a typed open term is typed, with the same +-- usage. The type and the context are the instances. +T8-Inst : Type +T8-Inst = ∀ {Δ Δ' n} (σ : TySub Δ' Δ) {γ : Usage n} {Γ : Cxᵖ Δ n} + {t : Tmᵖ Δ n} {A : Ty Δ ★} → + γ ▸ Γ ⊢ᵖ t ∶ A → + γ ▸ (λ i → sub σ (Γ i)) ⊢ᵖ inst σ t ∶ sub σ A + +-- T8-Closed. A typed term with no type variable is a typed term of the +-- target calculus of stages 1 to 5. So T0 to T6 apply to each closed +-- instance of an open term. +T8-Closed : Type +T8-Closed = ∀ {n} {γ : Usage n} {Γ : Cxᵖ [] n} {t : Tmᵖ [] n} {A : Ty [] ★} → + γ ▸ Γ ⊢ᵖ t ∶ A → γ ▸ Γ ⊢ ⌊ t ⌋ ∶ A diff --git a/verification/proofs/agda/Wager/Poly/Term.agda b/verification/proofs/agda/Wager/Poly/Term.agda new file mode 100644 index 0000000..5725b12 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Term.agda @@ -0,0 +1,70 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. Terms of the target with open types. +-- The terms of `Wager.L2.Term` have closed types only (`Ty [] ★`). Here a +-- term is in a context Δ of type variables, and a type annotation is a type +-- in Δ. There is no quantifier: a polymorphic program is an open term. +open import Wager.L1.Signature +import Wager.L2.Signature + +module Wager.Poly.Term (S : Sig) (TS : Wager.L2.Signature.TSig S) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Wager.L1.Syntax S +open import Wager.L2.Term S TS + +private + variable + n m : ℕ + Δ Δ' : Ctx + +data Tmᵖ (Δ : Ctx) : ℕ → Type where + tvar : Fin n → Tmᵖ Δ n + tlam : TG → Ty Δ ★ → Tmᵖ Δ (suc n) → Tmᵖ Δ n + tapp : Tmᵖ Δ n → Tmᵖ Δ n → Tmᵖ Δ n + pair : Tmᵖ Δ n → Tmᵖ Δ n → Tmᵖ Δ n + letp : Tmᵖ Δ n → Tmᵖ Δ (suc (suc n)) → Tmᵖ Δ n + inj₁ : Tmᵖ Δ n → Tmᵖ Δ n + inj₂ : Tmᵖ Δ n → Tmᵖ Δ n + case : Tmᵖ Δ n → Tmᵖ Δ (suc n) → Tmᵖ Δ (suc n) → Tmᵖ Δ n + lit : Lit → Tmᵖ Δ n + step : Op → Tmᵖ Δ n → Tmᵖ Δ n + +-- Instantiation: a substitution of types for the type variables of a term. +inst : TySub Δ' Δ → Tmᵖ Δ n → Tmᵖ Δ' n +inst σ (tvar i) = tvar i +inst σ (tlam q A b) = tlam q (sub σ A) (inst σ b) +inst σ (tapp f a) = tapp (inst σ f) (inst σ a) +inst σ (pair s t) = pair (inst σ s) (inst σ t) +inst σ (letp s b) = letp (inst σ s) (inst σ b) +inst σ (inj₁ t) = inj₁ (inst σ t) +inst σ (inj₂ t) = inj₂ (inst σ t) +inst σ (case s l r) = case (inst σ s) (inst σ l) (inst σ r) +inst σ (lit ℓ) = lit ℓ +inst σ (step o t) = step o (inst σ t) + +-- A term with no type variable is a term of `Wager.L2.Term`. +⌊_⌋ : Tmᵖ [] n → Tm n +⌊ tvar i ⌋ = tvar i +⌊ tlam q A b ⌋ = tlam q A ⌊ b ⌋ +⌊ tapp f a ⌋ = tapp ⌊ f ⌋ ⌊ a ⌋ +⌊ pair s t ⌋ = pair ⌊ s ⌋ ⌊ t ⌋ +⌊ letp s b ⌋ = letp ⌊ s ⌋ ⌊ b ⌋ +⌊ inj₁ t ⌋ = inj₁ ⌊ t ⌋ +⌊ inj₂ t ⌋ = inj₂ ⌊ t ⌋ +⌊ case s l r ⌋ = case ⌊ s ⌋ ⌊ l ⌋ ⌊ r ⌋ +⌊ lit ℓ ⌋ = lit ℓ +⌊ step o t ⌋ = step o ⌊ t ⌋ + +-- A closed type in a context of type variables. +εᵣ : Ren Δ [] +εᵣ k () + +⇑ : Ty [] ★ → Ty Δ ★ +⇑ A = ren εᵣ A diff --git a/verification/proofs/agda/Wager/Poly/Typing.agda b/verification/proofs/agda/Wager/Poly/Typing.agda new file mode 100644 index 0000000..2477c81 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Typing.agda @@ -0,0 +1,68 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The typing judgement for terms with open types. +-- Each rule is the rule of `Wager.L2.Typing` with the types in Δ. +-- No rule is new, and no rule names a grade other than 𝟘 and 𝟙. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature + +module Wager.Poly.Typing + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Wager.L1.Syntax S +open import Wager.L1.Conversion S +open import Wager.L2.Term S TS using (Lit; litTy; Op; carrier; from; to; _at_) +open import Wager.L2.Usage ops public +open import Wager.Poly.Term S TS public +open GradeOps ops + +private + variable + n : ℕ + Δ : Ctx + +Cxᵖ : Ctx → ℕ → Type +Cxᵖ Δ n = Fin n → Ty Δ ★ + +infixl 5 _▹ᵖ_ +_▹ᵖ_ : Cxᵖ Δ n → Ty Δ ★ → Cxᵖ Δ (suc n) +(Γ ▹ᵖ A) zero = A +(Γ ▹ᵖ A) (suc i) = Γ i + +infix 3 _▸_⊢ᵖ_∶_ +data _▸_⊢ᵖ_∶_ {Δ : Ctx} {n : ℕ} : Usage n → Cxᵖ Δ n → Tmᵖ Δ n → Ty Δ ★ → Type where + t-var : ∀ {Γ} i → unit i ▸ Γ ⊢ᵖ tvar i ∶ Γ i + t-lam : ∀ {γ Γ q A B b} → + (γ ▹ q) ▸ (Γ ▹ᵖ A) ⊢ᵖ b ∶ B → + γ ▸ Γ ⊢ᵖ tlam q A b ∶ arr q A B + t-app : ∀ {γ δ Γ q A B f a} → + γ ▸ Γ ⊢ᵖ f ∶ arr q A B → δ ▸ Γ ⊢ᵖ a ∶ A → + (γ +ᵘ (q ·ᵘ δ)) ▸ Γ ⊢ᵖ tapp f a ∶ B + t-pair : ∀ {γ δ Γ A B s t} → + γ ▸ Γ ⊢ᵖ s ∶ A → δ ▸ Γ ⊢ᵖ t ∶ B → + (γ +ᵘ δ) ▸ Γ ⊢ᵖ pair s t ∶ A ⊗ B + t-letp : ∀ {γ δ Γ A B C s b} → + γ ▸ Γ ⊢ᵖ s ∶ A ⊗ B → + (δ ▹ 𝟙 ▹ 𝟙) ▸ (Γ ▹ᵖ A ▹ᵖ B) ⊢ᵖ b ∶ C → + (γ +ᵘ δ) ▸ Γ ⊢ᵖ letp s b ∶ C + t-inj₁ : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ᵖ t ∶ A → γ ▸ Γ ⊢ᵖ inj₁ t ∶ A ⊕ B + t-inj₂ : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ᵖ t ∶ B → γ ▸ Γ ⊢ᵖ inj₂ t ∶ A ⊕ B + t-case : ∀ {γ δ Γ A B C s l r} → + γ ▸ Γ ⊢ᵖ s ∶ A ⊕ B → + (δ ▹ 𝟙) ▸ (Γ ▹ᵖ A) ⊢ᵖ l ∶ C → + (δ ▹ 𝟙) ▸ (Γ ▹ᵖ B) ⊢ᵖ r ∶ C → + (γ +ᵘ δ) ▸ Γ ⊢ᵖ case s l r ∶ C + t-lit : ∀ {Γ} ℓ → 0ᵘ ▸ Γ ⊢ᵖ lit ℓ ∶ base (litTy ℓ) + t-step : ∀ {γ Γ t} o → + γ ▸ Γ ⊢ᵖ t ∶ ⇑ (carrier o at from o) → + γ ▸ Γ ⊢ᵖ step o t ∶ ⇑ (carrier o at to o) + t-conv : ∀ {γ Γ A B t} → γ ▸ Γ ⊢ᵖ t ∶ A → DefEq A B → γ ▸ Γ ⊢ᵖ t ∶ B + t-sub : ∀ {γ δ Γ A t} → γ ▸ Γ ⊢ᵖ t ∶ A → γ ≤ᵘ δ → δ ▸ Γ ⊢ᵖ t ∶ A From a2c9619cb156ef8087b2a58df4d1d99a001adea0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 22:52:50 +0000 Subject: [PATCH 02/11] wip(wager): Stage 8 proofs, NOT type-checked yet Wager/Poly/Proofs.agda has the proofs of T8-Conv, T8-Inst and T8-Closed. t8-conv and t8-inst are not confirmed; t8-closed fails with unsolved constraints (the `subst` motives need explicit arguments). Do not merge. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_0136P7ZmiFSCoB3UR9Kk56rK --- .../proofs/agda/Wager/Poly/Proofs.agda | 135 ++++++++++++++++++ 1 file changed, 135 insertions(+) create mode 100644 verification/proofs/agda/Wager/Poly/Proofs.agda diff --git a/verification/proofs/agda/Wager/Poly/Proofs.agda b/verification/proofs/agda/Wager/Poly/Proofs.agda new file mode 100644 index 0000000..fa109d7 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Proofs.agda @@ -0,0 +1,135 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. Proofs of T8-Conv, T8-Inst and T8-Closed. +open import Wager.L1.Signature +open import Wager.Grade.Algebra +import Wager.L2.Signature + +module Wager.Poly.Proofs + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Wager.L1.Syntax S +open import Wager.L1.SyntaxLemmas S +open import Wager.L1.Conversion S +open import Wager.L2.Term S TS using (Lit; litTy; Op; carrier; from; to; _at_) +import Wager.L2.Typing S TS ops as C +open import Wager.Poly.Typing S TS ops +open import Wager.Poly.Statements S TS ops + +private + variable + Γ Δ Δ' : Ctx + k j : Kind + +-- Substitution and β. +sub-β : (σ : TySub Δ' Δ) (b : Ty (j ∷ Δ) k) (u : Ty Δ j) → + sub σ (b [ u ]) ≡ sub (exts σ) b [ sub σ u ] +sub-β σ b u = + sub-sub σ (u ∷ₛ ids) b + ∙ cong (λ τ → sub τ b) (subExt pt) + ∙ sym (sub-sub (sub σ u ∷ₛ ids) (exts σ) b) + where + pt : ∀ k x → sub σ ((u ∷ₛ ids) k x) ≡ sub (sub σ u ∷ₛ ids) (exts σ k x) + pt k vz = refl + pt k (vs x) = sym (sub-ren (sub σ u ∷ₛ ids) wk (σ k x) ∙ sub-id (σ k x)) + +sub-resTy : (σ : TySub Δ' Δ) (x : Base ⊎ Prim) (A : Ty Δ ★) → + sub σ (resTy x A) ≡ resTy x (sub σ A) +sub-resTy σ (inl b) A = refl +sub-resTy σ (inr q) A = refl + +t8-conv : T8-Conv +t8-conv σ d-refl = d-refl +t8-conv σ (d-sym d) = d-sym (t8-conv σ d) +t8-conv σ (d-trans d e) = d-trans (t8-conv σ d) (t8-conv σ e) +t8-conv σ (d-beta b u) = + d-trans (d-beta (sub (exts σ) b) (sub σ u)) (≡→DefEq (sym (sub-β σ b u))) +t8-conv σ (d-capp d) = d-capp (t8-conv σ d) +t8-conv σ (d-papp d) = d-papp (t8-conv σ d) +t8-conv σ (d-arr d e) = d-arr (t8-conv σ d) (t8-conv σ e) +t8-conv σ (d-prod d e) = d-prod (t8-conv σ d) (t8-conv σ e) +t8-conv σ (d-sum d e) = d-sum (t8-conv σ d) (t8-conv σ e) +t8-conv σ (d-lam d) = d-lam (t8-conv (exts σ) d) +t8-conv σ (d-app d e) = d-app (t8-conv σ d) (t8-conv σ e) +t8-conv σ (δ-base p b) = δ-base p b +t8-conv σ (δ-capp p c A) = + d-trans (δ-capp p c (sub σ A)) (≡→DefEq (sym (sub-resTy σ (onCon p c) A))) +t8-conv σ (δ-arr p q A B) = δ-arr p q (sub σ A) (sub σ B) +t8-conv σ (δ-prod p A B) = δ-prod p (sub σ A) (sub σ B) +t8-conv σ (δ-sum p A B) = δ-sum p (sub σ A) (sub σ B) + +-- A closed type does not change under a substitution. +sub-⇑ : (σ : TySub Δ' Δ) (A : Ty [] ★) → sub σ (⇑ A) ≡ ⇑ A +sub-⇑ σ A = + sub-ren σ εᵣ A + ∙ cong (λ τ → sub τ A) (subExt (λ k ())) + ∙ sym (sub-ren ids εᵣ A) + ∙ sub-id (ren εᵣ A) + +private + cx-▹ : ∀ {n} (σ : TySub Δ' Δ) (Γ : Cxᵖ Δ n) (A : Ty Δ ★) → + (λ i → sub σ ((Γ ▹ᵖ A) i)) ≡ ((λ i → sub σ (Γ i)) ▹ᵖ sub σ A) + cx-▹ σ Γ A = funExt λ { zero → refl ; (suc i) → refl } + +t8-inst : T8-Inst +t8-inst σ (t-var i) = t-var i +t8-inst σ {Γ = Γ} (t-lam {A = A} d) = + t-lam (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ A) (t8-inst σ d)) +t8-inst σ (t-app d e) = t-app (t8-inst σ d) (t8-inst σ e) +t8-inst σ (t-pair d e) = t-pair (t8-inst σ d) (t8-inst σ e) +t8-inst σ {Γ = Γ} (t-letp {A = A} {B = B} d e) = + t-letp (t8-inst σ d) + (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) + (cx-▹ σ (Γ ▹ᵖ A) B ∙ cong (_▹ᵖ sub σ B) (cx-▹ σ Γ A)) + (t8-inst σ e)) +t8-inst σ (t-inj₁ d) = t-inj₁ (t8-inst σ d) +t8-inst σ (t-inj₂ d) = t-inj₂ (t8-inst σ d) +t8-inst σ {Γ = Γ} (t-case {A = A} {B = B} d l r) = + t-case (t8-inst σ d) + (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ A) (t8-inst σ l)) + (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ B) (t8-inst σ r)) +t8-inst σ (t-lit ℓ) = t-lit ℓ +t8-inst σ (t-step o d) = + subst (λ T → _ ▸ _ ⊢ᵖ _ ∶ T) (sym (sub-⇑ σ (carrier o at to o))) + (t-step o (subst (λ T → _ ▸ _ ⊢ᵖ _ ∶ T) (sub-⇑ σ (carrier o at from o)) (t8-inst σ d))) +t8-inst σ (t-conv d e) = t-conv (t8-inst σ d) (t8-conv σ e) +t8-inst σ (t-sub d le) = t-sub (t8-inst σ d) le + +-- With no type variable, `⇑` is the identity. +⇑-closed : (A : Ty [] ★) → ⇑ A ≡ A +⇑-closed A = cong (λ r → ren r A) (renExt (λ k ())) ∙ ren-id A + +private + cx-C : ∀ {n} (Γ : Cxᵖ [] n) (A : Ty [] ★) → (Γ ▹ᵖ A) ≡ (Γ C.▹ᶜ A) + cx-C Γ A = funExt λ { zero → refl ; (suc i) → refl } + +t8-closed : T8-Closed +t8-closed (t-var i) = C.t-var i +t8-closed {Γ = Γ} (t-lam {A = A} d) = + C.t-lam (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ A) (t8-closed d)) +t8-closed (t-app d e) = C.t-app (t8-closed d) (t8-closed e) +t8-closed (t-pair d e) = C.t-pair (t8-closed d) (t8-closed e) +t8-closed {Γ = Γ} (t-letp {A = A} {B = B} d e) = + C.t-letp (t8-closed d) + (subst (λ G → _ C.▸ G ⊢ _ ∶ _) + (cx-C (Γ ▹ᵖ A) B ∙ cong (C._▹ᶜ B) (cx-C Γ A)) (t8-closed e)) +t8-closed (t-inj₁ d) = C.t-inj₁ (t8-closed d) +t8-closed (t-inj₂ d) = C.t-inj₂ (t8-closed d) +t8-closed {Γ = Γ} (t-case {A = A} {B = B} d l r) = + C.t-case (t8-closed d) + (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ A) (t8-closed l)) + (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ B) (t8-closed r)) +t8-closed (t-lit ℓ) = C.t-lit ℓ +t8-closed (t-step o d) = + subst (λ T → _ C.▸ _ ⊢ _ ∶ T) (sym (⇑-closed (carrier o at to o))) + (C.t-step o (subst (λ T → _ C.▸ _ ⊢ _ ∶ T) (⇑-closed (carrier o at from o)) (t8-closed d))) +t8-closed (t-conv d e) = C.t-conv (t8-closed d) e +t8-closed (t-sub d le) = C.t-sub (t8-closed d) le From 893f830f132545934178b0e6b4985cbbc284db91 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 22:56:19 +0000 Subject: [PATCH 03/11] proof(wager): Stage 8, T8-Conv, T8-Inst and T8-Closed type-check Each transport of a derivation now has an explicit motive: the usage, the term and the other index are named. Agda 2.8.0 checks Wager/Poly/Proofs.agda with --cubical --safe. No frozen statement changed. Co-Authored-By: Claude --- .../proofs/agda/Wager/Poly/Proofs.agda | 43 +++++++++++++------ 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/verification/proofs/agda/Wager/Poly/Proofs.agda b/verification/proofs/agda/Wager/Poly/Proofs.agda index fa109d7..03ab884 100644 --- a/verification/proofs/agda/Wager/Poly/Proofs.agda +++ b/verification/proofs/agda/Wager/Poly/Proofs.agda @@ -74,6 +74,25 @@ sub-⇑ σ A = ∙ sym (sub-ren ids εᵣ A) ∙ sub-id (ren εᵣ A) +-- Transport of a derivation along a path of contexts or of types. +-- The usage, the term and the other index are explicit in each motive. +private + cxᵖ : ∀ {n} {γ : Usage n} {G G' : Cxᵖ Δ n} {t : Tmᵖ Δ n} {A : Ty Δ ★} → + G ≡ G' → γ ▸ G ⊢ᵖ t ∶ A → γ ▸ G' ⊢ᵖ t ∶ A + cxᵖ {γ = γ} {t = t} {A = A} p d = subst (λ G → γ ▸ G ⊢ᵖ t ∶ A) p d + + tyᵖ : ∀ {n} {γ : Usage n} {G : Cxᵖ Δ n} {t : Tmᵖ Δ n} {A A' : Ty Δ ★} → + A ≡ A' → γ ▸ G ⊢ᵖ t ∶ A → γ ▸ G ⊢ᵖ t ∶ A' + tyᵖ {γ = γ} {G = G} {t = t} p d = subst (λ T → γ ▸ G ⊢ᵖ t ∶ T) p d + + cxᶜ : ∀ {n} {γ : Usage n} {G G' : C.Cx n} {t : C.Tm n} {A : Ty [] ★} → + G ≡ G' → γ C.▸ G ⊢ t ∶ A → γ C.▸ G' ⊢ t ∶ A + cxᶜ {γ = γ} {t = t} {A = A} p d = subst (λ G → γ C.▸ G ⊢ t ∶ A) p d + + tyᶜ : ∀ {n} {γ : Usage n} {G : C.Cx n} {t : C.Tm n} {A A' : Ty [] ★} → + A ≡ A' → γ C.▸ G ⊢ t ∶ A → γ C.▸ G ⊢ t ∶ A' + tyᶜ {γ = γ} {G = G} {t = t} p d = subst (λ T → γ C.▸ G ⊢ t ∶ T) p d + private cx-▹ : ∀ {n} (σ : TySub Δ' Δ) (Γ : Cxᵖ Δ n) (A : Ty Δ ★) → (λ i → sub σ ((Γ ▹ᵖ A) i)) ≡ ((λ i → sub σ (Γ i)) ▹ᵖ sub σ A) @@ -82,24 +101,24 @@ private t8-inst : T8-Inst t8-inst σ (t-var i) = t-var i t8-inst σ {Γ = Γ} (t-lam {A = A} d) = - t-lam (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ A) (t8-inst σ d)) + t-lam (cxᵖ (cx-▹ σ Γ A) (t8-inst σ d)) t8-inst σ (t-app d e) = t-app (t8-inst σ d) (t8-inst σ e) t8-inst σ (t-pair d e) = t-pair (t8-inst σ d) (t8-inst σ e) t8-inst σ {Γ = Γ} (t-letp {A = A} {B = B} d e) = t-letp (t8-inst σ d) - (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) + (cxᵖ (cx-▹ σ (Γ ▹ᵖ A) B ∙ cong (_▹ᵖ sub σ B) (cx-▹ σ Γ A)) (t8-inst σ e)) t8-inst σ (t-inj₁ d) = t-inj₁ (t8-inst σ d) t8-inst σ (t-inj₂ d) = t-inj₂ (t8-inst σ d) t8-inst σ {Γ = Γ} (t-case {A = A} {B = B} d l r) = t-case (t8-inst σ d) - (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ A) (t8-inst σ l)) - (subst (λ G → _ ▸ G ⊢ᵖ _ ∶ _) (cx-▹ σ Γ B) (t8-inst σ r)) + (cxᵖ (cx-▹ σ Γ A) (t8-inst σ l)) + (cxᵖ (cx-▹ σ Γ B) (t8-inst σ r)) t8-inst σ (t-lit ℓ) = t-lit ℓ t8-inst σ (t-step o d) = - subst (λ T → _ ▸ _ ⊢ᵖ _ ∶ T) (sym (sub-⇑ σ (carrier o at to o))) - (t-step o (subst (λ T → _ ▸ _ ⊢ᵖ _ ∶ T) (sub-⇑ σ (carrier o at from o)) (t8-inst σ d))) + tyᵖ (sym (sub-⇑ σ (carrier o at to o))) + (t-step o (tyᵖ (sub-⇑ σ (carrier o at from o)) (t8-inst σ d))) t8-inst σ (t-conv d e) = t-conv (t8-inst σ d) (t8-conv σ e) t8-inst σ (t-sub d le) = t-sub (t8-inst σ d) le @@ -114,22 +133,22 @@ private t8-closed : T8-Closed t8-closed (t-var i) = C.t-var i t8-closed {Γ = Γ} (t-lam {A = A} d) = - C.t-lam (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ A) (t8-closed d)) + C.t-lam (cxᶜ (cx-C Γ A) (t8-closed d)) t8-closed (t-app d e) = C.t-app (t8-closed d) (t8-closed e) t8-closed (t-pair d e) = C.t-pair (t8-closed d) (t8-closed e) t8-closed {Γ = Γ} (t-letp {A = A} {B = B} d e) = C.t-letp (t8-closed d) - (subst (λ G → _ C.▸ G ⊢ _ ∶ _) + (cxᶜ (cx-C (Γ ▹ᵖ A) B ∙ cong (C._▹ᶜ B) (cx-C Γ A)) (t8-closed e)) t8-closed (t-inj₁ d) = C.t-inj₁ (t8-closed d) t8-closed (t-inj₂ d) = C.t-inj₂ (t8-closed d) t8-closed {Γ = Γ} (t-case {A = A} {B = B} d l r) = C.t-case (t8-closed d) - (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ A) (t8-closed l)) - (subst (λ G → _ C.▸ G ⊢ _ ∶ _) (cx-C Γ B) (t8-closed r)) + (cxᶜ (cx-C Γ A) (t8-closed l)) + (cxᶜ (cx-C Γ B) (t8-closed r)) t8-closed (t-lit ℓ) = C.t-lit ℓ t8-closed (t-step o d) = - subst (λ T → _ C.▸ _ ⊢ _ ∶ T) (sym (⇑-closed (carrier o at to o))) - (C.t-step o (subst (λ T → _ C.▸ _ ⊢ _ ∶ T) (⇑-closed (carrier o at from o)) (t8-closed d))) + tyᶜ (sym (⇑-closed (carrier o at to o))) + (C.t-step o (tyᶜ (⇑-closed (carrier o at from o)) (t8-closed d))) t8-closed (t-conv d e) = C.t-conv (t8-closed d) e t8-closed (t-sub d le) = C.t-sub (t8-closed d) le From d7f4189fda498f94b1a56f8c1b28015672ff5f72 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:01:36 +0000 Subject: [PATCH 04/11] proof(wager): Stage 8, second freeze: 14 statements before their proofs New definitions (no proof): Wager/Poly/Coercion.agda. Open source types, open representational coercions, their translation to 1 open term, and the list of trope operations of a term. Frozen statements, each a type that Agda 2.8.0 checks: - Poly/Statements.agda: T8-Closed-Instance, T8-Instance-Progress, T8-Instance-Preservation. The 3 statements of the first freeze did not change. - Poly/CoercionStatements.agda: T8-Type-Instance, T8-Coercion-Typed, T8-Coercion-Instance, T8-Ops-Rigid, T8-No-Uniform-Unwrap. - Poly/RoleStatements.agda: T8-Role, T8-Role-Representational, T8-Role-Phantom, T8-Role-Nominal. - Poly/IdentityStatements.agda: T8-Evidence-Rigid, T8-Gadt-Not-Open. No proof of these 14 statements exists at this commit. Co-Authored-By: Claude --- .../proofs/agda/Wager/Poly/Coercion.agda | 240 ++++++++++++++++++ .../agda/Wager/Poly/CoercionStatements.agda | 72 ++++++ .../agda/Wager/Poly/IdentityStatements.agda | 52 ++++ .../agda/Wager/Poly/RoleStatements.agda | 83 ++++++ .../proofs/agda/Wager/Poly/Statements.agda | 35 ++- 5 files changed, 481 insertions(+), 1 deletion(-) create mode 100644 verification/proofs/agda/Wager/Poly/Coercion.agda create mode 100644 verification/proofs/agda/Wager/Poly/CoercionStatements.agda create mode 100644 verification/proofs/agda/Wager/Poly/IdentityStatements.agda create mode 100644 verification/proofs/agda/Wager/Poly/RoleStatements.agda diff --git a/verification/proofs/agda/Wager/Poly/Coercion.agda b/verification/proofs/agda/Wager/Poly/Coercion.agda new file mode 100644 index 0000000..66437a4 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Coercion.agda @@ -0,0 +1,240 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. Coercions at open types. Definitions only. +-- +-- An open source type has type variables. Its other leaves are closed +-- source types. An open coercion is built from: +-- the identity, at each open type; +-- each closed representational coercion of `Wager.FC.Coercion`; +-- symmetry, transitivity, and congruence for a function, a pair and +-- a sum. +-- Its translation is ONE open term of `Wager.Poly.Term`. +-- +-- A newtype that is applied to a type variable is not an open source +-- type here. The reason is in `T8-No-Uniform-Unwrap`: a trope operation +-- has a closed carrier (`Wager.L2.Signature.TSig`). +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Poly.Coercion + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Cubical.Data.List.Base using (_++_) + +open import Wager.Role.Role +open import Wager.FC.Types SS hiding (inst) +open import Wager.FC.Coercion SS +open import Wager.Trans.Target SS Sc ops +open import Wager.Trans.Coercion SS Sc ops using (Tm; Iso; coI; coerceT) +import Wager.L2.Term tSig tTSig as C +open import Wager.Poly.Term tSig tTSig public +open GradeOps ops using (𝟙) + +private + variable + n : ℕ + Δ : Ctx + τ σ : STy + +------------------------------------------------------------------------ +-- Open source types. + +infixr 20 _⇒ᵒ_ +infixr 30 _+ᵒ_ +infixr 40 _×ᵒ_ + +data OTy (Δ : Ctx) : Type where + ovar : Var Δ ★ → OTy Δ + -- A closed source type. + clo : STy → OTy Δ + _⇒ᵒ_ : OTy Δ → OTy Δ → OTy Δ + _×ᵒ_ : OTy Δ → OTy Δ → OTy Δ + _+ᵒ_ : OTy Δ → OTy Δ → OTy Δ + +private + variable + θ θ' φ φ' χ : OTy Δ + +-- An instantiation of the source: a closed source type for each type +-- variable of the kind ★. +SInst : Ctx → Type +SInst Δ = Var Δ ★ → STy + +infix 45 _⟦_⟧ +_⟦_⟧ : OTy Δ → SInst Δ → STy +ovar x ⟦ ρ ⟧ = ρ x +clo τ ⟦ ρ ⟧ = τ +(θ ⇒ᵒ φ) ⟦ ρ ⟧ = θ ⟦ ρ ⟧ ⇒ˢ φ ⟦ ρ ⟧ +(θ ×ᵒ φ) ⟦ ρ ⟧ = θ ⟦ ρ ⟧ ×ˢ φ ⟦ ρ ⟧ +(θ +ᵒ φ) ⟦ ρ ⟧ = θ ⟦ ρ ⟧ +ˢ φ ⟦ ρ ⟧ + +-- The translation of an open source type: an open type of the target. +Tᵒ : OTy Δ → Ty Δ ★ +Tᵒ (ovar x) = var x +Tᵒ (clo τ) = ⇑ (T τ) +Tᵒ (θ ⇒ᵒ φ) = arr 𝟙 (Tᵒ θ) (Tᵒ φ) +Tᵒ (θ ×ᵒ φ) = Tᵒ θ ⊗ Tᵒ φ +Tᵒ (θ +ᵒ φ) = Tᵒ θ ⊕ Tᵒ φ + +-- A substitution of the target agrees with an instantiation of the +-- source when it gives each type variable of the kind ★ the +-- translation of its source type. +Agrees : TySub [] Δ → SInst Δ → Type +Agrees {Δ} s ρ = (x : Var Δ ★) → s ★ x ≡ T (ρ x) + +------------------------------------------------------------------------ +-- Open representational coercions. + +data Coᵒ {Δ : Ctx} : OTy Δ → OTy Δ → Type where + o-refl : Coᵒ θ θ + o-clo : Co rep τ σ → Coᵒ (clo τ) (clo σ) + o-sym : Coᵒ θ φ → Coᵒ φ θ + o-trans : Coᵒ θ φ → Coᵒ φ χ → Coᵒ θ χ + o-arr : Coᵒ θ θ' → Coᵒ φ φ' → Coᵒ (θ ⇒ᵒ φ) (θ' ⇒ᵒ φ') + o-prod : Coᵒ θ θ' → Coᵒ φ φ' → Coᵒ (θ ×ᵒ φ) (θ' ×ᵒ φ') + o-sum : Coᵒ θ θ' → Coᵒ φ φ' → Coᵒ (θ +ᵒ φ) (θ' +ᵒ φ') + +-- Each instance of an open coercion is a closed representational +-- coercion of the source calculus. +infix 45 _⟦_⟧ᶜ +_⟦_⟧ᶜ : {θ φ : OTy Δ} → Coᵒ θ φ → (ρ : SInst Δ) → Co rep (θ ⟦ ρ ⟧) (φ ⟦ ρ ⟧) +o-refl ⟦ ρ ⟧ᶜ = c-sub c-refl +o-clo γ ⟦ ρ ⟧ᶜ = γ +o-sym c ⟦ ρ ⟧ᶜ = c-sym (c ⟦ ρ ⟧ᶜ) +o-trans c d ⟦ ρ ⟧ᶜ = c-trans (c ⟦ ρ ⟧ᶜ) (d ⟦ ρ ⟧ᶜ) +o-arr c d ⟦ ρ ⟧ᶜ = c-arr (c ⟦ ρ ⟧ᶜ) (d ⟦ ρ ⟧ᶜ) +o-prod c d ⟦ ρ ⟧ᶜ = c-prod (c ⟦ ρ ⟧ᶜ) (d ⟦ ρ ⟧ᶜ) +o-sum c d ⟦ ρ ⟧ᶜ = c-sum (c ⟦ ρ ⟧ᶜ) (d ⟦ ρ ⟧ᶜ) + +------------------------------------------------------------------------ +-- Term transformers on open terms. Each definition has the text of its +-- definition in `Wager.Trans.Coercion`, with the types in Δ. + +Trᵖ : Ctx → Type +Trᵖ Δ = ∀ {n} → Tmᵖ Δ n → Tmᵖ Δ n + +record Isoᵖ (Δ : Ctx) : Type where + constructor isoᵖ + field + fwdᵖ : Trᵖ Δ + bwdᵖ : Trᵖ Δ +open Isoᵖ public + +idIsoᵖ : Isoᵖ Δ +idIsoᵖ = isoᵖ (λ t → t) (λ t → t) + +swapIsoᵖ : Isoᵖ Δ → Isoᵖ Δ +swapIsoᵖ i = isoᵖ (bwdᵖ i) (fwdᵖ i) + +compIsoᵖ : Isoᵖ Δ → Isoᵖ Δ → Isoᵖ Δ +compIsoᵖ i j = isoᵖ (λ t → fwdᵖ j (fwdᵖ i t)) (λ t → bwdᵖ i (bwdᵖ j t)) + +arrMapᵖ : (X A : Ty Δ ★) → Trᵖ Δ → Trᵖ Δ → Trᵖ Δ +arrMapᵖ X A h g t = + tapp (tlam 𝟙 X (tlam 𝟙 A (g (tapp (tvar (suc zero)) (h (tvar zero)))))) t + +arrIsoᵖ : (A A' B B' : Ty Δ ★) → Isoᵖ Δ → Isoᵖ Δ → Isoᵖ Δ +arrIsoᵖ A A' B B' i j = + isoᵖ (arrMapᵖ (arr 𝟙 A B) A' (bwdᵖ i) (fwdᵖ j)) + (arrMapᵖ (arr 𝟙 A' B') A (fwdᵖ i) (bwdᵖ j)) + +prodMapᵖ : Trᵖ Δ → Trᵖ Δ → Trᵖ Δ +prodMapᵖ f g t = letp t (pair (f (tvar (suc zero))) (g (tvar zero))) + +prodIsoᵖ : Isoᵖ Δ → Isoᵖ Δ → Isoᵖ Δ +prodIsoᵖ i j = isoᵖ (prodMapᵖ (fwdᵖ i) (fwdᵖ j)) (prodMapᵖ (bwdᵖ i) (bwdᵖ j)) + +sumMapᵖ : Trᵖ Δ → Trᵖ Δ → Trᵖ Δ +sumMapᵖ f g t = case t (inj₁ (f (tvar zero))) (inj₂ (g (tvar zero))) + +sumIsoᵖ : Isoᵖ Δ → Isoᵖ Δ → Isoᵖ Δ +sumIsoᵖ i j = isoᵖ (sumMapᵖ (fwdᵖ i) (fwdᵖ j)) (sumMapᵖ (bwdᵖ i) (bwdᵖ j)) + +-- The two trope transitions of a newtype instance. The instance is +-- closed: an operation of the signature has a closed carrier. +stepIsoᵖ : Inst → Isoᵖ Δ +stepIsoᵖ x = isoᵖ (λ t → step (unwrap , x) t) (λ t → step (wrap , x) t) + +bodyIsoᵖ : Body Base Fam → (X Y : Ty [] ★) → Isoᵖ Δ → Isoᵖ Δ +bodyIsoᵖ bvar X Y i = i +bodyIsoᵖ (bbase b) X Y i = idIsoᵖ +bodyIsoᵖ (barr β γ) X Y i = + arrIsoᵖ (⇑ (TB β X)) (⇑ (TB β Y)) (⇑ (TB γ X)) (⇑ (TB γ Y)) + (bodyIsoᵖ β X Y i) (bodyIsoᵖ γ X Y i) +bodyIsoᵖ (bprod β γ) X Y i = prodIsoᵖ (bodyIsoᵖ β X Y i) (bodyIsoᵖ γ X Y i) +bodyIsoᵖ (bsum β γ) X Y i = sumIsoᵖ (bodyIsoᵖ β X Y i) (bodyIsoᵖ γ X Y i) +bodyIsoᵖ (bfam F β) X Y i = idIsoᵖ + +ntIsoᵖ : (N : N₁) (τ σ : STy) → Isoᵖ Δ → Isoᵖ Δ +ntIsoᵖ N τ σ i = + isoᵖ (λ t → step (wrap , inr (N , σ)) (fwdᵖ b (step (unwrap , inr (N , τ)) t))) + (λ t → step (wrap , inr (N , τ)) (bwdᵖ b (step (unwrap , inr (N , σ)) t))) + where b = bodyIsoᵖ (body N) (T τ) (T σ) i + +-- A closed coercion, as a transformer of open terms. +coIᵖ : (r : Role) → Co r τ σ → Isoᵖ Δ +coIᵖ nom γ = idIsoᵖ +coIᵖ ph γ = idIsoᵖ +coIᵖ rep (c-sym γ) = swapIsoᵖ (coIᵖ rep γ) +coIᵖ rep (c-trans γ δ) = compIsoᵖ (coIᵖ rep γ) (coIᵖ rep δ) +coIᵖ rep (c-sub γ) = idIsoᵖ +coIᵖ rep (c-arr {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + arrIsoᵖ (⇑ (T τ)) (⇑ (T τ')) (⇑ (T σ)) (⇑ (T σ')) (coIᵖ rep γ) (coIᵖ rep δ) +coIᵖ rep (c-prod γ δ) = prodIsoᵖ (coIᵖ rep γ) (coIᵖ rep δ) +coIᵖ rep (c-sum γ δ) = sumIsoᵖ (coIᵖ rep γ) (coIᵖ rep δ) +coIᵖ rep (c-nt₁ {τ = τ} {σ = σ} N γ) = ntIsoᵖ N τ σ (coIᵖ (mulG rep (role N)) γ) +coIᵖ rep (c-ax₀ N) = stepIsoᵖ (inl N) +coIᵖ rep (c-ax₁ N τ) = stepIsoᵖ (inr (N , τ)) + +-- THE TRANSLATION OF AN OPEN COERCION. +coIᵒ : {θ φ : OTy Δ} → Coᵒ θ φ → Isoᵖ Δ +coIᵒ o-refl = idIsoᵖ +coIᵒ (o-clo γ) = coIᵖ rep γ +coIᵒ (o-sym c) = swapIsoᵖ (coIᵒ c) +coIᵒ (o-trans c d) = compIsoᵖ (coIᵒ c) (coIᵒ d) +coIᵒ (o-arr {θ = θ} {θ' = θ'} {φ = φ} {φ' = φ'} c d) = + arrIsoᵖ (Tᵒ θ) (Tᵒ θ') (Tᵒ φ) (Tᵒ φ') (coIᵒ c) (coIᵒ d) +coIᵒ (o-prod c d) = prodIsoᵖ (coIᵒ c) (coIᵒ d) +coIᵒ (o-sum c d) = sumIsoᵖ (coIᵒ c) (coIᵒ d) + +-- The open coercion as one open function of the target. +coerceᵒ : {θ φ : OTy Δ} → Coᵒ θ φ → Tmᵖ Δ n +coerceᵒ {θ = θ} c = tlam 𝟙 (Tᵒ θ) (fwdᵖ (coIᵒ c) (tvar zero)) + +------------------------------------------------------------------------ +-- The trope operations of a term, in the order of the text. + +opsOf : Tm n → List C.Op +opsOf (C.tvar i) = [] +opsOf (C.tlam q A b) = opsOf b +opsOf (C.tapp f a) = opsOf f ++ opsOf a +opsOf (C.pair s t) = opsOf s ++ opsOf t +opsOf (C.letp s b) = opsOf s ++ opsOf b +opsOf (C.inj₁ t) = opsOf t +opsOf (C.inj₂ t) = opsOf t +opsOf (C.case s l r) = opsOf s ++ (opsOf l ++ opsOf r) +opsOf (C.lit ℓ) = [] +opsOf (C.step o t) = o ∷ opsOf t + +opsOfᵖ : Tmᵖ Δ n → List C.Op +opsOfᵖ (tvar i) = [] +opsOfᵖ (tlam q A b) = opsOfᵖ b +opsOfᵖ (tapp f a) = opsOfᵖ f ++ opsOfᵖ a +opsOfᵖ (pair s t) = opsOfᵖ s ++ opsOfᵖ t +opsOfᵖ (letp s b) = opsOfᵖ s ++ opsOfᵖ b +opsOfᵖ (inj₁ t) = opsOfᵖ t +opsOfᵖ (inj₂ t) = opsOfᵖ t +opsOfᵖ (case s l r) = opsOfᵖ s ++ (opsOfᵖ l ++ opsOfᵖ r) +opsOfᵖ (lit ℓ) = [] +opsOfᵖ (step o t) = o ∷ opsOfᵖ t diff --git a/verification/proofs/agda/Wager/Poly/CoercionStatements.agda b/verification/proofs/agda/Wager/Poly/CoercionStatements.agda new file mode 100644 index 0000000..521a12d --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/CoercionStatements.agda @@ -0,0 +1,72 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The statements about coercions at open types, frozen before +-- their proofs. This file imports definitions and no proof. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Poly.CoercionStatements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + +open import Cubical.Data.Nat.Base using (ℕ) +open import Cubical.Data.Sigma using (_,_) +open import Cubical.Data.Sum.Base using (inr) + +open import Wager.Role.Role using (rep) +open import Wager.FC.Types SS using (STy; N₁) +open import Wager.FC.Coercion SS using (Co; c-ax₁) +open SSig SS using (WellRoled) +open import Wager.Trans.Target SS Sc ops +open import Wager.Trans.Coercion SS Sc ops using (coerceT) +open import Wager.Poly.Coercion SS Sc ops +open import Wager.Poly.Typing tSig tTSig ops using (Cxᵖ; 0ᵘ; _▸_⊢ᵖ_∶_) +open GradeOps ops using (𝟙) + +-- T8-Type-Instance. The translation of types commutes with +-- instantiation: the instance of the translation of an open source type +-- is the translation of the instance. +T8-Type-Instance : Type +T8-Type-Instance = ∀ {Δ} (θ : OTy Δ) (ρ : SInst Δ) (s : TySub [] Δ) → + Agrees s ρ → sub s (Tᵒ θ) ≡ T (θ ⟦ ρ ⟧) + +-- T8-Coercion-Typed. ONE POLYMORPHIC COERCION. For a source signature +-- that passes the role check, and for the laws of a grade algebra, the +-- translation of an open coercion is one typed open function of the +-- target. It uses no term variable of the context. +T8-Coercion-Typed : Type +T8-Coercion-Typed = GradeLaws ops → WellRoled → + ∀ {Δ} {θ φ : OTy Δ} (c : Coᵒ θ φ) {n} (Γ : Cxᵖ Δ n) → + 0ᵘ ▸ Γ ⊢ᵖ coerceᵒ c ∶ arr 𝟙 (Tᵒ θ) (Tᵒ φ) + +-- T8-Coercion-Instance. Each closed instance of the open function is +-- the closed coercion function of `Wager.Trans.Coercion`, for the +-- instance of the coercion. The two terms are equal as terms. +T8-Coercion-Instance : Type +T8-Coercion-Instance = ∀ {Δ} {θ φ : OTy Δ} (c : Coᵒ θ φ) (ρ : SInst Δ) + (s : TySub [] Δ) → Agrees s ρ → ∀ {n} → + ⌊ inst s (coerceᵒ {n = n} c) ⌋ ≡ coerceT (c ⟦ ρ ⟧ᶜ) + +-- T8-Ops-Rigid. Instantiation does not change a trope operation: each +-- closed instance of an open term has the operations of the open term. +T8-Ops-Rigid : Type +T8-Ops-Rigid = ∀ {Δ n} (s : TySub [] Δ) (t : Tmᵖ Δ n) → + opsOf ⌊ inst s t ⌋ ≡ opsOfᵖ t + +-- T8-No-Uniform-Unwrap. THE LIMIT. Let N be a newtype with a +-- parameter. If one open term has, at two instantiations, the two +-- closed coercion functions `N τ₁ → body` and `N τ₂ → body`, then τ₁ +-- and τ₂ are one source type. So no open term is the coercion +-- `N a → body` at each instance of a type variable a. +T8-No-Uniform-Unwrap : Type +T8-No-Uniform-Unwrap = ∀ {Δ} (N : N₁) (τ₁ τ₂ : STy) (t : Tmᵖ Δ 0) + (s₁ s₂ : TySub [] Δ) → + ⌊ inst s₁ t ⌋ ≡ coerceT (c-ax₁ N τ₁) → + ⌊ inst s₂ t ⌋ ≡ coerceT (c-ax₁ N τ₂) → + τ₁ ≡ τ₂ diff --git a/verification/proofs/agda/Wager/Poly/IdentityStatements.agda b/verification/proofs/agda/Wager/Poly/IdentityStatements.agda new file mode 100644 index 0000000..b9c1aac --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/IdentityStatements.agda @@ -0,0 +1,52 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The GADT program of Stage 6 and open types: the statements, +-- frozen before their proofs. +-- +-- The signature is the signature of `Wager.Identity.Instance`, the one +-- signature of this development that has an identity family. The +-- start has one base constant b₀ at least. +open import Cubical.Foundations.Prelude +open import Wager.Grade.Algebra + +module Wager.Poly.IdentityStatements + (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) (b₀ : B₀) where + +open import Cubical.Data.Sigma using (Σ-syntax) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Identity.Instance B₀ L₀ ty₀ ops +import Wager.Identity.Family +open import Wager.L1.Syntax sig +open import Wager.L1.Conversion sig +open Wager.Identity.Family.IdFamily family using (Id) + +-- The base type of the start. +I₀ : Ty [] ★ +I₀ = base (cb b₀) + +-- The data of the GADT program of Stage 6, part 2, at the closed type +-- α (`Wager.Examples.Stage6Identity.Gⁱ`, with b₀ for `int`). +Gᵍ : Ty [] ★ → Ty [] ★ +Gᵍ α = (base (Id α I₀) ⊗ α) ⊕ (base (Id α (I₀ ⊕ I₀)) ⊗ α) + +-- T8-Evidence-Rigid. No open type with one type variable has the +-- evidence type `Id α B` as its instance at each closed type α. +-- The identity family is a family of base constants, and a +-- substitution does not change a base constant. +T8-Evidence-Rigid : Type +T8-Evidence-Rigid = + (B : Ty [] ★) → + ¬ (Σ[ E ∈ Ty (★ ∷ []) ★ ] (∀ α → DefEq (E [ α ]) (base (Id α B)))) + +-- T8-Gadt-Not-Open. No open type with one type variable has the data +-- type of the GADT program as its instance at each closed type α. +-- The statement is about a type. It is not about each encoding of the +-- program (DESIGN-CHOICES.adoc, DC-8.6). +T8-Gadt-Not-Open : Type +T8-Gadt-Not-Open = + ¬ (Σ[ G ∈ Ty (★ ∷ []) ★ ] (∀ α → DefEq (G [ α ]) (Gᵍ α))) diff --git a/verification/proofs/agda/Wager/Poly/RoleStatements.agda b/verification/proofs/agda/Wager/Poly/RoleStatements.agda new file mode 100644 index 0000000..74785f5 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/RoleStatements.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The role of a type variable: the statements, frozen before +-- their proofs. +-- +-- This file imports the definitions `LR` and `EnvLR` of the logical +-- relation from `Wager.Role.Noninterference`. It uses no lemma of that +-- module. +open import Cubical.Foundations.Prelude +open import Wager.Role.Signature +open import Wager.Role.Table + +module Wager.Poly.RoleStatements (RS : RoleSig) where + +open import Cubical.Data.Bool.Base using (true) +open import Wager.Role.Role +import Wager.L1.Syntax +import Wager.L1.Eval +import Wager.L1.Kinding +import Wager.Role.RepEq +import Wager.Role.Validity +import Wager.Role.Noninterference + +-- For each composition table T. +module ForTable (T : RoleTable) where + open RoleTable T using (mul) + open Wager.L1.Syntax (toSig RS) + open Wager.L1.Eval (toSig RS) + open Wager.L1.Kinding (toSig RS) (tableOps T) + open Wager.Role.Validity RS mul + open Wager.Role.Noninterference RS T using (EnvLR) + + -- T8-Role. Noninterference for an open type. Let the signature + -- respect its declared grades. Let A be a type in a context Δ of + -- type variables, and let kinding accept the usage vector γ for A. + -- Let two closed instantiations give each variable x two types that + -- the observer `ρ · γ x` cannot tell apart. Then the observer ρ + -- cannot tell the two instances of A apart. + T8-Role : Type + T8-Role = + Valid → + ∀ {Δ} {γ : KUsage Δ} {A : Ty Δ ★} → γ ⊢ᵏ A → + (ρ : Role) (s s' : TySub [] Δ) → + EnvLR ρ γ (λ k x → eval (s k x) idEnv) (λ k x → eval (s' k x) idEnv) → + R★ ρ (nf (sub s A)) (nf (sub s' A)) + +-- The lawful table, and one type variable of the kind ★. +module Lawful where + open Wager.L1.Syntax (toSig RS) + open Wager.L1.Eval (toSig RS) + open Wager.L1.Kinding (toSig RS) (tableOps tableZ) + open Wager.Role.RepEq RS + open Wager.Role.Validity RS mulZ + + -- T8-Role-Representational. A type variable at a grade that is at + -- most representational: two instances at equivalent types are + -- equivalent. + T8-Role-Representational : Type + T8-Role-Representational = + Valid → + ∀ {r : Role} {A : Ty (★ ∷ []) ★} → (0ᵏ ▹ᵏ r) ⊢ᵏ A → + leR r rep ≡ true → + (B C : Ty [] ★) → nf B ≈ nf C → nf (A [ B ]) ≈ nf (A [ C ]) + + -- T8-Role-Phantom. A type variable at the grade phantom: each two + -- instances have one normal form. + T8-Role-Phantom : Type + T8-Role-Phantom = + Valid → + ∀ {A : Ty (★ ∷ []) ★} → (0ᵏ ▹ᵏ ph) ⊢ᵏ A → + (B C : Ty [] ★) → nf (A [ B ]) ≡ nf (A [ C ]) + + -- T8-Role-Nominal. A type variable at the grade nominal: two + -- instances at types with one normal form have one normal form. No + -- kinding hypothesis is needed. + T8-Role-Nominal : Type + T8-Role-Nominal = + ∀ (A : Ty (★ ∷ []) ★) (B C : Ty [] ★) → + nf B ≡ nf C → nf (A [ B ]) ≡ nf (A [ C ]) diff --git a/verification/proofs/agda/Wager/Poly/Statements.agda b/verification/proofs/agda/Wager/Poly/Statements.agda index 8be7401..8798ef6 100644 --- a/verification/proofs/agda/Wager/Poly/Statements.agda +++ b/verification/proofs/agda/Wager/Poly/Statements.agda @@ -14,9 +14,11 @@ module Wager.Poly.Statements open import Cubical.Foundations.Prelude open import Cubical.Data.Nat.Base using (ℕ) +open import Cubical.Data.Sigma using (Σ-syntax) +open import Cubical.Data.Sum.Base using (_⊎_) open import Wager.L1.Syntax S open import Wager.L1.Conversion S -open import Wager.L2.Typing S TS ops using (_▸_⊢_∶_) +open import Wager.L2.Typing S TS ops using (_▸_⊢_∶_; Tm; Value; _⟶_) open import Wager.Poly.Typing S TS ops -- T8-Conv. Conversion of types is stable under a substitution of types. @@ -38,3 +40,34 @@ T8-Inst = ∀ {Δ Δ' n} (σ : TySub Δ' Δ) {γ : Usage n} {Γ : Cxᵖ Δ n} T8-Closed : Type T8-Closed = ∀ {n} {γ : Usage n} {Γ : Cxᵖ [] n} {t : Tmᵖ [] n} {A : Ty [] ★} → γ ▸ Γ ⊢ᵖ t ∶ A → γ ▸ Γ ⊢ ⌊ t ⌋ ∶ A + +------------------------------------------------------------------------ +-- The second freeze of Stage 8. The 3 statements above did not change. + +-- T8-Closed-Instance. Each closed instance of a typed open term is a +-- typed term of the target calculus of stages 1 to 5, with the same +-- usage. Its type and its context are the instances. +T8-Closed-Instance : Type +T8-Closed-Instance = ∀ {Δ n} (σ : TySub [] Δ) {γ : Usage n} {Γ : Cxᵖ Δ n} + {t : Tmᵖ Δ n} {A : Ty Δ ★} → + γ ▸ Γ ⊢ᵖ t ∶ A → + γ ▸ (λ i → sub σ (Γ i)) ⊢ ⌊ inst σ t ⌋ ∶ sub σ A + +-- T8-Instance-Progress. T0, part 3 applies to each closed instance: an +-- instance of a typed open term with no term variable is a value, or +-- it can make one reduction step. +T8-Instance-Progress : Type +T8-Instance-Progress = ∀ {Δ} (σ : TySub [] Δ) {γ : Usage 0} {Γ : Cxᵖ Δ 0} + {t : Tmᵖ Δ 0} {A : Ty Δ ★} → + γ ▸ Γ ⊢ᵖ t ∶ A → + Value ⌊ inst σ t ⌋ ⊎ (Σ[ t' ∈ Tm 0 ] (⌊ inst σ t ⌋ ⟶ t')) + +-- T8-Instance-Preservation. T0, part 2 applies to each closed instance, +-- when the operations satisfy the laws of a grade algebra: a reduction +-- step of an instance keeps the instance of the type, and the usage. +T8-Instance-Preservation : Type +T8-Instance-Preservation = GradeLaws ops → + ∀ {Δ n} (σ : TySub [] Δ) {γ : Usage n} {Γ : Cxᵖ Δ n} + {t : Tmᵖ Δ n} {A : Ty Δ ★} {t' : Tm n} → + γ ▸ Γ ⊢ᵖ t ∶ A → ⌊ inst σ t ⌋ ⟶ t' → + γ ▸ (λ i → sub σ (Γ i)) ⊢ t' ∶ sub σ A From f2c81419fccbc9256a49d274afb3e24f17856afa Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:07:18 +0000 Subject: [PATCH 05/11] proof(wager): Stage 8, proofs of the 14 statements of the second freeze Agda 2.8.0 checks each module with --cubical --safe. No frozen statement changed. - Poly/Proofs.agda: t8-closed-instance, t8-instance-progress, t8-instance-preservation. - Poly/CoercionProofs.agda: t8-type-instance, t8-coercion-typed, t8-coercion-instance, t8-ops-rigid, t8-no-uniform-unwrap. - Poly/Role.agda: t8-role, t8-role-representational, t8-role-phantom, t8-role-nominal. - Poly/IdentityRigid.agda: t8-evidence-rigid, t8-gadt-not-open. The index modules, the examples, the gate watch and the records are not in this commit. The MANIFEST does not list the Poly modules yet, so the gate is red at this commit. Co-Authored-By: Claude --- .../agda/Wager/Poly/CoercionProofs.agda | 410 ++++++++++++++++++ .../proofs/agda/Wager/Poly/IdentityRigid.agda | 132 ++++++ .../proofs/agda/Wager/Poly/Proofs.agda | 19 + verification/proofs/agda/Wager/Poly/Role.agda | 79 ++++ 4 files changed, 640 insertions(+) create mode 100644 verification/proofs/agda/Wager/Poly/CoercionProofs.agda create mode 100644 verification/proofs/agda/Wager/Poly/IdentityRigid.agda create mode 100644 verification/proofs/agda/Wager/Poly/Role.agda diff --git a/verification/proofs/agda/Wager/Poly/CoercionProofs.agda b/verification/proofs/agda/Wager/Poly/CoercionProofs.agda new file mode 100644 index 0000000..2688af1 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/CoercionProofs.agda @@ -0,0 +1,410 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. Coercions at open types: proofs. +-- +-- 1. The translation of types commutes with instantiation. +-- 2. Instantiation does not change a trope operation. So one open +-- term is not the unwrap of a newtype at each instance of a type +-- variable. +-- 3. The translation of an open coercion is typed. The proof has the +-- shape of the proof of Stage 4 (`Wager.Trans.Typing`), with the +-- types in Δ. +-- 4. Each closed instance of the translation of an open coercion is +-- the translation of the instance, as a term. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Poly.CoercionProofs + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + +open import Cubical.Data.Bool.Base using (true; false) +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; fst; snd) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Cubical.Data.List.Base using (_++_) + +open import Wager.Grade.Finite using (false≢true) +open import Wager.Role.Role +open import Wager.FC.Types SS hiding (inst) +open import Wager.FC.Coercion SS +open import Wager.Trans.Target SS Sc ops +open import Wager.Trans.Nominal SS Sc ops using (nominal-defeq; T-inst; T-embE) +open import Wager.Trans.Coercion SS Sc ops + using ( Tm; Tr; Iso; fwd; bwd; idIso; swapIso; compIso; arrMap; arrIso + ; prodMap; prodIso; sumMap; sumIso; stepIso; bodyIso; ntIso; coI; coerceT ) +import Wager.L2.Term tSig tTSig as C +import Wager.Trans.Typing +open import Wager.L1.Conversion tSig +open import Wager.Poly.Coercion SS Sc ops +open import Wager.Poly.Typing tSig tTSig ops + using ( Usage; 0ᵘ; _+ᵘ_; _·ᵘ_; _▹_; unit; Cxᵖ; _▹ᵖ_; _▸_⊢ᵖ_∶_ + ; t-var; t-lam; t-app; t-pair; t-letp; t-inj₁; t-inj₂; t-case + ; t-step; t-conv ) +open import Wager.Poly.Proofs tSig tTSig ops using (sub-⇑; ⇑-closed) +open import Wager.Poly.CoercionStatements SS Sc ops +open GradeOps ops + +private + variable + n : ℕ + Δ : Ctx + +------------------------------------------------------------------------ +-- 1. Types. + +-- A closed type does not change under an instantiation. +private + cl : (s : TySub [] Δ) (X : Ty [] ★) → sub s (⇑ X) ≡ X + cl s X = sub-⇑ s X ∙ ⇑-closed X + +t8-type-instance : T8-Type-Instance +t8-type-instance (ovar x) ρ s ag = ag x +t8-type-instance (clo τ) ρ s ag = cl s (T τ) +t8-type-instance (θ ⇒ᵒ φ) ρ s ag = + cong₂ (arr 𝟙) (t8-type-instance θ ρ s ag) (t8-type-instance φ ρ s ag) +t8-type-instance (θ ×ᵒ φ) ρ s ag = + cong₂ _⊗_ (t8-type-instance θ ρ s ag) (t8-type-instance φ ρ s ag) +t8-type-instance (θ +ᵒ φ) ρ s ag = + cong₂ _⊕_ (t8-type-instance θ ρ s ag) (t8-type-instance φ ρ s ag) + +------------------------------------------------------------------------ +-- 2. Trope operations. + +t8-ops-rigid : T8-Ops-Rigid +t8-ops-rigid s (tvar i) = refl +t8-ops-rigid s (tlam q A b) = t8-ops-rigid s b +t8-ops-rigid s (tapp f a) = cong₂ _++_ (t8-ops-rigid s f) (t8-ops-rigid s a) +t8-ops-rigid s (pair t u) = cong₂ _++_ (t8-ops-rigid s t) (t8-ops-rigid s u) +t8-ops-rigid s (letp t b) = cong₂ _++_ (t8-ops-rigid s t) (t8-ops-rigid s b) +t8-ops-rigid s (inj₁ t) = t8-ops-rigid s t +t8-ops-rigid s (inj₂ t) = t8-ops-rigid s t +t8-ops-rigid s (case t l r) = + cong₂ _++_ (t8-ops-rigid s t) (cong₂ _++_ (t8-ops-rigid s l) (t8-ops-rigid s r)) +t8-ops-rigid s (lit ℓ) = refl +t8-ops-rigid s (step o t) = cong (o ∷_) (t8-ops-rigid s t) + +private + -- The source type in the first operation of a list, when the + -- operation is on an instance of a newtype with a parameter. + firstArg : STy → List C.Op → STy + firstArg d ((_ , inr (_ , τ)) ∷ _) = τ + firstArg d _ = d + +t8-no-uniform-unwrap : T8-No-Uniform-Unwrap +t8-no-uniform-unwrap N τ₁ τ₂ t s₁ s₂ p₁ p₂ = + cong (firstArg τ₁) + (sym (cong opsOf p₁) ∙ t8-ops-rigid s₁ t ∙ sym (t8-ops-rigid s₂ t) ∙ cong opsOf p₂) + +------------------------------------------------------------------------ +-- 3. Typing, for the laws of a grade algebra. + +module Typed (laws : GradeLaws ops) (wr : WellRoled) where + open GradeLaws laws + private + GA : GradeAlgebra R + GA = record { ops = ops ; laws = laws } + open Wager.Trans.Typing SS Sc GA using (body-defeq) + + private + castUᵖ : {γ γ' : Usage n} {Γ : Cxᵖ Δ n} {t : Tmᵖ Δ n} {A : Ty Δ ★} → + γ ≡ γ' → γ ▸ Γ ⊢ᵖ t ∶ A → γ' ▸ Γ ⊢ᵖ t ∶ A + castUᵖ {Γ = Γ} {t} {A} p d = subst (λ z → z ▸ Γ ⊢ᵖ t ∶ A) p d + + -- A transformer that maps a term of the type X to a term of the type + -- Y, with the same usage vector. + TyTrᵖ : (X Y : Ty Δ ★) → Trᵖ Δ → Type + TyTrᵖ {Δ} X Y f = ∀ {n} {γ : Usage n} {Γ : Cxᵖ Δ n} {t : Tmᵖ Δ n} → + γ ▸ Γ ⊢ᵖ t ∶ X → γ ▸ Γ ⊢ᵖ f t ∶ Y + + IsoTypedᵖ : Ty Δ ★ → Ty Δ ★ → Isoᵖ Δ → Type + IsoTypedᵖ X Y i = TyTrᵖ X Y (fwdᵖ i) × TyTrᵖ Y X (bwdᵖ i) + + module _ {Δ : Ctx} where + private + variable + X Y Z X' Y' : Ty Δ ★ + + id-typedᵖ : DefEq X Y → IsoTypedᵖ X Y idIsoᵖ + id-typedᵖ e = (λ d → t-conv d e) , (λ d → t-conv d (d-sym e)) + + swap-typedᵖ : ∀ {i} → IsoTypedᵖ X Y i → IsoTypedᵖ Y X (swapIsoᵖ i) + swap-typedᵖ (f , g) = g , f + + comp-typedᵖ : ∀ {i j} → IsoTypedᵖ X Y i → IsoTypedᵖ Y Z j → + IsoTypedᵖ X Z (compIsoᵖ i j) + comp-typedᵖ (f , g) (f' , g') = (λ d → f' (f d)) , (λ d → g (g' d)) + + arrMap-typedᵖ : ∀ {h g : Trᵖ Δ} → TyTrᵖ X' X h → TyTrᵖ Y Y' g → + TyTrᵖ (arr 𝟙 X Y) (arr 𝟙 X' Y') (arrMapᵖ (arr 𝟙 X Y) X' h g) + arrMap-typedᵖ th tg {γ = γ} d = + castUᵖ (funExt λ i → zero-add (𝟙 · γ i) ∙ one-mul (γ i)) + (t-app + (t-lam {γ = 0ᵘ} + (t-lam {γ = 0ᵘ ▹ 𝟙} + (castUᵖ eq (tg (t-app (t-var (suc zero)) (th (t-var zero))))))) + d) + where + eq : ∀ {n} → (unit {n = suc (suc n)} (suc zero) +ᵘ (𝟙 ·ᵘ unit zero)) ≡ (0ᵘ ▹ 𝟙 ▹ 𝟙) + eq = funExt λ { zero → zero-add (𝟙 · 𝟙) ∙ one-mul 𝟙 + ; (suc zero) → cong (𝟙 +_) (mul-zero 𝟙) ∙ add-zero 𝟙 + ; (suc (suc i)) → cong (𝟘 +_) (mul-zero 𝟙) ∙ add-zero 𝟘 } + + arrIso-typedᵖ : ∀ {i j} → IsoTypedᵖ X X' i → IsoTypedᵖ Y Y' j → + IsoTypedᵖ (arr 𝟙 X Y) (arr 𝟙 X' Y') (arrIsoᵖ X X' Y Y' i j) + arrIso-typedᵖ (f , g) (f' , g') = arrMap-typedᵖ g f' , arrMap-typedᵖ f g' + + prodMap-typedᵖ : ∀ {f g : Trᵖ Δ} → TyTrᵖ X X' f → TyTrᵖ Y Y' g → + TyTrᵖ (X ⊗ Y) (X' ⊗ Y') (prodMapᵖ f g) + prodMap-typedᵖ tf tg {γ = γ} d = + castUᵖ (funExt λ i → add-zero (γ i)) + (t-letp {δ = 0ᵘ} d + (castUᵖ eq (t-pair (tf (t-var (suc zero))) (tg (t-var zero))))) + where + eq : ∀ {n} → (unit {n = suc (suc n)} (suc zero) +ᵘ unit zero) ≡ (0ᵘ ▹ 𝟙 ▹ 𝟙) + eq = funExt λ { zero → zero-add 𝟙 + ; (suc zero) → add-zero 𝟙 + ; (suc (suc i)) → add-zero 𝟘 } + + prodIso-typedᵖ : ∀ {i j} → IsoTypedᵖ X X' i → IsoTypedᵖ Y Y' j → + IsoTypedᵖ (X ⊗ Y) (X' ⊗ Y') (prodIsoᵖ i j) + prodIso-typedᵖ (f , g) (f' , g') = prodMap-typedᵖ f f' , prodMap-typedᵖ g g' + + sumMap-typedᵖ : ∀ {f g : Trᵖ Δ} → TyTrᵖ X X' f → TyTrᵖ Y Y' g → + TyTrᵖ (X ⊕ Y) (X' ⊕ Y') (sumMapᵖ f g) + sumMap-typedᵖ tf tg {γ = γ} d = + castUᵖ (funExt λ i → add-zero (γ i)) + (t-case {δ = 0ᵘ} d (t-inj₁ (tf (t-var zero))) (t-inj₂ (tg (t-var zero)))) + + sumIso-typedᵖ : ∀ {i j} → IsoTypedᵖ X X' i → IsoTypedᵖ Y Y' j → + IsoTypedᵖ (X ⊕ Y) (X' ⊕ Y') (sumIsoᵖ i j) + sumIso-typedᵖ (f , g) (f' , g') = sumMap-typedᵖ f f' , sumMap-typedᵖ g g' + + -- The two trope transitions of a newtype instance, by `t-step`. + step-typedᵖ : (x : Inst) → + IsoTypedᵖ {Δ} (⇑ (capp (stateOf x) (carrierOf x))) (⇑ (carrierOf x)) + (stepIsoᵖ x) + step-typedᵖ x = (λ d → t-step (unwrap , x) d) , (λ d → t-step (wrap , x) d) + + -- The map of a body, for a parameter that is used at the role d. + module _ {d : Role} {U V : Ty [] ★} (hn : leR nom d ≡ true → DefEq U V) + {i : Isoᵖ Δ} (hv : leR rep d ≡ true → IsoTypedᵖ (⇑ U) (⇑ V) i) where + + body-typedᵖ : ∀ β → leR (roleOf β) d ≡ true → + IsoTypedᵖ (⇑ (TB β U)) (⇑ (TB β V)) (bodyIsoᵖ β U V i) + body-typedᵖ bvar le = hv le + body-typedᵖ (bbase b) le = id-typedᵖ d-refl + body-typedᵖ (barr β γ) le = + arrIso-typedᵖ (body-typedᵖ β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typedᵖ γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typedᵖ (bprod β γ) le = + prodIso-typedᵖ (body-typedᵖ β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typedᵖ γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typedᵖ (bsum β γ) le = + sumIso-typedᵖ (body-typedᵖ β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typedᵖ γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typedᵖ (bfam F β) le = + id-typedᵖ (DefEq-ren εᵣ (d-papp (body-defeq hn β le))) + + -- What the translation of a closed coercion at the role r gives. + SemTyᵖ : Role → STy → STy → Isoᵖ Δ → Type + SemTyᵖ nom τ σ i = DefEq (T τ) (T σ) + SemTyᵖ rep τ σ i = IsoTypedᵖ (⇑ (T τ)) (⇑ (T σ)) i + SemTyᵖ ph τ σ i = Unit + + private + nt-wrapᵖ : ∀ N {τ σ} {i : Isoᵖ Δ} → + IsoTypedᵖ (⇑ (TB (body N) (T τ))) (⇑ (TB (body N) (T σ))) + (bodyIsoᵖ (body N) (T τ) (T σ) i) → + IsoTypedᵖ (⇑ (T (nt₁ N τ))) (⇑ (T (nt₁ N σ))) (ntIsoᵖ N τ σ i) + nt-wrapᵖ N {τ} {σ} (f , g) = + (λ d → t-step (wrap , inr (N , σ)) (f (t-step (unwrap , inr (N , τ)) d))) + , (λ d → t-step (wrap , inr (N , τ)) (g (t-step (unwrap , inr (N , σ)) d))) + + nt-typedᵖ : ∀ N d {τ σ} → leR (roleOf (body N)) d ≡ true → + (γ : Co d τ σ) → SemTyᵖ d τ σ (coIᵖ {Δ = Δ} d γ) → + IsoTypedᵖ (⇑ (T (nt₁ N τ))) (⇑ (T (nt₁ N σ))) (ntIsoᵖ N τ σ (coIᵖ {Δ = Δ} d γ)) + nt-typedᵖ N rep le γ sem = + nt-wrapᵖ N (body-typedᵖ (λ p → ⊥.rec (false≢true p)) {i = coIᵖ rep γ} (λ _ → sem) (body N) le) + nt-typedᵖ N nom le γ sem = + nt-wrapᵖ N (body-typedᵖ (λ _ → sem) {i = idIsoᵖ} + (λ _ → id-typedᵖ (DefEq-ren εᵣ sem)) (body N) le) + nt-typedᵖ N ph le γ sem = + nt-wrapᵖ N (body-typedᵖ (λ p → ⊥.rec (false≢true p)) {i = idIsoᵖ} + (λ p → ⊥.rec (false≢true p)) (body N) le) + + coIᵖ-typed : ∀ r {τ σ} (γ : Co r τ σ) → SemTyᵖ r τ σ (coIᵖ {Δ = Δ} r γ) + coIᵖ-typed nom γ = nominal-defeq γ + coIᵖ-typed ph γ = tt + coIᵖ-typed rep (c-sym γ) = swap-typedᵖ (coIᵖ-typed rep γ) + coIᵖ-typed rep (c-trans γ δ) = comp-typedᵖ (coIᵖ-typed rep γ) (coIᵖ-typed rep δ) + coIᵖ-typed rep (c-sub γ) = id-typedᵖ (DefEq-ren εᵣ (nominal-defeq γ)) + coIᵖ-typed rep (c-arr γ δ) = arrIso-typedᵖ (coIᵖ-typed rep γ) (coIᵖ-typed rep δ) + coIᵖ-typed rep (c-prod γ δ) = prodIso-typedᵖ (coIᵖ-typed rep γ) (coIᵖ-typed rep δ) + coIᵖ-typed rep (c-sum γ δ) = sumIso-typedᵖ (coIᵖ-typed rep γ) (coIᵖ-typed rep δ) + coIᵖ-typed rep (c-nt₁ N γ) = + nt-typedᵖ N (mulG rep (role N)) (wr N) γ (coIᵖ-typed (mulG rep (role N)) γ) + coIᵖ-typed rep (c-ax₀ N) = + subst (λ Z → IsoTypedᵖ (⇑ (T (nt₀ N))) (⇑ Z) (stepIsoᵖ (inl N))) + (sym (T-embE (rep₀ N))) (step-typedᵖ (inl N)) + coIᵖ-typed rep (c-ax₁ N τ) = + subst (λ Z → IsoTypedᵖ (⇑ (T (nt₁ N τ))) (⇑ Z) (stepIsoᵖ (inr (N , τ)))) + (sym (T-inst (body N) τ)) (step-typedᵖ (inr (N , τ))) + + -- The typing of the translation of an open coercion. + coIᵒ-typed : ∀ {θ φ : OTy Δ} (c : Coᵒ θ φ) → IsoTypedᵖ (Tᵒ θ) (Tᵒ φ) (coIᵒ c) + coIᵒ-typed o-refl = id-typedᵖ d-refl + coIᵒ-typed (o-clo γ) = coIᵖ-typed rep γ + coIᵒ-typed (o-sym c) = swap-typedᵖ (coIᵒ-typed c) + coIᵒ-typed (o-trans c d) = comp-typedᵖ (coIᵒ-typed c) (coIᵒ-typed d) + coIᵒ-typed (o-arr c d) = arrIso-typedᵖ (coIᵒ-typed c) (coIᵒ-typed d) + coIᵒ-typed (o-prod c d) = prodIso-typedᵖ (coIᵒ-typed c) (coIᵒ-typed d) + coIᵒ-typed (o-sum c d) = sumIso-typedᵖ (coIᵒ-typed c) (coIᵒ-typed d) + +t8-coercion-typed : T8-Coercion-Typed +t8-coercion-typed laws wr c Γ = + t-lam {γ = 0ᵘ} (fst (Typed.coIᵒ-typed laws wr c) (t-var zero)) + +------------------------------------------------------------------------ +-- 4. Instances. The instantiation s is fixed. + +module Instance {Δ : Ctx} (s : TySub [] Δ) where + + -- The closed instance of an open term. + ⟪_⟫ : Tmᵖ Δ n → Tm n + ⟪ t ⟫ = ⌊ inst s t ⌋ + + -- A transformer of open terms and a transformer of closed terms + -- that agree on each instance. + Nat : Tr → Trᵖ Δ → Type + Nat f fᵖ = ∀ {n} (t : Tmᵖ Δ n) → ⟪ fᵖ t ⟫ ≡ f ⟪ t ⟫ + + -- A record, so that Agda finds the two isomorphisms from the type. + infixr 4 _,ⁿ_ + record NatIso (i : Iso) (iᵖ : Isoᵖ Δ) : Type where + constructor _,ⁿ_ + field + natF : Nat (fwd i) (fwdᵖ iᵖ) + natB : Nat (bwd i) (bwdᵖ iᵖ) + open NatIso + + id-nat : NatIso idIso idIsoᵖ + id-nat = (λ t → refl) ,ⁿ (λ t → refl) + + swap-nat : ∀ {i iᵖ} → NatIso i iᵖ → NatIso (swapIso i) (swapIsoᵖ iᵖ) + swap-nat (f ,ⁿ g) = g ,ⁿ f + + comp-nat : ∀ {i iᵖ j jᵖ} → NatIso i iᵖ → NatIso j jᵖ → + NatIso (compIso i j) (compIsoᵖ iᵖ jᵖ) + comp-nat {i} {iᵖ} {j} {jᵖ} (f ,ⁿ g) (f' ,ⁿ g') = + (λ t → f' (fwdᵖ iᵖ t) ∙ cong (λ z → fwd j z) (f t)) + ,ⁿ (λ t → g (bwdᵖ jᵖ t) ∙ cong (λ z → bwd i z) (g' t)) + + arrMap-nat : ∀ {X A : Ty [] ★} {Xᵖ Aᵖ : Ty Δ ★} {h g : Tr} {hᵖ gᵖ : Trᵖ Δ} → + sub s Xᵖ ≡ X → sub s Aᵖ ≡ A → Nat h hᵖ → Nat g gᵖ → + Nat (arrMap X A h g) (arrMapᵖ Xᵖ Aᵖ hᵖ gᵖ) + arrMap-nat {h = h} {g} {hᵖ} {gᵖ} pX pA nh ng t i = + C.tapp (C.tlam 𝟙 (pX i) (C.tlam 𝟙 (pA i) (inner i))) ⟪ t ⟫ + where + inner : ⟪ gᵖ (tapp (tvar (suc zero)) (hᵖ (tvar zero))) ⟫ + ≡ g (C.tapp (C.tvar (suc zero)) (h (C.tvar zero))) + inner = ng (tapp (tvar (suc zero)) (hᵖ (tvar zero))) + ∙ cong (λ z → g (C.tapp (C.tvar (suc zero)) z)) (nh (tvar zero)) + + arrIso-nat : ∀ {A A' B B' : Ty [] ★} {Aᵖ A'ᵖ Bᵖ B'ᵖ : Ty Δ ★} {i iᵖ j jᵖ} → + sub s Aᵖ ≡ A → sub s A'ᵖ ≡ A' → sub s Bᵖ ≡ B → sub s B'ᵖ ≡ B' → + NatIso i iᵖ → NatIso j jᵖ → + NatIso (arrIso A A' B B' i j) (arrIsoᵖ Aᵖ A'ᵖ Bᵖ B'ᵖ iᵖ jᵖ) + arrIso-nat {Aᵖ = Aᵖ} {A'ᵖ} {Bᵖ} {B'ᵖ} {i} {iᵖ} {j} {jᵖ} pA pA' pB pB' (f ,ⁿ g) (f' ,ⁿ g') = + arrMap-nat {Xᵖ = arr 𝟙 Aᵖ Bᵖ} {Aᵖ = A'ᵖ} + {h = bwd i} {g = fwd j} {hᵖ = bwdᵖ iᵖ} {gᵖ = fwdᵖ jᵖ} + (cong₂ (arr 𝟙) pA pB) pA' g f' + ,ⁿ arrMap-nat {Xᵖ = arr 𝟙 A'ᵖ B'ᵖ} {Aᵖ = Aᵖ} + {h = fwd i} {g = bwd j} {hᵖ = fwdᵖ iᵖ} {gᵖ = bwdᵖ jᵖ} + (cong₂ (arr 𝟙) pA' pB') pA f g' + + prodMap-nat : ∀ {f g : Tr} {fᵖ gᵖ : Trᵖ Δ} → Nat f fᵖ → Nat g gᵖ → + Nat (prodMap f g) (prodMapᵖ fᵖ gᵖ) + prodMap-nat nf ng t i = + C.letp ⟪ t ⟫ (C.pair (nf (tvar (suc zero)) i) (ng (tvar zero) i)) + + prodIso-nat : ∀ {i iᵖ j jᵖ} → NatIso i iᵖ → NatIso j jᵖ → + NatIso (prodIso i j) (prodIsoᵖ iᵖ jᵖ) + prodIso-nat {i} {iᵖ} {j} {jᵖ} (f ,ⁿ g) (f' ,ⁿ g') = + prodMap-nat {f = fwd i} {g = fwd j} {fᵖ = fwdᵖ iᵖ} {gᵖ = fwdᵖ jᵖ} f f' + ,ⁿ prodMap-nat {f = bwd i} {g = bwd j} {fᵖ = bwdᵖ iᵖ} {gᵖ = bwdᵖ jᵖ} g g' + + sumMap-nat : ∀ {f g : Tr} {fᵖ gᵖ : Trᵖ Δ} → Nat f fᵖ → Nat g gᵖ → + Nat (sumMap f g) (sumMapᵖ fᵖ gᵖ) + sumMap-nat nf ng t i = + C.case ⟪ t ⟫ (C.inj₁ (nf (tvar zero) i)) (C.inj₂ (ng (tvar zero) i)) + + sumIso-nat : ∀ {i iᵖ j jᵖ} → NatIso i iᵖ → NatIso j jᵖ → + NatIso (sumIso i j) (sumIsoᵖ iᵖ jᵖ) + sumIso-nat {i} {iᵖ} {j} {jᵖ} (f ,ⁿ g) (f' ,ⁿ g') = + sumMap-nat {f = fwd i} {g = fwd j} {fᵖ = fwdᵖ iᵖ} {gᵖ = fwdᵖ jᵖ} f f' + ,ⁿ sumMap-nat {f = bwd i} {g = bwd j} {fᵖ = bwdᵖ iᵖ} {gᵖ = bwdᵖ jᵖ} g g' + + step-nat : (x : Inst) → NatIso (stepIso x) (stepIsoᵖ x) + step-nat x = (λ t → refl) ,ⁿ (λ t → refl) + + body-nat : ∀ β (X Y : Ty [] ★) {i iᵖ} → NatIso i iᵖ → + NatIso (bodyIso β X Y i) (bodyIsoᵖ β X Y iᵖ) + body-nat bvar X Y ni = ni + body-nat (bbase b) X Y ni = id-nat + body-nat (barr β γ) X Y ni = + arrIso-nat (cl s (TB β X)) (cl s (TB β Y)) (cl s (TB γ X)) (cl s (TB γ Y)) + (body-nat β X Y ni) (body-nat γ X Y ni) + body-nat (bprod β γ) X Y ni = prodIso-nat (body-nat β X Y ni) (body-nat γ X Y ni) + body-nat (bsum β γ) X Y ni = sumIso-nat (body-nat β X Y ni) (body-nat γ X Y ni) + body-nat (bfam F β) X Y ni = id-nat + + nt-nat : ∀ N τ σ {i iᵖ} → NatIso i iᵖ → NatIso (ntIso N τ σ i) (ntIsoᵖ N τ σ iᵖ) + nt-nat N τ σ ni = + (λ t → cong (C.step (wrap , inr (N , σ))) (natF b (step (unwrap , inr (N , τ)) t))) + ,ⁿ (λ t → cong (C.step (wrap , inr (N , τ))) (natB b (step (unwrap , inr (N , σ)) t))) + where b = body-nat (body N) (T τ) (T σ) ni + + coIᵖ-nat : ∀ r {τ σ} (γ : Co r τ σ) → NatIso (coI r γ) (coIᵖ r γ) + coIᵖ-nat nom γ = id-nat + coIᵖ-nat ph γ = id-nat + coIᵖ-nat rep (c-sym γ) = swap-nat (coIᵖ-nat rep γ) + coIᵖ-nat rep (c-trans γ δ) = comp-nat (coIᵖ-nat rep γ) (coIᵖ-nat rep δ) + coIᵖ-nat rep (c-sub γ) = id-nat + coIᵖ-nat rep (c-arr {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + arrIso-nat (cl s (T τ)) (cl s (T τ')) (cl s (T σ)) (cl s (T σ')) + (coIᵖ-nat rep γ) (coIᵖ-nat rep δ) + coIᵖ-nat rep (c-prod γ δ) = prodIso-nat (coIᵖ-nat rep γ) (coIᵖ-nat rep δ) + coIᵖ-nat rep (c-sum γ δ) = sumIso-nat (coIᵖ-nat rep γ) (coIᵖ-nat rep δ) + coIᵖ-nat rep (c-nt₁ {τ = τ} {σ = σ} N γ) = + nt-nat N τ σ (coIᵖ-nat (mulG rep (role N)) γ) + coIᵖ-nat rep (c-ax₀ N) = step-nat (inl N) + coIᵖ-nat rep (c-ax₁ N τ) = step-nat (inr (N , τ)) + + module _ (ρ : SInst Δ) (ag : Agrees s ρ) where + + coIᵒ-nat : ∀ {θ φ : OTy Δ} (c : Coᵒ θ φ) → NatIso (coI rep (c ⟦ ρ ⟧ᶜ)) (coIᵒ c) + coIᵒ-nat o-refl = id-nat + coIᵒ-nat (o-clo γ) = coIᵖ-nat rep γ + coIᵒ-nat (o-sym c) = swap-nat (coIᵒ-nat c) + coIᵒ-nat (o-trans c d) = comp-nat (coIᵒ-nat c) (coIᵒ-nat d) + coIᵒ-nat (o-arr {θ = θ} {θ' = θ'} {φ = φ} {φ' = φ'} c d) = + arrIso-nat (t8-type-instance θ ρ s ag) (t8-type-instance θ' ρ s ag) + (t8-type-instance φ ρ s ag) (t8-type-instance φ' ρ s ag) + (coIᵒ-nat c) (coIᵒ-nat d) + coIᵒ-nat (o-prod c d) = prodIso-nat (coIᵒ-nat c) (coIᵒ-nat d) + coIᵒ-nat (o-sum c d) = sumIso-nat (coIᵒ-nat c) (coIᵒ-nat d) + +t8-coercion-instance : T8-Coercion-Instance +t8-coercion-instance {θ = θ} c ρ s ag i = + C.tlam 𝟙 (t8-type-instance θ ρ s ag i) + (Instance.NatIso.natF (Instance.coIᵒ-nat s ρ ag c) (tvar zero) i) diff --git a/verification/proofs/agda/Wager/Poly/IdentityRigid.agda b/verification/proofs/agda/Wager/Poly/IdentityRigid.agda new file mode 100644 index 0000000..6e65338 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/IdentityRigid.agda @@ -0,0 +1,132 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The identity family and open types: proofs. +-- +-- An open type E with one type variable is convertible to the +-- embedding of its normal form v. The proof looks at v. In the +-- signature of `Wager.Identity.Instance`, v is the variable, a base +-- constant, an arrow, a product or a sum. No case has the evidence +-- type `Id α B` at each instance α: +-- the variable its instance at the type `I₀ ⊗ I₀` is a product; +-- a base constant its instances at `I₀` and at `I₀ ⊗ I₀` are one +-- constant, and the two evidence types are two +-- constants; +-- the other cases the instance is not a base constant. +open import Cubical.Foundations.Prelude +open import Wager.Grade.Algebra + +module Wager.Poly.IdentityRigid + (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) (b₀ : B₀) where + +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sigma using (_,_) + +open import Wager.Identity.Instance B₀ L₀ ty₀ ops +open import Wager.L1.Syntax sig +open import Wager.L1.Normal sig +open import Wager.L1.Eval sig +open import Wager.L1.Conversion sig +open import Wager.L1.Soundness sig using (soundness) +open import Wager.L1.Equality sig using (defEq→nf) +open import Wager.Poly.Proofs sig tsig ops using (t8-conv) +open import Wager.Poly.IdentityStatements B₀ L₀ ty₀ ops b₀ + +private + O : Ctx + O = ★ ∷ [] + + -- The normal form of the instance of a normal form. + at : Nf O ★ → Ty [] ★ → Nf [] ★ + at v α = nf (embNf v [ α ]) + + -- If each instance of E is convertible to X α, then each instance of + -- the normal form of E has the normal form of X α. + to-nf : (E : Ty O ★) (X : Ty [] ★ → Ty [] ★) → + (∀ α → DefEq (E [ α ]) (X α)) → ∀ α → at (nf E) α ≡ nf (X α) + to-nf E X h α = + sym (defEq→nf (t8-conv (α ∷ₛ ids) (soundness E))) ∙ defEq→nf (h α) + + -- The context O has no variable of an arrow kind, so it has no + -- neutral term of an arrow kind. + noNeArr : ∀ {k g j} → Ne O (k ⇒[ g ] j) → ⊥ + noNeArr (nvar (vs ())) + noNeArr (napp n v) = noNeArr n + + -- The shape of a closed normal form. + isBase isArr isProd isSum : Nf [] ★ → Type + isBase (nbase _) = Unit + isBase _ = ⊥ + isArr (narr _ _ _) = Unit + isArr _ = ⊥ + isProd (_ n⊗ _) = Unit + isProd _ = ⊥ + isSum (_ n⊕ _) = Unit + isSum _ = ⊥ + + -- A base constant of the family whose first index is the code of a + -- base constant. + isIdAtBase : Nf [] ★ → Type + isIdAtBase (nbase (cid (cq _) _)) = Unit + isIdAtBase _ = ⊥ + + left⊕ left⊗ : Nf [] ★ → Nf [] ★ + left⊕ (a n⊕ b) = a + left⊕ v = v + left⊗ (a n⊗ b) = a + left⊗ v = v + + I₀⊗I₀ : Ty [] ★ + I₀⊗I₀ = I₀ ⊗ I₀ + + -- The evidence type at α, as a normal form. + evN : Ty [] ★ → Ty [] ★ → Nf [] ★ + evN α B = nbase (cid (enc (nf α)) (enc (nf B))) + + -- No normal form has the evidence type at each instance. + no-evidence : (B : Ty [] ★) (v : Nf O ★) → (∀ α → at v α ≡ evN α B) → ⊥ + no-evidence B (ne (nvar vz)) h = subst isProd (h I₀⊗I₀) tt + no-evidence B (ne (nvar (vs ()))) h + no-evidence B (ne (napp n _)) h = noNeArr n + no-evidence B (ne (nstuck () _)) h + no-evidence B (nbase c) h = subst isIdAtBase (sym (h I₀) ∙ h I₀⊗I₀) tt + no-evidence B (ncapp () _) h + no-evidence B (narr q a b) h = subst isArr (h I₀) tt + no-evidence B (a n⊗ b) h = subst isProd (h I₀) tt + no-evidence B (a n⊕ b) h = subst isSum (h I₀) tt + + -- One summand of the data type: the evidence and the payload. + no-summand : (B : Ty [] ★) (v : Nf O ★) → (∀ α → at v α ≡ (evN α B n⊗ nf α)) → ⊥ + no-summand B (ne (nvar vz)) h = subst isBase (h I₀) tt + no-summand B (ne (nvar (vs ()))) h + no-summand B (ne (napp n _)) h = noNeArr n + no-summand B (ne (nstuck () _)) h + no-summand B (nbase c) h = subst isBase (h I₀) tt + no-summand B (ncapp () _) h + no-summand B (narr q a b) h = subst isArr (h I₀) tt + no-summand B (a n⊗ b) h = no-evidence B a (λ α → cong left⊗ (h α)) + no-summand B (a n⊕ b) h = subst isSum (h I₀) tt + + no-data : (v : Nf O ★) → (∀ α → at v α ≡ nf (Gᵍ α)) → ⊥ + no-data (ne (nvar vz)) h = subst isBase (h I₀) tt + no-data (ne (nvar (vs ()))) h + no-data (ne (napp n _)) h = noNeArr n + no-data (ne (nstuck () _)) h + no-data (nbase c) h = subst isBase (h I₀) tt + no-data (ncapp () _) h + no-data (narr q a b) h = subst isArr (h I₀) tt + no-data (a n⊗ b) h = subst isProd (h I₀) tt + no-data (a n⊕ b) h = no-summand I₀ a (λ α → cong left⊕ (h α)) + +t8-evidence-rigid : T8-Evidence-Rigid +t8-evidence-rigid B (E , h) = + no-evidence B (nf E) (to-nf E (λ α → base (Id α B)) h) + where open import Wager.Identity.Family sig tsig using (module IdFamily) + open IdFamily family using (Id) + +t8-gadt-not-open : T8-Gadt-Not-Open +t8-gadt-not-open (G , h) = no-data (nf G) (to-nf G Gᵍ h) diff --git a/verification/proofs/agda/Wager/Poly/Proofs.agda b/verification/proofs/agda/Wager/Poly/Proofs.agda index 03ab884..7ffc7ff 100644 --- a/verification/proofs/agda/Wager/Poly/Proofs.agda +++ b/verification/proofs/agda/Wager/Poly/Proofs.agda @@ -21,6 +21,8 @@ open import Wager.L1.SyntaxLemmas S open import Wager.L1.Conversion S open import Wager.L2.Term S TS using (Lit; litTy; Op; carrier; from; to; _at_) import Wager.L2.Typing S TS ops as C +import Wager.L2.Progress +import Wager.L2.Preservation open import Wager.Poly.Typing S TS ops open import Wager.Poly.Statements S TS ops @@ -152,3 +154,20 @@ t8-closed (t-step o d) = (C.t-step o (tyᶜ (⇑-closed (carrier o at from o)) (t8-closed d))) t8-closed (t-conv d e) = C.t-conv (t8-closed d) e t8-closed (t-sub d le) = C.t-sub (t8-closed d) le + +------------------------------------------------------------------------ +-- The second freeze: each closed instance is a term of the target, so +-- the theorems of the target apply to it. + +t8-closed-instance : T8-Closed-Instance +t8-closed-instance σ d = t8-closed (t8-inst σ d) + +-- Progress uses the operations only, and no law. +t8-instance-progress : T8-Instance-Progress +t8-instance-progress σ d = + Wager.L2.Progress.progress S TS ops (t8-closed-instance σ d) + +t8-instance-preservation : T8-Instance-Preservation +t8-instance-preservation laws σ d r = + Wager.L2.Preservation.preservation S TS (record { ops = ops ; laws = laws }) + (t8-closed-instance σ d) r diff --git a/verification/proofs/agda/Wager/Poly/Role.agda b/verification/proofs/agda/Wager/Poly/Role.agda new file mode 100644 index 0000000..a1d28d3 --- /dev/null +++ b/verification/proofs/agda/Wager/Poly/Role.agda @@ -0,0 +1,79 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8. The role of a type variable: proofs. +-- +-- The fundamental lemma of Stage 2 (`Wager.Role.Noninterference.fund`) +-- is about a type in a context. Stage 2 used it at the empty context. +-- Here it is used at a context of type variables. The link between an +-- instance `sub s A` and the evaluation of A is the lemma `eval-sub` +-- of Stage 1. +open import Cubical.Foundations.Prelude +open import Wager.Role.Signature +open import Wager.Role.Table + +module Wager.Poly.Role (RS : RoleSig) where + +open import Cubical.Data.Unit using (tt) +open import Wager.Role.Role +open import Wager.L1.Syntax (toSig RS) +open import Wager.L1.Eval (toSig RS) +open import Wager.L1.Completeness (toSig RS) using (eval-sub; envExt) +import Wager.L1.Kinding +import Wager.Role.Noninterference +open import Wager.Poly.RoleStatements RS + +private + -- The instance of A is the value of A in the environment of the + -- values of the substitution. + nf-sub : ∀ {Δ} (A : Ty Δ ★) (s : TySub [] Δ) → + nf (sub s A) ≡ eval A (λ k x → eval (s k x) idEnv) + nf-sub A s = eval-sub A s {ρ = idEnv} {ρ' = idEnv} (λ k ()) + +module ForTableProofs (T : RoleTable) where + open ForTable T + open Wager.Role.Noninterference RS T + open import Wager.Role.Validity RS (RoleTable.mul T) using (R★) + + t8-role : T8-Role + t8-role V {A = A} d ρ s s' e = + subst2 (R★ ρ) (sym (nf-sub A s)) (sym (nf-sub A s')) (fund V d ρ e) + +module LawfulProofs where + open Lawful + open ForTableProofs tableZ + open Wager.L1.Kinding (toSig RS) (tableOps tableZ) + open Wager.Role.Noninterference RS tableZ using (LR; R★-anti) + + private + -- The two instantiations of one type variable, as two environments + -- that an observer cannot tell apart at the grade r. + one-var : ∀ (ρ r : Role) (B C : Ty [] ★) → LR (mulZ ρ r) ★ (nf B) (nf C) → + ∀ k (x : Var (★ ∷ []) k) → + LR (mulZ ρ ((0ᵏ ▹ᵏ r) k x)) k + (eval ((B ∷ₛ ids) k x) idEnv) (eval ((C ∷ₛ ids) k x) idEnv) + one-var ρ r B C h k vz = h + + t8-role-representational : T8-Role-Representational + t8-role-representational V {r} d le B C h = + t8-role V d rep (B ∷ₛ ids) (C ∷ₛ ids) + (one-var rep r B C (R★-anti r rep le h)) + + -- The proof uses the entry nominal · phantom = phantom of the lawful + -- table. + t8-role-phantom : T8-Role-Phantom + t8-role-phantom V d B C = + t8-role V d nom (B ∷ₛ ids) (C ∷ₛ ids) (one-var nom ph B C tt) + + t8-role-nominal : T8-Role-Nominal + t8-role-nominal A B C h = + nf-sub A (B ∷ₛ ids) + ∙ cong (eval A) (envExt pt) + ∙ sym (nf-sub A (C ∷ₛ ids)) + where + pt : ∀ k (x : Var (★ ∷ []) k) → + eval ((B ∷ₛ ids) k x) idEnv ≡ eval ((C ∷ₛ ids) k x) idEnv + pt k vz = h From aac0f77b48fd99d1e54b79180b587dd578304621 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:13:12 +0000 Subject: [PATCH 06/11] proof(wager): Stage 8, examples, index modules and MANIFEST - Examples/Stage8.agda: accepted and rejected examples for open terms, open coercions, the role of a type variable and the identity family. - Statements.agda, Proofs.agda, Everything.agda: a Stage 8 section in each. No earlier statement changed. - MANIFEST: 12 new gated modules. The marker in PROOF-STATUS.adoc is gated=91. scripts/check-proofs.sh agda: PASS, 91 modules. scripts/check-proof-status.sh: PASS. Co-Authored-By: Claude --- docs/status/PROOF-STATUS.adoc | 2 +- verification/proofs/agda/MANIFEST | 12 + .../proofs/agda/Wager/Everything.agda | 12 + .../proofs/agda/Wager/Examples/Stage8.agda | 360 ++++++++++++++++++ verification/proofs/agda/Wager/Proofs.agda | 77 ++++ .../proofs/agda/Wager/Statements.agda | 52 +++ 6 files changed, 514 insertions(+), 1 deletion(-) create mode 100644 verification/proofs/agda/Wager/Examples/Stage8.agda diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index b973804..b569f27 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -13,7 +13,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh. // Do not edit by hand without changing the MANIFEST accordingly. // gate:lean4 gated=20 quarantined=0 -// gate:agda gated=79 quarantined=0 +// gate:agda gated=91 quarantined=0 == Summary diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index 469eab3..8572d32 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -80,3 +80,15 @@ verification/proofs/agda|Wager/Examples/Stage6Identity.agda|gated|Stage 6, part verification/proofs/agda|Wager/Univalent/Model.agda|gated|Stage 7 (optional): the model of target types in the cubical universe, realisers, and the path of a coercion (definitions only) verification/proofs/agda|Wager/Univalent/CrossCheck.agda|gated|Stage 7 (optional): the translation of a representational coercion denotes transport along its path, for each source signature, state scheme, grade algebra and interpretation of the base constants verification/proofs/agda|Wager/Examples/Stage7.agda|gated|Stage 7 (optional): accepted and rejected closed examples +verification/proofs/agda|Wager/Poly/Term.agda|gated|Stage 8: terms of the target with open types, instantiation, and the map from a term with no type variable to a target term (definitions only) +verification/proofs/agda|Wager/Poly/Typing.agda|gated|Stage 8: the typing judgement for terms with open types; each rule is the rule of the target with the types in a context of type variables (definitions only) +verification/proofs/agda|Wager/Poly/Statements.agda|gated|Stage 8: 6 statements about open terms and their closed instances (types only) +verification/proofs/agda|Wager/Poly/Proofs.agda|gated|Stage 8: conversion is stable under substitution; each instance of a typed open term is typed; each closed instance is a typed target term, with progress and preservation +verification/proofs/agda|Wager/Poly/Coercion.agda|gated|Stage 8: open source types, open representational coercions and their translation to 1 open term (definitions only) +verification/proofs/agda|Wager/Poly/CoercionStatements.agda|gated|Stage 8: 5 statements about coercions at open types (types only) +verification/proofs/agda|Wager/Poly/CoercionProofs.agda|gated|Stage 8: the open coercion is typed for the laws of a grade algebra; each closed instance is the closed coercion of Stage 4; no open term is the unwrap of a newtype at each instance of a type variable +verification/proofs/agda|Wager/Poly/RoleStatements.agda|gated|Stage 8: 4 statements about the role of a type variable (types only) +verification/proofs/agda|Wager/Poly/Role.agda|gated|Stage 8: noninterference for a type with free type variables, for each composition table and a valid signature; the lawful table at 1 variable +verification/proofs/agda|Wager/Poly/IdentityStatements.agda|gated|Stage 8: 2 statements about the identity family and open types (types only) +verification/proofs/agda|Wager/Poly/IdentityRigid.agda|gated|Stage 8: in the signature with an identity family, no open type with 1 type variable has the evidence types or the GADT data type as its instances +verification/proofs/agda|Wager/Examples/Stage8.agda|gated|Stage 8: accepted and rejected examples for open terms, open coercions, the role of a type variable and the identity family diff --git a/verification/proofs/agda/Wager/Everything.agda b/verification/proofs/agda/Wager/Everything.agda index aafdd5b..20d4154 100644 --- a/verification/proofs/agda/Wager/Everything.agda +++ b/verification/proofs/agda/Wager/Everything.agda @@ -84,3 +84,15 @@ import Wager.Examples.Stage6Identity import Wager.Univalent.Model import Wager.Univalent.CrossCheck import Wager.Examples.Stage7 +import Wager.Poly.Term +import Wager.Poly.Typing +import Wager.Poly.Statements +import Wager.Poly.Proofs +import Wager.Poly.Coercion +import Wager.Poly.CoercionStatements +import Wager.Poly.CoercionProofs +import Wager.Poly.RoleStatements +import Wager.Poly.Role +import Wager.Poly.IdentityStatements +import Wager.Poly.IdentityRigid +import Wager.Examples.Stage8 diff --git a/verification/proofs/agda/Wager/Examples/Stage8.agda b/verification/proofs/agda/Wager/Examples/Stage8.agda new file mode 100644 index 0000000..5ecc3cb --- /dev/null +++ b/verification/proofs/agda/Wager/Examples/Stage8.agda @@ -0,0 +1,360 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Stage 8 anti-vacuity examples: terms with open types. +-- +-- Open-Terms the signature of Stage 5 (`taggedS rep`, the row +-- scheme), the one-point grade algebra. +-- Open-Coercions the same signature. One example is in the algebra +-- {0, 1, ω}. +-- Role-Of-A-Variable the signature `classicSig rep` of Stage 2. +-- Identity-Family the signature of `Wager.Identity.Instance`. +module Wager.Examples.Stage8 where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax; fst; snd) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Algebra +open import Wager.Grade.Trivial +open import Wager.Grade.Affine using (affineOps; affineLaws; a1) +open import Wager.Role.Role +open import Wager.Role.Table +open import Wager.Role.Signature +open import Wager.FC.Tagged +import Wager.FC.Types +import Wager.FC.Coercion +import Wager.Trans.Scheme +import Wager.Trans.Target +import Wager.Trans.Coercion +import Wager.L1.Syntax +import Wager.L1.Normal +import Wager.L1.Eval +import Wager.L1.Conversion +import Wager.L1.Kinding +import Wager.L2.Typing +import Wager.L2.Erasure +import Wager.Role.RepEq +import Wager.Role.Classic +import Wager.Role.ClassicProofs as CP +import Wager.Identity.Instance +import Wager.Identity.Family +import Wager.Poly.Coercion +import Wager.Poly.Typing +open import Wager.Erased.Untyped using (ETy; ebase) +open import Wager.Examples.Stage3 using (module Role-Check) +import Wager.Examples.Stage6Identity as E6 +open import Wager.Statements using (module T8-Identity-Statements) +open import Wager.Proofs + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +------------------------------------------------------------------------ +-- T8-Inst, T8-Closed, T8-Closed-Instance, T8-Instance-Progress. + +module Open-Terms where + open Wager.FC.Types SS using (STy; sbase) + open Wager.Trans.Target SS Sc trivialOps + import Wager.L2.Typing tSig tTSig trivialOps as C + open Wager.L2.Erasure tSig tTSig trivialOps using (erT; eraseᵗ; identity-one-type) + open Wager.Poly.Typing tSig tTSig trivialOps + + -- One type variable of the kind ★. + O : Ctx + O = ★ ∷ [] + + a : Ty O ★ + a = var vz + + tInt tBool : Ty [] ★ + tInt = base bInt + tBool = base bBool + + ∅ᵖ : Cxᵖ O 0 + ∅ᵖ () + + -- The polymorphic identity function: 1 open term. + idᵖ : Tmᵖ O 0 + idᵖ = tlam tt a (tvar zero) + + -- ACCEPTED: it has the open type `a → a`. + idᵖ-typed : 0ᵘ ▸ ∅ᵖ ⊢ᵖ idᵖ ∶ arr tt a a + idᵖ-typed = t-lam {γ = 0ᵘ} (t-var zero) + + at-int at-bool : TySub [] O + at-int = tInt ∷ₛ ids + at-bool = tBool ∷ₛ ids + + -- Its instance at Int is the identity function of the target at Int. + id-at-int : ⌊ inst at-int idᵖ ⌋ ≡ C.tlam tt tInt (C.tvar zero) + id-at-int = refl + + -- ACCEPTED (T8-Closed-Instance): the instance is a typed term of the + -- target of stages 1 to 5. + id-at-int-typed : + 0ᵘ C.▸ (λ i → sub at-int (∅ᵖ i)) ⊢ ⌊ inst at-int idᵖ ⌋ ∶ arr tt tInt tInt + id-at-int-typed = t8-closed-instance tSig tTSig trivialOps at-int idᵖ-typed + + -- ACCEPTED (T8-Instance-Progress): T0 applies to the instance. + id-at-int-progress : + C.Value ⌊ inst at-int idᵖ ⌋ ⊎ (Σ[ t' ∈ C.Tm 0 ] (⌊ inst at-int idᵖ ⌋ C.⟶ t')) + id-at-int-progress = t8-instance-progress tSig tTSig trivialOps at-int idᵖ-typed + + private + IsBool : ETy BaseName → Type + IsBool (ebase bBool) = Unit + IsBool _ = ⊥ + + -- REJECTED: the same open term does not have the open type `a → Int`. + -- If it had, its instance at Bool would be a typed identity function + -- from Bool to Int (T8-Closed-Instance), and a typed term of the + -- target that erases to the identity has one erased type on its two + -- sides (`identity-one-type`, Stage 6). + id-not-to-int : ∀ {γ} → ¬ (γ ▸ ∅ᵖ ⊢ᵖ idᵖ ∶ arr tt a (⇑ tInt)) + id-not-to-int d = + subst IsBool + (identity-one-type + (t8-closed-instance tSig tTSig trivialOps at-bool d) refl) + tt + +------------------------------------------------------------------------ +-- T8-Coercion-Typed, T8-Coercion-Instance, T8-No-Uniform-Unwrap. + +module Open-Coercions where + open Wager.FC.Types SS hiding (inst) + open Wager.FC.Coercion SS + open TTypes rep + open Role-Check using (wr-rep) + open Wager.Trans.Target SS Sc trivialOps + open Wager.Trans.Coercion SS Sc trivialOps using (coerceT) + open Wager.Poly.Coercion SS Sc trivialOps + open Wager.Poly.Typing tSig tTSig trivialOps using (Cxᵖ; 0ᵘ; _▸_⊢ᵖ_∶_) + + O : Ctx + O = ★ ∷ [] + + ∅ᵖ : Cxᵖ O 0 + ∅ᵖ () + + -- Two open source types: `a → Age` and `a → Int`. + θ φ : OTy O + θ = ovar vz ⇒ᵒ clo sAge + φ = ovar vz ⇒ᵒ clo sInt + + -- The open coercion between them: the identity at the variable, and + -- the axiom of the newtype Age at the result. + c : Coᵒ θ φ + c = o-arr o-refl (o-clo (c-ax₀ ageE)) + + -- ONE POLYMORPHIC COERCION: 1 open term. + poly : Tmᵖ O 0 + poly = coerceᵒ c + + -- ACCEPTED (T8-Coercion-Typed): it is typed at the open types. + poly-typed : 0ᵘ ▸ ∅ᵖ ⊢ᵖ poly ∶ arr tt (Tᵒ θ) (Tᵒ φ) + poly-typed = t8-coercion-typed SS Sc trivialOps trivialLaws wr-rep c ∅ᵖ + + -- Two instantiations of the type variable: Bool, and the newtype Age. + ρ-bool ρ-age : SInst O + ρ-bool _ = sBool + ρ-age _ = sAge + + s-bool s-age : TySub [] O + s-bool = T sBool ∷ₛ ids + s-age = T sAge ∷ₛ ids + + ag-bool : Agrees s-bool ρ-bool + ag-bool vz = refl + + ag-age : Agrees s-age ρ-age + ag-age vz = refl + + -- ACCEPTED (T8-Coercion-Instance): the two instances of the 1 open + -- term are the two closed coercion functions of Stage 4. + poly-at-bool : + ⌊ inst s-bool poly ⌋ + ≡ coerceT {τ = sBool ⇒ˢ sAge} {σ = sBool ⇒ˢ sInt} + (c-arr (c-sub c-refl) (c-ax₀ ageE)) + poly-at-bool = t8-coercion-instance SS Sc trivialOps c ρ-bool s-bool ag-bool + + poly-at-age : + ⌊ inst s-age poly ⌋ + ≡ coerceT {τ = sAge ⇒ˢ sAge} {σ = sAge ⇒ˢ sInt} + (c-arr (c-sub c-refl) (c-ax₀ ageE)) + poly-at-age = t8-coercion-instance SS Sc trivialOps c ρ-age s-age ag-age + + -- ACCEPTED: an open coercion that unwraps a newtype with a parameter + -- at a CLOSED argument: `a → Tag Int` to `a → Int`. + tag-closed : Coᵒ {Δ = O} (ovar vz ⇒ᵒ clo (Tag sInt)) (ovar vz ⇒ᵒ clo sInt) + tag-closed = o-arr o-refl (o-clo (c-ax₁ tagE sInt)) + + tag-closed-typed : + 0ᵘ ▸ ∅ᵖ ⊢ᵖ coerceᵒ tag-closed + ∶ arr tt (Tᵒ (ovar vz ⇒ᵒ clo (Tag sInt))) (Tᵒ (ovar vz ⇒ᵒ clo sInt)) + tag-closed-typed = + t8-coercion-typed SS Sc trivialOps trivialLaws wr-rep tag-closed ∅ᵖ + + private + IsInt : STy → Type + IsInt (sbase bInt) = Unit + IsInt _ = ⊥ + + -- REJECTED (T8-No-Uniform-Unwrap): no open term is the coercion + -- `Tag a → Int` at the two instances a := Int and a := Bool. + no-poly-tag : + ¬ (Σ[ t ∈ Tmᵖ O 0 ] + (⌊ inst s-age t ⌋ ≡ coerceT (c-ax₁ tagE sInt)) + × (⌊ inst s-bool t ⌋ ≡ coerceT (c-ax₁ tagE sBool))) + no-poly-tag (t , p , q) = + subst IsInt + (t8-no-uniform-unwrap SS Sc trivialOps tagE sInt sBool t s-age s-bool p q) tt + +-- ACCEPTED: the polymorphic coercion is typed in the algebra {0, 1, ω}. +-- A coercion uses each variable one time. +module Open-Coercions-In-Affine where + open Wager.FC.Types SS hiding (inst) + open Wager.FC.Coercion SS + open TTypes rep + open Role-Check using (wr-rep) + open Wager.Trans.Target SS Sc affineOps + open Wager.Poly.Coercion SS Sc affineOps + open Wager.Poly.Typing tSig tTSig affineOps using (Cxᵖ; 0ᵘ; _▸_⊢ᵖ_∶_) + + O : Ctx + O = ★ ∷ [] + + ∅ᵖ : Cxᵖ O 0 + ∅ᵖ () + + c : Coᵒ {Δ = O} (ovar vz ⇒ᵒ clo sAge) (ovar vz ⇒ᵒ clo sInt) + c = o-arr o-refl (o-clo (c-ax₀ ageE)) + + poly-typed : + 0ᵘ ▸ ∅ᵖ ⊢ᵖ coerceᵒ c + ∶ arr a1 (Tᵒ (ovar vz ⇒ᵒ clo sAge)) (Tᵒ (ovar vz ⇒ᵒ clo sInt)) + poly-typed = t8-coercion-typed SS Sc affineOps affineLaws wr-rep c ∅ᵖ + +------------------------------------------------------------------------ +-- T8-Role-Representational, T8-Role-Phantom, T8-Role-Nominal. + +module Role-Of-A-Variable where + open Wager.Role.Classic + private + RS = classicSig rep + S = toSig RS + open Wager.L1.Syntax S + open Wager.L1.Normal S + open Wager.L1.Eval S + open Wager.Role.RepEq RS + open Types rep + open CP.LawfulKinding rep + + O : Ctx + O = ★ ∷ [] + + -- The open type `a →[1] Proxy a`. The variable has the grade + -- representational. + A₁ : Ty O ★ + A₁ = arr a1 (var vz) (Proxy (var vz)) + + A₁-kinded : (0ᵏ ▹ᵏ rep) ⊢ᵏ A₁ + A₁-kinded = k-sub (k-arr (k-var vz) (k-capp proxy (k-var vz))) le + where + le : (unitᵏ vz ⊕ᵏ (rep ⊙ᵏ unitᵏ vz)) ≼ᵏ (0ᵏ ▹ᵏ rep) + le k vz = refl + + -- ACCEPTED (T8-Role-Representational): the instances at Age and at + -- Int are equivalent. + accepted-representational : nf (A₁ [ Age ]) ≈ nf (A₁ [ Int ]) + accepted-representational = + t8-role-representational RS CP.ProxyB.valid A₁-kinded refl Age Int + (CP.Generic.age≈int rep) + + -- The open type `isAge Int`. The variable does not occur, and it has + -- the grade phantom. + A₂ : Ty O ★ + A₂ = papp isAge Int + + A₂-kinded : (0ᵏ ▹ᵏ ph) ⊢ᵏ A₂ + A₂-kinded = k-sub (k-papp isAge (k-base bInt)) le + where + le : (nom ⊙ᵏ 0ᵏ) ≼ᵏ (0ᵏ ▹ᵏ ph) + le k vz = refl + + -- ACCEPTED (T8-Role-Phantom): the instances at Age and at Bool have + -- one normal form. + accepted-phantom : nf (A₂ [ Age ]) ≡ nf (A₂ [ Bool' ]) + accepted-phantom = t8-role-phantom RS CP.ProxyB.valid A₂-kinded Age Bool' + + -- The body of the classic function: `isAge a`. + A₃ : Ty O ★ + A₃ = papp isAge (var vz) + + -- REJECTED: kinding does not accept the grade representational for + -- the variable of `isAge a` (this is T4), and the instances at Age + -- and at Int are not equivalent. + rejected : (¬ ((0ᵏ ▹ᵏ rep) ⊢ᵏ A₃)) + × (¬ (nf (A₃ [ Age ]) ≈ nf (A₃ [ Int ]))) + rejected = + (λ d → t4-kinding-rejects rep refl 0ᵏ (k-lam d)) + , snd t4-not-equivalent rep + + -- ACCEPTED (T8-Role-Nominal): at the grade nominal the two arguments + -- must have one normal form. `(λb. b) Int` and `Int` have one. + accepted-nominal : nf (A₃ [ app (lam {g = rep} (var vz)) Int ]) ≡ nf (A₃ [ Int ]) + accepted-nominal = + t8-role-nominal RS A₃ (app (lam {g = rep} (var vz)) Int) Int refl + +------------------------------------------------------------------------ +-- T8-Evidence-Rigid, T8-Gadt-Not-Open. + +module Identity-Family where + open E6 using (B₀; int; L₀; tInt; Gⁱ) + open Wager.Identity.Instance B₀ L₀ (λ _ → int) trivialOps + open Wager.L1.Syntax sig + open Wager.L1.Conversion sig using (DefEq) + open Wager.Identity.Family.IdFamily family using (Id) + open T8-Identity-Statements B₀ L₀ (λ _ → int) trivialOps int using (Gᵍ) + + -- The data type of the statement is the data type of the example of + -- Stage 6, part 2. + same-data : ∀ α → Gᵍ α ≡ Gⁱ α + same-data α = refl + + -- REJECTED (T8-Evidence-Rigid): no open type with one type variable + -- has the evidence type `Id α Int` at each instance α. + no-open-evidence : + ¬ (Σ[ E ∈ Ty (★ ∷ []) ★ ] (∀ α → DefEq (E [ α ]) (base (Id α tInt)))) + no-open-evidence = t8-evidence-rigid B₀ L₀ (λ _ → int) trivialOps int tInt + + -- REJECTED (T8-Gadt-Not-Open): no open type with one type variable + -- has the data type of the GADT program at each instance α. + no-open-data : + ¬ (Σ[ G ∈ Ty (★ ∷ []) ★ ] (∀ α → DefEq (G [ α ]) (Gⁱ α))) + no-open-data = t8-gadt-not-open B₀ L₀ (λ _ → int) trivialOps int + + -- ACCEPTED: an open type with THREE type variables has the data type + -- at each α. The two other variables stand for the two evidence + -- types, and the instantiation gives them the two base constants. + -- This open type does not say that its first two variables are + -- evidence types. The rule `t-cast` needs evidence of a type + -- `base (Id A B)`, so it does not apply to a term of the type of such + -- a variable (DESIGN-CHOICES.adoc, DC-8.6). + G₃ : Ty (★ ∷ ★ ∷ ★ ∷ []) ★ + G₃ = (var vz ⊗ var (vs (vs vz))) ⊕ (var (vs vz) ⊗ var (vs (vs vz))) + + at₃ : Ty [] ★ → TySub [] (★ ∷ ★ ∷ ★ ∷ []) + at₃ α = base (Id α tInt) ∷ₛ base (Id α (tInt ⊕ tInt)) ∷ₛ α ∷ₛ ids + + three-variables : ∀ α → sub (at₃ α) G₃ ≡ Gⁱ α + three-variables α = refl diff --git a/verification/proofs/agda/Wager/Proofs.agda b/verification/proofs/agda/Wager/Proofs.agda index 689cbf9..2b79744 100644 --- a/verification/proofs/agda/Wager/Proofs.agda +++ b/verification/proofs/agda/Wager/Proofs.agda @@ -77,6 +77,10 @@ import Wager.Local.Separation import Wager.Identity.Family import Wager.Identity.Soundness import Wager.Univalent.CrossCheck +import Wager.Poly.Proofs +import Wager.Poly.CoercionProofs +import Wager.Poly.Role +import Wager.Poly.IdentityRigid module _ where open T1-Statements @@ -334,3 +338,76 @@ module _ (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) coerce-function-is-transport : Coerce-Function-Is-Transport coerce-function-is-transport = CC.coerce-function-is-transport + +------------------------------------------------------------------------ +-- STAGE 8 +------------------------------------------------------------------------ + +module _ (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + open T8-Statements S TS ops + private module P = Wager.Poly.Proofs S TS ops + + t8-conv : T8-Conv + t8-conv = P.t8-conv + + t8-inst : T8-Inst + t8-inst = P.t8-inst + + t8-closed : T8-Closed + t8-closed = P.t8-closed + + t8-closed-instance : T8-Closed-Instance + t8-closed-instance = P.t8-closed-instance + + -- Progress uses the operations only, and no law. + t8-instance-progress : T8-Instance-Progress + t8-instance-progress = P.t8-instance-progress + + t8-instance-preservation : T8-Instance-Preservation + t8-instance-preservation = P.t8-instance-preservation + +module _ (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + open T8-Coercion-Statements SS Sc ops + private module CP8 = Wager.Poly.CoercionProofs SS Sc ops + + t8-type-instance : T8-Type-Instance + t8-type-instance = CP8.t8-type-instance + + t8-coercion-typed : T8-Coercion-Typed + t8-coercion-typed = CP8.t8-coercion-typed + + t8-coercion-instance : T8-Coercion-Instance + t8-coercion-instance = CP8.t8-coercion-instance + + t8-ops-rigid : T8-Ops-Rigid + t8-ops-rigid = CP8.t8-ops-rigid + + t8-no-uniform-unwrap : T8-No-Uniform-Unwrap + t8-no-uniform-unwrap = CP8.t8-no-uniform-unwrap + +module _ (RS : RoleSig) where + open T8-Role-Statements RS + private module PR = Wager.Poly.Role RS + + t8-role : (T : RoleTable) → ForTable.T8-Role T + t8-role T = PR.ForTableProofs.t8-role T + + t8-role-representational : T8-Role-Representational + t8-role-representational = PR.LawfulProofs.t8-role-representational + + t8-role-phantom : T8-Role-Phantom + t8-role-phantom = PR.LawfulProofs.t8-role-phantom + + t8-role-nominal : T8-Role-Nominal + t8-role-nominal = PR.LawfulProofs.t8-role-nominal + +module _ (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) (b₀ : B₀) where + open T8-Identity-Statements B₀ L₀ ty₀ ops b₀ + private module IR = Wager.Poly.IdentityRigid B₀ L₀ ty₀ ops b₀ + + t8-evidence-rigid : T8-Evidence-Rigid + t8-evidence-rigid = IR.t8-evidence-rigid + + t8-gadt-not-open : T8-Gadt-Not-Open + t8-gadt-not-open = IR.t8-gadt-not-open diff --git a/verification/proofs/agda/Wager/Statements.agda b/verification/proofs/agda/Wager/Statements.agda index a5ede86..ff8da9c 100644 --- a/verification/proofs/agda/Wager/Statements.agda +++ b/verification/proofs/agda/Wager/Statements.agda @@ -58,6 +58,10 @@ import Wager.Local.Gadt import Wager.Identity.Family import Wager.Identity.Typing import Wager.Univalent.Model +import Wager.Poly.Statements +import Wager.Poly.CoercionStatements +import Wager.Poly.RoleStatements +import Wager.Poly.IdentityStatements ------------------------------------------------------------------------ -- STAGE 1 @@ -839,3 +843,51 @@ module Stage7-Statements Coerce-Function-Is-Transport = (wr : WellRoled) → ∀ {τ σ} (γ : Co rep τ σ) {n} {ρ : UEnv n} → Real (arr 𝟙 (T τ) (T σ)) ρ (eraseT (coerceT γ)) (transport (pathOf wr γ)) + +------------------------------------------------------------------------ +-- STAGE 8 +------------------------------------------------------------------------ + +-- Stage 8 gives a term of the target a context Δ of type variables. +-- There is no quantifier. The statements are in the 4 statement modules +-- of `Wager/Poly`, each with its plain-English reading. This section +-- gives them their place in this file. It adds no statement. + +-- English: conversion is stable under a substitution of types; each +-- instance of a typed open term is typed; a typed term with no type +-- variable is a typed term of the target of stages 1 to 5; so each +-- closed instance is a typed term of the target, and progress and +-- preservation (T0) apply to it. +module T8-Statements + (S : Sig) (TS : Wager.L2.Signature.TSig S) (ops : GradeOps (Sig.TG S)) where + open Wager.Poly.Statements S TS ops public + using ( T8-Conv; T8-Inst; T8-Closed + ; T8-Closed-Instance; T8-Instance-Progress; T8-Instance-Preservation ) + +-- English: the translation of an open coercion is one typed open +-- function; each closed instance of it is the closed coercion function +-- of Stage 4; instantiation does not change a trope operation, so no +-- open term is the unwrap of a newtype at each instance of a type +-- variable. +module T8-Coercion-Statements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) where + open Wager.Poly.CoercionStatements SS Sc ops public + using ( T8-Type-Instance; T8-Coercion-Typed; T8-Coercion-Instance + ; T8-Ops-Rigid; T8-No-Uniform-Unwrap ) + +-- English: noninterference (T2) for a type with free type variables, +-- at the grade of each variable in the kinding context. +module T8-Role-Statements (RS : RoleSig) where + module ForTable (T : RoleTable) where + open Wager.Poly.RoleStatements.ForTable RS T public using (T8-Role) + open Wager.Poly.RoleStatements.Lawful RS public + using (T8-Role-Representational; T8-Role-Phantom; T8-Role-Nominal) + +-- English: in the signature with an identity family, no open type with +-- one type variable has the evidence types, or the data type of the +-- GADT program, as its instances. +module T8-Identity-Statements + (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) (b₀ : B₀) where + open Wager.Poly.IdentityStatements B₀ L₀ ty₀ ops b₀ public + using (Gᵍ; T8-Evidence-Rigid; T8-Gadt-Not-Open) From a62c03ae8b218883defb7c74b6ee92d73ee5a8de Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:21:18 +0000 Subject: [PATCH 07/11] docs(wager): Stage 8 records: design choices, ledgers, verdict sections, proof status - DESIGN-CHOICES.adoc: DC-8.1 to DC-8.7. - RELATION-LEDGER.adoc: R26 to R29. No ADDED entry. R26 is 'baseline, changed': the typing judgement of the extension has a context of type variables. The owner decides how it counts. - RULE-DIFF-LEDGER.adoc: no entry. The difference table of the extension. - VERDICT.adoc: new sections for Stage 8 at the end. No result of stages 1 to 7 changes. - PROOF-STATUS.adoc: a row for Stage 8. Records only. No Agda file is in this commit. The gate watch of Stage 8 and its record in TOOLCHAIN.adoc are not done yet. Co-Authored-By: Claude --- docs/status/PROOF-STATUS.adoc | 21 +- .../proofs/agda/Wager/DESIGN-CHOICES.adoc | 117 ++++++++++- .../proofs/agda/Wager/RELATION-LEDGER.adoc | 44 +++- .../proofs/agda/Wager/RULE-DIFF-LEDGER.adoc | 50 ++++- verification/proofs/agda/Wager/VERDICT.adoc | 190 ++++++++++++++++++ 5 files changed, 416 insertions(+), 6 deletions(-) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index b569f27..ade0e8a 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -24,7 +24,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. | ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 11 | MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | — | MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | — -| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation; stages 0 to 7 are done; 2 decisions are with the owner) | 1 | 1 | - | - +| WAGER: the wager experiment for coercions and roles, Cubical Agda (claims no ET obligation; stages 0 to 8 are done; Stage 9, the quantifier, has no proof yet; 2 decisions are with the owner) | 1 | 1 | - | - |=== The Done/In-progress claims above are scoped to the *mechanized core @@ -192,6 +192,25 @@ no file uses coinduction. One warning class is silenced | *Proven*, for each source signature that passes the role check. The denotation is by realisers: the development has no denotation of each typed term + +| 8 +| Terms with open types: a term is typed in a context of type variables. + There is no quantifier. `Wager.Proofs.t8-conv`, `t8-inst`, `t8-closed`, + `t8-closed-instance`, `t8-instance-progress`, `t8-instance-preservation` : + each closed instance of a typed open term is a typed term of the target. + `t8-coercion-typed`, `t8-coercion-instance` : the translation of an open + coercion is 1 typed open function, and each closed instance of it is the + closed coercion of Stage 4. `t8-role`, `t8-role-representational`, + `t8-role-phantom`, `t8-role-nominal` : noninterference for a type with + free type variables, at the grade of each variable. + The limits: `t8-ops-rigid`, `t8-no-uniform-unwrap`, `t8-evidence-rigid`, + `t8-gadt-not-open` +| *Proven*. The extension is in separate modules, and the target of stages + 1 to 5 does not change. 2 limits are checked: no open term is the unwrap + of a newtype at each instance of a type variable, and, in the one + signature with an identity family, no open type with 1 type variable has + the data type of the GADT program as its instances. There is no source + program with type variables and no theorem as T5 for one |=== == Mechanization slots diff --git a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc index 48bf4a4..22c2ecb 100644 --- a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc +++ b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: design choices -Status: entries of Stage 0 to Stage 5. +Status: entries of Stage 0 to Stage 8. :toc: left :sectnums!: @@ -670,3 +670,118 @@ A trope transition (wrap, unwrap) is thus an equivalence, and `ua unboxEquiv` is * congruence for a newtype gives the path of the body below the wrapper, by the role of the parameter. The path needs the source role check, as the typing of a translated coercion does (T3). + +== Stage 8 + +[[DC-8.1]] +=== DC-8.1: the owner chose open types first, and the quantifier next + +*The decision of the owner (2026-11-10).* "Open types now, quantifier next." + +* Stage 8: a term is typed in a context Δ of type variables. There is no `∀` type former. +* Stage 9: the quantifier. The owner accepts a plan before any proof of Stage 9. + +*Choice.* The modules of Stage 8 are in `Wager/Poly` and in `Wager/Examples/Stage8.agda`. No definition, no statement and no proof of the 79 modules of stages 1 to 7 changes. +The 3 index modules (`Everything.agda`, `Statements.agda`, `Proofs.agda`) get a section for Stage 8 at the end. `VERDICT.adoc` gets new sections, and its results of stages 1 to 7 do not change. + +*The reason for the stage.* Each limit of stages 3 to 6 that names "a type is closed" comes from one fact: a term has types `Ty [] ★` only (DC-3.1, DC-6.2). The type syntax of Stage 1 already has type variables, renaming and substitution. + +[[DC-8.2]] +=== DC-8.2: a term with open types, and its typing judgement + +*Choice.* `Tmᵖ Δ n` (`Wager.Poly.Term`) is the term syntax of the target with one change: the type of a binder is a type in the context Δ. The judgement `γ ▸ Γ ⊢ᵖ t ∶ A` (`Wager.Poly.Typing`) has the 12 rules of the target judgement, with the types in Δ. No rule is new. +The rule `t-step` uses the carrier of a trope operation. The carrier is a closed type of the signature, so the rule uses it through `⇑`, the renaming from the empty context. + +*Polymorphism without a quantifier.* A polymorphic program is an open term. An instance is the term `inst σ t`, for a substitution σ of types for the type variables. Instantiation is a function of Agda. It is not a term former: the calculus has no type abstraction and no type application. +`⌊_⌋` maps a term with no type variable to a term of the target of stages 1 to 5. + +*Limits.* + +* An open term has no reduction relation. Progress and preservation are statements about a closed instance (DC-8.3). +* A type variable has a kind, and a term uses a type of the kind ★. A term cannot take a type as an argument. +* The judgement has no kinding premise: a type in a term is a type of `Wager.L1.Syntax`, with its simple kind. The graded kinding judgement is not used by a typing rule. This is the same in stages 1 to 5. +* `Tmᵖ` has no substitution of terms and no renaming. Stage 8 does not need them. + +*Alternative.* A change of `Wager.L2.Term` to a term with a context Δ. This changes the modules of stages 1 to 7. The owner excluded it. + +[[DC-8.3]] +=== DC-8.3: what "T0 to T6 apply to a closed instance" means + +*What Agda checks.* `T8-Closed-Instance`: for a typed open term and a substitution σ into the empty context, the term `⌊ inst σ t ⌋` is a typed term of the target, with the same usage vector, at the instance of the type. It is the composition of `T8-Inst` and `T8-Closed`. +A theorem of stages 1 to 6 that is about each typed target term thus applies to the instance. Two are stated and proved for the instance: progress (`T8-Instance-Progress`, for each set of grade operations) and preservation (`T8-Instance-Preservation`, for the laws of a grade algebra). + +*What Agda does not check.* + +* The substitution part of T0 is not stated for an instance. It applies by the same composition. +* T3, T5 and T6 are statements about the translation of a source program. They are not about each target term. They apply to an instance that is the translation of a source program. For an open coercion this is `T8-Coercion-Instance` (DC-8.4). No statement of T3 is restated for an instance. +* T2 and T4 are statements about types. The statement of T2 for a type with free variables is `T8-Role` (DC-8.7). +* No statement is about the open term alone: Stage 8 has no theorem "an open term is safe" that does not go through an instance. + +[[DC-8.4]] +=== DC-8.4: open source types and open coercions + +*Choice.* An open source type (`OTy Δ`, `Wager.Poly.Coercion`) is a type variable of the kind ★, a closed source type, or a function, a pair or a sum of open source types. An open coercion (`Coᵒ`) is the identity, a closed representational coercion of Stage 3, symmetry, transitivity, or congruence for a function, a pair and a sum. +The translation `coerceᵒ c` is 1 open term. The transformers have the text of `Wager.Trans.Coercion`, with the types in Δ. + +*What Agda checks.* + +* `T8-Coercion-Typed`: for a source signature that passes the role check and for the laws of a grade algebra, `coerceᵒ c` has the open type `Tᵒ θ → Tᵒ φ`, with the usage vector `0ᵘ`. The laws are needed for the same reason as in Stage 4: the map of a function is a β-redex, and its usage vector is equal to the usage vector of its argument by the laws. +* `T8-Coercion-Instance`: for an instantiation ρ of the source and a substitution of the target that agrees with it, `⌊ inst s (coerceᵒ c) ⌋` and `coerceT (c ⟦ ρ ⟧ᶜ)` are equal as terms. The second term is the coercion function of Stage 4 for the instance of the coercion. +* `T8-Type-Instance`: the instance of the translation of an open source type is the translation of the instance. + +*Limits.* + +* A newtype with a parameter can be in an open source type at a closed argument only. `Tag a`, with a type variable a, is not an open source type (DC-8.5). +* A type-level function at a type variable, `F a`, is not an open source type. The target has the type `papp F (var x)`. Stage 8 does not translate to it. +* An open coercion has no nominal part other than a closed nominal coercion below `c-sub`. There is no coercion variable. +* There is no open source term and no translation of one. T5 is not stated for a program with type variables. +* `Agrees` is a hypothesis about the type variables of the kind ★. The statement says nothing about a type variable of another kind, and an open source type has none. + +[[DC-8.5]] +=== DC-8.5: a trope operation has a closed carrier + +*The fact.* A trope operation of a signature has one closed carrier type (`Wager.L2.Signature.TSig.carrier : Op → Ty [] ★`). In the target of Stage 4, the unwrap of `N τ` is the operation `(unwrap , N , τ)`: one operation for each closed source type τ (DC-4.3). +Instantiation of types does not change an operation: `inst σ (step o t)` is `step o (inst σ t)`. + +*What Agda checks.* `T8-Ops-Rigid`: each closed instance of an open term has the list of operations of the open term. `T8-No-Uniform-Unwrap`: if one open term has the coercion function `N τ₁ → body` at one instantiation and the coercion function `N τ₂ → body` at another instantiation, then τ₁ and τ₂ are one source type. +So the coercion `N a → body`, for a newtype N with a parameter and a type variable a, is not 1 open term of Stage 8. This holds for each source signature and each state scheme, the two-state scheme also: the cause is the closed carrier. + +*A second cause, for the row scheme.* The state of `N τ` is the index of τ (DC-4.1). It depends on the argument. A type with a type variable as the argument has no single state. Agda does not check a statement about this cause. + +*What can remove the limit.* A trope operation with type parameters: one operation `unwrap N` with a carrier in a context of type variables, and a rule `t-step` that instantiates it. This changes `TSig` and the rule `t-step`. It is not done. It is an input for the plan of Stage 9. + +[[DC-8.6]] +=== DC-8.6: the GADT program of Stage 6 is not 1 open term with 1 open type + +*The task.* The GADT program of Stage 6 as 1 open term with 1 open type, in the identity extension, or a checked reason why not. + +*Result.* Not done as 1 open term. The reason has a checked part and a part by inspection. + +*The checked part.* The identity family is a family of base constants, `Id A B`, for two closed types (DC-6.5). A substitution of types does not change a base constant. +In the signature of `Wager.Identity.Instance`, no open type with one type variable has the evidence type `Id α B` as its instance at each closed type α (`T8-Evidence-Rigid`), and none has the data type of the GADT program as its instance at each α (`T8-Gadt-Not-Open`). "Instance" is up to conversion. +The data type of the statement is the data type of the example of Stage 6 (`Wager.Examples.Stage8.Identity-Family.same-data`). + +*The part by inspection.* An open type with 3 type variables has the data type at each α, when the two other variables get the two evidence types (`three-variables`, checked). This does not give the program. The rule `t-cast` needs evidence of a type of the form `base (Id A B)`. A term of the type of a type variable is not such evidence, so the cast of the program has no typing with this open type. Agda does not check this sentence: Stage 8 has no identity extension with open types. + +*Limits of the checked part.* + +* One signature. Agda checked no other signature with an identity family. A signature with an inspection primitive that gives a constant of the family is not excluded. +* One type variable, of the kind ★. +* The statement is about a type. It is not a statement "no open term is the program". + +*What can remove the limit.* An identity type that is a type former with two type arguments, so that `Id a Int` is a type in a context with the variable a. The type language of Stage 1 has unary constants only. This changes `Ty`. It is not done. It is an input for the plan of Stage 9. + +[[DC-8.7]] +=== DC-8.7: the role of a type variable + +*Choice.* The role of a type variable is its grade in the kinding context: `γ ⊢ᵏ A` gives the type A a usage vector γ for its type variables (DC-1.3, R1). +`T8-Role` is noninterference for A: let two closed instantiations give each variable x two types that the observer `ρ · γ x` cannot tell apart. Then the observer ρ cannot tell the two instances of A apart. It holds for each composition table and each signature that respects its grades (`Valid`, as in T2). +The proof is the fundamental lemma of Stage 2, which is about a type in a context, and the lemma `eval-sub` of Stage 1. + +*The readable forms.* For the lawful table and one variable: `T8-Role-Representational`, `T8-Role-Phantom`, `T8-Role-Nominal`. + +*Notes.* + +* The statement `T8-Role` uses the definition `EnvLR` of `Wager.Role.Noninterference`, for a variable of each kind. `RoleStatements.agda` imports this definition from a module that also has proofs. +* `T8-Role-Nominal` has no kinding hypothesis and no hypothesis `Valid`. It says that an instance respects conversion of the argument. +* The typing judgement of terms does not use the kinding judgement (DC-8.2). The role of a type variable is a property of a type. No typing rule of Stage 8 checks it. diff --git a/verification/proofs/agda/Wager/RELATION-LEDGER.adoc b/verification/proofs/agda/Wager/RELATION-LEDGER.adoc index c649c8f..76c4b50 100644 --- a/verification/proofs/agda/Wager/RELATION-LEDGER.adoc +++ b/verification/proofs/agda/Wager/RELATION-LEDGER.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: relation ledger -Status: Stage 7 (the last stage). Each stage added its entries in the same commit as its rules. +Status: Stage 8. Each stage added its entries in the same commit as its rules, or in the commit of its records. :toc: left :sectnums: @@ -23,7 +23,8 @@ Each entry has one class: An ADDED entry counts against the wager. *Stages 1 to 5 and Stage 6, part 1 have no ADDED entry.* Stage 6, part 2 has 2 entries with no class (R23, R24). The task says that the owner decides how they count. -The ledger has one "baseline, changed" entry (R1). The owner decides how it counts. +The ledger has one "baseline, changed" entry for the target calculus (R1). The owner decides how it counts. +Stage 8 has no ADDED entry. It has one "baseline, changed" entry (R26): the typing judgement of the extension of Stage 8 has a context of type variables. The owner asked for this extension (DC-8.1), and the owner decides how it counts. == Judgement forms of the target calculus @@ -115,8 +116,9 @@ The ledger has one "baseline, changed" entry (R1). The owner decides how it coun | R13 | `LR`, `EnvLR` in `Wager.Role.Noninterference` (Stage 2) -| proof-internal +| proof-internal in stages 2 to 7; specification only since Stage 8 | The logical relation on closed values, indexed by the role of the observer. + Since Stage 8 the statement `T8-Role` uses `EnvLR` (DC-8.7). No rule uses it. |=== == Relations of the source calculus and of the erased calculus (Stage 3) @@ -245,9 +247,45 @@ The statements of T7, part 2 use the evaluation of untyped terms (R16) and obser |=== `⟦_⟧`, `pathOf` and `unboxEquiv` (`Wager.Univalent.Model`) are a function, a path and an equivalence. They are not relations. +== Stage 8 (terms with open types) + +Stage 8 is an extension in separate modules (`Wager/Poly`). No judgement and no relation of stages 1 to 7 changes. + +[cols="1,3,2,5",options="header"] +|=== +| Id | Agda identifier | Class | Notes + +| R26 +| `_▸_⊢ᵖ_∶_` in `Wager.Poly.Typing` +| baseline, changed +| The typing judgement for a term with open types. It has the form of R4 (`Γ ⊢ᵣ t : A` of 00-notation), and the types are in a context Δ of type variables. This is the change. + It is a new Agda data type (DC-8.2), with the 12 rules of R4. No rule is new. The only relation between types in a rule is `DefEq` (rule `t-conv`), at the context Δ. + R4 does not change. With no type variable, R26 gives R4 (`T8-Closed`). + The owner asked for the extension (DC-8.1). The owner decides how the entry counts. + +| R27 +| `Coᵒ` in `Wager.Poly.Coercion` +| source +| Representational coercions between open source types. Each instance is a coercion of R14 (`_⟦_⟧ᶜ`). The target has no such relation: the translation of an open coercion is a term (`coerceᵒ`). + +| R28 +| `Agrees` in `Wager.Poly.Coercion` +| specification only +| A substitution of the target agrees with an instantiation of the source. It is a hypothesis of `T8-Type-Instance` and of `T8-Coercion-Instance`. No rule uses it. + +| R29 +| `TyTrᵖ`, `IsoTypedᵖ`, `SemTyᵖ`, `Nat`, `NatIso` in `Wager.Poly.CoercionProofs` +| proof-internal +| A typed transformer of open terms, and a pair of transformers that agree on each instance. +|=== + +`inst`, `⌊_⌋`, `⇑`, `Tᵒ`, `_⟦_⟧`, `coIᵒ`, `coerceᵒ`, `opsOf` and `opsOfᵖ` are functions. They are not relations. +The statements about the identity family (`T8-Evidence-Rigid`, `T8-Gadt-Not-Open`) use `DefEq` (R2) and no other relation. + == What is absent * The target calculus has no coercion relation and no cast judgement. The coercion relation `Co` (R14) is in the source calculus only. The translation of Stage 4 makes each representational coercion a term of the target, with no new judgement. * Representational equivalence exists as "specification only" (R11). It is not a judgement of the calculus. * There is no subtyping relation between types. * The extension of Stage 6, part 2 has no equality judgement with assumptions and no cast judgement. It has a term former (`cast`) and a rule of the typing judgement (R23). +* Stage 8 has no quantifier over types, no type abstraction and no type application. Instantiation is a function of Agda (`inst`). It is not a judgement. diff --git a/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc b/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc index 6a6066b..e743599 100644 --- a/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc +++ b/verification/proofs/agda/Wager/RULE-DIFF-LEDGER.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: rule-diff ledger -Status: Stage 5. *The ledger is empty.* +Status: Stage 8. *The ledger is empty.* :toc: left :sectnums: @@ -136,3 +136,51 @@ The other statements of part 2 hold for each set of grade operations. == Stage 7 Stage 7 adds no typing rule and no kinding rule to the target calculus. The cross-check is a statement about a model of the target of Stage 4. + +== Stage 8 + +Stage 8 (terms with open types) is an extension of the target calculus, in separate modules (`Wager/Poly`). No rule of the target calculus changes. The extension adds no entry to this ledger. + +The evidence is structural, as for the target: `Wager.Poly.Typing` is a module with the parameter `ops : GradeOps (Sig.TG S)`. It takes the operations only. A rule can name a grade only as `𝟘`, as `𝟙`, or as a variable. + +The difference between the target and the extension: + +[cols="3,1,5",options="header"] +|=== +| Item | Count | Text + +| New judgement forms +| 0 +| The judgement `_▸_⊢ᵖ_∶_` has the form of the target judgement. Its types are in a context Δ of type variables (R26). + +| New typing rules +| 0 +| The 12 rules of `Wager.L2.Typing`, with the types in Δ. Each rule names the grades that its rule of the target names. + +| Changed typing rules +| 1 +| `t-step`: the carrier of a trope operation is a closed type of the signature, and the rule uses it in Δ through the renaming `⇑`. + +| New kinding rules +| 0 +| + +| New conversion rules +| 0 +| `DefEq` does not change. It is used at the context Δ. + +| New type formers +| 0 +| There is no `∀`. A type variable is in the type syntax of Stage 1. + +| New term formers +| 0 +| `Tmᵖ Δ n` has the 10 formers of `Tm n`. The type of a binder is a type in Δ. There is no type abstraction and no type application. + +| New entries of a signature +| 0 +| +|=== + +`T8-Coercion-Typed` and `T8-Instance-Preservation` have the hypothesis `GradeLaws`. The proof of the first uses the laws that the proof of Stage 4 uses (`zero-add`, `one-mul`, `mul-zero`, `add-zero`). The second uses preservation of Stage 1. A hypothesis of a theorem is not a side condition of a rule, so it is not an entry of this ledger. +The other statements of Stage 8 about terms hold for each set of grade operations. diff --git a/verification/proofs/agda/Wager/VERDICT.adoc b/verification/proofs/agda/Wager/VERDICT.adoc index 8910c21..3dfa88e 100644 --- a/verification/proofs/agda/Wager/VERDICT.adoc +++ b/verification/proofs/agda/Wager/VERDICT.adoc @@ -2,6 +2,7 @@ // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) = Wager: verdict Status: FINAL, after Stage 7 (2026-11-10). Two decisions are with the owner: the class of the kinding judgement (R1), and the class of the extension of Stage 6, part 2 (R23, R24). +Stage 8 (2026-11-10) adds sections at the end of this file. No result of stages 1 to 7 changes. :toc: left :sectnums: @@ -665,3 +666,192 @@ The draft asks the owner for 4 decisions: * The candidates are independent. The owner can take a part of the list. * W-9 and W-10 are two answers to one question. The owner can keep W-9 as the record of the limit with or without W-10. * Nothing in the experiment changes an existing obligation or its status. + +== Stage 8: terms with open types + +This section and the sections after it were added after the final verdict. They record Stage 8. They change no result above. + +*The decision of the owner (2026-11-10).* "Open types now, quantifier next." Stage 8 gives a term of the target a context Δ of type variables. It has no `∀` type former (DC-8.1). Stage 9 is the quantifier. It has a plan and no proof. + +*What Stage 8 is.* An extension of the target in separate modules (`Wager/Poly`). A term `Tmᵖ Δ n` has types in Δ, and the judgement `γ ▸ Γ ⊢ᵖ t ∶ A` has the 12 rules of the target judgement with the types in Δ (DC-8.2). A polymorphic program is an open term, and an instance is the term `inst σ t`. +The 79 modules of stages 1 to 7 keep each definition, each statement and each proof. The 3 index modules have a new section at the end. + +=== Status of each statement of Stage 8 + +Each statement is a type in a statement module of `Wager/Poly`, and `Wager.Statements` gives it a place (`T8-Statements`, `T8-Coercion-Statements`, `T8-Role-Statements`, `T8-Identity-Statements`). `Wager.Proofs` has one inhabitant for each. + +[cols="2,1,6",options="header"] +|=== +| Statement | Status | Evidence and reading + +| `T8-Conv` +| PROVED +| `Wager.Proofs.t8-conv`. Conversion of types is stable under a substitution of types. For each signature. + +| `T8-Inst` +| PROVED +| `Wager.Proofs.t8-inst`. Each instance of a typed open term is typed, with the same usage vector. The type and the context are the instances. For each signature, each term signature and each set of grade operations. + +| `T8-Closed` +| PROVED +| `Wager.Proofs.t8-closed`. A typed term with no type variable is a typed term of the target of stages 1 to 5. + +| `T8-Closed-Instance` +| PROVED +| `Wager.Proofs.t8-closed-instance`. Each closed instance of a typed open term is a typed term of the target. It is the composition of the 2 statements above. + +| `T8-Instance-Progress`, `T8-Instance-Preservation` +| PROVED +| `Wager.Proofs.t8-instance-progress`, `t8-instance-preservation`. T0 applies to each closed instance: progress for each set of grade operations, preservation for the laws of a grade algebra. + +| `T8-Type-Instance` +| PROVED +| `Wager.Proofs.t8-type-instance`. The translation of an open source type commutes with instantiation. + +| `T8-Coercion-Typed` +| PROVED +| `Wager.Proofs.t8-coercion-typed`. ONE POLYMORPHIC COERCION: the translation of an open coercion is 1 typed open function of the target, at the open types. For each source signature that passes the role check, each state scheme and the laws of a grade algebra. + +| `T8-Coercion-Instance` +| PROVED +| `Wager.Proofs.t8-coercion-instance`. Each closed instance of that open function is the closed coercion function of Stage 4 (`coerceT`) for the instance of the coercion. The two are equal as terms. For each source signature, each state scheme and each set of grade operations. + +| `T8-Ops-Rigid`, `T8-No-Uniform-Unwrap` +| PROVED (a limit) +| `Wager.Proofs.t8-ops-rigid`, `t8-no-uniform-unwrap`. Instantiation does not change a trope operation. So no open term is the coercion `N a → body` at two different instances of a type variable a, for a newtype N with a parameter (DC-8.5). + +| `T8-Role` +| PROVED +| `Wager.Proofs.t8-role`. Noninterference for a type with free type variables: two instantiations that the observer `ρ · γ x` cannot tell apart at each variable x give two instances that the observer ρ cannot tell apart. For each composition table, and for a signature that respects its grades (`Valid`, the hypothesis of T2). + +| `T8-Role-Representational`, `T8-Role-Phantom`, `T8-Role-Nominal` +| PROVED +| `Wager.Proofs.t8-role-representational`, `t8-role-phantom`, `t8-role-nominal`. The lawful table and one type variable: a grade at most representational respects `≈`; the grade phantom gives one normal form; at the grade nominal an instance respects conversion of the argument. + +| `T8-Evidence-Rigid`, `T8-Gadt-Not-Open` +| PROVED (a limit) +| `Wager.Proofs.t8-evidence-rigid`, `t8-gadt-not-open`. In the signature of `Wager.Identity.Instance`, no open type with one type variable has the evidence type `Id α B`, or the data type of the GADT program, as its instance at each closed type α (DC-8.6). +|=== + +=== The 4 tasks of Stage 8 + +. *Each closed instance of a typed open term is a typed term of the target, so T0 to T6 apply to it.* Done: `T8-Closed-Instance`. Progress and preservation are restated and proved for an instance. The other theorems are not restated (DC-8.3). T3, T5 and T6 are about the translation of a source program, so they apply to an instance that is such a translation. +. *One polymorphic coercion.* Done, for the open coercions of DC-8.4: `T8-Coercion-Typed` and `T8-Coercion-Instance`. The example is the coercion from `a → Age` to `a → Int` (`Wager.Examples.Stage8.Open-Coercions.poly`), with its instances at `a := Bool` and at `a := Age`. + Not done, with a checked reason: a coercion that unwraps a newtype at a type variable (`T8-No-Uniform-Unwrap`). +. *The role of a type variable.* Done: `T8-Role`, for each grade of the kinding context. +. *The GADT program of Stage 6 as 1 open term with 1 open type.* Not done. The checked reason is `T8-Evidence-Rigid` and `T8-Gadt-Not-Open`, with the limits of DC-8.6: one signature, one type variable, a statement about a type. One part of the reason is by inspection of the rule `t-cast`. + +=== Checked examples of Stage 8 + +`Wager.Examples.Stage8`: + +* Accepted: the polymorphic identity function `λ x : a. x` has the open type `a → a` (`idᵖ-typed`). Its instance at Int is the identity function at Int (`id-at-int`), a typed term of the target (`id-at-int-typed`), with progress (`id-at-int-progress`). +* Rejected: the same open term does not have the open type `a → Int` (`id-not-to-int`). The proof uses the instance at Bool and `identity-one-type` of Stage 6. +* Accepted: the polymorphic coercion from `a → Age` to `a → Int` is typed in the one-point grade algebra (`poly-typed`) and in the algebra `{0, 1, ω}` (`Open-Coercions-In-Affine.poly-typed`). Its instances at Bool and at Age are the 2 closed coercion functions of Stage 4 (`poly-at-bool`, `poly-at-age`). +* Accepted: an open coercion that unwraps `Tag Int`, a newtype with a parameter at a closed argument (`tag-closed-typed`). +* Rejected: no open term is the coercion `Tag a → Int` at the 2 instances `a := Int` and `a := Bool` (`no-poly-tag`). +* Accepted: the open type `a → Proxy a` has the variable at the grade representational, and its instances at Age and at Int are equivalent (`accepted-representational`). The open type `isAge Int` has the variable at the grade phantom, and its instances at Age and at Bool have one normal form (`accepted-phantom`). +* Rejected: kinding does not accept the grade representational for the variable of `isAge a`, and its instances at Age and at Int are not equivalent (`rejected`). +* Rejected: no open type with one type variable has the evidence type `Id α Int` at each α (`no-open-evidence`), and none has the data type of the GADT program (`no-open-data`). +* Accepted: an open type with 3 type variables has the data type at each α, when 2 variables get the 2 evidence types (`three-variables`). It does not give the program (DC-8.6). + +=== What Stage 8 changes in the limits of stages 3 to 6 + +"A type is closed" was a limit of stages 3 to 6 (DC-3.1, DC-6.2). Stage 8 removes a part of it and keeps a part of it. + +[cols="3,2,5",options="header"] +|=== +| Limit of an earlier stage | After Stage 8 | Evidence + +| A term of the target has closed types only. +| Removed, with no quantifier. +| `Tmᵖ`, `_▸_⊢ᵖ_∶_`, `T8-Inst`, `T8-Closed-Instance`. + +| A coercion is between closed types. +| Removed for a function, a pair and a sum of type variables and closed types. Kept for a newtype at a type variable. +| `T8-Coercion-Typed`, `T8-Coercion-Instance`; `T8-No-Uniform-Unwrap`. + +| T2 is about a closed type function and its argument. +| Removed: the statement is about a type with free variables. +| `T8-Role`. + +| A source term has no type variable (DC-3.1). +| Kept. +| Stage 8 has no source term with a type variable, and no theorem as T5 for one. + +| The statement of T7 is about each closed instance of the GADT program, and not about a polymorphic program (DC-6.2). +| Kept. +| `T8-Gadt-Not-Open`, DC-8.6. + +| There is no quantifier over types. +| Kept. It is the subject of Stage 9. +| DC-8.1. +|=== + +=== Not proved in Stage 8 + +* A statement about an open term that does not go through a closed instance. An open term has no reduction relation. +* The substitution part of T0 for an instance, and T3 for an instance of a polymorphic coercion. Each follows by composition with a proved statement, and Agda does not check a statement of it. +* A translation of a source program with type variables, and a theorem as T5 for it. +* An open coercion at a type-level function of a type variable (`F a`), and an open nominal coercion. +* That a trope operation with type parameters removes the limit of DC-8.5. This is a proposal, not a result. +* The limit of DC-8.6 for a signature other than `Wager.Identity.Instance`, for more than one type variable, and as a statement about terms. +* That the typing judgement of Stage 8 respects roles. No typing rule uses the kinding judgement (DC-8.2, DC-8.7). +* Parametricity. Stage 8 has no logical relation with relation variables. That is a part of Stage 9. + +=== Findings of Stage 8 + +[cols="1,8",options="header"] +|=== +| Id | Finding + +| F22 +| The type syntax, conversion and the noninterference proof of stages 1 and 2 were already about types in a context. Stage 8 needed no new lemma about types other than "conversion is stable under substitution" (`T8-Conv`). + The fundamental lemma of Stage 2 gives `T8-Role` with the lemma `eval-sub` of Stage 1. + +| F23 +| A trope operation has a closed carrier, and the target of Stage 4 has one unwrap operation for each closed instance of a newtype. So a coercion that unwraps a newtype at a type variable is not 1 open term (`T8-No-Uniform-Unwrap`). + The row scheme adds a second cause: the state of `N τ` depends on τ (DC-8.5). The first addition of the overall result (trope states with an index) thus has a cost for polymorphism. Agda checks the first cause and not the second. + +| F24 +| The identity family of Stage 6, part 2 is a family of base constants, and a substitution does not change a base constant. An equality with a type variable, such as `a ~ Int`, is not a type of the extension of Stage 6 in a context with the variable a (`T8-Evidence-Rigid`, for one signature). + The example of the task of Stage 6, `a ~ Int`, is thus still out of reach after Stage 8 (see F17). + +| F25 +| F23 and F24 have one shape: an entry of a signature is indexed by closed types (an operation by its carrier, a constant of the family by 2 types). An open type cannot name such an entry at a type variable. + A quantifier alone does not change this. Stage 9 needs a decision on signature entries with type parameters. + +| F26 +| No typing rule of the target, of the extension of Stage 6 or of Stage 8 uses the graded kinding judgement. The role of a type variable is a property of a type (`T8-Role`). The typing of a term does not check it. + This is by inspection of the 3 judgements. It was true in stages 1 to 7 and was not recorded as a finding. +|=== + +=== Changes to theorem statements in Stage 8 + +None after a statement was put in a statement module. + +Process notes: + +* The first freeze (`T8-Conv`, `T8-Inst`, `T8-Closed`) was committed (`326d25f`) before its proofs. The first version of the proofs (`a2c9619`) did not type-check: 3 transports had a motive with implicit indices. The repair (`893f830`) names the indices. It changes no statement. +* The second freeze (14 statements) was committed (`d7f4189`) before its proofs (`f2c8141`). The 3 modules of definitions that the statements name were written before the statements (`Poly/Term`, `Poly/Typing`, `Poly/Coercion`). They have no proof. +* Lemmas that existed before the statements: the fundamental lemma of Stage 2 and `eval-sub` of Stage 1 (for `T8-Role`), and the typing proof of Stage 4, whose shape the proof of `T8-Coercion-Typed` follows. +* `T8-Closed-Instance` is the composition of 2 statements that were proved before it was frozen. This is not the order "statement before proof" in substance. +* The commit `d7f4189` was pushed while the proof gate was red: the MANIFEST did not list the modules of `Wager/Poly`. The 2 earlier commits of the stage were pushed in the same state. The gate is green from the commit that adds the examples and the MANIFEST entries. + +=== Ledgers after Stage 8 + +* `RELATION-LEDGER.adoc`: no ADDED entry. One new "baseline, changed" entry, R26: the typing judgement of the extension of Stage 8 has a context of type variables. The owner asked for the extension, and the owner decides how the entry counts. + One new "source" entry (R27, open coercions), one "specification only" entry (R28) and one "proof-internal" entry (R29). The class of R13 is now "specification only": `T8-Role` uses `EnvLR`. +* `RULE-DIFF-LEDGER.adoc`: no entry. The extension has 0 new typing rules, 0 new term formers, 0 new type formers and 0 new judgement forms. One rule has a changed text: `t-step` uses the closed carrier through a renaming. + +=== Effect of Stage 8 on the overall result + +The overall result does not change: W does not hold as written, and W holds for the fragment with 2 additions. + +Stage 8 is not a part of the fragment of W. It answers a question about the limits of the fragment: + +* The target does not need closed types. A term with type variables has the same 12 rules, and each closed instance is a term of the target of stages 1 to 5. +* A representational coercion can be 1 polymorphic term, when it does not unwrap a newtype at a type variable. +* 2 limits stay, and each is checked for the cases that this section names: the unwrap of a newtype at a type variable, and an equality assumption with a type variable. + +A third decision is with the owner after Stage 8: the class of R26. From caa63ce2009ff6c61650d81dc2a428fcd261a7de Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:24:47 +0000 Subject: [PATCH 08/11] proof(wager): side item, freeze: the translation with a grade q, 9 statements A relayed question of the owner (2026-11-10): is the second addition of the verdict (an unrestricted grade 1) stronger than necessary? The candidate: a top grade q is enough, when the translation writes q. New modules, no proof: - Wager/Top/Translation.agda: the translation of Stage 4 with the grade q on each arrow and each binder of a source function (definitions). - Wager/Top/Statements.agda: Top-Coercion-Typed, Top-Coerce-Typed, Top-Typing-All (the candidate, to prove or to refute), Top-Typing (the candidate with no pair elimination and no case), Top-Same-Erasure, Top-Behaviour, Top-Nominal. - Wager/Top/AffineStatements.agda: Omega-Is-Top, Top-Typing-All-Fails. Agda 2.8.0 checks the 3 modules. The MANIFEST does not list them yet, so the gate is red at this commit. No module of stages 1 to 8 changes. Co-Authored-By: Claude --- .../agda/Wager/Top/AffineStatements.agda | 35 +++++ .../proofs/agda/Wager/Top/Statements.agda | 99 ++++++++++++++ .../proofs/agda/Wager/Top/Translation.agda | 128 ++++++++++++++++++ 3 files changed, 262 insertions(+) create mode 100644 verification/proofs/agda/Wager/Top/AffineStatements.agda create mode 100644 verification/proofs/agda/Wager/Top/Statements.agda create mode 100644 verification/proofs/agda/Wager/Top/Translation.agda diff --git a/verification/proofs/agda/Wager/Top/AffineStatements.agda b/verification/proofs/agda/Wager/Top/AffineStatements.agda new file mode 100644 index 0000000..3918db6 --- /dev/null +++ b/verification/proofs/agda/Wager/Top/AffineStatements.agda @@ -0,0 +1,35 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The variant of the translation with a grade q, in the algebra +-- {0, 1, ω} with q = ω: the statements, frozen before their proofs. +-- The source signature is `taggedS rep`, with the row scheme. +module Wager.Top.AffineStatements where + +open import Cubical.Foundations.Prelude +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Algebra +open import Wager.Grade.Affine using (affineOps; aω) +open import Wager.Role.Role using (rep) +open import Wager.FC.Tagged +import Wager.Trans.Scheme +import Wager.Top.Statements + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +open Wager.Top.Statements SS Sc affineOps aω + +-- English: ω is a top grade of the algebra {0, 1, ω}. +Omega-Is-Top : Type +Omega-Is-Top = IsTop + +-- English: THE CANDIDATE IS FALSE for the whole source fragment, in +-- the algebra {0, 1, ω} with q = ω. +Top-Typing-All-Fails : Type +Top-Typing-All-Fails = ¬ Top-Typing-All diff --git a/verification/proofs/agda/Wager/Top/Statements.agda b/verification/proofs/agda/Wager/Top/Statements.agda new file mode 100644 index 0000000..3b22be9 --- /dev/null +++ b/verification/proofs/agda/Wager/Top/Statements.agda @@ -0,0 +1,99 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The variant of the translation with a grade q: the statements, +-- frozen before their proofs. This file imports definitions and no +-- proof. +-- +-- The question of the owner: is the second addition of the verdict (an +-- unrestricted grade 𝟙) stronger than necessary? The candidate: a top +-- grade q is enough, when the translation writes q. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Top.Statements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) (q : R) where + +open import Cubical.Data.Nat.Base using (ℕ) +open import Cubical.Data.Sigma using (_×_; Σ-syntax) + +open import Wager.Role.Role using (rep; nom) +open import Wager.FC.Types SS +open import Wager.FC.Coercion SS +open import Wager.FC.Term SS +open import Wager.Top.Translation SS Sc ops q +open import Wager.Trans.Target SS Sc opsq using (tSig; tTSig; T; arr; ★; []) +open import Wager.Trans.Coercion SS Sc opsq using (Tm; fwd; eraseT) +import Wager.Trans.Coercion SS Sc ops as Stage4 +open import Wager.L1.Eval tSig using (nf) +open import Wager.L2.Typing tSig tTSig ops using (Usage; Cx; _▸_⊢_∶_; 0ᵘ) +open import Wager.Erased.LogRel litTy +open GradeOps ops using (𝟙; _≤_) + +-- The grade q is a top grade. +IsTop : Type +IsTop = ∀ r → r ≤ q + +-- Top-Coercion-Typed. For the laws of a grade algebra and a source +-- signature that passes the role check: the transformer of a +-- representational coercion maps a term of the type `T τ` to a term of +-- the type `T σ`, with the same usage vector. The types have the grade +-- q on each arrow. The statement has NO hypothesis on q. +Top-Coercion-Typed : Type +Top-Coercion-Typed = + GradeLaws ops → WellRoled → + ∀ {τ σ} (c : Co rep τ σ) {n} {γ : Usage n} {Γ : Cx n} {t : Tm n} → + γ ▸ Γ ⊢ t ∶ T τ → γ ▸ Γ ⊢ fwd (coIq rep c) t ∶ T σ + +-- Top-Coerce-Typed. The coercion function, with the grade q on its +-- binder, is typed when 𝟙 ≤ q. +Top-Coerce-Typed : Type +Top-Coerce-Typed = + GradeLaws ops → WellRoled → 𝟙 ≤ q → + ∀ {τ σ} (c : Co rep τ σ) {n} (Γ : Cx n) → + 0ᵘ ▸ Γ ⊢ coerceTq c ∶ arr q (T τ) (T σ) + +-- Top-Typing-All. THE CANDIDATE OF THE OWNER, for each term of the +-- source fragment: with a top grade q, the translation of a term of +-- the type τ has the type `T τ`, with the usage q for each variable. +-- This is a statement to prove or to refute. It is not claimed here. +Top-Typing-All : Type +Top-Typing-All = + GradeLaws ops → WellRoled → IsTop → + ∀ {n} {Γ : SCx n} {τ} (e : STm Γ τ) → + (λ _ → q) ▸ (λ i → T (Γ i)) ⊢ trq e ∶ T τ + +-- Top-Typing. The candidate for a source term with no elimination of a +-- pair and no `case`. +Top-Typing : Type +Top-Typing = + GradeLaws ops → WellRoled → IsTop → + ∀ {n} {Γ : SCx n} {τ} (e : STm Γ τ) → NoElim e → + (λ _ → q) ▸ (λ i → T (Γ i)) ⊢ trq e ∶ T τ + +-- Top-Same-Erasure. The variant and the translation of Stage 4 have +-- one erasure: the erasure does not read a grade. +Top-Same-Erasure : Type +Top-Same-Erasure = + ∀ {n} {Γ : SCx n} {τ} (e : STm Γ τ) → + eraseT (trq e) ≡ Stage4.eraseT (Stage4.tr e) + +-- Top-Behaviour. T5, behaviour, for the variant: for a closed source +-- term, the erased source term and the erased translation evaluate, +-- and the two values are observationally equal at the erased type. +Top-Behaviour : Type +Top-Behaviour = + WellRoled → ∀ {τ} (e : STm ∅ˢ τ) → + Σ[ v ∈ UVal ] Σ[ w ∈ UVal ] + (∅ᵉ ⊢ eraseTm e ⇓ v) × (∅ᵉ ⊢ eraseT (trq e) ⇓ w) × 𝒱 (er τ) v w + +-- Top-Nominal. T6 for the variant: for each nominal coercion, the two +-- translated types have one normal form. +Top-Nominal : Type +Top-Nominal = ∀ {τ σ} → Co nom τ σ → nf (T τ) ≡ nf (T σ) diff --git a/verification/proofs/agda/Wager/Top/Translation.agda b/verification/proofs/agda/Wager/Top/Translation.agda new file mode 100644 index 0000000..befdb79 --- /dev/null +++ b/verification/proofs/agda/Wager/Top/Translation.agda @@ -0,0 +1,128 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- A variant of the translation of Stage 4, with a grade q on each +-- arrow and on each binder that the translation of a source function +-- makes. Definitions only. +-- +-- The translation of Stage 4 writes the grade 𝟙 there. The question: +-- is a top grade q enough for the typing of a whole program, in the +-- place of an unrestricted grade 𝟙? +-- +-- The translation of types is the translation of Stage 4, read with q +-- in the place of 𝟙 (`opsq`). `opsq` is used for this reading only. The +-- typing judgement of the statements has the operations `ops`. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Top.Translation + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) (q : R) where + +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) +open import Cubical.Data.Unit using (Unit) +open import Cubical.Data.Empty using (⊥) + +open import Wager.Role.Role +open import Wager.FC.Types SS +open import Wager.FC.Coercion SS +open import Wager.FC.Term SS + +-- The operations of `ops`, with q in the place of 𝟙. +opsq : GradeOps R +opsq = record + { _+_ = GradeOps._+_ ops ; _·_ = GradeOps._·_ ops + ; 𝟘 = GradeOps.𝟘 ops ; 𝟙 = q ; _≤_ = GradeOps._≤_ ops } + +-- Types: `T (τ ⇒ˢ σ)` is `arr q (T τ) (T σ)`. +open import Wager.Trans.Target SS Sc opsq +-- Terms, and the transformers that name no grade. +open import Wager.Trans.Coercion SS Sc opsq + hiding (arrMap; arrIso; bodyIso; ntIso; coI; coerceT; tr) +open GradeOps ops using (𝟙) + +private + variable + n : ℕ + τ σ : STy + +-- The map of a function: (λf. λx. g (f (h x))) t. +-- The binder of f has the grade 𝟙: the map uses f one time. +-- The binder of x has the grade q: it is the binder of the result, +-- a function of the type `arr q A' B'`. +arrMapq : (X A : Ty [] ★) → Tr → Tr → Tr +arrMapq X A h g t = + tapp (tlam 𝟙 X (tlam q A (g (tapp (tvar (suc zero)) (h (tvar zero)))))) t + +arrIsoq : (A A' B B' : Ty [] ★) → Iso → Iso → Iso +arrIsoq A A' B B' i j = + iso (arrMapq (arr q A B) A' (bwd i) (fwd j)) + (arrMapq (arr q A' B') A (fwd i) (bwd j)) + +bodyIsoq : Body Base Fam → (X Y : Ty [] ★) → Iso → Iso +bodyIsoq bvar X Y i = i +bodyIsoq (bbase b) X Y i = idIso +bodyIsoq (barr β γ) X Y i = + arrIsoq (TB β X) (TB β Y) (TB γ X) (TB γ Y) (bodyIsoq β X Y i) (bodyIsoq γ X Y i) +bodyIsoq (bprod β γ) X Y i = prodIso (bodyIsoq β X Y i) (bodyIsoq γ X Y i) +bodyIsoq (bsum β γ) X Y i = sumIso (bodyIsoq β X Y i) (bodyIsoq γ X Y i) +bodyIsoq (bfam F β) X Y i = idIso + +ntIsoq : (N : N₁) (τ σ : STy) → Iso → Iso +ntIsoq N τ σ i = + iso (λ t → step (wrap , inr (N , σ)) (fwd b (step (unwrap , inr (N , τ)) t))) + (λ t → step (wrap , inr (N , τ)) (bwd b (step (unwrap , inr (N , σ)) t))) + where b = bodyIsoq (body N) (T τ) (T σ) i + +coIq : (r : Role) → Co r τ σ → Iso +coIq nom γ = idIso +coIq ph γ = idIso +coIq rep (c-sym γ) = swapIso (coIq rep γ) +coIq rep (c-trans γ δ) = compIso (coIq rep γ) (coIq rep δ) +coIq rep (c-sub γ) = idIso +coIq rep (c-arr {τ = τ} {τ' = τ'} {σ = σ} {σ' = σ'} γ δ) = + arrIsoq (T τ) (T τ') (T σ) (T σ') (coIq rep γ) (coIq rep δ) +coIq rep (c-prod γ δ) = prodIso (coIq rep γ) (coIq rep δ) +coIq rep (c-sum γ δ) = sumIso (coIq rep γ) (coIq rep δ) +coIq rep (c-nt₁ {τ = τ} {σ = σ} N γ) = ntIsoq N τ σ (coIq (mulG rep (role N)) γ) +coIq rep (c-ax₀ N) = stepIso (inl N) +coIq rep (c-ax₁ N τ) = stepIso (inr (N , τ)) + +-- The coercion as a function of the target, with the grade q. +coerceTq : Co rep τ σ → Tm n +coerceTq {τ = τ} γ = tlam q (T τ) (fwd (coIq rep γ) (tvar zero)) + +-- The translation of terms: each binder of a source function has the +-- grade q. +trq : ∀ {Γ : SCx n} → STm Γ τ → Tm n +trq (svar i) = tvar i +trq (slam {τ = τ} b) = tlam q (T τ) (trq b) +trq (sapp f a) = tapp (trq f) (trq a) +trq (spair s t) = pair (trq s) (trq t) +trq (sletp s b) = letp (trq s) (trq b) +trq (sinl t) = inj₁ (trq t) +trq (sinr t) = inj₂ (trq t) +trq (scase s l r) = case (trq s) (trq l) (trq r) +trq (slit ℓ) = lit ℓ +trq (cast γ e) = fwd (coIq rep γ) (trq e) + +-- A source term with no elimination of a pair and no `case`. +NoElim : ∀ {Γ : SCx n} → STm Γ τ → Type +NoElim (svar i) = Unit +NoElim (slam b) = NoElim b +NoElim (sapp f a) = NoElim f × NoElim a +NoElim (spair s t) = NoElim s × NoElim t +NoElim (sletp s b) = ⊥ +NoElim (sinl t) = NoElim t +NoElim (sinr t) = NoElim t +NoElim (scase s l r) = ⊥ +NoElim (slit ℓ) = Unit +NoElim (cast γ e) = NoElim e From db9397726d11b6f18077c6b7185621240df096b2 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:46:05 +0000 Subject: [PATCH 09/11] proof(wager): side item, proofs and a checked counterexample; Stage 8 warning lines Side item (the variant of the translation with a grade q, Wager/Top): - Top/Proofs.agda: top-coercion-typed, top-coerce-typed, top-typing, top-same-erasure, top-behaviour, top-nominal. - Top/Affine.agda: omega-is-top, top-typing-all-fails. The candidate 'a top grade is enough for each program' is false in the algebra {0, 1, omega} with q = omega: the translation of 'let (x, y) = (5, 5) in 5' has no type. - No frozen statement changed (freeze: caa63ce). - Index modules, MANIFEST (96 gated modules) and PROOF-STATUS.adoc. Stage 8: the line -WnoUnsupportedIndexedMatch is removed from the 5 files of Wager/Poly that give no such warning. scripts/check-proofs.sh agda: PASS, 96 modules. scripts/check-proof-status.sh: PASS. Co-Authored-By: Claude --- docs/status/PROOF-STATUS.adoc | 11 +- verification/proofs/agda/MANIFEST | 5 + .../proofs/agda/Wager/Everything.agda | 5 + .../agda/Wager/Poly/CoercionStatements.agda | 1 - .../agda/Wager/Poly/IdentityStatements.agda | 1 - .../agda/Wager/Poly/RoleStatements.agda | 1 - .../proofs/agda/Wager/Poly/Statements.agda | 1 - verification/proofs/agda/Wager/Poly/Term.agda | 1 - verification/proofs/agda/Wager/Proofs.agda | 39 ++ .../proofs/agda/Wager/Statements.agda | 26 ++ .../proofs/agda/Wager/Top/Affine.agda | 118 ++++++ .../agda/Wager/Top/AffineStatements.agda | 1 - .../proofs/agda/Wager/Top/Proofs.agda | 398 ++++++++++++++++++ .../proofs/agda/Wager/Top/Statements.agda | 1 - 14 files changed, 601 insertions(+), 8 deletions(-) create mode 100644 verification/proofs/agda/Wager/Top/Affine.agda create mode 100644 verification/proofs/agda/Wager/Top/Proofs.agda diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index ade0e8a..78c1f57 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -13,7 +13,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh. // Do not edit by hand without changing the MANIFEST accordingly. // gate:lean4 gated=20 quarantined=0 -// gate:agda gated=91 quarantined=0 +// gate:agda gated=96 quarantined=0 == Summary @@ -211,6 +211,15 @@ no file uses coinduction. One warning class is silenced signature with an identity family, no open type with 1 type variable has the data type of the GADT program as its instances. There is no source program with type variables and no theorem as T5 for one + +| 8, side item +| A variant of the translation with a grade q on each arrow and each + binder of a source function. `Wager.Proofs.top-typing`, + `top-coercion-typed`, `top-same-erasure`, `top-behaviour`, `top-nominal`, + `top-typing-all-fails` +| *Proven* for a top grade q and a source term with no elimination of a + pair and no `case`. *Refuted* for the whole fragment: a checked + counterexample in the algebra `{0, 1, ω}` with q = ω |=== == Mechanization slots diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST index 8572d32..82f5a4c 100644 --- a/verification/proofs/agda/MANIFEST +++ b/verification/proofs/agda/MANIFEST @@ -92,3 +92,8 @@ verification/proofs/agda|Wager/Poly/Role.agda|gated|Stage 8: noninterference for verification/proofs/agda|Wager/Poly/IdentityStatements.agda|gated|Stage 8: 2 statements about the identity family and open types (types only) verification/proofs/agda|Wager/Poly/IdentityRigid.agda|gated|Stage 8: in the signature with an identity family, no open type with 1 type variable has the evidence types or the GADT data type as its instances verification/proofs/agda|Wager/Examples/Stage8.agda|gated|Stage 8: accepted and rejected examples for open terms, open coercions, the role of a type variable and the identity family +verification/proofs/agda|Wager/Top/Translation.agda|gated|Side item after Stage 8: the translation of Stage 4 with a grade q on each arrow and each binder of a source function (definitions only) +verification/proofs/agda|Wager/Top/Statements.agda|gated|Side item after Stage 8: 7 statements about the variant with a grade q; one is the candidate of the owner, to prove or to refute (types only) +verification/proofs/agda|Wager/Top/AffineStatements.agda|gated|Side item after Stage 8: 2 statements in the algebra {0,1,omega} with q = omega (types only) +verification/proofs/agda|Wager/Top/Proofs.agda|gated|Side item after Stage 8: a coercion is typed for each q; a term with no pair elimination and no case is typed for a top grade q; one erasure with Stage 4, so T5 behaviour and T6 hold for the variant +verification/proofs/agda|Wager/Top/Affine.agda|gated|Side item after Stage 8: in {0,1,omega} with q = omega the candidate is false for the whole fragment (checked counterexample); accepted and rejected examples diff --git a/verification/proofs/agda/Wager/Everything.agda b/verification/proofs/agda/Wager/Everything.agda index 20d4154..986e08b 100644 --- a/verification/proofs/agda/Wager/Everything.agda +++ b/verification/proofs/agda/Wager/Everything.agda @@ -96,3 +96,8 @@ import Wager.Poly.Role import Wager.Poly.IdentityStatements import Wager.Poly.IdentityRigid import Wager.Examples.Stage8 +import Wager.Top.Translation +import Wager.Top.Statements +import Wager.Top.AffineStatements +import Wager.Top.Proofs +import Wager.Top.Affine diff --git a/verification/proofs/agda/Wager/Poly/CoercionStatements.agda b/verification/proofs/agda/Wager/Poly/CoercionStatements.agda index 521a12d..dc13ebb 100644 --- a/verification/proofs/agda/Wager/Poly/CoercionStatements.agda +++ b/verification/proofs/agda/Wager/Poly/CoercionStatements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Poly/IdentityStatements.agda b/verification/proofs/agda/Wager/Poly/IdentityStatements.agda index b9c1aac..45df5ac 100644 --- a/verification/proofs/agda/Wager/Poly/IdentityStatements.agda +++ b/verification/proofs/agda/Wager/Poly/IdentityStatements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Poly/RoleStatements.agda b/verification/proofs/agda/Wager/Poly/RoleStatements.agda index 74785f5..40fb4b2 100644 --- a/verification/proofs/agda/Wager/Poly/RoleStatements.agda +++ b/verification/proofs/agda/Wager/Poly/RoleStatements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Poly/Statements.agda b/verification/proofs/agda/Wager/Poly/Statements.agda index 8798ef6..4a63f38 100644 --- a/verification/proofs/agda/Wager/Poly/Statements.agda +++ b/verification/proofs/agda/Wager/Poly/Statements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Poly/Term.agda b/verification/proofs/agda/Wager/Poly/Term.agda index 5725b12..59d2094 100644 --- a/verification/proofs/agda/Wager/Poly/Term.agda +++ b/verification/proofs/agda/Wager/Poly/Term.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Proofs.agda b/verification/proofs/agda/Wager/Proofs.agda index 2b79744..0b1323b 100644 --- a/verification/proofs/agda/Wager/Proofs.agda +++ b/verification/proofs/agda/Wager/Proofs.agda @@ -81,6 +81,8 @@ import Wager.Poly.Proofs import Wager.Poly.CoercionProofs import Wager.Poly.Role import Wager.Poly.IdentityRigid +import Wager.Top.Proofs +import Wager.Top.Affine module _ where open T1-Statements @@ -411,3 +413,40 @@ module _ (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R t8-gadt-not-open : T8-Gadt-Not-Open t8-gadt-not-open = IR.t8-gadt-not-open + +------------------------------------------------------------------------ +-- SIDE ITEM AFTER STAGE 8 +------------------------------------------------------------------------ + +module _ (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) (q : R) where + open Top-Statements SS Sc ops q + private module TP = Wager.Top.Proofs SS Sc ops q + + top-coercion-typed : Top-Coercion-Typed + top-coercion-typed = TP.top-coercion-typed + + top-coerce-typed : Top-Coerce-Typed + top-coerce-typed = TP.top-coerce-typed + + top-typing : Top-Typing + top-typing = TP.top-typing + + top-same-erasure : Top-Same-Erasure + top-same-erasure = TP.top-same-erasure + + top-behaviour : Top-Behaviour + top-behaviour = TP.top-behaviour + + top-nominal : Top-Nominal + top-nominal = TP.top-nominal + +module _ where + open Top-Affine-Statements + + omega-is-top : Omega-Is-Top + omega-is-top = Wager.Top.Affine.omega-is-top + + -- The candidate `Top-Typing-All` is false in the algebra {0, 1, ω}. + top-typing-all-fails : Top-Typing-All-Fails + top-typing-all-fails = Wager.Top.Affine.top-typing-all-fails diff --git a/verification/proofs/agda/Wager/Statements.agda b/verification/proofs/agda/Wager/Statements.agda index ff8da9c..fb6ff8e 100644 --- a/verification/proofs/agda/Wager/Statements.agda +++ b/verification/proofs/agda/Wager/Statements.agda @@ -62,6 +62,8 @@ import Wager.Poly.Statements import Wager.Poly.CoercionStatements import Wager.Poly.RoleStatements import Wager.Poly.IdentityStatements +import Wager.Top.Statements +import Wager.Top.AffineStatements ------------------------------------------------------------------------ -- STAGE 1 @@ -891,3 +893,27 @@ module T8-Identity-Statements (B₀ L₀ : Type) (ty₀ : L₀ → B₀) {R : Type} (ops : GradeOps R) (b₀ : B₀) where open Wager.Poly.IdentityStatements B₀ L₀ ty₀ ops b₀ public using (Gᵍ; T8-Evidence-Rigid; T8-Gadt-Not-Open) + +------------------------------------------------------------------------ +-- SIDE ITEM AFTER STAGE 8: a top grade in the place of an unrestricted 𝟙 +------------------------------------------------------------------------ + +-- The variant of the translation of Stage 4 with a grade q on each +-- arrow and on each binder of a source function (`Wager/Top`). The +-- statements are in `Wager.Top.Statements`, each with its +-- plain-English reading. This section adds no statement. +-- +-- English: `Top-Typing-All` is the candidate "a top grade q is enough +-- for each program". It is a statement to refute, and +-- `Top-Typing-All-Fails` is its negation in the algebra {0, 1, ω} with +-- q = ω. `Top-Typing` is the candidate for a term with no elimination +-- of a pair and no `case`. +module Top-Statements + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) (q : R) where + open Wager.Top.Statements SS Sc ops q public + using ( IsTop; Top-Coercion-Typed; Top-Coerce-Typed; Top-Typing-All; Top-Typing + ; Top-Same-Erasure; Top-Behaviour; Top-Nominal ) + +module Top-Affine-Statements where + open Wager.Top.AffineStatements public using (Omega-Is-Top; Top-Typing-All-Fails) diff --git a/verification/proofs/agda/Wager/Top/Affine.agda b/verification/proofs/agda/Wager/Top/Affine.agda new file mode 100644 index 0000000..a160474 --- /dev/null +++ b/verification/proofs/agda/Wager/Top/Affine.agda @@ -0,0 +1,118 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The variant of the translation with a grade q, in the algebra +-- {0, 1, ω} with q = ω: proofs and examples. +-- +-- THE CANDIDATE IS FALSE for the whole fragment. The counterexample is +-- the source term `let (x, y) = (5, 5) in 5`. The rule `t-letp` binds +-- each component of a pair at the grade 𝟙, also in the variant. The +-- body drops the two components, and in this algebra 𝟘 ≤ 𝟙 is false. +module Wager.Top.Affine where + +open import Cubical.Foundations.Prelude +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; Σ-syntax; fst) +open import Cubical.Relation.Nullary using (¬_) + +open import Wager.Grade.Algebra +open import Wager.Grade.Finite using (false≢true) +open import Wager.Grade.Affine using (Affine; a0; a1; aω; affineOps; affineLaws; affine) +open import Wager.Role.Role using (rep) +open import Wager.FC.Signature +open import Wager.FC.Tagged +import Wager.FC.Types +import Wager.FC.Coercion +import Wager.FC.Term +import Wager.Trans.Scheme +import Wager.Trans.Target +import Wager.Trans.Coercion +import Wager.L2.Typing +import Wager.L2.Inversion +import Wager.Top.Translation +import Wager.Top.Statements +import Wager.Top.Proofs +open import Wager.Top.AffineStatements + +private + SS = taggedS rep + Sc = Wager.Trans.Scheme.rowScheme SS + +open Wager.FC.Types SS +open Wager.FC.Coercion SS +open Wager.FC.Term SS +open TTypes rep +open Wager.Top.Translation SS Sc affineOps aω +open Wager.Top.Statements SS Sc affineOps aω +private module P = Wager.Top.Proofs SS Sc affineOps aω +open Wager.Trans.Target SS Sc opsq using (tSig; tTSig; T; Ty; ★; []; arr) +open Wager.Trans.Coercion SS Sc opsq using (Tm; letp; lit) +open Wager.L2.Typing tSig tTSig affineOps + using (Usage; Cx; _▸_⊢_∶_; 0ᵘ; _▹_; _▹ᶜ_; t-letp; t-conv; t-sub) +open Wager.L2.Inversion tSig tTSig affine using (inv-lit) +open GradeOps affineOps using (𝟙) + +-- The role check of the signature. +wr : SSig.WellRoled SS +wr boxE = refl +wr tagE = refl +wr teeE = refl + +omega-is-top : Omega-Is-Top +omega-is-top a0 = refl +omega-is-top a1 = refl +omega-is-top aω = refl + +------------------------------------------------------------------------ +-- ACCEPTED. The function `λx. 5` drops its argument. The translation +-- of Stage 4 has no type for it in this algebra +-- (`Wager.Examples.Stage4.Coercions-In-Affine.const-rejected`). The +-- variant with q = ω has one. + +constFun : STm ∅ˢ (sInt ⇒ˢ sInt) +constFun = slam (slit ℓint) + +const-typed : (λ _ → aω) ▸ (λ i → T (∅ˢ i)) ⊢ trq constFun ∶ T (sInt ⇒ˢ sInt) +const-typed = P.top-typing affineLaws wr omega-is-top constFun tt + +-- ACCEPTED. A coercion function of the variant: Box Age → Box Int. Its +-- binder has the grade ω. +box-co : Co rep (Box sAge) (Box sInt) +box-co = c-nt₁ boxE (c-ax₀ ageE) + +box-typed : ∀ {n} (Γ : Cx n) → + 0ᵘ ▸ Γ ⊢ coerceTq box-co ∶ arr aω (T (Box sAge)) (T (Box sInt)) +box-typed Γ = P.top-coerce-typed affineLaws wr refl box-co Γ + +------------------------------------------------------------------------ +-- REJECTED. A pair elimination that drops a component. + +dropPair : STm ∅ˢ sInt +dropPair = sletp (spair (slit ℓint) (slit ℓint)) (slit ℓint) + +private + -- Inversion of the rule `t-letp`: the body has a derivation with the + -- grade 𝟙 for each of the two components. + inv-letp : ∀ {n} {γ : Usage n} {Γ : Cx n} {s : Tm n} {b : Tm (suc (suc n))} {C : Ty [] ★} → + γ ▸ Γ ⊢ letp s b ∶ C → + Σ[ δ ∈ Usage n ] Σ[ A ∈ Ty [] ★ ] Σ[ B ∈ Ty [] ★ ] Σ[ C' ∈ Ty [] ★ ] + ((δ ▹ 𝟙 ▹ 𝟙) ▸ (Γ ▹ᶜ A ▹ᶜ B) ⊢ b ∶ C') + inv-letp (t-letp d e) = _ , _ , _ , _ , e + inv-letp (t-conv d e) = inv-letp d + inv-letp (t-sub d le) = inv-letp d + +-- The translation of `dropPair` has no type, for each usage vector, +-- each context and each type. +drop-rejected : ∀ {γ : Usage 0} {Γ : Cx 0} {C} → ¬ (γ ▸ Γ ⊢ trq dropPair ∶ C) +drop-rejected d = + let (δ , A , B , C' , e) = inv-letp d + in false≢true (fst (inv-lit e) zero) + +top-typing-all-fails : Top-Typing-All-Fails +top-typing-all-fails h = drop-rejected (h affineLaws wr omega-is-top dropPair) diff --git a/verification/proofs/agda/Wager/Top/AffineStatements.agda b/verification/proofs/agda/Wager/Top/AffineStatements.agda index 3918db6..0d5fdec 100644 --- a/verification/proofs/agda/Wager/Top/AffineStatements.agda +++ b/verification/proofs/agda/Wager/Top/AffineStatements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- diff --git a/verification/proofs/agda/Wager/Top/Proofs.agda b/verification/proofs/agda/Wager/Top/Proofs.agda new file mode 100644 index 0000000..f9e0de6 --- /dev/null +++ b/verification/proofs/agda/Wager/Top/Proofs.agda @@ -0,0 +1,398 @@ +{-# OPTIONS --cubical --safe #-} +{-# OPTIONS --guardedness #-} +{-# OPTIONS -WnoUnsupportedIndexedMatch #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- The variant of the translation with a grade q: proofs. +-- +-- 1. Typing of a coercion, in each grade algebra and for each q. The +-- proof has the shape of `Wager.Trans.Typing`. The map of a +-- function binds the function at 𝟙 and the argument at q. +-- 2. Typing of a term with no pair elimination and no `case`, for a +-- top grade q. +-- 3. The variant and the translation of Stage 4 have one erasure. So +-- the behaviour part of T5 holds for the variant. +-- 4. T6 for the variant: the theorem of Stage 5, read with q in the +-- place of 𝟙. +open import Cubical.Foundations.Prelude +open import Wager.FC.Signature +open import Wager.Grade.Algebra +import Wager.Trans.Scheme + +module Wager.Top.Proofs + (SS : SSig) (Sc : Wager.Trans.Scheme.StateScheme SS) + {R : Type} (ops : GradeOps R) (q : R) where + +open import Cubical.Data.Bool.Base using (true; false) +open import Cubical.Data.Empty as ⊥ using (⊥) +open import Cubical.Data.Unit using (Unit; tt) +open import Cubical.Data.Nat.Base using (ℕ; zero; suc) +open import Cubical.Data.FinData.Base using (Fin; zero; suc) +open import Cubical.Data.Sigma using (_×_; _,_; fst; snd) +open import Cubical.Data.Sum.Base using (_⊎_; inl; inr) + +open import Wager.Grade.Finite using (false≢true) +open import Wager.Role.Role +open import Wager.FC.Types SS +open import Wager.FC.Coercion SS +open import Wager.FC.Term SS +open import Wager.FC.RoleSoundness SS using (nomZ-l; nomZ-r; nomZ-idem) +open import Wager.Top.Translation SS Sc ops q +open import Wager.Top.Statements SS Sc ops q +open import Wager.Trans.Target SS Sc opsq +open import Wager.Trans.Nominal SS Sc opsq using (nominal-defeq; nominal-nf; T-inst; T-embE) +open import Wager.Trans.Coercion SS Sc opsq + hiding (arrMap; arrIso; bodyIso; ntIso; coI; coerceT; tr) +import Wager.Trans.Coercion SS Sc ops as S4 +import Wager.Trans.Target SS Sc ops as T4 +import Wager.Trans.Simulation +open import Wager.L1.Conversion tSig +open import Wager.L2.Typing tSig tTSig ops + using ( Usage; 0ᵘ; _+ᵘ_; _·ᵘ_; _≤ᵘ_; _▹_; unit; Cx; _▹ᶜ_; _▸_⊢_∶_ + ; t-var; t-lam; t-app; t-pair; t-letp; t-inj₁; t-inj₂; t-case + ; t-lit; t-step; t-conv; t-sub ) +open import Wager.Erased.Untyped +open GradeOps ops + +private + variable + n : ℕ + X Y Z X' Y' : Ty [] ★ + + castU : {γ γ' : Usage n} {Γ : Cx n} {t : Tm n} {A : Ty [] ★} → + γ ≡ γ' → γ ▸ Γ ⊢ t ∶ A → γ' ▸ Γ ⊢ t ∶ A + castU {Γ = Γ} {t} {A} p d = subst (λ z → z ▸ Γ ⊢ t ∶ A) p d + + castT : {γ : Usage n} {Γ : Cx n} {t : Tm n} {A B : Ty [] ★} → + A ≡ B → γ ▸ Γ ⊢ t ∶ A → γ ▸ Γ ⊢ t ∶ B + castT {γ = γ} {Γ} {t} p d = subst (λ z → γ ▸ Γ ⊢ t ∶ z) p d + +------------------------------------------------------------------------ +-- 1 and 2. Typing, for the laws of a grade algebra. + +module Typed (laws : GradeLaws ops) where + open GradeLaws laws + + TyTr : (X Y : Ty [] ★) → Tr → Type + TyTr X Y f = ∀ {n} {γ : Usage n} {Γ : Cx n} {t : Tm n} → + γ ▸ Γ ⊢ t ∶ X → γ ▸ Γ ⊢ f t ∶ Y + + IsoTyped : Ty [] ★ → Ty [] ★ → Iso → Type + IsoTyped X Y i = TyTr X Y (fwd i) × TyTr Y X (bwd i) + + id-typed : DefEq X Y → IsoTyped X Y idIso + id-typed e = (λ d → t-conv d e) , (λ d → t-conv d (d-sym e)) + + swap-typed : ∀ {i} → IsoTyped X Y i → IsoTyped Y X (swapIso i) + swap-typed (f , g) = g , f + + comp-typed : ∀ {i j} → IsoTyped X Y i → IsoTyped Y Z j → IsoTyped X Z (compIso i j) + comp-typed (f , g) (f' , g') = (λ d → f' (f d)) , (λ d → g (g' d)) + + -- The function f is bound at 𝟙 and used one time. The argument x is + -- bound at q: the function f has an arrow of the grade q, so the use + -- of x counts q · 𝟙. + arrMapq-typed : ∀ {h g : Tr} → TyTr X' X h → TyTr Y Y' g → + TyTr (arr q X Y) (arr q X' Y') (arrMapq (arr q X Y) X' h g) + arrMapq-typed th tg {γ = γ} d = + castU (funExt λ i → zero-add (𝟙 · γ i) ∙ one-mul (γ i)) + (t-app + (t-lam {γ = 0ᵘ} + (t-lam {γ = 0ᵘ ▹ 𝟙} + (castU eq (tg (t-app (t-var (suc zero)) (th (t-var zero))))))) + d) + where + eq : ∀ {n} → (unit {n = suc (suc n)} (suc zero) +ᵘ (q ·ᵘ unit zero)) ≡ (0ᵘ ▹ 𝟙 ▹ q) + eq = funExt λ { zero → zero-add (q · 𝟙) ∙ mul-one q + ; (suc zero) → cong (𝟙 +_) (mul-zero q) ∙ add-zero 𝟙 + ; (suc (suc i)) → cong (𝟘 +_) (mul-zero q) ∙ add-zero 𝟘 } + + arrIsoq-typed : ∀ {i j} → IsoTyped X X' i → IsoTyped Y Y' j → + IsoTyped (arr q X Y) (arr q X' Y') (arrIsoq X X' Y Y' i j) + arrIsoq-typed (f , g) (f' , g') = arrMapq-typed g f' , arrMapq-typed f g' + + prodMap-typed : ∀ {f g : Tr} → TyTr X X' f → TyTr Y Y' g → + TyTr (X ⊗ Y) (X' ⊗ Y') (prodMap f g) + prodMap-typed tf tg {γ = γ} d = + castU (funExt λ i → add-zero (γ i)) + (t-letp {δ = 0ᵘ} d + (castU eq (t-pair (tf (t-var (suc zero))) (tg (t-var zero))))) + where + eq : ∀ {n} → (unit {n = suc (suc n)} (suc zero) +ᵘ unit zero) ≡ (0ᵘ ▹ 𝟙 ▹ 𝟙) + eq = funExt λ { zero → zero-add 𝟙 + ; (suc zero) → add-zero 𝟙 + ; (suc (suc i)) → add-zero 𝟘 } + + prodIso-typed : ∀ {i j} → IsoTyped X X' i → IsoTyped Y Y' j → + IsoTyped (X ⊗ Y) (X' ⊗ Y') (prodIso i j) + prodIso-typed (f , g) (f' , g') = prodMap-typed f f' , prodMap-typed g g' + + sumMap-typed : ∀ {f g : Tr} → TyTr X X' f → TyTr Y Y' g → + TyTr (X ⊕ Y) (X' ⊕ Y') (sumMap f g) + sumMap-typed tf tg {γ = γ} d = + castU (funExt λ i → add-zero (γ i)) + (t-case {δ = 0ᵘ} d (t-inj₁ (tf (t-var zero))) (t-inj₂ (tg (t-var zero)))) + + sumIso-typed : ∀ {i j} → IsoTyped X X' i → IsoTyped Y Y' j → + IsoTyped (X ⊕ Y) (X' ⊕ Y') (sumIso i j) + sumIso-typed (f , g) (f' , g') = sumMap-typed f f' , sumMap-typed g g' + + step-typed : (x : Inst) → IsoTyped (capp (stateOf x) (carrierOf x)) (carrierOf x) (stepIso x) + step-typed x = (λ d → t-step (unwrap , x) d) , (λ d → t-step (wrap , x) d) + + module _ {d : Role} (hn : leR nom d ≡ true → DefEq X Y) where + + body-defeq : ∀ β → leR (mulZ nom (roleOf β)) d ≡ true → DefEq (TB β X) (TB β Y) + body-defeq bvar le = hn le + body-defeq (bbase b) le = d-refl + body-defeq (barr β γ) le = + d-arr (body-defeq β (leR-trans _ _ _ (nomZ-l (roleOf β) (roleOf γ)) le)) + (body-defeq γ (leR-trans _ _ _ (nomZ-r (roleOf β) (roleOf γ)) le)) + body-defeq (bprod β γ) le = + d-prod (body-defeq β (leR-trans _ _ _ (nomZ-l (roleOf β) (roleOf γ)) le)) + (body-defeq γ (leR-trans _ _ _ (nomZ-r (roleOf β) (roleOf γ)) le)) + body-defeq (bsum β γ) le = + d-sum (body-defeq β (leR-trans _ _ _ (nomZ-l (roleOf β) (roleOf γ)) le)) + (body-defeq γ (leR-trans _ _ _ (nomZ-r (roleOf β) (roleOf γ)) le)) + body-defeq (bfam F β) le = + d-papp (body-defeq β (subst (λ r → leR r d ≡ true) (nomZ-idem (roleOf β)) le)) + + module _ {i : Iso} (hv : leR rep d ≡ true → IsoTyped X Y i) where + + body-typed : ∀ β → leR (roleOf β) d ≡ true → + IsoTyped (TB β X) (TB β Y) (bodyIsoq β X Y i) + body-typed bvar le = hv le + body-typed (bbase b) le = id-typed d-refl + body-typed (barr β γ) le = + arrIsoq-typed (body-typed β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typed γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typed (bprod β γ) le = + prodIso-typed (body-typed β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typed γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typed (bsum β γ) le = + sumIso-typed (body-typed β (leR-trans _ _ _ (max-upper-l (roleOf β) (roleOf γ)) le)) + (body-typed γ (leR-trans _ _ _ (max-upper-r (roleOf β) (roleOf γ)) le)) + body-typed (bfam F β) le = id-typed (d-papp (body-defeq β le)) + + SemTy : Role → STy → STy → Iso → Type + SemTy nom τ σ i = DefEq (T τ) (T σ) + SemTy rep τ σ i = IsoTyped (T τ) (T σ) i + SemTy ph τ σ i = Unit + + module _ (wr : WellRoled) where + + private + nt-wrap : ∀ N {τ σ i} → + IsoTyped (TB (body N) (T τ)) (TB (body N) (T σ)) (bodyIsoq (body N) (T τ) (T σ) i) → + IsoTyped (T (nt₁ N τ)) (T (nt₁ N σ)) (ntIsoq N τ σ i) + nt-wrap N {τ} {σ} (f , g) = + (λ d → t-step (wrap , inr (N , σ)) (f (t-step (unwrap , inr (N , τ)) d))) + , (λ d → t-step (wrap , inr (N , τ)) (g (t-step (unwrap , inr (N , σ)) d))) + + nt-typed : ∀ N d {τ σ} → leR (roleOf (body N)) d ≡ true → + (γ : Co d τ σ) → SemTy d τ σ (coIq d γ) → + IsoTyped (T (nt₁ N τ)) (T (nt₁ N σ)) (ntIsoq N τ σ (coIq d γ)) + nt-typed N rep le γ sem = + nt-wrap N (body-typed (λ p → ⊥.rec (false≢true p)) {i = coIq rep γ} (λ _ → sem) (body N) le) + nt-typed N nom le γ sem = + nt-wrap N (body-typed (λ _ → sem) {i = idIso} (λ _ → id-typed sem) (body N) le) + nt-typed N ph le γ sem = + nt-wrap N (body-typed (λ p → ⊥.rec (false≢true p)) {i = idIso} + (λ p → ⊥.rec (false≢true p)) (body N) le) + + coIq-typed : ∀ r {τ σ} (γ : Co r τ σ) → SemTy r τ σ (coIq r γ) + coIq-typed nom γ = nominal-defeq γ + coIq-typed ph γ = tt + coIq-typed rep (c-sym γ) = swap-typed (coIq-typed rep γ) + coIq-typed rep (c-trans γ δ) = comp-typed (coIq-typed rep γ) (coIq-typed rep δ) + coIq-typed rep (c-sub γ) = id-typed (nominal-defeq γ) + coIq-typed rep (c-arr γ δ) = arrIsoq-typed (coIq-typed rep γ) (coIq-typed rep δ) + coIq-typed rep (c-prod γ δ) = prodIso-typed (coIq-typed rep γ) (coIq-typed rep δ) + coIq-typed rep (c-sum γ δ) = sumIso-typed (coIq-typed rep γ) (coIq-typed rep δ) + coIq-typed rep (c-nt₁ N γ) = + nt-typed N (mulG rep (role N)) (wr N) γ (coIq-typed (mulG rep (role N)) γ) + coIq-typed rep (c-ax₀ N) = + subst (λ Z → IsoTyped (T (nt₀ N)) Z (stepIso (inl N))) + (sym (T-embE (rep₀ N))) (step-typed (inl N)) + coIq-typed rep (c-ax₁ N τ) = + subst (λ Z → IsoTyped (T (nt₁ N τ)) Z (stepIso (inr (N , τ)))) + (sym (T-inst (body N) τ)) (step-typed (inr (N , τ))) + + -- 2. A term with no pair elimination and no `case`, for a top grade. + module _ (top : IsTop) where + + private + Qs : Usage n → Type + Qs γ = ∀ i → γ i ≡ q + + qs-ext : {γ : Usage n} → Qs γ → Qs (γ ▹ q) + qs-ext o zero = refl + qs-ext o (suc i) = o i + + -- Each usage vector is below a vector of top grades. + top-le : (δ : Usage n) {γ : Usage n} → Qs γ → δ ≤ᵘ γ + top-le δ o i = subst (δ i ≤_) (sym (o i)) (top (δ i)) + + Agree : Cx n → SCx n → Type + Agree Δ Γ = ∀ i → Δ i ≡ T (Γ i) + + agree-ext : ∀ {Δ : Cx n} {Γ : SCx n} τ → Agree Δ Γ → Agree (Δ ▹ᶜ T τ) (Γ ▹ˢ τ) + agree-ext τ h zero = refl + agree-ext τ h (suc i) = h i + + trq-typed′ : ∀ {Γ : SCx n} {τ} (e : STm Γ τ) → NoElim e → + (γ : Usage n) (Δ : Cx n) → Qs γ → Agree Δ Γ → γ ▸ Δ ⊢ trq e ∶ T τ + trq-typed′ (svar i) ne γ Δ o h = t-sub (castT (h i) (t-var i)) (top-le _ o) + trq-typed′ (slam {τ = τ} b) ne γ Δ o h = + t-lam (trq-typed′ b ne (γ ▹ q) (Δ ▹ᶜ T τ) (qs-ext o) (agree-ext τ h)) + trq-typed′ (sapp f a) (nf , na) γ Δ o h = + t-sub (t-app (trq-typed′ f nf γ Δ o h) (trq-typed′ a na γ Δ o h)) (top-le _ o) + trq-typed′ (spair s t) (ns , nt) γ Δ o h = + t-sub (t-pair (trq-typed′ s ns γ Δ o h) (trq-typed′ t nt γ Δ o h)) (top-le _ o) + trq-typed′ (sinl t) ne γ Δ o h = t-inj₁ (trq-typed′ t ne γ Δ o h) + trq-typed′ (sinr t) ne γ Δ o h = t-inj₂ (trq-typed′ t ne γ Δ o h) + trq-typed′ (slit ℓ) ne γ Δ o h = t-sub (t-lit ℓ) (top-le _ o) + trq-typed′ (cast c e) ne γ Δ o h = fst (coIq-typed rep c) (trq-typed′ e ne γ Δ o h) + +top-coercion-typed : Top-Coercion-Typed +top-coercion-typed laws wr c d = fst (Typed.coIq-typed laws wr rep c) d + +top-coerce-typed : Top-Coerce-Typed +top-coerce-typed laws wr le c Γ = + t-lam {γ = 0ᵘ} + (t-sub (fst (Typed.coIq-typed laws wr rep c) (t-var zero)) + (λ { zero → le ; (suc i) → GradeLaws.le-refl laws 𝟘 })) + +top-typing : Top-Typing +top-typing laws wr top {Γ = Γ} e ne = + Typed.trq-typed′ laws wr top e ne (λ _ → q) (λ i → T (Γ i)) (λ i → refl) (λ i → refl) + +------------------------------------------------------------------------ +-- 3. One erasure. The erasure does not read a grade or a type. + +private + -- A transformer of the variant and a transformer of Stage 4 that + -- keep "the two terms have one erasure". + Er : Tr → S4.Tr → Type + Er f f4 = ∀ {n} (t : Tm n) (t4 : S4.Tm n) → + eraseT t ≡ S4.eraseT t4 → eraseT (f t) ≡ S4.eraseT (f4 t4) + + infixr 4 _,ᵉ_ + record ErIso (i : Iso) (i4 : S4.Iso) : Type where + constructor _,ᵉ_ + field + eraF : Er (fwd i) (S4.fwd i4) + eraB : Er (bwd i) (S4.bwd i4) + open ErIso + + id-er : ErIso idIso S4.idIso + id-er = (λ t t4 p → p) ,ᵉ (λ t t4 p → p) + + swap-er : ∀ {i i4} → ErIso i i4 → ErIso (swapIso i) (S4.swapIso i4) + swap-er (f ,ᵉ g) = g ,ᵉ f + + comp-er : ∀ {i i4 j j4} → ErIso i i4 → ErIso j j4 → + ErIso (compIso i j) (S4.compIso i4 j4) + comp-er {i} {i4} {j} {j4} (f ,ᵉ g) (f' ,ᵉ g') = + (λ t t4 p → f' (fwd i t) (S4.fwd i4 t4) (f t t4 p)) + ,ᵉ (λ t t4 p → g (bwd j t) (S4.bwd j4 t4) (g' t t4 p)) + + arrMap-er : ∀ {X A : Ty [] ★} {X4 A4 : T4.Ty [] T4.★} {h g : Tr} {h4 g4 : S4.Tr} → + Er h h4 → Er g g4 → Er (arrMapq X A h g) (S4.arrMap X4 A4 h4 g4) + arrMap-er {h = h} {h4 = h4} eh eg t t4 p i = + uapp (ulam (ulam (eg (tapp (tvar (suc zero)) (h (tvar zero))) + (S4.tapp (S4.tvar (suc zero)) (h4 (S4.tvar zero))) + (λ j → uapp (uvar (suc zero)) (eh (tvar zero) (S4.tvar zero) refl j)) i))) + (p i) + + arrIso-er : ∀ {A A' B B' : Ty [] ★} {A4 A'4 B4 B'4 : T4.Ty [] T4.★} {i i4 j j4} → + ErIso i i4 → ErIso j j4 → + ErIso (arrIsoq A A' B B' i j) (S4.arrIso A4 A'4 B4 B'4 i4 j4) + arrIso-er {A = A} {A'} {B} {B'} {A4} {A'4} {B4} {B'4} {i} {i4} {j} {j4} (f ,ᵉ g) (f' ,ᵉ g') = + arrMap-er {X = arr q A B} {A = A'} {X4 = T4.arr 𝟙 A4 B4} {A4 = A'4} + {h = bwd i} {g = fwd j} {h4 = S4.bwd i4} {g4 = S4.fwd j4} g f' + ,ᵉ arrMap-er {X = arr q A' B'} {A = A} {X4 = T4.arr 𝟙 A'4 B'4} {A4 = A4} + {h = fwd i} {g = bwd j} {h4 = S4.fwd i4} {g4 = S4.bwd j4} f g' + + prodMap-er : ∀ {f g : Tr} {f4 g4 : S4.Tr} → Er f f4 → Er g g4 → + Er (prodMap f g) (S4.prodMap f4 g4) + prodMap-er ef eg t t4 p i = + uletp (p i) (upair (ef (tvar (suc zero)) (S4.tvar (suc zero)) refl i) + (eg (tvar zero) (S4.tvar zero) refl i)) + + prodIso-er : ∀ {i i4 j j4} → ErIso i i4 → ErIso j j4 → + ErIso (prodIso i j) (S4.prodIso i4 j4) + prodIso-er {i} {i4} {j} {j4} (f ,ᵉ g) (f' ,ᵉ g') = + prodMap-er {f = fwd i} {g = fwd j} {f4 = S4.fwd i4} {g4 = S4.fwd j4} f f' + ,ᵉ prodMap-er {f = bwd i} {g = bwd j} {f4 = S4.bwd i4} {g4 = S4.bwd j4} g g' + + sumMap-er : ∀ {f g : Tr} {f4 g4 : S4.Tr} → Er f f4 → Er g g4 → + Er (sumMap f g) (S4.sumMap f4 g4) + sumMap-er ef eg t t4 p i = + ucase (p i) (uinl (ef (tvar zero) (S4.tvar zero) refl i)) + (uinr (eg (tvar zero) (S4.tvar zero) refl i)) + + sumIso-er : ∀ {i i4 j j4} → ErIso i i4 → ErIso j j4 → + ErIso (sumIso i j) (S4.sumIso i4 j4) + sumIso-er {i} {i4} {j} {j4} (f ,ᵉ g) (f' ,ᵉ g') = + sumMap-er {f = fwd i} {g = fwd j} {f4 = S4.fwd i4} {g4 = S4.fwd j4} f f' + ,ᵉ sumMap-er {f = bwd i} {g = bwd j} {f4 = S4.bwd i4} {g4 = S4.bwd j4} g g' + + step-er : (x : Inst) → ErIso (stepIso x) (S4.stepIso x) + step-er x = (λ t t4 p → p) ,ᵉ (λ t t4 p → p) + + body-er : ∀ β (X Y : Ty [] ★) (X4 Y4 : T4.Ty [] T4.★) {i i4} → ErIso i i4 → + ErIso (bodyIsoq β X Y i) (S4.bodyIso β X4 Y4 i4) + body-er bvar X Y X4 Y4 e = e + body-er (bbase b) X Y X4 Y4 e = id-er + body-er (barr β γ) X Y X4 Y4 e = arrIso-er (body-er β X Y X4 Y4 e) (body-er γ X Y X4 Y4 e) + body-er (bprod β γ) X Y X4 Y4 e = prodIso-er (body-er β X Y X4 Y4 e) (body-er γ X Y X4 Y4 e) + body-er (bsum β γ) X Y X4 Y4 e = sumIso-er (body-er β X Y X4 Y4 e) (body-er γ X Y X4 Y4 e) + body-er (bfam F β) X Y X4 Y4 e = id-er + + nt-er : ∀ N τ σ {i i4} → ErIso i i4 → ErIso (ntIsoq N τ σ i) (S4.ntIso N τ σ i4) + nt-er N τ σ e = + (λ t t4 p → eraF b (step (unwrap , inr (N , τ)) t) (S4.step (T4.unwrap , inr (N , τ)) t4) p) + ,ᵉ (λ t t4 p → eraB b (step (unwrap , inr (N , σ)) t) (S4.step (T4.unwrap , inr (N , σ)) t4) p) + where b = body-er (body N) (T τ) (T σ) (T4.T τ) (T4.T σ) e + + coI-er : ∀ r {τ σ} (γ : Co r τ σ) → ErIso (coIq r γ) (S4.coI r γ) + coI-er nom γ = id-er + coI-er ph γ = id-er + coI-er rep (c-sym γ) = swap-er (coI-er rep γ) + coI-er rep (c-trans γ δ) = comp-er (coI-er rep γ) (coI-er rep δ) + coI-er rep (c-sub γ) = id-er + coI-er rep (c-arr γ δ) = arrIso-er (coI-er rep γ) (coI-er rep δ) + coI-er rep (c-prod γ δ) = prodIso-er (coI-er rep γ) (coI-er rep δ) + coI-er rep (c-sum γ δ) = sumIso-er (coI-er rep γ) (coI-er rep δ) + coI-er rep (c-nt₁ {τ = τ} {σ = σ} N γ) = nt-er N τ σ (coI-er (mulG rep (role N)) γ) + coI-er rep (c-ax₀ N) = step-er (inl N) + coI-er rep (c-ax₁ N τ) = step-er (inr (N , τ)) + +top-same-erasure : Top-Same-Erasure +top-same-erasure (svar i) = refl +top-same-erasure (slam b) = cong ulam (top-same-erasure b) +top-same-erasure (sapp f a) = cong₂ uapp (top-same-erasure f) (top-same-erasure a) +top-same-erasure (spair s t) = cong₂ upair (top-same-erasure s) (top-same-erasure t) +top-same-erasure (sletp s b) = cong₂ uletp (top-same-erasure s) (top-same-erasure b) +top-same-erasure (sinl t) = cong uinl (top-same-erasure t) +top-same-erasure (sinr t) = cong uinr (top-same-erasure t) +top-same-erasure (scase s l r) i = + ucase (top-same-erasure s i) (top-same-erasure l i) (top-same-erasure r i) +top-same-erasure (slit ℓ) = refl +top-same-erasure (cast c e) = + ErIso.eraF (coI-er rep c) (trq e) (S4.tr e) (top-same-erasure e) + +-- The behaviour part of T5, moved along the equality of the erasures. +top-behaviour : Top-Behaviour +top-behaviour wr e = + let (v , w , d , d' , h) = Wager.Trans.Simulation.behaviour SS Sc ops wr e + in v , w , d , subst (λ u → ∅ᵉ ⊢ u ⇓ w) (sym (top-same-erasure e)) d' , h + +------------------------------------------------------------------------ +-- 4. T6. The theorem of Stage 5 holds for each set of grade +-- operations, so it holds with q in the place of 𝟙. + +top-nominal : Top-Nominal +top-nominal = nominal-nf diff --git a/verification/proofs/agda/Wager/Top/Statements.agda b/verification/proofs/agda/Wager/Top/Statements.agda index 3b22be9..67646e2 100644 --- a/verification/proofs/agda/Wager/Top/Statements.agda +++ b/verification/proofs/agda/Wager/Top/Statements.agda @@ -1,6 +1,5 @@ {-# OPTIONS --cubical --safe #-} {-# OPTIONS --guardedness #-} -{-# OPTIONS -WnoUnsupportedIndexedMatch #-} -- SPDX-License-Identifier: MPL-2.0 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) -- From b61653f09d246e01b94d7dcd4751e7323f1f62e1 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:46:05 +0000 Subject: [PATCH 10/11] docs(wager): gate watch of Stage 8, trust base, and the records of the side item - TOOLCHAIN.adoc: the gate watch of Stage 8 (11 deliberate defects, each makes the gate fail), the gate watch of the side item, and the test of the silenced warning for the 17 new files. - VERDICT.adoc: the trust base after Stage 8, and a new section for the side item with finding F27. The overall result is not rewritten. - DESIGN-CHOICES.adoc: DC-8.8. Co-Authored-By: Claude --- .../proofs/agda/Wager/DESIGN-CHOICES.adoc | 25 +++++ verification/proofs/agda/Wager/TOOLCHAIN.adoc | 93 +++++++++++++++++++ verification/proofs/agda/Wager/VERDICT.adoc | 64 +++++++++++++ 3 files changed, 182 insertions(+) diff --git a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc index 22c2ecb..5bfcd1a 100644 --- a/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc +++ b/verification/proofs/agda/Wager/DESIGN-CHOICES.adoc @@ -785,3 +785,28 @@ The proof is the fundamental lemma of Stage 2, which is about a type in a contex * The statement `T8-Role` uses the definition `EnvLR` of `Wager.Role.Noninterference`, for a variable of each kind. `RoleStatements.agda` imports this definition from a module that also has proofs. * `T8-Role-Nominal` has no kinding hypothesis and no hypothesis `Valid`. It says that an instance respects conversion of the argument. * The typing judgement of terms does not use the kinding judgement (DC-8.2). The role of a type variable is a property of a type. No typing rule of Stage 8 checks it. + +== Side item after Stage 8: a top grade in the place of an unrestricted grade `𝟙` + +[[DC-8.8]] +=== DC-8.8: the variant of the translation with a grade q + +*The question of the owner (2026-11-10, relayed by the parent session).* Is the second addition of the verdict, an unrestricted grade `𝟙` (`𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙`), stronger than necessary? The candidate: a top grade q (`∀ r → r ≤ q`) is enough, when the translation writes q. + +*Choice.* A variant of the translation in new modules (`Wager/Top`). No module of stages 1 to 8 changes. + +* Types: the translation of types of Stage 4, read with q in the place of `𝟙`. `T (τ ⇒ˢ σ)` is `arr q (T τ) (T σ)`. The module `Wager.Trans.Target` is used with the operations `opsq`, which are the operations with q for `𝟙`. `opsq` is used for this reading only: the typing judgement of each statement has the operations of the algebra. +* Terms: the binder of a source function has the grade q (`trq`). +* The map of a function in a coercion (`arrMapq`) binds the function at `𝟙` and the argument at q. With q on the two binders, the map of a pair of functions has no typing by the derivation of Stage 4: the map of a pair binds a component at `𝟙`, and a function with the binder grade q then uses the component at `q · 𝟙`. Agda did not check that no other derivation exists. + +*Result.* The candidate is FALSE for the whole source fragment, and TRUE for a part of it. + +* TRUE: for a top grade q and the laws of a grade algebra, each source term with no elimination of a pair and no `case` has a typed translation with the usage q for each variable (`Top-Typing`). A coercion is typed for each q, with no hypothesis on q (`Top-Coercion-Typed`). +* FALSE: in the algebra `{0, 1, ω}` with q = ω, the translation of `let (x, y) = (5, 5) in 5` has no type (`Wager.Top.Affine.drop-rejected`, `Top-Typing-All-Fails`). + +*The cause.* The rules `t-letp` and `t-case` of Stage 1 bind a component of a pair and the variable of a branch at the grade `𝟙` (finding F13). The translation does not choose this grade. A program that drops such a variable needs `𝟘 ≤ 𝟙`. +A program that gives such a variable to a function of the variant needs `q ≤ 𝟙`, by the same reading of the rule `t-app`. With a top grade q this makes `𝟙` a top grade, and then `𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙` hold. Agda does not check this second sentence. + +*Behaviour and T6.* The variant and the translation of Stage 4 have one erasure (`Top-Same-Erasure`), so the behaviour part of T5 holds for the variant (`Top-Behaviour`). T6 holds for the variant (`Top-Nominal`): the theorem of Stage 5 holds for each set of grade operations. + +*Not done.* A target with a graded pair or a graded `case`, in which a component has a grade other than `𝟙`. `VERDICT.adoc` already says that the target has no pair with a graded component. T3 and the cross-check of Stage 7 for the variant. A proof that the condition of `Top-Typing` is necessary. diff --git a/verification/proofs/agda/Wager/TOOLCHAIN.adoc b/verification/proofs/agda/Wager/TOOLCHAIN.adoc index 222b95b..3846cb5 100644 --- a/verification/proofs/agda/Wager/TOOLCHAIN.adoc +++ b/verification/proofs/agda/Wager/TOOLCHAIN.adoc @@ -424,3 +424,96 @@ A clean build of `Wager/Everything.agda` (79 modules) takes about 48 seconds and The second test shows that the proof depends on the rule "a wrapper is not seen at run time". The third test fails in the model, before the proof: a wrong path does not have the type of a path between the two interpretations. + +=== Gate watch at the end of Stage 8 (terms with open types) + +The toolchain was installed again on a new machine on 2026-11-10, by the steps of this file. The checksum of the archive matched, the commit of the library matched, and `agda --version` printed the text above. + +A clean build of `Wager/Everything.agda` at the end of Stage 8 (91 modules) takes about 56 seconds and prints no warning. + +Each row is one change, alone. After each change the 2 commands `agda --safe Wager/Everything.agda` and `scripts/check-proofs.sh agda` ran, and the change was removed. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Examples/Stage8.agda`: a false lemma (the instance of the polymorphic identity at Int has the binder type Bool) +| `[UnequalTerms] bInt != bBool` in `id-at-int` +| FAIL + +| `Wager/Poly/Term.agda`: `⌊ tapp f a ⌋` swaps the function and the argument +| `[UnequalTerms] f != a` in `Wager.Poly.Proofs.t8-closed` +| FAIL + +| `Wager/Poly/Typing.agda`: the rule `t-app` does not scale the usage of the argument +| `[UnequalTerms]` in `Wager.Poly.Proofs.t8-closed`, the case of `t-app` +| FAIL + +| `Wager/Poly/Coercion.agda`: the translation of a symmetric open coercion does not swap the 2 directions +| `[MismatchedProjectionsError]` (`bwdᵖ` and `fwdᵖ`) in `Wager.Poly.CoercionProofs.coIᵒ-typed` +| FAIL + +| `Wager/Poly/Coercion.agda`: `opsOfᵖ` drops the operation of a `step` +| `[UnequalTerms]` in `Wager.Poly.CoercionProofs.t8-ops-rigid` +| FAIL + +| `Wager/Poly/Coercion.agda`: `coerceᵒ` gives its binder the type of the result +| `[UnequalTerms] φ != θ` in `Wager.Poly.CoercionProofs.t8-coercion-typed` +| FAIL + +| `Wager/Examples/Stage8.agda`: a kinding derivation for `isAge a` with the variable at the grade representational +| `[UnequalTerms] false != true` in the subusage proof +| FAIL + +| `Wager/Examples/Stage8.agda`: the base constant `Id Int Int` as an open type with the evidence type at each instance +| `[UnequalTerms]`: the code of `Int` is not the code of the normal form of α +| FAIL + +| `Wager/Poly/Role.agda`: the phantom lemma uses the observer representational +| `[UnequalTerms]`: `≈` is not `≡`, in `t8-role-phantom` +| FAIL + +| `Wager/Poly/Proofs.agda`: `postulate t8-by-fiat : T8-Closed` +| `[SafeFlagPostulate]`. `scan-dangerous.sh` also fails. +| FAIL + +| `Wager/Poly/CoercionProofs.agda`: a hole in `t8-type-instance` +| `[SolvedButOpenHoles]` in `Wager/Proofs.agda`: the module cannot be imported +| FAIL + +| All changes removed +| None +| PASS. The gate passed with 91 files before the watch. After the watch it ran with the 5 files of the side item: PASS, 96 files. +|=== + +The second and the third test show that the proof of `T8-Closed` depends on the map `⌊_⌋` and on the text of a rule. +The fifth test shows that the limit `T8-No-Uniform-Unwrap` depends on the list of operations. + +The machine was restarted during the tenth test. The tenth and the eleventh test ran again after the restart, with the same 2 commands. + +=== Gate watch for the side item after Stage 8 (the variant with a grade q) + +A build of `Wager/Everything.agda` (96 modules) prints no warning. + +[cols="3,3,1",options="header"] +|=== +| Change | Error from Agda | Gate + +| `Wager/Top/Translation.agda`: the map of a function binds the function at the grade q +| `[UnequalTerms] q != 𝟙` in `Wager.Top.Proofs.arrMapq-typed` +| FAIL + +| `Wager/Top/Translation.agda`: the binder of a source function has the grade `𝟙` +| `[UnequalTerms] 𝟙 != q` in `Wager.Top.Proofs.trq-typed′` +| Not run. `agda --safe Wager/Everything.agda` fails. + +| All changes removed +| None +| PASS, 96 files +|=== + +The first test shows that the typing of a coercion in the variant depends on the grade of the 2 binders of the map of a function (DC-8.8). + +=== The silenced warning in stages 8 and after + +Of the 12 files of Stage 8, 7 have the line `-WnoUnsupportedIndexedMatch`. Of the 5 files of the side item, 3 have the line. For each of these 17 files a test without the line was made: the 10 files that have the line give the warning, and the 7 other files give none. diff --git a/verification/proofs/agda/Wager/VERDICT.adoc b/verification/proofs/agda/Wager/VERDICT.adoc index 3dfa88e..c92d2fe 100644 --- a/verification/proofs/agda/Wager/VERDICT.adoc +++ b/verification/proofs/agda/Wager/VERDICT.adoc @@ -844,6 +844,13 @@ Process notes: One new "source" entry (R27, open coercions), one "specification only" entry (R28) and one "proof-internal" entry (R29). The class of R13 is now "specification only": `T8-Role` uses `EnvLR`. * `RULE-DIFF-LEDGER.adoc`: no entry. The extension has 0 new typing rules, 0 new term formers, 0 new type formers and 0 new judgement forms. One rule has a changed text: `t-step` uses the closed carrier through a renaming. +=== Trust base after Stage 8 and the side item + +* The trust base does not change: Agda 2.8.0 with `--cubical --safe`, `agda/cubical` v0.9, no `postulate`, no hole, no termination pragma, no positivity pragma. `--guardedness` is on in each file, and no file uses coinduction. +* The development has 96 files: 79 of stages 1 to 7, 12 of Stage 8 and 5 of the side item. +* The warning `UnsupportedIndexedMatch` is silenced in 55 of the 96 files: the 45 files of stages 1 to 7, 7 files of Stage 8 and 3 files of the side item. For each of the 17 new files a test without the line was made (`TOOLCHAIN.adoc`). +* The gate watch of Stage 8 has 11 deliberate defects. Each made the gate fail. + === Effect of Stage 8 on the overall result The overall result does not change: W does not hold as written, and W holds for the fragment with 2 additions. @@ -855,3 +862,60 @@ Stage 8 is not a part of the fragment of W. It answers a question about the limi * 2 limits stay, and each is checked for the cases that this section names: the unwrap of a newtype at a type variable, and an equality assumption with a type variable. A third decision is with the owner after Stage 8: the class of R26. + +== Side item after Stage 8: is the second addition stronger than necessary? + +This section was added after the final verdict. It does not rewrite the overall result. The wording of W is the decision of the owner. + +*The question of the owner (2026-11-10, relayed by the parent session).* The second addition is: for a whole program, a grade algebra in which the grade `𝟙` is unrestricted (`𝟘 ≤ 𝟙` and `𝟙 + 𝟙 ≤ 𝟙`). Is it enough that the algebra has a top grade q, if the translation writes q? + +*Answer.* Not for the whole fragment. Yes for the part of the fragment with no elimination of a pair and no `case`. +The variant of the translation is in `Wager/Top` (DC-8.8). Each statement was frozen (`caa63ce`) before its proof. + +[cols="2,1,6",options="header"] +|=== +| Statement (`Wager.Top.Statements`, `Wager.Top.AffineStatements`) | Status | Evidence and reading + +| `Top-Typing-All` (the candidate) +| REFUTED +| `Wager.Top.Affine.top-typing-all-fails`. In the algebra `{0, 1, ω}` with q = ω, for the signature `taggedS rep` and the row scheme, the translation of `let (x, y) = (5, 5) in 5` has no type, for each usage vector, each context and each type (`drop-rejected`). ω is a top grade there (`omega-is-top`). + +| `Top-Typing` +| PROVED +| `Wager.Top.Proofs.top-typing`. For a source signature that passes the role check, the laws of a grade algebra and a top grade q: each source term with no elimination of a pair and no `case` has a typed translation, with the usage q for each variable. + +| `Top-Coercion-Typed`, `Top-Coerce-Typed` +| PROVED +| `Wager.Top.Proofs.top-coercion-typed`, `top-coerce-typed`. The transformer of a coercion keeps the usage vector, for each q and each grade algebra: no hypothesis on q. The coercion function with the binder grade q needs `𝟙 ≤ q`. + The map of a function is not the map of Stage 4 with q for `𝟙`: it binds the function at `𝟙` and the argument at q (DC-8.8). + +| `Top-Same-Erasure`, `Top-Behaviour` +| PROVED +| `Wager.Top.Proofs.top-same-erasure`, `top-behaviour`. The variant and the translation of Stage 4 have one erasure. The behaviour part of T5 thus holds for the variant, for each term of the fragment. + +| `Top-Nominal` +| PROVED +| `Wager.Top.Proofs.top-nominal`. T6 for the variant. +|=== + +Checked instance in the algebra `{0, 1, ω}` with q = ω (`Wager.Top.Affine`): the function `λx. 5` is typed (`const-typed`). The translation of Stage 4 has no type for it there (`const-rejected`). A coercion function is typed with the binder grade ω (`box-typed`). + +*What this says about the second addition.* The second addition has a weaker sufficient form for a part of the fragment: a top grade q, with the translation `trq`, for programs with no elimination of a pair and no `case`. For the whole fragment the weaker form is not sufficient. +The cause is in the target and not in the translation: the rules `t-letp` and `t-case` bind at the grade `𝟙` (F13, F27). + +*Not proved.* + +* That the second addition is necessary for the whole fragment. The counterexample is in one algebra. +* The typing of a program with `letp` or `case` in the variant under the hypotheses of the second addition. This was not tried. +* T3 and the cross-check of Stage 7 for the variant. +* A target with a graded pair or a graded `case`. With such a rule the candidate can hold for the whole fragment. This is a proposal and not a result. + +[cols="1,8",options="header"] +|=== +| Id | Finding + +| F27 +| A top grade does not replace an unrestricted grade `𝟙` for the whole fragment. The translation can write a top grade q on each arrow and each binder of a function, and a function that drops its argument is then typed in the algebra `{0, 1, ω}` (`const-typed`). + The elimination of a pair and `case` bind at `𝟙` by a rule of the target, so a program that drops a component still needs `𝟘 ≤ 𝟙` (`drop-rejected`). + The second addition is thus a fact about 2 rules of the target, `t-letp` and `t-case`, and not about the translation of functions. +|=== From d2d957a781c8843890b90cf14523930ad0e9b556 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 23:46:50 +0000 Subject: [PATCH 11/11] docs(wager): plan of Stage 9 (the quantifier), a proposal for the owner Status: PROPOSAL. The owner did not accept it. No proof of Stage 9 exists, and none starts before the owner accepts a plan. The plan has 4 decisions for the owner (D1 to D4), each with a recommended option and with the most complete long-term form named. Co-Authored-By: Claude --- .../proofs/agda/Wager/PLAN-STAGE9.adoc | 153 ++++++++++++++++++ 1 file changed, 153 insertions(+) create mode 100644 verification/proofs/agda/Wager/PLAN-STAGE9.adoc diff --git a/verification/proofs/agda/Wager/PLAN-STAGE9.adoc b/verification/proofs/agda/Wager/PLAN-STAGE9.adoc new file mode 100644 index 0000000..686bb9e --- /dev/null +++ b/verification/proofs/agda/Wager/PLAN-STAGE9.adoc @@ -0,0 +1,153 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Wager: plan of Stage 9, the quantifier +Status: PROPOSAL of 2026-11-10. The owner did not accept it yet. No proof of Stage 9 exists, and none starts before the owner accepts a plan. +:sectnums: + +== Goal + +Stage 9 adds the quantifier to the target with open types of Stage 8: a `∀` type former, type abstraction and type application, and a logical relation with relation variables. +A proof is a success. A checked counterexample is a success. A vague result is a failure. + +The overall result of `VERDICT.adoc` is about the fragment of claim W. Stage 9 is outside that fragment, as Stage 8 is. It can change no result of stages 1 to 8. + +== What Stage 8 gives to Stage 9 + +. Terms with open types, and their typing judgement with the 12 rules of the target (`Wager/Poly`, DC-8.2). +. Instantiation of the types of a term (`inst`), and the lemma that it keeps typing, for a substitution into each context (`T8-Inst`). This is the type-substitution lemma that the rule of type application needs. +. Conversion is stable under a substitution of types (`T8-Conv`). +. Noninterference for a type with free variables (`T8-Role`). +. Two checked limits with one shape (F25): an entry of a signature is indexed by closed types. A trope operation has a closed carrier (DC-8.5), and a constant of the identity family has 2 closed types (DC-8.6). A quantifier alone does not remove them. + +== Four decisions for the owner + +Each decision has a recommended option, written first. The text says which option is the most complete long-term form. + +=== D1: where the quantifier lives + +[cols="1,4,3",options="header"] +|=== +| Option | Text | Cost and risk + +| D1-a (recommended) +| A layer of type schemes over the type language of Stage 1, which does not change. A scheme is a type of Stage 1, a quantifier `∀ k. S`, or a function, a pair or a sum of schemes. A type variable stands for a type of Stage 1, so instantiation is predicative. + New modules only. No module of stages 1 to 8 changes. +| Moderate. Conversion of schemes is the congruence of `DefEq`, and its normal form is `nf` in each leaf. No second normalisation proof. + The limit: a type variable cannot stand for a quantified type. GHC has this limit by default. + +| D1-b (the most complete long-term form) +| A second type language with `∀` as a type former of the kind ★, beside the language of Stage 1. Instantiation is impredicative, as in System F and System FC. + New modules only, and the modules of Stage 1 for syntax, conversion and normalisation are written again for the new language. +| High. About 1500 lines of Stage 1 have a second version with one more former, with `DefEq t u ↔ nf t ≡ nf u` proved again. Stages 2 to 8 do not apply to the new language until each is ported. + +| D1-c +| The former `∀` is added to `Wager.L1.Syntax`. Each module of stages 1 to 8 that matches on a type changes. +| High, and it breaks the rule "the checked modules do not change". `VERDICT.adoc` is final for 79 modules. +|=== + +=== D2: the scope, after finding F25 + +[cols="1,4,3",options="header"] +|=== +| Option | Text | Cost and risk + +| D2-a (recommended) +| The quantifier, and an identity type with 2 type arguments at the level of schemes (possible with D1-a without a change of Stage 1). The GADT program of Stage 6 is then 1 term with 1 type `∀ a. G a → a`, with the equality `a ~ Int` as a type in a context with the variable a. +| Moderate. It answers the example of the task of Stage 6 (F17, F24). The class of the identity type stays the decision of the owner (R23, R24). + +| D2-b +| The quantifier only. The 2 limits of Stage 8 stay. +| Low. The quantifier then has few programs to show: the GADT program and the polymorphic unwrap stay out of reach. + +| D2-c (the most complete long-term form) +| D2-a, and trope operations with type parameters, so that the unwrap of a newtype at a type variable is 1 term. +| High, with an open question. For the row scheme the state of `N τ` depends on τ (DC-8.5), so a parameter of the operation is not enough. The work can end with a checked limit for the row scheme and a positive result for the two-state scheme. +|=== + +=== D3: evaluation and erasure + +[cols="1,4,3",options="header"] +|=== +| Option | Text | Cost and risk + +| D3-a (recommended) +| Type abstraction and type application are erased: the erased term has no trace of them. The results about behaviour are statements about the erased term, by the logical relation. The calculus with the quantifier has no reduction relation, as the extensions of stages 6 and 8 have none. +| Moderate. The erasure of a type abstraction evaluates its body earlier. This is sound because each typed term has a value. The fundamental lemma proves this fact, so the plan depends on that lemma. + +| D3-b (the most complete long-term form) +| D3-a, and a reduction relation with type abstraction as a value, with progress and preservation (T0 for the quantifier). +| Higher. It needs substitution of terms and of types in the terms of Stage 8, which Stage 8 did not need (DC-8.2). +|=== + +=== D4: a grade on the quantifier + +[cols="1,4,3",options="header"] +|=== +| Option | Text | Cost and risk + +| D4-a (recommended) +| The quantifier has no grade. The role of a type variable stays a property of a type (`T8-Role`, F26). +| None. + +| D4-b (the most complete long-term form) +| The quantifier has the grade of its variable, `∀[g] a. S`, and the rule of type abstraction has a kinding premise at that grade. The typing of a term then checks roles. +| Moderate to high. It makes the kinding judgement (R1) a premise of a typing rule. That is a new use of a judgement, and it needs an entry in the relation ledger. +|=== + +== Stages of the work, for the recommended options + +Each part freezes its statements in a statement module, and the freeze is committed before the proofs. The names of the statements are working names. + +[cols="1,5,4",options="header"] +|=== +| Part | Method | Main risk or decision point + +| 9a: the calculus +| `Wager/Forall`: schemes `Sch Δ`; terms with type abstraction and type application; the typing judgement with the 12 rules of Stage 8 and 2 new rules. + Statements: each typed term of Stage 8 is a typed term at a scheme with no quantifier (`T9-Conservative`); the closure of a typed open term of Stage 8 by type abstractions has the closed scheme `∀ Δ. A` (`T9-Generalise`); the application of that closure to the types of a substitution σ and the instance `inst σ t` of Stage 8 have one erasure (`T9-Instantiate`); instantiation keeps typing (`T9-Inst`). +| The 2 new rules are the first new typing rules since `t-cast`. They are entries of the rule-diff table for the extension, with a count of 2. + The rule of type abstraction weakens each type of the context. This needs renaming of the types of a context. + +| 9b: the logical relation +| The erasure of a term. A relation on untyped values, by recursion on a scheme, with an environment that gives each type variable 2 closed types and a relation between values. The aim: at a type of Stage 1 with no variable it agrees with the relation `𝒱` of Stage 4 (DC-4.6). This is a statement to prove (`T9-Agrees`). + Statements: the fundamental lemma (`T9-Fund`): the erasure of a typed term, in related environments, evaluates to related values. Corollary: the erasure of each closed typed term has a value. +| The universe: the relation at a quantifier ranges over all relations, so it is in `Type₁`. It is defined by recursion on the scheme, so Agda accepts it. + The substitution lemma of the relation (the relation at `S[A]` and the relation at S in an extended environment). The plan states it as a logical equivalence, to avoid a path between relations. + A type of Stage 1 under a relation environment needs the normal form of an open type. If this lemma fails for types with inspection primitives at a type variable, the part reports the lemma that fails. A primitive inspects the head of its argument, and a relation variable has no head: a first fix is to demand the grade nominal for that variable, which is finding F26 again. + +| 9c: free theorems +| Checked examples and 2 statements. Each closed term of the type `∀ a. a → a` erases to a function that is observationally the identity (`T9-Identity`). The closure of the polymorphic coercion of Stage 8 erases to a function that is observationally the identity at each instance (`T9-Coercion`, T3 for a polymorphic coercion). + Rejected examples: a term that is not parametric has no type. +| Low, when 9b holds. + +| 9d: the identity type with type arguments (only with D2-a) +| A scheme former `Id A B` for 2 types in Δ, the literal `rfl`, and the rule of the cast with evidence at the grade `𝟘`, as in Stage 6, part 2. + Statements: the GADT program is 1 typed term at the scheme `∀ a. G a → a` (`T9-Gadt`); the erasure of the proofs in casts is sound (`T9-Erasure`); closed evidence exists exactly for convertible types (`T9-Canonicity`); each closed instance is the program of Stage 6, part 2 (`T9-Gadt-Instance`). +| An open term can have a false assumption. The relation at `Id A B` under a relation environment is the place where this shows. If the fundamental lemma needs a condition on the relation of a variable that occurs in an identity type, the condition is recorded as a change. + The class of the identity type is the decision of the owner. The entries have no class. + +| 9e: records +| Gate watch, examples, DC-9.x, the 2 ledgers, `TOOLCHAIN.adoc`, new sections in `VERDICT.adoc`, the index modules, `PROOF-STATUS.adoc` and the MANIFEST. One draft pull request. +| None. +|=== + +== What Stage 9 does not do, in each option + +* A source calculus with a quantifier, and a theorem as T5 for a polymorphic source program. The source calculus stays the calculus of Stage 3. +* Type-level functions over schemes, and kinds other than the kinds of Stage 1. +* Recursion in terms or in types. +* A change of a result of stages 1 to 8. + +== Rules of work + +The rules of `PLAN.adoc` hold: statements before proofs; the ledgers change with the rules; each theorem has an accepted and a rejected example; the gate is watched to fail; `--cubical --safe`, no `postulate`, no hole, no termination or positivity pragma. +The 91 checked modules of stages 1 to 8 do not change, apart from a new section at the end of each index module. + +A part that cannot be proved as stated stops, and the owner gets the statement, the lemma that fails and the options. A statement does not change in silence. + +== Questions for the owner + +. D1: the scheme layer (D1-a), a second type language (D1-b), or a change of Stage 1 (D1-c)? +. D2: the quantifier with the identity type (D2-a), the quantifier only (D2-b), or also trope operations with type parameters (D2-c)? +. D3: erasure only (D3-a), or also a reduction relation with progress and preservation (D3-b)? +. D4: no grade on the quantifier (D4-a), or a graded quantifier with a kinding premise (D4-b)?