-----------------------------------------------------------------------------
-- |
-- 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 = y' `BN.bigNatRem` (primeMod p) }
              (# (# #) | #) -> 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 = (BN.bigNatSubUnsafe (primeMod p) (py s))  `BN.bigNatRem` (primeMod p) }
{-# 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
"integer with 0 width", Integer -> String
forall a. Show a => a -> String
show Integer
h]
        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