fixed

commit 2217c94f454868508766bc7142ff385a704debeb
parent 2d8d28f3441bbf97d4329da974e7249e6773ec9e
Author: Jared Tobin <jared@jtobin.io>
Date:   Wed, 22 Jan 2025 13:07:15 +0400

test: passing mul_c, umul_hop, umul_step

Diffstat:
M
test/Main.hs
 | 
40
+++++++++++++++++++++++++++++++++++++---

1 file changed, 37 insertions(+), 3 deletions(-)
diff --git a/test/Main.hs b/test/Main.hs
@@ -1,7 +1,10 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE BangPatterns #-}
 
 module Main where
 
+import Data.Bits ((.|.), (.&.), (.<<.), (.>>.))
+import Data.Word (Word64)
 import Data.Word.Extended
 import Test.Tasty
 import qualified Test.Tasty.QuickCheck as Q
@@ -26,11 +29,33 @@ instance (Q.Arbitrary a, Ord a) => Q.Arbitrary (Monotonic a) where
 
 -- properties -----------------------------------------------------------------
 
+mul_c_matches :: Word64 -> Word64 -> Bool
+mul_c_matches a b =
+  let c = fi a * fi b :: Integer
+      c_hi = fi (c .>>. 64) :: Word64
+      c_lo = fi (c .&. 0xffffffffffffffff) :: Word64
+
+      W64P hi lo = mul_c a b
+  in  hi == c_hi && lo == c_lo
+
+-- (hi * 2 ^ 64 + lo) = z + (x * y)
+umul_hop_predicate_holds :: Word64 -> Word64 -> Word64 -> Bool
+umul_hop_predicate_holds z x y =
+  let !(W64P hi lo) = umul_hop z x y
+  in  fi hi * 2 ^ (64 :: Int) + fi lo == (fi z + (fi x * fi y) :: Integer)
+
+-- (hi * 2 ^ 64 + lo) = z + (x * y) + c
+umul_step_predicate_holds :: Word64 -> Word64 -> Word64 -> Word64 -> Bool
+umul_step_predicate_holds z x y c =
+  let !(W64P hi lo) = umul_step z x y c
+      !left = fi hi * 2 ^ (64 :: Int) + fi lo :: Integer
+      !rite = fi z + (fi x * fi y) + fi c :: Integer
+  in  left == rite
+
 to_word256_inverts_to_integer :: Word256 -> Bool
 to_word256_inverts_to_integer w256 =
   to_word256 (to_integer w256) == w256
 
--- doesn't hold for negative inputs
 to_integer_inverts_to_word256 :: Q.NonNegative Integer -> Bool
 to_integer_inverts_to_word256 (Q.NonNegative n) =
   to_integer (to_word256 n) == n
@@ -43,7 +68,6 @@ subtraction_matches :: Monotonic (Q.NonNegative Integer) -> Bool
 subtraction_matches (Monotonic (Q.NonNegative a, Q.NonNegative b)) =
   to_integer (to_word256 a `sub` to_word256 b) == a - b
 
-
 -- main -----------------------------------------------------------------------
 
 inverses :: TestTree
@@ -62,10 +86,20 @@ arithmetic = testGroup "arithmetic" [
       Q.withMaxSuccess 1000 subtraction_matches
   ]
 
+utils :: TestTree
+utils = testGroup "utils" [
+    Q.testProperty "mul_c matches integer multiplication" $
+      Q.withMaxSuccess 1000 mul_c_matches
+  , Q.testProperty "umul_hop: (hi * 2 ^ 64 + lo) = z + (x * y)" $
+      Q.withMaxSuccess 1000 umul_hop_predicate_holds
+  , Q.testProperty "umul_step: (hi * 2 ^ 64 + lo) = z + (x * y) + c" $
+      Q.withMaxSuccess 1000 umul_step_predicate_holds
+  ]
 
 main :: IO ()
 main = defaultMain $ testGroup "ppad-fw" [
-    inverses
+    utils
+  , inverses
   , arithmetic
   ]