Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data ArithmeticCircuit a p i o
- type Constraint c i = Poly c (SysVar i) Natural
- data Var a i
- witnessGenerator :: (Arithmetic a, Representable p, Representable i) => ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a
- optimize :: ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o
- desugarRanges :: (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i)) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o
- emptyCircuit :: ArithmeticCircuit a p i U1
- idCircuit :: Representable i => ArithmeticCircuit a p i i
- naturalCircuit :: (Arithmetic a, Representable p, Representable i, Traversable o, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i)) => (forall x. p x -> i x -> o x) -> ArithmeticCircuit a p i o
- inputPayload :: (Representable p, Representable i) => (forall x. p x -> i x -> o x) -> o (WitnessF a (WitVar p i))
- guessOutput :: (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Binary (Rep o)) => (Ord (Rep i), Ord (Rep o), NFData (Rep i), NFData (Rep o)) => (Representable i, Representable o, Foldable o) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p (i :*: o) U1
- eval :: (Arithmetic a, Representable p, Representable i, Functor o) => ArithmeticCircuit a p i o -> p a -> i a -> o a
- eval1 :: (Arithmetic a, Representable p, Representable i) => ArithmeticCircuit a p i Par1 -> p a -> i a -> a
- exec :: (Arithmetic a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a
- exec1 :: Arithmetic a => ArithmeticCircuit a U1 U1 Par1 -> a
- acSizeN :: ArithmeticCircuit a p i o -> Natural
- acSizeM :: ArithmeticCircuit a p i o -> Natural
- acSizeR :: ArithmeticCircuit a p i o -> Natural
- acSystem :: ArithmeticCircuit a p i o -> Map ByteString (Constraint a i)
- acValue :: (Arithmetic a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a
- acPrint :: (Arithmetic a, Show a, Show (o (Var a U1)), Show (o a), Functor o) => ArithmeticCircuit a U1 U1 o -> IO ()
- hlmap :: (Representable i, Representable j, Ord (Rep j), Functor o) => (forall x. j x -> i x) -> ArithmeticCircuit a p i o -> ArithmeticCircuit a p j o
- hpmap :: (Representable p, Representable q) => (forall x. q x -> p x) -> ArithmeticCircuit a p i o -> ArithmeticCircuit a q i o
- mapVarArithmeticCircuit :: (Field a, Eq a, Functor o, Ord (Rep i), Representable i, Foldable i) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o
- acWitness :: ArithmeticCircuit a p i o -> Map ByteString (WitnessF a (WitVar p i))
- acInput :: Representable i => i (Var a i)
- acOutput :: ArithmeticCircuit a p i o -> o (Var a i)
- checkCircuit :: Arbitrary (p a) => Arbitrary (i a) => Arithmetic a => Show a => Representable p => Representable i => ArithmeticCircuit a p i o -> Property
- checkClosedCircuit :: forall a o. Arithmetic a => Show a => ArithmeticCircuit a U1 U1 o -> Property
- isConstantInput :: (Arithmetic a, Show a, Representable p, Representable i, Show (p a), Show (i a), Arbitrary (p a), Arbitrary (i a)) => ArithmeticCircuit a p i o -> Property
Documentation
data ArithmeticCircuit a p i o Source #
Arithmetic circuit in the form of a system of polynomial constraints.
Instances
type Constraint c i = Poly c (SysVar i) Natural Source #
The type that represents a constraint in the arithmetic circuit.
Instances
witnessGenerator :: (Arithmetic a, Representable p, Representable i) => ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a Source #
optimize :: ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o Source #
Optimizes the constraint system.
TODO: Implement nontrivial optimizations.
desugarRanges :: (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i)) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o Source #
Desugars range constraints into polynomial constraints
emptyCircuit :: ArithmeticCircuit a p i U1 Source #
idCircuit :: Representable i => ArithmeticCircuit a p i i Source #
Identity circuit which returns its input i
and doesn't use the payload.
naturalCircuit :: (Arithmetic a, Representable p, Representable i, Traversable o, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i)) => (forall x. p x -> i x -> o x) -> ArithmeticCircuit a p i o Source #
Given a natural transformation
from payload p
and input i
to output o
,
returns a corresponding arithmetic circuit
where outputs computing the payload are unconstrained.
inputPayload :: (Representable p, Representable i) => (forall x. p x -> i x -> o x) -> o (WitnessF a (WitVar p i)) Source #
Payload of an input to arithmetic circuit.
To be used as an argument to compileWith
.
guessOutput :: (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Binary (Rep o)) => (Ord (Rep i), Ord (Rep o), NFData (Rep i), NFData (Rep o)) => (Representable i, Representable o, Foldable o) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p (i :*: o) U1 Source #
eval :: (Arithmetic a, Representable p, Representable i, Functor o) => ArithmeticCircuit a p i o -> p a -> i a -> o a Source #
Evaluates the arithmetic circuit using the supplied input map.
eval1 :: (Arithmetic a, Representable p, Representable i) => ArithmeticCircuit a p i Par1 -> p a -> i a -> a Source #
Evaluates the arithmetic circuit with one output using the supplied input map.
exec :: (Arithmetic a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a Source #
Evaluates the arithmetic circuit with no inputs.
exec1 :: Arithmetic a => ArithmeticCircuit a U1 U1 Par1 -> a Source #
Evaluates the arithmetic circuit with no inputs and one output.
acSizeN :: ArithmeticCircuit a p i o -> Natural Source #
Calculates the number of constraints in the system.
acSizeM :: ArithmeticCircuit a p i o -> Natural Source #
Calculates the number of variables in the system.
acSizeR :: ArithmeticCircuit a p i o -> Natural Source #
Calculates the number of range lookups in the system.
acSystem :: ArithmeticCircuit a p i o -> Map ByteString (Constraint a i) Source #
The system of polynomial constraints
acValue :: (Arithmetic a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a Source #
acPrint :: (Arithmetic a, Show a, Show (o (Var a U1)), Show (o a), Functor o) => ArithmeticCircuit a U1 U1 o -> IO () Source #
Prints the constraint system, the witness, and the output.
TODO: Move this elsewhere (?) TODO: Check that all arguments have been applied.
hlmap :: (Representable i, Representable j, Ord (Rep j), Functor o) => (forall x. j x -> i x) -> ArithmeticCircuit a p i o -> ArithmeticCircuit a p j o Source #
hpmap :: (Representable p, Representable q) => (forall x. q x -> p x) -> ArithmeticCircuit a p i o -> ArithmeticCircuit a q i o Source #
mapVarArithmeticCircuit :: (Field a, Eq a, Functor o, Ord (Rep i), Representable i, Foldable i) => ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o Source #
acWitness :: ArithmeticCircuit a p i o -> Map ByteString (WitnessF a (WitVar p i)) Source #
The witness generation functions
acInput :: Representable i => i (Var a i) Source #
acOutput :: ArithmeticCircuit a p i o -> o (Var a i) Source #
The output variables
checkCircuit :: Arbitrary (p a) => Arbitrary (i a) => Arithmetic a => Show a => Representable p => Representable i => ArithmeticCircuit a p i o -> Property Source #
checkClosedCircuit :: forall a o. Arithmetic a => Show a => ArithmeticCircuit a U1 U1 o -> Property Source #
isConstantInput :: (Arithmetic a, Show a, Representable p, Representable i, Show (p a), Show (i a), Arbitrary (p a), Arbitrary (i a)) => ArithmeticCircuit a p i o -> Property Source #