-----------------------------------------------------------------------------
-- |
-- 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 MagicHash #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Cryptol.PrimeEC
  ( PrimeModulus
  , primeModulus
  , ProjectivePoint(..)
  , integerToBigNat
  , Integer.bigNatToInteger

  , ec_double
  , ec_add_nonzero
  , ec_mult
  , ec_twin_mult
  ) where


import           GHC.Integer.GMP.Internals (BigNat)
import qualified GHC.Integer.GMP.Internals as Integer
import           GHC.Prim
import           Data.Bits

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
  }

-- | 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
Integer.oneBigNat BigNat
Integer.oneBigNat BigNat
Integer.zeroBigNat

-- | Coerce an integer value to a @BigNat@.  This operation only really makes
--   sense for nonnegative values, but this condition is not checked.
integerToBigNat :: Integer -> BigNat
integerToBigNat :: Integer -> BigNat
integerToBigNat (Integer.S# Int#
i)  = Word# -> BigNat
Integer.wordToBigNat (Int# -> Word#
int2Word# Int#
i)
integerToBigNat (Integer.Jp# BigNat
b) = BigNat
b
integerToBigNat (Integer.Jn# BigNat
b) = BigNat
b

-- | 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 = BigNat -> PrimeModulus
PrimeModulus (BigNat -> PrimeModulus)
-> (Integer -> BigNat) -> Integer -> PrimeModulus
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> BigNat
integerToBigNat
{-# INLINE primeModulus #-}


-- Barrett reduction replaces a division by the modulus with
-- two multiplications and some shifting, masking, and additions
-- (and some fairly negligible pre-processing). For the size of
-- moduli we are working with for ECC, this does not appear to be
-- a performance win.  Even for largest NIST curve (P-521) Barrett
-- reduction is about 20% slower than naive modular reduction.
-- Smaller curves are worse WRT the baseline.

-- {-# INLINE primeModulus #-}
-- primeModulus :: Integer -> PrimeModulus
-- primeModulus = untrie modulusParameters

-- data PrimeModulus = PrimeModulus
--   { primeMod :: !Integer
--   , barrettInverse :: !Integer
--   , barrettK       :: !Int
--   , barrettMask    :: !Integer
--   }
--  deriving (Show, Eq)

-- {-# NOINLINE modulusParameters #-}
-- modulusParameters :: Integer :->: PrimeModulus
-- modulusParameters = trie computeModulusParameters

-- computeModulusParameters :: Integer -> PrimeModulus
-- computeModulusParameters p = PrimeModulus p inv k mask
--   where
--   k = fromInteger w

--   b :: Integer
--   b = 2 ^ (64::Int)

--   -- w is the number of 64-bit words required to express p
--   w = (widthInteger p + 63) `div` 64

--   mask = b^(k+1) - 1

--   -- inv = floor ( b^(2*k) / p )
--   inv = b^(2*k) `div` p

-- barrettReduction :: PrimeModulus -> Integer -> Integer
-- barrettReduction p x = go r3
--   where
--     m    = primeMod p
--     k    = barrettK p
--     inv  = barrettInverse p
--     mask = barrettMask p

--     -- q1 <- floor (x / b^(k-1))
--     q1 = x `shiftR` (64 * (k-1))

--     -- q2 <- q1 * floor ( b^(2*k) / m )
--     q2 = q1 * inv

--     -- q3 <- floor (q2 / b^(k+1))
--     q3 = q2 `shiftR` (64 * (k+1))

--     -- r1 <- x mod b^(k+1)
--     r1 = x .&. mask

--     -- r2 <- (q3 * m) mod b^(k+1)
--     r2 = (q3 * m) .&. mask

--     -- r3 <- r1 - r2
--     r3 = r1 - r2

--     -- up to 2 multiples of m must be removed
--     go z = if z > m then go (z - m) else z

-- | Modular addition of two values.  The inputs are
--   required to be in reduced form, and will output
--   a value in reduced form.
mod_add :: PrimeModulus -> BigNat -> BigNat -> BigNat
mod_add :: PrimeModulus -> BigNat -> BigNat -> BigNat
mod_add PrimeModulus
p !BigNat
x !BigNat
y =
    case BigNat -> Int#
Integer.isNullBigNat# BigNat
rmp of
      Int#
0# -> BigNat
rmp
      Int#
_  -> BigNat
r
  where r :: BigNat
r = BigNat -> BigNat -> BigNat
Integer.plusBigNat BigNat
x BigNat
y
        rmp :: BigNat
rmp = BigNat -> BigNat -> BigNat
Integer.minusBigNat BigNat
r (PrimeModulus -> BigNat
primeMod PrimeModulus
p)

-- | 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
Integer.testBitBigNat BigNat
x Int#
0# then BigNat
qodd else BigNat
qeven
  where
  qodd :: BigNat
qodd  = (BigNat -> BigNat -> BigNat
Integer.plusBigNat BigNat
x (PrimeModulus -> BigNat
primeMod PrimeModulus
p)) BigNat -> Int# -> BigNat
`Integer.shiftRBigNat` Int#
1#
  qeven :: BigNat
qeven = BigNat
x BigNat -> Int# -> BigNat
`Integer.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
Integer.timesBigNat BigNat
x BigNat
y) BigNat -> BigNat -> BigNat
`Integer.remBigNat` (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 = PrimeModulus -> BigNat -> BigNat -> BigNat
mod_add PrimeModulus
p BigNat
x (BigNat -> BigNat -> BigNat
Integer.minusBigNat (PrimeModulus -> BigNat
primeMod PrimeModulus
p) BigNat
y)

-- | Compute the modular square of an input value @x@; that is, @x*x@.
--   The input is not required to be in reduced form, and the output
--   will be in reduced form.
mod_square :: PrimeModulus -> BigNat -> BigNat
mod_square :: PrimeModulus -> BigNat -> BigNat
mod_square PrimeModulus
p !BigNat
x = BigNat -> BigNat
Integer.sqrBigNat BigNat
x BigNat -> BigNat -> BigNat
`Integer.remBigNat` 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 =
    case BigNat -> Int#
Integer.isNullBigNat# BigNat
rmp of
      Int#
0# -> BigNat
rmp
      Int#
_  -> BigNat
r
 where
   r :: BigNat
r = BigNat
x BigNat -> Int# -> BigNat
`Integer.shiftLBigNat` Int#
1#
   rmp :: BigNat
rmp = BigNat -> BigNat -> BigNat
Integer.minusBigNat BigNat
r (PrimeModulus -> BigNat
primeMod PrimeModulus
p)

-- | 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 (BigNat -> BigNat) -> BigNat -> BigNat
forall a b. (a -> b) -> a -> b
$! 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 (BigNat -> BigNat) -> BigNat -> BigNat
forall a b. (a -> b) -> a -> b
$! 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 (BigNat -> BigNat) -> BigNat -> BigNat
forall a b. (a -> b) -> a -> b
$! 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
Integer.isZeroBigNat 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
Integer.isZeroBigNat (ProjectivePoint -> BigNat
pz ProjectivePoint
s) = ProjectivePoint
t
  | BigNat -> Bool
Integer.isZeroBigNat (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 = ProjectivePoint
t{ py :: BigNat
py = BigNat -> BigNat -> BigNat
Integer.minusBigNat (PrimeModulus -> BigNat
primeMod PrimeModulus
p) (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
Integer.minusBigNat (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
Integer.isZeroBigNat BigNat
r13 then
      if BigNat -> Bool
Integer.isZeroBigNat 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 -> BigNat -> Bool
Integer.eqBigNat BigNat
tz BigNat
Integer.oneBigNat

  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 -> BigNat -> Bool
Integer.eqBigNat BigNat
z BigNat
Integer.oneBigNat = ProjectivePoint
s
  | Bool
otherwise = BigNat -> BigNat -> BigNat -> ProjectivePoint
ProjectivePoint BigNat
x' BigNat
y' BigNat
Integer.oneBigNat
 where
  m :: BigNat
m = PrimeModulus -> BigNat
primeMod PrimeModulus
p

  l :: BigNat
l  = BigNat -> BigNat -> BigNat
Integer.recipModBigNat BigNat
z BigNat
m
  l2 :: BigNat
l2 = BigNat -> BigNat
Integer.sqrBigNat BigNat
l
  l3 :: BigNat
l3 = BigNat -> BigNat -> BigNat
Integer.timesBigNat BigNat
l BigNat
l2

  x' :: BigNat
x' = (BigNat -> BigNat -> BigNat
Integer.timesBigNat BigNat
x BigNat
l2) BigNat -> BigNat -> BigNat
`Integer.remBigNat` BigNat
m
  y' :: BigNat
y' = (BigNat -> BigNat -> BigNat
Integer.timesBigNat BigNat
y BigNat
l3) BigNat -> BigNat -> BigNat
`Integer.remBigNat` 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
Integer.isZeroBigNat (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
Integer.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
integerToBigNat Integer
d
   h' :: BigNat
h' = Integer -> BigNat
integerToBigNat Integer
h

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

   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
Integer.testBitBigNat BigNat
h' Int#
i
      d_i :: Bool
d_i = BigNat -> Int# -> Bool
Integer.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
Integer.isZeroBigNat BigNat
a Bool -> Bool -> Bool
&& BigNat -> Bool
Integer.isZeroBigNat BigNat
b =
        (ProjectivePoint
zro, ProjectivePoint
zro, ProjectivePoint
zro, ProjectivePoint
zro)

     -- S == 0 && T != 0
   | BigNat -> Bool
Integer.isZeroBigNat 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
Integer.isZeroBigNat 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
Integer.isZeroBigNat 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
Integer.isZeroBigNat 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
Integer.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
Integer.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
Integer.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
Integer.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
Integer.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
integerToBigNat -> BigNat
d0) ProjectivePoint
s (Integer -> BigNat
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
Integer.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
Integer.bigNatToInteger (PrimeModulus -> BigNat
primeMod PrimeModulus
p))) of
        Integer.S# 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
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
>=# Int#
0#) = BigNat -> Int# -> Bool
Integer.testBitBigNat BigNat
x Int#
i
    | Bool
otherwise = Bool
False

  f :: Int# -> Int#
f Int#
i =
    if Int# -> Bool
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
<# Int#
18#) then
      if Int# -> Bool
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
<# Int#
12#) then
        if Int# -> Bool
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
<# Int#
4#) then
          Int#
12#
        else
          Int#
14#
      else
        if Int# -> Bool
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
<# Int#
14#) then
          Int#
12#
        else
          Int#
10#
    else
      if Int# -> Bool
forall a. Int# -> a
tagToEnum# (Int#
i Int# -> Int# -> Int#
<# Int#
22#) then
        Int#
9#
      else
        if Int# -> Bool
forall a. Int# -> a
tagToEnum# (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
forall a. Int# -> a
tagToEnum# (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
forall a. Int# -> a
tagToEnum# (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
forall a. Int# -> a
tagToEnum# (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
forall a. Bits a => a -> a
complement Bool
c1) Bool
c2 Bool
c3 Bool
c4 Bool
c5 Bool
e