ZkFold.Symbolic.Class

Documentation

type Arithmetic a = (ResidueField Natural a, Eq a, Ord a, NFData a)

Field of residues with decidable equality and ordering is called an `arithmetic' field.

type CircuitFun (fs :: [Type -> Type]) (g :: Type -> Type) (c :: (Type -> Type) -> Type) = forall i m. (NFData i, MonadCircuit i (BaseField c) (WitnessField c) m) => FunBody fs g i m

A type of mappings between functors inside a circuit. fs are input functors, g is an output functor, c is context.

A function is a mapping between functors inside a circuit if, given an arbitrary builder of circuits m over c 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.

type family FunBody (fs :: [Type -> Type]) (g :: Type -> Type) (i :: Type) (m :: Type -> Type) where ...

Equations

FunBody '[] g i m = m (g i)

FunBody (f ': fs) g i m = f i -> FunBody fs g i m

class (HApplicative c, Package c, Arithmetic (BaseField c), ResidueField (Const (WitnessField c)) (WitnessField c)) => Symbolic c where

A Symbolic DSL for performant pure computations with arithmetic circuits. c is a generic context in which computations are performed.

Minimal complete definition

witnessF, fromCircuitF

Associated Types

type BaseField c :: Type

Base algebraic field over which computations are performed.

type WitnessField c :: Type

Type of witnesses usable inside circuit construction

Methods

witnessF :: Functor f => c f -> f (WitnessField c)

Computes witnesses (exact value may depend on the input to context).

fromCircuitF :: c f -> CircuitFun '[f] g c -> c g

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 an algorithm for turning f into g inside a circuit.

sanityF :: BaseField c ~ a => c f -> (f a -> g a) -> (c f -> c g) -> c g

If there is a simpler implementation of a function in pure context, you can provide it via sanityF to use it in pure contexts.

Instances

Arithmetic a => Symbolic (Interpreter a)

Defined in ZkFold.Symbolic.Interpreter

Associated Types

type BaseField (Interpreter a)

type WitnessField (Interpreter a)

Methods

witnessF :: Functor f => Interpreter a f -> f (WitnessField (Interpreter a))

fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type). Interpreter a f -> CircuitFun '[f] g (Interpreter a) -> Interpreter a g

sanityF :: BaseField (Interpreter a) ~ a0 => Interpreter a f -> (f a0 -> g a0) -> (Interpreter a f -> Interpreter a g) -> Interpreter a g

(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), NFData (Rep i)) => Symbolic (ArithmeticCircuit a p i)

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Associated Types

type BaseField (ArithmeticCircuit a p i)

type WitnessField (ArithmeticCircuit a p i)

Methods

witnessF :: Functor f => ArithmeticCircuit a p i f -> f (WitnessField (ArithmeticCircuit a p i))

fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type). ArithmeticCircuit a p i f -> CircuitFun '[f] g (ArithmeticCircuit a p i) -> ArithmeticCircuit a p i g

sanityF :: BaseField (ArithmeticCircuit a p i) ~ a0 => ArithmeticCircuit a p i f -> (f a0 -> g a0) -> (ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g) -> ArithmeticCircuit a p i g

embed :: (Symbolic c, Functor f) => f (BaseField c) -> c f

Embeds the pure value(s) into generic context c.

symbolicF :: (Symbolic c, BaseField c ~ a) => c f -> (f a -> g a) -> CircuitFun '[f] g c -> c g

symbolic2F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> (f a -> g a -> h a) -> CircuitFun '[f, g] h c -> c h

Runs the binary function from f and g into h in a generic context c.

fromCircuit2F :: Symbolic c => c f -> c g -> CircuitFun '[f, g] h c -> c h

Runs the binary CircuitFun in a generic context.

symbolic3F :: (Symbolic c, BaseField c ~ a) => c f -> c g -> c h -> (f a -> g a -> h a -> k a) -> CircuitFun '[f, g, h] k c -> c k

Runs the ternary function from f, g and h into k in a context c.

fromCircuit3F :: Symbolic c => c f -> c g -> c h -> CircuitFun '[f, g, h] k c -> c k

Runs the ternary CircuitFun in a generic context.

symbolicVF :: (Symbolic c, BaseField c ~ a, WitnessField c ~ w, Foldable f, Functor f) => f (c g) -> (f (g a) -> h a) -> (forall i m. MonadCircuit i a w m => f (g i) -> m (h i)) -> c h

Given a generic context c, runs the function from f many c g's into c h.

fromCircuitVF :: (Symbolic c, BaseField c ~ a, WitnessField c ~ w, Foldable f, Functor f) => f (c g) -> (forall i m. MonadCircuit i a w m => f (g i) -> m (h i)) -> c h

Given a generic context c, runs the CircuitFun from f many c g's into c h.