[arch-commits] Commit in cryptol/trunk (PKGBUILD ghc9.patch)
Felix Yan
felixonmars at gemini.archlinux.org
Fri Jul 8 13:12:55 UTC 2022
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 <felixonmars at 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 <rdockins at 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 at 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 at 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 at . 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 at . Such values must exist
- -- in @Z p@ when @p > 2 at . 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 at .
- -- 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 at .
- -- 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 at .
- -- 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 at .
- -- 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 at .
- -- 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 <rdockins at 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 at .
- -- 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 #-}
-
-
More information about the arch-commits
mailing list