From dd97e0a58b377161fb8e9ab7b5524f63b875612c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 19 Mar 2022 17:26:39 +0000 Subject: Add definition of Hoare logic semantics. --- src/Helium/Data/Pseudocode/Manipulate.agda | 1554 +++++++++++++++++++++++++ src/Helium/Data/Pseudocode/Properties.agda | 109 ++ src/Helium/Semantics/Axiomatic/Assertion.agda | 173 +++ src/Helium/Semantics/Axiomatic/Core.agda | 85 ++ src/Helium/Semantics/Axiomatic/Term.agda | 385 ++++++ src/Helium/Semantics/Axiomatic/Triple.agda | 46 + 6 files changed, 2352 insertions(+) create mode 100644 src/Helium/Data/Pseudocode/Manipulate.agda create mode 100644 src/Helium/Data/Pseudocode/Properties.agda create mode 100644 src/Helium/Semantics/Axiomatic/Assertion.agda create mode 100644 src/Helium/Semantics/Axiomatic/Core.agda create mode 100644 src/Helium/Semantics/Axiomatic/Term.agda create mode 100644 src/Helium/Semantics/Axiomatic/Triple.agda (limited to 'src') diff --git a/src/Helium/Data/Pseudocode/Manipulate.agda b/src/Helium/Data/Pseudocode/Manipulate.agda new file mode 100644 index 0000000..a798ad8 --- /dev/null +++ b/src/Helium/Data/Pseudocode/Manipulate.agda @@ -0,0 +1,1554 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Ways to modify pseudocode statements and expressions. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Data.Vec using (Vec) +open import Helium.Data.Pseudocode.Core + +module Helium.Data.Pseudocode.Manipulate + {o} {Σ : Vec Type o} + where + +import Algebra.Solver.IdempotentCommutativeMonoid as ComMonoidSolver +open import Data.Fin as Fin using (Fin; suc) +open import Data.Fin.Patterns +open import Data.Nat as ℕ using (ℕ; suc; _⊔_) +import Data.Nat.Induction as ℕᵢ +import Data.Nat.Properties as ℕₚ +open import Data.Nat.Solver using (module +-*-Solver) +open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; <_,_>) +open import Data.Sum using (_⊎_; inj₁; inj₂) +import Data.Product.Relation.Binary.Lex.Strict as Lex +open import Data.Vec as Vec using ([]; _∷_) +import Data.Vec.Properties as Vecₚ +open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) +open import Data.Vec.Relation.Unary.Any using (Any; here; there) +open import Function using (_on_; _∘_; _∋_; case_return_of_) +open import Function.Nary.NonDependent using (congₙ) +open import Helium.Data.Pseudocode.Properties +import Induction.WellFounded as Wf +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning) +open import Relation.Nullary using (yes; no; ¬_) +open import Relation.Nullary.Decidable.Core using (True; fromWitness; toWitness; toWitnessFalse) +open import Relation.Nullary.Negation using (contradiction) + +open ComMonoidSolver (record + { isIdempotentCommutativeMonoid = record + { isCommutativeMonoid = ℕₚ.⊔-0-isCommutativeMonoid + ; idem = ℕₚ.⊔-idem + } + }) + using (_⊕_; _⊜_) + renaming (solve to ⊔-solve) + +open Code Σ + +private + variable + m n : ℕ + Γ Δ : Vec Type m + t t′ ret : Type + +-- TODO: make argument irrelevant +castType : Expression Γ t → (t ≡ t′) → Expression Γ t′ +castType e refl = e + +cast-pres-assignable : ∀ {e : Expression Γ t} → CanAssign e → (eq : t ≡ t′) → CanAssign (castType e eq) +cast-pres-assignable e refl = e + +cast-pres-stateless : ∀ {e : Expression Γ t} → (eq : t ≡ t′) → ReferencesState (castType e eq) → ReferencesState e +cast-pres-stateless refl e = e + +punchOut⇒insert : ∀ {a} {A : Set a} (xs : Vec A n) {i j : Fin (suc n)} (i≢j : ¬ i ≡ j) x → Vec.lookup xs (Fin.punchOut i≢j) ≡ Vec.lookup (Vec.insert xs i x) j +punchOut⇒insert xs {i} {j} i≢j x = begin + Vec.lookup xs (Fin.punchOut i≢j) + ≡˘⟨ cong (λ x → Vec.lookup x _) (Vecₚ.remove-insert xs i x) ⟩ + Vec.lookup (Vec.remove (Vec.insert xs i x) i) (Fin.punchOut i≢j) + ≡⟨ Vecₚ.remove-punchOut (Vec.insert xs i x) i≢j ⟩ + Vec.lookup (Vec.insert xs i x) j + ∎ + where open ≡-Reasoning + +elimAt : ∀ i → Expression (Vec.insert Γ i t′) t → Expression Γ t′ → Expression Γ t +elimAt′ : ∀ i → All (Expression (Vec.insert Γ i t′)) Δ → Expression Γ t′ → All (Expression Γ) Δ + +elimAt i (lit x) e′ = lit x +elimAt i (state j) e′ = state j +elimAt i (var j) e′ with i Fin.≟ j +... | yes refl = castType e′ (sym (Vecₚ.insert-lookup _ i _)) +... | no i≢j = castType (var (Fin.punchOut i≢j)) (punchOut⇒insert _ i≢j _) +elimAt i (abort e) e′ = abort (elimAt i e e′) +elimAt i (_≟_ {hasEquality = hasEq} e e₁) e′ = _≟_ {hasEquality = hasEq} (elimAt i e e′) (elimAt i e₁ e′) +elimAt i (_> x) e′ = elimAt i e e′ >> x +elimAt i (rnd e) e′ = rnd (elimAt i e e′) +elimAt i (fin x e) e′ = fin x (elimAt i e e′) +elimAt i (asInt e) e′ = asInt (elimAt i e e′) +elimAt i nil e′ = nil +elimAt i (cons e e₁) e′ = cons (elimAt i e e′) (elimAt i e₁ e′) +elimAt i (head e) e′ = head (elimAt i e e′) +elimAt i (tail e) e′ = tail (elimAt i e e′) +elimAt i (call f es) e′ = call f (elimAt′ i es e′) +elimAt i (if e then e₁ else e₂) e′ = if elimAt i e e′ then elimAt i e₁ e′ else elimAt i e₂ e′ + +elimAt′ i [] e′ = [] +elimAt′ i (e ∷ es) e′ = elimAt i e e′ ∷ elimAt′ i es e′ + +wknAt : ∀ i → Expression Γ t → Expression (Vec.insert Γ i t′) t +wknAt′ : ∀ i → All (Expression Γ) Δ → All (Expression (Vec.insert Γ i t′)) Δ + +wknAt i (lit x) = lit x +wknAt i (state j) = state j +wknAt i (var j) = castType (var (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j) +wknAt i (abort e) = abort (wknAt i e) +wknAt i (_≟_ {hasEquality = hasEq} e e₁) = _≟_ {hasEquality = hasEq} (wknAt i e) (wknAt i e₁) +wknAt i (_> x) = wknAt i e >> x +wknAt i (rnd e) = rnd (wknAt i e) +wknAt i (fin x e) = fin x (wknAt i e) +wknAt i (asInt e) = asInt (wknAt i e) +wknAt i nil = nil +wknAt i (cons e e₁) = cons (wknAt i e) (wknAt i e₁) +wknAt i (head e) = head (wknAt i e) +wknAt i (tail e) = tail (wknAt i e) +wknAt i (call f es) = call f (wknAt′ i es) +wknAt i (if e then e₁ else e₂) = if wknAt i e then wknAt i e₁ else wknAt i e₂ + +wknAt′ i [] = [] +wknAt′ i (e ∷ es) = wknAt i e ∷ wknAt′ i es + +substAt : ∀ i → Expression Γ t → Expression Γ (Vec.lookup Γ i) → Expression Γ t +substAt′ : ∀ i → All (Expression Γ) Δ → Expression Γ (Vec.lookup Γ i) → All (Expression Γ) Δ +substAt i (lit x) e′ = lit x +substAt i (state j) e′ = state j +substAt i (var j) e′ with i Fin.≟ j +... | yes refl = e′ +... | no _ = var j +substAt i (abort e) e′ = abort (substAt i e e′) +substAt i (_≟_ {hasEquality = hasEq} e e₁) e′ = _≟_ {hasEquality = hasEq} (substAt i e e′) (substAt i e₁ e′) +substAt i (_> x) e′ = substAt i e e′ >> x +substAt i (rnd e) e′ = rnd (substAt i e e′) +substAt i (fin x e) e′ = fin x (substAt i e e′) +substAt i (asInt e) e′ = asInt (substAt i e e′) +substAt i nil e′ = nil +substAt i (cons e e₁) e′ = cons (substAt i e e′) (substAt i e₁ e′) +substAt i (head e) e′ = head (substAt i e e′) +substAt i (tail e) e′ = tail (substAt i e e′) +substAt i (call f es) e′ = call f (substAt′ i es e′) +substAt i (if e then e₁ else e₂) e′ = if substAt i e e′ then substAt i e₁ e′ else substAt i e₂ e′ + +substAt′ i [] e′ = [] +substAt′ i (e ∷ es) e′ = substAt i e e′ ∷ substAt′ i es e′ + +updateRef : ∀ {e : Expression Γ t} (ref : CanAssign e) → ¬ ReferencesState e → Expression Γ t → Expression Γ t′ → Expression Γ t′ +updateRef (state i) stateless val e = contradiction (state i) stateless +updateRef (var i) stateless val e = substAt i e val +updateRef (abort _) stateless val e = e +updateRef [ ref ] stateless val e = updateRef ref (stateless ∘ [_]) (unbox val) e +updateRef (unbox ref) stateless val e = updateRef ref (stateless ∘ unbox) [ val ] e +updateRef (splice ref ref₁ e₂) stateless val e = updateRef ref₁ (stateless ∘ (λ x → spliceʳ _ x _)) (head (tail (cut val e₂))) (updateRef ref (stateless ∘ (λ x → spliceˡ x _ _)) (head (cut val e₂)) e) +updateRef (cut ref e₁) stateless val e = updateRef ref (stateless ∘ (λ x → cut x _)) (splice (head val) (head (tail val)) e₁) e +updateRef (cast eq ref) stateless val e = updateRef ref (stateless ∘ cast eq) (cast (sym eq) val) e +updateRef nil stateless val e = e +updateRef (cons ref ref₁) stateless val e = updateRef ref₁ (stateless ∘ (λ x → consʳ _ x)) (tail val) (updateRef ref (stateless ∘ (λ x → consˡ x _)) (head val) e) +updateRef (head {e = e′} ref) stateless val e = updateRef ref (stateless ∘ head) (cons val (tail e′)) e +updateRef (tail {e = e′} ref) stateless val e = updateRef ref (stateless ∘ tail) (cons (head e′) val) e + +wknAt-pres-assignable : ∀ i {e} → CanAssign e → CanAssign (wknAt {Γ = Γ} {t} {t′} i e) +wknAt-pres-assignable i (state j) = state j +wknAt-pres-assignable i (var j) = cast-pres-assignable (var (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j) +wknAt-pres-assignable i (abort e) = abort (wknAt i e) +wknAt-pres-assignable i [ ref ] = [ wknAt-pres-assignable i ref ] +wknAt-pres-assignable i (unbox ref) = unbox (wknAt-pres-assignable i ref) +wknAt-pres-assignable i (splice ref ref₁ e₂) = splice (wknAt-pres-assignable i ref) (wknAt-pres-assignable i ref₁) (wknAt i e₂) +wknAt-pres-assignable i (cut ref e₁) = cut (wknAt-pres-assignable i ref) (wknAt i e₁) +wknAt-pres-assignable i (cast eq ref) = cast eq (wknAt-pres-assignable i ref) +wknAt-pres-assignable i nil = nil +wknAt-pres-assignable i (cons ref ref₁) = cons (wknAt-pres-assignable i ref) (wknAt-pres-assignable i ref₁) +wknAt-pres-assignable i (head ref) = head (wknAt-pres-assignable i ref) +wknAt-pres-assignable i (tail ref) = tail (wknAt-pres-assignable i ref) + +wknAt-pres-stateless : ∀ i {e} → ReferencesState (wknAt {Γ = Γ} {t} {t′} i e) → ReferencesState e +wknAt-pres-stateless i {state _} (state j) = state j +wknAt-pres-stateless i {var j} e = contradiction (cast-pres-stateless {e = var (Fin.punchIn i j)} (Vecₚ.insert-punchIn _ i _ j) e) (λ ()) +wknAt-pres-stateless i {[ _ ]} [ e ] = [ wknAt-pres-stateless i e ] +wknAt-pres-stateless i {unbox _} (unbox e) = unbox (wknAt-pres-stateless i e) +wknAt-pres-stateless i {splice _ _ _} (spliceˡ e e₁ e₂) = spliceˡ (wknAt-pres-stateless i e) _ _ +wknAt-pres-stateless i {splice _ _ _} (spliceʳ e e₁ e₂) = spliceʳ _ (wknAt-pres-stateless i e₁) _ +wknAt-pres-stateless i {cut _ _} (cut e e₁) = cut (wknAt-pres-stateless i e) _ +wknAt-pres-stateless i {cast _ _} (cast eq e) = cast eq (wknAt-pres-stateless i e) +wknAt-pres-stateless i {cons _ _} (consˡ e e₁) = consˡ (wknAt-pres-stateless i e) _ +wknAt-pres-stateless i {cons _ _} (consʳ e e₁) = consʳ _ (wknAt-pres-stateless i e₁) +wknAt-pres-stateless i {head _} (head e) = head (wknAt-pres-stateless i e) +wknAt-pres-stateless i {tail _} (tail e) = tail (wknAt-pres-stateless i e) + +wknStatementAt : ∀ t i → Statement Γ → Statement (Vec.insert Γ i t) +wknStatementAt t i (s ∙ s₁) = wknStatementAt t i s ∙ wknStatementAt t i s₁ +wknStatementAt t i skip = skip +wknStatementAt t i (_≔_ ref {assignable} x) = _≔_ (wknAt i ref) {fromWitness (wknAt-pres-assignable i (toWitness assignable))} (wknAt i x) +wknStatementAt t i (declare x s) = declare (wknAt i x) (wknStatementAt t (suc i) s) +wknStatementAt t i (invoke p es) = invoke p (wknAt′ i es) +wknStatementAt t i (if x then s) = if wknAt i x then wknStatementAt t i s +wknStatementAt t i (if x then s else s₁) = if wknAt i x then wknStatementAt t i s else wknStatementAt t i s₁ +wknStatementAt t i (for m s) = for m (wknStatementAt t (suc i) s) + +subst : Expression Γ t → All (Expression Δ) Γ → Expression Δ t +subst′ : ∀ {n ts} → All (Expression Γ) {n} ts → All (Expression Δ) Γ → All (Expression Δ) ts + +subst (lit x) xs = lit x +subst (state i) xs = state i +subst (var i) xs = All.lookup i xs +subst (abort e) xs = abort (subst e xs) +subst (_≟_ {hasEquality = hasEq} e e₁) xs = _≟_ {hasEquality = hasEq} (subst e xs) (subst e₁ xs) +subst (_> x) xs = subst e xs >> x +subst (rnd e) xs = rnd (subst e xs) +subst (fin x e) xs = fin x (subst e xs) +subst (asInt e) xs = asInt (subst e xs) +subst nil xs = nil +subst (cons e e₁) xs = cons (subst e xs) (subst e₁ xs) +subst (head e) xs = head (subst e xs) +subst (tail e) xs = tail (subst e xs) +subst (call f es) xs = call f (subst′ es xs) +subst (if e then e₁ else e₂) xs = if subst e xs then subst e₁ xs else subst e₂ xs + +subst′ [] xs = [] +subst′ (e ∷ es) xs = subst e xs ∷ subst′ es xs + +callDepth : Expression Γ t → ℕ +callDepth′ : All (Expression Γ) Δ → ℕ +stmtCallDepth : Statement Γ → ℕ +funCallDepth : Function Γ ret → ℕ +procCallDepth : Procedure Γ → ℕ + +callDepth (lit x) = 0 +callDepth (state i) = 0 +callDepth (var i) = 0 +callDepth (abort e) = callDepth e +callDepth (e ≟ e₁) = callDepth e ⊔ callDepth e₁ +callDepth (e > x) = callDepth e +callDepth (rnd e) = callDepth e +callDepth (fin x e) = callDepth e +callDepth (asInt e) = callDepth e +callDepth nil = 0 +callDepth (cons e e₁) = callDepth e ⊔ callDepth e₁ +callDepth (head e) = callDepth e +callDepth (tail e) = callDepth e +callDepth (call f es) = suc (funCallDepth f) ⊔ callDepth′ es +callDepth (if e then e₁ else e₂) = callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂ + +callDepth′ [] = 0 +callDepth′ (e ∷ es) = callDepth e ⊔ callDepth′ es + +stmtCallDepth (s ∙ s₁) = stmtCallDepth s ⊔ stmtCallDepth s₁ +stmtCallDepth skip = 0 +stmtCallDepth (ref ≔ x) = callDepth ref ⊔ callDepth x +stmtCallDepth (declare x s) = callDepth x ⊔ stmtCallDepth s +stmtCallDepth (invoke p es) = procCallDepth p ⊔ callDepth′ es +stmtCallDepth (if x then s) = callDepth x ⊔ stmtCallDepth s +stmtCallDepth (if x then s else s₁) = callDepth x ⊔ stmtCallDepth s ⊔ stmtCallDepth s₁ +stmtCallDepth (for m s) = stmtCallDepth s + +funCallDepth (s ∙return x) = stmtCallDepth s ⊔ callDepth x +funCallDepth (declare x f) = funCallDepth f ⊔ callDepth x + +procCallDepth (x ∙end) = stmtCallDepth x + +open ℕₚ.≤-Reasoning + +castType-pres-callDepth : ∀ (e : Expression Γ t) (eq : t ≡ t′) → callDepth (castType e eq) ≡ callDepth e +castType-pres-callDepth e refl = refl + +elimAt-pres-callDepth : ∀ i (e : Expression (Vec.insert Γ i t′) t) (e′ : Expression Γ t′) → callDepth (elimAt i e e′) ℕ.≤ callDepth e′ ⊔ callDepth e +elimAt′-pres-callDepth : ∀ i (es : All (Expression (Vec.insert Γ i t′)) Δ) (e′ : Expression Γ t′) → callDepth′ (elimAt′ i es e′) ℕ.≤ callDepth e′ ⊔ callDepth′ es + +elimAt-pres-callDepth i (lit x) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +elimAt-pres-callDepth i (state j) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +elimAt-pres-callDepth i (var j) e′ with i Fin.≟ j +... | yes refl = begin + callDepth (castType e′ (sym (Vecₚ.insert-lookup _ i _))) + ≡⟨ castType-pres-callDepth e′ (sym (Vecₚ.insert-lookup _ i _)) ⟩ + callDepth e′ + ≤⟨ ℕₚ.m≤m⊔n (callDepth e′) 0 ⟩ + callDepth e′ ⊔ 0 + ∎ +elimAt-pres-callDepth {Γ = Γ} i (var j) e′ | no i≢j = begin + callDepth (castType (var {Γ = Γ} (Fin.punchOut i≢j)) (punchOut⇒insert Γ i≢j _)) + ≡⟨ castType-pres-callDepth (var {Γ = Γ} (Fin.punchOut i≢j)) (punchOut⇒insert Γ i≢j _) ⟩ + 0 + ≤⟨ ℕ.z≤n ⟩ + callDepth e′ ⊔ 0 + ∎ +elimAt-pres-callDepth i (abort e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (e ≟ e₁) e′ = begin + callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) + ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁) + ∎ +elimAt-pres-callDepth i (e > x) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (rnd e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (fin x e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (asInt e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i nil e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +elimAt-pres-callDepth i (cons e e₁) e′ = begin + callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) + ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁) + ∎ +elimAt-pres-callDepth i (head e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (tail e) e′ = elimAt-pres-callDepth i e e′ +elimAt-pres-callDepth i (call f es) e′ = begin + suc (funCallDepth f) ⊔ callDepth′ (elimAt′ i es e′) + ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (elimAt′-pres-callDepth i es e′) ⟩ + suc (funCallDepth f) ⊔ (callDepth e′ ⊔ callDepth′ es) + ≡⟨ ⊔-solve 3 (λ a b c → b ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (suc (funCallDepth f)) (callDepth′ es) ⟩ + callDepth e′ ⊔ (suc (funCallDepth f) ⊔ callDepth′ es) + ∎ +elimAt-pres-callDepth i (if e then e₁ else e₂) e′ = begin + callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′) ⊔ callDepth (elimAt i e₂ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′)) (elimAt-pres-callDepth i e₂ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂) + ≡⟨ ⊔-solve 4 (λ m n o p → (((m ⊕ n) ⊕ (m ⊕ o)) ⊕ (m ⊕ p)) ⊜ (m ⊕ ((n ⊕ o) ⊕ p))) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂) + ∎ + +elimAt′-pres-callDepth i [] e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +elimAt′-pres-callDepth i (e ∷ es) e′ = begin + callDepth (elimAt i e e′) ⊔ callDepth′ (elimAt′ i es e′) + ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt′-pres-callDepth i es e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth′ es) + ≡⟨ ⊔-solve 3 (λ a b c → ((a ⊕ b) ⊕ (a ⊕ c)) ⊜ (a ⊕ (b ⊕ c))) refl (callDepth e′) (callDepth e) (callDepth′ es) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth′ es) + ∎ + +wknAt-pres-callDepth : ∀ i (e : Expression Γ t) → callDepth (wknAt {t′ = t′} i e) ≡ callDepth e +wknAt′-pres-callDepth : ∀ i (es : All (Expression Γ) Δ) → callDepth′ (wknAt′ {t′ = t′} i es) ≡ callDepth′ es + +wknAt-pres-callDepth i (Code.lit x) = refl +wknAt-pres-callDepth i (Code.state j) = refl +wknAt-pres-callDepth {Γ = Γ} i (Code.var j) = castType-pres-callDepth (var {Γ = Vec.insert Γ i _} (Fin.punchIn i j)) (Vecₚ.insert-punchIn Γ i _ j) +wknAt-pres-callDepth i (Code.abort e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (e Code.≟ e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁) +wknAt-pres-callDepth i (e Code.> x) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (Code.rnd e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (Code.fin x e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (Code.asInt e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i Code.nil = refl +wknAt-pres-callDepth i (Code.cons e e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁) +wknAt-pres-callDepth i (Code.head e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (Code.tail e) = wknAt-pres-callDepth i e +wknAt-pres-callDepth i (Code.call f es) = cong (suc (funCallDepth f) ⊔_) (wknAt′-pres-callDepth i es) +wknAt-pres-callDepth i (Code.if e then e₁ else e₂) = congₙ 3 (λ m n o → m ⊔ n ⊔ o) (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁) (wknAt-pres-callDepth i e₂) + +wknAt′-pres-callDepth i [] = refl +wknAt′-pres-callDepth i (e ∷ es) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt′-pres-callDepth i es) + +substAt-pres-callDepth : ∀ i (e : Expression Γ t) e′ → callDepth (substAt i e e′) ℕ.≤ callDepth e′ ⊔ callDepth e +substAt-pres-callDepth i (Code.lit x) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +substAt-pres-callDepth i (Code.state j) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +substAt-pres-callDepth i (Code.var j) e′ with i Fin.≟ j +... | yes refl = ℕₚ.m≤m⊔n (callDepth e′) 0 +... | no _ = ℕₚ.m≤n⊔m (callDepth e′) 0 +substAt-pres-callDepth i (Code.abort e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (e Code.≟ e₁) e′ = begin + callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁) + ∎ +substAt-pres-callDepth i (e Code.> x) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (Code.rnd e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (Code.fin x e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (Code.asInt e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i Code.nil e′ = ℕₚ.m≤n⊔m (callDepth e′) 0 +substAt-pres-callDepth i (Code.cons e e₁) e′ = begin + callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁) + ∎ +substAt-pres-callDepth i (Code.head e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (Code.tail e) e′ = substAt-pres-callDepth i e e′ +substAt-pres-callDepth i (Code.call f es) e′ = begin + suc (funCallDepth f) ⊔ callDepth′ (substAt′ i es e′) + ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (helper es) ⟩ + suc (funCallDepth f) ⊔ (callDepth e′ ⊔ callDepth′ es) + ≡⟨ ⊔-solve 3 (λ a b c → b ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (suc (funCallDepth f)) (callDepth′ es) ⟩ + callDepth e′ ⊔ (suc (funCallDepth f) ⊔ callDepth′ es) + ∎ + where + helper : ∀ {n ts} (es : All _ {n} ts) → callDepth′ (substAt′ i es e′) ℕ.≤ callDepth e′ ⊔ callDepth′ es + helper [] = ℕₚ.m≤n⊔m (callDepth e′) 0 + helper (e ∷ es) = begin + callDepth (substAt i e e′) ⊔ callDepth′ (substAt′ i es e′) + ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (helper es) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth′ es) + ≡⟨ ⊔-solve 3 (λ a b c → ((a ⊕ b) ⊕ (a ⊕ c)) ⊜ (a ⊕ (b ⊕ c))) refl (callDepth e′) (callDepth e) (callDepth′ es) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth′ es) + ∎ +substAt-pres-callDepth i (Code.if e then e₁ else e₂) e′ = begin + callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′) ⊔ callDepth (substAt i e₂ e′) + ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′)) (substAt-pres-callDepth i e₂ e′) ⟩ + callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂) + ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ b) ⊕ (a ⊕ c)) ⊕ (a ⊕ d) ⊜ a ⊕ ((b ⊕ c) ⊕ d)) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩ + callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂) + ∎ + +updateRef-pres-callDepth : ∀ {e : Expression Γ t} ref stateless val (e′ : Expression Γ t′) → + callDepth (updateRef {e = e} ref stateless val e′) ℕ.≤ callDepth e ⊔ callDepth val ⊔ callDepth e′ +updateRef-pres-callDepth (state i) stateless val e′ = contradiction (state i) stateless +updateRef-pres-callDepth (var i) stateless val e′ = substAt-pres-callDepth i e′ val +updateRef-pres-callDepth (abort e) stateless val e′ = ℕₚ.m≤n⊔m (callDepth e ⊔ callDepth val) (callDepth e′) +updateRef-pres-callDepth [ ref ] stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ [_]) (unbox val) e′ +updateRef-pres-callDepth (unbox ref) stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ unbox) [ val ] e′ +updateRef-pres-callDepth (splice {e₁ = e₁} {e₂ = e₂} ref ref₁ e₃) stateless val e′ = begin + callDepth outer + ≤⟨ updateRef-pres-callDepth ref₁ (stateless ∘ (λ x → spliceʳ _ x e₃)) (head (tail (cut val e₃))) inner ⟩ + callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ callDepth inner + ≤⟨ ℕₚ.⊔-monoʳ-≤ (callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃)) (updateRef-pres-callDepth ref (stateless ∘ (λ x → spliceˡ x _ e₃)) (head (cut val e₃)) e′) ⟩ + callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ (callDepth e₁ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ callDepth e′) + ≡⟨ ⊔-solve 5 (λ a b c d e → ((b ⊕ (d ⊕ c)) ⊕ ((a ⊕ (d ⊕ c)) ⊕ e)) ⊜ ((((a ⊕ b) ⊕ c) ⊕ d) ⊕ e)) refl (callDepth e₁) (callDepth e₂) (callDepth e₃) (callDepth val) (callDepth e′) ⟩ + callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth e₃ ⊔ callDepth val ⊔ callDepth e′ + ∎ + where + inner = updateRef ref (stateless ∘ (λ x → spliceˡ x _ e₃)) (head (cut val e₃)) e′ + outer = updateRef ref₁ (stateless ∘ (λ x → spliceʳ _ x e₃)) (head (tail (cut val e₃))) inner +updateRef-pres-callDepth (cut {e₁ = e₁} ref e₂) stateless val e′ = begin + callDepth (updateRef ref (stateless ∘ (λ x → (cut x e₂))) (splice (head val) (head (tail val)) e₂) e′) + ≤⟨ updateRef-pres-callDepth ref (stateless ∘ (λ x → (cut x e₂))) (splice (head val) (head (tail val)) e₂) e′ ⟩ + callDepth e₁ ⊔ (callDepth val ⊔ callDepth val ⊔ callDepth e₂) ⊔ callDepth e′ + ≡⟨ ⊔-solve 4 (λ a b c d → (a ⊕ ((c ⊕ c) ⊕ b)) ⊕ d ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e₁) (callDepth e₂) (callDepth val) (callDepth e′) ⟩ + callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth val ⊔ callDepth e′ + ∎ +updateRef-pres-callDepth (cast eq ref) stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ cast eq) (cast (sym eq) val) e′ +updateRef-pres-callDepth nil stateless val e′ = ℕₚ.m≤n⊔m (callDepth val) (callDepth e′) +updateRef-pres-callDepth (cons {e₁ = e₁} {e₂ = e₂} ref ref₁) stateless val e′ = begin + callDepth outer + ≤⟨ updateRef-pres-callDepth ref₁ (stateless ∘ consʳ e₁) (tail val) inner ⟩ + callDepth e₂ ⊔ callDepth val ⊔ callDepth inner + ≤⟨ ℕₚ.⊔-monoʳ-≤ (callDepth e₂ ⊔ callDepth val) (updateRef-pres-callDepth ref (stateless ∘ (λ x → consˡ x e₂)) (head val) e′) ⟩ + callDepth e₂ ⊔ callDepth val ⊔ (callDepth e₁ ⊔ callDepth val ⊔ callDepth e′) + ≡⟨ ⊔-solve 4 (λ a b c d → (b ⊕ c) ⊕ ((a ⊕ c) ⊕ d) ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e₁) (callDepth e₂) (callDepth val) (callDepth e′) ⟩ + callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth val ⊔ callDepth e′ + ∎ + where + inner = updateRef ref (stateless ∘ (λ x → consˡ x e₂)) (head val) e′ + outer = updateRef ref₁ (stateless ∘ consʳ e₁) (tail val) inner +updateRef-pres-callDepth (head {e = e} ref) stateless val e′ = begin + callDepth (updateRef ref (stateless ∘ head) (cons val (tail e)) e′) + ≤⟨ updateRef-pres-callDepth ref (stateless ∘ head) (cons val (tail e)) e′ ⟩ + callDepth e ⊔ (callDepth val ⊔ callDepth e) ⊔ callDepth e′ + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ (b ⊕ a)) ⊕ c ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth val) (callDepth e′) ⟩ + callDepth e ⊔ callDepth val ⊔ callDepth e′ + ∎ +updateRef-pres-callDepth (tail {e = e} ref) stateless val e′ = begin + callDepth (updateRef ref (stateless ∘ tail) (cons (head e) val) e′) + ≤⟨ updateRef-pres-callDepth ref (stateless ∘ tail) (cons (head e) val) e′ ⟩ + callDepth e ⊔ (callDepth e ⊔ callDepth val) ⊔ callDepth e′ + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ (a ⊕ b)) ⊕ c ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth val) (callDepth e′) ⟩ + callDepth e ⊔ callDepth val ⊔ callDepth e′ + ∎ + +subst-pres-callDepth : ∀ (e : Expression Γ t) (args : All (Expression Δ) Γ) → callDepth (subst e args) ℕ.≤ callDepth e ⊔ callDepth′ args +subst-pres-callDepth (lit x) args = ℕ.z≤n +subst-pres-callDepth (state i) args = ℕ.z≤n +subst-pres-callDepth (var i) args = helper i args + where + helper : ∀ i (es : All (Expression Γ) Δ) → callDepth (All.lookup i es) ℕ.≤ callDepth′ es + helper 0F (e ∷ es) = ℕₚ.m≤m⊔n (callDepth e) (callDepth′ es) + helper (suc i) (e ∷ es) = ℕₚ.m≤n⇒m≤o⊔n (callDepth e) (helper i es) +subst-pres-callDepth (abort e) args = subst-pres-callDepth e args +subst-pres-callDepth (e ≟ e₁) args = begin + callDepth (subst e args) ⊔ callDepth (subst e₁ args) + ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩ + callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args) + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩ + callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args + ∎ +subst-pres-callDepth (e > x) args = subst-pres-callDepth e args +subst-pres-callDepth (rnd e) args = subst-pres-callDepth e args +subst-pres-callDepth (fin x e) args = subst-pres-callDepth e args +subst-pres-callDepth (asInt e) args = subst-pres-callDepth e args +subst-pres-callDepth nil args = ℕ.z≤n +subst-pres-callDepth (cons e e₁) args = begin + callDepth (subst e args) ⊔ callDepth (subst e₁ args) + ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩ + callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args) + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩ + callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args + ∎ +subst-pres-callDepth (head e) args = subst-pres-callDepth e args +subst-pres-callDepth (tail e) args = subst-pres-callDepth e args +subst-pres-callDepth (call f es) args = begin + suc (funCallDepth f) ⊔ callDepth′ (subst′ es args) + ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (helper es args) ⟩ + suc (funCallDepth f) ⊔ (callDepth′ es ⊔ callDepth′ args) + ≡⟨ ⊔-solve 3 (λ a b c → a ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (suc (funCallDepth f)) (callDepth′ es) (callDepth′ args) ⟩ + suc (funCallDepth f) ⊔ callDepth′ es ⊔ callDepth′ args + ∎ + where + helper : ∀ {n ts} (es : All (Expression Γ) {n} ts) (args : All (Expression Δ) Γ) → callDepth′ (subst′ es args) ℕ.≤ callDepth′ es ℕ.⊔ callDepth′ args + helper [] args = ℕ.z≤n + helper (e ∷ es) args = begin + callDepth (subst e args) ⊔ callDepth′ (subst′ es args) + ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (helper es args) ⟩ + callDepth e ⊔ callDepth′ args ⊔ (callDepth′ es ⊔ callDepth′ args) + ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth′ es) (callDepth′ args) ⟩ + callDepth e ⊔ callDepth′ es ⊔ callDepth′ args + ∎ +subst-pres-callDepth (if e then e₁ else e₂) args = begin + callDepth (subst e args) ⊔ callDepth (subst e₁ args) ⊔ callDepth (subst e₂ args) + ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args)) (subst-pres-callDepth e₂ args) ⟩ + callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args) ⊔ (callDepth e₂ ⊔ callDepth′ args) + ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ d) ⊕ (b ⊕ d)) ⊕ (c ⊕ d) ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e) (callDepth e₁) (callDepth e₂) (callDepth′ args) ⟩ + callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth′ args + ∎ + +wkn-pres-callDepth : ∀ t i (s : Statement Γ) → stmtCallDepth (wknStatementAt t i s) ≡ stmtCallDepth s +wkn-pres-callDepth t i (s Code.∙ s₁) = cong₂ _⊔_ (wkn-pres-callDepth t i s) (wkn-pres-callDepth t i s₁) +wkn-pres-callDepth t i Code.skip = refl +wkn-pres-callDepth t i (ref Code.≔ x) = cong₂ _⊔_ (wknAt-pres-callDepth i ref) (wknAt-pres-callDepth i x) +wkn-pres-callDepth t i (Code.declare x s) = cong₂ _⊔_ (wknAt-pres-callDepth i x) (wkn-pres-callDepth t (suc i) s) +wkn-pres-callDepth t i (Code.invoke p es) = cong (procCallDepth p ⊔_) (wknAt′-pres-callDepth i es) +wkn-pres-callDepth t i (Code.if x then s) = cong₂ _⊔_ (wknAt-pres-callDepth i x) (wkn-pres-callDepth t i s) +wkn-pres-callDepth t i (Code.if x then s else s₁) = congₙ 3 (λ m n o → m ⊔ n ⊔ o) (wknAt-pres-callDepth i x) (wkn-pres-callDepth t i s) (wkn-pres-callDepth t i s₁) +wkn-pres-callDepth t i (Code.for m s) = wkn-pres-callDepth t (suc i) s + +private + index₀ : Statement Γ → ℕ + index₀ (s ∙ s₁) = index₀ s ℕ.+ index₀ s₁ + index₀ skip = 0 + index₀ (ref ≔ x) = 0 + index₀ (declare x s) = index₀ s + index₀ (invoke p es) = 0 + index₀ (if x then s) = index₀ s + index₀ (if x then s else s₁) = suc (index₀ s ℕ.+ index₀ s₁) + index₀ (for m s) = index₀ s + + index₁ : Statement Γ → ℕ + index₁ (s ∙ s₁) = suc (index₁ s ℕ.+ index₁ s₁) + index₁ skip = 0 + index₁ (ref ≔ x) = 0 + index₁ (declare x s) = index₁ s + index₁ (invoke x x₁) = 0 + index₁ (if x then s) = suc (3 ℕ.* index₁ s) + index₁ (if x then s else s₁) = suc (3 ℕ.* index₁ s ℕ.+ index₁ s₁) + index₁ (for m s) = suc (index₁ s) + + index₂ : Statement Γ → ℕ + index₂ (s ∙ s₁) = 0 + index₂ skip = 0 + index₂ (ref ≔ x) = 0 + index₂ (declare x s) = suc (index₂ s) + index₂ (invoke _ _) = 0 + index₂ (if x then s) = 2 ℕ.* index₂ s + index₂ (if x then s else s₁) = 0 + index₂ (for m s) = 0 + + wkn-pres-index₀ : ∀ t i s → index₀ (wknStatementAt {Γ = Γ} t i s) ≡ index₀ s + wkn-pres-index₀ _ i (s ∙ s₁) = cong₂ ℕ._+_ (wkn-pres-index₀ _ i s) (wkn-pres-index₀ _ i s₁) + wkn-pres-index₀ _ i skip = refl + wkn-pres-index₀ _ i (ref ≔ x) = refl + wkn-pres-index₀ _ i (declare x s) = wkn-pres-index₀ _ (suc i) s + wkn-pres-index₀ _ i (invoke x x₁) = refl + wkn-pres-index₀ _ i (if x then s) = wkn-pres-index₀ _ i s + wkn-pres-index₀ _ i (if x then s else s₁) = cong₂ (λ m n → suc (m ℕ.+ n)) (wkn-pres-index₀ _ i s) (wkn-pres-index₀ _ i s₁) + wkn-pres-index₀ _ i (for m s) = wkn-pres-index₀ _ (suc i) s + + wkn-pres-index₁ : ∀ t i s → index₁ (wknStatementAt {Γ = Γ} t i s) ≡ index₁ s + wkn-pres-index₁ _ i (s ∙ s₁) = cong₂ (λ m n → suc (m ℕ.+ n)) (wkn-pres-index₁ _ i s) (wkn-pres-index₁ _ i s₁) + wkn-pres-index₁ _ i skip = refl + wkn-pres-index₁ _ i (ref ≔ x) = refl + wkn-pres-index₁ _ i (declare x s) = wkn-pres-index₁ _ (suc i) s + wkn-pres-index₁ _ i (invoke x x₁) = refl + wkn-pres-index₁ _ i (if x then s) = cong (λ m → suc (3 ℕ.* m)) (wkn-pres-index₁ _ i s) + wkn-pres-index₁ _ i (if x then s else s₁) = cong₂ (λ m n → suc (3 ℕ.* m ℕ.+ n)) (wkn-pres-index₁ _ i s) (wkn-pres-index₁ _ i s₁) + wkn-pres-index₁ _ i (for m s) = cong suc (wkn-pres-index₁ _ (suc i) s) + + wkn-pres-changes : ∀ t i {s} → ChangesState (wknStatementAt {Γ = Γ} t i s) → ChangesState s + wkn-pres-changes t i {_ ∙ _} (s ∙ˡ s₁) = wkn-pres-changes t i s ∙ˡ _ + wkn-pres-changes t i {_ ∙ _} (s ∙ʳ s₁) = _ ∙ʳ wkn-pres-changes t i s₁ + wkn-pres-changes t i {_ ≔ _} (_≔_ ref {canAssign} {refsState} e) = _≔_ _ {refsState = fromWitness (wknAt-pres-stateless i (toWitness refsState))} _ + wkn-pres-changes t i {declare _ _} (declare e s) = declare _ (wkn-pres-changes t (suc i) s) + wkn-pres-changes t i {invoke _ _} (invoke p es) = invoke _ _ + wkn-pres-changes t i {if _ then _} (if e then s) = if _ then wkn-pres-changes t i s + wkn-pres-changes t i {if _ then _ else _} (if e then′ s else s₁) = if _ then′ wkn-pres-changes t i s else _ + wkn-pres-changes t i {if _ then _ else _} (if e then s else′ s₁) = if _ then _ else′ wkn-pres-changes t i s₁ + wkn-pres-changes t i {for _ _} (for m s) = for m (wkn-pres-changes t (suc i) s) + + RecItem : Set + RecItem = ∃ λ n → ∃ (Statement {n}) + + inlinePredicate : RecItem → Set + inlinePredicate (_ , Γ , s) = ¬ ChangesState s → ∀ {ret} → (e : Expression Γ ret) → ∃ λ (e′ : Expression Γ ret) → callDepth e′ ℕ.≤ stmtCallDepth s ⊔ callDepth e + + inlineRel : RecItem → RecItem → Set + inlineRel = Lex.×-Lex _≡_ ℕ._<_ (Lex.×-Lex _≡_ ℕ._<_ ℕ._<_) on < (index₀ ∘ proj₂ ∘ proj₂) , < (index₁ ∘ proj₂ ∘ proj₂) , (index₂ ∘ proj₂ ∘ proj₂) > > + + inlineRelWf : Wf.WellFounded inlineRel + inlineRelWf = + On.wellFounded + < (index₀ ∘ proj₂ ∘ proj₂) , < (index₁ ∘ proj₂ ∘ proj₂) , (index₂ ∘ proj₂ ∘ proj₂) > > + (Lex.×-wellFounded ℕᵢ.<-wellFounded (Lex.×-wellFounded ℕᵢ.<-wellFounded ℕᵢ.<-wellFounded)) + + s> x) = suc (index e) + index (Code.rnd e) = suc (index e) + index (Code.fin x e) = suc (index e) + index (Code.asInt e) = suc (index e) + index Code.nil = 0 + index (Code.cons e e₁) = 1 ℕ.+ index e ℕ.+ index e₁ + index (Code.head e) = suc (index e) + index (Code.tail e) = suc (index e) + index (Code.call f es) = index′ es + index (Code.if e then e₁ else e₂) = 1 ℕ.+ index e ℕ.+ index e₁ ℕ.+ index e₂ + + index′ [] = 1 + index′ (e ∷ es) = index e ℕ.+ index′ es + + pred : ∃ (Expression Γ) → Set + pred (t , e) = ∃ λ (e : Expression Γ t) → callDepth e ≡ 0 + + pred′ : All (Expression Γ) Δ → Set + pred′ {Δ = Δ} _ = ∃ λ (es : All (Expression Γ) Δ) → callDepth′ es ≡ 0 + + rel = Lex.×-Lex _≡_ ℕ._<_ ℕ._<_ on < callDepth ∘ proj₂ , index ∘ proj₂ > + + data _<′₁_ : ∃ (Expression Γ) → All (Expression Γ) Δ → Set where + inj₁ : {e : Expression Γ t} {es : All (Expression Γ) Δ} → callDepth e ℕ.< callDepth′ es → (t , e) <′₁ es + inj₂ : {e : Expression Γ t} {es : All (Expression Γ) Δ} → callDepth e ≡ callDepth′ es → index e ℕ.< index′ es → (t , e) <′₁ es + + data _<′₂_ : ∀ {n ts} → All (Expression Γ) {n} ts → All (Expression Γ) Δ → Set where + inj₁ : ∀ {n ts} {es′ : All (Expression Γ) {n} ts} {es : All (Expression Γ) Δ} → callDepth′ es′ ℕ.< callDepth′ es → es′ <′₂ es + inj₂ : ∀ {n ts} {es′ : All (Expression Γ) {n} ts} {es : All (Expression Γ) Δ} → callDepth′ es′ ≡ callDepth′ es → index′ es′ ℕ.≤ index′ es → es′ <′₂ es + + <′₁-<′₂-trans : ∀ {n ts} {e : Expression Γ t} {es : All (Expression Γ) Δ} {es′ : All (Expression Γ) {n} ts} → + (t , e) <′₁ es → es <′₂ es′ → (t , e) <′₁ es′ + <′₁-<′₂-trans (inj₁ <₁) (inj₁ <₂) = inj₁ (ℕₚ.<-trans <₁ <₂) + <′₁-<′₂-trans (inj₁ <₁) (inj₂ ≡₂ _) = inj₁ (ℕₚ.<-transˡ <₁ (ℕₚ.≤-reflexive ≡₂)) + <′₁-<′₂-trans (inj₂ ≡₁ _) (inj₁ <₂) = inj₁ (ℕₚ.<-transʳ (ℕₚ.≤-reflexive ≡₁) <₂) + <′₁-<′₂-trans (inj₂ ≡₁ <₁) (inj₂ ≡₂ ≤₂) = inj₂ (trans ≡₁ ≡₂) (ℕₚ.<-transˡ <₁ ≤₂) + + <′₂-trans : ∀ {m n ts ts′} {es : All (Expression Γ) Δ} {es′ : All (Expression Γ) {n} ts} {es′′ : All (Expression Γ) {m} ts′} → + es <′₂ es′ → es′ <′₂ es′′ → es <′₂ es′′ + <′₂-trans (inj₁ <₁) (inj₁ <₂) = inj₁ (ℕₚ.<-trans <₁ <₂) + <′₂-trans (inj₁ <₁) (inj₂ ≡₂ _) = inj₁ (ℕₚ.<-transˡ <₁ (ℕₚ.≤-reflexive ≡₂)) + <′₂-trans (inj₂ ≡₁ _) (inj₁ <₂) = inj₁ (ℕₚ.<-transʳ (ℕₚ.≤-reflexive ≡₁) <₂) + <′₂-trans (inj₂ ≡₁ ≤₁) (inj₂ ≡₂ ≤₂) = inj₂ (trans ≡₁ ≡₂) (ℕₚ.≤-trans ≤₁ ≤₂) + + index′>0 : ∀ (es : All (Expression Γ) Δ) → index′ es ℕ.> 0 + index′>0 [] = ℕₚ.≤-refl + index′>0 (e ∷ es) = ℕₚ.<-transˡ (index′>0 es) (ℕₚ.m≤n+m (index′ es) (index e)) + + e<′₁es⇒e0 es) + + e<′₁e∷es : ∀ e (es : All (Expression Γ) Δ) → (t , e) <′₁ (e ∷ es) + e<′₁e∷es e es with callDepth e in eq₁ | callDepth′ es in eq₂ | ℕ.compare (callDepth e) (callDepth′ es) + ... | _ | _ | ℕ.less m k = inj₁ + (begin + suc (callDepth e) ≡⟨ cong suc eq₁ ⟩ + suc m ≤⟨ ℕₚ.m≤m+n (suc m) k ⟩ + suc m ℕ.+ k ≤⟨ ℕₚ.m≤n⊔m m (suc m ℕ.+ k) ⟩ + m ⊔ (suc m ℕ.+ k) ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩ + callDepth e ⊔ callDepth′ es ∎) + ... | _ | _ | ℕ.equal m = inj₂ + (begin-equality + callDepth e ≡⟨ eq₁ ⟩ + m ≡˘⟨ ℕₚ.⊔-idem m ⟩ + m ⊔ m ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩ + callDepth e ⊔ callDepth′ es ∎) + (e<ᵢe∷es e es) + ... | _ | _ | ℕ.greater n k = inj₂ + (sym (ℕₚ.m≥n⇒m⊔n≡m (begin + callDepth′ es ≡⟨ eq₂ ⟩ + n ≤⟨ ℕₚ.n≤1+n n ⟩ + suc n ≤⟨ ℕₚ.m≤m+n (suc n) k ⟩ + suc n ℕ.+ k ≡˘⟨ eq₁ ⟩ + callDepth e ∎))) + (e<ᵢe∷es e es) + + es<′₂e∷es : ∀ (e : Expression Γ t) (es : All (Expression Γ) Δ) → es <′₂ (e ∷ es) + es<′₂e∷es e es with callDepth e in eq₁ | callDepth′ es in eq₂ | ℕ.compare (callDepth e) (callDepth′ es) + ... | _ | _ | ℕ.less m k = inj₂ + (sym (ℕₚ.m≤n⇒m⊔n≡n (begin + callDepth e ≡⟨ eq₁ ⟩ + m ≤⟨ ℕₚ.n≤1+n m ⟩ + suc m ≤⟨ ℕₚ.m≤m+n (suc m) k ⟩ + suc m ℕ.+ k ≡˘⟨ eq₂ ⟩ + callDepth′ es ∎))) + (ℕₚ.m≤n+m (index′ es) (index e)) + ... | _ | _ | ℕ.equal m = inj₂ + (begin-equality + callDepth′ es ≡⟨ eq₂ ⟩ + m ≡˘⟨ ℕₚ.⊔-idem m ⟩ + m ⊔ m ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩ + callDepth e ⊔ callDepth′ es ∎) + (ℕₚ.m≤n+m (index′ es) (index e)) + ... | _ | _ | ℕ.greater n k = inj₁ + (begin + suc (callDepth′ es) ≡⟨ cong suc eq₂ ⟩ + suc n ≤⟨ ℕₚ.m≤m+n (suc n) k ⟩ + suc n ℕ.+ k ≤⟨ ℕₚ.m≤m⊔n (suc n ℕ.+ k) n ⟩ + suc n ℕ.+ k ⊔ n ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩ + callDepth e ⊔ callDepth′ es ∎) + + relWf = On.wellFounded < callDepth ∘ proj₂ , index ∘ proj₂ > (Lex.×-wellFounded ℕᵢ.<-wellFounded ℕᵢ.<-wellFounded) + + wf′₁ : ∀ f (es : All (Expression Γ) Δ) → Wf.WfRec rel pred (t , call f es) → + ∀ t,e → t,e <′₁ es → pred t,e + wf′₁ f _ rec (_ , e) r = rec (_ , e) (e<′₁es⇒e> x) acc = rec₁ (_>> x) refl refl e acc + helper (_ , Code.rnd e) acc = rec₁ rnd refl refl e acc + helper (_ , Code.fin x e) acc = rec₁ (fin x) refl refl e acc + helper (_ , Code.asInt e) acc = rec₁ asInt refl refl e acc + helper (_ , Code.nil) acc = nil , refl + helper (_ , Code.cons e e₁) acc = rec₂ cons refl refl e e₁ acc + helper (_ , Code.head e) acc = rec₁ head refl refl e acc + helper (_ , Code.tail e) acc = rec₁ tail refl refl e acc + helper (_ , Code.call f es) acc = + acc + (_ , inlineFunction f (proj₁ inner)) + (inj₁ (begin-strict + callDepth (inlineFunction f (proj₁ inner)) ≤⟨ inlineFunction-lowers-callDepth f (proj₁ inner) ⟩ + funCallDepth f ⊔ callDepth′ (proj₁ inner) ≡⟨ cong (funCallDepth f ⊔_) (proj₂ inner) ⟩ + funCallDepth f ⊔ 0 ≡⟨ ℕₚ.⊔-identityʳ (funCallDepth f) ⟩ + funCallDepth f <⟨ ℕₚ.n<1+n (funCallDepth f) ⟩ + suc (funCallDepth f) ≤⟨ ℕₚ.m≤m⊔n (suc (funCallDepth f)) (callDepth′ es) ⟩ + suc (funCallDepth f) ⊔ callDepth′ es ∎)) + where inner = helper′ es (wf′₁ f es acc) (wf′₂ f es acc) + helper (_ , (Code.if e then e₁ else e₂)) acc = rec₃ if_then_else_ refl refl e e₁ e₂ acc + + proj₁ (helper′ [] acc acc′) = [] + proj₁ (helper′ (e ∷ es) acc acc′) = proj₁ (acc (_ , e) (e<′₁e∷es e es)) ∷ proj₁ (acc′ es (es<′₂e∷es e es)) + proj₂ (helper′ [] acc acc′) = refl + proj₂ (helper′ (e ∷ es) acc acc′) = cong₂ _⊔_ (proj₂ (acc (_ , e) (e<′₁e∷es e es))) (proj₂ (acc′ es (es<′₂e∷es e es))) diff --git a/src/Helium/Data/Pseudocode/Properties.agda b/src/Helium/Data/Pseudocode/Properties.agda new file mode 100644 index 0000000..d73b4dd --- /dev/null +++ b/src/Helium/Data/Pseudocode/Properties.agda @@ -0,0 +1,109 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Basic properties of the pseudocode data types +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Helium.Data.Pseudocode.Properties where + +import Data.Nat as ℕ +open import Data.Product using (_,_; uncurry) +open import Data.Vec using ([]; _∷_) +open import Function using (_∋_) +open import Helium.Data.Pseudocode.Core +import Relation.Binary.Consequences as Consequences +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) +open import Relation.Nullary using (Dec; yes; no) +open import Relation.Nullary.Decidable.Core using (map′) +open import Relation.Nullary.Product using (_×-dec_) + +infixl 4 _≟ᵗ_ _≟ˢ_ + +_≟ᵗ_ : ∀ (t t′ : Type) → Dec (t ≡ t′) +bool ≟ᵗ bool = yes refl +bool ≟ᵗ int = no (λ ()) +bool ≟ᵗ fin n = no (λ ()) +bool ≟ᵗ real = no (λ ()) +bool ≟ᵗ bit = no (λ ()) +bool ≟ᵗ bits n = no (λ ()) +bool ≟ᵗ tuple n x = no (λ ()) +bool ≟ᵗ array t′ n = no (λ ()) +int ≟ᵗ bool = no (λ ()) +int ≟ᵗ int = yes refl +int ≟ᵗ fin n = no (λ ()) +int ≟ᵗ real = no (λ ()) +int ≟ᵗ bit = no (λ ()) +int ≟ᵗ bits n = no (λ ()) +int ≟ᵗ tuple n x = no (λ ()) +int ≟ᵗ array t′ n = no (λ ()) +fin n ≟ᵗ bool = no (λ ()) +fin n ≟ᵗ int = no (λ ()) +fin m ≟ᵗ fin n = map′ (cong fin) (λ { refl → refl }) (m ℕ.≟ n) +fin n ≟ᵗ real = no (λ ()) +fin n ≟ᵗ bit = no (λ ()) +fin n ≟ᵗ bits n₁ = no (λ ()) +fin n ≟ᵗ tuple n₁ x = no (λ ()) +fin n ≟ᵗ array t′ n₁ = no (λ ()) +real ≟ᵗ bool = no (λ ()) +real ≟ᵗ int = no (λ ()) +real ≟ᵗ fin n = no (λ ()) +real ≟ᵗ real = yes refl +real ≟ᵗ bit = no (λ ()) +real ≟ᵗ bits n = no (λ ()) +real ≟ᵗ tuple n x = no (λ ()) +real ≟ᵗ array t′ n = no (λ ()) +bit ≟ᵗ bool = no (λ ()) +bit ≟ᵗ int = no (λ ()) +bit ≟ᵗ fin n = no (λ ()) +bit ≟ᵗ real = no (λ ()) +bit ≟ᵗ bit = yes refl +bit ≟ᵗ bits n = no (λ ()) +bit ≟ᵗ tuple n x = no (λ ()) +bit ≟ᵗ array t n = no (λ ()) +bits n ≟ᵗ bool = no (λ ()) +bits n ≟ᵗ int = no (λ ()) +bits n ≟ᵗ fin n₁ = no (λ ()) +bits n ≟ᵗ real = no (λ ()) +bits m ≟ᵗ bit = no (λ ()) +bits m ≟ᵗ bits n = map′ (cong bits) (λ { refl → refl }) (m ℕ.≟ n) +bits n ≟ᵗ tuple n₁ x = no (λ ()) +bits n ≟ᵗ array t′ n₁ = no (λ ()) +tuple n x ≟ᵗ bool = no (λ ()) +tuple n x ≟ᵗ int = no (λ ()) +tuple n x ≟ᵗ fin n₁ = no (λ ()) +tuple n x ≟ᵗ real = no (λ ()) +tuple n x ≟ᵗ bit = no (λ ()) +tuple n x ≟ᵗ bits n₁ = no (λ ()) +tuple _ [] ≟ᵗ tuple _ [] = yes refl +tuple _ [] ≟ᵗ tuple _ (y ∷ ys) = no (λ ()) +tuple _ (x ∷ xs) ≟ᵗ tuple _ [] = no (λ ()) +tuple _ (x ∷ xs) ≟ᵗ tuple _ (y ∷ ys) = map′ (λ { (refl , refl) → refl }) (λ { refl → refl , refl }) (x ≟ᵗ y ×-dec tuple _ xs ≟ᵗ tuple _ ys) +tuple n x ≟ᵗ array t′ n₁ = no (λ ()) +array t n ≟ᵗ bool = no (λ ()) +array t n ≟ᵗ int = no (λ ()) +array t n ≟ᵗ fin n₁ = no (λ ()) +array t n ≟ᵗ real = no (λ ()) +array t n ≟ᵗ bit = no (λ ()) +array t n ≟ᵗ bits n₁ = no (λ ()) +array t n ≟ᵗ tuple n₁ x = no (λ ()) +array t m ≟ᵗ array t′ n = map′ (uncurry (cong₂ array)) (λ { refl → refl , refl }) (t ≟ᵗ t′ ×-dec m ℕ.≟ n) + +_≟ˢ_ : ∀ (t t′ : Sliced) → Dec (t ≡ t′) +bits ≟ˢ bits = yes refl +bits ≟ˢ array x = no (λ ()) +array x ≟ˢ bits = no (λ ()) +array x ≟ˢ array y = map′ (cong array) (λ { refl → refl }) (x ≟ᵗ y) + +bits-injective : ∀ {m n} → (Type ∋ bits m) ≡ bits n → m ≡ n +bits-injective refl = refl + +array-injective₁ : ∀ {t t′ m n} → (Type ∋ array t m) ≡ array t′ n → t ≡ t′ +array-injective₁ refl = refl + +array-injective₂ : ∀ {t t′ m n} → (Type ∋ array t m) ≡ array t′ n → m ≡ n +array-injective₂ refl = refl + +typeEqRecomp : ∀ {t t′} → .(eq : t ≡ t′) → t ≡ t′ +typeEqRecomp = Consequences.dec⇒recomputable _≟ᵗ_ diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda new file mode 100644 index 0000000..8192e5f --- /dev/null +++ b/src/Helium/Semantics/Axiomatic/Assertion.agda @@ -0,0 +1,173 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of assertions used in correctness triples +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Data.Pseudocode.Types using (RawPseudocode) + +module Helium.Semantics.Axiomatic.Assertion + {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} + (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) + where + +open RawPseudocode rawPseudocode + +open import Data.Bool as Bool using (Bool) +open import Data.Empty.Polymorphic using (⊥) +open import Data.Fin as Fin using (suc) +open import Data.Fin.Patterns +open import Data.Nat using (ℕ; suc) +import Data.Nat.Properties as ℕₚ +open import Data.Product using (∃; _×_; _,_; proj₁; proj₂) +open import Data.Sum using (_⊎_) +open import Data.Unit.Polymorphic using (⊤) +open import Data.Vec as Vec using (Vec; []; _∷_; _++_) +open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) +open import Function using (_$_) +open import Helium.Data.Pseudocode.Core +open import Helium.Semantics.Axiomatic.Core rawPseudocode +open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (Term) +open import Level using (_⊔_; Lift; lift; lower) renaming (suc to ℓsuc) + +private + variable + t t′ : Type + m n o : ℕ + Γ Δ Σ ts : Vec Type m + +open Term.Term + +data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) + +data Assertion Σ Γ Δ where + all : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ + some : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ + pred : Term Σ Γ Δ bool → Assertion Σ Γ Δ + comb : ∀ {n} → (Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n → Set (b₁ ⊔ i₁ ⊔ r₁)) → Vec (Assertion Σ Γ Δ) n → Assertion Σ Γ Δ + +substVars : Assertion Σ Γ Δ → All (Term Σ ts Δ) Γ → Assertion Σ ts Δ +substVars (all P) ts = all (substVars P (Term.wknMeta′ ts)) +substVars (some P) ts = some (substVars P (Term.wknMeta′ ts)) +substVars (pred p) ts = pred (Term.substVars p ts) +substVars (comb f Ps) ts = comb f (helper Ps ts) + where + helper : ∀ {n m ts} → Vec (Assertion Σ _ Δ) n → All (Term {n = m} Σ ts Δ) Γ → Vec (Assertion Σ ts Δ) n + helper [] ts = [] + helper (P ∷ Ps) ts = substVars P ts ∷ helper Ps ts + +elimVar : Assertion Σ (t ∷ Γ) Δ → Term Σ Γ Δ t → Assertion Σ Γ Δ +elimVar (all P) t = all (elimVar P (Term.wknMeta t)) +elimVar (some P) t = some (elimVar P (Term.wknMeta t)) +elimVar (pred p) t = pred (Term.elimVar p t) +elimVar (comb f Ps) t = comb f (helper Ps t) + where + helper : ∀ {n} → Vec (Assertion Σ (_ ∷ Γ) Δ) n → Term Σ Γ Δ _ → Vec (Assertion Σ Γ Δ) n + helper [] t = [] + helper (P ∷ Ps) t = elimVar P t ∷ helper Ps t + +wknVar : Assertion Σ Γ Δ → Assertion Σ (t ∷ Γ) Δ +wknVar (all P) = all (wknVar P) +wknVar (some P) = some (wknVar P) +wknVar (pred p) = pred (Term.wknVar p) +wknVar (comb f Ps) = comb f (helper Ps) + where + helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (_ ∷ Γ) Δ) n + helper [] = [] + helper (P ∷ Ps) = wknVar P ∷ helper Ps + +wknVars : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (ts ++ Γ) Δ +wknVars τs (all P) = all (wknVars τs P) +wknVars τs (some P) = some (wknVars τs P) +wknVars τs (pred p) = pred (Term.wknVars τs p) +wknVars τs (comb f Ps) = comb f (helper Ps) + where + helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (τs ++ Γ) Δ) n + helper [] = [] + helper (P ∷ Ps) = wknVars τs P ∷ helper Ps + +addVars : Assertion Σ [] Δ → Assertion Σ Γ Δ +addVars (all P) = all (addVars P) +addVars (some P) = some (addVars P) +addVars (pred p) = pred (Term.addVars p) +addVars (comb f Ps) = comb f (helper Ps) + where + helper : ∀ {n} → Vec (Assertion Σ [] Δ) n → Vec (Assertion Σ Γ Δ) n + helper [] = [] + helper (P ∷ Ps) = addVars P ∷ helper Ps + +wknMetaAt : ∀ i → Assertion Σ Γ Δ → Assertion Σ Γ (Vec.insert Δ i t) +wknMetaAt i (all P) = all (wknMetaAt (suc i) P) +wknMetaAt i (some P) = some (wknMetaAt (suc i) P) +wknMetaAt i (pred p) = pred (Term.wknMetaAt i p) +wknMetaAt i (comb f Ps) = comb f (helper i Ps) + where + helper : ∀ {n} i → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ Γ (Vec.insert Δ i _)) n + helper i [] = [] + helper i (P ∷ Ps) = wknMetaAt i P ∷ helper i Ps + +-- NOTE: better to induct on P instead of ts? +wknMetas : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ Γ (ts ++ Δ) +wknMetas [] P = P +wknMetas (_ ∷ ts) P = wknMetaAt 0F (wknMetas ts P) + +module _ (2≉0 : Term.2≉0) where + -- NOTE: better to induct on e here than in Term? + subst : Assertion Σ Γ Δ → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Assertion Σ Γ Δ + subst (all P) e t = all (subst P e (Term.wknMeta t)) + subst (some P) e t = some (subst P e (Term.wknMeta t)) + subst (pred p) e t = pred (Term.subst 2≉0 p e t) + subst (comb f Ps) e t = comb f (helper Ps e t) + where + helper : ∀ {t n} → Vec (Assertion Σ Γ Δ) n → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) n + helper [] e t = [] + helper (P ∷ Ps) e t = subst P e t ∷ helper Ps e t + +module Construct where + infixl 6 _∧_ + infixl 5 _∨_ + + true : Assertion Σ Γ Δ + true = comb (λ _ → ⊤) [] + + false : Assertion Σ Γ Δ + false = comb (λ _ → ⊥) [] + + _∧_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ + P ∧ Q = comb (λ { (P ∷ Q ∷ []) → P × Q }) (P ∷ Q ∷ []) + + _∨_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ + P ∨ Q = comb (λ { (P ∷ Q ∷ []) → P ⊎ Q }) (P ∷ Q ∷ []) + + equal : Term Σ Γ Δ t → Term Σ Γ Δ t → Assertion Σ Γ Δ + equal {t = bool} x y = pred Term.[ bool ][ x ≟ y ] + equal {t = int} x y = pred Term.[ int ][ x ≟ y ] + equal {t = fin n} x y = pred Term.[ fin ][ x ≟ y ] + equal {t = real} x y = pred Term.[ real ][ x ≟ y ] + equal {t = bit} x y = pred Term.[ bit ][ x ≟ y ] + equal {t = bits n} x y = pred Term.[ bits ][ x ≟ y ] + equal {t = tuple _ []} x y = true + equal {t = tuple _ (t ∷ ts)} x y = equal {t = t} (Term.func₁ proj₁ x) (Term.func₁ proj₁ y) ∧ equal (Term.func₁ proj₂ x) (Term.func₁ proj₂ y) + equal {t = array t 0} x y = true + equal {t = array t (suc n)} x y = all (equal {t = t} (index x) (index y)) + where + index = λ v → Term.unbox (array t) $ + Term.func₁ proj₁ $ + Term.cut (array t) + (Term.cast (array t) (ℕₚ.+-comm 1 n) (Term.wknMeta v)) + (meta 0F) + +open Construct public + +⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Set (b₁ ⊔ i₁ ⊔ r₁) +⟦_⟧′ : Vec (Assertion Σ Γ Δ) n → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n + +⟦ all P ⟧ σ γ δ = ∀ x → ⟦ P ⟧ σ γ (x , δ) +⟦ some P ⟧ σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (x , δ) +⟦ pred p ⟧ σ γ δ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Bool.T (lower (Term.⟦ p ⟧ σ γ δ))) +⟦ comb f Ps ⟧ σ γ δ = f (⟦ Ps ⟧′ σ γ δ) + +⟦ [] ⟧′ σ γ δ = [] +⟦ P ∷ Ps ⟧′ σ γ δ = ⟦ P ⟧ σ γ δ ∷ ⟦ Ps ⟧′ σ γ δ diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda new file mode 100644 index 0000000..3b7e8db --- /dev/null +++ b/src/Helium/Semantics/Axiomatic/Core.agda @@ -0,0 +1,85 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Base definitions for the axiomatic semantics +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Data.Pseudocode.Types using (RawPseudocode) + +module Helium.Semantics.Axiomatic.Core + {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} + (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) + where + +private + open module C = RawPseudocode rawPseudocode + +open import Data.Bool as Bool using (Bool) +open import Data.Fin as Fin using (Fin; zero; suc) +open import Data.Fin.Patterns +open import Data.Nat as ℕ using (ℕ; suc) +import Data.Nat.Induction as Natᵢ +import Data.Nat.Properties as ℕₚ +open import Data.Product as × using (_×_; _,_; uncurry) +open import Data.Sum using (_⊎_) +open import Data.Unit using (⊤) +open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup) +open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) +open import Function using (_on_) +open import Helium.Data.Pseudocode.Core +open import Helium.Data.Pseudocode.Properties +import Induction.WellFounded as Wf +open import Level using (_⊔_; Lift; lift) +import Relation.Binary.Construct.On as On +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) +open import Relation.Nullary using (Dec; does; yes; no) +open import Relation.Nullary.Decidable.Core using (True; toWitness; map′) +open import Relation.Nullary.Product using (_×-dec_) +open import Relation.Unary using (_⊆_) + +private + variable + t t′ : Type + m n : ℕ + Γ Δ Σ ts : Vec Type m + +⟦_⟧ₜ : Type → Set (b₁ ⊔ i₁ ⊔ r₁) +⟦_⟧ₜ′ : Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) + +⟦ bool ⟧ₜ = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool +⟦ int ⟧ₜ = Lift (b₁ ⊔ r₁) ℤ +⟦ fin n ⟧ₜ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n) +⟦ real ⟧ₜ = Lift (b₁ ⊔ i₁) ℝ +⟦ bit ⟧ₜ = Lift (i₁ ⊔ r₁) Bit +⟦ bits n ⟧ₜ = Vec ⟦ bit ⟧ₜ n +⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ +⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n + +⟦ [] ⟧ₜ′ = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤ +⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′ + +fetch : ∀ i → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ +fetch {Γ = _ ∷ _} 0F (x , _) = x +fetch {Γ = _ ∷ _} (suc i) (_ , xs) = fetch i xs + +Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁) +Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ + +Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁) +Predicate ts = ⟦ ts ⟧ₜ′ → Bool + +-- data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where +-- _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R +-- skip : ∀ {P} → HoareTriple P skip P + +-- assign : ∀ {P t ref canAssign e} → HoareTriple (asrtSubst P (toWitness canAssign) (ℰ e)) (_≔_ {t = t} ref {canAssign} e) P +-- declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (termWknVar (ℰ e))) s (asrtWknVar Q) → HoareTriple (asrtElimVar P (ℰ e)) (declare {t = t} e s) Q +-- invoke : ∀ {m ts P Q s e} → HoareTriple (assignMetas Δ ts (All.tabulate var) (asrtAddVars P)) s (asrtAddVars Q) → HoareTriple (assignMetas Δ ts (All.tabulate (λ i → ℰ (All.lookup i e))) (asrtAddVars P)) (invoke {m = m} {ts} (s ∙end) e) (asrtAddVars Q) +-- if : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q +-- for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.inject₁ x) }) (meta 1F ∷ [])))) s (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.suc x) }) (meta 1F ∷ [])))) → HoareTriple (some (I ∧ equal (meta 0F) (func (λ _ _ → lift 0F) []))) (for m s) (some (I ∧ equal (meta 0F) (func (λ _ _ → lift (Fin.fromℕ m)) []))) + +-- consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → ⟦ P₁ ⟧ₐ ⊆ ⟦ P₂ ⟧ₐ → HoareTriple P₂ s Q₂ → ⟦ Q₂ ⟧ₐ ⊆ ⟦ Q₁ ⟧ₐ → HoareTriple P₁ s Q₁ +-- some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q) +-- frame : ∀ {P Q R s} → HoareTriple P s Q → HoareTriple (P * R) s (Q * R) diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda new file mode 100644 index 0000000..2719455 --- /dev/null +++ b/src/Helium/Semantics/Axiomatic/Term.agda @@ -0,0 +1,385 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of terms for use in assertions +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Data.Pseudocode.Types using (RawPseudocode) + +module Helium.Semantics.Axiomatic.Term + {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} + (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) + where + +open RawPseudocode rawPseudocode + +import Data.Bool as Bool +open import Data.Fin as Fin using (Fin; suc) +import Data.Fin.Properties as Finₚ +open import Data.Fin.Patterns +open import Data.Nat as ℕ using (ℕ; suc) +import Data.Nat.Properties as ℕₚ +open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; uncurry; dmap) +open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup) +import Data.Vec.Functional as VecF +import Data.Vec.Properties as Vecₚ +open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_) +open import Function using (_∘_; _∘₂_; id; flip) +open import Helium.Data.Pseudocode.Core +import Helium.Data.Pseudocode.Manipulate as M +open import Helium.Semantics.Axiomatic.Core rawPseudocode +open import Level using (_⊔_; lift; lower) +open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst) +open import Relation.Nullary using (does; yes; no; ¬_) +open import Relation.Nullary.Decidable.Core using (True; toWitness) +open import Relation.Nullary.Negation using (contradiction) + +private + variable + t t′ t₁ t₂ : Type + m n o : ℕ + Γ Δ Σ ts : Vec Type m + +data Term (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where + state : ∀ i → Term Σ Γ Δ (lookup Σ i) + var : ∀ i → Term Σ Γ Δ (lookup Γ i) + meta : ∀ i → Term Σ Γ Δ (lookup Δ i) + func : Transform ts t → All (Term Σ Γ Δ) ts → Term Σ Γ Δ t + +castType : Term Σ Γ Δ t → t ≡ t′ → Term Σ Γ Δ t′ +castType (state i) refl = state i +castType (var i) refl = var i +castType (meta i) refl = meta i +castType (func f ts) eq = func (≡-subst (Transform _) eq f) ts + +substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t +substState (state i) j t′ with i Fin.≟ j +... | yes refl = t′ +... | no _ = state i +substState (var i) j t′ = var i +substState (meta i) j t′ = meta i +substState (func f ts) j t′ = func f (helper ts j t′) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Σ i) → All (Term Σ Γ Δ) ts + helper [] i t′ = [] + helper (t ∷ ts) i t′ = substState t i t′ ∷ helper ts i t′ + +substVar : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Γ i) → Term Σ Γ Δ t +substVar (state i) j t′ = state i +substVar (var i) j t′ with i Fin.≟ j +... | yes refl = t′ +... | no _ = var i +substVar (meta i) j t′ = meta i +substVar (func f ts) j t′ = func f (helper ts j t′) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Γ i) → All (Term Σ Γ Δ) ts + helper [] i t′ = [] + helper (t ∷ ts) i t′ = substVar t i t′ ∷ helper ts i t′ + +substVars : Term Σ Γ Δ t → All (Term Σ ts Δ) Γ → Term Σ ts Δ t +substVars (state i) ts = state i +substVars (var i) ts = All.lookup i ts +substVars (meta i) ts = meta i +substVars (func f ts′) ts = func f (helper ts′ ts) + where + helper : ∀ {ts ts′} → All (Term Σ Γ Δ) {n} ts → All (Term {n = m} Σ ts′ Δ) Γ → All (Term Σ ts′ Δ) ts + helper [] ts = [] + helper (t ∷ ts′) ts = substVars t ts ∷ helper ts′ ts + +elimVar : Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t +elimVar (state i) t′ = state i +elimVar (var 0F) t′ = t′ +elimVar (var (suc i)) t′ = var i +elimVar (meta i) t′ = meta i +elimVar (func f ts) t′ = func f (helper ts t′) + where + helper : ∀ {n ts} → All (Term Σ (_ ∷ Γ) Δ) {n} ts → Term Σ Γ Δ _ → All (Term Σ Γ Δ) ts + helper [] t′ = [] + helper (t ∷ ts) t′ = elimVar t t′ ∷ helper ts t′ + +wknVar : Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t +wknVar (state i) = state i +wknVar (var i) = var (suc i) +wknVar (meta i) = meta i +wknVar (func f ts) = func f (helper ts) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (_ ∷ Γ) Δ) ts + helper [] = [] + helper (t ∷ ts) = wknVar t ∷ helper ts + +wknVars : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t +wknVars τs (state i) = state i +wknVars τs (var i) = castType (var (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknVars τs (meta i) = meta i +wknVars τs (func f ts) = func f (helper ts) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (τs ++ Γ) Δ) ts + helper [] = [] + helper (t ∷ ts) = wknVars τs t ∷ helper ts + +addVars : Term Σ [] Δ t → Term Σ Γ Δ t +addVars (state i) = state i +addVars (meta i) = meta i +addVars (func f ts) = func f (helper ts) + where + helper : ∀ {n ts} → All (Term Σ [] Δ) {n} ts → All (Term Σ Γ Δ) ts + helper [] = [] + helper (t ∷ ts) = addVars t ∷ helper ts + +wknMetaAt : ∀ i → Term Σ Γ Δ t → Term Σ Γ (Vec.insert Δ i t′) t +wknMetaAt′ : ∀ i → All (Term Σ Γ Δ) ts → All (Term Σ Γ (Vec.insert Δ i t′)) ts + +wknMetaAt i (state j) = state j +wknMetaAt i (var j) = var j +wknMetaAt i (meta j) = castType (meta (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j) +wknMetaAt i (func f ts) = func f (wknMetaAt′ i ts) + +wknMetaAt′ i [] = [] +wknMetaAt′ i (t ∷ ts) = wknMetaAt i t ∷ wknMetaAt′ i ts + +wknMeta : Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t +wknMeta = wknMetaAt 0F + +wknMeta′ : All (Term Σ Γ Δ) ts → All (Term Σ Γ (t′ ∷ Δ)) ts +wknMeta′ = wknMetaAt′ 0F + +wknMetas : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (ts ++ Δ) t +wknMetas τs (state i) = state i +wknMetas τs (var i) = var i +wknMetas τs (meta i) = castType (meta (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i) +wknMetas τs (func f ts) = func f (helper ts) + where + helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts + helper [] = [] + helper (t ∷ ts) = wknMetas τs t ∷ helper ts + +func₀ : ⟦ t ⟧ₜ → Term Σ Γ Δ t +func₀ f = func (λ _ → f) [] + +func₁ : (⟦ t ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t → Term Σ Γ Δ t′ +func₁ f t = func (λ (x , _) → f x) (t ∷ []) + +func₂ : (⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ t′ +func₂ f t₁ t₂ = func (λ (x , y , _) → f x y) (t₁ ∷ t₂ ∷ []) + +[_][_≟_] : HasEquality t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool +[ bool ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Bool.≟ y))) t t′ +[ int ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᶻ y))) t t′ +[ fin ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Fin.≟ y))) t t′ +[ real ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ʳ y))) t t′ +[ bit ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᵇ₁ y))) t t′ +[ bits ][ t ≟ t′ ] = func₂ (λ xs ys → lift (does (VecF.fromVec (Vec.map lower xs) ≟ᵇ VecF.fromVec (Vec.map lower ys)))) t t′ + +[_][_>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int +[ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t + +-- 0 of y is 0 of result +join′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ +join′ bits = flip _++_ +join′ (array t) = flip _++_ + +take′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t m ⟧ₜ +take′ bits m = Vec.take m +take′ (array t) m = Vec.take m + +drop′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t n ⟧ₜ +drop′ bits m = Vec.drop m +drop′ (array t) m = Vec.drop m + +private + m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n + m≤n⇒m+k≡n ℕ.z≤n = _ , refl + m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n) + + slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n + slicedSize n m i = k , (begin + n ℕ.+ m ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩ + (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨ ℕₚ.+-assoc (Fin.toℕ i) k m ⟩ + Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨ cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩ + Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) , + proj₂ i+k≡n + where + open ≡-Reasoning + i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ> n) eq = [ 2≉0 ][ helper e eq >> n ] + helper (Code.rnd e) eq = func₁ (lift ∘ ⌊_⌋ ∘ lower) (helper e eq) + helper (Code.fin f e) eq = func₁ (lift ∘ f ∘ flatten) (helper e eq) + helper (Code.asInt e) eq = func₁ (lift ∘ (ℤ′._×′ 1ℤ) ∘ Fin.toℕ ∘ lower) (helper e eq) + helper Code.nil eq = func₀ _ + helper (Code.cons e e₁) eq = func₂ _,_ (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq)) + helper (Code.head e) eq = func₁ proj₁ (helper e eq) + helper (Code.tail e) eq = func₁ proj₂ (helper e eq) + helper (Code.call f es) eq = contradiction (trans (sym eq) (proj₂ (1+m⊔n≡1+k (M.funCallDepth f) (M.callDepth′ es)))) ℕₚ.0≢1+n + helper (Code.if e then e₁ else e₂) eq = func (λ (lift b , x , x₁ , _) → Bool.if b then x else x₁) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ []) + + ℰ′ : All (Code.Expression Σ Γ) ts → All (Term Σ Γ Δ) ts + ℰ′ [] = [] + ℰ′ (e ∷ es) = ℰ e ∷ ℰ′ es + + subst : Term Σ Γ Δ t → {e : Code.Expression Σ Γ t′} → Code.CanAssign Σ e → Term Σ Γ Δ t′ → Term Σ Γ Δ t + subst t (Code.state i) t′ = substState t i t′ + subst t (Code.var i) t′ = substVar t i t′ + subst t (Code.abort e) t′ = func₁ (λ ()) (ℰ e) + subst t (Code.[_] {t = τ} ref) t′ = subst t ref (unbox τ t′) + subst t (Code.unbox {t = τ} ref) t′ = subst t ref [ τ ][ t′ ] + subst t (Code.splice {t = τ} ref ref₁ e₃) t′ = subst (subst t ref (func₁ proj₁ (cut τ t′ (ℰ e₃)))) ref₁ (func₁ (proj₁ ∘ proj₂) (cut τ t′ (ℰ e₃))) + subst t (Code.cut {t = τ} ref e₂) t′ = subst t ref (splice τ (func₁ proj₁ t′) (func₁ (proj₁ ∘ proj₂) t′) (ℰ e₂)) + subst t (Code.cast {t = τ} eq ref) t′ = subst t ref (cast τ (sym eq) t′) + subst t Code.nil t′ = t + subst t (Code.cons ref ref₁) t′ = subst (subst t ref (func₁ proj₁ t′)) ref₁ (func₁ proj₂ t′) + subst t (Code.head {e = e} ref) t′ = subst t ref (func₂ _,_ t′ (func₁ proj₂ (ℰ e))) + subst t (Code.tail {t = τ} {e = e} ref) t′ = subst t ref (func₂ {t₁ = τ} _,_ (func₁ proj₁ (ℰ e)) t′) + +⟦_⟧ : Term Σ Γ Δ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ t ⟧ₜ +⟦_⟧′ : ∀ {ts} → All (Term Σ Γ Δ) {n} ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ ts ⟧ₜ′ + +⟦ state i ⟧ σ γ δ = fetch i σ +⟦ var i ⟧ σ γ δ = fetch i γ +⟦ meta i ⟧ σ γ δ = fetch i δ +⟦ func f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ) + +⟦ [] ⟧′ σ γ δ = _ +⟦ t ∷ ts ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ ts ⟧′ σ γ δ diff --git a/src/Helium/Semantics/Axiomatic/Triple.agda b/src/Helium/Semantics/Axiomatic/Triple.agda new file mode 100644 index 0000000..7564983 --- /dev/null +++ b/src/Helium/Semantics/Axiomatic/Triple.agda @@ -0,0 +1,46 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of Hoare triples +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Data.Pseudocode.Types using (RawPseudocode) + +module Helium.Semantics.Axiomatic.Triple + {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} + (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) + where + +private + open module C = RawPseudocode rawPseudocode + +import Data.Bool as Bool +import Data.Fin as Fin +open import Data.Fin.Patterns +open import Data.Nat using (suc) +open import Data.Vec using (Vec; _∷_) +open import Function using (_∘_) +open import Helium.Data.Pseudocode.Core +open import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Asrt +open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (var; meta; func₀; func₁; 𝒦; ℰ; ℰ′) +open import Level using (_⊔_; lift; lower) renaming (suc to ℓsuc) +open import Relation.Nullary.Decidable.Core using (toWitness) +open import Relation.Unary using (_⊆′_) + +module _ (2≉0 : Term.2≉0) {o} {Σ : Vec Type o} where + open Code Σ + data HoareTriple {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} : Assertion Σ Γ Δ → Statement Γ → Assertion Σ Γ Δ → Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) where + _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R + skip : ∀ {P} → HoareTriple P skip P + + assign : ∀ {P t ref canAssign e} → HoareTriple (subst 2≉0 P (toWitness canAssign) (ℰ 2≉0 e)) (_≔_ {t = t} ref {canAssign} e) P + declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (Term.wknVar (ℰ 2≉0 e))) s (Asrt.wknVar Q) → HoareTriple (Asrt.elimVar P (ℰ 2≉0 e)) (declare {t = t} e s) Q + invoke : ∀ {m ts P Q s es} → HoareTriple P s (Asrt.addVars Q) → HoareTriple (Asrt.substVars P (ℰ′ 2≉0 es)) (invoke {m = m} {ts} (s ∙end) es) (Asrt.addVars Q) + if : ∀ {P Q e s} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s Q → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.false ′b))) skip Q → HoareTriple P (if e then s) Q + if-else : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q + for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.inject₁ ∘ lower) (meta 1F)))) s (some (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.suc ∘ lower) (meta 1F)))) → HoareTriple (some (I ∧ equal (meta 0F) (func₀ (lift 0F)))) (for m s) (some (I ∧ equal (meta 0F) (func₀ (lift (Fin.fromℕ m))))) + + consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → (∀ σ γ δ → ⟦ P₁ ⟧ σ γ δ → ⟦ P₂ ⟧ σ γ δ) → HoareTriple P₂ s Q₂ → (∀ σ γ δ → ⟦ Q₂ ⟧ σ γ δ → ⟦ Q₁ ⟧ σ γ δ) → HoareTriple P₁ s Q₁ + some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q) -- cgit v1.2.3