fixed

Pure Haskell large fixed-width integers.
git clone git://git.ppad.tech/fixed.git
Log | Files | Refs | README | LICENSE

commit efed000cc004a1ab568e3e12226f3daced7f385d
parent 9c417daa84b3c054aa0787da3782c3cdcb29df93
Author: Jared Tobin <jared@jtobin.io>
Date:   Tue, 28 Jan 2025 21:06:31 +0400

lib: yet another optimising wip

Diffstat:
Mbench/Main.hs | 75++++++++++++++++++++++++++++++++++++++-------------------------------------
Mbench/Weight.hs | 13++-----------
Mlib/Data/Word/Extended.hs | 416++++++++++++++++++++++++++++++++++++-------------------------------------------
Mtest/Main.hs | 57++++++++++++++++++++++++++-------------------------------
4 files changed, 254 insertions(+), 307 deletions(-)

diff --git a/bench/Main.hs b/bench/Main.hs @@ -23,7 +23,12 @@ multiplication = bgroup "multiplication" [ ] division = bgroup "division" [ - quotrem_by1 + div + , div_baseline + , mod + , mod_baseline + , recip_2by1 + , quotrem_by1 , rem_by1 , quotrem_2by1 , quot_r @@ -87,6 +92,10 @@ quot_r :: Benchmark quot_r = bench "quot_r" $ nf (W.quot_r 4 0xffffffffffffffff) (B.complement 4) +recip_2by1 :: Benchmark +recip_2by1 = bench "recip_2by1" $ + nf W.recip_2by1 0xFFFF_FFFF_FFFF_FF00 + quotrem_2by1 :: Benchmark quotrem_2by1 = bench "quotrem_2by1" $ nf (W.quotrem_2by1 8 4 0xFFFF_FFFF_FFFF_FF00) r @@ -96,7 +105,7 @@ quotrem_2by1 = bench "quotrem_2by1" $ quotrem_by1 :: Benchmark quotrem_by1 = env setup $ \ ~(q, u, d) -> bench "quotrem_by1" $ - nfIO (W.quotrem_by1 q u d) + nfAppIO (W.quotrem_by1 q u) d where setup = do qm <- PA.newPrimArray 2 @@ -109,6 +118,32 @@ rem_by1 :: Benchmark rem_by1 = bench "rem_by1" $ nf (W.rem_by1 (PA.primArrayFromList [4, 8])) (B.complement 0xFF :: Word64) +div_baseline :: Benchmark +div_baseline = bench "div (baseline)" $ nf (Prelude.div w0) w1 where + w0, w1 :: Integer + !w0 = 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a + !w1 = 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 + +div :: Benchmark +div = bench "div" $ nf (W.div w0) w1 where + !w0 = W.to_word256 + 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a + !w1 = W.to_word256 + 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 + +mod_baseline :: Benchmark +mod_baseline = bench "mod (baseline)" $ nf (Prelude.rem w0) w1 where + w0, w1 :: Integer + !w0 = 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a + !w1 = 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 + +mod :: Benchmark +mod = bench "mod" $ nf (W.mod w0) w1 where + !w0 = W.to_word256 + 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a + !w1 = W.to_word256 + 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 + -- quotrem_by1_case0 :: H.Assertion -- quotrem_by1_case0 = do @@ -171,41 +206,7 @@ rem_by1 = bench "rem_by1" $ -- mul128 = bench "mul128" $ nf (W.mul w0) w1 where -- !w0 = W.to_word256 0x7fffffffffffffffffffffffffffffed -- !w1 = W.to_word256 0x7ffffffffffffffbffffffffffffffed --- --- div_baseline :: Benchmark --- div_baseline = bench "div (baseline)" $ nf (Prelude.div w0) w1 where --- w0, w1 :: Integer --- !w0 = 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a --- !w1 = 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 --- --- div :: Benchmark --- div = bench "div" $ nf (W.div w0) w1 where --- !w0 = W.to_word256 --- 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a --- !w1 = W.to_word256 --- 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 --- --- div_baseline_small :: Benchmark --- div_baseline_small = --- bench "div, small (baseline)" $ nf (Prelude.div w0) w1 --- where --- w0, w1 :: Integer --- !w0 = 0x7fffffed --- !w1 = 0x7ffbffed --- --- mod_baseline :: Benchmark --- mod_baseline = bench "mod (baseline)" $ nf (Prelude.rem w0) w1 where --- w0, w1 :: Integer --- !w0 = 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a --- !w1 = 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 --- --- mod :: Benchmark --- mod = bench "mod (pure)" $ nf (W.mod w0) w1 where --- !w0 = W.to_word256 --- 0x41cf50c7d0d65afabcf5ba37750dba71c7db29ec9f20a216d3ef013a59b9188a --- !w1 = W.to_word256 --- 0x066bd4c3c10e30260cb6e7832af25f15527b089b258a1fef13b6eec3ce73bf06 --- + -- arithmetic :: Benchmark -- arithmetic = bgroup "arithmetic" [ -- add diff --git a/bench/Weight.hs b/bench/Weight.hs @@ -36,17 +36,8 @@ main = W.mainWith $ do W.func "mul" (E.mul w0) w1 W.func "quotrem_r" (E.quotrem_r 4 0xffffffffffffffff) (B.complement 4) W.func "quotrem_2by1" (E.quotrem_2by1 8 4 0xffffffffffffffff) r + W.func "div (baseline)" (Prelude.div i2) i3 + W.func "div" (E.div w2) w3 where !r = E.recip_2by1 0xFFFF_FFFF_FFFF_FF00 --- main :: IO () --- main = W.mainWith $ do --- W.func "add (baseline)" ((+) i0) i1 --- W.func "add" (E.add w0) w1 --- W.func "sub (baseline)" ((-) i0) i1 --- W.func "sub" (E.sub w0) w1 --- W.func "mul (baseline)" ((*) i0) i1 --- W.func "mul" (E.mul w0) w1 --- W.func "div (baseline)" (Prelude.div i2) i3 --- W.func "div" (E.div w2) w3 - diff --git a/lib/Data/Word/Extended.hs b/lib/Data/Word/Extended.hs @@ -642,73 +642,122 @@ rem_by1 u d = do !hl = PA.indexPrimArray u (l - 1) loop (l - 2) hl --- quotrem --- :: PrimMonad m --- => PA.MutablePrimArray (PrimState m) Word64 -- quotient (potentially large) --- -> PA.PrimArray Word64 -- dividend (potentially large) --- -> Word256 -- divisor (256-bit) --- -> m (PA.PrimArray Word64) -- remainder (256-bit) --- quotrem quo u (Word256 d0 d1 d2 d3) = do --- let -- normalize divisor --- (dlen, shift) --- | d3 /= 0 = (4, B.countLeadingZeros d3) --- | d2 /= 0 = (3, B.countLeadingZeros d2) --- | d1 /= 0 = (2, B.countLeadingZeros d1) --- | otherwise = (1, B.countLeadingZeros d0) -- zero not checked --- dn_3 = (d3 .<<. shift) .|. (d2 .>>. (64 - shift)) --- dn_2 = (d2 .<<. shift) .|. (d1 .>>. (64 - shift)) --- dn_1 = (d1 .<<. shift) .|. (d0 .>>. (64 - shift)) --- dn_0 = d0 .<<. shift --- !dn = Word256 dn_0 dn_1 dn_2 dn_3 --- -- get size of normalized dividend --- lu = PA.sizeofPrimArray u --- ulen = let loop !j --- | j < 0 = 0 --- | PA.indexPrimArray u j /= 0 = j + 1 --- | otherwise = loop (j - 1) --- in loop (lu - 1) --- if ulen < dlen --- then do --- -- u always has size at least 4 --- !r <- PA.newPrimArray 4 --- PA.copyPrimArray r 0 u 0 4 --- PA.unsafeFreezePrimArray r --- else do --- -- normalize dividend --- !un <- PA.newPrimArray (ulen + 1) --- PA.setPrimArray un 0 (ulen + 1) 0 --- let u_hi = PA.indexPrimArray u (ulen - 1) --- PA.writePrimArray un ulen (u_hi .>>. (64 - shift)) --- let normalize_u !j !uj --- | j == 0 = --- PA.writePrimArray un 0 (PA.indexPrimArray u 0 .<<. shift) --- | otherwise = do --- let !uj_1 = PA.indexPrimArray u (j - 1) --- !val = (uj .<<. shift) .|. (uj_1 .>>. (64 - shift)) --- PA.writePrimArray un j val --- normalize_u (pred j) uj_1 --- normalize_u (ulen - 1) u_hi --- if dlen == 1 --- then do --- -- normalized divisor is small --- !un_final <- PA.unsafeFreezePrimArray un --- !r <- quotrem_by1 quo un_final dn_0 --- pure $ PA.primArrayFromList [r .>>. shift, 0, 0, 0] -- XX --- else do --- quotrem_knuth quo un dn dlen --- -- unnormalize remainder --- let unn_rem !j !un_j --- | j == dlen = do --- PA.writePrimArray un (j - 1) (un_j .>>. shift) --- PA.unsafeFreezePrimArray un --- | otherwise = do --- !un_j_1 <- PA.readPrimArray un (j + 1) --- let !unn_j = (un_j .>>. shift) .|. (un_j_1 .<<. (64 - shift)) --- PA.writePrimArray un j unn_j --- unn_rem (j + 1) un_j_1 --- --- !un_0 <- PA.readPrimArray un 0 --- {-# SCC "unn_rem" #-} unn_rem 0 un_0 +quotrem_knuth + :: PrimMonad m + => PA.MutablePrimArray (PrimState m) Word64 -- quotient (potentially large) + -> PA.MutablePrimArray (PrimState m) Word64 -- normalized dividend + -> Word256 -- normalized divisor + -> Int -- words in normalized divisor + -> m () +quotrem_knuth quo u d@(Word256 d0 d1 d2 d3) ld = do + !lu <- PA.getSizeofMutablePrimArray u + darr <- PA.newPrimArray 4 + PA.writePrimArray darr 0 d0 + PA.writePrimArray darr 1 d1 + PA.writePrimArray darr 2 d2 + PA.writePrimArray darr 3 d3 + d_final <- PA.unsafeFreezePrimArray darr + let (dh, dl) = case ld of + 4 -> (d3, d2) + 3 -> (d2, d1) + 2 -> (d1, d0) + _ -> error "ppad-fixed (quotrem_knuth): bad index" + !rec = recip_2by1 dh + loop !j + | j < 0 = pure () + | otherwise = do + !u2 <- PA.readPrimArray u (j + ld) + !u1 <- PA.readPrimArray u (j + ld - 1) + !u0 <- PA.readPrimArray u (j + ld - 2) + let !qhat + | u2 >= dh = 0xffff_ffff_ffff_ffff + | otherwise = + let !(P qh rh) = quotrem_2by1 u2 u1 dh rec + !(P ph pl) = mul_c qh dl + in if ph > rh || (ph == rh && pl > u0) + then qh - 1 + else qh + + !borrow <- sub_mul u j d_final ld qhat + PA.writePrimArray u (j + ld) (u2 - borrow) + if u2 < borrow + then do + let !qh = qhat - 1 + r <- add_to u j d ld + PA.writePrimArray u (j + ld) r + PA.writePrimArray quo j qh + else + PA.writePrimArray quo j qhat + loop (pred j) + loop (lu - ld - 1) + +quotrem + :: PrimMonad m + => PA.MutablePrimArray (PrimState m) Word64 -- quotient (potentially large) + -> PA.PrimArray Word64 -- dividend (potentially large) + -> Word256 -- divisor (256-bit) + -> m (PA.PrimArray Word64) -- remainder (256-bit) +quotrem quo u (Word256 d0 d1 d2 d3) = do + let -- normalize divisor + (dlen, shift) + | d3 /= 0 = (4, B.countLeadingZeros d3) + | d2 /= 0 = (3, B.countLeadingZeros d2) + | d1 /= 0 = (2, B.countLeadingZeros d1) + | otherwise = (1, B.countLeadingZeros d0) -- zero not checked + dn_3 = (d3 .<<. shift) .|. (d2 .>>. (64 - shift)) + dn_2 = (d2 .<<. shift) .|. (d1 .>>. (64 - shift)) + dn_1 = (d1 .<<. shift) .|. (d0 .>>. (64 - shift)) + dn_0 = d0 .<<. shift + !dn = Word256 dn_0 dn_1 dn_2 dn_3 + -- get size of normalized dividend + lu = PA.sizeofPrimArray u + ulen = let loop !j + | j < 0 = 0 + | PA.indexPrimArray u j /= 0 = j + 1 + | otherwise = loop (j - 1) + in loop (lu - 1) + if ulen < dlen + then do + -- u always has size at least 4 + !r <- PA.newPrimArray 4 + PA.copyPrimArray r 0 u 0 4 + PA.unsafeFreezePrimArray r + else do + -- normalize dividend + !un <- PA.newPrimArray (ulen + 1) + PA.setPrimArray un 0 (ulen + 1) 0 + let u_hi = PA.indexPrimArray u (ulen - 1) + PA.writePrimArray un ulen (u_hi .>>. (64 - shift)) + let normalize_u !j !uj + | j == 0 = + PA.writePrimArray un 0 (PA.indexPrimArray u 0 .<<. shift) + | otherwise = do + let !uj_1 = PA.indexPrimArray u (j - 1) + !val = (uj .<<. shift) .|. (uj_1 .>>. (64 - shift)) + PA.writePrimArray un j val + normalize_u (pred j) uj_1 + normalize_u (ulen - 1) u_hi + if dlen == 1 + then do + -- normalized divisor is small + !un_final <- PA.unsafeFreezePrimArray un + !r <- quotrem_by1 quo un_final dn_0 + pure $ PA.primArrayFromList [r .>>. shift, 0, 0, 0] -- XX + else do + quotrem_knuth quo un dn dlen + -- unnormalize remainder + let unn_rem !j !un_j + | j == dlen = do + PA.writePrimArray un (j - 1) (un_j .>>. shift) + PA.unsafeFreezePrimArray un + | otherwise = do + !un_j_1 <- PA.readPrimArray un (j + 1) + let !unn_j = (un_j .>>. shift) .|. (un_j_1 .<<. (64 - shift)) + PA.writePrimArray un j unn_j + unn_rem (j + 1) un_j_1 + + !un_0 <- PA.readPrimArray un 0 + unn_rem 0 un_0 -- x =- y * m -- requires (len x - x_offset) >= len y > 0 @@ -733,165 +782,76 @@ sub_mul x x_offset y l m = do loop (succ j) (ph + carry1 + carry2) loop 0 0 --- -- quotrem of dividend divided by word --- quotrem_by1 --- :: PrimMonad m --- => Memory m -- memory --- -> Int -- normalized dividend offset --- -> Int -- length of normalized dividend --- -> Int -- normalized divisor offset --- -> m Word64 -- remainder --- quotrem_by1 (Memory buf) un_offset lun dn_offset = do --- d <- PA.readPrimArray buf dn_offset --- let rec = recip_2by1 d --- r0 <- PA.readPrimArray buf (un_offset + lun - 1) --- let loop !j !racc --- | j < 0 = pure racc --- | otherwise = do --- !uj <- PA.readPrimArray buf (un_offset + j) --- let !(P qj rnex) = quotrem_2by1 racc uj d rec --- PA.writePrimArray buf j qj --- loop (j - 1) rnex --- loop (lun - 2) r0 - --- quotrem_by1 --- :: PrimMonad m --- => PA.MutablePrimArray (PrimState m) Word64 --- -> PA.PrimArray Word64 --- -> Word64 --- -> m Word64 --- quotrem_by1 quo u d = do --- let !rec = recip_2by1 d --- !lu = PA.sizeofPrimArray u --- !r0 = PA.indexPrimArray u (lu - 1) --- loop !j !racc --- | j < 0 = pure racc --- | otherwise = do --- let uj = PA.indexPrimArray u j --- !(P qj rnex) = quotrem_2by1 racc uj d rec --- PA.writePrimArray quo j qj --- loop (pred j) rnex --- loop (lu - 2) r0 --- --- add_to --- :: PrimMonad m --- => PA.MutablePrimArray (PrimState m) Word64 --- -> Int --- -> Word256 --- -> Int --- -> m Word64 --- add_to x x_offset (Word256 y0 y1 y2 y3) l = do --- let loop !j !cacc --- | j == l = pure cacc --- | otherwise = do --- xj <- PA.readPrimArray x (j + x_offset) --- let !(P nex carry) = case j of --- 0 -> add_c xj y0 cacc --- 1 -> add_c xj y1 cacc --- 2 -> add_c xj y2 cacc --- 3 -> add_c xj y3 cacc --- _ -> error "ppad-fixed (add_to): bad index" --- PA.writePrimArray x (j + x_offset) nex --- loop (succ j) carry --- loop 0 0 --- --- quotrem_knuth --- :: PrimMonad m --- => PA.MutablePrimArray (PrimState m) Word64 -- quotient (potentially large) --- -> PA.MutablePrimArray (PrimState m) Word64 -- normalized dividend --- -> Word256 -- normalized divisor --- -> Int -- words in normalized divisor --- -> m () --- quotrem_knuth quo u d@(Word256 d0 d1 d2 d3) ld = do --- !lu <- PA.getSizeofMutablePrimArray u --- darr <- PA.newPrimArray 4 --- PA.writePrimArray darr 0 d0 --- PA.writePrimArray darr 1 d1 --- PA.writePrimArray darr 2 d2 --- PA.writePrimArray darr 3 d3 --- d_final <- PA.unsafeFreezePrimArray darr --- let (dh, dl) = case ld of --- 4 -> (d3, d2) --- 3 -> (d2, d1) --- 2 -> (d1, d0) --- _ -> error "ppad-fixed (quotrem_knuth): bad index" --- !rec = recip_2by1 dh --- loop !j --- | j < 0 = pure () --- | otherwise = do --- !u2 <- PA.readPrimArray u (j + ld) --- !u1 <- PA.readPrimArray u (j + ld - 1) --- !u0 <- PA.readPrimArray u (j + ld - 2) --- let !qhat --- | u2 >= dh = 0xffff_ffff_ffff_ffff --- | otherwise = --- let !(P qh rh) = quotrem_2by1 u2 u1 dh rec --- !(P ph pl) = mul_c qh dl --- in if ph > rh || (ph == rh && pl > u0) --- then qh - 1 --- else qh --- --- !borrow <- sub_mul u j d_final ld qhat --- PA.writePrimArray u (j + ld) (u2 - borrow) --- if u2 < borrow --- then do --- let !qh = qhat - 1 --- r <- add_to u j d ld --- PA.writePrimArray u (j + ld) r --- PA.writePrimArray quo j qh --- else --- PA.writePrimArray quo j qhat --- loop (pred j) --- loop (lu - ld - 1) --- --- div :: Word256 -> Word256 -> Word256 --- div u@(Word256 u0 u1 u2 u3) d@(Word256 d0 _ _ _) --- | is_zero d || d `gt` u = zero -- ? --- | u == d = one --- | is_word64 u = Word256 (u0 `quot` d0) 0 0 0 --- | otherwise = runST $ do --- -- allocate quotient --- quo <- PA.newPrimArray 4 --- PA.setPrimArray quo 0 4 0 --- -- allocate dividend --- u_arr <- PA.newPrimArray 4 --- PA.setPrimArray u_arr 0 4 0 --- PA.writePrimArray u_arr 0 u0 --- PA.writePrimArray u_arr 1 u1 --- PA.writePrimArray u_arr 2 u2 --- PA.writePrimArray u_arr 3 u3 --- u_final <- PA.unsafeFreezePrimArray u_arr --- _ <- quotrem quo u_final d --- q0 <- PA.readPrimArray quo 0 --- q1 <- PA.readPrimArray quo 1 --- q2 <- PA.readPrimArray quo 2 --- q3 <- PA.readPrimArray quo 3 --- pure (Word256 q0 q1 q2 q3) +add_to + :: PrimMonad m + => PA.MutablePrimArray (PrimState m) Word64 + -> Int + -> Word256 + -> Int + -> m Word64 +add_to x x_offset (Word256 y0 y1 y2 y3) l = do + let loop !j !cacc + | j == l = pure cacc + | otherwise = do + xj <- PA.readPrimArray x (j + x_offset) + let !(P nex carry) = case j of + 0 -> add_c xj y0 cacc + 1 -> add_c xj y1 cacc + 2 -> add_c xj y2 cacc + 3 -> add_c xj y3 cacc + _ -> error "ppad-fixed (add_to): bad index" + PA.writePrimArray x (j + x_offset) nex + loop (succ j) carry + loop 0 0 + +div :: Word256 -> Word256 -> Word256 +div u@(Word256 u0 u1 u2 u3) d@(Word256 d0 _ _ _) + | is_zero d || d `gt` u = zero -- ? + | u == d = one + | is_word64 u = Word256 (u0 `quot` d0) 0 0 0 + | otherwise = runST $ do + -- allocate quotient + quo <- PA.newPrimArray 4 + PA.setPrimArray quo 0 4 0 + -- allocate dividend + u_arr <- PA.newPrimArray 4 + PA.setPrimArray u_arr 0 4 0 + PA.writePrimArray u_arr 0 u0 + PA.writePrimArray u_arr 1 u1 + PA.writePrimArray u_arr 2 u2 + PA.writePrimArray u_arr 3 u3 + u_final <- PA.unsafeFreezePrimArray u_arr + _ <- quotrem quo u_final d + q0 <- PA.readPrimArray quo 0 + q1 <- PA.readPrimArray quo 1 + q2 <- PA.readPrimArray quo 2 + q3 <- PA.readPrimArray quo 3 + pure (Word256 q0 q1 q2 q3) + +-- | Modulo operation on 'Word256' values. -- --- -- | Modulo operation on 'Word256' values. --- -- --- -- >>> to_word256 0xFFFFFFFFFF `mod` to_word256 0xFFFFFF --- -- 65535 --- mod :: Word256 -> Word256 -> Word256 --- mod u@(Word256 u0 u1 u2 u3) d@(Word256 d0 _ _ _) --- | is_zero d || d `gt` u = zero -- ? --- | u == d = one --- | is_word64 u = Word256 (u0 `quot` d0) 0 0 0 --- | otherwise = runST $ do --- -- allocate quotient --- quo <- PA.newPrimArray 4 --- PA.setPrimArray quo 0 4 0 --- -- allocate dividend --- u_arr <- PA.newPrimArray 4 --- PA.setPrimArray u_arr 0 4 0 --- PA.writePrimArray u_arr 0 u0 --- PA.writePrimArray u_arr 1 u1 --- PA.writePrimArray u_arr 2 u2 --- PA.writePrimArray u_arr 3 u3 --- u_final <- PA.unsafeFreezePrimArray u_arr --- r <- quotrem quo u_final d --- let r0 = PA.indexPrimArray r 0 --- r1 = PA.indexPrimArray r 1 --- r2 = PA.indexPrimArray r 2 --- r3 = PA.indexPrimArray r 3 --- pure (Word256 r0 r1 r2 r3) +-- >>> to_word256 0xFFFFFFFFFF `mod` to_word256 0xFFFFFF +-- 65535 +mod :: Word256 -> Word256 -> Word256 +mod u@(Word256 u0 u1 u2 u3) d@(Word256 d0 _ _ _) + | is_zero d || d `gt` u = zero -- ? + | u == d = one + | is_word64 u = Word256 (u0 `quot` d0) 0 0 0 + | otherwise = runST $ do + -- allocate quotient + quo <- PA.newPrimArray 4 + PA.setPrimArray quo 0 4 0 + -- allocate dividend + u_arr <- PA.newPrimArray 4 + PA.setPrimArray u_arr 0 4 0 + PA.writePrimArray u_arr 0 u0 + PA.writePrimArray u_arr 1 u1 + PA.writePrimArray u_arr 2 u2 + PA.writePrimArray u_arr 3 u3 + u_final <- PA.unsafeFreezePrimArray u_arr + r <- quotrem quo u_final d + let r0 = PA.indexPrimArray r 0 + r1 = PA.indexPrimArray r 1 + r2 = PA.indexPrimArray r 2 + r3 = PA.indexPrimArray r 3 + pure (Word256 r0 r1 r2 r3) diff --git a/test/Main.hs b/test/Main.hs @@ -36,7 +36,15 @@ instance Q.Arbitrary Monotonic where `Q.suchThat` (\b -> b <= a) pure (Monotonic (a, b)) --- properties ----------------------------------------------------------------- +newtype DivMonotonic = DivMonotonic (Integer, Integer) + deriving Show + +instance Q.Arbitrary DivMonotonic where + arbitrary = do + a <- Q.chooseInteger (1, 2 ^ (256 :: Int) - 1) + b <- (Q.chooseInteger (1, 2 ^ (256 :: Int) - 1)) + `Q.suchThat` (\b -> b <= a) + pure (DivMonotonic (a, b)) -- addition / subtraction ---------------- @@ -85,6 +93,18 @@ mul_lo_matches (Q.NonNegative a) (Q.NonNegative b) = -- division ------------------------------ +div_matches :: DivMonotonic -> Bool +div_matches (DivMonotonic (a, b)) = + let !left = to_word256 a `div` to_word256 b + !rite = to_word256 (a `Prelude.div` b) + in left == rite + +mod_matches :: DivMonotonic -> Bool +mod_matches (DivMonotonic (a, b)) = + let !left = to_word256 a `mod` to_word256 b + !rite = to_word256 (a `rem` b) + in left == rite + quotrem_r_case0 :: H.Assertion quotrem_r_case0 = do let !(P q r) = quotrem_r 2 4 4 @@ -129,8 +149,6 @@ quotrem_by1_case0 = do -- tests ---------------------------------------------------------------------- - - add_sub :: TestTree add_sub = testGroup "addition & subtraction" [ Q.testProperty "addition matches (nonneg)" $ @@ -149,10 +167,10 @@ multiplication = testGroup "arithmetic" [ Q.withMaxSuccess 1000 umul_step_predicate_holds , Q.testProperty "mul matches (nonneg, low bits)" $ Q.withMaxSuccess 1000 mul_lo_matches - -- , Q.testProperty "division matches" $ - -- Q.withMaxSuccess 1000 div_matches - -- , Q.testProperty "mod matches" $ - -- Q.withMaxSuccess 1000 mod_matches + , Q.testProperty "division matches" $ + Q.withMaxSuccess 1000 div_matches + , Q.testProperty "mod matches" $ + Q.withMaxSuccess 1000 mod_matches ] main :: IO () @@ -193,17 +211,7 @@ main = defaultMain $ testGroup "ppad-fixed" [ -- Q.NonNegative b <- -- Q.arbitrary `Q.suchThat` (\(Q.NonNegative b) -> b * m <= a) -- pure (MulMonotonic (a, b, m)) --- --- newtype DivMonotonic = DivMonotonic (Integer, Integer) --- deriving Show --- --- instance Q.Arbitrary DivMonotonic where --- arbitrary = do --- a <- Q.chooseInteger (1, 2 ^ (256 :: Int) - 1) --- b <- (Q.chooseInteger (1, 2 ^ (256 :: Int) - 1)) --- `Q.suchThat` (\b -> b <= a) --- pure (DivMonotonic (a, b)) --- + -- -- properties ----------------------------------------------------------------- -- -- lt_matches :: Different (Q.NonNegative Integer) -> Bool @@ -239,19 +247,6 @@ main = defaultMain $ testGroup "ppad-fixed" [ -- sub_matches :: Monotonic -> Bool -- sub_matches (Monotonic (a, b)) = -- to_integer (to_word256 a `sub` to_word256 b) == a - b --- --- div_matches :: DivMonotonic -> Bool --- div_matches (DivMonotonic (a, b)) = --- let !left = to_word256 a `div` to_word256 b --- !rite = to_word256 (a `Prelude.div` b) --- in left == rite --- --- mod_matches :: DivMonotonic -> Bool --- mod_matches (DivMonotonic (a, b)) = --- let !left = to_word256 a `mod` to_word256 b --- !rite = to_word256 (a `rem` b) --- in left == rite --- -- -- assertions ------------------------------------------------------------------ -- -- quotrem_r_case0 :: H.Assertion