Date: Friday, July 16, 2021 @ 08:05:00 Author: felixonmars Revision: 977578
upgpkg: cryptol 2.11.0-36: rebuild with ghc 9.0.1 Added: cryptol/trunk/ghc9.patch Modified: cryptol/trunk/PKGBUILD ------------+ PKGBUILD | 11 ghc9.patch | 841 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 848 insertions(+), 4 deletions(-) Modified: PKGBUILD =================================================================== --- PKGBUILD 2021-07-16 07:43:50 UTC (rev 977577) +++ PKGBUILD 2021-07-16 08:05:00 UTC (rev 977578) @@ -2,12 +2,12 @@ pkgname=cryptol pkgver=2.11.0 -pkgrel=35 +pkgrel=36 pkgdesc="The Language of Cryptography" url="https://www.cryptol.net"; license=("BSD") arch=('x86_64') -depends=('ghc-libs' 'z3' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized' +depends=('ghc-libs' 'z3' 'haskell-arithmoi' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized' 'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-extra' 'haskell-gitrev' 'haskell-graphscc' 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie' 'haskell-monad-control' 'haskell-monadlib' 'haskell-optparse-applicative' @@ -15,11 +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' 'alex' 'happy' 'uusi') -source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz";) -sha512sums=('4e8e9dec727c02e76043ee390b91d0a740df747a8f49b2551686ac7db3cc0c94c36e20316b59e7e50e28b838f3f9bf7202095cf6ce683d83fd47826702381649') +source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz"; + ghc9.patch) +sha512sums=('4e8e9dec727c02e76043ee390b91d0a740df747a8f49b2551686ac7db3cc0c94c36e20316b59e7e50e28b838f3f9bf7202095cf6ce683d83fd47826702381649' + 'cf201d5d633101343399bb43e264e482e9f7e4615512ff658455772add3055d14571954f20ddf2cb2e35704c5638e7d2a3dab494bbb981229c519dcf88867e17') prepare() { cd $pkgname-$pkgver + patch -p1 -i ../ghc9.patch uusi -u sbv -u what4 $pkgname.cabal } Added: ghc9.patch =================================================================== --- ghc9.patch (rev 0) +++ ghc9.patch 2021-07-16 08:05:00 UTC (rev 977578) @@ -0,0 +1,841 @@ +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-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal +index f0f75d18e..4cd02c5e6 100644 +--- a/cryptol-remote-api/cryptol-remote-api.cabal ++++ b/cryptol-remote-api/cryptol-remote-api.cabal +@@ -49,7 +49,7 @@ common deps + cryptol >= 2.9.0, + directory, + filepath ^>= 1.4, +- lens >= 4.17 && < 4.20, ++ lens >= 4.17 && < 5.1, + mtl ^>= 2.2, + scientific ^>= 0.3, + text ^>= 1.2.3, +@@ -90,8 +90,7 @@ executable cryptol-remote-api + ghc-options: -threaded -rtsopts -with-rtsopts=-xb0x200000000 + + build-depends: +- cryptol-remote-api, +- sbv < 8.10 ++ cryptol-remote-api, sbv + + if os(linux) && flag(static) + ld-options: -static -pthread +@@ -108,7 +107,7 @@ executable cryptol-eval-server + build-depends: + cryptol-remote-api, + optparse-applicative, +- sbv < 8.10 ++ sbv + + if os(linux) && flag(static) + ld-options: -static -pthread +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 #-} + +
