From 84194fc1871cf32a3b722b80bdd2c7887640aad4 Mon Sep 17 00:00:00 2001 From: Ryan Date: Wed, 10 Jul 2024 10:13:11 -0600 Subject: [PATCH 1/5] Issue#1675, add failing test for ec_mult as y should be 0 rather than 13. --- tests/issues/issue1675/issue1675.icry | 5 +++++ tests/issues/issue1675/issue1675.icry.stdout | 13 +++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 tests/issues/issue1675/issue1675.icry create mode 100644 tests/issues/issue1675/issue1675.icry.stdout diff --git a/tests/issues/issue1675/issue1675.icry b/tests/issues/issue1675/issue1675.icry new file mode 100644 index 00000000..76d6738e --- /dev/null +++ b/tests/issues/issue1675/issue1675.icry @@ -0,0 +1,5 @@ +:m PrimeEC +ec_mult`{13} 3 {x = 0, y = 0, z = 1} +:t ec_mult`{13} +ec_mult`{13} 3 {x = 0, y = 0, z = 1} : ProjectivePoint 13 +{x = 0, y = 13, z = 1} : ProjectivePoint 13 \ No newline at end of file diff --git a/tests/issues/issue1675/issue1675.icry.stdout b/tests/issues/issue1675/issue1675.icry.stdout new file mode 100644 index 00000000..2180c833 --- /dev/null +++ b/tests/issues/issue1675/issue1675.icry.stdout @@ -0,0 +1,13 @@ +Loading module Cryptol +Loading module Cryptol +Loading module PrimeEC +{x = 0, y = 0, z = 1} +ec_mult`{13} : Z 13 -> ProjectivePoint 13 -> ProjectivePoint 13 +{x = 0, y = 0, z = 1} + +[error] at issue1675.icry:5:13--5:15: + • Unsolvable constraint: + 13 >= 14 + arising from + use of literal or demoted expression + at issue1675.icry:5:13--5:15 From e1774d45c10038f3aa0b50f97c79316071afbb4a Mon Sep 17 00:00:00 2001 From: Ryan Date: Wed, 10 Jul 2024 11:26:37 -0600 Subject: [PATCH 2/5] Mod y variable by p in ec_sub It appears that a modulus was not happening in ec_sub that was causing the odd issue noted in #1675. This commit adds that modulus and fixes it. --- src/Cryptol/PrimeEC.hs | 2 +- src/GHC/Num/Compat.hs | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index e86771ba..c9b50533 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -202,7 +202,7 @@ ec_add p s t ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_sub p s t = ec_add p s u where u = case BN.bigNatSub (primeMod p) (py t) of - (# | y' #) -> t{ py = y' } + (# | y' #) -> t{ py = BN.modBigNat y' (primeMod p) } (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))] {-# INLINE ec_sub #-} diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs index 84ed6abb..4df9ac07 100644 --- a/src/GHC/Num/Compat.hs +++ b/src/GHC/Num/Compat.hs @@ -24,6 +24,7 @@ module GHC.Num.Compat , bigNatSqr , bigNatSub , bigNatSubUnsafe + , modBigNat , oneBigNat , recipModBigNat , shiftLBigNat @@ -73,6 +74,9 @@ oneBigNat _ = BN.bigNatFromWord# 1## recipModBigNat :: BigNat# -> BigNat# -> BigNat# recipModBigNat = BN.sbignat_recip_mod 0# +modBigNat :: BigNat# -> BigNat# -> BigNat# +modBigNat x y = BN.bigNatPowMod x (integerToBigNat 1) y + shiftLBigNat :: BigNat# -> Int# -> BigNat# shiftLBigNat bn i = BN.bigNatShiftL# bn (int2Word# i) From 873fa9cd67e6e148c8121b78a830c6578b9cdd01 Mon Sep 17 00:00:00 2001 From: Ryan Date: Wed, 10 Jul 2024 12:31:43 -0600 Subject: [PATCH 3/5] Remove bigNatMod and replace with bigNatRem, and add same fix to negate as well --- src/Cryptol/PrimeEC.hs | 4 ++-- src/GHC/Num/Compat.hs | 4 ---- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index c9b50533..b72ccb06 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -202,13 +202,13 @@ ec_add p s t ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_sub p s t = ec_add p s u where u = case BN.bigNatSub (primeMod p) (py t) of - (# | y' #) -> t{ py = BN.modBigNat y' (primeMod p) } + (# | y' #) -> t{ py = y' `BN.bigNatRem` (primeMod p) } (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))] {-# INLINE ec_sub #-} ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -ec_negate p s = s{ py = BN.bigNatSubUnsafe (primeMod p) (py s) } +ec_negate p s = s{ py = (BN.bigNatSubUnsafe (primeMod p) (py s)) `BN.bigNatRem` (primeMod p) } {-# INLINE ec_negate #-} -- | Compute the elliptic curve group addition operation diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs index 4df9ac07..84ed6abb 100644 --- a/src/GHC/Num/Compat.hs +++ b/src/GHC/Num/Compat.hs @@ -24,7 +24,6 @@ module GHC.Num.Compat , bigNatSqr , bigNatSub , bigNatSubUnsafe - , modBigNat , oneBigNat , recipModBigNat , shiftLBigNat @@ -74,9 +73,6 @@ oneBigNat _ = BN.bigNatFromWord# 1## recipModBigNat :: BigNat# -> BigNat# -> BigNat# recipModBigNat = BN.sbignat_recip_mod 0# -modBigNat :: BigNat# -> BigNat# -> BigNat# -modBigNat x y = BN.bigNatPowMod x (integerToBigNat 1) y - shiftLBigNat :: BigNat# -> Int# -> BigNat# shiftLBigNat bn i = BN.bigNatShiftL# bn (int2Word# i) From 39b0682fbb92d2679e17d7bdceb35b78c90e4419 Mon Sep 17 00:00:00 2001 From: Ryan Date: Wed, 10 Jul 2024 13:30:17 -0600 Subject: [PATCH 4/5] Clean up panic error message in ec_mult --- src/Cryptol/PrimeEC.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index b72ccb06..f230a1db 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -294,7 +294,7 @@ ec_mult p d s | BN.bigNatIsZero (pz s) = zro | otherwise = case m of - 0# -> panic "ec_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))] + 0# -> panic "ec_mult" ["integer with 0 width", show h] _ -> go m zro where From dd112501ca1d3f08350fedf481267d3631832bf4 Mon Sep 17 00:00:00 2001 From: Ryan Date: Wed, 10 Jul 2024 15:02:15 -0600 Subject: [PATCH 5/5] Remove unnecessary line from issue1675 test. --- tests/issues/issue1675/issue1675.icry | 3 +-- tests/issues/issue1675/issue1675.icry.stdout | 7 ------- 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/tests/issues/issue1675/issue1675.icry b/tests/issues/issue1675/issue1675.icry index 76d6738e..716382ca 100644 --- a/tests/issues/issue1675/issue1675.icry +++ b/tests/issues/issue1675/issue1675.icry @@ -1,5 +1,4 @@ :m PrimeEC ec_mult`{13} 3 {x = 0, y = 0, z = 1} :t ec_mult`{13} -ec_mult`{13} 3 {x = 0, y = 0, z = 1} : ProjectivePoint 13 -{x = 0, y = 13, z = 1} : ProjectivePoint 13 \ No newline at end of file +ec_mult`{13} 3 {x = 0, y = 0, z = 1} : ProjectivePoint 13 \ No newline at end of file diff --git a/tests/issues/issue1675/issue1675.icry.stdout b/tests/issues/issue1675/issue1675.icry.stdout index 2180c833..753daaa1 100644 --- a/tests/issues/issue1675/issue1675.icry.stdout +++ b/tests/issues/issue1675/issue1675.icry.stdout @@ -4,10 +4,3 @@ Loading module PrimeEC {x = 0, y = 0, z = 1} ec_mult`{13} : Z 13 -> ProjectivePoint 13 -> ProjectivePoint 13 {x = 0, y = 0, z = 1} - -[error] at issue1675.icry:5:13--5:15: - • Unsolvable constraint: - 13 >= 14 - arising from - use of literal or demoted expression - at issue1675.icry:5:13--5:15