From d00c4d301f2995ac40a011b711f2c16526e188b8 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Sun, 13 Feb 2022 15:28:51 +0000
Subject: Write pseudocode definition of Barrett reduction

---
 src/Helium/Instructions/Instances/Barrett.agda | 46 ++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 src/Helium/Instructions/Instances/Barrett.agda

(limited to 'src/Helium/Instructions/Instances')

diff --git a/src/Helium/Instructions/Instances/Barrett.agda b/src/Helium/Instructions/Instances/Barrett.agda
new file mode 100644
index 0000000..5ec9ba4
--- /dev/null
+++ b/src/Helium/Instructions/Instances/Barrett.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Implementation of Barrett reduction.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+module Helium.Instructions.Instances.Barrett where
+
+open import Data.Bool using (false)
+open import Data.Sum using (inj₁)
+open import Data.Vec using ([])
+open import Data.Vec.Relation.Unary.All using ([])
+open import Helium.Instructions.Base
+open import Helium.Instructions.Core
+
+-- Given:
+--   m     = ⌊ (1 << l) * n⁻¹ ⌋
+--   -n    = n
+--   n     < 2 ^ 32
+--   | z | < 2 ^ 31
+-- Computes:
+--   z mod n
+barret : (m -n : Expression [] (bits 32)) (t z : VecReg) (im : GenReg) → Procedure []
+barret m -n t z im =
+  index R (lit (im ′f)) ≔ m ∙
+  invoke vqrdmulh-s32,t,z,m (tup []) ∙
+  index R (lit (im ′f)) ≔ -n ∙
+  invoke vmla-s32,z,t,-n (tup []) ∙end
+  where
+  vqrdmulh-s32,t,z,m =
+    ExecBeats (vqrdmulh (record
+      { size = 32bit
+      ; dest = t
+      ; src₁ = z
+      ; src₂ = inj₁ im
+      }))
+  vmla-s32,z,t,-n =
+    ExecBeats (vmla (record
+      { size     = 32bit
+      ; unsigned = false
+      ; acc      = z
+      ; src₁     = t
+      ; src₂     = im
+      }))
-- 
cgit v1.2.3