Date: Friday, January 21, 2022 @ 23:38:15
Author: felixonmars
Revision: 1112889
archrelease: copy trunk to community-staging-x86_64
Added:
cryptol/repos/community-staging-x86_64/
cryptol/repos/community-staging-x86_64/PKGBUILD
(from rev 1112888, cryptol/trunk/PKGBUILD)
cryptol/repos/community-staging-x86_64/ghc9.patch
(from rev 1112888, cryptol/trunk/ghc9.patch)
------------+
PKGBUILD | 50 +++
ghc9.patch | 809 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 859 insertions(+)
Copied: cryptol/repos/community-staging-x86_64/PKGBUILD (from rev 1112888,
cryptol/trunk/PKGBUILD)
===================================================================
--- community-staging-x86_64/PKGBUILD (rev 0)
+++ community-staging-x86_64/PKGBUILD 2022-01-21 23:38:15 UTC (rev 1112889)
@@ -0,0 +1,50 @@
+# Maintainer: Felix Yan <felixonm...@archlinux.org>
+
+pkgname=cryptol
+pkgver=2.12.0
+pkgrel=5
+pkgdesc="The Language of Cryptography"
+url="https://www.cryptol.net";
+license=("BSD")
+arch=('x86_64')
+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'
+ 'haskell-parameterized-utils' 'haskell-panic' 'haskell-prettyprinter'
'haskell-sbv'
+ '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')
+source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz";
+ ghc9.patch)
+sha512sums=('3e7a58de47e5ae1fdc5067b2bcca66c04ee06c71e84f890104b64c59d1cd125667a23f537c3afd0503c059c97f5d168e6afa0df4fdc6c1e9448aae434e616bc8'
+
'f41afa8f65b01aaa5fc92a6433ed09ae85e86f58cb86e64b72de7e6765b32835974cb998305235d5c1ed8ff1112595f61400e16bd2ffd16c578c0c499d02486b')
+
+prepare() {
+ cd $pkgname-$pkgver
+ patch -p1 -i ../ghc9.patch
+}
+
+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" \
+ --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid
--ghc-option=-fllvm \
+ -f-static -f-relocatable --ghc-option='-pie'
+ runhaskell Setup build $MAKEFLAGS
+ runhaskell Setup register --gen-script
+ runhaskell Setup unregister --gen-script
+ sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh
+ sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh
+}
+
+package() {
+ cd "${srcdir}/${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"
+ runhaskell Setup copy --destdir="${pkgdir}"
+ install -D -m644 LICENSE "$pkgdir"/usr/share/licenses/$pkgname/LICENSE
+ rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE
+}
Copied: cryptol/repos/community-staging-x86_64/ghc9.patch (from rev 1112888,
cryptol/trunk/ghc9.patch)
===================================================================
--- community-staging-x86_64/ghc9.patch (rev 0)
+++ community-staging-x86_64/ghc9.patch 2022-01-21 23:38:15 UTC (rev 1112889)
@@ -0,0 +1,809 @@
+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 #-}
+
+
