[arch-commits] Commit in cryptol/repos/community-x86_64 (4 files)

Felix Yan felixonmars at gemini.archlinux.org
Mon Jan 17 08:18:42 UTC 2022


    Date: Monday, January 17, 2022 @ 08:18:42
  Author: felixonmars
Revision: 1107490

archrelease: copy trunk to community-x86_64

Added:
  cryptol/repos/community-x86_64/PKGBUILD
    (from rev 1107489, cryptol/trunk/PKGBUILD)
  cryptol/repos/community-x86_64/ghc9.patch
    (from rev 1107489, cryptol/trunk/ghc9.patch)
Deleted:
  cryptol/repos/community-x86_64/PKGBUILD
  cryptol/repos/community-x86_64/ghc9.patch

------------+
 PKGBUILD   |  101 +--
 ghc9.patch | 1650 ++++++++++++++++++++++++++++-------------------------------
 2 files changed, 859 insertions(+), 892 deletions(-)

Deleted: PKGBUILD
===================================================================
--- PKGBUILD	2022-01-17 08:18:32 UTC (rev 1107489)
+++ PKGBUILD	2022-01-17 08:18:42 UTC (rev 1107490)
@@ -1,51 +0,0 @@
-# Maintainer: Felix Yan <felixonmars at archlinux.org>
-
-pkgname=cryptol
-pkgver=2.11.0
-pkgrel=122
-pkgdesc="The Language of Cryptography"
-url="https://www.cryptol.net"
-license=("BSD")
-arch=('x86_64')
-depends=('ghc-libs' 'z3' 'haskell-arithmoi' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized'
-         'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-extra' 'haskell-gitrev'
-         'haskell-graphscc' 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie'
-         'haskell-monad-control' 'haskell-monadlib' 'haskell-optparse-applicative'
-         'haskell-parameterized-utils' 'haskell-panic' 'haskell-random' 'haskell-sbv'
-         'haskell-simple-smt' 'haskell-strict' 'haskell-temporary' 'haskell-tf-random'
-         'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html')
-makedepends=('ghc' 'alex' 'happy' 'uusi')
-source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz"
-        ghc9.patch)
-sha512sums=('4e8e9dec727c02e76043ee390b91d0a740df747a8f49b2551686ac7db3cc0c94c36e20316b59e7e50e28b838f3f9bf7202095cf6ce683d83fd47826702381649'
-            'cf201d5d633101343399bb43e264e482e9f7e4615512ff658455772add3055d14571954f20ddf2cb2e35704c5638e7d2a3dab494bbb981229c519dcf88867e17')
-
-prepare() {
-    cd $pkgname-$pkgver
-    patch -p1 -i ../ghc9.patch
-    uusi -u sbv -u what4 $pkgname.cabal
-}
-
-build() {
-    cd "${srcdir}/${pkgname}-${pkgver}"
-
-    runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \
-        --prefix=/usr --docdir="/usr/share/doc/${pkgname}" --datasubdir="$pkgname" \
-        --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid --ghc-option=-fllvm \
-            -f-static -f-relocatable --ghc-option='-pie'
-    runhaskell Setup build $MAKEFLAGS
-    runhaskell Setup register --gen-script
-    runhaskell Setup unregister --gen-script
-    sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh
-    sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh
-}
-
-package() {
-    cd "${srcdir}/${pkgname}-${pkgver}"
-
-    install -D -m744 register.sh   "${pkgdir}/usr/share/haskell/register/${pkgname}.sh"
-    install -D -m744 unregister.sh "${pkgdir}/usr/share/haskell/unregister/${pkgname}.sh"
-    runhaskell Setup copy --destdir="${pkgdir}"
-    install -D -m644 LICENSE "$pkgdir"/usr/share/licenses/$pkgname/LICENSE
-    rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE
-}

Copied: cryptol/repos/community-x86_64/PKGBUILD (from rev 1107489, cryptol/trunk/PKGBUILD)
===================================================================
--- PKGBUILD	                        (rev 0)
+++ PKGBUILD	2022-01-17 08:18:42 UTC (rev 1107490)
@@ -0,0 +1,50 @@
+# Maintainer: Felix Yan <felixonmars at archlinux.org>
+
+pkgname=cryptol
+pkgver=2.12.0
+pkgrel=1
+pkgdesc="The Language of Cryptography"
+url="https://www.cryptol.net"
+license=("BSD")
+arch=('x86_64')
+depends=('ghc-libs' 'z3' 'haskell-arithmoi' 'haskell-async' 'haskell-base-compat' 'haskell-bv-sized'
+         'haskell-cryptohash-sha1' 'haskell-exceptions' 'haskell-extra' 'haskell-gitrev'
+         'haskell-graphscc' 'haskell-heredoc' 'haskell-libbf' 'haskell-memotrie'
+         'haskell-monad-control' 'haskell-monadlib' 'haskell-optparse-applicative'
+         'haskell-parameterized-utils' 'haskell-panic' 'haskell-prettyprinter' 'haskell-sbv'
+         'haskell-simple-smt' 'haskell-strict' 'haskell-temporary' 'haskell-tf-random'
+         'haskell-transformers-base' 'haskell-what4' 'haskell-ansi-terminal' 'haskell-blaze-html')
+makedepends=('ghc' 'alex' 'happy')
+source=("$pkgname-$pkgver.tar.gz::https://github.com/GaloisInc/cryptol/archive/$pkgver.tar.gz"
+        ghc9.patch)
+sha512sums=('3e7a58de47e5ae1fdc5067b2bcca66c04ee06c71e84f890104b64c59d1cd125667a23f537c3afd0503c059c97f5d168e6afa0df4fdc6c1e9448aae434e616bc8'
+            'f41afa8f65b01aaa5fc92a6433ed09ae85e86f58cb86e64b72de7e6765b32835974cb998305235d5c1ed8ff1112595f61400e16bd2ffd16c578c0c499d02486b')
+
+prepare() {
+    cd $pkgname-$pkgver
+    patch -p1 -i ../ghc9.patch
+}
+
+build() {
+    cd "${srcdir}/${pkgname}-${pkgver}"
+
+    runhaskell Setup configure -O --enable-shared --enable-executable-dynamic --disable-library-vanilla \
+        --prefix=/usr --docdir="/usr/share/doc/${pkgname}" --datasubdir="$pkgname" \
+        --dynlibdir=/usr/lib --libsubdir=\$compiler/site-local/\$pkgid --ghc-option=-fllvm \
+            -f-static -f-relocatable --ghc-option='-pie'
+    runhaskell Setup build $MAKEFLAGS
+    runhaskell Setup register --gen-script
+    runhaskell Setup unregister --gen-script
+    sed -i -r -e "s|ghc-pkg.*update[^ ]* |&'--force' |" register.sh
+    sed -i -r -e "s|ghc-pkg.*unregister[^ ]* |&'--force' |" unregister.sh
+}
+
+package() {
+    cd "${srcdir}/${pkgname}-${pkgver}"
+
+    install -D -m744 register.sh   "${pkgdir}/usr/share/haskell/register/${pkgname}.sh"
+    install -D -m744 unregister.sh "${pkgdir}/usr/share/haskell/unregister/${pkgname}.sh"
+    runhaskell Setup copy --destdir="${pkgdir}"
+    install -D -m644 LICENSE "$pkgdir"/usr/share/licenses/$pkgname/LICENSE
+    rm -f "$pkgdir"/usr/share/doc/$pkgname/LICENSE
+}

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

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



More information about the arch-commits mailing list