| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
ZkFold.Symbolic.Compiler.ArithmeticCircuit.MonadBlueprint
Contents
Synopsis
- type ClosedPoly i a = forall x. Algebra a x => (i -> x) -> x
- class Monad m => MonadBlueprint i a m | m -> i, m -> a where
- input :: m i
- output :: i -> m (ArithmeticCircuit a)
- runCircuit :: ArithmeticCircuit a -> m i
- newConstrained :: NewConstraint i a -> Witness i a -> m i
- constraint :: ClosedPoly i a -> m ()
- newAssigned :: ClosedPoly i a -> m i
- type NewConstraint i a = forall x. Algebra a x => (i -> x) -> i -> x
- type Witness i a = forall x. WitnessField a x => (i -> x) -> x
- type WitnessField a x = (Algebra a x, FiniteField x, BinaryExpansion x, Eq (Bool x) x, Conditional (Bool x) x, Conditional (Bool x) (Bool x))
- circuit :: Arithmetic a => (forall i m. MonadBlueprint i a m => m i) -> ArithmeticCircuit a
- circuits :: (Arithmetic a, Functor f) => (forall i m. MonadBlueprint i a m => m (f i)) -> f (ArithmeticCircuit a)
Documentation
type ClosedPoly i a = forall x. Algebra a x => (i -> x) -> x Source #
A type of polynomial expressions. i is a type of variables, a is a base field.
A function is a polynomial expression if, given an arbitrary algebra x over
a and a function mapping known variables to their witnesses, it computes a
new value in that algebra.
NOTE: the property above is correct by construction for each function of a suitable type, you don't have to check it yourself.
class Monad m => MonadBlueprint i a m | m -> i, m -> a where Source #
Minimal complete definition
Methods
DSL for constructing arithmetic circuits. i is a type of variables,
a is a base field and m is a monad for constructing the circuit.
DSL provides the following guarantees: * There are no unconstrained variables; * Variables with equal constraints and witnesses are reused as much as possible; * Variables with either different constraints or different witnesses are different; * There is an order in which witnesses can be generated; * Constraints never reference undefined variables.
However, DSL does NOT provide the following guarantees (yet):
* That provided witnesses satisfy the provided constraints. To check this,
you can use checkCircuit.
* That introduced polynomial constraints are supported by the zk-SNARK
utilized for later proving.
Creates new input variable.
output :: i -> m (ArithmeticCircuit a) Source #
Returns a circuit with supplied variable as output.
runCircuit :: ArithmeticCircuit a -> m i Source #
Adds the supplied circuit to the blueprint and returns its output variable.
newConstrained :: NewConstraint i a -> Witness i a -> m i Source #
Creates new variable given a constraint polynomial and a witness.
constraint :: ClosedPoly i a -> m () Source #
Adds new constraint to the system.
newAssigned :: ClosedPoly i a -> m i Source #
Creates new variable given a polynomial witness.
Instances
| Arithmetic a => MonadBlueprint Natural a (State (ArithmeticCircuit a)) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.MonadBlueprint Methods input :: State (ArithmeticCircuit a) Natural Source # output :: Natural -> State (ArithmeticCircuit a) (ArithmeticCircuit a) Source # runCircuit :: ArithmeticCircuit a -> State (ArithmeticCircuit a) Natural Source # newConstrained :: NewConstraint Natural a -> Witness Natural a -> State (ArithmeticCircuit a) Natural Source # constraint :: ClosedPoly Natural a -> State (ArithmeticCircuit a) () Source # newAssigned :: ClosedPoly Natural a -> State (ArithmeticCircuit a) Natural Source # | |
type NewConstraint i a = forall x. Algebra a x => (i -> x) -> i -> x Source #
A type of constraints for new variables. i is a type of variables, a is a base field.
A function is a constraint for a new variable if, given an arbitrary algebra
x over a, a function mapping known variables to their witnesses in that
algebra and a new variable, it computes the value of a constraint polynomial
in that algebra.
NOTE: the property above is correct by construction for each function of a suitable type, you don't have to check it yourself.
type Witness i a = forall x. WitnessField a x => (i -> x) -> x Source #
A type of witness builders. i is a type of variables, a is a base field.
A function is a witness builer if, given an arbitrary field of witnesses x
over a and a function mapping known variables to their witnesses, it computes
the new witness in x.
NOTE: the property above is correct by construction for each function of a suitable type, you don't have to check it yourself.
type WitnessField a x = (Algebra a x, FiniteField x, BinaryExpansion x, Eq (Bool x) x, Conditional (Bool x) x, Conditional (Bool x) (Bool x)) Source #
DSL for constructing witnesses in an arithmetic circuit. a is a base
field; x is a "field of witnesses over a" which you can safely assume to
be identical to a with internalized equality.
circuit :: Arithmetic a => (forall i m. MonadBlueprint i a m => m i) -> ArithmeticCircuit a Source #
Builds a circuit from blueprint. A blueprint is a function which, given an
arbitrary type of variables i and a monad m supporting the MonadBlueprint
API, computes the output variable of a future circuit.
circuits :: (Arithmetic a, Functor f) => (forall i m. MonadBlueprint i a m => m (f i)) -> f (ArithmeticCircuit a) Source #
Builds a collection of circuits from one blueprint. A blueprint is a function
which, given an arbitrary type of variables i and a monad m supporting the
MonadBlueprint API, computes the collection of output variables of future circuits.
Orphan instances
| (Finite a, Ord i) => Conditional (Bool (Sources a i)) (Bool (Sources a i)) Source # | |
Methods bool :: Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) Source # gif :: Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) Source # (?) :: Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) -> Bool (Sources a i) Source # | |
| (Finite a, Ord i) => Conditional (Bool (Sources a i)) (Sources a i) Source # | |
| Ord i => Eq (Bool (Sources a i)) (Sources a i) Source # | |