{-# LANGUAGE RebindableSyntax     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Symbolic.Data.Secp256k1 (Secp256k1_Point) where

import           Prelude                                     (fromInteger, type (~), ($))
import qualified Prelude                                     as P

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.EllipticCurve.Secp256k1 (Secp256k1_Base, Secp256k1_PointOf)
import           ZkFold.Symbolic.Class                       (Symbolic (..))
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.ByteString
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.FFA
import           ZkFold.Symbolic.Data.FieldElement

type Secp256k1_Point ctx = Secp256k1_PointOf (Bool ctx) (FFA Secp256k1_Base ctx)

instance Symbolic ctx => CyclicGroup (Secp256k1_Point ctx) where
  type ScalarFieldOf (Secp256k1_Point ctx) = FieldElement ctx
  pointGen :: Secp256k1_Point ctx
pointGen = FFA Secp256k1_Base ctx
-> FFA Secp256k1_Base ctx -> Secp256k1_Point ctx
forall field point. Planar field point => field -> field -> point
pointXY
    (Natural -> FFA Secp256k1_Base ctx
forall a b. FromConstant a b => a -> b
fromConstant (Natural
0x79BE667EF9DCBBAC55A06295CE870B07029BFCDB2DCE28D959F2815B16F81798 :: Natural))
    (Natural -> FFA Secp256k1_Base ctx
forall a b. FromConstant a b => a -> b
fromConstant (Natural
0x483ADA7726A3C4655DA4FBFC0E1108A8FD17B448A68554199C47D08FFB10D4B8 :: Natural))

instance
  ( Symbolic ctx
  , a ~ BaseField ctx
  , bits ~ NumberOfBits a
  ) => Scale (FieldElement ctx) (Secp256k1_Point ctx) where

    scale :: FieldElement ctx -> Secp256k1_Point ctx -> Secp256k1_Point ctx
scale FieldElement ctx
sc Secp256k1_Point ctx
x = [Secp256k1_Point ctx] -> Secp256k1_Point ctx
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([Secp256k1_Point ctx] -> Secp256k1_Point ctx)
-> [Secp256k1_Point ctx] -> Secp256k1_Point ctx
forall a b. (a -> b) -> a -> b
$ (Natural -> Secp256k1_Point ctx -> Secp256k1_Point ctx)
-> [Natural] -> [Secp256k1_Point ctx] -> [Secp256k1_Point ctx]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
P.zipWith (\Natural
b Secp256k1_Point ctx
p -> forall b a. Conditional b a => a -> a -> b -> a
bool @(Bool ctx) Secp256k1_Point ctx
forall a. AdditiveMonoid a => a
zero Secp256k1_Point ctx
p (ByteString bits ctx -> Natural -> Bool ctx
forall (c :: (Type -> Type) -> Type) (n :: Natural).
Symbolic c =>
ByteString n c -> Natural -> Bool c
isSet ByteString bits ctx
bits Natural
b)) [Natural
upper, Natural
upper Natural -> Natural -> Natural
-! Natural
1 .. Natural
0] ((Secp256k1_Point ctx -> Secp256k1_Point ctx)
-> Secp256k1_Point ctx -> [Secp256k1_Point ctx]
forall a. (a -> a) -> a -> [a]
P.iterate (\Secp256k1_Point ctx
e -> Secp256k1_Point ctx
e Secp256k1_Point ctx -> Secp256k1_Point ctx -> Secp256k1_Point ctx
forall a. AdditiveSemigroup a => a -> a -> a
+ Secp256k1_Point ctx
e) Secp256k1_Point ctx
x)
        where
            bits :: ByteString bits ctx
            bits :: ByteString bits ctx
bits = ctx (Vector bits) -> ByteString bits ctx
forall (n :: Natural) (context :: (Type -> Type) -> Type).
context (Vector n) -> ByteString n context
ByteString (ctx (Vector bits) -> ByteString bits ctx)
-> ctx (Vector bits) -> ByteString bits ctx
forall a b. (a -> b) -> a -> b
$ FieldElement ctx -> Bits (FieldElement ctx)
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion FieldElement ctx
sc

            upper :: Natural
            upper :: Natural
upper = forall (n :: Natural). KnownNat n => Natural
value @bits Natural -> Natural -> Natural
-! Natural
1