From 889bfd65116b8817bd97b18e8a1e66db57c135cf Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 14 Jul 2021 22:44:53 -0700 Subject: [PATCH 01/15] 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, @@ -64,7 +65,7 @@ library parameterized-utils >= 2.0.2, pretty >= 1.1, process >= 1.2, - sbv >= 8.6 && < 8.15, + sbv >= 8.10 && < 8.16, simple-smt >= 0.7.1, stm >= 2.4, strict, 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 Date: Wed, 14 Jul 2021 22:55:37 -0700 Subject: [PATCH 02/15] 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 #-} From 2e32fcd6192358de3561575366f7adc297989e00 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 12 Jan 2022 09:40:20 -0500 Subject: [PATCH 03/15] Bump some upper version bounds for GHC 9.0 --- cabal.project | 4 ++++ cryptol-remote-api/cryptol-remote-api.cabal | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/cabal.project b/cabal.project index d8665fc91..e12f539f4 100644 --- a/cabal.project +++ b/cabal.project @@ -3,3 +3,7 @@ packages: cryptol-remote-api tests deps/argo/argo + +allow-newer: + -- See https://github.com/GaloisInc/test-lib/pull/2 + test-lib:base diff --git a/cryptol-remote-api/cryptol-remote-api.cabal b/cryptol-remote-api/cryptol-remote-api.cabal index 9dfcb34cf..c3bf422fe 100644 --- a/cryptol-remote-api/cryptol-remote-api.cabal +++ b/cryptol-remote-api/cryptol-remote-api.cabal @@ -40,7 +40,7 @@ common errors common deps build-depends: - base >=4.11.1.0 && <4.15, + base >=4.11.1.0 && <4.16, argo, aeson >= 1.4.2 && < 2.1, base64-bytestring >= 1.0, From 38935c0c513dee40114ce864af28181ea06af763 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 12 Jan 2022 09:40:35 -0500 Subject: [PATCH 04/15] CI: Test GHC 9.0.2 --- .github/workflows/ci.yml | 4 +- cabal.GHC-9.0.2.config | 310 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 313 insertions(+), 1 deletion(-) create mode 100644 cabal.GHC-9.0.2.config diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 00c6e8d9b..2fc38f51f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -52,13 +52,15 @@ jobs: fail-fast: false matrix: os: [ubuntu-latest, macos-latest, windows-latest] - ghc-version: ["8.6.5", "8.8.4", "8.10.2"] + ghc-version: ["8.6.5", "8.8.4", "8.10.2", "9.0.2"] exclude: # https://gitlab.haskell.org/ghc/ghc/-/issues/18550 - os: windows-latest ghc-version: 8.8.4 - os: windows-latest ghc-version: 8.10.2 + - os: windows-latest + ghc-version: 9.0.2 outputs: test-lib-json: ${{ steps.test-lib.outputs.targets-json }} env: diff --git a/cabal.GHC-9.0.2.config b/cabal.GHC-9.0.2.config new file mode 100644 index 000000000..821fb804e --- /dev/null +++ b/cabal.GHC-9.0.2.config @@ -0,0 +1,310 @@ +active-repositories: hackage.haskell.org:merge +constraints: any.Cabal ==3.4.1.0, + any.Glob ==0.10.2, + any.GraphSCC ==1.0.4, + GraphSCC -use-maps, + any.HUnit ==1.6.2.0, + any.MemoTrie ==0.6.10, + MemoTrie -examples, + any.OneTuple ==0.3.1, + any.Only ==0.1, + any.QuickCheck ==2.14.2, + QuickCheck -old-random +templatehaskell, + any.StateVar ==1.2.2, + any.abstract-deque ==0.3, + abstract-deque -usecas, + any.abstract-par ==0.3.3, + any.adjunctions ==4.4, + any.aeson ==2.0.3.0, + aeson -cffi +ordered-keymap, + any.alex ==3.2.6, + alex +small_base, + any.ansi-terminal ==0.11.1, + ansi-terminal -example, + any.ansi-wl-pprint ==0.6.9, + ansi-wl-pprint -example, + any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, + any.array ==0.5.4.0, + any.asn1-encoding ==0.9.6, + any.asn1-parse ==0.9.5, + any.asn1-types ==0.3.4, + any.assoc ==1.0.2, + any.async ==2.2.4, + async -bench, + any.attoparsec ==0.14.3, + attoparsec -developer, + any.auto-update ==0.1.6, + any.base ==4.15.1.0, + any.base-compat ==0.11.2, + any.base-compat-batteries ==0.11.2, + any.base-orphans ==0.8.6, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, + bifunctors +semigroups +tagged, + any.bimap ==0.4.0, + any.binary ==0.8.8.0, + any.binary-orphans ==1.0.2, + any.bitwise ==1.0.0.1, + any.blaze-builder ==0.4.2.2, + any.blaze-html ==0.9.1.2, + any.blaze-markup ==0.8.2.8, + any.bsb-http-chunked ==0.0.0.4, + any.bv-sized ==1.0.3, + any.byteorder ==1.0.4, + any.bytestring ==0.10.12.1, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, + any.case-insensitive ==1.2.1.0, + any.cassava ==0.5.2.0, + cassava -bytestring--lt-0_10_4, + any.cereal ==0.5.8.2, + cereal -bytestring-builder, + any.chimera ==0.3.2.0, + chimera +representable, + any.clock ==0.8.2, + clock -llvm, + any.code-page ==0.2.1, + any.colour ==2.3.6, + any.comonad ==5.0.8, + comonad +containers +distributive +indexed-traversable, + any.config-value ==0.8.2, + any.constraints ==0.13.2, + any.containers ==0.6.4.1, + any.contravariant ==1.5.5, + contravariant +semigroups +statevar +tagged, + any.cookie ==0.4.5, + any.criterion ==1.5.12.0, + criterion -embed-data-files -fast, + any.criterion-measurement ==0.1.3.0, + criterion-measurement -fast, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, + cryptol +relocatable -static, + cryptol-remote-api -notthreaded -static, + cryptol-test-runner -static, + any.cryptonite ==0.29, + cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, + any.data-binary-ieee754 ==0.4.4, + any.data-default-class ==0.1.2.0, + any.data-fix ==0.3.2, + any.deepseq ==1.4.5.0, + any.dense-linear-algebra ==0.1.0.0, + any.deriving-compat ==0.6, + deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, + any.directory ==1.3.6.2, + any.distributive ==0.6.2.1, + distributive +semigroups +tagged, + any.dlist ==1.0, + dlist -werror, + any.easy-file ==0.2.2, + any.entropy ==0.4.1.7, + entropy -halvm, + any.exact-pi ==0.5.0.1, + any.exceptions ==0.10.4, + any.extensible-exceptions ==0.1.1.4, + any.extra ==1.7.10, + any.fail ==4.9.0.0, + any.fast-logger ==3.1.0, + any.filelock ==0.1.1.5, + any.filepath ==1.4.2.1, + any.fingertree ==0.1.4.2, + any.free ==5.1.7, + any.ghc-bignum ==1.1, + any.ghc-boot-th ==9.0.2, + any.ghc-prim ==0.7.0, + any.gitrev ==1.3.1, + any.happy ==1.20.0, + any.hashable ==1.3.5.0, + hashable +integer-gmp -random-initial-seed, + any.hashtables ==1.2.4.2, + hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, + any.haskeline ==0.8.2, + any.heredoc ==0.2.0.0, + any.hostname ==1.0, + any.hourglass ==0.2.12, + any.hsc2hs ==0.68.8, + hsc2hs -in-ghc-tree, + any.http-date ==0.0.11, + any.http-types ==0.12.3, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, + any.integer-gmp ==1.1, + any.integer-logarithms ==1.0.3.1, + integer-logarithms -check-bounds +integer-gmp, + any.integer-roots ==1.0.2.0, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, + io-streams +network -nointeractivetests +zlib, + any.iproute ==1.7.12, + any.js-chart ==2.9.4.1, + any.kan-extensions ==5.2.3, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, + libBF -system-libbf, + any.math-functions ==0.3.4.2, + math-functions +system-erf +system-expm1, + any.megaparsec ==9.2.0, + megaparsec -dev, + any.memory ==0.16.0, + memory +support_basement +support_bytestring +support_deepseq +support_foundation, + any.microstache ==1.0.2, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.monad-control ==1.0.3.1, + any.monad-par ==0.3.5, + monad-par -chaselev -newgeneric, + any.monad-par-extras ==0.3.3, + any.monadLib ==3.10, + any.mtl ==2.2.2, + any.mwc-random ==0.15.0.2, + any.nats ==1.1.2, + nats +binary +hashable +template-haskell, + any.network ==3.1.2.5, + network -devel, + any.network-byte-order ==0.1.6, + any.network-info ==0.2.0.10, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, + any.old-locale ==1.0.0.7, + any.old-time ==1.1.0.3, + any.optparse-applicative ==0.16.1.0, + optparse-applicative +process, + any.panic ==0.4.0.1, + any.parallel ==3.2.2.0, + any.parameterized-utils ==2.1.4.0, + parameterized-utils +unsafe-operations, + any.parsec ==3.1.14.0, + any.parser-combinators ==1.3.0, + parser-combinators -dev, + any.pem ==0.2.4, + any.pretty ==1.1.3.6, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.primitive ==0.7.3.0, + any.process ==1.6.13.2, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, + quickcheck-instances -bytestring-builder, + any.random ==1.2.1, + any.reflection ==2.1.6, + reflection -slow +template-haskell, + any.regex-base ==0.94.0.2, + any.regex-compat ==0.95.2.1, + any.regex-posix ==0.96.0.1, + regex-posix -_regex-posix-clib, + any.resourcet ==1.2.4.3, + any.rts ==1.0.2, + any.safe ==0.3.19, + any.sbv ==8.16, + any.scientific ==0.3.7.0, + scientific -bytestring-builder -integer-simple, + any.scotty ==0.12, + any.semialign ==1.2.0.1, + semialign +semigroupoids, + any.semigroupoids ==5.3.6, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.20, + semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, + any.semirings ==0.6, + semirings +containers +unordered-containers, + any.silently ==1.2.5.2, + any.simple-get-opt ==0.4, + any.simple-sendfile ==0.2.30, + simple-sendfile +allow-bsd, + any.simple-smt ==0.9.7, + any.splitmix ==0.1.0.4, + splitmix -optimised-mixer, + any.statistics ==0.15.2.0, + any.stm ==2.5.0.0, + any.streaming-commons ==0.2.2.3, + streaming-commons -use-bytestring-builder, + any.strict ==0.4.0.1, + strict +assoc, + any.syb ==0.7.2.1, + any.tagged ==0.8.6.1, + tagged +deepseq +transformers, + any.tasty ==1.4.2.1, + tasty +clock +unix, + any.tasty-hunit ==0.10.0.3, + any.tasty-quickcheck ==0.10.2, + any.template-haskell ==2.17.0.0, + any.temporary ==1.3, + any.terminfo ==0.4.1.5, + any.test-framework ==0.8.2.0, + any.test-framework-hunit ==0.3.0.2, + test-framework-hunit -base3 +base4, + any.test-lib ==0.3, + any.text ==1.2.5.0, + any.text-short ==0.1.5, + text-short -asserts, + any.tf-random ==0.5, + any.th-abstraction ==0.4.3.0, + any.th-lift ==0.8.2, + any.th-lift-instances ==0.1.19, + any.these ==1.1.1.1, + these +assoc, + any.time ==1.9.3, + any.time-compat ==1.9.6.1, + time-compat -old-locale, + any.time-manager ==0.0.0, + any.tls ==1.5.6, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, + any.transformers ==0.5.6.2, + any.transformers-base ==0.4.6, + transformers-base +orphaninstances, + any.transformers-compat ==0.7.1, + transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, + any.type-equality ==1, + any.unbounded-delays ==0.1.1.1, + any.uniplate ==1.6.13, + any.unix ==2.7.2.2, + any.unix-compat ==0.5.3, + unix-compat -old-time, + any.unix-time ==0.4.7, + any.unliftio ==0.2.20, + any.unliftio-core ==0.2.0.1, + any.unordered-containers ==0.2.16.0, + unordered-containers -debug, + any.utf8-string ==1.0.2, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, + any.vault ==0.3.1.5, + vault +useghc, + any.vector ==0.12.3.1, + vector +boundschecks -internalchecks -unsafechecks -wall, + any.vector-algorithms ==0.8.0.4, + vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.1, + any.void ==0.7.3, + void -safe, + any.wai ==3.2.3, + any.wai-extra ==3.1.8, + wai-extra -build-example, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, + warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, + any.wcwidth ==0.0.2, + wcwidth -cli +split-base, + any.what4 ==1.2.1, + what4 -drealtestdisable -solvertests -stptestdisable, + any.witherable ==0.4.2, + any.word8 ==0.1.3, + any.x509 ==1.7.5, + any.x509-store ==1.6.7, + any.x509-validation ==1.6.11, + any.xml ==1.3.14, + any.zenc ==0.1.2, + any.zlib ==0.6.2.3, + zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, + any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2022-01-06T13:38:03Z From 7bdb84beca224968b3262128419588601adde8cd Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 09:47:10 -0500 Subject: [PATCH 05/15] CI: Drop GHC 8.6 --- .github/workflows/ci.yml | 6 +- README.md | 4 +- cabal.GHC-8.6.5.config | 224 --------------------------------------- 3 files changed, 5 insertions(+), 229 deletions(-) delete mode 100644 cabal.GHC-8.6.5.config diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2fc38f51f..ac2e65c44 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -52,7 +52,7 @@ jobs: fail-fast: false matrix: os: [ubuntu-latest, macos-latest, windows-latest] - ghc-version: ["8.6.5", "8.8.4", "8.10.2", "9.0.2"] + ghc-version: ["8.8.4", "8.10.2", "9.0.2"] exclude: # https://gitlab.haskell.org/ghc/ghc/-/issues/18550 - os: windows-latest @@ -188,13 +188,13 @@ jobs: if-no-files-found: error retention-days: ${{ needs.config.outputs.retention-days }} - - if: matrix.ghc-version == '8.6.5' + - if: matrix.ghc-version == '8.8.4' uses: actions/upload-artifact@v2 with: path: dist/bin name: ${{ runner.os }}-dist-bin - - if: matrix.ghc-version == '8.6.5' + - if: matrix.ghc-version == '8.8.4' uses: actions/upload-artifact@v2 with: path: bin diff --git a/README.md b/README.md index d33affc97..1ee69d36f 100644 --- a/README.md +++ b/README.md @@ -81,8 +81,8 @@ Windows. We regularly build and test it in the following environments: ## Prerequisites Cryptol is regularly built and tested with the three most recent -versions of GHC, which at the time of this writing are 8.6.5, 8.8.4, and -8.10.2. The easiest way to install an approporiate version of GHC is +versions of GHC, which at the time of this writing are 8.8.4, 8.10.2, and +9.0.2. The easiest way to install an approporiate version of GHC is with [ghcup](https://www.haskell.org/ghcup/). Some supporting non-Haskell libraries are required to build diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config deleted file mode 100644 index 50a7b7fb1..000000000 --- a/cabal.GHC-8.6.5.config +++ /dev/null @@ -1,224 +0,0 @@ -constraints: any.Cabal ==2.4.0.1, - any.FloatingHex ==0.4, - any.Glob ==0.10.0, - any.GraphSCC ==1.0.4, - GraphSCC -use-maps, - any.HUnit ==1.6.0.0, - any.Only ==0.1, - any.QuickCheck ==2.14, - QuickCheck +templatehaskell, - any.StateVar ==1.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, - any.aeson ==1.4.7.1, - aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.5, - alex +small_base, - any.ansi-terminal ==0.10.3, - ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, - any.array ==0.5.3.0, - any.async ==2.2.2, - async -bench, - any.attoparsec ==0.13.2.4, - attoparsec -developer, - any.base ==4.12.0.0, - any.base-compat ==0.11.1, - any.base-compat-batteries ==0.11.1, - any.base-orphans ==0.8.2, - any.bifunctors ==5.5.7, - bifunctors +semigroups +tagged, - any.bimap ==0.4.0, - any.binary ==0.8.6.0, - any.binary-orphans ==1.0.1, - any.blaze-builder ==0.4.1.0, - any.blaze-html ==0.9.1.2, - any.blaze-markup ==0.8.2.5, - any.bv-sized ==1.0.2, - any.bytestring ==0.10.8.2, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.2.0, - any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, - cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, - cereal -bytestring-builder, - any.clock ==0.8, - clock -llvm, - any.code-page ==0.2, - any.colour ==2.3.5, - any.comonad ==5.0.6, - comonad +containers +distributive +test-doctests, - any.concurrent-output ==1.10.11, - any.constraints ==0.11.2, - any.containers ==0.6.0.1, - any.contravariant ==1.5.2, - contravariant +semigroups +statevar +tagged, - any.crackNum ==2.3, - any.criterion ==1.5.6.2, - criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, - criterion-measurement -fast, - any.cryptohash-sha1 ==0.11.100.1, - cryptol +relocatable -static, - cryptol-test-runner -static, - any.data-binary-ieee754 ==0.4.4, - any.data-default-class ==0.1.2.0, - any.deepseq ==1.4.4.0, - any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.8, - deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, - any.directory ==1.3.3.0, - any.distributive ==0.6.2, - distributive +semigroups +tagged, - any.dlist ==0.8.0.8, - any.erf ==2.0.0.0, - any.exceptions ==0.10.4, - exceptions +transformers-0-4, - any.extensible-exceptions ==0.1.1.4, - any.extra ==1.7.1, - any.fail ==4.9.0.0, - any.filepath ==1.4.2.1, - any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, - generic-deriving +base-4-9, - any.ghc ==8.6.5, - any.ghc-boot ==8.6.5, - any.ghc-boot-th ==8.6.5, - any.ghc-heap ==8.6.5, - any.ghc-prim ==0.5.3, - any.ghci ==8.6.5, - any.gitrev ==1.3.1, - any.happy ==1.19.12, - happy +small_base, - any.hashable ==1.3.0.0, - hashable -examples +integer-gmp +sse2 -sse41, - any.hashtables ==1.2.3.4, - hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.7.4.3, - any.haskell-lexer ==1.1, - any.hedgehog ==1.0.2, - any.heredoc ==0.2.0.0, - any.hostname ==1.0, - any.hpc ==0.6.0.3, - hsc2hs -in-ghc-tree, - any.integer-gmp ==1.0.2.0, - any.integer-logarithms ==1.0.3, - integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.5.3, - any.io-streams ==1.5.1.0, - io-streams -nointeractivetests, - any.js-flot ==0.8.3, - any.js-jquery ==3.3.1, - any.kan-extensions ==5.2, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.lifted-async ==0.10.0.6, - any.lifted-base ==0.2.3.12, - any.math-functions ==0.3.3.0, - math-functions +system-erf +system-expm1, - any.megaparsec ==8.0.0, - megaparsec -dev, - any.microstache ==1.0.1.1, - any.mmorph ==1.1.3, - any.monad-control ==1.0.2.3, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, - any.monadLib ==3.10, - any.mtl ==2.2.2, - any.mwc-random ==0.14.0.0, - any.old-locale ==1.0.0.7, - any.optparse-applicative ==0.15.1.0, - any.panic ==0.4.0.1, - any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.0, - parameterized-utils +unsafe-operations, - any.parsec ==3.1.13.0, - any.parser-combinators ==1.2.1, - parser-combinators -dev, - any.pretty ==1.1.3.6, - any.pretty-show ==1.10, - any.primitive ==0.7.0.1, - any.process ==1.6.5.0, - any.profunctors ==5.5.2, - any.random ==1.1, - any.reflection ==2.1.5, - reflection -slow +template-haskell, - any.regex-base ==0.94.0.0, - any.regex-posix ==0.96.0.0, - any.resourcet ==1.2.4, - any.rts ==1.0, - any.sbv ==8.6, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, - scientific -bytestring-builder -integer-simple, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, - semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, - any.simple-get-opt ==0.4, - any.simple-smt ==0.9.7, - any.splitmix ==0.0.4, - splitmix -optimised-mixer +random, - any.statistics ==0.15.2.0, - any.stm ==2.5.0.0, - any.strict ==0.3.2, - strict +split-base, - any.syb ==0.7.1, - any.tagged ==0.8.6, - tagged +deepseq +transformers, - any.tasty ==1.2.3, - tasty +clock, - any.tasty-hedgehog ==1.0.0.2, - any.tasty-hunit ==0.10.0.2, - any.template-haskell ==2.14.0.0, - any.temporary ==1.3, - any.terminal-size ==0.3.2.1, - any.test-framework ==0.8.2.0, - any.test-framework-hunit ==0.3.0.2, - test-framework-hunit -base3 +base4, - any.test-lib ==0.3, - any.text ==1.2.4.0, - any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, - any.time ==1.8.0.2, - any.time-compat ==1.9.3, - time-compat -old-locale, - any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, - transformers-base +orphaninstances, - any.transformers-compat ==0.6.5, - transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, - any.type-equality ==1, - any.unbounded-delays ==0.1.1.0, - any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.10.0, - unordered-containers -debug, - any.utf8-string ==1.0.1.1, - any.uuid-types ==1.0.3, - any.vector ==0.12.1.2, - vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.3, - vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.7, - any.versions ==4.0.2, - any.void ==0.7.3, - void -safe, - any.wcwidth ==0.0.2, - wcwidth -cli +split-base, - any.what4 ==1.2.1, - what4 -drealtestdisable -solvertests -stptestdisable, - any.wl-pprint-annotated ==0.1.0.1, - any.xml ==1.3.14, - any.zenc ==0.1.1, - any.zlib ==0.6.2.1, - zlib -non-blocking-ffi -pkg-config, - any.zlib-bindings ==0.1.1.5 From 1181076f1f9c8f3b5e1993b19c1f7a85e166ff39 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 12:13:40 -0500 Subject: [PATCH 06/15] Factor out compatibility shims into GHC.Num.Compat --- cryptol.cabal | 9 +- src/Cryptol/Backend/Concrete.hs | 6 +- src/Cryptol/Backend/SBV.hs | 6 +- src/Cryptol/Backend/What4.hs | 8 +- src/Cryptol/Eval/Reference.lhs | 6 +- src/Cryptol/PrimeEC.hs | 68 +++++++-------- src/GHC/Num/Compat.hs | 149 ++++++++++++++++++++++++++++++++ 7 files changed, 200 insertions(+), 52 deletions(-) create mode 100644 src/GHC/Num/Compat.hs diff --git a/cryptol.cabal b/cryptol.cabal index 4f908da84..e65b1579d 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -41,6 +41,7 @@ library Default-language: Haskell2010 Build-depends: base >= 4.8 && < 5, + arithmoi >= 0.12, async >= 2.2 && < 2.3, base-compat >= 0.6 && < 0.12, bv-sized >= 1.0 && < 1.1, @@ -56,8 +57,6 @@ library ghc-prim, GraphSCC >= 1.0.4, heredoc >= 0.2, - ghc-bignum, - arithmoi, libBF >= 0.6 && < 0.7, MemoTrie >= 0.6 && < 0.7, monad-control >= 1.0, @@ -77,6 +76,11 @@ library panic >= 0.3, what4 >= 1.2 && < 1.3 + if impl(ghc >= 9.0) + build-depends: ghc-bignum >= 1.0 && < 1.3 + else + build-depends: integer-gmp >= 1.0 && < 1.1 + Build-tool-depends: alex:alex, happy:happy hs-source-dirs: src @@ -202,6 +206,7 @@ library Other-modules: Cryptol.Parser.LexerUtils, Cryptol.Parser.ParserUtils, Cryptol.Prelude, + GHC.Num.Compat, Paths_cryptol, GitRev diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs index 466e51d6c..33b83246d 100644 --- a/src/Cryptol/Backend/Concrete.hs +++ b/src/Cryptol/Backend/Concrete.hs @@ -42,7 +42,7 @@ import Data.Bits import Data.Ratio import Numeric (showIntAtBase) import qualified LibBF as FP -import qualified GHC.Num.Integer as Integer +import qualified GHC.Num.Compat as Integer import qualified Cryptol.Backend.Arch as Arch import qualified Cryptol.Backend.FloatHelpers as FP @@ -343,8 +343,8 @@ instance Backend Concrete where -- the only values for which no inverse exists are -- congruent to 0 modulo m. znRecip sym m x = - case Integer.integerRecipMod# x (Integer.integerToNaturalClamp m) of - (# r | #) -> integerLit sym (toInteger r) + case Integer.integerRecipMod x m of + (# r | #) -> integerLit sym r (# | () #) -> raiseError sym DivideByZero znPlus _ = liftBinIntMod (+) diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs index 90341b14b..d036e1625 100644 --- a/src/Cryptol/Backend/SBV.hs +++ b/src/Cryptol/Backend/SBV.hs @@ -40,7 +40,7 @@ import Control.Monad.IO.Class (MonadIO(..)) import Data.Bits (bit, complement) import Data.List (foldl') -import qualified GHC.Num.Integer as Integer +import qualified GHC.Num.Compat as Integer import Data.SBV.Dynamic as SBV import qualified Data.SBV.Internals as SBV @@ -431,8 +431,8 @@ 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 - = case Integer.integerRecipMod# xi (Integer.integerToNaturalClamp m) of - (# r | #) -> integerLit sym (toInteger r) + = case Integer.integerRecipMod xi m of + (# r | #) -> integerLit sym r (# | () #) -> raiseError sym DivideByZero -- If the input is symbolic, create a new symbolic constant diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs index 699fe1ab9..7d49a098f 100644 --- a/src/Cryptol/Backend/What4.hs +++ b/src/Cryptol/Backend/What4.hs @@ -30,7 +30,7 @@ import Data.Text (Text) import Data.Parameterized.NatRepr import Data.Parameterized.Some -import qualified GHC.Num.Integer as Integer +import qualified GHC.Num.Compat as Integer import qualified What4.Interface as W4 import qualified What4.SWord as SW @@ -343,7 +343,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where wordMult sym x y = liftIO (SW.bvMul (w4 sym) x y) wordNegate sym x = liftIO (SW.bvNeg (w4 sym) x) wordLg2 sym x = sLg2 (w4 sym) x - + wordShiftLeft sym x y = w4bvShl (w4 sym) x y wordShiftRight sym x y = w4bvLshr (w4 sym) x y wordRotateLeft sym x y = w4bvRol (w4 sym) x y @@ -670,8 +670,8 @@ 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 - = case Integer.integerRecipMod# xi (Integer.integerToNaturalClamp m) of - (# r | #) -> integerLit sym (toInteger r) + = case Integer.integerRecipMod xi m of + (# r | #) -> integerLit sym r (# | () #) -> raiseError sym DivideByZero -- If the input is symbolic, create a new symbolic constant diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index d5d91b77b..9771e7de1 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -33,7 +33,7 @@ > import qualified Data.Text as T (pack) > import LibBF (BigFloat) > import qualified LibBF as FP -> import qualified GHC.Num.Integer as Integer +> import qualified GHC.Num.Compat as Integer > > import Cryptol.ModuleSystem.Name (asPrim) > import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul) @@ -1334,8 +1334,8 @@ confused with integral division). > > zRecip :: Integer -> Integer -> E Integer > zRecip m x = -> case Integer.integerRecipMod# x (Integer.integerToNaturalClamp m) of -> (# r | #) -> pure (toInteger r) +> case Integer.integerRecipMod x m of +> (# r | #) -> pure r > (# | () #) -> cryError DivideByZero > > zDiv :: Integer -> Integer -> Integer -> E Integer diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index 33783e859..cfd1d631b 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -29,8 +29,8 @@ module Cryptol.PrimeEC , primeModulus , ProjectivePoint(..) , toProjectivePoint - , integerToBigNat - , bigNatToInteger + , BN.integerToBigNat + , BN.bigNatToInteger , ec_double , ec_add_nonzero @@ -39,12 +39,15 @@ module Cryptol.PrimeEC ) where +{- 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 GHC.Types +-} +import GHC.Num.Compat (BigNat#) +import qualified GHC.Num.Compat as BN +import GHC.Exts import Cryptol.TypeCheck.Solver.InfNat (widthInteger) import Cryptol.Utils.Panic @@ -61,20 +64,12 @@ data ProjectivePoint = toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint toProjectivePoint x y z = - ProjectivePoint (integerToBigNat x) (integerToBigNat y) (integerToBigNat z) + ProjectivePoint (BN.integerToBigNat x) (BN.integerToBigNat y) (BN.integerToBigNat z) -- | The projective "point at infinity", which represents the zero element -- of the ECC group. zro :: ProjectivePoint -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 = BN.integerToBigNatClamp# - -bigNatToInteger :: BigNat# -> Integer -bigNatToInteger = BN.integerFromBigNat# +zro = ProjectivePoint (BN.oneBigNat (# #)) (BN.oneBigNat (# #)) (BN.zeroBigNat (# #)) -- | Simple newtype wrapping the @BigNat@ value of the -- modulus of the underlying field Z p. This modulus @@ -85,7 +80,7 @@ newtype PrimeModulus = PrimeModulus { primeMod :: BigNat# } -- | Inject an integer value into the @PrimeModulus@ type. -- This modulus is required to be prime. primeModulus :: Integer -> PrimeModulus -primeModulus x = PrimeModulus (integerToBigNat x) +primeModulus x = PrimeModulus (BN.integerToBigNat x) {-# INLINE primeModulus #-} @@ -104,10 +99,10 @@ mod_add p x y = -- 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 BN.bigNatTestBit x 0 then qodd else qeven +mod_half p x = if BN.testBitBigNat x 0# then qodd else qeven where - qodd = (BN.bigNatAdd x (primeMod p)) `BN.bigNatShiftR#` 1## - qeven = x `BN.bigNatShiftR#` 1## + qodd = (BN.bigNatAdd x (primeMod p)) `BN.shiftRBigNat` 1# + qeven = x `BN.shiftRBigNat` 1# -- | Compute the modular multiplication of two input values. Currently, this -- uses naive modular reduction, and does not require the inputs to be in @@ -134,7 +129,7 @@ mod_square p x = BN.bigNatSqr x `BN.bigNatRem` primeMod p -- will be in reduced form. mul2 :: PrimeModulus -> BigNat# -> BigNat# mul2 p x = - let r = x `BN.bigNatShiftL#` 1## in + let r = x `BN.shiftLBigNat` 1# in case BN.bigNatSub r (primeMod p) of (# (# #) | #) -> r (# | rmp #) -> rmp @@ -206,7 +201,7 @@ ec_sub :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint ec_sub p s t = ec_add p s u where u = case BN.bigNatSub (primeMod p) (py t) of (# | y' #) -> t{ py = y' } - (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (bigNatToInteger (py t))] + (# (# #) | #) -> panic "ec_sub" ["cooridnate not in reduced form!", show (BN.bigNatToInteger (py t))] {-# INLINE ec_sub #-} @@ -275,11 +270,11 @@ ec_add_nonzero p s@(ProjectivePoint sx sy sz) (ProjectivePoint tx ty tz) = ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint ec_normalize p s@(ProjectivePoint x y z) | BN.bigNatIsOne z = s - | otherwise = ProjectivePoint x' y' (BN.bigNatFromWord# 1##) + | otherwise = ProjectivePoint x' y' (BN.oneBigNat (# #)) where m = primeMod p - l = BN.sbignat_recip_mod 0# z m + l = BN.recipModBigNat z m l2 = BN.bigNatSqr l l3 = BN.bigNatMul l l2 @@ -297,15 +292,15 @@ ec_mult p d s | BN.bigNatIsZero (pz s) = zro | otherwise = case m of - 0# -> panic "ec_mult" ["modulus too large", show (bigNatToInteger (primeMod p))] + 0# -> panic "ec_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))] _ -> go m zro where s' = ec_normalize p s h = 3*d - d' = integerToBigNat d - h' = integerToBigNat h + d' = BN.integerToBigNat d + h' = BN.integerToBigNat h m = case widthInteger h of BN.IS mint -> mint @@ -317,9 +312,8 @@ ec_mult p d s | otherwise = go (i -# 1#) r' where - wi = int2Word# i - h_i = isTrue# (BN.bigNatTestBit# h' wi) - d_i = isTrue# (BN.bigNatTestBit# d' wi) + h_i = BN.testBitBigNat h' i + d_i = BN.testBitBigNat d' i r' = if h_i then if d_i then r2 else ec_add p r2 s' @@ -389,7 +383,7 @@ normalizeForTwinMult p s t abcd = mod_mul p a bcd - e = BN.sbignat_recip_mod 0# abcd m + e = BN.recipModBigNat abcd m a_inv = mod_mul p e bcd b_inv = mod_mul p e acd @@ -408,11 +402,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) (BN.bigNatFromWord# 1##) - t' = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) (BN.bigNatFromWord# 1##) + s' = ProjectivePoint (mod_mul p (px s) a_inv2) (mod_mul p (py s) a_inv3) (BN.oneBigNat (# #)) + t' = ProjectivePoint (mod_mul p (px t) b_inv2) (mod_mul p (py t) b_inv3) (BN.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##) + spt' = ProjectivePoint (mod_mul p (px spt) c_inv2) (mod_mul p (py spt) c_inv3) (BN.oneBigNat (# #)) + smt' = ProjectivePoint (mod_mul p (px smt) d_inv2) (mod_mul p (py smt) d_inv3) (BN.oneBigNat (# #)) -- | Given an integer @j@ and a projective point @S@, together with @@ -425,15 +419,15 @@ ec_twin_mult :: PrimeModulus -> Integer -> ProjectivePoint -> Integer -> ProjectivePoint -> ProjectivePoint -ec_twin_mult p (integerToBigNat -> d0) s (integerToBigNat -> d1) t = +ec_twin_mult p (BN.integerToBigNat -> d0) s (BN.integerToBigNat -> d1) t = case m of - 0# -> panic "ec_twin_mult" ["modulus too large", show (bigNatToInteger (primeMod p))] + 0# -> panic "ec_twin_mult" ["modulus too large", show (BN.bigNatToInteger (primeMod p))] _ -> go m init_c0 init_c1 zro where (s',t',spt',smt') = normalizeForTwinMult p s t - m = case max 4 (widthInteger (bigNatToInteger (primeMod p))) of + m = case max 4 (widthInteger (BN.bigNatToInteger (primeMod p))) of BN.IS mint -> mint _ -> 0# -- if `m` doesn't fit into an Int, should be impossible @@ -441,7 +435,7 @@ ec_twin_mult p (integerToBigNat -> d0) s (integerToBigNat -> d1) t = init_c1 = C False False (tst d1 (m -# 1#)) (tst d1 (m -# 2#)) (tst d1 (m -# 3#)) (tst d1 (m -# 4#)) tst x i - | isTrue# (i >=# 0#) = isTrue# (BN.bigNatTestBit# x (int2Word# i)) + | isTrue# (i >=# 0#) = BN.testBitBigNat x i | otherwise = False f i = diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs new file mode 100644 index 000000000..18adca6d6 --- /dev/null +++ b/src/GHC/Num/Compat.hs @@ -0,0 +1,149 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE UnboxedSums #-} +{-# LANGUAGE UnboxedTuples #-} + +-- | +-- Module : GHC.Num.Compat +-- Description : Defines numeric compatibility shims that work with both +-- ghc-bignum (GHC 9.0+) and integer-gmp (older GHCs). +-- Copyright : (c) 2021 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +module GHC.Num.Compat + ( -- * BigNat# + BigNat# + , bigNatAdd + , bigNatIsOne + , bigNatIsZero + , bigNatMul + , bigNatRem + , bigNatSqr + , bigNatSub + , bigNatSubUnsafe + , oneBigNat + , recipModBigNat + , shiftLBigNat + , shiftRBigNat + , testBitBigNat + , zeroBigNat + + -- * Integer + , Integer(IS, IP, IN) + , integerRecipMod + + -- * Conversions + , bigNatToInteger + , integerToBigNat + ) where + +#if defined(MIN_VERSION_ghc_bignum) +import GHC.Num.BigNat (BigNat#, bigNatAdd, bigNatIsOne, bigNatIsZero, bigNatMul, bigNatRem, bigNatSqr, bigNatSub, bigNatSubUnsafe) +import qualified GHC.Num.Backend as BN +import qualified GHC.Num.BigNat as BN +import GHC.Num.Integer (Integer(IS, IP, IN)) +import qualified GHC.Num.Integer as Integer +import GHC.Exts + +-- | Coerce a @BigNat#@ to an integer value. +bigNatToInteger :: BigNat# -> Integer +bigNatToInteger = Integer.integerFromBigNat# + +integerRecipMod :: Integer -> Integer -> (# Integer | () #) +integerRecipMod x y = + case Integer.integerRecipMod# x (Integer.integerToNaturalClamp y) of + (# r | #) -> (# toInteger r | #) + (# | () #) -> (# | () #) + +-- | 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.integerToBigNatClamp# + +-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk. +oneBigNat :: (# #) -> BigNat# +oneBigNat _ = BN.bigNatFromWord# 1## + +recipModBigNat :: BigNat# -> BigNat# -> BigNat# +recipModBigNat = BN.sbignat_recip_mod 0# + +shiftLBigNat :: BigNat# -> Int# -> BigNat# +shiftLBigNat bn i = BN.bigNatShiftL# bn (int2Word# i) + +shiftRBigNat :: BigNat# -> Int# -> BigNat# +shiftRBigNat bn i = BN.bigNatShiftR# bn (int2Word# i) + +testBitBigNat :: BigNat# -> Int# -> Bool +testBitBigNat bn i = isTrue# (BN.bigNatTestBit# bn (int2Word# i)) + +-- Top-level unlifted bindings aren't allowed, so we fake one with a thunk. +zeroBigNat :: (# #) -> BigNat# +zeroBigNat _ = BN.bigNatFromWord# 0## +#else +import GHC.Integer.GMP.Internals (bigNatToInteger, recipModBigNat, shiftLBigNat, shiftRBigNat, testBitBigNat) +import qualified GHC.Integer.GMP.Internals as GMP +import GHC.Exts + +type BigNat# = GMP.BigNat + +{-# COMPLETE IS, IP, IN #-} + +pattern IS :: Int# -> Integer +pattern IS i = GMP.S# i + +pattern IP :: ByteArray# -> Integer +pattern IP ba = GMP.Jp# (GMP.BN# ba) + +pattern IN :: ByteArray# -> Integer +pattern IN ba = GMP.Jn# (GMP.BN# ba) + +bigNatAdd :: BigNat# -> BigNat# -> BigNat# +bigNatAdd = GMP.plusBigNat + +bigNatIsOne :: BigNat# -> Bool +bigNatIsOne bn = GMP.eqBigNat bn GMP.oneBigNat + +bigNatIsZero :: BigNat# -> Bool +bigNatIsZero = GMP.isZeroBigNat + +bigNatMul :: BigNat# -> BigNat# -> BigNat# +bigNatMul = GMP.timesBigNat + +bigNatRem :: BigNat# -> BigNat# -> BigNat# +bigNatRem = GMP.remBigNat + +bigNatSqr :: BigNat# -> BigNat# +bigNatSqr = GMP.sqrBigNat + +bigNatSub :: BigNat# -> BigNat# -> (# (# #) | BigNat# #) +bigNatSub x y = + case GMP.isNullBigNat# res of + 0# -> (# | res #) + _ -> (# (# #) | #) + where + res = GMP.minusBigNat x y + +bigNatSubUnsafe :: BigNat# -> BigNat# -> BigNat# +bigNatSubUnsafe = GMP.minusBigNat + +integerToBigNat :: Integer -> BigNat# +integerToBigNat (GMP.S# i) = GMP.wordToBigNat (int2Word# i) +integerToBigNat (GMP.Jp# b) = b +integerToBigNat (GMP.Jn# b) = b + +integerRecipMod :: Integer -> Integer -> (# Integer | () #) +integerRecipMod x y + | res == 0 = (# | () #) + | otherwise = (# res | #) + where + res = GMP.recipModInteger x y + +oneBigNat :: (##) -> BigNat# +oneBigNat _ = GMP.oneBigNat + +zeroBigNat :: (##) -> BigNat# +zeroBigNat _ = GMP.zeroBigNat +#endif From 31ca666b3a67858b5dcbd185f87c0012ef3b5a35 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 12:16:10 -0500 Subject: [PATCH 07/15] Regenerate cabal.GHC-*.config files --- .github/workflows/ci.yml | 6 +- README.md | 2 +- cabal.GHC-8.10.2.config | 228 ------------- ...C-8.10.3.config => cabal.GHC-8.10.7.config | 260 +++++++------- cabal.GHC-8.8.4.config | 321 +++++++++++------- 5 files changed, 352 insertions(+), 465 deletions(-) delete mode 100644 cabal.GHC-8.10.2.config rename cabal.GHC-8.10.3.config => cabal.GHC-8.10.7.config (56%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ac2e65c44..2e6e2ef37 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -52,13 +52,13 @@ jobs: fail-fast: false matrix: os: [ubuntu-latest, macos-latest, windows-latest] - ghc-version: ["8.8.4", "8.10.2", "9.0.2"] + ghc-version: ["8.8.4", "8.10.7", "9.0.2"] exclude: # https://gitlab.haskell.org/ghc/ghc/-/issues/18550 - os: windows-latest ghc-version: 8.8.4 - os: windows-latest - ghc-version: 8.10.2 + ghc-version: 8.10.7 - os: windows-latest ghc-version: 9.0.2 outputs: @@ -238,7 +238,7 @@ jobs: - uses: haskell/actions/setup@v1 with: - ghc-version: '8.10.3' + ghc-version: '8.10.7' - if: matrix.suite == 'rpc' uses: actions/setup-python@v2 diff --git a/README.md b/README.md index 1ee69d36f..e23ab78fd 100644 --- a/README.md +++ b/README.md @@ -81,7 +81,7 @@ Windows. We regularly build and test it in the following environments: ## Prerequisites Cryptol is regularly built and tested with the three most recent -versions of GHC, which at the time of this writing are 8.8.4, 8.10.2, and +versions of GHC, which at the time of this writing are 8.8.4, 8.10.7, and 9.0.2. The easiest way to install an approporiate version of GHC is with [ghcup](https://www.haskell.org/ghcup/). diff --git a/cabal.GHC-8.10.2.config b/cabal.GHC-8.10.2.config deleted file mode 100644 index 46dba0c2b..000000000 --- a/cabal.GHC-8.10.2.config +++ /dev/null @@ -1,228 +0,0 @@ -constraints: any.Cabal ==3.2.0.0, - any.FloatingHex ==0.4, - any.Glob ==0.10.0, - any.GraphSCC ==1.0.4, - GraphSCC -use-maps, - any.HUnit ==1.6.0.0, - any.Only ==0.1, - any.QuickCheck ==2.14, - QuickCheck +templatehaskell, - any.StateVar ==1.2, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, - any.aeson ==1.5.1.0, - aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.5, - alex +small_base, - any.ansi-terminal ==0.10.3, - ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, - any.array ==0.5.4.0, - any.assoc ==1.0.1, - any.async ==2.2.2, - async -bench, - any.attoparsec ==0.13.2.4, - attoparsec -developer, - any.base ==4.14.1.0, - any.base-compat ==0.11.1, - any.base-compat-batteries ==0.11.1, - any.base-orphans ==0.8.2, - any.bifunctors ==5.5.7, - bifunctors +semigroups +tagged, - any.bimap ==0.4.0, - any.binary ==0.8.8.0, - any.binary-orphans ==1.0.1, - any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.1.0, - any.blaze-html ==0.9.1.2, - any.blaze-markup ==0.8.2.5, - any.bv-sized ==1.0.2, - any.bytestring ==0.10.10.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.2.0, - any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, - cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, - cereal -bytestring-builder, - any.clock ==0.8, - clock -llvm, - any.code-page ==0.2, - any.colour ==2.3.5, - any.comonad ==5.0.6, - comonad +containers +distributive +test-doctests, - any.concurrent-output ==1.10.11, - any.constraints ==0.11.2, - any.containers ==0.6.2.1, - any.contravariant ==1.5.2, - contravariant +semigroups +statevar +tagged, - any.crackNum ==2.3, - any.criterion ==1.5.6.2, - criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, - criterion-measurement -fast, - any.cryptohash-sha1 ==0.11.100.1, - cryptol +relocatable -static, - cryptol-test-runner -static, - any.data-binary-ieee754 ==0.4.4, - any.data-default-class ==0.1.2.0, - any.deepseq ==1.4.4.0, - any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, - deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, - any.directory ==1.3.6.0, - any.distributive ==0.6.2, - distributive +semigroups +tagged, - any.dlist ==0.8.0.8, - any.erf ==2.0.0.0, - any.exceptions ==0.10.4, - any.extensible-exceptions ==0.1.1.4, - any.extra ==1.7.3, - any.fail ==4.9.0.0, - any.filepath ==1.4.2.1, - any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, - generic-deriving +base-4-9, - any.ghc-boot-th ==8.10.2, - any.gitrev ==1.3.1, - any.happy ==1.19.12, - happy +small_base, - any.hashable ==1.3.0.0, - hashable -examples +integer-gmp +sse2 -sse41, - any.hashtables ==1.2.3.4, - hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.8.0.0, - any.haskell-lexer ==1.1, - any.hedgehog ==1.0.2, - any.heredoc ==0.2.0.0, - any.hostname ==1.0, - any.hpc ==0.6.1.0, - any.hsc2hs ==0.68.7, - hsc2hs -in-ghc-tree, - any.integer-gmp ==1.0.3.0, - any.integer-logarithms ==1.0.3, - integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.5.3, - any.io-streams ==1.5.1.0, - io-streams -nointeractivetests, - any.js-flot ==0.8.3, - any.js-jquery ==3.3.1, - any.kan-extensions ==5.2, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.lifted-async ==0.10.0.6, - any.lifted-base ==0.2.3.12, - any.math-functions ==0.3.4.0, - math-functions +system-erf +system-expm1, - any.megaparsec ==8.0.0, - megaparsec -dev, - any.microstache ==1.0.1.1, - any.mmorph ==1.1.3, - any.monad-control ==1.0.2.3, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, - any.monadLib ==3.10, - any.mtl ==2.2.2, - any.mwc-random ==0.14.0.0, - any.old-locale ==1.0.0.7, - any.optparse-applicative ==0.15.1.0, - any.panic ==0.4.0.1, - any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.0, - parameterized-utils +unsafe-operations, - any.parsec ==3.1.14.0, - any.parser-combinators ==1.2.1, - parser-combinators -dev, - any.pretty ==1.1.3.6, - any.pretty-show ==1.10, - any.primitive ==0.7.0.1, - any.process ==1.6.9.0, - any.profunctors ==5.5.2, - any.random ==1.1, - any.reflection ==2.1.6, - reflection -slow +template-haskell, - any.regex-base ==0.94.0.0, - any.regex-posix ==0.96.0.0, - any.resourcet ==1.2.4.1, - any.rts ==1.0, - any.sbv ==8.6, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, - scientific -bytestring-builder -integer-simple, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, - semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, - any.simple-get-opt ==0.4, - any.simple-smt ==0.9.7, - any.splitmix ==0.0.5, - splitmix -optimised-mixer +random, - any.statistics ==0.15.2.0, - any.stm ==2.5.0.0, - any.strict ==0.3.2, - strict +split-base, - any.syb ==0.7.1, - any.tagged ==0.8.6, - tagged +deepseq +transformers, - any.tasty ==1.3.1, - tasty +clock, - any.tasty-hedgehog ==1.0.0.2, - any.tasty-hunit ==0.10.0.2, - any.tasty-quickcheck ==0.10.1.1, - any.template-haskell ==2.16.0.0, - any.temporary ==1.3, - any.terminal-size ==0.3.2.1, - any.terminfo ==0.4.1.4, - any.test-framework ==0.8.2.0, - any.test-framework-hunit ==0.3.0.2, - test-framework-hunit -base3 +base4, - any.test-lib ==0.3, - any.text ==1.2.4.1, - any.text-short ==0.1.3, - text-short -asserts, - any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, - any.th-lift ==0.8.2, - any.these ==1.1, - these +assoc, - any.time ==1.9.3, - any.time-compat ==1.9.3, - time-compat -old-locale, - any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, - transformers-base +orphaninstances, - any.transformers-compat ==0.6.5, - transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, - any.type-equality ==1, - any.unbounded-delays ==0.1.1.0, - any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.10.0, - unordered-containers -debug, - any.utf8-string ==1.0.1.1, - any.uuid-types ==1.0.3, - any.vector ==0.12.1.2, - vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.3, - vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.7, - any.versions ==4.0.2, - any.void ==0.7.3, - void -safe, - any.wcwidth ==0.0.2, - wcwidth -cli +split-base, - any.what4 ==1.2.1, - what4 -drealtestdisable -solvertests -stptestdisable, - any.wl-pprint-annotated ==0.1.0.1, - any.xml ==1.3.14, - any.zenc ==0.1.1, - any.zlib ==0.6.2.1, - zlib -non-blocking-ffi -pkg-config, - any.zlib-bindings ==0.1.1.5 diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.7.config similarity index 56% rename from cabal.GHC-8.10.3.config rename to cabal.GHC-8.10.7.config index f562fbe06..4d0d22689 100644 --- a/cabal.GHC-8.10.3.config +++ b/cabal.GHC-8.10.7.config @@ -1,222 +1,237 @@ +active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.2.1.0, - any.FloatingHex ==0.5, - any.Glob ==0.10.1, + any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, - any.HUnit ==1.6.1.0, + any.HUnit ==1.6.2.0, any.MemoTrie ==0.6.10, MemoTrie -examples, + any.OneTuple ==0.3.1, any.Only ==0.1, any.QuickCheck ==2.14.2, - QuickCheck +old-random +templatehaskell, - any.StateVar ==1.2.1, + QuickCheck -old-random +templatehaskell, + any.StateVar ==1.2.2, any.abstract-deque ==0.3, abstract-deque -usecas, any.abstract-par ==0.3.3, any.adjunctions ==4.4, - any.aeson ==1.5.4.1, - aeson -bytestring-builder -cffi -developer -fast, + any.aeson ==2.0.3.0, + aeson -cffi +ordered-keymap, any.alex ==3.2.6, alex +small_base, - any.ansi-terminal ==0.10.3, + any.ansi-terminal ==0.11.1, ansi-terminal -example, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, any.asn1-types ==0.3.4, any.assoc ==1.0.2, - any.async ==2.2.2, + any.async ==2.2.4, async -bench, - any.attoparsec ==0.13.2.4, + any.attoparsec ==0.14.3, attoparsec -developer, any.auto-update ==0.1.6, - any.base ==4.14.1.0, + any.base ==4.14.3.0, any.base-compat ==0.11.2, any.base-compat-batteries ==0.11.2, - any.base-orphans ==0.8.4, - any.base64-bytestring ==1.2.0.1, - any.basement ==0.0.11, - any.bifunctors ==5.5.7, + any.base-orphans ==0.8.6, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, bifunctors +semigroups +tagged, any.bimap ==0.4.0, any.binary ==0.8.8.0, - any.binary-orphans ==1.0.1, + any.binary-orphans ==1.0.2, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.1.0, + any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, - any.blaze-markup ==0.8.2.7, + any.blaze-markup ==0.8.2.8, any.bsb-http-chunked ==0.0.0.4, - any.bv-sized ==1.0.2, + any.bv-sized ==1.0.3, any.byteorder ==1.0.4, any.bytestring ==0.10.12.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.2.0, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cassava ==0.5.2.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, + any.cereal ==0.5.8.2, cereal -bytestring-builder, - any.clock ==0.8, + any.chimera ==0.3.2.0, + chimera +representable, + any.clock ==0.8.2, clock -llvm, - any.code-page ==0.2, - any.colour ==2.3.5, - any.comonad ==5.0.7, - comonad +containers +distributive +indexed-traversable +test-doctests, - any.constraints ==0.12, - any.containers ==0.6.2.1, - any.contravariant ==1.5.2, + any.code-page ==0.2.1, + any.colour ==2.3.6, + any.comonad ==5.0.8, + comonad +containers +distributive +indexed-traversable, + any.config-value ==0.8.2, + any.constraints ==0.13.2, + any.containers ==0.6.5.1, + any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.crackNum ==2.4, - any.criterion ==1.5.9.0, + any.criterion ==1.5.12.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, + any.criterion-measurement ==0.1.3.0, criterion-measurement -fast, - any.cryptohash-md5 ==0.11.100.1, - any.cryptohash-sha1 ==0.11.100.1, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, cryptol +relocatable -static, + cryptol-remote-api -notthreaded -static, cryptol-test-runner -static, - any.cryptonite ==0.27, + any.cryptonite ==0.29, cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.0, + any.data-fix ==0.3.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, + any.deriving-compat ==0.6, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, - any.distributive ==0.6.2, + any.distributive ==0.6.2.1, distributive +semigroups +tagged, any.dlist ==1.0, dlist -werror, any.easy-file ==0.2.2, - any.entropy ==0.4.1.6, + any.entropy ==0.4.1.7, entropy -halvm, + any.exact-pi ==0.5.0.1, any.exceptions ==0.10.4, any.extensible-exceptions ==0.1.1.4, - any.extra ==1.7.9, + any.extra ==1.7.10, any.fail ==4.9.0.0, - any.fast-logger ==3.0.2, + any.fast-logger ==3.1.0, any.filelock ==0.1.1.5, any.filepath ==1.4.2.1, any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.ghc-boot-th ==8.10.3, + any.free ==5.1.7, + any.ghc-boot-th ==8.10.7, any.ghc-prim ==0.6.1, any.gitrev ==1.3.1, any.happy ==1.20.0, - any.hashable ==1.3.0.0, - hashable -examples +integer-gmp +sse2 -sse41, - any.hashtables ==1.2.4.1, + any.hashable ==1.3.5.0, + hashable +integer-gmp -random-initial-seed, + any.hashtables ==1.2.4.2, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.8.0.1, + any.haskeline ==0.8.2, any.heredoc ==0.2.0.0, any.hostname ==1.0, any.hourglass ==0.2.12, - any.hsc2hs ==0.68.7, + any.hsc2hs ==0.68.8, hsc2hs -in-ghc-tree, - any.http-date ==0.0.10, + any.http-date ==0.0.11, any.http-types ==0.12.3, - any.http2 ==2.0.5, - http2 -devel, - any.indexed-traversable ==0.1.1, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, any.integer-gmp ==1.0.3.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.5.3, - any.io-streams ==1.5.2.0, + any.integer-roots ==1.0.2.0, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, - any.iproute ==1.7.10, + any.iproute ==1.7.12, any.js-chart ==2.9.4.1, - any.kan-extensions ==5.2.1, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6, - any.math-functions ==0.3.4.1, + any.kan-extensions ==5.2.3, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, + libBF -system-libbf, + any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==9.0.1, + any.megaparsec ==9.2.0, megaparsec -dev, - any.memory ==0.15.0, + any.memory ==0.16.0, memory +support_basement +support_bytestring +support_deepseq +support_foundation, - any.microstache ==1.0.1.2, - any.monad-control ==1.0.2.3, + any.microstache ==1.0.2, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.monad-control ==1.0.3.1, any.monad-par ==0.3.5, monad-par -chaselev -newgeneric, any.monad-par-extras ==0.3.3, any.monadLib ==3.10, any.mtl ==2.2.2, - any.mwc-random ==0.14.0.0, + any.mwc-random ==0.15.0.2, any.nats ==1.1.2, nats +binary +hashable +template-haskell, - any.network ==3.1.2.1, + any.network ==3.1.2.5, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.0.10, - any.newtype-generics ==0.5.4, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.1, + any.parameterized-utils ==2.1.4.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.14.0, - any.parser-combinators ==1.2.1, + any.parser-combinators ==1.3.0, parser-combinators -dev, any.pem ==0.2.4, any.pretty ==1.1.3.6, - any.primitive ==0.7.1.0, - any.process ==1.6.9.0, - any.profunctors ==5.6, - any.psqueues ==0.2.7.2, - any.quickcheck-instances ==0.3.25.1, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.primitive ==0.7.3.0, + any.process ==1.6.13.2, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, quickcheck-instances -bytestring-builder, - any.random ==1.1, + any.random ==1.2.1, any.reflection ==2.1.6, reflection -slow +template-haskell, - any.regex-base ==0.94.0.0, - any.regex-compat ==0.95.2.0, - any.regex-posix ==0.96.0.0, + any.regex-base ==0.94.0.2, + any.regex-compat ==0.95.2.1, + any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.2, - any.rts ==1.0, + any.resourcet ==1.2.4.3, + any.rts ==1.0.1, any.safe ==0.3.19, - any.sbv ==8.9, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, + any.sbv ==8.16, + any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, + any.semialign ==1.2.0.1, + semialign +semigroupoids, + any.semigroupoids ==5.3.6, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, - any.silently ==1.2.5.1, + any.semirings ==0.6, + semirings +containers +unordered-containers, + any.silently ==1.2.5.2, any.simple-get-opt ==0.4, any.simple-sendfile ==0.2.30, simple-sendfile +allow-bsd, any.simple-smt ==0.9.7, - any.splitmix ==0.1.0.3, + any.splitmix ==0.1.0.4, splitmix -optimised-mixer, any.statistics ==0.15.2.0, - any.stm ==2.5.0.0, - any.streaming-commons ==0.2.2.1, + any.stm ==2.5.0.1, + any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, any.strict ==0.4.0.1, strict +assoc, - any.syb ==0.7.1, + any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.0.1, + any.tasty ==1.4.2.1, tasty +clock +unix, any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.1.2, + any.tasty-quickcheck ==0.10.2, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminfo ==0.4.1.4, @@ -225,59 +240,70 @@ constraints: any.Cabal ==3.2.1.0, test-framework-hunit -base3 +base4, any.test-lib ==0.3, any.text ==1.2.4.1, - any.text-short ==0.1.3, + any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, + any.th-abstraction ==0.4.3.0, any.th-lift ==0.8.2, + any.th-lift-instances ==0.1.19, any.these ==1.1.1.1, these +assoc, any.time ==1.9.3, - any.time-compat ==1.9.5, + any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, + any.tls ==1.5.6, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, + any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.6.6, + any.transformers-compat ==0.7.1, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.2, + any.unix-compat ==0.5.3, unix-compat -old-time, any.unix-time ==0.4.7, + any.unliftio ==0.2.20, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.13.0, + any.unordered-containers ==0.2.16.0, unordered-containers -debug, - any.utf8-string ==1.0.1.1, - any.uuid ==1.3.13, - any.uuid-types ==1.0.3, - any.vault ==0.3.1.4, + any.utf8-string ==1.0.2, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, + any.vault ==0.3.1.5, vault +useghc, - any.vector ==0.12.1.2, + any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.8.0.4, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.7, - any.versions ==4.0.2, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.1, any.void ==0.7.3, void -safe, - any.wai ==3.2.2.1, - any.wai-extra ==3.1.4.1, + any.wai ==3.2.3, + any.wai-extra ==3.1.8, wai-extra -build-example, - any.wai-logger ==2.3.6, - any.warp ==3.3.13, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.2.1, what4 -drealtestdisable -solvertests -stptestdisable, + any.witherable ==0.4.2, any.word8 ==0.1.3, any.x509 ==1.7.5, + any.x509-store ==1.6.7, + any.x509-validation ==1.6.11, any.xml ==1.3.14, - any.zenc ==0.1.1, - any.zlib ==0.6.2.2, + any.zenc ==0.1.2, + any.zlib ==0.6.2.3, + zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2022-01-06T13:38:03Z diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index 0f67db8fe..9e7eccfb4 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -1,221 +1,310 @@ +active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.0.1.0, - any.FloatingHex ==0.4, - any.Glob ==0.10.0, + any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, - any.HUnit ==1.6.0.0, + any.HUnit ==1.6.2.0, + any.MemoTrie ==0.6.10, + MemoTrie -examples, + any.OneTuple ==0.3.1, any.Only ==0.1, - any.QuickCheck ==2.14, - QuickCheck +templatehaskell, - any.StateVar ==1.2, + any.QuickCheck ==2.14.2, + QuickCheck -old-random +templatehaskell, + any.StateVar ==1.2.2, any.abstract-deque ==0.3, abstract-deque -usecas, any.abstract-par ==0.3.3, any.adjunctions ==4.4, - any.aeson ==1.4.7.1, - aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.5, + any.aeson ==2.0.3.0, + aeson -cffi +ordered-keymap, + any.alex ==3.2.6, alex +small_base, - any.ansi-terminal ==0.10.3, + any.ansi-terminal ==0.11.1, ansi-terminal -example, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, + any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, any.array ==0.5.4.0, - any.async ==2.2.2, + any.asn1-encoding ==0.9.6, + any.asn1-parse ==0.9.5, + any.asn1-types ==0.3.4, + any.assoc ==1.0.2, + any.async ==2.2.4, async -bench, - any.attoparsec ==0.13.2.4, + any.attoparsec ==0.14.3, attoparsec -developer, + any.auto-update ==0.1.6, any.base ==4.13.0.0, - any.base-compat ==0.11.1, - any.base-compat-batteries ==0.11.1, - any.base-orphans ==0.8.2, - any.bifunctors ==5.5.7, + any.base-compat ==0.11.2, + any.base-compat-batteries ==0.11.2, + any.base-orphans ==0.8.6, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, bifunctors +semigroups +tagged, any.bimap ==0.4.0, any.binary ==0.8.7.0, - any.binary-orphans ==1.0.1, - any.blaze-builder ==0.4.1.0, + any.binary-orphans ==1.0.2, + any.bitwise ==1.0.0.1, + any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, - any.blaze-markup ==0.8.2.5, - any.bv-sized ==1.0.2, + any.blaze-markup ==0.8.2.8, + any.bsb-http-chunked ==0.0.0.4, + any.bv-sized ==1.0.3, + any.byteorder ==1.0.4, any.bytestring ==0.10.10.1, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.2.0, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cassava ==0.5.2.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, + any.cereal ==0.5.8.2, cereal -bytestring-builder, - any.clock ==0.8, + any.chimera ==0.3.2.0, + chimera +representable, + any.clock ==0.8.2, clock -llvm, - any.code-page ==0.2, - any.colour ==2.3.5, - any.comonad ==5.0.6, - comonad +containers +distributive +test-doctests, - any.concurrent-output ==1.10.11, - any.constraints ==0.11.2, + any.code-page ==0.2.1, + any.colour ==2.3.6, + any.comonad ==5.0.8, + comonad +containers +distributive +indexed-traversable, + any.config-value ==0.8.2, + any.constraints ==0.13.2, any.containers ==0.6.2.1, - any.contravariant ==1.5.2, + any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, - any.crackNum ==2.3, - any.criterion ==1.5.6.2, + any.cookie ==0.4.5, + any.criterion ==1.5.12.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, + any.criterion-measurement ==0.1.3.0, criterion-measurement -fast, - any.cryptohash-sha1 ==0.11.100.1, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, cryptol +relocatable -static, + cryptol-remote-api -notthreaded -static, cryptol-test-runner -static, + any.cryptonite ==0.29, + cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, + any.data-fix ==0.3.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.8, + any.deriving-compat ==0.6, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, - any.distributive ==0.6.2, + any.distributive ==0.6.2.1, distributive +semigroups +tagged, - any.dlist ==0.8.0.8, - any.erf ==2.0.0.0, + any.dlist ==1.0, + dlist -werror, + any.easy-file ==0.2.2, + any.entropy ==0.4.1.7, + entropy -halvm, + any.exact-pi ==0.5.0.1, any.exceptions ==0.10.4, exceptions +transformers-0-4, any.extensible-exceptions ==0.1.1.4, - any.extra ==1.7.1, + any.extra ==1.7.10, any.fail ==4.9.0.0, + any.fast-logger ==3.1.0, + any.filelock ==0.1.1.5, any.filepath ==1.4.2.1, any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, - generic-deriving +base-4-9, + any.free ==5.1.7, any.ghc-boot-th ==8.8.4, any.ghc-prim ==0.5.3, any.gitrev ==1.3.1, - any.happy ==1.19.12, - happy +small_base, - any.hashable ==1.3.0.0, - hashable -examples +integer-gmp +sse2 -sse41, - any.hashtables ==1.2.3.4, + any.happy ==1.20.0, + any.hashable ==1.3.5.0, + hashable +integer-gmp -random-initial-seed, + any.hashtables ==1.2.4.2, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.7.5.0, - any.haskell-lexer ==1.1, - any.hedgehog ==1.0.2, any.heredoc ==0.2.0.0, any.hostname ==1.0, - any.hpc ==0.6.0.3, - any.hsc2hs ==0.68.7, + any.hourglass ==0.2.12, + any.hsc2hs ==0.68.8, hsc2hs -in-ghc-tree, + any.http-date ==0.0.11, + any.http-types ==0.12.3, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, any.integer-gmp ==1.0.2.0, - any.integer-logarithms ==1.0.3, + any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, - any.invariant ==0.5.3, - any.io-streams ==1.5.1.0, - io-streams -nointeractivetests, - any.js-flot ==0.8.3, - any.js-jquery ==3.3.1, - any.kan-extensions ==5.2, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.lifted-async ==0.10.0.6, - any.lifted-base ==0.2.3.12, - any.math-functions ==0.3.3.0, + any.integer-roots ==1.0.2.0, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, + io-streams +network -nointeractivetests +zlib, + any.iproute ==1.7.12, + any.js-chart ==2.9.4.1, + any.kan-extensions ==5.2.3, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, + libBF -system-libbf, + any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==8.0.0, + any.megaparsec ==9.2.0, megaparsec -dev, - any.microstache ==1.0.1.1, - any.mmorph ==1.1.3, - any.monad-control ==1.0.2.3, + any.memory ==0.16.0, + memory +support_basement +support_bytestring +support_deepseq +support_foundation, + any.microstache ==1.0.2, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.monad-control ==1.0.3.1, any.monad-par ==0.3.5, monad-par -chaselev -newgeneric, any.monad-par-extras ==0.3.3, any.monadLib ==3.10, any.mtl ==2.2.2, - any.mwc-random ==0.14.0.0, + any.mwc-random ==0.15.0.2, + any.nats ==1.1.2, + nats +binary +hashable +template-haskell, + any.network ==3.1.2.5, + network -devel, + any.network-byte-order ==0.1.6, + any.network-info ==0.2.0.10, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, - any.optparse-applicative ==0.15.1.0, + any.old-time ==1.1.0.3, + any.optparse-applicative ==0.16.1.0, + optparse-applicative +process, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, - any.parameterized-utils ==2.1.0, + any.parameterized-utils ==2.1.4.0, parameterized-utils +unsafe-operations, any.parsec ==3.1.14.0, - any.parser-combinators ==1.2.1, + any.parser-combinators ==1.3.0, parser-combinators -dev, + any.pem ==0.2.4, any.pretty ==1.1.3.6, - any.pretty-show ==1.10, - any.primitive ==0.7.0.1, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.primitive ==0.7.3.0, any.process ==1.6.9.0, - any.profunctors ==5.5.2, - any.random ==1.1, - any.reflection ==2.1.5, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, + quickcheck-instances -bytestring-builder, + any.random ==1.2.1, + any.reflection ==2.1.6, reflection -slow +template-haskell, - any.regex-base ==0.94.0.0, - any.regex-posix ==0.96.0.0, - any.resourcet ==1.2.4, + any.regex-base ==0.94.0.2, + any.regex-compat ==0.95.2.1, + any.regex-posix ==0.96.0.1, + regex-posix -_regex-posix-clib, + any.resourcet ==1.2.4.3, any.rts ==1.0, - any.sbv ==8.6, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, + any.safe ==0.3.19, + any.sbv ==8.16, + any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, + any.scotty ==0.12, + any.semialign ==1.2.0.1, + semialign +semigroupoids, + any.semigroupoids ==5.3.6, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, + any.semirings ==0.6, + semirings +containers +unordered-containers, + any.silently ==1.2.5.2, any.simple-get-opt ==0.4, + any.simple-sendfile ==0.2.30, + simple-sendfile +allow-bsd, any.simple-smt ==0.9.7, - any.splitmix ==0.0.4, - splitmix -optimised-mixer +random, + any.splitmix ==0.1.0.4, + splitmix -optimised-mixer, any.statistics ==0.15.2.0, any.stm ==2.5.0.0, - any.strict ==0.3.2, - strict +split-base, - any.syb ==0.7.1, - any.tagged ==0.8.6, + any.streaming-commons ==0.2.2.3, + streaming-commons -use-bytestring-builder, + any.strict ==0.4.0.1, + strict +assoc, + any.syb ==0.7.2.1, + any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.2.3, - tasty +clock, - any.tasty-hedgehog ==1.0.0.2, - any.tasty-hunit ==0.10.0.2, + any.tasty ==1.4.2.1, + tasty +clock +unix, + any.tasty-hunit ==0.10.0.3, + any.tasty-quickcheck ==0.10.2, any.template-haskell ==2.15.0.0, any.temporary ==1.3, - any.terminal-size ==0.3.2.1, + any.terminfo ==0.4.1.4, any.test-framework ==0.8.2.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.test-lib ==0.3, any.text ==1.2.4.0, + any.text-short ==0.1.5, + text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, + any.th-abstraction ==0.4.3.0, + any.th-lift ==0.8.2, + any.th-lift-instances ==0.1.19, + any.these ==1.1.1.1, + these +assoc, any.time ==1.9.3, - any.time-compat ==1.9.3, + any.time-compat ==1.9.6.1, time-compat -old-locale, + any.time-manager ==0.0.0, + any.tls ==1.5.6, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, + any.transformers-base ==0.4.6, transformers-base +orphaninstances, - any.transformers-compat ==0.6.5, + any.transformers-compat ==0.7.1, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.unbounded-delays ==0.1.1.0, + any.unbounded-delays ==0.1.1.1, + any.uniplate ==1.6.13, + any.unix ==2.7.2.2, + any.unix-compat ==0.5.3, + unix-compat -old-time, + any.unix-time ==0.4.7, + any.unliftio ==0.2.20, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.10.0, + any.unordered-containers ==0.2.16.0, unordered-containers -debug, - any.utf8-string ==1.0.1.1, - any.uuid-types ==1.0.3, - any.vector ==0.12.1.2, + any.utf8-string ==1.0.2, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, + any.vault ==0.3.1.5, + vault +useghc, + any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.3, + any.vector-algorithms ==0.8.0.4, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.7, - any.versions ==4.0.2, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.1, any.void ==0.7.3, void -safe, + any.wai ==3.2.3, + any.wai-extra ==3.1.8, + wai-extra -build-example, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, + warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.what4 ==1.2.1, what4 -drealtestdisable -solvertests -stptestdisable, - any.wl-pprint-annotated ==0.1.0.1, + any.witherable ==0.4.2, + any.word8 ==0.1.3, + any.x509 ==1.7.5, + any.x509-store ==1.6.7, + any.x509-validation ==1.6.11, any.xml ==1.3.14, - any.zenc ==0.1.1, - any.zlib ==0.6.2.1, - zlib -non-blocking-ffi -pkg-config, + any.zenc ==0.1.2, + any.zlib ==0.6.2.3, + zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2022-01-06T13:38:03Z From c6cd69d531a48a972ca91be1e344be0e967791cb Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 12:57:23 -0500 Subject: [PATCH 08/15] Only enable UnliftedNewtypes on GHC 9.0+ --- src/Cryptol/PrimeEC.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index cfd1d631b..026f2f82d 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -18,11 +18,19 @@ -- in order to speed up the basic modular arithmetic operations. ----------------------------------------------------------------------------- {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE UnboxedTuples #-} + +#if __GLASGOW_HASKELL__ >= 900 +-- On GHC 9.0 or later—that is, when building with ghc-bignum—BigNum# is an +-- unlifted type, so we need UnliftedNewtypes to declare a newtype on top of +-- it. On older versions of GHC, BigNat# is simply a synonym for BigNat. BigNat +-- is lifted, so declaring a newtype on top of it works out of the box. {-# LANGUAGE UnliftedNewtypes #-} +#endif module Cryptol.PrimeEC ( PrimeModulus From 2255e942f2ba2317d71ea341a9d2cda58d986acc Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 13:13:43 -0500 Subject: [PATCH 09/15] Avoid an -Woverlapping-patterns warning on GHC 9.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit GHC 9.0's pattern-match coverage checker is more clever and flags this guard as redundant: ``` [ 48 of 111] Compiling Cryptol.TypeCheck.SimpleSolver ( src/Cryptol/TypeCheck/SimpleSolver.hs, /tmp/ghc54946_0/ghc_169.o ) src/Cryptol/TypeCheck/SimpleSolver.hs:37:7: warning: [-Woverlapping-patterns] Pattern match is redundant In an equation for ‘dbg’: dbg msg x | False = ... | 37 | | False = ppTrace msg x | ^^^^^ ``` While true, we want to keep this code in to keep in from bitrotting. I have tweaked the code slightly so that it is just clever enough to defeat the pattern-match coverage checker. --- src/Cryptol/TypeCheck/SimpleSolver.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs index 4f60e2972..285ed2a0d 100644 --- a/src/Cryptol/TypeCheck/SimpleSolver.hs +++ b/src/Cryptol/TypeCheck/SimpleSolver.hs @@ -34,7 +34,10 @@ simplify ctxt p = where dbg msg x - | False = ppTrace msg x + -- Change `False` to `True` below to enable extra tracing. Note that + -- this is written with an extraneous `id` expression to suppress + -- pattern-match coverage checking warnings in this one case. + | id False = ppTrace msg x | otherwise = x From 7030088e13007f37e7037b29eda6ba6d1eb88e00 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 15:09:47 -0500 Subject: [PATCH 10/15] Ensure that there is at least one Windows build --- .github/workflows/ci.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2e6e2ef37..be0c04405 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -55,8 +55,6 @@ jobs: ghc-version: ["8.8.4", "8.10.7", "9.0.2"] exclude: # https://gitlab.haskell.org/ghc/ghc/-/issues/18550 - - os: windows-latest - ghc-version: 8.8.4 - os: windows-latest ghc-version: 8.10.7 - os: windows-latest From cb1cf652aedb952742850d1ec159f6964dc002de Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 15:12:57 -0500 Subject: [PATCH 11/15] Use test-lib-0.4 --- cabal.GHC-8.10.7.config | 12 ++++++------ cabal.GHC-8.8.4.config | 12 ++++++------ cabal.GHC-9.0.2.config | 12 ++++++------ cabal.project | 4 ---- 4 files changed, 18 insertions(+), 22 deletions(-) diff --git a/cabal.GHC-8.10.7.config b/cabal.GHC-8.10.7.config index 4d0d22689..0b01a4b7d 100644 --- a/cabal.GHC-8.10.7.config +++ b/cabal.GHC-8.10.7.config @@ -32,7 +32,7 @@ constraints: any.Cabal ==3.2.1.0, any.assoc ==1.0.2, any.async ==2.2.4, async -bench, - any.attoparsec ==0.14.3, + any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.14.3.0, @@ -206,7 +206,7 @@ constraints: any.Cabal ==3.2.1.0, any.scotty ==0.12, any.semialign ==1.2.0.1, semialign +semigroupoids, - any.semigroupoids ==5.3.6, + any.semigroupoids ==5.3.7, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, @@ -219,7 +219,7 @@ constraints: any.Cabal ==3.2.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.15.2.0, + any.statistics ==0.16.0.1, any.stm ==2.5.0.1, any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, @@ -238,7 +238,7 @@ constraints: any.Cabal ==3.2.1.0, any.test-framework ==0.8.2.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, - any.test-lib ==0.3, + any.test-lib ==0.4, any.text ==1.2.4.1, any.text-short ==0.1.5, text-short -asserts, @@ -264,7 +264,7 @@ constraints: any.Cabal ==3.2.1.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.3, + any.unix-compat ==0.5.4, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.20, @@ -306,4 +306,4 @@ constraints: any.Cabal ==3.2.1.0, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-01-06T13:38:03Z +index-state: hackage.haskell.org 2022-01-13T19:44:37Z diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index 9e7eccfb4..c776541e5 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -32,7 +32,7 @@ constraints: any.Cabal ==3.0.1.0, any.assoc ==1.0.2, any.async ==2.2.4, async -bench, - any.attoparsec ==0.14.3, + any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.13.0.0, @@ -207,7 +207,7 @@ constraints: any.Cabal ==3.0.1.0, any.scotty ==0.12, any.semialign ==1.2.0.1, semialign +semigroupoids, - any.semigroupoids ==5.3.6, + any.semigroupoids ==5.3.7, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, @@ -220,7 +220,7 @@ constraints: any.Cabal ==3.0.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.15.2.0, + any.statistics ==0.16.0.1, any.stm ==2.5.0.0, any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, @@ -239,7 +239,7 @@ constraints: any.Cabal ==3.0.1.0, any.test-framework ==0.8.2.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, - any.test-lib ==0.3, + any.test-lib ==0.4, any.text ==1.2.4.0, any.text-short ==0.1.5, text-short -asserts, @@ -265,7 +265,7 @@ constraints: any.Cabal ==3.0.1.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.3, + any.unix-compat ==0.5.4, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.20, @@ -307,4 +307,4 @@ constraints: any.Cabal ==3.0.1.0, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-01-06T13:38:03Z +index-state: hackage.haskell.org 2022-01-13T19:44:37Z diff --git a/cabal.GHC-9.0.2.config b/cabal.GHC-9.0.2.config index 821fb804e..a154e58b7 100644 --- a/cabal.GHC-9.0.2.config +++ b/cabal.GHC-9.0.2.config @@ -32,7 +32,7 @@ constraints: any.Cabal ==3.4.1.0, any.assoc ==1.0.2, any.async ==2.2.4, async -bench, - any.attoparsec ==0.14.3, + any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.15.1.0, @@ -207,7 +207,7 @@ constraints: any.Cabal ==3.4.1.0, any.scotty ==0.12, any.semialign ==1.2.0.1, semialign +semigroupoids, - any.semigroupoids ==5.3.6, + any.semigroupoids ==5.3.7, semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, any.semigroups ==0.20, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, @@ -220,7 +220,7 @@ constraints: any.Cabal ==3.4.1.0, any.simple-smt ==0.9.7, any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.15.2.0, + any.statistics ==0.16.0.1, any.stm ==2.5.0.0, any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, @@ -239,7 +239,7 @@ constraints: any.Cabal ==3.4.1.0, any.test-framework ==0.8.2.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, - any.test-lib ==0.3, + any.test-lib ==0.4, any.text ==1.2.5.0, any.text-short ==0.1.5, text-short -asserts, @@ -265,7 +265,7 @@ constraints: any.Cabal ==3.4.1.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.3, + any.unix-compat ==0.5.4, unix-compat -old-time, any.unix-time ==0.4.7, any.unliftio ==0.2.20, @@ -307,4 +307,4 @@ constraints: any.Cabal ==3.4.1.0, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2022-01-06T13:38:03Z +index-state: hackage.haskell.org 2022-01-13T19:44:37Z diff --git a/cabal.project b/cabal.project index e12f539f4..d8665fc91 100644 --- a/cabal.project +++ b/cabal.project @@ -3,7 +3,3 @@ packages: cryptol-remote-api tests deps/argo/argo - -allow-newer: - -- See https://github.com/GaloisInc/test-lib/pull/2 - test-lib:base From 3a204fc4aa2de19ea7773c98f3edfeeefadeb16e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 13 Jan 2022 15:35:41 -0500 Subject: [PATCH 12/15] Make integerRecipMod return a Maybe instead of an unboxed sum --- src/Cryptol/Backend/Concrete.hs | 6 ++---- src/Cryptol/Backend/SBV.hs | 6 ++---- src/Cryptol/Backend/What4.hs | 6 ++---- src/Cryptol/Eval/Reference.lhs | 6 ++---- src/GHC/Num/Compat.hs | 12 ++++++------ 5 files changed, 14 insertions(+), 22 deletions(-) diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs index 33b83246d..9472d8a6a 100644 --- a/src/Cryptol/Backend/Concrete.hs +++ b/src/Cryptol/Backend/Concrete.hs @@ -9,7 +9,6 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE BlockArguments #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MagicHash #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Rank2Types #-} @@ -18,7 +17,6 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE UnboxedTuples #-} module Cryptol.Backend.Concrete ( BV(..) , binBV @@ -344,8 +342,8 @@ instance Backend Concrete where -- congruent to 0 modulo m. znRecip sym m x = case Integer.integerRecipMod x m of - (# r | #) -> integerLit sym r - (# | () #) -> raiseError sym DivideByZero + Just r -> integerLit sym r + Nothing -> raiseError sym DivideByZero znPlus _ = liftBinIntMod (+) znMinus _ = liftBinIntMod (-) diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs index d036e1625..1ad01990b 100644 --- a/src/Cryptol/Backend/SBV.hs +++ b/src/Cryptol/Backend/SBV.hs @@ -11,14 +11,12 @@ {-# 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 @@ -432,8 +430,8 @@ sModRecip sym m x -- If the input is concrete, evaluate the answer | Just xi <- svAsInteger x = case Integer.integerRecipMod xi m of - (# r | #) -> integerLit sym r - (# | () #) -> raiseError sym DivideByZero + Just r -> integerLit sym r + Nothing -> 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 7d49a098f..d28c1dc3e 100644 --- a/src/Cryptol/Backend/What4.hs +++ b/src/Cryptol/Backend/What4.hs @@ -8,12 +8,10 @@ {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MagicHash #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE UnboxedTuples #-} module Cryptol.Backend.What4 where @@ -671,8 +669,8 @@ sModRecip sym m x -- If the input is concrete, evaluate the answer | Just xi <- W4.asInteger x = case Integer.integerRecipMod xi m of - (# r | #) -> integerLit sym r - (# | () #) -> raiseError sym DivideByZero + Just r -> integerLit sym r + Nothing -> 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/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 9771e7de1..f4d824f9c 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -10,8 +10,6 @@ > {-# LANGUAGE BlockArguments #-} > {-# LANGUAGE PatternGuards #-} > {-# LANGUAGE LambdaCase #-} -> {-# LANGUAGE MagicHash #-} -> {-# LANGUAGE UnboxedTuples #-} > > module Cryptol.Eval.Reference > ( Value(..) @@ -1335,8 +1333,8 @@ confused with integral division). > zRecip :: Integer -> Integer -> E Integer > zRecip m x = > case Integer.integerRecipMod x m of -> (# r | #) -> pure r -> (# | () #) -> cryError DivideByZero +> Just r -> pure r +> Nothing -> cryError DivideByZero > > zDiv :: Integer -> Integer -> Integer -> E Integer > zDiv m x y = f <$> zRecip m y diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs index 18adca6d6..8c96a6a8a 100644 --- a/src/GHC/Num/Compat.hs +++ b/src/GHC/Num/Compat.hs @@ -52,11 +52,11 @@ import GHC.Exts bigNatToInteger :: BigNat# -> Integer bigNatToInteger = Integer.integerFromBigNat# -integerRecipMod :: Integer -> Integer -> (# Integer | () #) +integerRecipMod :: Integer -> Integer -> Maybe Integer integerRecipMod x y = case Integer.integerRecipMod# x (Integer.integerToNaturalClamp y) of - (# r | #) -> (# toInteger r | #) - (# | () #) -> (# | () #) + (# r | #) -> Just (toInteger r) + (# | () #) -> Nothing -- | Coerce an integer value to a @BigNat#@. This operation only really makes -- sense for nonnegative values, but this condition is not checked. @@ -134,10 +134,10 @@ integerToBigNat (GMP.S# i) = GMP.wordToBigNat (int2Word# i) integerToBigNat (GMP.Jp# b) = b integerToBigNat (GMP.Jn# b) = b -integerRecipMod :: Integer -> Integer -> (# Integer | () #) +integerRecipMod :: Integer -> Integer -> Maybe Integer integerRecipMod x y - | res == 0 = (# | () #) - | otherwise = (# res | #) + | res == 0 = Nothing + | otherwise = Just res where res = GMP.recipModInteger x y From 09aaf1d82c3b41013a34f2fc092e192c1bb4891f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 14 Jan 2022 14:45:08 -0500 Subject: [PATCH 13/15] Make issue{066,093} resilient to different solvers' behavior This adopts the same approach as in commit 3ea5e9e51c260c3bdb85da0ab7ea790bbdff81a4: use `:set show-examples=false` in the affected examples to avoid showing the particular data that a solver picks for examples/counterexamples. Also avoid printing the contents of `it` for similar reasons. I have verified that the new output works across a wide range of Z3 versions. Fixes #1280. --- tests/issues/issue066.icry | 14 +++----------- tests/issues/issue066.icry.stdout | 22 ---------------------- tests/issues/issue072.icry | 2 ++ tests/issues/issue093.icry | 5 ++++- tests/issues/issue093.icry.stdout | 5 ----- 5 files changed, 9 insertions(+), 39 deletions(-) diff --git a/tests/issues/issue066.icry b/tests/issues/issue066.icry index d2a69ac63..1765d2990 100644 --- a/tests/issues/issue066.icry +++ b/tests/issues/issue066.icry @@ -1,35 +1,27 @@ +// Don't show examples, as they can differ depending on the solver version. +// See #1280. +:set show-examples=false let f x = (x : [4]) == x :prove f :t it -it it.result let f x = (x : [4]) == 3 :prove f :t it -it it.result :sat f :t it -it it.result let f x = (x : [4]) == 3 /\ x == 2 :sat f :t it -it let g p = (p : { x : [32], y : [32]}).x == p.y :prove g :t it -it :sat g :t it -it let h x y = (x : [8]) < y :prove h :t it -it -let result = it -result.arg1 -result.arg2 :sat h :t it -it \ No newline at end of file diff --git a/tests/issues/issue066.icry.stdout b/tests/issues/issue066.icry.stdout index 5503ed6bf..02dd5d624 100644 --- a/tests/issues/issue066.icry.stdout +++ b/tests/issues/issue066.icry.stdout @@ -1,42 +1,20 @@ Loading module Cryptol Q.E.D. it : {result : Bit, arg1 : [4]} - -Run-time error: no counterexample available --- Backtrace -- -Cryptol::error called at issue066.icry:2:8--2:9 True Counterexample -f 0xc = False it : {result : Bit, arg1 : [4]} -{result = False, arg1 = 0xc} False Satisfiable -f 0x3 = True it : {result : Bit, arg1 : [4]} -{result = True, arg1 = 0x3} True Unsatisfiable it : {result : Bit, arg1 : [4]} - -Run-time error: no satisfying assignment available --- Backtrace -- -Cryptol::error called at issue066.icry:16:6--16:7 Counterexample -g {x = 0xffffffff, y = 0x00000000} = False it : {result : Bit, arg1 : {x : [32], y : [32]}} -{result = False, arg1 = {x = 0xffffffff, y = 0x00000000}} Satisfiable -g {x = 0x00000000, y = 0x00000000} = True it : {result : Bit, arg1 : {x : [32], y : [32]}} -{result = True, arg1 = {x = 0x00000000, y = 0x00000000}} Counterexample -h 0x00 0x00 = False it : {result : Bit, arg1 : [8], arg2 : [8]} -{result = False, arg1 = 0x00, arg2 = 0x00} -0x00 -0x00 Satisfiable -h 0x00 0x01 = True it : {result : Bit, arg1 : [8], arg2 : [8]} -{result = True, arg1 = 0x00, arg2 = 0x01} diff --git a/tests/issues/issue072.icry b/tests/issues/issue072.icry index 0c1178fac..f33909136 100644 --- a/tests/issues/issue072.icry +++ b/tests/issues/issue072.icry @@ -1,3 +1,5 @@ +// Don't show examples, as they can differ depending on the solver version. +// See #1280. :set show-examples=false :sat \x -> x > 0x4 :t it diff --git a/tests/issues/issue093.icry b/tests/issues/issue093.icry index 71f3eceb6..cadebaf89 100644 --- a/tests/issues/issue093.icry +++ b/tests/issues/issue093.icry @@ -1,4 +1,7 @@ +// Don't show examples, as they can differ depending on the solver version. +// See #1280. +:set show-examples=false :l issue093.cry :check :prove -:sat \ No newline at end of file +:sat diff --git a/tests/issues/issue093.icry.stdout b/tests/issues/issue093.icry.stdout index 082440795..1aef8e83f 100644 --- a/tests/issues/issue093.icry.stdout +++ b/tests/issues/issue093.icry.stdout @@ -12,7 +12,6 @@ Testing... Passed 100 tests. Expected test coverage: 0.00% (100 of 2^^64 values) property f0 Using exhaustive testing. Testing... Counterexample -f0 = False :prove t0 Q.E.D. :prove t1 @@ -21,15 +20,11 @@ f0 = False Q.E.D. :prove f0 Counterexample -f0 = False :sat t0 Satisfiable -t0 = True :sat t1 Satisfiable -t1 0x00000000 = True :sat t2 Satisfiable -t2 0xfffffffe 0xffffffff = True :sat f0 Unsatisfiable From 3b9eafbc91cdfc7f7a51e03ffb9747a5991750ef Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 14 Jan 2022 14:48:09 -0500 Subject: [PATCH 14/15] CI: Update what4-solvers to use Z3 4.8.14 The previous `what4-solvers` snapshot used Z3 4.8.10, which is known to cause severe performance regressions with the `negshift` regression test. See #1107. This updates to a more recent `what4-solvers` snapshot that uses Z3 4.8.14 instead, which is known to work more reliably with `negshift`. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index be0c04405..5b8a81241 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,7 +9,7 @@ on: workflow_dispatch: env: - SOLVER_PKG_VERSION: "snapshot-20210917" + SOLVER_PKG_VERSION: "snapshot-20220114" jobs: config: From 38926159987ace310e601645c6edf03d3a6ed41c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 25 Jan 2022 17:03:03 -0500 Subject: [PATCH 15/15] Address review comments --- src/Cryptol/PrimeEC.hs | 6 ------ src/GHC/Num/Compat.hs | 6 ++++++ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Cryptol/PrimeEC.hs b/src/Cryptol/PrimeEC.hs index 026f2f82d..e86771ba3 100644 --- a/src/Cryptol/PrimeEC.hs +++ b/src/Cryptol/PrimeEC.hs @@ -47,12 +47,6 @@ module Cryptol.PrimeEC ) where -{- -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.Num.Compat (BigNat#) import qualified GHC.Num.Compat as BN import GHC.Exts diff --git a/src/GHC/Num/Compat.hs b/src/GHC/Num/Compat.hs index 8c96a6a8a..84ed6abbe 100644 --- a/src/GHC/Num/Compat.hs +++ b/src/GHC/Num/Compat.hs @@ -52,6 +52,9 @@ import GHC.Exts bigNatToInteger :: BigNat# -> Integer bigNatToInteger = Integer.integerFromBigNat# +-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@. +-- +-- PRECONDITION: @m@ must be strictly positive. integerRecipMod :: Integer -> Integer -> Maybe Integer integerRecipMod x y = case Integer.integerRecipMod# x (Integer.integerToNaturalClamp y) of @@ -134,6 +137,9 @@ integerToBigNat (GMP.S# i) = GMP.wordToBigNat (int2Word# i) integerToBigNat (GMP.Jp# b) = b integerToBigNat (GMP.Jn# b) = b +-- | @'integerRecipMod' x m@ computes the modular inverse of @x@ mod @m@. +-- +-- PRECONDITION: @m@ must be strictly positive. integerRecipMod :: Integer -> Integer -> Maybe Integer integerRecipMod x y | res == 0 = Nothing