Date: Friday, July 8, 2022 @ 13:12:55 Author: felixonmars Revision: 1248677
upgpkg: cryptol 2.13.0-1: rebuild with cryptol 2.13.0, what4 1.3 Modified: cryptol/trunk/PKGBUILD Deleted: cryptol/trunk/ghc9.patch ------------+ PKGBUILD | 27 - ghc9.patch | 809 ----------------------------------------------------------- 2 files changed, 12 insertions(+), 824 deletions(-) Modified: PKGBUILD =================================================================== --- PKGBUILD 2022-07-08 13:10:36 UTC (rev 1248676) +++ PKGBUILD 2022-07-08 13:12:55 UTC (rev 1248677) @@ -1,8 +1,8 @@ # Maintainer: Felix Yan <felixonm...@archlinux.org> pkgname=cryptol -pkgver=2.12.0 -pkgrel=98 +pkgver=2.13.0 +pkgrel=1 pkgdesc="The Language of Cryptography" url="https://www.cryptol.net" license=("BSD") @@ -15,22 +15,14 @@ 'haskell-simple-smt' 'haskell-strict' 'haskell-temporary' 'haskell-tf-random' 'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html') makedepends=('ghc' 'uusi' 'alex' 'happy') -source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz" - ghc9.patch) -sha512sums=('3e7a58de47e5ae1fdc5067b2bcca66c04ee06c71e84f890104b64c59d1cd125667a23f537c3afd0503c059c97f5d168e6afa0df4fdc6c1e9448aae434e616bc8' - 'f41afa8f65b01aaa5fc92a6433ed09ae85e86f58cb86e64b72de7e6765b32835974cb998305235d5c1ed8ff1112595f61400e16bd2ffd16c578c0c499d02486b') +source=("https://github.com/GaloisInc/cryptol/archive/$pkgver/$pkgname-$pkgver.tar.gz") +sha512sums=('232a91964379f8638a41845bc30040e42ded53089410f4f1ecd5649d2cc7811994963c3c3061710c5712eeaeb1813eb409c65197372cac64b5babbc7e99b2296') -prepare() { +build() { cd $pkgname-$pkgver - patch -p1 -i ../ghc9.patch - uusi -u base-compat -u sbv $pkgname.cabal -} -build() { - cd "${srcdir}/${pkgname}-${pkgver}" - runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \ - --prefix=/usr --docdir=/usr/share/doc/$pkgname --datasubdir=$pkgname \ + --prefix=/usr --docdir=/usr/share/doc/$pkgname --datasubdir=$pkgname --enable-tests \ --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid --ghc-option=-fllvm \ -f-static -f-relocatable --ghc-option='-pie' runhaskell Setup build $MAKEFLAGS @@ -40,8 +32,13 @@ sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh } +check() { + cd $pkgname-$pkgver + runhaskell Setup test --show-details=direct +} + package() { - cd "${srcdir}/${pkgname}-${pkgver}" + cd $pkgname-$pkgver install -D -m744 register.sh "${pkgdir}/usr/share/haskell/register/${pkgname}.sh" install -D -m744 unregister.sh "${pkgdir}/usr/share/haskell/unregister/${pkgname}.sh" Deleted: ghc9.patch =================================================================== --- ghc9.patch 2022-07-08 13:10:36 UTC (rev 1248676) +++ ghc9.patch 2022-07-08 13:12:55 UTC (rev 1248677) @@ -1,809 +0,0 @@ -From 889bfd65116b8817bd97b18e8a1e66db57c135cf Mon Sep 17 00:00:00 2001 -From: Rob Dockins <rdock...@galois.com> -Date: Wed, 14 Jul 2021 22:44:53 -0700 -Subject: [PATCH 1/2] First take at GHC 9.* compatibility. - -There's a lot here that can be cleaned up, and we need -some backward compatiblity layer, but this is just a first -try. - -Something in the PrimeEC module is causing hard crashes -during the test suite, so I'll have to figure out what's -going on there. ---- - cryptol-remote-api/cryptol-remote-api.cabal | 7 +- - cryptol.cabal | 5 +- - cryptol/OptParser.hs | 1 - - src/Cryptol/Backend/Concrete.hs | 13 +- - src/Cryptol/Backend/SBV.hs | 9 +- - src/Cryptol/Backend/What4.hs | 9 +- - src/Cryptol/Eval/Concrete.hs | 4 +- - src/Cryptol/Eval/Reference.lhs | 10 +- - src/Cryptol/ModuleSystem/Name.hs | 4 +- - src/Cryptol/PrimeEC.hs | 259 ++++++++------------ - src/Cryptol/TypeCheck/Solver/Numeric.hs | 8 +- - 11 files changed, 138 insertions(+), 191 deletions(-) - -diff --git a/cryptol.cabal b/cryptol.cabal -index c140f87dd..b6e31f471 100644 ---- a/cryptol.cabal -+++ b/cryptol.cabal -@@ -56,7 +56,8 @@ library - ghc-prim, - GraphSCC >= 1.0.4, - heredoc >= 0.2, -- integer-gmp >= 1.0 && < 1.1, -+ ghc-bignum, -+ arithmoi, - libBF >= 0.6 && < 0.7, - MemoTrie >= 0.6 && < 0.7, - monad-control >= 1.0, -diff --git a/cryptol/OptParser.hs b/cryptol/OptParser.hs -index 4aa4b3153..74ea6084f 100644 ---- a/cryptol/OptParser.hs -+++ b/cryptol/OptParser.hs -@@ -9,7 +9,6 @@ - - module OptParser where - --import Data.Monoid (Endo(..)) - import Data.Semigroup - - import Prelude () -diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs -index 3a0d7a1fa..ab802761f 100644 ---- a/src/Cryptol/Backend/Concrete.hs -+++ b/src/Cryptol/Backend/Concrete.hs -@@ -9,6 +9,7 @@ - {-# LANGUAGE BangPatterns #-} - {-# LANGUAGE BlockArguments #-} - {-# LANGUAGE LambdaCase #-} -+{-# LANGUAGE MagicHash #-} - {-# LANGUAGE NamedFieldPuns #-} - {-# LANGUAGE PatternGuards #-} - {-# LANGUAGE Rank2Types #-} -@@ -17,6 +18,7 @@ - {-# LANGUAGE TupleSections #-} - {-# LANGUAGE TypeFamilies #-} - {-# LANGUAGE ViewPatterns #-} -+{-# LANGUAGE UnboxedTuples #-} - module Cryptol.Backend.Concrete - ( BV(..) - , binBV -@@ -40,7 +42,7 @@ import Data.Bits - import Data.Ratio - import Numeric (showIntAtBase) - import qualified LibBF as FP --import qualified GHC.Integer.GMP.Internals as Integer -+import qualified GHC.Num.Integer as Integer - - import qualified Cryptol.Backend.Arch as Arch - import qualified Cryptol.Backend.FloatHelpers as FP -@@ -339,11 +341,10 @@ instance Backend Concrete where - -- NB: under the precondition that `m` is prime, - -- the only values for which no inverse exists are - -- congruent to 0 modulo m. -- znRecip sym m x -- | r == 0 = raiseError sym DivideByZero -- | otherwise = pure r -- where -- r = Integer.recipModInteger x m -+ znRecip sym m x = -+ case Integer.integerRecipMod# x (Integer.integerToNaturalClamp m) of -+ (# r | #) -> integerLit sym (toInteger r) -+ (# | () #) -> raiseError sym DivideByZero - - znPlus _ = liftBinIntMod (+) - znMinus _ = liftBinIntMod (-) -diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs -index e18a195d8..87cc7b0a2 100644 ---- a/src/Cryptol/Backend/SBV.hs -+++ b/src/Cryptol/Backend/SBV.hs -@@ -11,12 +11,14 @@ - {-# LANGUAGE FlexibleInstances #-} - {-# LANGUAGE GeneralizedNewtypeDeriving #-} - {-# LANGUAGE LambdaCase #-} -+{-# LANGUAGE MagicHash #-} - {-# LANGUAGE MultiParamTypeClasses #-} - {-# LANGUAGE MultiWayIf #-} - {-# LANGUAGE PatternGuards #-} - {-# LANGUAGE TypeFamilies #-} - {-# LANGUAGE TypeSynonymInstances #-} - {-# LANGUAGE ViewPatterns #-} -+{-# LANGUAGE UnboxedTuples #-} - module Cryptol.Backend.SBV - ( SBV(..), SBVEval(..), SBVResult(..) - , literalSWord -@@ -38,7 +40,7 @@ import Control.Monad.IO.Class (MonadIO(..)) - import Data.Bits (bit, complement) - import Data.List (foldl') - --import qualified GHC.Integer.GMP.Internals as Integer -+import qualified GHC.Num.Integer as Integer - - import Data.SBV.Dynamic as SBV - import qualified Data.SBV.Internals as SBV -@@ -428,8 +430,9 @@ sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"] - sModRecip sym m x - -- If the input is concrete, evaluate the answer - | Just xi <- svAsInteger x -- = let r = Integer.recipModInteger xi m -- in if r == 0 then raiseError sym DivideByZero else integerLit sym r -+ = case Integer.integerRecipMod# xi (Integer.integerToNaturalClamp m) of -+ (# r | #) -> integerLit sym (toInteger r) -+ (# | () #) -> raiseError sym DivideByZero - - -- If the input is symbolic, create a new symbolic constant - -- and assert that it is the desired multiplicitive inverse. -diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs -index 11731522a..3ff9c9069 100644 ---- a/src/Cryptol/Backend/What4.hs -+++ b/src/Cryptol/Backend/What4.hs -@@ -8,10 +8,12 @@ - {-# LANGUAGE DeriveFunctor #-} - {-# LANGUAGE ExistentialQuantification #-} - {-# LANGUAGE LambdaCase #-} -+{-# LANGUAGE MagicHash #-} - {-# LANGUAGE MultiWayIf #-} - {-# LANGUAGE ScopedTypeVariables #-} - {-# LANGUAGE TypeFamilies #-} - {-# LANGUAGE ViewPatterns #-} -+{-# LANGUAGE UnboxedTuples #-} - module Cryptol.Backend.What4 where - - -@@ -28,7 +30,7 @@ import Data.Text (Text) - import Data.Parameterized.NatRepr - import Data.Parameterized.Some - --import qualified GHC.Integer.GMP.Internals as Integer -+import qualified GHC.Num.Integer as Integer - - import qualified What4.Interface as W4 - import qualified What4.SWord as SW -@@ -667,8 +669,9 @@ sModRecip _sym 0 _ = panic "sModRecip" ["0 modulus not allowed"] - sModRecip sym m x - -- If the input is concrete, evaluate the answer - | Just xi <- W4.asInteger x -- = let r = Integer.recipModInteger xi m -- in if r == 0 then raiseError sym DivideByZero else integerLit sym r -+ = case Integer.integerRecipMod# xi (Integer.integerToNaturalClamp m) of -+ (# r | #) -> integerLit sym (toInteger r) -+ (# | () #) -> raiseError sym DivideByZero - - -- If the input is symbolic, create a new symbolic constant - -- and assert that it is the desired multiplicitive inverse. -diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs -index f93cd304d..6ef406411 100644 ---- a/src/Cryptol/Eval/Concrete.hs -+++ b/src/Cryptol/Eval/Concrete.hs -@@ -250,9 +250,9 @@ primeECPrims = Map.fromList $ map (\(n,v) -> (primeECPrim n, v)) - ] - - toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint --toProjectivePoint v = PrimeEC.ProjectivePoint <$> f "x" <*> f "y" <*> f "z" -+toProjectivePoint v = PrimeEC.toProjectivePoint <$> f "x" <*> f "y" <*> f "z" - where -- f nm = PrimeEC.integerToBigNat . fromVInteger <$> lookupRecord nm v -+ f nm = fromVInteger <$> lookupRecord nm v - - fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value - fromProjectivePoint (PrimeEC.ProjectivePoint x y z) = -diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs -index 761ee5bae..3d98be154 100644 ---- a/src/Cryptol/Eval/Reference.lhs -+++ b/src/Cryptol/Eval/Reference.lhs -@@ -10,6 +10,8 @@ - > {-# LANGUAGE BlockArguments #-} - > {-# LANGUAGE PatternGuards #-} - > {-# LANGUAGE LambdaCase #-} -+> {-# LANGUAGE MagicHash #-} -+> {-# LANGUAGE UnboxedTuples #-} - > - > module Cryptol.Eval.Reference - > ( Value(..) -@@ -31,7 +33,7 @@ - > import qualified Data.Text as T (pack) - > import LibBF (BigFloat) - > import qualified LibBF as FP --> import qualified GHC.Integer.GMP.Internals as Integer -+> import qualified GHC.Num.Integer as Integer - > - > import Cryptol.ModuleSystem.Name (asPrim) - > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul) -@@ -1287,8 +1289,10 @@ confused with integral division). - > ratRecip x = pure (recip x) - > - > zRecip :: Integer -> Integer -> E Integer --> zRecip m x = if r == 0 then cryError DivideByZero else pure r --> where r = Integer.recipModInteger x m -+> zRecip m x = -+> case Integer.integerRecipMod# x (Integer.integerToNaturalClamp m) of -+> (# r | #) -> pure (toInteger r) -+> (# | () #) -> cryError DivideByZero - > - > zDiv :: Integer -> Integer -> Integer -> E Integer - > zDiv m x y = f <$> zRecip m y -diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs -index 2dcc9e1d9..6fbb16186 100644 ---- a/src/Cryptol/ModuleSystem/Name.hs -+++ b/src/Cryptol/ModuleSystem/Name.hs -@@ -183,12 +183,12 @@ instance PP Name where - instance PPName Name where - ppNameFixity n = nameFixity n - -- ppInfixName n @ Name { .. } -+ ppInfixName n@Name { .. } - | isInfixIdent nIdent = ppName n - | otherwise = panic "Name" [ "Non-infix name used infix" - , show nIdent ] - -- ppPrefixName n @ Name { .. } = optParens (isInfixIdent nIdent) (ppName n) -+ ppPrefixName n@Name { .. } = optParens (isInfixIdent nIdent) (ppName n) - - - -- | Pretty-print a name with its source location information. -diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs -index e8f9289e7..11f96004c 100644 ---- a/src/Cryptol/PrimeEC.hs -+++ b/src/Cryptol/PrimeEC.hs -@@ -21,13 +21,16 @@ - {-# LANGUAGE MagicHash #-} - {-# LANGUAGE TypeOperators #-} - {-# LANGUAGE ViewPatterns #-} -+{-# LANGUAGE UnboxedTuples #-} -+{-# LANGUAGE UnliftedNewtypes #-} - - module Cryptol.PrimeEC - ( PrimeModulus - , primeModulus - , ProjectivePoint(..) -+ , toProjectivePoint - , integerToBigNat -- , Integer.bigNatToInteger -+ , bigNatToInteger - - , ec_double - , ec_add_nonzero -@@ -36,10 +39,12 @@ module Cryptol.PrimeEC - ) where - - --import GHC.Integer.GMP.Internals (BigNat) --import qualified GHC.Integer.GMP.Internals as Integer -+import GHC.Num.BigNat (BigNat#) -+import qualified GHC.Num.Backend as BN -+import qualified GHC.Num.BigNat as BN -+import qualified GHC.Num.Integer as BN - import GHC.Prim --import Data.Bits -+import GHC.Types - - import Cryptol.TypeCheck.Solver.InfNat (widthInteger) - import Cryptol.Utils.Panic -@@ -48,172 +53,107 @@ import Cryptol.Utils.Panic - -- homogenous coordinates. - data ProjectivePoint = - ProjectivePoint -- { px :: !BigNat -- , py :: !BigNat -- , pz :: !BigNat -+ { px :: !BigNat# -+ , py :: !BigNat# -+ , pz :: !BigNat# - } - -+ -+toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint -+toProjectivePoint x y z = -+ ProjectivePoint (integerToBigNat x) (integerToBigNat y) (integerToBigNat z) -+ - -- | The projective "point at infinity", which represents the zero element - -- of the ECC group. - zro :: ProjectivePoint --zro = ProjectivePoint Integer.oneBigNat Integer.oneBigNat Integer.zeroBigNat -+zro = ProjectivePoint (BN.bigNatFromWord# 1##) (BN.bigNatFromWord# 1##) (BN.bigNatFromWord# 0##) - - -- | Coerce an integer value to a @BigNat@. This operation only really makes - -- sense for nonnegative values, but this condition is not checked. --integerToBigNat :: Integer -> BigNat --integerToBigNat (Integer.S# i) = Integer.wordToBigNat (int2Word# i) --integerToBigNat (Integer.Jp# b) = b --integerToBigNat (Integer.Jn# b) = b -+integerToBigNat :: Integer -> BigNat# -+integerToBigNat = BN.integerToBigNatClamp# -+ -+bigNatToInteger :: BigNat# -> Integer -+bigNatToInteger = BN.integerFromBigNat# - - -- | Simple newtype wrapping the @BigNat@ value of the - -- modulus of the underlying field Z p. This modulus - -- is required to be prime. --newtype PrimeModulus = PrimeModulus { primeMod :: BigNat } -+newtype PrimeModulus = PrimeModulus { primeMod :: BigNat# } - - - -- | Inject an integer value into the @PrimeModulus@ type. - -- This modulus is required to be prime. - primeModulus :: Integer -> PrimeModulus --primeModulus = PrimeModulus . integerToBigNat -+primeModulus x = PrimeModulus (integerToBigNat x) - {-# INLINE primeModulus #-} - - ---- Barrett reduction replaces a division by the modulus with ---- two multiplications and some shifting, masking, and additions ---- (and some fairly negligible pre-processing). For the size of ---- moduli we are working with for ECC, this does not appear to be ---- a performance win. Even for largest NIST curve (P-521) Barrett ---- reduction is about 20% slower than naive modular reduction. ---- Smaller curves are worse WRT the baseline. -- ---- {-# INLINE primeModulus #-} ---- primeModulus :: Integer -> PrimeModulus ---- primeModulus = untrie modulusParameters -- ---- data PrimeModulus = PrimeModulus ---- { primeMod :: !Integer ---- , barrettInverse :: !Integer ---- , barrettK :: !Int ---- , barrettMask :: !Integer ---- } ---- deriving (Show, Eq) -- ---- {-# NOINLINE modulusParameters #-} ---- modulusParameters :: Integer :->: PrimeModulus ---- modulusParameters = trie computeModulusParameters -- ---- computeModulusParameters :: Integer -> PrimeModulus ---- computeModulusParameters p = PrimeModulus p inv k mask ---- where ---- k = fromInteger w -- ---- b :: Integer ---- b = 2 ^ (64::Int) -- ---- -- w is the number of 64-bit words required to express p ---- w = (widthInteger p + 63) `div` 64 -- ---- mask = b^(k+1) - 1 -- ---- -- inv = floor ( b^(2*k) / p ) ---- inv = b^(2*k) `div` p -- ---- barrettReduction :: PrimeModulus -> Integer -> Integer ---- barrettReduction p x = go r3 ---- where ---- m = primeMod p ---- k = barrettK p ---- inv = barrettInverse p ---- mask = barrettMask p -- ---- -- q1 <- floor (x / b^(k-1)) ---- q1 = x `shiftR` (64 * (k-1)) -- ---- -- q2 <- q1 * floor ( b^(2*k) / m ) ---- q2 = q1 * inv -- ---- -- q3 <- floor (q2 / b^(k+1)) ---- q3 = q2 `shiftR` (64 * (k+1)) -- ---- -- r1 <- x mod b^(k+1) ---- r1 = x .&. mask -- ---- -- r2 <- (q3 * m) mod b^(k+1) ---- r2 = (q3 * m) .&. mask -- ---- -- r3 <- r1 - r2 ---- r3 = r1 - r2 -- ---- -- up to 2 multiples of m must be removed ---- go z = if z > m then go (z - m) else z -- - -- | Modular addition of two values. The inputs are - -- required to be in reduced form, and will output - -- a value in reduced form. --mod_add :: PrimeModulus -> BigNat -> BigNat -> BigNat --mod_add p !x !y = -- case Integer.isNullBigNat# rmp of -- 0# -> rmp -- _ -> r -- where r = Integer.plusBigNat x y -- rmp = Integer.minusBigNat r (primeMod p) -+mod_add :: PrimeModulus -> BigNat# -> BigNat# -> BigNat# -+mod_add p x y = -+ let r = BN.bigNatAdd x y in -+ case BN.bigNatSub r (primeMod p) of -+ (# (# #) | #) -> r -+ (# | rmp #) -> rmp - - -- | Compute the "half" value of a modular integer. For a given input @x@ - -- this is a value @y@ such that @y+y == x@. Such values must exist - -- in @Z p@ when @p > 2@. The input @x@ is required to be in reduced form, - -- and will output a value in reduced form. --mod_half :: PrimeModulus -> BigNat -> BigNat --mod_half p !x = if Integer.testBitBigNat x 0# then qodd else qeven -+mod_half :: PrimeModulus -> BigNat# -> BigNat# -+mod_half p x = if BN.bigNatTestBit x 0 then qodd else qeven - where -- qodd = (Integer.plusBigNat x (primeMod p)) `Integer.shiftRBigNat` 1# -- qeven = x `Integer.shiftRBigNat` 1# -+ qodd = (BN.bigNatAdd x (primeMod p)) `BN.bigNatShiftR#` 1## -+ qeven = x `BN.bigNatShiftR#` 1## - - -- | Compute the modular multiplication of two input values. Currently, this - -- uses naive modular reduction, and does not require the inputs to be in - -- reduced form. The output is in reduced form. --mod_mul :: PrimeModulus -> BigNat -> BigNat -> BigNat --mod_mul p !x !y = (Integer.timesBigNat x y) `Integer.remBigNat` (primeMod p) -+mod_mul :: PrimeModulus -> BigNat# -> BigNat# -> BigNat# -+mod_mul p x y = (BN.bigNatMul x y) `BN.bigNatRem` (primeMod p) - - -- | Compute the modular difference of two input values. The inputs are - -- required to be in reduced form, and will output a value in reduced form. --mod_sub :: PrimeModulus -> BigNat -> BigNat -> BigNat --mod_sub p !x !y = mod_add p x (Integer.minusBigNat (primeMod p) y) -+mod_sub :: PrimeModulus -> BigNat# -> BigNat# -> BigNat# -+mod_sub p x y = mod_add p x (BN.bigNatSubUnsafe (primeMod p) y) - - -- | Compute the modular square of an input value @x@; that is, @x*x@. - -- The input is not required to be in reduced form, and the output - -- will be in reduced form. --mod_square :: PrimeModulus -> BigNat -> BigNat --mod_square p !x = Integer.sqrBigNat x `Integer.remBigNat` primeMod p -+mod_square :: PrimeModulus -> BigNat# -> BigNat# -+mod_square p x = BN.bigNatSqr x `BN.bigNatRem` primeMod p - - -- | Compute the modular scalar multiplication @2x = x+x@. - -- The input is required to be in reduced form and the output - -- will be in reduced form. --mul2 :: PrimeModulus -> BigNat -> BigNat --mul2 p !x = -- case Integer.isNullBigNat# rmp of -- 0# -> rmp -- _ -> r -- where -- r = x `Integer.shiftLBigNat` 1# -- rmp = Integer.minusBigNat r (primeMod p) -+mul2 :: PrimeModulus -> BigNat# -> BigNat# -+mul2 p x = -+ let r = x `BN.bigNatShiftL#` 1## in -+ case BN.bigNatSub r (primeMod p) of -+ (# (# #) | #) -> r -+ (# | rmp #) -> rmp - - -- | Compute the modular scalar multiplication @3x = x+x+x@. - -- The input is required to be in reduced form and the output - -- will be in reduced form. --mul3 :: PrimeModulus -> BigNat -> BigNat --mul3 p x = mod_add p x $! mul2 p x -+mul3 :: PrimeModulus -> BigNat# -> BigNat# -+mul3 p x = mod_add p x (mul2 p x) - - -- | Compute the modular scalar multiplication @4x = x+x+x+x@. - -- The input is required to be in reduced form and the output - -- will be in reduced form. --mul4 :: PrimeModulus -> BigNat -> BigNat --mul4 p x = mul2 p $! mul2 p x -+mul4 :: PrimeModulus -> BigNat# -> BigNat# -+mul4 p x = mul2 p (mul2 p x) - - -- | Compute the modular scalar multiplication @8x = x+x+x+x+x+x+x+x@. - -- The input is required to be in reduced form and the output - -- will be in reduced form. --mul8 :: PrimeModulus -> BigNat -> BigNat --mul8 p x = mul2 p $! mul4 p x -+mul8 :: PrimeModulus -> BigNat# -> BigNat# -+mul8 p x = mul2 p (mul4 p x) -+ - - -- | Compute the elliptic curve group doubling operation. - -- In other words, if @S@ is a projective point on a curve, -@@ -225,7 +165,7 @@ mul8 p x = mul2 p $! mul4 p x - -- reflected across the x axis. - ec_double :: PrimeModulus -> ProjectivePoint -> ProjectivePoint - ec_double p (ProjectivePoint sx sy sz) = -- if Integer.isZeroBigNat sz then zro else ProjectivePoint r18 r23 r13 -+ if BN.bigNatIsZero sz then zro else ProjectivePoint r18 r23 r13 - - where - r7 = mod_square p sz {- 7: t4 <- (t3)^2 -} -@@ -250,22 +190,23 @@ ec_double p (ProjectivePoint sx sy sz) = - -- case for adding points which might be the identity. - ec_add :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint - ec_add p s t -- | Integer.isZeroBigNat (pz s) = t -- | Integer.isZeroBigNat (pz t) = s -+ | BN.bigNatIsZero (pz s) = t -+ | BN.bigNatIsZero (pz t) = s - | otherwise = ec_add_nonzero p s t - {-# INLINE ec_add #-} - - -+ - -- | Compute the elliptic curve group subtraction operation, including the special - -- cases for subtracting points which might be the identity. - ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint - ec_sub p s t = ec_add p s u -- where u = t{ py = Integer.minusBigNat (primeMod p) (py t) } -+ where u = t{ py = BN.bigNatSubUnsafe (primeMod p) (py t) } - {-# INLINE ec_sub #-} - - - ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint --ec_negate p s = s{ py = Integer.minusBigNat (primeMod p) (py s) } -+ec_negate p s = s{ py = BN.bigNatSubUnsafe (primeMod p) (py s) } - {-# INLINE ec_negate #-} - - -- | Compute the elliptic curve group addition operation -@@ -280,8 +221,8 @@ ec_negate p s = s{ py = Integer.minusBigNat (primeMod p) (py s) } - -- which instead computes a tangent line to @S@ . - ec_add_nonzero :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint - ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) = -- if Integer.isZeroBigNat r13 then -- if Integer.isZeroBigNat r14 then -+ if BN.bigNatIsZero r13 then -+ if BN.bigNatIsZero r14 then - ec_double p s - else - zro -@@ -289,7 +230,7 @@ ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) = - ProjectivePoint r32 r37 r27 - - where -- tNormalized = Integer.eqBigNat tz Integer.oneBigNat -+ tNormalized = BN.bigNatIsOne tz - - tz2 = mod_square p tz - tz3 = mod_mul p tz tz2 -@@ -328,17 +269,17 @@ ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) = - -- be added many times. - ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint - ec_normalize p s@(ProjectivePoint x y z) -- | Integer.eqBigNat z Integer.oneBigNat = s -- | otherwise = ProjectivePoint x' y' Integer.oneBigNat -+ | BN.bigNatIsOne z = s -+ | otherwise = ProjectivePoint x' y' (BN.bigNatFromWord# 1##) - where - m = primeMod p - -- l = Integer.recipModBigNat z m -- l2 = Integer.sqrBigNat l -- l3 = Integer.timesBigNat l l2 -+ l = BN.sbignat_recip_mod 0# z m -+ l2 = BN.bigNatSqr l -+ l3 = BN.bigNatMul l l2 - -- x' = (Integer.timesBigNat x l2) `Integer.remBigNat` m -- y' = (Integer.timesBigNat y l3) `Integer.remBigNat` m -+ x' = (BN.bigNatMul x l2) `BN.bigNatRem` m -+ y' = (BN.bigNatMul y l3) `BN.bigNatRem` m - - - -- | Given an integer @k@ and a projective point @S@, compute -@@ -348,10 +289,10 @@ ec_mult :: PrimeModulus -> Integer -> ProjectivePoint -> ProjectivePoint - ec_mult p d s - | d == 0 = zro - | d == 1 = s -- | Integer.isZeroBigNat (pz s) = zro -+ | BN.bigNatIsZero (pz s) = zro - | otherwise = - case m of -- 0# -> panic "ec_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))] -+ 0# -> panic "ec_mult" ["modulus too large", show (bigNatToInteger (primeMod p))] - _ -> go m zro - - where -@@ -362,16 +303,18 @@ ec_mult p d s - h' = integerToBigNat h - - m = case widthInteger h of -- Integer.S# mint -> mint -+ BN.IS mint -> mint - _ -> 0# - -+ go :: Int# -> ProjectivePoint -> ProjectivePoint - go i !r - | tagToEnum# (i ==# 0#) = r - | otherwise = go (i -# 1#) r' - - where -- h_i = Integer.testBitBigNat h' i -- d_i = Integer.testBitBigNat d' i -+ wi = int2Word# i -+ h_i = isTrue# (BN.bigNatTestBit# h' wi) -+ d_i = isTrue# (BN.bigNatTestBit# d' wi) - - r' = if h_i then - if d_i then r2 else ec_add p r2 s' -@@ -395,26 +338,26 @@ normalizeForTwinMult :: - (ProjectivePoint, ProjectivePoint, ProjectivePoint, ProjectivePoint) - normalizeForTwinMult p s t - -- S == 0 && T == 0 -- | Integer.isZeroBigNat a && Integer.isZeroBigNat b = -+ | BN.bigNatIsZero a && BN.bigNatIsZero b = - (zro, zro, zro, zro) - - -- S == 0 && T != 0 -- | Integer.isZeroBigNat a = -+ | BN.bigNatIsZero a = - let tnorm = ec_normalize p t - in (zro, tnorm, tnorm, ec_negate p tnorm) - - -- T == 0 && S != 0 -- | Integer.isZeroBigNat b = -+ | BN.bigNatIsZero b = - let snorm = ec_normalize p s - in (snorm, zro, snorm, snorm) - - -- S+T == 0, both != 0 -- | Integer.isZeroBigNat c = -+ | BN.bigNatIsZero c = - let snorm = ec_normalize p s - in (snorm, ec_negate p snorm, zro, ec_double p snorm) - - -- S-T == 0, both != 0 -- | Integer.isZeroBigNat d = -+ | BN.bigNatIsZero d = - let snorm = ec_normalize p s - in (snorm, snorm, ec_double p snorm, zro) - -@@ -441,7 +384,7 @@ normalizeForTwinMult p s t - - abcd = mod_mul p a bcd - -- e = Integer.recipModBigNat abcd m -+ e = BN.sbignat_recip_mod 0# abcd m - - a_inv = mod_mul p e bcd - b_inv = mod_mul p e acd -@@ -460,11 +403,11 @@ normalizeForTwinMult p s t - d_inv2 = mod_square p d_inv - d_inv3 = mod_mul p d_inv d_inv2 - -- s' = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) Integer.oneBigNat -- t' = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) Integer.oneBigNat -+ s' = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) (BN.bigNatFromWord# 1##) -+ t' = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) (BN.bigNatFromWord# 1##) - -- spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) Integer.oneBigNat -- smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) Integer.oneBigNat -+ spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) (BN.bigNatFromWord# 1##) -+ smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) (BN.bigNatFromWord# 1##) - - - -- | Given an integer @j@ and a projective point @S@, together with -@@ -479,50 +422,50 @@ ec_twin_mult :: PrimeModulus -> - ProjectivePoint - ec_twin_mult p (integerToBigNat -> d0) s (integerToBigNat -> d1) t = - case m of -- 0# -> panic "ec_twin_mult" ["modulus too large", show (Integer.bigNatToInteger (primeMod p))] -+ 0# -> panic "ec_twin_mult" ["modulus too large", show (bigNatToInteger (primeMod p))] - _ -> go m init_c0 init_c1 zro - - where - (s',t',spt',smt') = normalizeForTwinMult p s t - -- m = case max 4 (widthInteger (Integer.bigNatToInteger (primeMod p))) of -- Integer.S# mint -> mint -+ m = case max 4 (widthInteger (bigNatToInteger (primeMod p))) of -+ BN.IS mint -> mint - _ -> 0# -- if `m` doesn't fit into an Int, should be impossible - - init_c0 = C False False (tst d0 (m -# 1#)) (tst d0 (m -# 2#)) (tst d0 (m -# 3#)) (tst d0 (m -# 4#)) - init_c1 = C False False (tst d1 (m -# 1#)) (tst d1 (m -# 2#)) (tst d1 (m -# 3#)) (tst d1 (m -# 4#)) - - tst x i -- | tagToEnum# (i >=# 0#) = Integer.testBitBigNat x i -+ | isTrue# (i >=# 0#) = isTrue# (BN.bigNatTestBit# x (int2Word# i)) - | otherwise = False - - f i = -- if tagToEnum# (i <# 18#) then -- if tagToEnum# (i <# 12#) then -- if tagToEnum# (i <# 4#) then -+ if isTrue# (i <# 18#) then -+ if isTrue# (i <# 12#) then -+ if isTrue# (i <# 4#) then - 12# - else - 14# - else -- if tagToEnum# (i <# 14#) then -+ if isTrue# (i <# 14#) then - 12# - else - 10# - else -- if tagToEnum# (i <# 22#) then -+ if isTrue# (i <# 22#) then - 9# - else -- if tagToEnum# (i <# 24#) then -+ if isTrue# (i <# 24#) then - 11# - else - 12# - -- go !k !c0 !c1 !r = if tagToEnum# (k <# 0#) then r else go (k -# 1#) c0' c1' r' -+ go !k !c0 !c1 !r = if isTrue# (k <# 0#) then r else go (k -# 1#) c0' c1' r' - where - h0 = cStateToH c0 - h1 = cStateToH c1 -- u0 = if tagToEnum# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#) -- u1 = if tagToEnum# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#) -+ u0 = if isTrue# (h0 <# f h1) then 0# else (if cHead c0 then -1# else 1#) -+ u1 = if isTrue# (h1 <# f h0) then 0# else (if cHead c1 then -1# else 1#) - c0' = cStateUpdate u0 c0 (tst d0 (k -# 5#)) - c1' = cStateUpdate u1 c1 (tst d1 (k -# 5#)) - -@@ -571,4 +514,4 @@ cStateUpdate :: Int# -> CState -> Bool -> CState - cStateUpdate u (C _ c1 c2 c3 c4 c5) e = - case u of - 0# -> C c1 c2 c3 c4 c5 e -- _ -> C (complement c1) c2 c3 c4 c5 e -+ _ -> C (not c1) c2 c3 c4 c5 e -diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs -index e41cba9e8..60123183a 100644 ---- a/src/Cryptol/TypeCheck/Solver/Numeric.hs -+++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs -@@ -9,8 +9,7 @@ import qualified Control.Monad.Fail as Fail - import Data.List (sortBy) - import Data.MemoTrie - --import qualified GHC.Integer.GMP.Internals as Integer -- -+import Math.NumberTheory.Primes.Testing (isPrime) - - import Cryptol.Utils.Patterns - import Cryptol.TypeCheck.Type hiding (tMul) -@@ -78,11 +77,6 @@ cryIsGeq i t1 t2 = - {-# NOINLINE primeTable #-} - primeTable :: Integer :->: Bool - primeTable = trie isPrime -- where -- isPrime i = -- case Integer.testPrimeInteger i 25# of -- 0# -> False -- _ -> True - - cryIsPrime :: Ctxt -> Type -> Solved - cryIsPrime _varInfo ty = - -From c69acab2a2da24d391cf23177c0d1b542307ebe5 Mon Sep 17 00:00:00 2001 -From: Rob Dockins <rdock...@galois.com> -Date: Wed, 14 Jul 2021 22:55:37 -0700 -Subject: [PATCH 2/2] Remove uses of `bigNatSubUnsafe`. This doesn't seem to - make a difference for the obeserved crash. - ---- - src/Cryptol/PrimeEC.hs | 9 +++++++-- - 1 file changed, 7 insertions(+), 2 deletions(-) - -diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs -index 11f96004c..33783e859 100644 ---- a/src/Cryptol/PrimeEC.hs -+++ b/src/Cryptol/PrimeEC.hs -@@ -118,7 +118,10 @@ mod_mul p x y = (BN.bigNatMul x y) `BN.bigNatRem` (primeMod p) - -- | Compute the modular difference of two input values. The inputs are - -- required to be in reduced form, and will output a value in reduced form. - mod_sub :: PrimeModulus -> BigNat# -> BigNat# -> BigNat# --mod_sub p x y = mod_add p x (BN.bigNatSubUnsafe (primeMod p) y) -+mod_sub p x y = -+ case BN.bigNatSub (primeMod p) y of -+ (# | y' #) -> mod_add p x y' -+ (# (# #) | #) -> x -- BOGUS! - - -- | Compute the modular square of an input value @x@; that is, @x*x@. - -- The input is not required to be in reduced form, and the output -@@ -201,7 +204,9 @@ ec_add p s t - -- cases for subtracting points which might be the identity. - ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint - ec_sub p s t = ec_add p s u -- where u = t{ py = BN.bigNatSubUnsafe (primeMod p) (py t) } -+ where u = case BN.bigNatSub (primeMod p) (py t) of -+ (# | y' #) -> t{ py = y' } -+ (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (bigNatToInteger (py t))] - {-# INLINE ec_sub #-} - -