{-# 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
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