Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Class

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.

Minimal complete definition

symbolicF

Associated Types

type BaseField c :: Type Source #

Base algebraic field over which computations are performed.

Methods

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 into g in a pure context;
An algorithm for turning f into g 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 #

A wrapper around symbolicF which extracts the pure computation from the circuit computation using the Witnesses newtype.

Instances

Instances details

(Arithmetic a, Binary a, Representable i, Binary (Rep i), Ord (Rep i)) => Symbolic (ArithmeticCircuit a i) Source #
Instance details Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal Associated Types type BaseField (ArithmeticCircuit a i) Source # Methods 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 #
Instance details Defined in ZkFold.Symbolic.Interpreter Associated Types type BaseField (Interpreter a) Source # Methods 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 CircuitFun in a generic context.

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 CircuitFun in a generic context.

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 CircuitFun from 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.