ZkFold.Base.Protocol.IVC.Internal

Documentation

data IVCProof k c f

The recursion circuit satisfiability proof.

Constructors

IVCProof

Fields

• _proofX :: Vector k (c f)

  The commitment to the witness of the recursion circuit satisfiability proof.

• _proofW :: Vector k [f]

  The witness of the recursion circuit satisfiability proof.

Instances

Generic (IVCProof k c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Associated Types

type Rep (IVCProof k c f) :: Type -> Type

Methods

from :: IVCProof k c f -> Rep (IVCProof k c f) x

to :: Rep (IVCProof k c f) x -> IVCProof k c f

(Show f, Show (c f)) => Show (IVCProof k c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Methods

showsPrec :: Int -> IVCProof k c f -> ShowS

show :: IVCProof k c f -> String

showList :: [IVCProof k c f] -> ShowS

(NFData f, NFData (c f)) => NFData (IVCProof k c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Methods

rnf :: IVCProof k c f -> ()

type Rep (IVCProof k c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

type Rep (IVCProof k c f) = D1 ('MetaData "IVCProof" "ZkFold.Base.Protocol.IVC.Internal" "symbolic-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "IVCProof" 'PrefixI 'True) (S1 ('MetaSel ('Just "_proofX") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector k (c f))) :*: S1 ('MetaSel ('Just "_proofW") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector k [f]))))

proofX :: forall k c f c. Lens (IVCProof k c f) (IVCProof k c f) (Vector k (c f)) (Vector k (c f))

proofW :: forall k c f. Lens' (IVCProof k c f) (Vector k [f])

noIVCProof :: forall k c f. (KnownNat k, AdditiveMonoid (c f), AdditiveMonoid f) => IVCProof k c f

data IVCResult k i c f

The current result of recursion together with the first iteration flag, the corresponding accumulator, and the recursion circuit satisfiability proof.

Constructors

IVCResult

Fields

• _z :: i f
• _acc :: Accumulator k (RecursiveI i) c f
• _proof :: IVCProof k c f

Instances

Generic (IVCResult k i c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Associated Types

type Rep (IVCResult k i c f) :: Type -> Type

Methods

from :: IVCResult k i c f -> Rep (IVCResult k i c f) x

to :: Rep (IVCResult k i c f) x -> IVCResult k i c f

(Show f, Show (i f), Show (c f)) => Show (IVCResult k i c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Methods

showsPrec :: Int -> IVCResult k i c f -> ShowS

show :: IVCResult k i c f -> String

showList :: [IVCResult k i c f] -> ShowS

(NFData f, NFData (i f), NFData (c f)) => NFData (IVCResult k i c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

Methods

rnf :: IVCResult k i c f -> ()

type Rep (IVCResult k i c f)

Defined in ZkFold.Base.Protocol.IVC.Internal

type Rep (IVCResult k i c f) = D1 ('MetaData "IVCResult" "ZkFold.Base.Protocol.IVC.Internal" "symbolic-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "IVCResult" 'PrefixI 'True) (S1 ('MetaSel ('Just "_z") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (i f)) :*: (S1 ('MetaSel ('Just "_acc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Accumulator k (RecursiveI i) c f)) :*: S1 ('MetaSel ('Just "_proof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IVCProof k c f)))))

z :: forall k i c f. Lens' (IVCResult k i c f) (i f)

proof :: forall k i c f. Lens' (IVCResult k i c f) (IVCProof k c f)

acc :: forall k i c f. Lens' (IVCResult k i c f) (Accumulator k (RecursiveI i) c f)

type IVCAssumptions ctx0 ctx1 algo d k a i p c f = (RecursivePredicateAssumptions algo d k a i p c, KnownNat (d + 1), k ~ 1, Zip i, Field f, HashAlgorithm algo f, RandomOracle algo f f, RandomOracle algo (i f) f, RandomOracle algo (c f) f, HomomorphicCommit [f] (c f), Scale a f, Scale a (PolyVec f (d + 1)), Scale f (c f), ctx0 ~ Interpreter a, RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0, ctx1 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1, RecursiveFunctionAssumptions algo d a i c (FieldElement ctx1) ctx1)

ivcSetup :: forall ctx0 ctx1 algo d k a i p c. IVCAssumptions ctx0 ctx1 algo d k a i p c a => StepFunction a i p -> i a -> p a -> IVCResult k i c a

Create the first IVC result

It differs from the rest of the iterations as we don't have anything accumulated just yet.

ivcProve :: forall ctx0 ctx1 algo d k a i p c. IVCAssumptions ctx0 ctx1 algo d k a i p c a => StepFunction a i p -> IVCResult k i c a -> p a -> IVCResult k i c a

ivcVerify :: forall ctx0 ctx1 algo d k a i p c f. IVCAssumptions ctx0 ctx1 algo d k a i p c f => StepFunction a i p -> IVCResult k i c f -> ((Vector k (c f), [f]), (Vector k (c f), c f))