feat: Build theory around unpacking and multiplication

Fp/Multiplication.lean

@@ -4,18 +4,24 @@ import Fp.Rounding
 
 @[bv_normalize]
 def UnpackedFloat.mul (x y : UnpackedFloat e s) : UnpackedFloat (e + 1) (2 * s) :=
-  let sigProd := x.sig.setWidth' (by omega) * y.sig.setWidth' (by omega)
   {
-    sign := x.sign ^^ y.sign
+    sign := sign
     -- Exponent guaranteed to fit in e+1 bits (no overflow):
     -- max: (2^(e-1) - 1) + (2^(e-1) - 1) + 1 = 2^e - 1 < 2^e
     -- min: -2^(e-1) + -2^(e-1) + 0 = -2^e
     -- Optimization: consider using `Bitvec.adc`
-    ex := x.ex.signExtend (e + 1) + y.ex.signExtend (e + 1) + (BitVec.ofBool sigProd.msb).setWidth' (by omega)
+    ex := ex
     -- If product in range [2,4) (i.e., 1x...x), then it is already normalized.
     -- If product in range [1,2) (i.e., 01x..x), then normalize by shifting left once.
-    sig := sigProd <<< BitVec.ofBool !sigProd.msb
+    sig := sig
   }
+  where
+    -- use 'where' blocks since they create auxiliary defs which can be neatly unfolded.
+    sigProd := x.sig.setWidth' (by omega) * y.sig.setWidth' (by omega)
+    sig := sigProd <<< BitVec.ofBool !sigProd.msb
+    -- | why does this not overflow? when `sigProd.msb` is `true`?
+    ex := x.ex.signExtend (e + 1) + y.ex.signExtend (e + 1) + (BitVec.ofBool sigProd.msb).setWidth' (by omega)
+    sign := x.sign ^^ y.sign
 
 @[bv_normalize]
 def EUnpackedFloat.mul (m : RoundingMode) (x y : EUnpackedFloat (exponentWidth e s) (s + 1))
@@ -41,8 +47,6 @@ instance : Mul (PackedFloat e s) where
 @[bv_normalize]
 theorem PackedFloat.mul_def {x y : PackedFloat e s} : x * y = PackedFloat.mul .RNE x y := rfl
 
-
-
 end PackedFloat
 
 /-- info: some 16 -/

Fp/Packing.lean

@@ -1,7 +1,11 @@
 import Fp.Basic
 
+/--
+Convert a packed float into an 'UnpackedFloat',
+ignoring the possibility that it could be NaN/± infinity.
+-/
 @[bv_normalize]
-def PackedFloat.unpackNormOrNonzeroSubnorm (pf : PackedFloat e s) :
+def PackedFloat.unpackNum (pf : PackedFloat e s) :
   UnpackedFloat (exponentWidth e s) (s + 1) :=
   if pf.isNorm then
     {
@@ -26,12 +30,12 @@ then we know that the unpacked version of it is also not zero. This is a useful
 -/
 @[simp, grind! →]
 axiom PackedFloat.unpackNormOrNonzeroSubnorm_isZero_eq_of_not_isZero (pf : PackedFloat e s) (hpf : ¬ pf.isZero := by grind) :
-  pf.unpackNormOrNonzeroSubnorm.isZero = false
+  pf.unpackNum.isZero = false
 
 @[simp]
 theorem PackedFloat.sign_unpackNormOrNonzeroSubnorm_eq_sign (pf : PackedFloat e s) :
-    pf.unpackNormOrNonzeroSubnorm.sign = pf.sign := by
-  simp [PackedFloat.unpackNormOrNonzeroSubnorm]
+    pf.unpackNum.sign = pf.sign := by
+  simp [unpackNum]
   by_cases hpf : pf.isNorm <;> simp [hpf]
 
 
@@ -44,7 +48,7 @@ def PackedFloat.unpack (pf : PackedFloat e s)
     EUnpackedFloat.mkInfinity pf.sign
   else bif pf.isZero then
     EUnpackedFloat.mkZero pf.sign
-  else EUnpackedFloat.mkNumber (pf.unpackNormOrNonzeroSubnorm)
+  else EUnpackedFloat.mkNumber (pf.unpackNum)
 
 @[simp, grind! .]
 theorem PackedFloat.isNaN_unpack_eq_isNaN (pf : PackedFloat e s) :
@@ -75,6 +79,23 @@ theorem PackedFloat.isZero_unpack_eq_isZero (pf : PackedFloat e s) :
     · by_cases hzero : pf.isZero <;> simp [hzero]
 
 
+@[simp, grind =]
+theorem PackedFloat.unpack_eq_unpackNum_of (pf : PackedFloat e s)
+    (hpf : pf.isNormOrNonzeroSubnorm) :
+     pf.unpack = EUnpackedFloat.mkNumber pf.unpackNum := by
+  unfold unpack
+  grind
+
+/-- Unpacking a packed float always results in a normalized float. -/
+@[simp, grind =]
+theorem PackedFloat.msb_unpackNum_eq_true {pf : PackedFloat e s}
+    (hpf : pf.isNormOrNonzeroSubnorm) :
+    pf.unpackNum.sig.msb = true := by
+  simp only [unpackNum, BitVec.truncate_eq_setWidth]
+  by_cases hf : pf.isNorm <;> simp only [hf, ↓reduceIte, BitVec.msb_cons]
+  have : pf.sig ≠ 0#s := by grind
+  simp [this]
+
 
 @[bv_normalize]
 def EUnpackedFloat.pack (uf : EUnpackedFloat (exponentWidth e s) (s + 1))
@@ -108,8 +129,8 @@ attribute [bv_normalize] BitVec.zero
 
 @[simp]
 theorem PackedFloat.unpack_eq_mkNumber_of_isNormOrNonzeroSubnorm
-  {pf : PackedFloat e s} (hpf : pf.isNormOrNonzeroSubnorm) :
-    pf.unpack = EUnpackedFloat.mkNumber pf.unpackNormOrNonzeroSubnorm := by
+  {pf : PackedFloat e s} (hpf : pf.isNormOrNonzeroSubnorm := by solve | simp | grind) :
+    pf.unpack = EUnpackedFloat.mkNumber pf.unpackNum := by
   have hnan : ¬ pf.isNaN := by grind
   have hinf : ¬ pf.isInfinite := by grind
   have hzero : ¬ pf.isZero := by grind

Fp/Remainder.lean

@@ -36,7 +36,7 @@ def remainderFixed (a b : PackedFloat e s) : PackedFloat e s :=
         num := {
           sign := a.sign ^^ remSign
           val := val.setWidth _ <<< bshift
-          hExOffset := by
+          hPrec := by
             have hexp0 : 0 < 2^e := Nat.two_pow_pos _
             have hexp1 : 2^(e-1) ≤ 2^e := two_pow_sub_one_le_two_pow e
             omega

Fp/Rounding.lean

@@ -309,7 +309,7 @@ def roundToInt (mode : RoundingMode) (x : PackedFloat e s) : PackedFloat e s :=
       num := {
         sign := x.sign
         val := integral
-        hExOffset := by
+        hPrec := by
           have h := Nat.two_pow_pos e
           omega
       }
@@ -331,7 +331,7 @@ def ofRat (e s : Nat) (mode : RoundingMode) (num : Int) (den : Nat) : PackedFloa
       num := {
         sign := num < 0
         val := BitVec.ofNat width quot
-        hExOffset := by
+        hPrec := by
           have hexp0 : 0 < 2^e := Nat.two_pow_pos _
           have hexp1 : 2^(e-1) ≤ 2^e := two_pow_sub_one_le_two_pow e
           omega

Fp/Theorems.lean

@@ -2,3 +2,4 @@ import Fp.Theorems.Basic
 import Fp.Theorems.Packing
 import Fp.Theorems.SmtLibSemanticsQ
 import Fp.Theorems.UnpackedRound
+import Fp.Theorems.Multiplication