Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 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.
ProtostarResult | |
|
Instances
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 #
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 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. |
(Ring a, KnownNat n) => LinearCombinationWith a (Vector n a) Source # | |
(AdditiveMonoid a, Ord key) => AdditiveMonoid (Map key a) Source # | |
(AdditiveSemigroup a, Ord key) => AdditiveSemigroup (Map key a) Source # | |
(Ring a, Ord key, KnownNat k) => LinearCombination (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 # | |