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

module ZkFold.Base.Protocol.Plonk (
    Plonk (..)
) where

import           Data.Binary                                         (Binary)
import           Data.Functor.Classes                                (Show1)
import           Data.Functor.Rep                                    (Rep)
import           Data.Kind                                           (Type)
import           Data.Word                                           (Word8)
import           Prelude                                             hiding (Num (..), div, drop, length, replicate,
                                                                      sum, take, (!!), (/), (^))
import qualified Prelude                                             as P hiding (length)
import           Test.QuickCheck                                     (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Data.Vector                             (Vector)
import           ZkFold.Base.Protocol.NonInteractiveProof
import           ZkFold.Base.Protocol.Plonk.Prover                   (plonkProve)
import           ZkFold.Base.Protocol.Plonk.Verifier                 (plonkVerify)
import           ZkFold.Base.Protocol.Plonkup.Input
import           ZkFold.Base.Protocol.Plonkup.Internal
import           ZkFold.Base.Protocol.Plonkup.Proof
import           ZkFold.Base.Protocol.Plonkup.Prover
import           ZkFold.Base.Protocol.Plonkup.Verifier
import           ZkFold.Base.Protocol.Plonkup.Witness
import           ZkFold.Symbolic.Compiler                            (desugarRanges)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal


{-| Based on the paper https://eprint.iacr.org/2019/953.pdf -}

data Plonk p i (n :: Natural) l g1 g2 transcript = Plonk {
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
omega :: ScalarFieldOf g1,
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k1    :: ScalarFieldOf g1,
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k2    :: ScalarFieldOf g1,
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
ac    :: ArithmeticCircuit (ScalarFieldOf g1) p i l,
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> g2
h1    :: g2,
        forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> Vector (n + 5) g1
gs'   :: Vector (n + 5) g1
    }

fromPlonkup ::
    ( Arithmetic (ScalarFieldOf g1)
    , Binary (ScalarFieldOf g1)
    , Binary (Rep p)
    , Binary (Rep i)
    , Ord (Rep i)
    ) => Plonkup p i n l g1 g2 ts -> Plonk p i n l g1 g2 ts
fromPlonkup :: forall {k} g1 (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) g2 (ts :: k).
(Arithmetic (ScalarFieldOf g1), Binary (ScalarFieldOf g1),
 Binary (Rep p), Binary (Rep i), Ord (Rep i)) =>
Plonkup p i n l g1 g2 ts -> Plonk p i n l g1 g2 ts
fromPlonkup Plonkup {g2
Vector (n + 5) g1
ArithmeticCircuit (ScalarFieldOf g1) p i l
ScalarFieldOf g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
ac :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> g2
gs' :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> Vector (n + 5) g1
..} = Plonk { ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
ac = ArithmeticCircuit (ScalarFieldOf g1) p i l
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i),
 Ord (Rep i)) =>
ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o
desugarRanges ArithmeticCircuit (ScalarFieldOf g1) p i l
ac, g2
Vector (n + 5) g1
ScalarFieldOf g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
gs' :: Vector (n + 5) g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
gs' :: Vector (n + 5) g1
..}

toPlonkup :: Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
toPlonkup :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (ts :: k).
Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
toPlonkup Plonk {g2
Vector (n + 5) g1
ArithmeticCircuit (ScalarFieldOf g1) p i l
ScalarFieldOf g1
omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
ac :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> g2
gs' :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> Vector (n + 5) g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
..} = Plonkup {g2
Vector (n + 5) g1
ArithmeticCircuit (ScalarFieldOf g1) p i l
ScalarFieldOf g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
..}

instance (Show1 l, Show (Rep i), Show (ScalarFieldOf g1), Ord (Rep i), Show g1, Show g2) => Show (Plonk p i n l g1 g2 t) where
    show :: Plonk p i n l g1 g2 t -> String
show Plonk {g2
Vector (n + 5) g1
ArithmeticCircuit (ScalarFieldOf g1) p i l
ScalarFieldOf g1
omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> ScalarFieldOf g1
ac :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> g2
gs' :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonk p i n l g1 g2 transcript -> Vector (n + 5) g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
..} =
        String
"Plonk: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
omega String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ l (Var (ScalarFieldOf g1) i) -> String
forall a. Show a => a -> String
show (ArithmeticCircuit (ScalarFieldOf g1) p i l
-> l (Var (ScalarFieldOf g1) i)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput ArithmeticCircuit (ScalarFieldOf g1) p i l
ac) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArithmeticCircuit (ScalarFieldOf g1) p i l -> String
forall a. Show a => a -> String
show ArithmeticCircuit (ScalarFieldOf g1) p i l
ac String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ g2 -> String
forall a. Show a => a -> String
show g2
h1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Vector (n + 5) g1 -> String
forall a. Show a => a -> String
show Vector (n + 5) g1
gs'

instance ( Arithmetic (ScalarFieldOf g1), Binary (ScalarFieldOf g1)
         , Binary (Rep p), Binary (Rep i), Ord (Rep i)
         , Arbitrary (Plonkup p i n l g1 g2 t))
        => Arbitrary (Plonk p i n l g1 g2 t) where
    arbitrary :: Gen (Plonk p i n l g1 g2 t)
arbitrary = Plonkup p i n l g1 g2 t -> Plonk p i n l g1 g2 t
forall {k} g1 (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) g2 (ts :: k).
(Arithmetic (ScalarFieldOf g1), Binary (ScalarFieldOf g1),
 Binary (Rep p), Binary (Rep i), Ord (Rep i)) =>
Plonkup p i n l g1 g2 ts -> Plonk p i n l g1 g2 ts
fromPlonkup (Plonkup p i n l g1 g2 t -> Plonk p i n l g1 g2 t)
-> Gen (Plonkup p i n l g1 g2 t) -> Gen (Plonk p i n l g1 g2 t)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Plonkup p i n l g1 g2 t)
forall a. Arbitrary a => Gen a
arbitrary

instance forall p i n l g1 g2 gt (ts :: Type) core .
        ( NonInteractiveProof (Plonkup p i n l g1 g2 ts) core
        , SetupProve (Plonkup p i n l g1 g2 ts) ~ PlonkupProverSetup p i n l g1 g2
        , SetupVerify (Plonkup p i n l g1 g2 ts) ~ PlonkupVerifierSetup p i n l g1 g2
        , Witness (Plonkup p i n l g1 g2 ts) ~ (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
        , Input (Plonkup p i n l g1 g2 ts) ~ PlonkupInput l g1
        , Proof (Plonkup p i n l g1 g2 ts) ~ PlonkupProof g1
        , KnownNat n
        , Foldable l
        , Compressible g1
        , Pairing g1 g2 gt
        , Eq gt
        , Arithmetic (ScalarFieldOf g1)
        , ToTranscript ts Word8
        , ToTranscript ts (ScalarFieldOf g1)
        , ToTranscript ts (Compressed g1)
        , FromTranscript ts (ScalarFieldOf g1)
        , CoreFunction g1 core
        ) => NonInteractiveProof (Plonk p i n l g1 g2 ts) core where
    type Transcript (Plonk p i n l g1 g2 ts)  = ts
    type SetupProve (Plonk p i n l g1 g2 ts)  = PlonkupProverSetup p i n l g1 g2
    type SetupVerify (Plonk p i n l g1 g2 ts) = PlonkupVerifierSetup p i n l g1 g2
    type Witness (Plonk p i n l g1 g2 ts)     = (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
    type Input (Plonk p i n l g1 g2 ts)       = PlonkupInput l g1
    type Proof (Plonk p i n l g1 g2 ts)       = PlonkupProof g1

    setupProve :: Plonk p i n l g1 g2 ts -> SetupProve (Plonk p i n l g1 g2 ts)
    setupProve :: Plonk p i n l g1 g2 ts -> SetupProve (Plonk p i n l g1 g2 ts)
setupProve = forall a (core :: k).
NonInteractiveProof a core =>
a -> SetupProve a
forall {k} a (core :: k).
NonInteractiveProof a core =>
a -> SetupProve a
setupProve @(Plonkup p i n l g1 g2 ts) @core (Plonkup p i n l g1 g2 ts -> PlonkupProverSetup p i n l g1 g2)
-> (Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts)
-> Plonk p i n l g1 g2 ts
-> PlonkupProverSetup p i n l g1 g2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (ts :: k).
Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
toPlonkup

    setupVerify :: Plonk p i n l g1 g2 ts -> SetupVerify (Plonk p i n l g1 g2 ts)
    setupVerify :: Plonk p i n l g1 g2 ts -> SetupVerify (Plonk p i n l g1 g2 ts)
setupVerify = forall a (core :: k).
NonInteractiveProof a core =>
a -> SetupVerify a
forall {k} a (core :: k).
NonInteractiveProof a core =>
a -> SetupVerify a
setupVerify @(Plonkup p i n l g1 g2 ts) @core (Plonkup p i n l g1 g2 ts -> PlonkupVerifierSetup p i n l g1 g2)
-> (Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts)
-> Plonk p i n l g1 g2 ts
-> PlonkupVerifierSetup p i n l g1 g2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (ts :: k).
Plonk p i n l g1 g2 ts -> Plonkup p i n l g1 g2 ts
toPlonkup

    prove :: SetupProve (Plonk p i n l g1 g2 ts) -> Witness (Plonk p i n l g1 g2 ts) -> (Input (Plonk p i n l g1 g2 ts), Proof (Plonk p i n l g1 g2 ts))
    prove :: SetupProve (Plonk p i n l g1 g2 ts)
-> Witness (Plonk p i n l g1 g2 ts)
-> (Input (Plonk p i n l g1 g2 ts), Proof (Plonk p i n l g1 g2 ts))
prove SetupProve (Plonk p i n l g1 g2 ts)
setup Witness (Plonk p i n l g1 g2 ts)
witness =
        let (PlonkupInput l g1
input, PlonkupProof g1
proof, PlonkupProverTestInfo n g1
_) = forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) g1 (g2 :: k1) ts (core :: k2).
(KnownNat n, Foldable l, Ord (ScalarFieldOf g1), Compressible g1,
 ToTranscript ts Word8, ToTranscript ts (ScalarFieldOf g1),
 ToTranscript ts (Compressed g1),
 FromTranscript ts (ScalarFieldOf g1), CoreFunction g1 core) =>
PlonkupProverSetup p i n l g1 g2
-> (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
-> (PlonkupInput l g1, PlonkupProof g1, PlonkupProverTestInfo n g1)
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 ts (core :: k).
(KnownNat n, Foldable l, Ord (ScalarFieldOf g1), Compressible g1,
 ToTranscript ts Word8, ToTranscript ts (ScalarFieldOf g1),
 ToTranscript ts (Compressed g1),
 FromTranscript ts (ScalarFieldOf g1), CoreFunction g1 core) =>
PlonkupProverSetup p i n l g1 g2
-> (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
-> (PlonkupInput l g1, PlonkupProof g1, PlonkupProverTestInfo n g1)
plonkProve @p @i @n @l @g1 @g2 @ts @core PlonkupProverSetup p i n l g1 g2
SetupProve (Plonk p i n l g1 g2 ts)
setup (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
Witness (Plonk p i n l g1 g2 ts)
witness
        in (PlonkupInput l g1
Input (Plonk p i n l g1 g2 ts)
input, PlonkupProof g1
Proof (Plonk p i n l g1 g2 ts)
proof)

    verify :: SetupVerify (Plonk p i n l g1 g2 ts) -> Input (Plonk p i n l g1 g2 ts) -> Proof (Plonk p i n l g1 g2 ts) -> Bool
    verify :: SetupVerify (Plonk p i n l g1 g2 ts)
-> Input (Plonk p i n l g1 g2 ts)
-> Proof (Plonk p i n l g1 g2 ts)
-> Bool
verify = forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 gt ts.
(KnownNat n, Foldable l, Pairing g1 g2 gt, Compressible g1,
 Eq (ScalarFieldOf g1), Eq gt, ToTranscript ts Word8,
 ToTranscript ts (ScalarFieldOf g1),
 ToTranscript ts (Compressed g1),
 FromTranscript ts (ScalarFieldOf g1)) =>
PlonkupVerifierSetup p i n l g1 g2
-> PlonkupInput l g1 -> PlonkupProof g1 -> Bool
plonkVerify @p @i @n @l @g1 @g2 @gt @ts