From 380a144614393d78141d0a9bba93fd74abed2cf9 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 17 Feb 2022 18:48:04 -0600 Subject: [PATCH] Well typed programs don't go wrong --- prototyping/FFI/Data/Vector.agda | 3 +- prototyping/Properties/StrictMode.agda | 135 ++----------------------- 2 files changed, 12 insertions(+), 126 deletions(-) diff --git a/prototyping/FFI/Data/Vector.agda b/prototyping/FFI/Data/Vector.agda index 8463769f..9d3e418f 100644 --- a/prototyping/FFI/Data/Vector.agda +++ b/prototyping/FFI/Data/Vector.agda @@ -34,11 +34,12 @@ postulate {-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-} postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0) +postulate lookup-empty : ∀ {A} n → (lookup (empty {A}) n ≡ nothing) postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x) postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x) postulate lookup-snoc-not : ∀ {A n} (x : A) (v : Vector A) → (n ≢ length v) → (lookup v n ≡ lookup (snoc v x) n) -{-# REWRITE length-empty lookup-snoc lookup-snoc-empty #-} +{-# REWRITE length-empty lookup-snoc lookup-snoc-empty lookup-empty #-} head : ∀ {A} → (Vector A) → (Maybe A) head vec with null vec diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 13e03731..d7e0b2e5 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -5,7 +5,7 @@ module Properties.StrictMode where import Agda.Builtin.Equality.Rewrite open import Agda.Builtin.Equality using (_≡_; refl) open import FFI.Data.Maybe using (Maybe; just; nothing) -open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ) +open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ) open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; block; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; addr) open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_) open import Luau.Syntax using (Expr; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg) @@ -21,7 +21,7 @@ open import Properties.Equality using (_≢_; sym; cong; trans; subst₁) open import Properties.Dec using (Dec; yes; no) open import Properties.Contradiction using (CONTRADICTION) open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ) -open import Luau.OpSem using (_⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst) +open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app; function; beta; return; block; done; local; subst; refl; step) open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; NilIsNotAFunction; UnboundVariable; SEGV; app; block; local; return) src = Luau.Type.src strict @@ -249,6 +249,10 @@ reflectᴴᴮ (return s) (heap W′) with reflectᴴᴱ s (heap W′) reflectᴴᴮ (return s) (heap W′) | heap W = heap W reflectᴴᴮ (return s) (heap W′) | expr W = block (return W) +reflect* : ∀ {H H′ B B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B) +reflect* refl W = W +reflect* (step s t) W = reflectᴴᴮ s (reflect* t W) + bot-not-obj : ∀ O → bot ≢ typeOfᴼ O bot-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) () @@ -267,126 +271,7 @@ runtimeWarningᴱ (block b err) = block b (runtimeWarningᴮ err) runtimeWarningᴮ (local (var x ∈ T) err) = local₁ (runtimeWarningᴱ err) runtimeWarningᴮ (return err) = return (runtimeWarningᴱ err) - - - - --- reflectᴱ (function {F = f ⟨ var x ∈ S ⟩∈ T} defn) (bot ()) --- reflectᴱ (function defn) (addr a T q) = CONTRADICTION (q refl) --- reflectᴱ (app s) (bot x) = {!x!} --- reflectᴱ (app s) (app₁ W) = app₁ {!reflectᴱ s W!} --- reflectᴱ (app s) (app₂ W) = {!!} --- reflectᴱ (beta x) W = {!!} --- reflectᴱ (block x) W = {!!} --- reflectᴱ (return x) W = {!!} --- reflectᴱ done W = {!!} - --- heap-miss : ∀ {Σ HV T} → (Σ ▷ HV ∈ T) → (HV ≡ nothing) → (T ≡ bot) --- heap-miss nothing refl = refl - --- data ProgressResultᴱ {Σ Γ S M T Δ} (H : Heap yes) (D : Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) : Set --- data ProgressResultᴮ {Σ Γ S B T Δ} (H : Heap yes) (D : Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) : Set - --- data ProgressResultᴱ {Σ Γ S M T Δ} H D where - --- value : ∀ V → (M ≡ val V) → ProgressResultᴱ H D --- warning : (Warningᴱ Σ D) → ProgressResultᴱ H D --- step : ∀ {M′ H′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → ProgressResultᴱ H D - --- data ProgressResultᴮ {Σ Γ S B T Δ} H D where - --- done : (B ≡ done) → ProgressResultᴮ H D --- return : ∀ V {C} → (B ≡ (return (val V) ∙ C)) → ProgressResultᴮ H D --- warning : (Warningᴮ Σ D) → ProgressResultᴮ H D --- step : ∀ {B′ H′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → ProgressResultᴮ H D - --- progressᴱ : ∀ {Σ Γ S M T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴱ H D --- progressᴮ : ∀ {Σ Γ S B T Δ} H → (Σ ▷ H ✓) → (D : Σ ▷ Γ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) → (Γ ≡ ∅) → ProgressResultᴮ H D - --- progressᴱ H h nil _ = value nil refl --- progressᴱ H h (var x p) refl = warning (bot p) --- progressᴱ H h (addr a refl) _ = value (addr a) refl --- progressᴱ H h (app D₁ D₂) p with progressᴱ H h D₁ p --- progressᴱ H h (app nil D₂) p | value nil refl = warning (bot refl) --- progressᴱ H h (app (var _ _) D₂) p | value nil () --- progressᴱ H h (app (app _ _) D₂) p | value nil () --- progressᴱ H h (app (function _) D₂) p | value nil () --- progressᴱ H h (app (block _ _) D₂) p | value nil () --- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl with remember(H [ a ]ᴴ) --- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (nothing , r) = warning (bot (cong tgt (heap-miss (h a) r))) --- progressᴱ H h (app (addr _ refl) D₂) p | value (addr a) refl | (just(function f ⟨ var x ∈ S ⟩∈ T is B end) , r) = step (beta r) --- progressᴱ H h (app D₁ D₂) p | warning W = warning (app₁ W) --- progressᴱ H h (app D₁ D₂) p | step S = step (app S) --- progressᴱ H h (function D) _ with alloc H _ --- progressᴱ H h (function D) _ | ok a H′ r = step (function r) --- progressᴱ H h (block b D) q with progressᴮ H h D q --- progressᴱ H h (block b D) q | done refl = step done --- progressᴱ H h (block b D) q | return V refl = step (return refl) --- progressᴱ H h (block b D) q | warning W = warning (block b W) --- progressᴱ H h (block b D) q | step S = step (block S) - --- progressᴮ H h done q = done refl --- progressᴮ H h (return D₁ D₂) q with progressᴱ H h D₁ q --- progressᴮ H h (return D₁ D₂) q | value V refl = return V refl --- progressᴮ H h (return D₁ D₂) q | warning W = warning (return W) --- progressᴮ H h (return D₁ D₂) q | step S = step (return S) --- progressᴮ H h (local D₁ D₂) q with progressᴱ H h D₁ q --- progressᴮ H h (local D₁ D₂) q | value V refl = step subst --- progressᴮ H h (local D₁ D₂) q | warning W = warning (local₁ W) --- progressᴮ H h (local D₁ D₂) q | step S = step (local S) --- progressᴮ H h (function D₁ D₂) q with alloc H _ --- progressᴮ H h (function D₁ D₂) q | ok a H′ r = step (function r) - --- data LookupResult {Σ V S} (D : Σ ▷ V ∈ S) : Set where - --- function : ∀ f {x B T U W} → --- (S ≡ (T ⇒ U)) → --- (V ≡ just(function f ⟨ var x ∈ T ⟩∈ U is B end)) → --- (Σ ▷ (x ↦ T) ⊢ᴮ U ∋ B ∈ U ⊣ (x ↦ W)) → --- LookupResult D - --- warningᴴ : --- Warningᴴ(D) → --- LookupResult D - --- lookup : ∀ {Σ V T} (D : Σ ▷ V ∈ T) → LookupResult D --- lookup nothing = warningᴴ nothing --- lookup (function f {U = U} {V = V} D) with U ≡ᵀ V --- lookup (function f D) | yes refl = function f refl refl D --- lookup (function f D) | no p = warningᴴ (function f (disagree p)) - --- data PreservationResultᴮ {Σ S Δ T H B} (D : ∅ ⊢ᴮ S ∋ B ∈ T ⊣ Δ) M′ H′ : Set where - --- ok : ∀ {Δ′} → (∅ ⊢ᴮ S ∋ M′ ∈ T ⊣ Δ′) → PreservationResultᴮ D M′ H′ --- warning : Warningᴮ Σ D → PreservationResultᴮ D M′ H′ - --- data PreservationResultᴱ {Σ S Δ T M} (D : ∅ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) M′ : Set where - --- ok : ∀ {Δ′} → (∅ ⊢ᴱ S ∋ M′ ∈ T ⊣ Δ′) → PreservationResultᴱ D M′ H′ --- warning : Warningᴱ Σ D → PreservationResultᴱ D M′ H′ - --- preservationᴱ : ∀ {Σ S Δ T H H′ M M′} → (D : ∅ ⊢ᴱ S ∋ M ∈ T ⊣ Δ) → (s : H ⊢ M ⟶ᴱ M′ ⊣ H′) → PreservationResultᴱ D M′ H′ --- preservationᴱ {S = S} {T = T} h D s with S ≡ᵀ T --- preservationᴱ h D s | no p = warning (disagree p) --- preservationᴱ h (app D₁ D₂) (app s) | yes refl with preservationᴱ h D₁ s --- preservationᴱ h (app D₁ D₂) (app s) | yes refl | ok h′ D₁′ = ok h′ (app D₁′ {!D₂!}) --- preservationᴱ h (app D₁ D₂) (app s) | yes refl | warning W = warning (app₁ W) --- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl with lookup (h a) --- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | function f r₁ r₂ D₁ with trans p r₁ | trans (sym q) r₂ --- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | function f r₁ r₂ D₁ | refl | refl = ok h (block f (local D₂ D₁)) --- -- preservationᴱ h (app (addr a p) D₂) (beta q) | yes refl | warningᴴ W = warningᴴ a W - --- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) with subst₂ (λ X Y → _ ▷ X ∈ Y) q (sym p) (h a) --- -- preservationᴱ {S = S} h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} {V = V′} D with S ≡ᵀ U′ | U′ ≡ᵀ V′ --- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} {V = V′} D | yes refl | yes refl = ok h (block _ (local D₂ D)) --- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} D | no r | _ = warningᴱ (disagree r) --- -- preservationᴱ h (app {T = T} {U = U} (addr a p) D₂) (beta q) | function f {T = T′} {U = U′} D | yes refl | no r = warningᴴ a {!function f (disagree r)!} -- (subst₁ Warningᴴ {!!} {!(function f (disagree r))!}) -- (function f (disagree r)) - --- -- with src T ≡ᵀ U -- = ok h (block f (local {!D₂!} {!!})) --- -- preservationᴱ h (app {T = T} {U = U} D₁ D₂) (beta {F = f ⟨ var x ∈ _ ⟩∈ R} p) | yes refl = ok h (block f (local D₂ {!!})) -- with src T ≡ᵀ S -- = ok h (block f (local {!D₂!} {!!})) --- -- preservationᴱ h (app {T = T} {U = U} D₁ D₂) (beta {F = f ⟨ var x ∈ S ⟩∈ R} p) | no q = warning (app₀ {!q!}) -- with src T ≡ᵀ S -- = ok h (block f (local {!D₂!} {!!})) --- preservationᴱ h D s | yes refl = {!!} --- preservationᴱ h (function D) (function p) = {!x!} --- preservationᴱ h (block b D) (block s) = {!!} --- preservationᴱ h (block b D) (return p) = {!x!} --- preservationᴱ h (block b D) done = {!!} +wellTypedProgramsDontGoWrong : ∀ {H′ B B′} → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B) +wellTypedProgramsDontGoWrong t err with reflect* t (block (runtimeWarningᴮ err)) +wellTypedProgramsDontGoWrong t err | heap (addr a refl ()) +wellTypedProgramsDontGoWrong t err | block W = W