{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RebindableSyntax    #-}
{-# LANGUAGE TypeOperators       #-}
module ZkFold.Symbolic.Algorithms.ECDSA.ECDSA where
import           Data.Type.Equality
import           GHC.Base                                (($))
import           GHC.TypeLits                            (KnownNat, Log2)
import qualified GHC.TypeNats

import           ZkFold.Base.Algebra.Basic.Class         hiding (Euclidean (..))
import           ZkFold.Base.Algebra.Basic.Number        (value)
import           ZkFold.Base.Algebra.EllipticCurve.Class
import qualified ZkFold.Symbolic.Class                   as S
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.ByteString         (ByteString)
import           ZkFold.Symbolic.Data.Combinators        (Iso (..), NumberOfRegisters, RegisterSize (Auto))
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.FieldElement       (FieldElement)
import           ZkFold.Symbolic.Data.UInt               (UInt, eea)

ecdsaVerify
  :: forall point n c curve baseField.
     ( S.Symbolic c
     , KnownNat n
     , baseField ~ UInt 256 'Auto c
     , ScalarFieldOf point ~ FieldElement c
     , point ~ Weierstrass curve (Point baseField)
     , CyclicGroup point
     , SemiEuclidean (UInt 256 'Auto c)
     , KnownNat (NumberOfRegisters (S.BaseField c) 256 'Auto)
     , Log2 (Order (S.BaseField c) GHC.TypeNats.- 1) ~ 255
     )
  => point
  -> ByteString 256 c
  -> (UInt 256 'Auto c, UInt 256 'Auto c)
  -> Bool c
ecdsaVerify :: forall {k} point (n :: Nat) (c :: (Type -> Type) -> Type)
       (curve :: k) baseField.
(Symbolic c, KnownNat n, baseField ~ UInt 256 'Auto c,
 ScalarFieldOf point ~ FieldElement c,
 point ~ Weierstrass curve (Point baseField), CyclicGroup point,
 SemiEuclidean (UInt 256 'Auto c),
 KnownNat (NumberOfRegisters (BaseField c) 256 'Auto),
 Log2 (Order (BaseField c) - 1) ~ 255) =>
point
-> ByteString 256 c
-> (UInt 256 'Auto c, UInt 256 'Auto c)
-> Bool c
ecdsaVerify point
publicKey ByteString 256 c
message (UInt 256 'Auto c
r, UInt 256 'Auto c
s) =
    case point
c of Weierstrass (Point UInt 256 'Auto c
x UInt 256 'Auto c
_ BooleanOf (UInt 256 'Auto c)
isInf) -> if Bool c
BooleanOf (UInt 256 'Auto c)
isInf then Bool c
forall b. BoolType b => b
false else UInt 256 'Auto c
r UInt 256 'Auto c
-> UInt 256 'Auto c -> BooleanOf (UInt 256 'Auto c)
forall a. Eq a => a -> a -> BooleanOf a
== (UInt 256 'Auto c
x UInt 256 'Auto c -> UInt 256 'Auto c -> UInt 256 'Auto c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt 256 'Auto c
n)
    where
        n :: UInt 256 'Auto c
n = Nat -> UInt 256 'Auto c
forall a b. FromConstant a b => a -> b
fromConstant (Nat -> UInt 256 'Auto c) -> Nat -> UInt 256 'Auto c
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @n

        g :: point
g = forall g. CyclicGroup g => g
pointGen @point

        (UInt 256 'Auto c
sInv, UInt 256 'Auto c
_, UInt 256 'Auto c
_) = UInt 256 'Auto c
-> UInt 256 'Auto c
-> (UInt 256 'Auto c, UInt 256 'Auto c, UInt 256 'Auto c)
forall (n :: Nat) (c :: (Type -> Type) -> Type)
       (r :: RegisterSize).
(Symbolic c, SemiEuclidean (UInt n r c), KnownNat n,
 KnownRegisters c n r, AdditiveGroup (UInt n r c)) =>
UInt n r c -> UInt n r c -> (UInt n r c, UInt n r c, UInt n r c)
eea UInt 256 'Auto c
s UInt 256 'Auto c
n

        u :: UInt 256 'Auto c
u = (ByteString 256 c -> UInt 256 'Auto c
forall a b. Iso a b => a -> b
from ByteString 256 c
message UInt 256 'Auto c -> UInt 256 'Auto c -> UInt 256 'Auto c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt 256 'Auto c
sInv) UInt 256 'Auto c -> UInt 256 'Auto c -> UInt 256 'Auto c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt 256 'Auto c
n

        v :: UInt 256 'Auto c
v = UInt 256 'Auto c
r UInt 256 'Auto c -> UInt 256 'Auto c -> UInt 256 'Auto c
forall a. MultiplicativeSemigroup a => a -> a -> a
* UInt 256 'Auto c
sInv UInt 256 'Auto c -> UInt 256 'Auto c -> UInt 256 'Auto c
forall a. SemiEuclidean a => a -> a -> a
`mod` UInt 256 'Auto c
n

        c :: point
c = (UInt 256 'Auto c -> FieldElement c
forall a b. Iso a b => a -> b
from UInt 256 'Auto c
u :: FieldElement c) FieldElement c -> point -> point
forall b a. Scale b a => b -> a -> a
`scale` point
g point -> point -> point
forall a. AdditiveSemigroup a => a -> a -> a
+ (UInt 256 'Auto c -> FieldElement c
forall a b. Iso a b => a -> b
from UInt 256 'Auto c
v :: FieldElement c) FieldElement c -> point -> point
forall b a. Scale b a => b -> a -> a
`scale` point
publicKey