{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Protocol.Plonkup (
    module ZkFold.Base.Protocol.Plonkup.Internal,
    Plonkup (..)
) where

import           Data.Binary                                         (Binary)
import           Data.Functor.Rep                                    (Rep, Representable)
import           Data.Word                                           (Word8)
import           Prelude                                             hiding (Num (..), div, drop, length, replicate,
                                                                      sum, take, (!!), (/), (^))
import qualified Prelude                                             as P hiding (length)

import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class             (Compressible (..), CyclicGroup (..), Pairing (..))
import           ZkFold.Base.Protocol.NonInteractiveProof
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.Setup
import           ZkFold.Base.Protocol.Plonkup.Verifier
import           ZkFold.Base.Protocol.Plonkup.Witness
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

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

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

    setupProve :: Plonkup p i n l g1 g2 ts -> SetupProve (Plonkup p i n l g1 g2 ts)
    setupProve :: Plonkup p i n l g1 g2 ts -> SetupProve (Plonkup p i n l g1 g2 ts)
setupProve Plonkup p i n l g1 g2 ts
plonk =
        let PlonkupSetup {g2
Vector g1
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
PlonkupCircuitPolynomials n g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
h0 :: g2
h1 :: g2
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: PlonkupCircuitPolynomials n g1
commitments :: PlonkupCircuitCommitments g1
omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
gs :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> Vector g1
h0 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1
commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1
..} = forall {k1} {k2} (i :: Type -> Type) (p :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt (ts :: k1) (core :: k2).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1),
 Binary (ScalarFieldOf g2), Pairing g1 g2 gt,
 CoreFunction g1 core) =>
Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
forall (i :: Type -> Type) (p :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt ts (core :: k).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1),
 Binary (ScalarFieldOf g2), Pairing g1 g2 gt,
 CoreFunction g1 core) =>
Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
plonkupSetup @i @p @n @l @g1 @g2 @gt @ts @core Plonkup p i n l g1 g2 ts
plonk
        in PlonkupProverSetup {Vector g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
PlonkupCircuitPolynomials n g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: PlonkupCircuitPolynomials n g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: PlonkupCircuitPolynomials n g1
..}

    setupVerify :: Plonkup p i n l g1 g2 ts -> SetupVerify (Plonkup p i n l g1 g2 ts)
    setupVerify :: Plonkup p i n l g1 g2 ts -> SetupVerify (Plonkup p i n l g1 g2 ts)
setupVerify Plonkup p i n l g1 g2 ts
plonk =
        let PlonkupSetup {g2
Vector g1
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
PlonkupCircuitPolynomials n g1
omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
gs :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> Vector g1
h0 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1
commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
h0 :: g2
h1 :: g2
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: PlonkupCircuitPolynomials n g1
commitments :: PlonkupCircuitCommitments g1
..} = forall {k1} {k2} (i :: Type -> Type) (p :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt (ts :: k1) (core :: k2).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1),
 Binary (ScalarFieldOf g2), Pairing g1 g2 gt,
 CoreFunction g1 core) =>
Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
forall (i :: Type -> Type) (p :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt ts (core :: k).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1),
 Binary (ScalarFieldOf g2), Pairing g1 g2 gt,
 CoreFunction g1 core) =>
Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
plonkupSetup @i @p @n @l @g1 @g2 @gt @ts @core Plonkup p i n l g1 g2 ts
plonk
        in PlonkupVerifierSetup {g2
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
commitments :: PlonkupCircuitCommitments g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
commitments :: PlonkupCircuitCommitments g1
..}

    prove :: SetupProve (Plonkup p i n l g1 g2 ts) -> Witness (Plonkup p i n l g1 g2 ts) -> (Input (Plonkup p i n l g1 g2 ts), Proof (Plonkup p i n l g1 g2 ts))
    prove :: SetupProve (Plonkup p i n l g1 g2 ts)
-> Witness (Plonkup p i n l g1 g2 ts)
-> (Input (Plonkup p i n l g1 g2 ts),
    Proof (Plonkup p i n l g1 g2 ts))
prove SetupProve (Plonkup p i n l g1 g2 ts)
setup Witness (Plonkup p i n l g1 g2 ts)
witness =
        let (PlonkupInput l g1
input, PlonkupProof g1
proof, PlonkupProverTestInfo n g1
_) = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k1) ts (core :: k2).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength 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 :: Nat)
       (l :: Type -> Type) g1 g2 ts (core :: k).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength 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)
plonkupProve @p @i @n @l @g1 @g2 @ts @core PlonkupProverSetup p i n l g1 g2
SetupProve (Plonkup p i n l g1 g2 ts)
setup (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
Witness (Plonkup p i n l g1 g2 ts)
witness)
        in (PlonkupInput l g1
Input (Plonkup p i n l g1 g2 ts)
input, PlonkupProof g1
Proof (Plonkup p i n l g1 g2 ts)
proof)

    verify :: SetupVerify (Plonkup p i n l g1 g2 ts) -> Input (Plonkup p i n l g1 g2 ts) -> Proof (Plonkup p i n l g1 g2 ts) -> Bool
    verify :: SetupVerify (Plonkup p i n l g1 g2 ts)
-> Input (Plonkup p i n l g1 g2 ts)
-> Proof (Plonkup p i n l g1 g2 ts)
-> Bool
verify = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) =>
  SetupVerify (Plonkup p i n l g1 g2 ts)
  -> Input (Plonkup p i n l g1 g2 ts)
  -> Proof (Plonkup p i n l g1 g2 ts)
  -> Bool)
 -> SetupVerify (Plonkup p i n l g1 g2 ts)
 -> Input (Plonkup p i n l g1 g2 ts)
 -> Proof (Plonkup p i n l g1 g2 ts)
 -> Bool)
-> (KnownNat ((4 * n) + 6) =>
    SetupVerify (Plonkup p i n l g1 g2 ts)
    -> Input (Plonkup p i n l g1 g2 ts)
    -> Proof (Plonkup p i n l g1 g2 ts)
    -> Bool)
-> SetupVerify (Plonkup p i n l g1 g2 ts)
-> Input (Plonkup p i n l g1 g2 ts)
-> Proof (Plonkup p i n l g1 g2 ts)
-> Bool
forall a b. (a -> b) -> a -> b
$ forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt ts.
(KnownNat n, KnownNat (PlonkupPolyExtendedLength 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
plonkupVerify @p @i @n @l @g1 @g2 @gt @ts