Add definition of Hoare logic semantics.

4 files changed, 689 insertions, 0 deletions

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′
+
+[_][_<?_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+[ int ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ᶻ? y))) t t′
+[ real ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ʳ? y))) t t′
+
+[_][_] : ∀ t → Term Σ Γ Δ (elemType t) → Term Σ Γ Δ (asType t 1)
+[ bits ][ t ] = func₁ (_∷ []) t
+[ array τ ][ t ] = func₁ (_∷ []) t
+
+unbox : ∀ t → Term Σ Γ Δ (asType t 1) → Term Σ Γ Δ (elemType t)
+unbox bits = func₁ Vec.head
+unbox (array t) = func₁ Vec.head
+
+castV : ∀ {a} {A : Set a} {m n} → .(eq : m ≡ n) → Vec A m → Vec A n
+castV {n = 0}     eq []       = []
+castV {n = suc n} eq (x ∷ xs) = x ∷ castV (ℕₚ.suc-injective eq) xs
+
+cast′ : ∀ t → .(eq : m ≡ n) → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ
+cast′ bits      eq = castV eq
+cast′ (array τ) eq = castV eq
+
+cast : ∀ t → .(eq : m ≡ n) → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n)
+cast τ eq = func₁ (cast′ τ eq)
+
+[_][-_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t
+[ int ][- t ] = func₁ (lift ∘ ℤ.-_ ∘ lower) t
+[ real ][- t ] = func₁ (lift ∘ ℝ.-_ ∘ lower) t
+
+[_,_,_,_][_+_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.+ y)) t t′
+[ int , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.+ y)) t t′
+[ real , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y /1)) t t′
+[ real , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y)) t t′
+
+[_,_,_,_][_*_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.* y)) t t′
+[ int , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.* y)) t t′
+[ real , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y /1)) t t′
+[ real , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y)) t t′
+
+[_][_^_] : IsNumeric t → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
+[ int ][ t ^ n ] = func₁ (lift ∘ (ℤ′._^′ n) ∘ lower) t
+[ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
+
+2≉0 : Set _
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+
+[_][_>>_] : 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 i))
+    k = proj₁ i+k≡n
+
+-- 0 of x is i of result
+splice′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+splice′ {m = m} t x y (lift i) = cast′ t eq (join′ t (join′ t high x) low)
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  n≡i+k = sym (proj₂ (proj₂ reasoning))
+  low = take′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  high = drop′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  eq = sym (proj₁ (proj₂ reasoning))
+
+splice : ∀ t → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (asType t (n ℕ.+ m))
+splice τ t₁ t₂ t′ = func (λ (x , y , i , _) → splice′ τ x y i) (t₁ ∷ t₂ ∷ t′ ∷ [])
+
+-- i of x is 0 of first
+cut′ : ∀ t → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
+cut′ {m = m} t x (lift i) = middle , cast′ t i+k≡n (join′ t high low) , _
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  i+k≡n = proj₂ (proj₂ reasoning)
+  eq = proj₁ (proj₂ reasoning)
+  low = take′ t (Fin.toℕ i) (cast′ t eq x)
+  middle = take′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+  high = drop′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+
+cut : ∀ t → Term Σ Γ Δ (asType t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (tuple _ (asType t m ∷ asType t n ∷ []))
+cut τ t t′ = func₂ (cut′ τ) t t′
+
+flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms
+flatten {ms = []}     _             = []
+flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs
+
+𝒦 : Literal t → Term Σ Γ Δ t
+𝒦 (x ′b) = func₀ (lift x)
+𝒦 (x ′i) = func₀ (lift (x ℤ′.×′ 1ℤ))
+𝒦 (x ′f) = func₀ (lift x)
+𝒦 (x ′r) = func₀ (lift (x ℝ′.×′ 1ℝ))
+𝒦 (x ′x) = func₀ (lift (Bool.if x then 1𝔹 else 0𝔹))
+𝒦 ([] ′xs) = func₀ []
+𝒦 ((x ∷ xs) ′xs) = func₂ (flip Vec._∷ʳ_) (𝒦 (x ′x)) (𝒦 (xs ′xs))
+𝒦 (x ′a) = func₁ Vec.replicate (𝒦 x)
+
+module _ (2≉0 : 2≉0) where
+  ℰ : Code.Expression Σ Γ t → Term Σ Γ Δ t
+  ℰ e = (uncurry helper) (M.elimFunctions e)
+    where
+    1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k
+    1+m⊔n≡1+k m 0       = m , refl
+    1+m⊔n≡1+k m (suc n) = m ℕ.⊔ n , refl
+
+    pull-0₂ : ∀ {x y} → x ℕ.⊔ y ≡ 0 → x ≡ 0
+    pull-0₂ {0} {0}     refl = refl
+    pull-0₂ {0} {suc y} ()
+
+    pull-0₃ : ∀ {x y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → x ≡ 0
+    pull-0₃ {0}     {0}     {0} refl = refl
+    pull-0₃ {0}     {suc y} {0}     ()
+    pull-0₃ {suc x} {0}     {0}     ()
+    pull-0₃ {suc x} {0}     {suc z} ()
+
+    pull-1₃ : ∀ x {y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → y ≡ 0
+    pull-1₃ 0       {0}     {0}     refl = refl
+    pull-1₃ 0       {suc y} {0}     ()
+    pull-1₃ (suc x) {0}     {0}     ()
+    pull-1₃ (suc x) {0}     {suc z} ()
+
+    pull-last : ∀ {x y} → x ℕ.⊔ y ≡ 0 → y ≡ 0
+    pull-last {0}     {0} refl = refl
+    pull-last {suc x} {0} ()
+
+    helper : ∀ (e : Code.Expression Σ Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t
+    helper (Code.lit x) eq = 𝒦 x
+    helper (Code.state i) eq = state i
+    helper (Code.var i) eq = var i
+    helper (Code.abort e) eq = func₁ (λ ()) (helper e eq)
+    helper (Code._≟_ {hasEquality = hasEq} e e₁) eq = [ toWitness hasEq ][ helper e (pull-0₂ eq) ≟ helper e₁ (pull-last eq) ]
+    helper (Code._<?_ {isNumeric = isNum} e e₁) eq = [ toWitness isNum ][ helper e (pull-0₂ eq) <? helper e₁ (pull-last eq) ]
+    helper (Code.inv e) eq = func₁ (lift ∘ Bool.not ∘ lower) (helper e eq)
+    helper (e Code.&& e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∧ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.|| e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∨ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.not e) eq = func₁ (Vec.map (lift ∘ 𝔹.¬_ ∘ lower)) (helper e eq)
+    helper (e Code.and e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∧ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.or e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∨ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.[_] {t = t} e) eq = [ t ][ helper e eq ]
+    helper (Code.unbox {t = t} e) eq = unbox t (helper e eq)
+    helper (Code.splice {t = t} e e₁ e₂) eq = splice t (helper e (pull-0₃ eq)) (helper e₁ (pull-1₃ (M.callDepth e) eq)) (helper e₂ (pull-last eq))
+    helper (Code.cut {t = t} e e₁) eq = cut t (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.cast {t = t} i≡j e) eq = cast t i≡j (helper e eq)
+    helper (Code.-_ {isNumeric = isNum} e) eq = [ toWitness isNum ][- helper e eq ]
+    helper (Code._+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) + helper e₁ (pull-last eq) ]
+    helper (Code._*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) * helper e₁ (pull-last eq) ]
+    helper (Code._^_ {isNumeric = isNum} e y) eq = [ toWitness isNum ][ helper e eq ^ y ]
+    helper (e Code.>> 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)