{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

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

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.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class             (EllipticCurve (..), Pairing (..), PointCompressed)
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 i n l c1 c2 ts core.
        ( KnownNat i
        , KnownNat n
        , KnownNat l
        , Ord (BaseField c1)
        , AdditiveGroup (BaseField c1)
        , Pairing c1 c2
        , Arithmetic (ScalarField c1)
        , ToTranscript ts Word8
        , ToTranscript ts (ScalarField c1)
        , ToTranscript ts (PointCompressed c1)
        , FromTranscript ts (ScalarField c1)
        , CoreFunction c1 core
        ) => NonInteractiveProof (Plonkup i n l c1 c2 ts) core where
    type Transcript (Plonkup i n l c1 c2 ts)  = ts
    type SetupProve (Plonkup i n l c1 c2 ts)  = PlonkupProverSetup i n l c1 c2
    type SetupVerify (Plonkup i n l c1 c2 ts) = PlonkupVerifierSetup i n l c1 c2
    type Witness (Plonkup i n l c1 c2 ts)     = (PlonkupWitnessInput i c1, PlonkupProverSecret c1)
    type Input (Plonkup i n l c1 c2 ts)       = PlonkupInput l c1
    type Proof (Plonkup i n l c1 c2 ts)       = PlonkupProof c1

    setupProve :: Plonkup i n l c1 c2 ts -> SetupProve (Plonkup i n l c1 c2 ts)
    setupProve :: Plonkup i n l c1 c2 ts -> SetupProve (Plonkup i n l c1 c2 ts)
setupProve Plonkup i n l c1 c2 ts
plonk =
        let PlonkupSetup {Vector (Point c1)
ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PolyVec (ScalarField c1) n
PlonkupRelation i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
h0 :: Point c2
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
commitments :: PlonkupCircuitCommitments c1
omega :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
k1 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
k2 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
gs :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Vector (Point c1)
h0 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Point c2
h1 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Point c2
sigma1s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupRelation i n l (ScalarField c1)
polynomials :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupCircuitPolynomials n c1
commitments :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupCircuitCommitments c1
..} = forall (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k) (c2 :: k1) ts
       (core :: k).
(KnownNat i, KnownNat l, KnownNat n, Arithmetic (ScalarField c1),
 Pairing c1 c2, CoreFunction c1 core) =>
Plonkup i n l c1 c2 ts -> PlonkupSetup i n l c1 c2
forall {k1} {k2} {k3} {k4} (i :: Nat) (n :: Nat) (l :: Nat)
       (c1 :: k1) (c2 :: k2) (ts :: k3) (core :: k4).
(KnownNat i, KnownNat l, KnownNat n, Arithmetic (ScalarField c1),
 Pairing c1 c2, CoreFunction c1 core) =>
Plonkup i n l c1 c2 ts -> PlonkupSetup i n l c1 c2
plonkupSetup @_ @_ @_ @c1 @_ @_ @core Plonkup i n l c1 c2 ts
plonk
        in PlonkupProverSetup {Vector (Point c1)
ScalarField c1
PolyVec (ScalarField c1) n
PlonkupRelation i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
..}

    setupVerify :: Plonkup i n l c1 c2 ts -> SetupVerify (Plonkup i n l c1 c2 ts)
    setupVerify :: Plonkup i n l c1 c2 ts -> SetupVerify (Plonkup i n l c1 c2 ts)
setupVerify Plonkup i n l c1 c2 ts
plonk =
        let PlonkupSetup {Vector (Point c1)
ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PolyVec (ScalarField c1) n
PlonkupRelation i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
k1 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
k2 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> ScalarField c1
gs :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Vector (Point c1)
h0 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Point c2
h1 :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> Point c2
sigma1s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupRelation i n l (ScalarField c1)
polynomials :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupCircuitPolynomials n c1
commitments :: forall {k1} {k2} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k1)
       (c2 :: k2).
PlonkupSetup i n l c1 c2 -> PlonkupCircuitCommitments c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
h0 :: Point c2
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
commitments :: PlonkupCircuitCommitments c1
..} = forall (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k) (c2 :: k1) ts
       (core :: k).
(KnownNat i, KnownNat l, KnownNat n, Arithmetic (ScalarField c1),
 Pairing c1 c2, CoreFunction c1 core) =>
Plonkup i n l c1 c2 ts -> PlonkupSetup i n l c1 c2
forall {k1} {k2} {k3} {k4} (i :: Nat) (n :: Nat) (l :: Nat)
       (c1 :: k1) (c2 :: k2) (ts :: k3) (core :: k4).
(KnownNat i, KnownNat l, KnownNat n, Arithmetic (ScalarField c1),
 Pairing c1 c2, CoreFunction c1 core) =>
Plonkup i n l c1 c2 ts -> PlonkupSetup i n l c1 c2
plonkupSetup @_ @_ @_ @c1 @_ @_ @core Plonkup i n l c1 c2 ts
plonk
        in PlonkupVerifierSetup {ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PolyVec (ScalarField c1) n
PlonkupRelation i n l (ScalarField c1)
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
commitments :: PlonkupCircuitCommitments c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation i n l (ScalarField c1)
commitments :: PlonkupCircuitCommitments c1
..}

    prove :: SetupProve (Plonkup i n l c1 c2 ts) -> Witness (Plonkup i n l c1 c2 ts) -> (Input (Plonkup i n l c1 c2 ts), Proof (Plonkup i n l c1 c2 ts))
    prove :: SetupProve (Plonkup i n l c1 c2 ts)
-> Witness (Plonkup i n l c1 c2 ts)
-> (Input (Plonkup i n l c1 c2 ts), Proof (Plonkup i n l c1 c2 ts))
prove SetupProve (Plonkup i n l c1 c2 ts)
setup Witness (Plonkup i n l c1 c2 ts)
witness =
        let (PlonkupInput l c1
input, PlonkupProof c1
proof, PlonkupProverTestInfo n c1
_) = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k) (c2 :: k1) ts
       (core :: k).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n),
 Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1), CoreFunction c1 core) =>
PlonkupProverSetup i n l c1 c2
-> (PlonkupWitnessInput i c1, PlonkupProverSecret c1)
-> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
forall {k} {k2} {k3} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k)
       (c2 :: k2) ts (core :: k3).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n),
 Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1), CoreFunction c1 core) =>
PlonkupProverSetup i n l c1 c2
-> (PlonkupWitnessInput i c1, PlonkupProverSecret c1)
-> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
plonkupProve @i @n @l @c1 @c2 @ts @core SetupProve (Plonkup i n l c1 c2 ts)
PlonkupProverSetup i n l c1 c2
setup (PlonkupWitnessInput i c1, PlonkupProverSecret c1)
Witness (Plonkup i n l c1 c2 ts)
witness)
        in (Input (Plonkup i n l c1 c2 ts)
PlonkupInput l c1
input, PlonkupProof c1
Proof (Plonkup i n l c1 c2 ts)
proof)

    verify :: SetupVerify (Plonkup i n l c1 c2 ts) -> Input (Plonkup i n l c1 c2 ts) -> Proof (Plonkup i n l c1 c2 ts) -> Bool
    verify :: SetupVerify (Plonkup i n l c1 c2 ts)
-> Input (Plonkup i n l c1 c2 ts)
-> Proof (Plonkup i n l c1 c2 ts)
-> Bool
verify = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) =>
  SetupVerify (Plonkup i n l c1 c2 ts)
  -> Input (Plonkup i n l c1 c2 ts)
  -> Proof (Plonkup i n l c1 c2 ts)
  -> Bool)
 -> SetupVerify (Plonkup i n l c1 c2 ts)
 -> Input (Plonkup i n l c1 c2 ts)
 -> Proof (Plonkup i n l c1 c2 ts)
 -> Bool)
-> (KnownNat ((4 * n) + 6) =>
    SetupVerify (Plonkup i n l c1 c2 ts)
    -> Input (Plonkup i n l c1 c2 ts)
    -> Proof (Plonkup i n l c1 c2 ts)
    -> Bool)
-> SetupVerify (Plonkup i n l c1 c2 ts)
-> Input (Plonkup i n l c1 c2 ts)
-> Proof (Plonkup i n l c1 c2 ts)
-> Bool
forall a b. (a -> b) -> a -> b
$ forall (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k) (c2 :: k1) ts.
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Pairing c1 c2,
 Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1)) =>
PlonkupVerifierSetup i n l c1 c2
-> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
forall {k} {k1} (i :: Nat) (n :: Nat) (l :: Nat) (c1 :: k)
       (c2 :: k1) ts.
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Pairing c1 c2,
 Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1)) =>
PlonkupVerifierSetup i n l c1 c2
-> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
plonkupVerify @i @n @l @c1 @c2 @ts