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/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 +++ 4 files changed, 689 insertions(+) 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/Helium/Semantics/Axiomatic') 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