Safe Haskell	Safe-Inferred
Language	Haskell2010

ZkFold.Symbolic.Class

Synopsis

type Arithmetic a = (ResidueField a, IntegralOf a ~ Integer, ToConstant a, Const a ~ Natural, Eq a, Ord a, NFData a)
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
type family FunBody (fs :: [Type -> Type]) (g :: Type -> Type) (i :: Type) (m :: Type -> Type) where ...
class (HApplicative c, Package c, Arithmetic (BaseField c), ResidueField (WitnessField c)) => Symbolic c where
- type BaseField c :: Type
- type WitnessField c :: Type
- witnessF :: Functor f => c f -> f (WitnessField c)
- fromCircuitF :: c f -> CircuitFun '[f] g c -> c g
- sanityF :: BaseField c ~ a => c f -> (f a -> g a) -> (c f -> c g) -> c g
embed :: (Symbolic c, Functor f) => f (BaseField c) -> c f
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
fromCircuit2F :: Symbolic c => c f -> c g -> CircuitFun '[f, g] h c -> c h
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
fromCircuit3F :: Symbolic c => c f -> c g -> c h -> CircuitFun '[f, g, h] k c -> c k
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
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

Documentation

type Arithmetic a = (ResidueField a, IntegralOf a ~ Integer, ToConstant a, Const a ~ Natural, Eq a, Ord a, NFData a) Source #

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 Source #

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 ... Source #

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 (WitnessField 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

witnessF, fromCircuitF

Associated Types

type BaseField c :: Type Source #

Base algebraic field over which computations are performed.

type WitnessField c :: Type Source #

Type of witnesses usable inside circuit construction

Methods

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

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

fromCircuitF :: c f -> CircuitFun '[f] g c -> 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 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 Source #

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

Instances details

Arithmetic a => Symbolic (Interpreter a) Source #
Instance details Defined in ZkFold.Symbolic.Interpreter Associated Types type BaseField (Interpreter a) Source # type WitnessField (Interpreter a) Source # Methods witnessF :: Functor f => Interpreter a f -> f (WitnessField (Interpreter a)) Source # fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type). Interpreter a f -> CircuitFun '[f] g (Interpreter a) -> Interpreter a g Source # sanityF :: BaseField (Interpreter a) ~ a0 => Interpreter a f -> (f a0 -> g a0) -> (Interpreter a f -> Interpreter a g) -> Interpreter a g Source #
(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), NFData (Rep i)) => Symbolic (ArithmeticCircuit a p i) Source #
Instance details Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal Associated Types type BaseField (ArithmeticCircuit a p i) Source # type WitnessField (ArithmeticCircuit a p i) Source # Methods witnessF :: Functor f => ArithmeticCircuit a p i f -> f (WitnessField (ArithmeticCircuit a p i)) Source # 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 Source # 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 Source #

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

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 Source #

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

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 Source #

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 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 -> CircuitFun '[f, g, h] k c -> c k Source #

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 Source #

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 Source #

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