    -----------------------------------------------------------------------------
    -- |
    -- Module    : Cryptol.PrimeEC
    -- Copyright : (c) Galois, Inc.
    -- License   : BSD3
    -- Maintainer: rdockins@galois.com
    -- Stability : experimental
    --
    -- This module provides fast primitives for elliptic curve cryptography
    -- defined on @Z p@ for prime @p > 3@.  These are exposed in cryptol
    -- by importing the built-in module "PrimeEC".  The primary primitives
    -- exposed here are the doubling and addition primitives in the ECC group
    -- as well as scalar multiplication and the "twin" multiplication primitive,
    -- which simultaneously computes the addition of two scalar multiplies.
    --
    -- This module makes heavy use of some GHC internals regarding the
    -- representation of the Integer type, and the underlying GMP primitives
    -- 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
      , primeModulus
      , ProjectivePoint(..)
      , toProjectivePoint
      , BN.integerToBigNat
      , BN.bigNatToInteger

      , ec_double
      , ec_add_nonzero
      , ec_mult
      , ec_twin_mult
      ) where

    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

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

    toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint
    toProjectivePoint :: Integer -> Integer -> Integer -> ProjectivePoint
    toProjectivePoint Integer
    x Integer
    y Integer
    z =
      BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint (Integer -> BigNat#
    BN.integerToBigNat Integer
    x) (Integer -> BigNat#
    BN.integerToBigNat Integer
    y) (Integer -> BigNat#
    BN.integerToBigNat Integer
    z)

    -- | The projective "point at infinity", which represents the zero element
    --   of the ECC group.
    zro :: ProjectivePoint
    zro :: ProjectivePoint
    zro = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint ((# #) -> BigNat#
    BN.oneBigNat (# #)) ((# #) -> BigNat#
    BN.oneBigNat (# #)) ((# #) -> BigNat#
    BN.zeroBigNat (# #))

    -- | 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 { PrimeModulus -> BigNat#
    primeMod :: BigNat# }

    -- | Inject an integer value into the @PrimeModulus@ type.
    --   This modulus is required to be prime.
    primeModulus :: Integer -> PrimeModulus
    primeModulus :: Integer -> PrimeModulus
    primeModulus Integer
    x = BigNat# -> PrimeModulus
    PrimeModulus (Integer -> BigNat#
    BN.integerToBigNat Integer
    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 :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_add PrimeModulus
    p BigNat#
    x BigNat#
    y =
      let r :: BigNat#
    r = BigNat# -> BigNat# -> BigNat#
    BN.bigNatAdd BigNat#
    x BigNat#
    y in
      case BigNat# -> BigNat# -> (# (# #) | BigNat# #)
    BN.bigNatSub BigNat#
    r (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p) of
        (# (# #) | #) -> BigNat#
    r
        (# | BigNat#
    rmp #)   -> BigNat#
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mod_half PrimeModulus
    p BigNat#
    x = if BigNat# -> Int# -> Bool
    BN.testBitBigNat BigNat#
    x Int#
    0# then BigNat#
    qodd else BigNat#
    qeven
      where
      qodd :: BigNat#
    qodd  = (BigNat# -> BigNat# -> BigNat#
    BN.bigNatAdd BigNat#
    x (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p)) BigNat# -> Int# -> BigNat#
    `BN.shiftRBigNat` Int#
    1#
      qeven :: BigNat#
    qeven = BigNat#
    x BigNat# -> Int# -> BigNat#
    `BN.shiftRBigNat` Int#
    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 :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    x BigNat#
    y = (BigNat# -> BigNat# -> BigNat#
    BN.bigNatMul BigNat#
    x BigNat#
    y) BigNat# -> BigNat# -> BigNat#
    `BN.bigNatRem` (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    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 :: PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub PrimeModulus
    p BigNat#
    x BigNat#
    y =
      case BigNat# -> BigNat# -> (# (# #) | BigNat# #)
    BN.bigNatSub (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p) BigNat#
    y of
        (# | BigNat#
    y' #) -> PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_add PrimeModulus
    p BigNat#
    x BigNat#
    y'
        (# (# #) | #) -> BigNat#
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    x = BigNat# -> BigNat#
    BN.bigNatSqr BigNat#
    x BigNat# -> BigNat# -> BigNat#
    `BN.bigNatRem` PrimeModulus -> BigNat#
    primeMod PrimeModulus
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    x =
      let r :: BigNat#
    r = BigNat#
    x BigNat# -> Int# -> BigNat#
    `BN.shiftLBigNat` Int#
    1# in
      case BigNat# -> BigNat# -> (# (# #) | BigNat# #)
    BN.bigNatSub BigNat#
    r (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p) of
        (# (# #) | #) -> BigNat#
    r
        (# | BigNat#
    rmp #)   -> BigNat#
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mul3 PrimeModulus
    p BigNat#
    x = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_add PrimeModulus
    p BigNat#
    x (PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mul4 PrimeModulus
    p BigNat#
    x = PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p (PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    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 :: PrimeModulus -> BigNat# -> BigNat#
    mul8 PrimeModulus
    p BigNat#
    x = PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p (PrimeModulus -> BigNat# -> BigNat#
    mul4 PrimeModulus
    p BigNat#
    x)

    -- | 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 :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p (ProjectivePoint BigNat#
    sx BigNat#
    sy BigNat#
    sz) =
        if BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    sz then ProjectivePoint
    zro else BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint BigNat#
    r18 BigNat#
    r23 BigNat#
    r13

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

    -- | Compute the elliptic curve group addition operation, including the special
    --   case for adding points which might be the identity.
    ec_add :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add :: PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t
      | BigNat# -> Bool
    BN.bigNatIsZero (ProjectivePoint -> BigNat#
    pz ProjectivePoint
    s) = ProjectivePoint
    t
      | BigNat# -> Bool
    BN.bigNatIsZero (ProjectivePoint -> BigNat#
    pz ProjectivePoint
    t) = ProjectivePoint
    s
      | Bool
    otherwise = PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add_nonzero PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    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 :: PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t = PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    u
      where u :: ProjectivePoint
    u = case BigNat# -> BigNat# -> (# (# #) | BigNat# #)
    BN.bigNatSub (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p) (ProjectivePoint -> BigNat#
    py ProjectivePoint
    t) of
                  (# | BigNat#
    y' #)    -> ProjectivePoint
    t{ py :: BigNat#
    py = BigNat#
    y' }
                  (# (# #) | #) -> String -> [String] -> ProjectivePoint
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "ec_sub" [String
    "cooridnate not in reduced form!", Integer -> String
    forall a. Show a => a -> String
    show (BigNat# -> Integer
    BN.bigNatToInteger (ProjectivePoint -> BigNat#
    py ProjectivePoint
    t))]
    {-# INLINE ec_sub #-}

    ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_negate :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_negate PrimeModulus
    p ProjectivePoint
    s = ProjectivePoint
    s{ py :: BigNat#
    py = BigNat# -> BigNat# -> BigNat#
    BN.bigNatSubUnsafe (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p) (ProjectivePoint -> BigNat#
    py ProjectivePoint
    s) }
    {-# INLINE ec_negate #-}

    -- | Compute the elliptic curve group addition operation
    --   for values known not to be the identity.
    --   In other words, if @S@ and @T@ are projective points on a curve,
    --   with nonzero @z@ coordinate this operation computes @S+T@ in the ECC group.
    --
    --   In geometric terms, this operation computes a line that passes through
    --   @S@ and @T@, and finds the (unique) other point @R@ where the line intersects
    --   the curve; then returns the point @R'@, which is @R@ reflected across the x axis.
    --   In the special case where @S == T@, we instead call the @ec_double@ operation,
    --   which instead computes a tangent line to @S@ .
    ec_add_nonzero :: PrimeModulus -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add_nonzero :: PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add_nonzero PrimeModulus
    p s :: ProjectivePoint
    s@(ProjectivePoint BigNat#
    sx BigNat#
    sy BigNat#
    sz) (ProjectivePoint BigNat#
    tx BigNat#
    ty BigNat#
    tz) =
        if BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    r13 then
          if BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    r14 then
            PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p ProjectivePoint
    s
          else
            ProjectivePoint
    zro
        else
          BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint BigNat#
    r32 BigNat#
    r37 BigNat#
    r27

      where
      tNormalized :: Bool
    tNormalized = BigNat# -> Bool
    BN.bigNatIsOne BigNat#
    tz

      tz2 :: BigNat#
    tz2 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    tz
      tz3 :: BigNat#
    tz3 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    tz BigNat#
    tz2

      r5 :: BigNat#
    r5  = if Bool
    tNormalized then BigNat#
    sx else PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    sx BigNat#
    tz2
      r7 :: BigNat#
    r7  = if Bool
    tNormalized then BigNat#
    sy else PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    sy BigNat#
    tz3

      r9 :: BigNat#
    r9  = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    sz                  {-  9: t7 <- (t3)^2 -}
      r10 :: BigNat#
    r10 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    tx BigNat#
    r9               {- 10: t4 <- t4 * t7 -}
      r11 :: BigNat#
    r11 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    sz BigNat#
    r9               {- 11: t7 <- t3 * t7 -}
      r12 :: BigNat#
    r12 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    ty BigNat#
    r11              {- 12: t5 <- t5 * t7 -}
      r13 :: BigNat#
    r13 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p BigNat#
    r5 BigNat#
    r10              {- 13: t4 <- t1 - t4 -}
      r14 :: BigNat#
    r14 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p BigNat#
    r7 BigNat#
    r12              {- 14: t5 <- t2 - t5 -}

      r22 :: BigNat#
    r22 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p (PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    r5) BigNat#
    r13     {- 22: t1 <- 2*t1 - t4 -}
      r23 :: BigNat#
    r23 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p (PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    r7) BigNat#
    r14     {- 23: t2 <- 2*t2 - t5 -}

      r25 :: BigNat#
    r25 = if Bool
    tNormalized then BigNat#
    sz else PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    sz BigNat#
    tz

      r27 :: BigNat#
    r27 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    r25 BigNat#
    r13             {- 27: t3 <- t3 * t4 -}
      r28 :: BigNat#
    r28 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    r13                 {- 28: t7 <- (t4)^2 -}
      r29 :: BigNat#
    r29 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    r13 BigNat#
    r28             {- 29: t4 <- t4 * t7 -}
      r30 :: BigNat#
    r30 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    r22 BigNat#
    r28             {- 30: t7 <- t1 * t7 -}
      r31 :: BigNat#
    r31 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    r14                 {- 31: t1 <- (t5)^2 -}
      r32 :: BigNat#
    r32 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p BigNat#
    r31 BigNat#
    r30             {- 32: t1 <- t1 - t7 -}
      r33 :: BigNat#
    r33 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p BigNat#
    r30 (PrimeModulus -> BigNat# -> BigNat#
    mul2 PrimeModulus
    p BigNat#
    r32)    {- 33: t7 <- t7 - 2*t1 -}
      r34 :: BigNat#
    r34 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    r14 BigNat#
    r33             {- 34: t5 <- t5 * t7 -}
      r35 :: BigNat#
    r35 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul    PrimeModulus
    p BigNat#
    r23 BigNat#
    r29             {- 35: t4 <- t2 * t4 -}
      r36 :: BigNat#
    r36 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_sub    PrimeModulus
    p BigNat#
    r34 BigNat#
    r35             {- 36: t2 <- t5 - t4 -}
      r37 :: BigNat#
    r37 = PrimeModulus -> BigNat# -> BigNat#
    mod_half   PrimeModulus
    p BigNat#
    r36                 {- 37: t2 <- t2/2 -}

    -- | Given a nonidentity projective point, normalize it so that
    --   its z component is 1.  This helps to avoid some modular
    --   multiplies in @ec_add@, and may be a win if the point will
    --   be added many times.
    ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize :: PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p s :: ProjectivePoint
    s@(ProjectivePoint BigNat#
    x BigNat#
    y BigNat#
    z)
      | BigNat# -> Bool
    BN.bigNatIsOne BigNat#
    z = ProjectivePoint
    s
      | Bool
    otherwise = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint BigNat#
    x' BigNat#
    y' ((# #) -> BigNat#
    BN.oneBigNat (# #))
     where
      m :: BigNat#
    m = PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p

      l :: BigNat#
    l  = BigNat# -> BigNat# -> BigNat#
    BN.recipModBigNat BigNat#
    z BigNat#
    m
      l2 :: BigNat#
    l2 = BigNat# -> BigNat#
    BN.bigNatSqr BigNat#
    l
      l3 :: BigNat#
    l3 = BigNat# -> BigNat# -> BigNat#
    BN.bigNatMul BigNat#
    l BigNat#
    l2

      x' :: BigNat#
    x' = (BigNat# -> BigNat# -> BigNat#
    BN.bigNatMul BigNat#
    x BigNat#
    l2) BigNat# -> BigNat# -> BigNat#
    `BN.bigNatRem` BigNat#
    m
      y' :: BigNat#
    y' = (BigNat# -> BigNat# -> BigNat#
    BN.bigNatMul BigNat#
    y BigNat#
    l3) BigNat# -> BigNat# -> BigNat#
    `BN.bigNatRem` BigNat#
    m

    -- | Given an integer @k@ and a projective point @S@, compute
    --   the scalar multiplication @kS@, which is @S@ added to itself
    --   @k@ times.
    ec_mult :: PrimeModulus -> Integer -> ProjectivePoint -> ProjectivePoint
    ec_mult :: PrimeModulus -> Integer -> ProjectivePoint -> ProjectivePoint
    ec_mult PrimeModulus
    p Integer
    d ProjectivePoint
    s
      | Integer
    d Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0    = ProjectivePoint
    zro
      | Integer
    d Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1    = ProjectivePoint
    s
      | BigNat# -> Bool
    BN.bigNatIsZero (ProjectivePoint -> BigNat#
    pz ProjectivePoint
    s) = ProjectivePoint
    zro
      | Bool
    otherwise =
          case Int#
    m of
            Int#
    0# -> String -> [String] -> ProjectivePoint
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "ec_mult" [String
    "modulus too large", Integer -> String
    forall a. Show a => a -> String
    show (BigNat# -> Integer
    BN.bigNatToInteger (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p))]
            Int#
    _  -> Int# -> ProjectivePoint -> ProjectivePoint
    go Int#
    m ProjectivePoint
    zro

     where
       s' :: ProjectivePoint
    s' = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p ProjectivePoint
    s
       h :: Integer
    h  = Integer
    3Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    d

       d' :: BigNat#
    d' = Integer -> BigNat#
    BN.integerToBigNat Integer
    d
       h' :: BigNat#
    h' = Integer -> BigNat#
    BN.integerToBigNat Integer
    h

       m :: Int#
    m = case Integer -> Integer
    widthInteger Integer
    h of
             BN.IS Int#
    mint -> Int#
    mint
             Integer
    _ -> Int#
    0#

       go :: Int# -> ProjectivePoint -> ProjectivePoint
       go :: Int# -> ProjectivePoint -> ProjectivePoint
    go Int#
    i !ProjectivePoint
    r
         | Int# -> Bool
    forall a. Int# -> a
    tagToEnum# (Int#
    i Int# -> Int# -> Int#
    ==# Int#
    0#) = ProjectivePoint
    r
         | Bool
    otherwise = Int# -> ProjectivePoint -> ProjectivePoint
    go (Int#
    i Int# -> Int# -> Int#
    -# Int#
    1#) ProjectivePoint
    r'

        where
          h_i :: Bool
    h_i = BigNat# -> Int# -> Bool
    BN.testBitBigNat BigNat#
    h' Int#
    i
          d_i :: Bool
    d_i = BigNat# -> Int# -> Bool
    BN.testBitBigNat BigNat#
    d' Int#
    i

          r' :: ProjectivePoint
    r' = if Bool
    h_i then
                 if Bool
    d_i then ProjectivePoint
    r2 else PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    s'
               else
                 if Bool
    d_i then PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    s' else ProjectivePoint
    r2

          r2 :: ProjectivePoint
    r2 = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p ProjectivePoint
    r

    {-# INLINE normalizeForTwinMult #-}

    -- | Compute the sum and difference of the given points,
    --   and normalize all four values.  This can be done jointly
    --   in a more efficient way than computing the necessary
    --   field inverses separately.
    --   When given points S and T, the returned tuple contains
    --   normalized representations for (S, T, S+T, S-T).
    --
    --   Note there are some special cases that must be handled separately.
    normalizeForTwinMult ::
      PrimeModulus -> ProjectivePoint -> ProjectivePoint ->
      (ProjectivePoint, ProjectivePoint, ProjectivePoint, ProjectivePoint)
    normalizeForTwinMult :: PrimeModulus
    -> ProjectivePoint
    -> ProjectivePoint
    -> (ProjectivePoint, ProjectivePoint, ProjectivePoint,
        ProjectivePoint)
    normalizeForTwinMult PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t
         -- S == 0 && T == 0
       | BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    a Bool -> Bool -> Bool
    && BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    b =
            (ProjectivePoint
    zro, ProjectivePoint
    zro, ProjectivePoint
    zro, ProjectivePoint
    zro)

         -- S == 0 && T != 0
       | BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    a =
            let tnorm :: ProjectivePoint
    tnorm = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p ProjectivePoint
    t
             in (ProjectivePoint
    zro, ProjectivePoint
    tnorm, ProjectivePoint
    tnorm, PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_negate PrimeModulus
    p ProjectivePoint
    tnorm)

         -- T == 0 && S != 0
       | BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    b =
            let snorm :: ProjectivePoint
    snorm = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p ProjectivePoint
    s
             in (ProjectivePoint
    snorm, ProjectivePoint
    zro, ProjectivePoint
    snorm, ProjectivePoint
    snorm)

         -- S+T == 0, both != 0
       | BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    c =
            let snorm :: ProjectivePoint
    snorm = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p ProjectivePoint
    s
             in (ProjectivePoint
    snorm, PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_negate PrimeModulus
    p ProjectivePoint
    snorm, ProjectivePoint
    zro, PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p ProjectivePoint
    snorm)

         -- S-T == 0, both != 0
       | BigNat# -> Bool
    BN.bigNatIsZero BigNat#
    d =
            let snorm :: ProjectivePoint
    snorm = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_normalize PrimeModulus
    p ProjectivePoint
    s
             in (ProjectivePoint
    snorm, ProjectivePoint
    snorm, PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p ProjectivePoint
    snorm, ProjectivePoint
    zro)

         -- S, T, S+T and S-T all != 0
       | Bool
    otherwise = (ProjectivePoint
    s',ProjectivePoint
    t',ProjectivePoint
    spt',ProjectivePoint
    smt')

      where
      spt :: ProjectivePoint
    spt = PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t
      smt :: ProjectivePoint
    smt = PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t

      m :: BigNat#
    m = PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p

      a :: BigNat#
    a = ProjectivePoint -> BigNat#
    pz ProjectivePoint
    s
      b :: BigNat#
    b = ProjectivePoint -> BigNat#
    pz ProjectivePoint
    t
      c :: BigNat#
    c = ProjectivePoint -> BigNat#
    pz ProjectivePoint
    spt
      d :: BigNat#
    d = ProjectivePoint -> BigNat#
    pz ProjectivePoint
    smt

      ab :: BigNat#
    ab  = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    a BigNat#
    b
      cd :: BigNat#
    cd  = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    c BigNat#
    d
      abc :: BigNat#
    abc = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    ab BigNat#
    c
      abd :: BigNat#
    abd = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    ab BigNat#
    d
      acd :: BigNat#
    acd = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    a BigNat#
    cd
      bcd :: BigNat#
    bcd = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    b BigNat#
    cd

      abcd :: BigNat#
    abcd = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    a BigNat#
    bcd

      e :: BigNat#
    e = BigNat# -> BigNat# -> BigNat#
    BN.recipModBigNat BigNat#
    abcd BigNat#
    m

      a_inv :: BigNat#
    a_inv = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    e BigNat#
    bcd
      b_inv :: BigNat#
    b_inv = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    e BigNat#
    acd
      c_inv :: BigNat#
    c_inv = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    e BigNat#
    abd
      d_inv :: BigNat#
    d_inv = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    e BigNat#
    abc

      a_inv2 :: BigNat#
    a_inv2 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    a_inv
      a_inv3 :: BigNat#
    a_inv3 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    a_inv BigNat#
    a_inv2

      b_inv2 :: BigNat#
    b_inv2 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    b_inv
      b_inv3 :: BigNat#
    b_inv3 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    b_inv BigNat#
    b_inv2

      c_inv2 :: BigNat#
    c_inv2 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    c_inv
      c_inv3 :: BigNat#
    c_inv3 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    c_inv BigNat#
    c_inv2

      d_inv2 :: BigNat#
    d_inv2 = PrimeModulus -> BigNat# -> BigNat#
    mod_square PrimeModulus
    p BigNat#
    d_inv
      d_inv3 :: BigNat#
    d_inv3 = PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p BigNat#
    d_inv BigNat#
    d_inv2

      s' :: ProjectivePoint
    s'   = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    px ProjectivePoint
    s) BigNat#
    a_inv2) (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    py ProjectivePoint
    s) BigNat#
    a_inv3) ((# #) -> BigNat#
    BN.oneBigNat (# #))
      t' :: ProjectivePoint
    t'   = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    px ProjectivePoint
    t) BigNat#
    b_inv2) (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    py ProjectivePoint
    t) BigNat#
    b_inv3) ((# #) -> BigNat#
    BN.oneBigNat (# #))

      spt' :: ProjectivePoint
    spt' = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    px ProjectivePoint
    spt) BigNat#
    c_inv2) (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    py ProjectivePoint
    spt) BigNat#
    c_inv3) ((# #) -> BigNat#
    BN.oneBigNat (# #))
      smt' :: ProjectivePoint
    smt' = BigNat# -> BigNat# -> BigNat# -> ProjectivePoint
    ProjectivePoint (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    px ProjectivePoint
    smt) BigNat#
    d_inv2) (PrimeModulus -> BigNat# -> BigNat# -> BigNat#
    mod_mul PrimeModulus
    p (ProjectivePoint -> BigNat#
    py ProjectivePoint
    smt) BigNat#
    d_inv3) ((# #) -> BigNat#
    BN.oneBigNat (# #))

    -- | Given an integer @j@ and a projective point @S@, together with
    --   another integer @k@ and point @T@ compute the "twin" scalar
    --   the scalar multiplication @jS + kT@.  This computation can be done
    --   essentially the same number of modular arithmetic operations
    --   as a single scalar multiplication by doing some additional bookkeeping
    --   and setup.
    ec_twin_mult :: PrimeModulus ->
      Integer -> ProjectivePoint ->
      Integer -> ProjectivePoint ->
      ProjectivePoint
    ec_twin_mult :: PrimeModulus
    -> Integer
    -> ProjectivePoint
    -> Integer
    -> ProjectivePoint
    -> ProjectivePoint
    ec_twin_mult PrimeModulus
    p (Integer -> BigNat#
    BN.integerToBigNat -> BigNat#
    d0) ProjectivePoint
    s (Integer -> BigNat#
    BN.integerToBigNat -> BigNat#
    d1) ProjectivePoint
    t =
       case Int#
    m of
         Int#
    0# -> String -> [String] -> ProjectivePoint
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "ec_twin_mult" [String
    "modulus too large", Integer -> String
    forall a. Show a => a -> String
    show (BigNat# -> Integer
    BN.bigNatToInteger (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p))]
         Int#
    _  -> Int# -> CState -> CState -> ProjectivePoint -> ProjectivePoint
    go Int#
    m CState
    init_c0 CState
    init_c1 ProjectivePoint
    zro

     where
      (ProjectivePoint
    s',ProjectivePoint
    t',ProjectivePoint
    spt',ProjectivePoint
    smt') = PrimeModulus
    -> ProjectivePoint
    -> ProjectivePoint
    -> (ProjectivePoint, ProjectivePoint, ProjectivePoint,
        ProjectivePoint)
    normalizeForTwinMult PrimeModulus
    p ProjectivePoint
    s ProjectivePoint
    t

      m :: Int#
    m = case Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    max Integer
    4 (Integer -> Integer
    widthInteger (BigNat# -> Integer
    BN.bigNatToInteger (PrimeModulus -> BigNat#
    primeMod PrimeModulus
    p))) of
            BN.IS Int#
    mint -> Int#
    mint
            Integer
    _ -> Int#
    0# -- if `m` doesn't fit into an Int, should be impossible

      init_c0 :: CState
    init_c0 = Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> CState
    C Bool
    False Bool
    False (BigNat# -> Int# -> Bool
    tst BigNat#
    d0 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    1#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d0 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    2#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d0 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    3#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d0 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    4#))
      init_c1 :: CState
    init_c1 = Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> CState
    C Bool
    False Bool
    False (BigNat# -> Int# -> Bool
    tst BigNat#
    d1 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    1#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d1 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    2#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d1 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    3#)) (BigNat# -> Int# -> Bool
    tst BigNat#
    d1 (Int#
    m Int# -> Int# -> Int#
    -# Int#
    4#))

      tst :: BigNat# -> Int# -> Bool
    tst BigNat#
    x Int#
    i
        | Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    >=# Int#
    0#) = BigNat# -> Int# -> Bool
    BN.testBitBigNat BigNat#
    x Int#
    i
        | Bool
    otherwise = Bool
    False

      f :: Int# -> Int#
    f Int#
    i =
        if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    18#) then
          if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    12#) then
            if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    4#) then
              Int#
    12#
            else
              Int#
    14#
          else
            if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    14#) then
              Int#
    12#
            else
              Int#
    10#
        else
          if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    22#) then
            Int#
    9#
          else
            if Int# -> Bool
    isTrue# (Int#
    i Int# -> Int# -> Int#
    <# Int#
    24#) then
              Int#
    11#
            else
              Int#
    12#

      go :: Int# -> CState -> CState -> ProjectivePoint -> ProjectivePoint
    go !Int#
    k !CState
    c0 !CState
    c1 !ProjectivePoint
    r = if Int# -> Bool
    isTrue# (Int#
    k Int# -> Int# -> Int#
    <# Int#
    0#) then ProjectivePoint
    r else Int# -> CState -> CState -> ProjectivePoint -> ProjectivePoint
    go (Int#
    k Int# -> Int# -> Int#
    -# Int#
    1#) CState
    c0' CState
    c1' ProjectivePoint
    r'
        where
          h0 :: Int#
    h0  = CState -> Int#
    cStateToH CState
    c0
          h1 :: Int#
    h1  = CState -> Int#
    cStateToH CState
    c1
          u0 :: Int#
    u0  = if Int# -> Bool
    isTrue# (Int#
    h0 Int# -> Int# -> Int#
    <# Int# -> Int#
    f Int#
    h1) then Int#
    0# else (if CState -> Bool
    cHead CState
    c0 then Int#
    -1# else Int#
    1#)
          u1 :: Int#
    u1  = if Int# -> Bool
    isTrue# (Int#
    h1 Int# -> Int# -> Int#
    <# Int# -> Int#
    f Int#
    h0) then Int#
    0# else (if CState -> Bool
    cHead CState
    c1 then Int#
    -1# else Int#
    1#)
          c0' :: CState
    c0' = Int# -> CState -> Bool -> CState
    cStateUpdate Int#
    u0 CState
    c0 (BigNat# -> Int# -> Bool
    tst BigNat#
    d0 (Int#
    k Int# -> Int# -> Int#
    -# Int#
    5#))
          c1' :: CState
    c1' = Int# -> CState -> Bool -> CState
    cStateUpdate Int#
    u1 CState
    c1 (BigNat# -> Int# -> Bool
    tst BigNat#
    d1 (Int#
    k Int# -> Int# -> Int#
    -# Int#
    5#))

          r2 :: ProjectivePoint
    r2 = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    ec_double PrimeModulus
    p ProjectivePoint
    r

          r' :: ProjectivePoint
    r' =
            case Int#
    u0 of
              Int#
    -1# ->
                case Int#
    u1 of
                  Int#
    -1# -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    spt'
                  Int#
    1#  -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    smt'
                  Int#
    _   -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    s'
              Int#
    1#  ->
                case Int#
    u1 of
                  Int#
    -1# -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    smt'
                  Int#
    1#  -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    spt'
                  Int#
    _   -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    s'
              Int#
    _   ->
                case Int#
    u1 of
                  Int#
    -1# -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_sub PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    t'
                  Int#
    1#  -> PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    ec_add PrimeModulus
    p ProjectivePoint
    r2 ProjectivePoint
    t'
                  Int#
    _   -> ProjectivePoint
    r2

    data CState = C !Bool !Bool !Bool !Bool !Bool !Bool

    {-# INLINE cHead #-}
    cHead :: CState -> Bool
    cHead :: CState -> Bool
    cHead (C Bool
    c0 Bool
    _ Bool
    _ Bool
    _ Bool
    _ Bool
    _) = Bool
    c0

    {-# INLINE cStateToH #-}
    cStateToH :: CState -> Int#
    cStateToH :: CState -> Int#
    cStateToH c :: CState
    c@(C Bool
    c0 Bool
    _ Bool
    _ Bool
    _ Bool
    _ Bool
    _) =
      if Bool
    c0 then Int#
    31# Int# -> Int# -> Int#
    -# CState -> Int#
    cStateToInt CState
    c else CState -> Int#
    cStateToInt CState
    c

    {-# INLINE cStateToInt #-}
    cStateToInt :: CState -> Int#
    cStateToInt :: CState -> Int#
    cStateToInt (C Bool
    _ Bool
    c1 Bool
    c2 Bool
    c3 Bool
    c4 Bool
    c5) =
      (Bool -> Int#
    forall a. a -> Int#
    dataToTag# Bool
    c1 Int# -> Int# -> Int#
    `uncheckedIShiftL#` Int#
    4#) Int# -> Int# -> Int#
    +#
      (Bool -> Int#
    forall a. a -> Int#
    dataToTag# Bool
    c2 Int# -> Int# -> Int#
    `uncheckedIShiftL#` Int#
    3#) Int# -> Int# -> Int#
    +#
      (Bool -> Int#
    forall a. a -> Int#
    dataToTag# Bool
    c3 Int# -> Int# -> Int#
    `uncheckedIShiftL#` Int#
    2#) Int# -> Int# -> Int#
    +#
      (Bool -> Int#
    forall a. a -> Int#
    dataToTag# Bool
    c4 Int# -> Int# -> Int#
    `uncheckedIShiftL#` Int#
    1#) Int# -> Int# -> Int#
    +#
      (Bool -> Int#
    forall a. a -> Int#
    dataToTag# Bool
    c5)

    {-# INLINE cStateUpdate #-}
    cStateUpdate :: Int# -> CState -> Bool -> CState
    cStateUpdate :: Int# -> CState -> Bool -> CState
    cStateUpdate Int#
    u (C Bool
    _ Bool
    c1 Bool
    c2 Bool
    c3 Bool
    c4 Bool
    c5) Bool
    e =
      case Int#
    u of
        Int#
    0# -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> CState
    C Bool
    c1 Bool
    c2 Bool
    c3 Bool
    c4 Bool
    c5 Bool
    e
        Int#
    _  -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> CState
    C (Bool -> Bool
    not Bool
    c1) Bool
    c2 Bool
    c3 Bool
    c4 Bool
    c5 Bool
    e