diff options
Diffstat (limited to 'src/Helium/Semantics')
| -rw-r--r-- | src/Helium/Semantics/Denotational.agda | 310 | ||||
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 128 |
2 files changed, 0 insertions, 438 deletions
diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda deleted file mode 100644 index 8e521ea..0000000 --- a/src/Helium/Semantics/Denotational.agda +++ /dev/null @@ -1,310 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Denotational semantics of Armv8-M instructions. ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -open import Helium.Data.Pseudocode.Types - -module Helium.Semantics.Denotational - {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} - (pseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) - where - -open import Algebra.Core using (Op₂) -open import Data.Bool as Bool using (Bool; true; false) -open import Data.Fin as Fin hiding (cast; lift; _+_) -import Data.Fin.Properties as Finₚ -import Data.List as List -open import Data.Nat hiding (_⊔_) -import Data.Nat.Properties as ℕₚ -open import Data.Product using (∃; _×_; _,_; dmap) -open import Data.Sum using ([_,_]′) -open import Data.Vec.Functional as V using (Vector; []; _∷_) -open import Function using (_|>_; _$_; _∘₂_) -open import Function.Nary.NonDependent.Base -import Helium.Instructions as Instr -import Helium.Semantics.Denotational.Core as Core -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong) -open import Relation.Nullary using (does) -open import Relation.Nullary.Decidable - -open RawPseudocode pseudocode - -private - ℓ : Level - ℓ = b₁ - -record State : Set ℓ where - field - S : Vector (Bits 32) 32 - R : Vector (Bits 32) 16 - P0 : Bits 16 - mask : Bits 8 - QC : Bit - advanceVPT : Bool - -open Core State - -Beat : Set -Beat = Fin 4 - -hilow : Beat → Fin 2 -hilow zero = zero -hilow (suc zero) = zero -hilow (suc (suc _)) = suc zero - -oddeven : Beat → Fin 2 -oddeven zero = zero -oddeven (suc zero) = suc zero -oddeven (suc (suc zero)) = zero -oddeven (suc (suc (suc zero))) = suc zero - -ElmtMask : Set b₁ -ElmtMask = Bits 4 - --- State properties - -&R : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 16) → Reference n Γ (Bits 32) -&R e = record - { get = λ σ ρ → State.R σ (e σ ρ) - ; set = λ x σ ρ → record σ { R = V.updateAt (e σ ρ) (λ _ → x) (State.R σ) } , ρ - } - -&S : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 32) → Reference n Γ (Bits 32) -&S e = record - { get = λ σ ρ → State.S σ (e σ ρ) - ; set = λ x σ ρ → record σ { S = V.updateAt (e σ ρ) (λ _ → x) (State.S σ) } , ρ - } - -&Q : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Instr.VecReg → Expr n Γ Beat → Reference n Γ (Bits 32) -&Q reg beat = &S λ σ ρ → combine (reg σ ρ) (beat σ ρ) - -&FPSCR-QC : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bit -&FPSCR-QC = record - { get = λ σ ρ → State.QC σ - ; set = λ x σ ρ → record σ { QC = x } , ρ - } - -&VPR-P0 : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 16) -&VPR-P0 = record - { get = λ σ ρ → State.P0 σ - ; set = λ x σ ρ → record σ { P0 = x } , ρ - } - -&VPR-mask : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ (Bits 8) -&VPR-mask = record - { get = λ σ ρ → State.mask σ - ; set = λ x σ ρ → record σ { mask = x } , ρ - } - -&AdvanceVPT : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bool -&AdvanceVPT = record - { get = λ σ ρ → State.advanceVPT σ - ; set = λ x σ ρ → record σ { advanceVPT = x } , ρ - } - --- Reference properties - -&cast : ∀ {k m n ls} {Γ : Sets n ls} → .(eq : k ≡ m) → Reference n Γ (Bits k) → Reference n Γ (Bits m) -&cast eq &v = record - { get = λ σ ρ → cast eq (Reference.get &v σ ρ) - ; set = λ x σ ρ → Reference.set &v (cast (sym eq) x) σ ρ - } - -slice : ∀ {k m n ls} {Γ : Sets n ls} → Reference n Γ (Bits m) → Expr n Γ (∃ λ (i : Fin (suc m)) → ∃ λ j → toℕ (i - j) ≡ k) → Reference n Γ (Bits k) -slice &v idx = record - { get = λ σ ρ → let (i , j , i-j≡k) = idx σ ρ in cast i-j≡k (sliceᵇ i j (Reference.get &v σ ρ)) - ; set = λ v σ ρ → - let (i , j , i-j≡k) = idx σ ρ in - Reference.set &v (updateᵇ i j (cast (sym (i-j≡k)) v) (Reference.get &v σ ρ)) σ ρ - } - -elem : ∀ {k n ls} {Γ : Sets n ls} m → Reference n Γ (Bits (k * m)) → Expr n Γ (Fin k) → Reference n Γ (Bits m) -elem m &v idx = slice &v (λ σ ρ → helper _ _ (idx σ ρ)) - where - helper : ∀ m n → Fin m → ∃ λ (i : Fin (suc (m * n))) → ∃ λ j → toℕ (i - j) ≡ n - helper (suc m) n zero = inject+ (m * n) (fromℕ n) , # 0 , eq - where - eq = trans (sym (Finₚ.toℕ-inject+ (m * n) (fromℕ n))) (Finₚ.toℕ-fromℕ n) - helper (suc m) n (suc i) with x , y , x-y≡n ← helper m n i = - u , - v , - trans - (cast‿- (raise n x) (Fin.cast eq₂ (raise n y)) eq₁) - (trans (raise‿- (suc (m * n)) n x y eq₂) x-y≡n) - where - eq₁ = ℕₚ.+-suc n (m * n) - eq₂ = trans (ℕₚ.+-suc n (toℕ x)) (cong suc (sym (Finₚ.toℕ-raise n x))) - eq₂′ = cong suc (sym (Finₚ.toℕ-cast eq₁ (raise n x))) - u = Fin.cast eq₁ (raise n x) - v = Fin.cast eq₂′ (Fin.cast eq₂ (raise n y)) - - raise‿- : ∀ m n (x : Fin m) y .(eq : n + suc (toℕ x) ≡ suc (toℕ (raise n x))) → toℕ (raise n x - Fin.cast eq (raise n y)) ≡ toℕ (x - y) - raise‿- m ℕ.zero x zero _ = refl - raise‿- (suc m) ℕ.zero (suc x) (suc y) p = raise‿- m ℕ.zero x y (ℕₚ.suc-injective p) - raise‿- m (suc n) x y p = raise‿- m n x y (ℕₚ.suc-injective p) - - cast‿- : ∀ {m n} (x : Fin m) y .(eq : m ≡ n) → toℕ (Fin.cast eq x - Fin.cast (cong suc (sym (Finₚ.toℕ-cast eq x))) y) ≡ toℕ (x - y) - cast‿- {suc m} {suc n} x zero eq = Finₚ.toℕ-cast eq x - cast‿- {suc m} {suc n} (suc x) (suc y) eq = cast‿- x y (ℕₚ.suc-injective eq) - --- General functions - -copyMasked : Instr.VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _) -copyMasked dest = - for 4 ( - -- 0:e 1:result 2:beat 3:elmtMask - if ⦇ hasBit (!# 0) (!# 3) ⦈ - then - elem 8 (&Q ⦇ dest ⦈ (!# 2)) (!# 0) ≔ ! elem 8 (var (# 1)) (!# 0) - else skip) - ∙end - -module fun-sliceᶻ - (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ)) - where - - open ShiftNotZero 1<<n≉0 - - signedSatQ : ∀ n → Function 1 (ℤ , _) (Bits (suc n) × Bool) - signedSatQ n = declare ⦇ true ⦈ $ - -- 0:sat 1:x - if ⦇ (λ i → does ((1ℤ << n) ℤ.+ ℤ.- 1ℤ <ᶻ? i)) (!# 1) ⦈ - then - var (# 1) ≔ ⦇ ((1ℤ << n) ℤ.+ ℤ.- 1ℤ) ⦈ - else if ⦇ (λ i → does (ℤ.- 1ℤ << n <ᶻ? i)) (!# 1) ⦈ - then - var (# 1) ≔ ⦇ (ℤ.- 1ℤ << n) ⦈ - else - var (# 0) ≔ ⦇ false ⦈ - ∙return ⦇ ⦇ (sliceᶻ (suc n) zero) (!# 1) ⦈ , (!# 0) ⦈ - -advanceVPT : Procedure 1 (Beat , _) -advanceVPT = declare (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) $ - -- 0:vptState 1:beat - if ⦇ (λ x → does (x ≟ᵇ 1𝔹 ∷ zeros)) (!# 0) ⦈ - then - var (# 0) ≔ ⦇ zeros ⦈ - else if ⦇ (λ x → does (x ≟ᵇ zeros)) (!# 0) ⦈ - then skip - else ( - if ⦇ (hasBit (# 3)) (!# 0) ⦈ - then - elem 4 &VPR-P0 (!# 1) ⟵ (Bits.¬_) - else skip ∙ - (var (# 0) ⟵ λ x → sliceᵇ (# 3) zero x V.++ 0𝔹 ∷ [])) ∙ - if ⦇ (λ x → does (oddeven x Finₚ.≟ # 1)) (!# 1) ⦈ - then - elem 4 &VPR-mask (hilow ∘₂ !# 1) ≔ !# 0 - else skip - ∙end - -execBeats : Procedure 2 (Beat , ElmtMask , _) → Procedure 0 _ -execBeats inst = declare ⦇ ones ⦈ $ - for 4 ( - -- 0:beat 1:elmtMask - if ⦇ (λ x → does (x ≟ᵇ zeros)) (! elem 4 &VPR-mask (hilow ∘₂ !# 0)) ⦈ - then - var (# 1) ≔ ⦇ ones ⦈ - else - var (# 1) ≔ ! elem 4 &VPR-P0 (!# 0) ∙ - &AdvanceVPT ≔ ⦇ true ⦈ ∙ - invoke inst ⦇ !# 0 , !# 1 ⦈ ∙ - if ! &AdvanceVPT - then - invoke advanceVPT (!# 0) - else skip) - ∙end - -module _ - (d : Instr.VecOp₂) - where - - open Instr.VecOp₂ d - - vec-op₂ : Op₂ (Bits (toℕ esize)) → Procedure 2 (Beat , ElmtMask , _) - vec-op₂ op = declare ⦇ zeros ⦈ $ declare (! &Q ⦇ src₁ ⦈ (!# 1)) $ - for (toℕ elements) ( - -- 0:e 1:op₁ 2:result 3:beat 4:elmntMask - elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0) ≔ - (⦇ op - (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0)) - ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈) - , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 3))) (!# 0)) - ]′ src₂) ⦈)) ∙ - invoke (copyMasked dest) ⦇ !# 1 , ⦇ !# 2 , !# 3 ⦈ ⦈ - ∙end - --- Instruction semantics - -module _ - (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ)) - where - - open ShiftNotZero 1<<n≉0 - open fun-sliceᶻ 1<<n≉0 - - vadd : Instr.VAdd → Procedure 2 (Beat , ElmtMask , _) - vadd d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ uint y)) - - vsub : Instr.VSub → Procedure 2 (Beat , ElmtMask , _) - vsub d = vec-op₂ d (λ x y → sliceᶻ _ zero (uint x ℤ.+ ℤ.- uint y)) - - vhsub : Instr.VHSub → Procedure 2 (Beat , ElmtMask , _) - vhsub d = vec-op₂ op₂ (λ x y → sliceᶻ _ (suc zero) (int x ℤ.+ ℤ.- int y)) - where open Instr.VHSub d ; int = Bool.if unsigned then uint else sint - - vmul : Instr.VMul → Procedure 2 (Beat , ElmtMask , _) - vmul d = vec-op₂ d (λ x y → sliceᶻ _ zero (sint x ℤ.* sint y)) - - vmulh : Instr.VMulH → Procedure 2 (Beat , ElmtMask , _) - vmulh d = vec-op₂ op₂ (λ x y → cast (eq _ esize) (sliceᶻ 2esize esize′ (int x ℤ.* int y ℤ.+ rval))) - where - open Instr.VMulH d - int = Bool.if unsigned then uint else sint - rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ - 2esize = toℕ esize + toℕ esize - esize′ = inject+ _ (strengthen esize) - eq : ∀ {n} m (i : Fin n) → toℕ i + m ℕ-ℕ inject+ m (strengthen i) ≡ m - eq m zero = refl - eq m (suc i) = eq m i - - vqdmulh : Instr.VQDMulH → Procedure 2 (Beat , ElmtMask , _) - vqdmulh d = declare ⦇ zeros ⦈ $ declare (! &Q ⦇ src₁ ⦈ (!# 1)) $ declare ⦇ false ⦈ $ - for (toℕ elements) ( - -- 0:e 1:sat 2:op₁ 3:result 4:beat 5:elmntMask - elem (toℕ esize) (&cast (sym e*e≡32) (var (# 3))) (!# 0) ,′ var (# 1) ≔ - call (signedSatQ (toℕ esize-1)) - ⦇ (λ x y → (2ℤ ℤ.* sint x ℤ.* sint y ℤ.+ rval) >> toℕ esize) - (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0)) - ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈) - , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 4))) (!# 0)) - ]′ src₂) ⦈ ∙ - if !# 1 - then if ⦇ (λ m e → hasBit (combine e zero) (cast (sym e*e>>3≡4) m)) (!# 5) (!# 0) ⦈ - then - &FPSCR-QC ≔ ⦇ 1𝔹 ⦈ - else skip - else skip) ∙ - invoke (copyMasked dest) ⦇ !# 2 , ⦇ !# 3 , !# 4 ⦈ ⦈ - ∙end - where - open Instr.VQDMulH d - rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ - - ⟦_⟧₁ : Instr.Instruction → Procedure 0 _ - ⟦ Instr.vadd x ⟧₁ = execBeats (vadd x) - ⟦ Instr.vsub x ⟧₁ = execBeats (vsub x) - ⟦ Instr.vmul x ⟧₁ = execBeats (vmul x) - ⟦ Instr.vmulh x ⟧₁ = execBeats (vmulh x) - ⟦ Instr.vqdmulh x ⟧₁ = execBeats (vqdmulh x) - - open List using (List; []; _∷_) - - ⟦_⟧ : List (Instr.Instruction) → Procedure 0 _ - ⟦ [] ⟧ = skip ∙end - ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ invoke ⟦ is ⟧ ⦇ _ ⦈ ∙end diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda deleted file mode 100644 index 9b6a3c8..0000000 --- a/src/Helium/Semantics/Denotational/Core.agda +++ /dev/null @@ -1,128 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Base definitions for the denotational semantics. ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -module Helium.Semantics.Denotational.Core - {ℓ′} - (State : Set ℓ′) - where - -open import Algebra.Core -open import Data.Bool as Bool using (Bool) -open import Data.Fin hiding (lift) -open import Data.Nat using (ℕ; zero; suc) -import Data.Nat.Properties as ℕₚ -open import Data.Product hiding (_<*>_; _,′_) -open import Data.Product.Nary.NonDependent -open import Data.Sum using (_⊎_; inj₁; inj₂; fromInj₂; [_,_]′) -open import Data.Unit using (⊤) -open import Level renaming (suc to ℓsuc) hiding (zero) -open import Function using (_∘_; _∘₂_; _|>_) -open import Function.Nary.NonDependent.Base -open import Relation.Nullary.Decidable using (True) - -private - variable - ℓ ℓ₁ ℓ₂ : Level - τ τ′ : Set ℓ - - update : ∀ {n ls} {Γ : Sets n ls} i → Projₙ Γ i → Product⊤ n Γ → Product⊤ n Γ - update zero y (_ , xs) = y , xs - update (suc i) y (x , xs) = x , update i y xs - -Expr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) -Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ - -record Reference n {ls} (Γ : Sets n ls) (τ : Set ℓ) : Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) where - field - get : Expr n Γ τ - set : τ → Expr n Γ (State × Product⊤ n Γ) - -Function : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) -Function n Γ τ = Expr n Γ τ - -Procedure : ∀ n {ls} → Sets n ls → Set (⨆ n ls ⊔ ℓ′) -Procedure n Γ = Expr n Γ State - -Statement : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) -Statement n Γ τ = Expr n Γ (State × (Product⊤ n Γ ⊎ τ)) - --- Expressions - -pure : ∀ {n ls} {Γ : Sets n ls} → τ → Expr n Γ τ -pure v σ ρ = v - -_<*>_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (τ → τ′) → Expr n Γ τ → Expr n Γ τ′ -_<*>_ f e σ ρ = f σ ρ |> λ f → f (e σ ρ) - -!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ -! r = Reference.get r - -call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ -call f e σ ρ = e σ ρ |> toProduct⊤ _ |> f σ - -declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Expr (suc n) (τ , Γ) τ′ → Expr n Γ τ′ -declare e s σ ρ = e σ ρ |> _, ρ |> s σ - --- References - -var : ∀ {n ls} {Γ : Sets n ls} i → Reference n Γ (Projₙ Γ i) -var i = record - { get = λ σ ρ → projₙ _ i (toProduct _ ρ) - ; set = λ v → curry (map₂ (update i v)) - } - -!#_ : ∀ {n ls} {Γ : Sets n ls} m {m<n : True (suc m ℕₚ.≤? n)} → Expr n Γ (Projₙ Γ (#_ m {n} {m<n})) -(!# m) {m<n} = ! var (#_ m {m<n = m<n}) - -_,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ′ → Reference n Γ (τ × τ′) -&x ,′ &y = record - { get = λ σ ρ → Reference.get &x σ ρ , Reference.get &y σ ρ - ; set = λ (x , y) σ ρ → uncurry (Reference.set &y y) (Reference.set &x x σ ρ) - } - --- Statements - -infixl 1 _∙_ _∙return_ -infix 1 _∙end -infixl 2 if_then_else_ -infix 4 _≔_ _⟵_ - -skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ -skip σ ρ = σ , inj₁ ρ - -invoke : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Procedure m Γ → Expr n Δ (Product m Γ) → Statement n Δ τ -invoke f e σ ρ = call f e σ ρ |> _, inj₁ ρ - -_≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′ -(&x ≔ e) σ ρ = e σ ρ |> λ x → Reference.set &x x σ ρ |> map₂ inj₁ - -_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′ -&x ⟵ e = &x ≔ ⦇ e (! &x) ⦈ - -if_then_else_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Bool → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ -(if e then b₁ else b₂) σ ρ = e σ ρ |> (Bool.if_then b₁ σ ρ else b₂ σ ρ) - -for : ∀ {n ls} {Γ : Sets n ls} m → Statement (suc n) (Fin m , Γ) τ → Statement n Γ τ -for zero b σ ρ = σ , inj₁ ρ -for (suc m) b σ ρ with b σ (zero , ρ) -... | σ′ , inj₂ x = σ′ , inj₂ x -... | σ′ , inj₁ (_ , ρ′) = for m b′ σ′ ρ′ - where - b′ : Statement (suc _) (Fin m , _) _ - b′ σ (i , ρ) with b σ (suc i , ρ) - ... | σ′ , inj₂ x = σ′ , inj₂ x - ... | σ′ , inj₁ (_ , ρ′) = σ′ , inj₁ (i , ρ′) - -_∙_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ -(b₁ ∙ b₂) σ ρ = b₁ σ ρ |> λ (σ , ρ⊎x) → [ b₂ σ , (σ ,_) ∘ inj₂ ]′ ρ⊎x - -_∙end : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ ⊤ → Procedure n Γ -_∙end s σ ρ = s σ ρ |> proj₁ - -_∙return_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Expr n Γ τ → Function n Γ τ -(s ∙return e) σ ρ = s σ ρ |> λ (σ , ρ⊎x) → fromInj₂ (e σ) ρ⊎x |