1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
|
{-# OPTIONS --safe --without-K #-}
open import Helium.Data.Pseudocode
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 Data.Fin as Fin hiding (cast; lift; _+_)
import Data.Fin.Properties as Finₚ
open import Data.Maybe using (just; nothing; _>>=_)
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.Nary.NonDependent.Base
open import Helium.Instructions
import Helium.Semantics.Denotational.Core as Core
open import Level hiding (lift; zero; suc)
open import Relation.Binary using (Transitive)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
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
open Core State
Beat : Set
Beat = Fin 4
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 = λ σ ρ → e σ ρ >>= λ (σ , i) → just (σ , State.R σ i)
; set = λ σ ρ x → e σ ρ >>= λ (σ , i) → just (record σ { R = V.updateAt i (λ _ → x) (State.R σ) } , ρ)
}
&S : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 32) → Reference n Γ (Bits 32)
&S e = record
{ get = λ σ ρ → e σ ρ >>= λ (σ , i) → just (σ , State.S σ i)
; set = λ σ ρ x → e σ ρ >>= λ (σ , i) → just (record σ { S = V.updateAt i (λ _ → x) (State.S σ) } , ρ)
}
&Q : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ VecReg → Expr n Γ Beat → Reference n Γ (Bits 32)
&Q reg beat = &S (λ σ ρ → reg σ ρ >>= λ (σ , reg) → beat σ ρ >>= λ (σ , beat) → just (σ , combine reg beat))
-- 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 = λ σ ρ → Reference.get &v σ ρ >>= λ (σ , v) → just (σ , cast eq 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 = λ σ ρ → Reference.get &v σ ρ >>= λ (σ , v) → idx σ ρ >>= λ (σ , i , j , i-j≡k) → just (σ , cast i-j≡k (sliceᵇ i j v))
; set = λ σ ρ v → Reference.get &v σ ρ >>= λ (σ , v′) → idx σ ρ >>= λ (σ , i , j , i-j≡k) → Reference.set &v σ ρ (updateᵇ i j (cast (sym i-j≡k) v) 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 λ σ ρ → idx σ ρ >>= λ (σ , i) → just (σ , helper _ _ i)
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)
-- Instruction semantics
module _
(≈ᶻ-trans : Transitive _≈ᶻ_)
(round∘⟦⟧ : ∀ x → x ≈ᶻ round ⟦ x ⟧)
(round-cong : ∀ {x y} → x ≈ʳ y → round x ≈ᶻ round y)
(0#-homo-round : round 0ℝ ≈ᶻ 0ℤ)
(2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ))
(*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
where
open sliceᶻ ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 *ᶻ-identityʳ
vadd : VAdd.VAdd → Procedure 2 (Beat , ElmtMask , _)
vadd d = declare ⦇ zeros ⦈ (declare (! &Q ⦇ src₁ ⦈ (!# 1)) (label λ
result op₁ beat elmtMask →
[ (λ src₂ → for (toℕ elements) (lift (
elem (toℕ esize) (&cast (sym e*e≡32) (wknRef result)) (!# 0) ≔
⦇ ! elem (toℕ esize) (&cast (sym e*e≡32) (wknRef op₁)) (!# 0) +ᵇ
! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈ ⦈)) )
, (λ src₂ → declare (! &Q ⦇ src₂ ⦈ (! beat)) (for (toℕ elements) (lift (
elem (toℕ esize) (&cast (sym e*e≡32) (wknRef (wknRef result))) (!# 0) ≔
⦇ ! elem (toℕ esize) (&cast (sym e*e≡32) (wknRef (wknRef op₁))) (!# 0) +ᵇ
! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 1))) (!# 0) ⦈))))
]′ src₂ ∙
for 4 (lift (
if ⦇ (λ x y → does (getᵇ y x ≟ᵇ 1b)) (! wknRef elmtMask) (!# 0) ⦈
then
elem 8 (&Q ⦇ dest ⦈ (! wknRef beat)) (!# 0) ≔ (! elem 8 (wknRef result) (!# 0))
else
skip))))
where
open VAdd.VAdd d
esize = VAdd.esize d
elements = VAdd.elements d
e*e≡32 = VAdd.elem*esize≡32 d
|
