Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Base.Protocol.Protostar.Fold

Contents

Orphan instances

Synopsis

type C n a = ArithmeticCircuit a (Vector n) (Vector n)
type FS_CM ctx n comm a = FiatShamir (FieldElement ctx) (CommitOpen (MapMessage (FieldElement ctx) (C n a)) comm (C n a))
type Acc ctx n comm a = Accumulator (Vector n (FieldElement ctx)) (FieldElement ctx) comm (MapMessage (FieldElement ctx) (C n a))
data ProtostarResult (ctx :: (Type -> Type) -> Type) n comm a = ProtostarResult {
- result :: Vector n (FieldElement ctx)
- proverOutput :: Acc ctx n comm a
}
toFS :: forall ctx n comm a. HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => FieldElement ctx -> C n a -> Vector n (FieldElement ctx) -> FS_CM ctx n comm a
ivcVerifier :: forall i f c m ctx a. Symbolic ctx => AccumulatorScheme i f c m ctx a => (i, c, (i, c, f, c, f), (i, c, f, c, f), c) -> (a, (f, (f, f)), ((i, c, f, c, f), m)) -> Bool ctx
ivcVerifierAc :: forall i f c m ctx a y t. Symbolic ctx => SymbolicInput (i, c, (i, c, f, c, f), (i, c, f, c, f), c) => SymbolicInput (a, (f, (f, f)), ((i, c, f, c, f), m)) => SymbolicData y => Context a ~ ctx => Context i ~ ctx => Context y ~ ctx => Support y ~ Proxy ctx => Layout y ~ Par1 => t ~ ((i, c, (i, c, f, c, f), (i, c, f, c, f), c), (a, (f, f, f), (i, c, f, c, f), m), Proxy ctx) => ctx ~ ArithmeticCircuit a (Layout t) => AccumulatorScheme i f c m ctx a => y
iterate :: forall ctx n comm a. KnownNat n => Arithmetic a => Binary a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => Eq (Bool ctx) comm => Eq (Bool ctx) [comm] => Eq (Bool ctx) [FieldElement ctx] => Eq (Bool ctx) (Vector n (FieldElement ctx)) => RandomOracle comm (FieldElement ctx) => HomomorphicCommit (FieldElement ctx) [FieldElement ctx] comm => HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => AdditiveGroup comm => Scale a (PolyVec (FieldElement ctx) 3) => Scale a (FieldElement ctx) => Scale (FieldElement ctx) comm => ctx ~ ArithmeticCircuit a (Vector n) => Input (FieldElement ctx) (C n a) ~ Vector n (FieldElement ctx) => (forall c. (Symbolic c, BaseField c ~ a) => Vector n (FieldElement c) -> Vector n (FieldElement c)) -> Vector n a -> Natural -> ProtostarResult ctx n comm a
instanceProof :: forall ctx n comm a. Symbolic ctx => Arithmetic a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => FieldElement ctx -> C n a -> MapInput (FieldElement ctx) (C n a) -> Vector n a -> InstanceProofPair (Vector n (FieldElement ctx)) comm (MapMessage (FieldElement ctx) (C n a))
iteration :: forall ctx n comm a. Symbolic ctx => KnownNat n => Arithmetic a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => Input (FieldElement ctx) (C n a) ~ Vector n (FieldElement ctx) => Eq (Bool ctx) comm => Eq (Bool ctx) [comm] => Eq (Bool ctx) [FieldElement ctx] => Eq (Bool ctx) (Vector n (FieldElement ctx)) => RandomOracle comm (FieldElement ctx) => HomomorphicCommit (FieldElement ctx) [FieldElement ctx] comm => HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => AdditiveGroup comm => Scale a (PolyVec (FieldElement ctx) 3) => Scale a (FieldElement ctx) => Scale (FieldElement ctx) comm => Natural -> FieldElement ctx -> (Vector n (FieldElement ctx) -> Vector n (FieldElement ctx)) -> C n a -> MapInput (FieldElement ctx) (C n a) -> Vector n a -> Acc ctx n comm a -> KeyScale (FieldElement ctx) -> ProtostarResult ctx n comm a

Documentation

type C n a = ArithmeticCircuit a (Vector n) (Vector n) Source #

type FS_CM ctx n comm a = FiatShamir (FieldElement ctx) (CommitOpen (MapMessage (FieldElement ctx) (C n a)) comm (C n a)) Source #

type Acc ctx n comm a = Accumulator (Vector n (FieldElement ctx)) (FieldElement ctx) comm (MapMessage (FieldElement ctx) (C n a)) Source #

data ProtostarResult (ctx :: (Type -> Type) -> Type) n comm a Source #

The final result of recursion and the final accumulator. Accumulation decider is an arithmetizable function which can be called on the final accumulator.

Constructors

ProtostarResult
Fields result :: Vector n (FieldElement ctx) proverOutput :: Acc ctx n comm a

Instances

Instances details

Generic (ProtostarResult ctx n comm a) Source #
Instance details Defined in ZkFold.Base.Protocol.Protostar.Fold Associated Types type Rep (ProtostarResult ctx n comm a) :: Type -> Type # Methods from :: ProtostarResult ctx n comm a -> Rep (ProtostarResult ctx n comm a) x # to :: Rep (ProtostarResult ctx n comm a) x -> ProtostarResult ctx n comm a #
(Show (Bool ctx), Show comm, Show (ctx Par1)) => Show (ProtostarResult ctx n comm a) Source #
Instance details Defined in ZkFold.Base.Protocol.Protostar.Fold Methods showsPrec :: Int -> ProtostarResult ctx n comm a -> ShowS # show :: ProtostarResult ctx n comm a -> String # showList :: [ProtostarResult ctx n comm a] -> ShowS #
(NFData (Bool ctx), NFData comm, NFData (FieldElement ctx)) => NFData (ProtostarResult ctx n comm a) Source #
Instance details Defined in ZkFold.Base.Protocol.Protostar.Fold Methods rnf :: ProtostarResult ctx n comm a -> () #
type Rep (ProtostarResult ctx n comm a) Source #
Instance details Defined in ZkFold.Base.Protocol.Protostar.Fold type Rep (ProtostarResult ctx n comm a) = D1 ('MetaData "ProtostarResult" "ZkFold.Base.Protocol.Protostar.Fold" "symbolic-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "ProtostarResult" 'PrefixI 'True) (S1 ('MetaSel ('Just "result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector n (FieldElement ctx))) :*: S1 ('MetaSel ('Just "proverOutput") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Acc ctx n comm a))))

toFS :: forall ctx n comm a. HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => FieldElement ctx -> C n a -> Vector n (FieldElement ctx) -> FS_CM ctx n comm a Source #

ivcVerifier :: forall i f c m ctx a. Symbolic ctx => AccumulatorScheme i f c m ctx a => (i, c, (i, c, f, c, f), (i, c, f, c, f), c) -> (a, (f, (f, f)), ((i, c, f, c, f), m)) -> Bool ctx Source #

ivcVerifierAc :: forall i f c m ctx a y t. Symbolic ctx => SymbolicInput (i, c, (i, c, f, c, f), (i, c, f, c, f), c) => SymbolicInput (a, (f, (f, f)), ((i, c, f, c, f), m)) => SymbolicData y => Context a ~ ctx => Context i ~ ctx => Context y ~ ctx => Support y ~ Proxy ctx => Layout y ~ Par1 => t ~ ((i, c, (i, c, f, c, f), (i, c, f, c, f), c), (a, (f, f, f), (i, c, f, c, f), m), Proxy ctx) => ctx ~ ArithmeticCircuit a (Layout t) => AccumulatorScheme i f c m ctx a => y Source #

instanceProof :: forall ctx n comm a. Symbolic ctx => Arithmetic a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => FieldElement ctx -> C n a -> MapInput (FieldElement ctx) (C n a) -> Vector n a -> InstanceProofPair (Vector n (FieldElement ctx)) comm (MapMessage (FieldElement ctx) (C n a)) Source #

iteration :: forall ctx n comm a. Symbolic ctx => KnownNat n => Arithmetic a => Scale a (BaseField ctx) => FromConstant a (BaseField ctx) => Input (FieldElement ctx) (C n a) ~ Vector n (FieldElement ctx) => Eq (Bool ctx) comm => Eq (Bool ctx) [comm] => Eq (Bool ctx) [FieldElement ctx] => Eq (Bool ctx) (Vector n (FieldElement ctx)) => RandomOracle comm (FieldElement ctx) => HomomorphicCommit (FieldElement ctx) [FieldElement ctx] comm => HomomorphicCommit (FieldElement ctx) [MapMessage (FieldElement ctx) (C n a)] comm => AdditiveGroup comm => Scale a (PolyVec (FieldElement ctx) 3) => Scale a (FieldElement ctx) => Scale (FieldElement ctx) comm => Natural -> FieldElement ctx -> (Vector n (FieldElement ctx) -> Vector n (FieldElement ctx)) -> C n a -> MapInput (FieldElement ctx) (C n a) -> Vector n a -> Acc ctx n comm a -> KeyScale (FieldElement ctx) -> ProtostarResult ctx n comm a Source #

Orphan instances

Scale s a => Scale s (Map k a) Source #	These instances might seem off, but accumulator scheme requires this exact behaviour for ProverMessages which are Maps in this case.
Instance details Methods scale :: s -> Map k a -> Map k a Source #
(Ring a, KnownNat n) => LinearCombinationWith a (Vector n a) Source #
Instance details Methods linearCombinationWith :: a -> Vector n a -> Vector n a -> Vector n a Source #
(AdditiveMonoid a, Ord key) => AdditiveMonoid (Map key a) Source #
Instance details Methods zero :: Map key a Source #
(AdditiveSemigroup a, Ord key) => AdditiveSemigroup (Map key a) Source #
Instance details Methods (+) :: Map key a -> Map key a -> Map key a Source #
(Ring a, Ord key, KnownNat k) => LinearCombination (Map key a) (Map key (PolyVec a k)) Source #
Instance details Methods linearCombination :: Map key a -> Map key a -> Map key (PolyVec a k) Source #
(Ring a, KnownNat n, KnownNat k) => LinearCombination (Vector n a) (Vector n (PolyVec a k)) Source #
Instance details Methods linearCombination :: Vector n a -> Vector n a -> Vector n (PolyVec a k) Source #