Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class (HApplicative c, Package c, Arithmetic (BaseField c)) => Symbolic c where
- type BaseField c :: Type
- symbolicF :: BaseField c ~ a => c f -> (f a -> g a) -> CircuitFun f g a -> c g
- fromCircuitF :: c f -> CircuitFun f g (BaseField c) -> c g
- type CircuitFun f g a = forall i m. MonadCircuit i a m => f i -> m (g i)
- embed :: (Symbolic c, Functor f) => f (BaseField c) -> c f
- fromCircuit2F :: Symbolic c => c f -> c g -> (forall i m. MonadCircuit i (BaseField c) m => f i -> g i -> m (h i)) -> c h
- symbolic2F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> (f a -> g a -> h a) -> (forall i m. MonadCircuit i a m => f i -> g i -> m (h i)) -> c h
- symbolic3F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> c h -> (f a -> g a -> h a -> k a) -> (forall i m. MonadCircuit i a m => f i -> g i -> h i -> m (k i)) -> c k
- fromCircuit3F :: Symbolic c => c f -> c g -> c h -> (forall i m. MonadCircuit i (BaseField c) m => f i -> g i -> h i -> m (k i)) -> c k
- symbolicVF :: (Symbolic c, BaseField c ~ a, Foldable f, Functor f) => f (c g) -> (f (g a) -> h a) -> (forall i m. MonadCircuit i a m => f (g i) -> m (h i)) -> c h
- fromCircuitVF :: (Symbolic c, Foldable f, Functor f) => f (c g) -> (forall i m. MonadCircuit i (BaseField c) m => f (g i) -> m (h i)) -> c h
- type Arithmetic a = (WitnessField Natural a, Eq a, Ord a)
Documentation
class (HApplicative c, Package c, Arithmetic (BaseField c)) => Symbolic c where Source #
A Symbolic DSL for performant pure computations with arithmetic circuits.
c
is a generic context in which computations are performed.
symbolicF :: BaseField c ~ a => c f -> (f a -> g a) -> CircuitFun f g a -> c g Source #
To perform computations in a generic context c
-- that is,
to form a mapping between c f
and c g
for given f
and g
--
you need to provide two things:
- An algorithm for turning
f
intog
in a pure context; - An algorithm for turning
f
intog
inside a circuit.
It is not however checked (yet) that the provided algorithms compute the same things.
If the pure-context computation is tautological to the circuit
computation, use
.fromCircuitF
fromCircuitF :: c f -> CircuitFun f g (BaseField c) -> c g Source #
Instances
(Arithmetic a, Binary a, Representable i, Binary (Rep i), Ord (Rep i)) => Symbolic (ArithmeticCircuit a i) Source # | |
Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal type BaseField (ArithmeticCircuit a i) Source # symbolicF :: BaseField (ArithmeticCircuit a i) ~ a0 => ArithmeticCircuit a i f -> (f a0 -> g a0) -> CircuitFun f g a0 -> ArithmeticCircuit a i g Source # fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type). ArithmeticCircuit a i f -> CircuitFun f g (BaseField (ArithmeticCircuit a i)) -> ArithmeticCircuit a i g Source # | |
Arithmetic a => Symbolic (Interpreter a) Source # | |
Defined in ZkFold.Symbolic.Interpreter type BaseField (Interpreter a) Source # symbolicF :: BaseField (Interpreter a) ~ a0 => Interpreter a f -> (f a0 -> g a0) -> CircuitFun f g a0 -> Interpreter a g Source # fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type). Interpreter a f -> CircuitFun f g (BaseField (Interpreter a)) -> Interpreter a g Source # |
type CircuitFun f g a = forall i m. MonadCircuit i a m => f i -> m (g i) Source #
A type of mappings between functors inside a circuit.
f
is an input functor, g
is an output functor, a
is a base field.
A function is a mapping between functors inside a circuit if,
given an arbitrary builder of circuits m
over a
with arbitrary i
as
variables, it maps f
many inputs to g
many outputs using m
.
NOTE: the property above is correct by construction for each function of a suitable type, you don't have to check it yourself.
embed :: (Symbolic c, Functor f) => f (BaseField c) -> c f Source #
Embeds the pure value(s) into generic context c
.
fromCircuit2F :: Symbolic c => c f -> c g -> (forall i m. MonadCircuit i (BaseField c) m => f i -> g i -> m (h i)) -> c h Source #
Runs the binary
in a generic context.CircuitFun
symbolic2F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> (f a -> g a -> h a) -> (forall i m. MonadCircuit i a m => f i -> g i -> m (h i)) -> c h Source #
Runs the binary function from f
and g
into h
in a generic context c
.
symbolic3F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> c h -> (f a -> g a -> h a -> k a) -> (forall i m. MonadCircuit i a m => f i -> g i -> h i -> m (k i)) -> c k Source #
Runs the ternary function from f
, g
and h
into k
in a context c
.
fromCircuit3F :: Symbolic c => c f -> c g -> c h -> (forall i m. MonadCircuit i (BaseField c) m => f i -> g i -> h i -> m (k i)) -> c k Source #
Runs the ternary
in a generic context.CircuitFun
symbolicVF :: (Symbolic c, BaseField c ~ a, Foldable f, Functor f) => f (c g) -> (f (g a) -> h a) -> (forall i m. MonadCircuit i a m => f (g i) -> m (h i)) -> c h Source #
Given a generic context c
, runs the function from f
many c g
's into c h
.
fromCircuitVF :: (Symbolic c, Foldable f, Functor f) => f (c g) -> (forall i m. MonadCircuit i (BaseField c) m => f (g i) -> m (h i)) -> c h Source #
Given a generic context c
, runs the
from CircuitFun
f
many c g
's into c h
.
type Arithmetic a = (WitnessField Natural a, Eq a, Ord a) Source #
Field of witnesses with decidable equality and ordering
is called an `arithmetic'
field.