-----------------------------------------------------------------------------
-- |
-- Module      :  Crypto.ECC.Weierstrass.Internal.Curvemath
-- Copyright   :  (c) Marcel Fourné 20[09..]
-- License     :  BSD3
-- Maintainer  :  Marcel Fourné (haskell@marcelfourne.de)
-- Stability   :  beta
-- Portability :  Good
--
-- This module contain the internal functions. It's use should be limited to the ECDH and ECDSA modules, which export certain types without constructors, so the timing attack surface is only over the verified functions.
-- ECC Base algorithms & point formats for NIST Curves as specified in NISTReCur.pdf[http://csrc.nist.gov/groups/ST/toolkit/documents/dss/NISTReCur.pdf]
-- 
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -O2 -feager-blackholing #-}
{-# LANGUAGE Safe, GADTs, DeriveDataTypeable, NoImplicitPrelude, StrictData #-}

module Crypto.ECC.Weierstrass.Internal.Curvemath where

import safe Prelude (Eq,Show,(==),(&&),Integer,Int,show,Bool,(++),(-),otherwise,(<),mod,(^),(+))
import safe qualified Data.Bits as B ((.&.))
import safe Data.Typeable(Typeable)
-- import safe Crypto.Common
import safe qualified Crypto.Fi as FP
-- import safe qualified Crypto.FPrime as FP
-- import safe qualified Crypto.F2 as F2

-- | all Elliptic Curves, the parameters being the BitLength L, A, B and P
data EC a where
  -- the Integer Curves, having the form y^2*z=x^3-3*x*z^2+B*z^3 mod P (projective with a = -3); relevant for "ison"
  ECi :: Int          -- the effective bitlength
      -> FP.FPrime    -- b
      -> FP.FPrime    -- p
      -> FP.FPrime    -- r
      -> EC FP.FPrime -- the resulting curve
  -- the Curves on F2, having the form  y^2*z+x*y*z=x^3+a*x^2*z+b*z^3 mod P (projective); relevant for "ison"
{-  ECb :: Int          -- the effective bitlength
      -> Int          -- a, may be 0 or 1
      -> F2.F2        -- b, may be 1 or something larger
      -> F2.F2        -- p
      -> FP.FPrime    -- r
      -> EC F2.F2     -- the resulting curve-}
     deriving(Typeable)

instance Eq (EC a) where
  (ECi Int
l FPrime
b FPrime
p FPrime
r) == :: EC a -> EC a -> Bool
== (ECi Int
l' FPrime
b' FPrime
p' FPrime
r') = Int
lInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
l' Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
b FPrime
b' Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
p FPrime
p' Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
r FPrime
r'
--  (ECb l a b p r) == (ECb l' a' b' p' r') = l==l' && a==a' && F2.eq b b' && F2.eq p p' && FP.eq r r'

instance Show (EC a) where
  show :: EC a -> String
show (ECi Int
l FPrime
b FPrime
p FPrime
r) = String
"Curve with length" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", y^2=x^3-3*x+" String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" mod " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and group order " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
--  show (ECb l a b p r) = "Curve with length" ++ show l ++", y^2=x^3+" ++ show a ++ "*x+" ++ show (F2.toInteger b) ++ " mod " ++ show (F2.toInteger p) ++ " and group order " ++ show r  ++ "."

-- every point has a curve on which it is valid (has to be tested manually), plus possibly some coordinates
-- parametrised by the kind of numbers one which it may be computed
-- point formats may be translated through functions
-- | data of Elliptic Curve Points
data ECPF a where 
  -- Elliptic Curve Point Projective coordinates, three parameters x, y and z, like affine (x/z,y/z)
  ECPp :: FP.FPrime      -- x
       -> FP.FPrime      -- y
       -> FP.FPrime      -- z
       -> ECPF FP.FPrime -- the point
  -- Elliptic Curve Point Projective coordinates in F2, three parameters x, y and z, like affine (x/z,y/z)
{-  ECPpF2 :: F2.F2        -- x
         -> F2.F2        -- y
         -> F2.F2        -- z
         -> ECPF F2.F2   -- the point -}
  deriving(Typeable)
instance Eq (ECPF a) where
  (ECPp FPrime
x FPrime
y FPrime
z) == :: ECPF a -> ECPF a -> Bool
== (ECPp FPrime
x' FPrime
y' FPrime
z') = FPrime -> FPrime -> Bool
FP.eq FPrime
x FPrime
x' Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
y FPrime
y' Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
z FPrime
z'
--  (ECPpF2 x y z) == (ECPpF2 x' y' z') = F2.eq x x' && F2.eq y y' && F2.eq z z'

instance Show (ECPF a) where
  show :: ECPF a -> String
show (ECPp FPrime
x FPrime
y FPrime
z) = String
"x: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" y: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" z: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FPrime -> String
forall a. Show a => a -> String
show FPrime
z
--  show (ECPpF2 x y z) = "x: " ++ show (F2.toInteger x) ++ " y: " ++ show (F2.toInteger y) ++ " z: " ++ show (F2.toInteger z)

-- | internal function, codifies point at infinity, is used in comparisons
isinf :: EC a -> ECPF a -> Bool
isinf :: EC a -> ECPF a -> Bool
isinf (ECi Int
l FPrime
_ FPrime
_ FPrime
_) (ECPp FPrime
x FPrime
_ FPrime
z) = FPrime -> FPrime -> Bool
FP.eq FPrime
x (Int -> FPrime -> FPrime
FP.fromInteger Int
l FPrime
0) {-&& FP.eq y (FP.fromInteger l 1)-} Bool -> Bool -> Bool
&& FPrime -> FPrime -> Bool
FP.eq FPrime
z (Int -> FPrime -> FPrime
FP.fromInteger Int
l FPrime
0)
-- isinf l (ECPpF2 x y z) = F2.eq x (F2.F2 l (zero l)) {-&& F2.eq y (F2.F2 l (one l))-} && F2.eq z (F2.F2 l (zero l))

-- | translate point in internal format to a pair of Integers in affine x and y coordinate
-- | this is intended as interface to other libraries
export :: EC a -> ECPF a -> (Integer,Integer)
export :: EC a -> ECPF a -> (FPrime, FPrime)
export c :: EC a
c@ECi{} pt :: ECPF a
pt@ECPp{} = let (FPrime
x,FPrime
y) = EC a -> ECPF a -> (FPrime, FPrime)
forall a. EC a -> ECPF a -> (FPrime, FPrime)
affine EC a
c ECPF a
pt
                           in (FPrime -> FPrime
FP.toInteger FPrime
x, FPrime -> FPrime
FP.toInteger FPrime
y)
{-export c@ECb{} pt@ECPpF2{} = let (x,y) = affine c pt
                             in (F2.toInteger x, F2.toInteger y) -}

-- | generic getter, returning the affine x and y-value
affine :: EC a -> ECPF a -> (Integer,Integer)
affine :: EC a -> ECPF a -> (FPrime, FPrime)
affine (ECi Int
_ FPrime
_ FPrime
p FPrime
_)   (ECPp FPrime
x FPrime
y FPrime
z) = let z' :: FPrime
z' = FPrime -> FPrime -> FPrime
FP.inv FPrime
p FPrime
z
                                      in (FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x FPrime
z', FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
y FPrime
z')
{-affine (ECb l _ _ p _) a@(ECPpF2 x y z)
  | isinf l a = error "converting Point at Infinity"
  | F2.eq z $ F2.F2 l (zero l) = (F2.fromInteger l 0, F2.fromInteger l 0)
  | F2.eq z $ F2.F2 l (one l) = (x,y)
  | otherwise = let z' = F2.inv p z
                in (F2.mulr p x z', F2.mulr p y z')-}
{-# INLINABLE affine #-}

-- | add an elliptic point onto itself, base for padd a a
pdouble :: EC a -> ECPF a -> ECPF a
pdouble :: EC a -> ECPF a -> ECPF a
pdouble (ECi Int
_ FPrime
b FPrime
p FPrime
_) (ECPp FPrime
x FPrime
y FPrime
z) =
{-
  if isinf l p1
  then p1
  else -- old: let a = ((-3)*z^(2::Int)+3*x^(2::Int)) `mod` p
       let a = FP.mulr p (FP.fromInteger l 3) (FP.mulr p (FP.subr p x z) (FP.addr p x z)) -- since alpha == -3 on NIST-curves
           b = FP.mulr p y z
           c = FP.mulr p x $ FP.mulr p y b
           d = FP.subr p (FP.pow p a (2::Integer)) (FP.mulr p (FP.fromInteger l 8) c)
           x3 = FP.mulr p (FP.fromInteger l 2) $ FP.mulr p b d
           y3 = FP.subr p (FP.mulr p a (FP.subr p (FP.mulr p (FP.fromInteger l 4) c) d)) (FP.mulr p (FP.mulr p (FP.fromInteger l 8) (FP.pow p y (2::Integer))) (FP.pow p b (2::Integer)))
           z3 = FP.mulr p (FP.fromInteger l 8) (FP.pow p b (3::Integer))
       in ECPp x3 y3 z3
-- -}
-- {-
  -- 1060.pdf Alg 6.
  -- TODO: nisttv
  let t0_0 :: FPrime
t0_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x FPrime
x
      t1_0 :: FPrime
t1_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
y FPrime
y
      t2_0 :: FPrime
t2_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
z FPrime
z
      t3_0 :: FPrime
t3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x FPrime
y
      t3_1 :: FPrime
t3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t3_0 FPrime
t3_0 -- 5.
      z3_0 :: FPrime
z3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x FPrime
z
      z3_1 :: FPrime
z3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_0 FPrime
z3_0
      y3_0 :: FPrime
y3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
b FPrime
t2_0
      y3_1 :: FPrime
y3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
y3_0 FPrime
z3_1
      x3_0 :: FPrime
x3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y3_1 FPrime
y3_1 -- 10.
      y3_2 :: FPrime
y3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x3_0 FPrime
y3_1
      x3_1 :: FPrime
x3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t1_0 FPrime
y3_2
      y3_3 :: FPrime
y3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_0 FPrime
y3_2
      y3_4 :: FPrime
y3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x3_1 FPrime
y3_3
      x3_2 :: FPrime
x3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x3_1 FPrime
t3_1 -- 15.
      t3_2 :: FPrime
t3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t2_0 FPrime
t2_0
      t2_1 :: FPrime
t2_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t2_0 FPrime
t3_2
      z3_2 :: FPrime
z3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
b FPrime
z3_1
      z3_3 :: FPrime
z3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
z3_2 FPrime
t2_1
      z3_4 :: FPrime
z3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
z3_3 FPrime
t0_0 -- 20.
      t3_3 :: FPrime
t3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_4 FPrime
z3_4
      z3_5 :: FPrime
z3_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_4 FPrime
t3_3
      t3_4 :: FPrime
t3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t0_0 FPrime
t0_0
      t0_1 :: FPrime
t0_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t3_4 FPrime
t0_0
      t0_2 :: FPrime
t0_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t0_1 FPrime
t2_1 -- 25.
      t0_3 :: FPrime
t0_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t0_2 FPrime
z3_5
      y3_5 :: FPrime
y3_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y3_4 FPrime
t0_3
      t0_4 :: FPrime
t0_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
y FPrime
z
      t0_5 :: FPrime
t0_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t0_4 FPrime
t0_4
      z3_6 :: FPrime
z3_6 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t0_5 FPrime
z3_5 -- 30.
      x3_3 :: FPrime
x3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
x3_2 FPrime
z3_6
      z3_7 :: FPrime
z3_7 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t0_5 FPrime
t1_0
      z3_8 :: FPrime
z3_8 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_7 FPrime
z3_7
      z3_9 :: FPrime
z3_9 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_8 FPrime
z3_8
  in FPrime -> FPrime -> FPrime -> ECPF FPrime
ECPp FPrime
x3_3 FPrime
y3_5 FPrime
z3_9
-- -}

{-pdouble (ECb l alpha _ p _) p1@(ECPpF2 x1 y1 z1) =
  if isinf l p1
  then p1
  else let a = F2.pow p x1 (2::Integer)
           b = F2.addr p a (F2.mulr p y1 z1)
           c = F2.mulr p x1 z1
           d = F2.pow p c (2::Integer)
           e = F2.addr p (F2.addr p (F2.pow p b (2::Integer)) (F2.mulr p b c)) (if alpha==1 then d else F2.F2 l (zero l))
           x3 = F2.mulr p c e
           y3 = F2.addr p (F2.mulr p (F2.addr p b c) e) (F2.mulr p (F2.pow p a (2::Integer)) c)
           z3 =  F2.mulr p c d
       in ECPpF2 x3 y3 z3 -}
{-# INLINABLE pdouble #-}

-- | add 2 elliptic points
padd :: EC a -> ECPF a -> ECPF a -> ECPF a
padd :: EC a -> ECPF a -> ECPF a -> ECPF a
padd (ECi Int
_ FPrime
b FPrime
p FPrime
_) (ECPp FPrime
x1 FPrime
y1 FPrime
z1) (ECPp FPrime
x2 FPrime
y2 FPrime
z2)
{-
        | FP.eq x1 x2 && FP.eq y1 (FP.neg p y2) && FP.eq z1 z2 = ECPp (FP.fromInteger l 0) (FP.fromInteger l 1) (FP.fromInteger l 0) -- Point at Infinity
        | isinf l p1 = p2
        | isinf l p2 = p1
        | p1==p2 = pdouble curve p1
        | otherwise = 
            let a = FP.subr p (FP.mulr p y2 z1) (FP.mulr p y1 z2)
                b = FP.subr p (FP.mulr p x2 z1) (FP.mulr p x1 z2)
                c = FP.subr p (FP.subr p (FP.mulr p (FP.pow p a (2::Integer)) $ FP.mulr p z1 z2) (FP.pow p b (3::Integer))) (FP.mulr p (FP.fromInteger l 2) $ FP.mulr p (FP.pow p b (2::Integer)) $ FP.mulr p x1 z2)
                x3 = FP.mulr p b c
                y3 = FP.subr p (FP.mulr p a (FP.subr p (FP.mulr p (FP.pow p b (2::Integer)) $ FP.mulr p x1 z2) c)) (FP.mulr p (FP.pow p b (3::Integer)) $ FP.mulr p y1 z2)
                z3 = FP.mulr p (FP.pow p b (3::Integer)) $ FP.mulr p z1 z2
            in ECPp x3 y3 y3
-- -}
-- {-
  -- 1060.pdf Alg 4.
  -- TODO: nisttv
  = let t0_0 :: FPrime
t0_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x1 FPrime
x2
        t1_0 :: FPrime
t1_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
y1 FPrime
y2
        t2_0 :: FPrime
t2_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
z1 FPrime
z2
        t3_0 :: FPrime
t3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x1 FPrime
y1
        t4_0 :: FPrime
t4_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x2 FPrime
y2 -- 5.
        t3_1 :: FPrime
t3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t3_0 FPrime
t4_0
        t4_1 :: FPrime
t4_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t0_0 FPrime
t1_0
        t3_2 :: FPrime
t3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t3_1 FPrime
t4_1
        t4_2 :: FPrime
t4_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y1 FPrime
z1
        x3_0 :: FPrime
x3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y2 FPrime
z2 -- 10.
        t4_3 :: FPrime
t4_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t4_2 FPrime
x3_0
        x3_1 :: FPrime
x3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_0 FPrime
t2_0
        t4_4 :: FPrime
t4_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t4_3 FPrime
x3_1
        x3_2 :: FPrime
x3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x1 FPrime
z1
        y3_0 :: FPrime
y3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x2 FPrime
z2 -- 15.
        x3_3 :: FPrime
x3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x3_2 FPrime
y3_0
        y3_1 :: FPrime
y3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t0_0 FPrime
t2_0
        y3_2 :: FPrime
y3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
x3_3 FPrime
y3_1
        z3_0 :: FPrime
z3_0 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
b FPrime
t2_0
        x3_4 :: FPrime
x3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
y3_2 FPrime
z3_0 -- 20.
        z3_1 :: FPrime
z3_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x3_4 FPrime
x3_4
        x3_5 :: FPrime
x3_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
x3_4 FPrime
z3_1
        z3_2 :: FPrime
z3_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t1_0 FPrime
x3_5
        x3_6 :: FPrime
x3_6 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_0 FPrime
x3_5
        y3_3 :: FPrime
y3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
b FPrime
y3_2 -- 25.
        t1_1 :: FPrime
t1_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t2_0 FPrime
t2_0
        t2_1 :: FPrime
t2_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_1 FPrime
t2_0
        y3_4 :: FPrime
y3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
y3_3 FPrime
t2_1
        y3_5 :: FPrime
y3_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
y3_4 FPrime
t0_0
        t1_2 :: FPrime
t1_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y3_5 FPrime
y3_5 -- 30.
        y3_6 :: FPrime
y3_6 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_2 FPrime
y3_5
        t1_3 :: FPrime
t1_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t0_0 FPrime
t0_0
        t0_1 :: FPrime
t0_1 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
t1_3 FPrime
t0_0
        t0_2 :: FPrime
t0_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
t0_1 FPrime
t2_1
        t1_4 :: FPrime
t1_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t4_4 FPrime
y3_6 -- 35.
        t2_2 :: FPrime
t2_2 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t0_2 FPrime
y3_6
        y3_7 :: FPrime
y3_7 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
x3_6 FPrime
z3_2
        y3_8 :: FPrime
y3_8 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
y3_7 FPrime
t2_2
        x3_7 :: FPrime
x3_7 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t3_2 FPrime
x3_6
        x3_8 :: FPrime
x3_8 = FPrime -> FPrime -> FPrime -> FPrime
FP.subr FPrime
p FPrime
x3_7 FPrime
t1_4 -- 40.
        z3_3 :: FPrime
z3_3 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t4_4 FPrime
z3_2
        t1_5 :: FPrime
t1_5 = FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
t3_2 FPrime
t0_2
        z3_4 :: FPrime
z3_4 = FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p FPrime
z3_3 FPrime
t1_5
    in FPrime -> FPrime -> FPrime -> ECPF FPrime
ECPp FPrime
x3_8 FPrime
y3_8 FPrime
z3_4
-- -}
{-padd curve@(ECb l alpha _ p _) p1@(ECPpF2 x1 y1 z1) p2@(ECPpF2 x2 y2 z2)
        | F2.eq x1 x2 && F2.eq y1 (F2.addr p x2 y2) && F2.eq z1 z2 = ECPpF2 (F2.F2 l (zero l)) (F2.F2 l (one l)) (F2.F2 l (zero l))  -- Point at Infinity
        | isinf l p1 = p2
        | isinf l p2 = p1
        | p1==p2 = pdouble curve p1
        | otherwise = 
            let a = F2.addr p (F2.mulr p y1 z2) (F2.mulr p z1 y2)
                b = F2.addr p (F2.mulr p x1 z2) (F2.mulr p z1 x2)
                c = F2.pow p b (2::Integer)
                d = F2.mulr p z1 z2
                e = F2.addr p
                    (F2.mulr p
                     (F2.addr p
                      (F2.addr p
                       (F2.pow p a (2::Integer))
                       (F2.mulr p a b)
                      )
                      (F2.mulr p (if alpha==1 then c else F2.F2 l (zero l)) c)
                     )
                     d
                    )
                    (F2.mulr p b c)
                x3 = F2.mulr p b e
                y3 = F2.addr p
                     (F2.mulr p
                      (F2.mulr p
                       c
                       (F2.addr p
                        (F2.mulr p a x1)
                        (F2.mulr p y1 b))
                      )
                      z2
                     )
                     (F2.mulr p (F2.addr p a b) e)
                z3 = F2.mulr p (F2.pow p b (3::Integer)) d
            in ECPpF2 x3 y3 z3
-}
{-# INLINABLE padd #-}

-- | "generic" verify, if generic ECP is on EC via getxA and getyA
ison :: EC a -> ECPF a -> Bool
ison :: EC a -> ECPF a -> Bool
ison (ECi Int
l FPrime
beta FPrime
p FPrime
_) (ECPp FPrime
x FPrime
y FPrime
z) = FPrime -> FPrime -> Bool
FP.eq
    (FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p (FPrime -> FPrime -> FPrime -> FPrime
FP.pow FPrime
p FPrime
y (FPrime
2::Integer)) FPrime
z)
    (FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p (FPrime -> FPrime -> FPrime -> FPrime
FP.pow FPrime
p FPrime
x (FPrime
3::Integer)) (FPrime -> FPrime -> FPrime -> FPrime
FP.addr FPrime
p (FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p (FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p (FPrime -> FPrime -> FPrime
FP.neg FPrime
p (Int -> FPrime -> FPrime
FP.fromInteger Int
l FPrime
3)) FPrime
x) (FPrime -> FPrime -> FPrime -> FPrime
FP.pow FPrime
p FPrime
z (FPrime
2::Integer))) (FPrime -> FPrime -> FPrime -> FPrime
FP.mulr FPrime
p FPrime
beta (FPrime -> FPrime -> FPrime -> FPrime
FP.pow FPrime
p FPrime
z (FPrime
3::Integer)))))
{-ison (ECb l alpha beta p _) a@(ECPpF2 x y z)
  | isinf l a = True
  | otherwise =
    F2.eq
    (F2.addr p
     (F2.mulr p (F2.pow p y (2::Integer)) z)
     (F2.mulr p (F2.mulr p x y) z)
    )
    (F2.addr p
     (F2.addr p
      (F2.pow p x (3::Integer))
      (if alpha==1 then F2.mulr p (F2.pow p x (2::Integer)) z else F2.F2 l (zero l))
     )
     (F2.mulr p beta (F2.pow p z (3::Integer)))
    ) -}
{-# INLINABLE ison #-}

-- | Point Multiplication.
pmul :: EC a -> ECPF a -> FP.FPrime -> ECPF a
-- {-
pmul :: EC a -> ECPF a -> FPrime -> ECPF a
pmul curve :: EC a
curve@(ECi Int
l FPrime
_ FPrime
p FPrime
_) (ECPp FPrime
x FPrime
y FPrime
z)  FPrime
k =
  let alleeins :: FPrime
alleeins = Int -> FPrime -> FPrime
FP.fromInteger Int
l (FPrime
2FPrime -> Int -> FPrime
forall a b. (Num a, Integral b) => a -> b -> a
^Int
lFPrime -> FPrime -> FPrime
forall a. Num a => a -> a -> a
-FPrime
1)
      eins :: FPrime
eins = Int -> FPrime -> FPrime
FP.fromInteger Int
l FPrime
1
      k' :: FPrime
k' = FPrime
k FPrime -> FPrime -> FPrime
forall a. Integral a => a -> a -> a
`mod` (FPrime
pFPrime -> FPrime -> FPrime
forall a. Num a => a -> a -> a
+FPrime
1)
      ex :: ECPF a -> Int -> ECPF a
ex ECPF a
erg Int
j
        | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = ECPF a
erg
        | Bool
otherwise = let s :: FPrime
s = FPrime -> Int -> FPrime
FP.condBit FPrime
k' Int
j
                          realpattern :: FPrime
realpattern = FPrime -> FPrime -> FPrime
FP.mul FPrime
alleeins FPrime
s
                          invpattern :: FPrime
invpattern = FPrime -> FPrime -> FPrime
FP.mul FPrime
alleeins (FPrime -> FPrime -> FPrime
FP.sub FPrime
eins FPrime
s)
                          x' :: FPrime
x' = FPrime
x FPrime -> FPrime -> FPrime
forall a. Bits a => a -> a -> a
B..&. FPrime
realpattern
                          y' :: FPrime
y' = FPrime -> FPrime -> FPrime
FP.add (FPrime
y FPrime -> FPrime -> FPrime
forall a. Bits a => a -> a -> a
B..&. FPrime
realpattern) (FPrime
eins FPrime -> FPrime -> FPrime
forall a. Bits a => a -> a -> a
B..&. FPrime
invpattern)
                          z' :: FPrime
z' = (FPrime
z FPrime -> FPrime -> FPrime
forall a. Bits a => a -> a -> a
B..&. FPrime
realpattern)
                      in ECPF a -> Int -> ECPF a
ex (EC a -> ECPF a -> ECPF a -> ECPF a
forall a. EC a -> ECPF a -> ECPF a -> ECPF a
padd EC a
curve (EC a -> ECPF a -> ECPF a
forall a. EC a -> ECPF a -> ECPF a
pdouble EC a
curve ECPF a
erg) (FPrime -> FPrime -> FPrime -> ECPF FPrime
ECPp FPrime
x' FPrime
y' FPrime
z')) (Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  in ECPF a -> Int -> ECPF a
ex (FPrime -> FPrime -> FPrime -> ECPF FPrime
ECPp FPrime
0 FPrime
1 FPrime
0) (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
-- -}
{-
pmul curve@(ECi l _ p _) b@ECPp{} k'  =
-- {- 
  let k = FP.redc (FP.subr p p (FP.fromInteger l 1)) k'
      ex p1 p2 i
        | i < 0 = p1
        | not (FP.testBit k i) = ex (pdouble curve p1) (padd curve p1 p2) (i - 1)
        | otherwise           = ex (padd curve p1 p2) (pdouble curve p2) (i - 1)
  in ex b (pdouble curve b) (log2len k - 2)
-- -}
-- -}
{-
  -- basic double and add, for comparison, demo of attacks
  let k = FP.redc (FP.subr p p (FP.fromInteger l 1)) k'
      ex p2 i
        | i < 0 = b
        | not (FP.testBit k i) = ex (pdouble curve p2) (i - 1)
        | otherwise           = ex (pdouble curve (padd curve b p2)) (i - 1)
  in ex (pdouble curve b) (log2len k - 2)
-- -}
{-pmul curve@(ECb l _ _ p _) b@ECPpF2{} k'  =
  let p' = (FP.fromInteger l $ F2.toInteger p)
      k = FP.redc (FP.subr p' p' (FP.fromInteger l 1)) k'
      ex p1 p2 i
        | i < 0 = p1
        | not (FP.testBit k i) = ex  (pdouble curve p1) (padd curve p1 p2) (i - 1)
        | otherwise           = ex (padd curve p1 p2) (pdouble curve p2) (i - 1)
  in ex b (pdouble curve b) (log2len k - 2) -}
{-
-- these rely on point addition/doubling to be branching free!
pmul curve@(ECi l _ p _) b@ECPp{} k'
  | k' == 0 = ECPp (FP.fromInteger l 0) (FP.fromInteger l 1) (FP.fromInteger l 0)
  | k' == 1 = b
  | otherwise =
    let k = FP.redc (FP.subr p p (FP.fromInteger l 1)) k'
        ex pt i
          | i < 0 = pt
          | otherwise = let cond = B.shift k (-i) `mod` 2
                        in ex (padd curve (pmul curve b cond) (pdouble curve pt)) (i - 1) -- cond == 1 -> b, cond == 0 -> inf (add neutral)
    in ex b (log2len k - 2) -- begin one after highest bit (always set for i > 0), loglen returns highest bit position +1
pmul curve@(ECb l _ _ p _) b@ECPpF2{} k'
  | k' == 0 = ECPpF2 (F2.fromInteger l 0) (F2.fromInteger l 1) (F2.fromInteger l 0)
  | k' == 1 = b
  | otherwise =
    let p' = (FP.fromInteger l $ F2.toInteger p)
        k = FP.redc (FP.subr p' p' (FP.fromInteger l 1)) k'
        ex pt i
          | i < 0 = pt
          | otherwise = let cond = B.shift k (-i) `mod` 2
                        in ex (padd curve (pmul curve pt cond) (pdouble curve pt)) (i - 1)
    in ex b (log2len k - 2)
-- -}
{-# INLINABLE pmul #-}