From e947c8ef6c844b612e7aec9670f67d00008661e3 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Wed, 2 Feb 2022 14:18:34 +0000
Subject: Define pseudocode for a number of instructions.

---
 src/Helium/Semantics/Denotational.agda | 310 ---------------------------------
 1 file changed, 310 deletions(-)
 delete mode 100644 src/Helium/Semantics/Denotational.agda

(limited to 'src/Helium/Semantics/Denotational.agda')

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
-- 
cgit v1.2.3