chore: cleanup, add sqrt impl

Author: bollu

Fp.lean

@@ -5,7 +5,7 @@ import Fp.Division
 import Fp.FMA
 import Fp.Multiplication
 import Fp.Negation
-import Fp.Remainder
+-- import Fp.Remainder
 import Fp.Rounding
 import Fp.Sqrt
 import Fp.Subtraction

Fp/Remainder.lean

@@ -3,19 +3,6 @@ import Fp.Rounding
 import Fp.Division
 import Fp.UnpackedRound
 
-def UnpackedFloat.remainder (a b : UnpackedFloat e s) : UnpackedFloat e s :=
-  let rnd := a.div b
-  let rne := rnd.round .RNE
-  sorry
-
-def EUnpackedFloat.remainder 
-    (a b : EUnpackedFloat (exponentWidth e s) (s + 1)) (rm : RoundingMode) :
-    EUnpackedFloat (exponentWidth e s) (s + 1) := 
-  if a.isNaN || b.isNaN || a.isInfinite || b.isZero then .mkNaN
-  else if a.isZero || b.isInfinite then a 
-  else 
-    let uf := UnpackedFloat.remainder a.num b.num
-    uf.round rm
 
 @[bv_normalize]
 def remainderFixed (a b : PackedFloat e s) : PackedFloat e s :=
@@ -60,4 +47,4 @@ def remainderFixed (a b : PackedFloat e s) : PackedFloat e s :=
     EFixedPoint.round e s .RTZ result
 
 /-- info: { sign := -, ex := 0x00#5, sig := 0x1#2 } -/
-#guard_msgs in #eval remainder (PackedFloat.ofBits 5 2 0b00000011) (PackedFloat.ofBits 5 2 0b00000100)
+#guard_msgs in #eval remainderFixed (PackedFloat.ofBits 5 2 0b00000011) (PackedFloat.ofBits 5 2 0b00000100)

Fp/Tests/ExhaustiveEnumerationRat.lean

@@ -5,6 +5,7 @@ import Fp.Basic
 import Fp.Addition
 import Fp.Multiplication
 import Fp.Division
+import Fp.Sqrt
 import Fp.Tests.PackedFloatEnumeration
 
 namespace Fp
@@ -172,5 +173,32 @@ def testDiv (ein sin : Nat) : IO (UnpackedRatTestSummary ein sin) := do
       results := results.push result
   return summarizeUnpackedRatTestResults "div" results
 
+/--
+Compute a rational approximation of sqrt(r) using Newton's method.
+-/
+def ratSqrt (r : Rat) (iters : Nat := 20) : Rat :=
+  if r ≤ 0 then 0
+  else Id.run do
+    let mut x : Rat := r
+    for _ in [:iters] do
+      x := (x + r / x) / 2
+    return x
+
+/--
+Produce the results from taking the square root of all packed floats
+for the given exponent and significand sizes.
+-/
+def testSqrt (ein sin : Nat) : IO (UnpackedRatTestSummary ein sin) := do
+  let mut results : Array (UnpackedRatTestResult ein sin) := #[]
+  let enum : PackedFloatEnumeration ein sin := PackedFloatEnumeration.mk ein sin
+  for (pf, r) in enum.enumeration do
+    if r ≤ 0 then continue
+    let uf := pf.unpack.num
+    let produced := UnpackedFloat.sqrt uf
+    let expected := ratSqrt r
+    let result := UnpackedRatTestResult.mk (Array.mk [(pf, r)]) produced expected
+    results := results.push result
+  return summarizeUnpackedRatTestResults "sqrt" results
+
 end ExhaustiveEnumerationRat
 end Fp

Main.lean

@@ -1,4 +1,5 @@
 import Fp
+import Fp.Remainder
 import Fp.Tests
 
 structure OpResult where
@@ -141,7 +142,7 @@ def test_rem (f : FP8Format) (m : RoundingMode) (a b : BitVec 8) : OpResult :=
   {
     oper := "rem"
     mode := m
-    result := [a, b, f.h.mp (remainder a' b').toBits'].map toDigits
+    result := [a, b, f.h.mp (remainderFixed a' b').toBits'].map toDigits
   }
 
 def test_binop (f : RoundingMode → BitVec 8 → BitVec 8 → OpResult) : Thunk (List OpResult) :=
@@ -275,6 +276,7 @@ def get_long_operation (args : List String) : IO Unit := do
   | ["addRat"] => IO.println (← Fp.ExhaustiveEnumerationRat.testAdd 3 4).toFormat
   | ["mulRat"] => IO.println (← Fp.ExhaustiveEnumerationRat.testMul 3 4).toFormat
   | ["divRat"] => IO.println (← Fp.ExhaustiveEnumerationRat.testDiv 3 4).toFormat
+  | ["sqrtRat"] => IO.println (← Fp.ExhaustiveEnumerationRat.testSqrt 3 4).toFormat
   | ["roundCircuitAgainstSmtLib"] =>
       test_roundCircuitAgainstSmtlib (ein := 3) (sin := 6) (eout := 3) (sout := 4)
       test_roundCircuitAgainstSmtlib (ein := 3) (sin := 6) (eout := 3) (sout := 4)