GHC 9.*

[robdockins]

This PR is work-in-progress toward GHC 9 support. The main thing we have to deal with here are the changes to the BigNat and Integer types that came in the 9.* series. This rearranged and renamed some operations, and removed the primality testing operation altogether.

To keep compatibility across these changes, we will need some intermediate compatibility layer. For now, I'm just figuring out what changes need to be made; then we can work out the compatibility API we need afterward.

[robdockins]

The first thing I notice when running the tests for this PR is the following, which looks ominous.

$ ./cry run -b tests/regression/twinmult.icry
Loading module Cryptol
Loading module Cryptol
Loading module PrimeEC
Loading module Main
property twin_mult_zro Using exhaustive testing.
Testing... Passed 49 tests.
Q.E.D.
property twin_mult_zro1 Using exhaustive testing.
Testing... cryptol: internal error: ARR_WORDS object (0x4200199b10) entered!
    (GHC version 9.0.1 for x86_64_apple_darwin)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
./cry: line 37: 51994 Abort trap: 6           cabal v2-exec cryptol -- $*

@RyanGlScott, any idea what's going on here? I don't know if this is a genuine GHC bug, or if I did a some kind of no-no.

[robdockins]

Minimizing further, we have:

$ ./cry run
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.11.0.99 (02aa441, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :m PrimeEC
Loading module Cryptol
Loading module PrimeEC
PrimeEC> let S = { x=0, y=2, z=1} : ProjectivePoint 7
PrimeEC> ec_double S
cryptol: internal error: ARR_WORDS object (0x42003a14a0) entered!
    (GHC version 9.0.1 for x86_64_apple_darwin)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
./cry: line 37: 52366 Abort trap: 6           cabal v2-exec cryptol -- $*

This error appears quite deterministic, although the pointer value in the error message changes.

[RyanGlScott]

Here is a minimal example that requires no external dependencies:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
module Main (main) where

import           GHC.Num.BigNat (BigNat#)
import qualified GHC.Num.BigNat as BN
import qualified GHC.Num.Integer as BN

main :: IO ()
main = print $ bigNatToInteger (px $ ec_double (primeModulus 7) s)
  where
    s = ProjectivePoint { px=integerToBigNat 0, py=integerToBigNat 2, pz=integerToBigNat 1 }

-- | Compute the elliptic curve group doubling operation.
--   In other words, if @S@ is a projective point on a curve,
--   this operation computes @S+S@ in the ECC group.
--
--   In geometric terms, this operation computes a tangent line
--   to the curve at @S@ and finds the (unique) intersection point of this
--   line with the curve, @R@; then returns the point @R'@, which is @R@
--   reflected across the x axis.
ec_double :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
ec_double p (ProjectivePoint sx sy sz) =
    if BN.bigNatIsZero sz then zro else ProjectivePoint r18 r23 r13

  where
  r7  = mod_square p sz                   {-  7: t4 <- (t3)^2  -}
  r8  = mod_sub    p sx r7                {-  8: t5 <- t1 - t4 -}
  r9  = mod_add    p sx r7                {-  9: t4 <- t1 + t4 -}
  r10 = mod_mul    p r9 r8                {- 10: t5 <- t4 * t5 -}
  r11 = mul3       p r10                  {- 11: t4 <- 3 * t5 -}
  r12 = mod_mul    p sz sy                {- 12: t3 <- t3 * t2 -}
  r13 = mul2       p r12                  {- 13: t3 <- 2 * t3 -}
  r14 = mod_square p sy                   {- 14: t2 <- (t2)^2 -}
  r15 = mod_mul    p sx r14               {- 15: t5 <- t1 * t2 -}
  r16 = mul4       p r15                  {- 16: t5 <- 4 * t5 -}
  r17 = mod_square p r11                  {- 17: t1 <- (t4)^2 -}
  r18 = mod_sub    p r17 (mul2 p r16)     {- 18: t1 <- t1 - 2 * t5 -}
  r19 = mod_square p r14                  {- 19: t2 <- (t2)^2 -}
  r20 = mul8       p r19                  {- 20: t2 <- 8 * t2 -}
  r21 = mod_sub    p r16 r18              {- 21: t5 <- t5 - t1 -}
  r22 = mod_mul    p r11 r21              {- 22: t5 <- t4 * t5 -}
  r23 = mod_sub    p r22 r20              {- 23: t2 <- t5 - t2 -}

-- | Points in the projective plane represented in
--   homogenous coordinates.
data ProjectivePoint =
  ProjectivePoint
  { px :: !BigNat#
  , py :: !BigNat#
  , pz :: !BigNat#
  }

-- | 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#

-- | The @BigNat@ value of the
--   modulus of the underlying field Z p.  This modulus
--   is required to be prime.
type PrimeModulus = BigNat#

-- | Inject an integer value into the @PrimeModulus@ type.
--   This modulus is required to be prime.
primeModulus :: Integer -> PrimeModulus
primeModulus x = integerToBigNat x
{-# INLINE primeModulus #-}

-- | 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 =
  let r = BN.bigNatAdd x y in
  case BN.bigNatSub r p of
    (# (# #) | #) -> r
    (# | rmp #)   -> rmp

-- | 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 = (BN.bigNatMul x y) `BN.bigNatRem` 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 =
  case BN.bigNatSub 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
--   will be in reduced form.
mod_square :: PrimeModulus -> BigNat# -> BigNat#
mod_square p x = BN.bigNatSqr x `BN.bigNatRem` 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 =
  let r = x `BN.bigNatShiftL#` 1## in
  case BN.bigNatSub r 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)

-- | 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)

-- | 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)

$ /opt/ghc/9.0.1/bin/runghc Bug.hs
Bug.hs: internal error: ARR_WORDS object (0x42002c4fd8) entered!
    (GHC version 9.0.1 for x86_64_unknown_linux)
    Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug
Aborted (core dumped)

Luckily, someone else encountered this issue before we did: see GHC#19645. That has been fixed upstream, and the fix will be included in GHC 9.0.2. Indeed, if I use a ghc-9.0 bindist artifact from GHC's GitLab instance, I can verify that the crash no longer occurs:

$ ~/Software/ghc-9.0.1.20210705/bin/runghc Bug.hs
2

I'm not sure if there's a workaround for GHC#19645, so we may just have to wait until GHC 9.0.2 gets released before landing these changes. If you want to keep prototyping this branch in anticipation of 9.0.2, however, you may want to download a bindist from GHC's GitLab and develop with that until then.

[robdockins]

Thanks Ryan, that's very helpful.

[robdockins]

I think I'm going to shelve this for now and wait for the 9.0.2 release, or until we have a pressing need for the 9.* series (in which case a larger refactoring might be required).

[RyanGlScott]

I hope you don't mind me pushing to your branch, @robdockins. I'm curious to see how the test suite fares now that GHC 9.0.2 is released.

[RyanGlScott]

Happily, the GHC 9.0.2 CI job worked like a charm. Now we just need to figure out the best way to achieve backwards compatibility with older GHCs.

[robdockins]

Happily, the GHC 9.0.2 CI job worked like a charm. Now we just need to figure out the best way to achieve backwards compatibility with older GHCs.

Excellent news.

[robdockins]

I think we can abstract pretty much everything we need (which basically ends up being modular arithmetic primitives and a primality test) into a utility module and just select different implementations based on the GHC/base version.

[RyanGlScott]

I've made an attempt to factor out all the compatibility shims into a GHC.Num.Compat module. I somewhat arbitrarily chose between the interfaces that ghc-bignum and integer-gmp use on a function-by-function basis, depending on which interface happened to be more convenient for cryptol's needs.

[RyanGlScott]

I might have celebrated CI passing a bit too early. Although the jobs which build the cryptol library do indeed work, the regression test jobs now time out. The CI logs are unfortunately not very helpful in figuring out where the timeout occurred, so I'll need to debug this locally.

[RyanGlScott]

I have a hunch that the reason the regression tests are stalling is because the negshift.icry test is being run with Z3 4.8.10, which has been known to cause issues in the past. See #1107. This seems to be the root of some nondeterministic CI timeouts in the past, such as this one, but the timeouts seem to be happening much more regularly with this patch (for reasons I don't fully understand).

[RyanGlScott]

Sure enough, upgrading to Z3 4.8.14 was enough to get the CI unstuck. Since the output of issue066 and issue093 were slightly different with Z3 4.8.14 (see #1280), I also pushed a commit which makes their output insensitive to the version of Z3 being used.

The CI is completely green now, so I'll mark this as ready for review.

[robdockins]

Well, I can't push the "approve" button since I initially authored this PR, but I think this looks good to me.