symbolic-base-0.1.0.0: ZkFold Symbolic compiler and zero-knowledge proof protocols
Safe HaskellSafe-Inferred
LanguageHaskell2010

ZkFold.Symbolic.Compiler.ArithmeticCircuit

Synopsis

Documentation

data ArithmeticCircuit a p i o Source #

Arithmetic circuit in the form of a system of polynomial constraints.

Instances

Instances details
(Ord (Rep i), Ord a) => HApplicative (ArithmeticCircuit a p i :: (Type -> Type) -> Type) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

hpure :: (forall (a0 :: k). f a0) -> ArithmeticCircuit a p i f Source #

hunit :: ArithmeticCircuit a p i U1 Source #

hap :: forall (f :: k -> Type) (g :: k -> Type). ArithmeticCircuit a p i (Transform f g) -> ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g Source #

hliftA2 :: (forall (a0 :: k). f a0 -> g a0 -> h a0) -> ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g -> ArithmeticCircuit a p i h Source #

hpair :: forall (f :: k -> Type) (g :: k -> Type). ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g -> ArithmeticCircuit a p i (f :*: g) Source #

HFunctor (ArithmeticCircuit a p i :: (Type -> Type) -> Type) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

hmap :: (forall (a0 :: k). f a0 -> g a0) -> ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g Source #

(Ord (Rep i), Ord a) => Package (ArithmeticCircuit a p i :: (Type -> Type) -> Type) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

unpack :: forall f (g :: k1 -> Type). Functor f => ArithmeticCircuit a p i (f :.: g) -> f (ArithmeticCircuit a p i g) Source #

unpackWith :: Functor f => (forall (a0 :: k1). h a0 -> f (g a0)) -> ArithmeticCircuit a p i h -> f (ArithmeticCircuit a p i g) Source #

pack :: forall f (g :: k1 -> Type). (Foldable f, Functor f) => f (ArithmeticCircuit a p i g) -> ArithmeticCircuit a p i (f :.: g) Source #

packWith :: (Foldable f, Functor f) => (forall (a0 :: k1). f (g a0) -> h a0) -> f (ArithmeticCircuit a p i g) -> ArithmeticCircuit a p i h Source #

(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), o ~ (U1 :: Type -> Type)) => MonadCircuit (Var a i) a (WitnessF a (WitVar p i)) (State (ArithmeticCircuit a p i o)) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

unconstrained :: WitnessF a (WitVar p i) -> State (ArithmeticCircuit a p i o) (Var a i) Source #

constraint :: ClosedPoly (Var a i) a -> State (ArithmeticCircuit a p i o) () Source #

rangeConstraint :: Var a i -> a -> State (ArithmeticCircuit a p i o) () Source #

newAssigned :: ClosedPoly (Var a i) a -> State (ArithmeticCircuit a p i o) (Var a i) 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 #

(Arithmetic a, Arbitrary a, Binary a, Binary (Rep p), Arbitrary (Rep i), Binary (Rep i), Ord (Rep i), NFData (Rep i), Representable i, Foldable i) => Arbitrary (ArithmeticCircuit a p i Par1) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance

(Arithmetic a, Arbitrary a, Binary a, Binary (Rep p), Arbitrary (Rep i), Binary (Rep i), Ord (Rep i), NFData (Rep i), Representable i, Foldable i, KnownNat l) => Arbitrary (ArithmeticCircuit a p i (Vector l)) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance

(FromJSON a, FromJSON (o (Var a i)), ToJSONKey (Var a i), FromJSONKey a, Ord a, Ord (Rep i), FromJSON (Rep i)) => FromJSON (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance

(ToJSON a, ToJSON (o (Var a i)), ToJSONKey a, FromJSONKey (Var a i), ToJSON (Rep i)) => ToJSON (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance

(Ord a, Ord (Rep i), o ~ (U1 :: Type -> Type)) => Monoid (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

mempty :: ArithmeticCircuit a p i o #

mappend :: ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o #

mconcat :: [ArithmeticCircuit a p i o] -> ArithmeticCircuit a p i o #

(Ord a, Ord (Rep i), o ~ (U1 :: Type -> Type)) => Semigroup (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

(<>) :: ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o #

sconcat :: NonEmpty (ArithmeticCircuit a p i o) -> ArithmeticCircuit a p i o #

stimes :: Integral b => b -> ArithmeticCircuit a p i o -> ArithmeticCircuit a p i o #

Generic (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Associated Types

type Rep (ArithmeticCircuit a p i o) :: Type -> Type #

Methods

from :: ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x #

to :: Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o #

(FiniteField a, Eq a, Show a, Show (o (Var a i)), Ord (Rep i), Show (Var a i), Show (Rep i)) => Show (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance

Methods

showsPrec :: Int -> ArithmeticCircuit a p i o -> ShowS #

show :: ArithmeticCircuit a p i o -> String #

showList :: [ArithmeticCircuit a p i o] -> ShowS #

(NFData a, NFData (o (Var a i)), NFData (Rep i)) => NFData (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

rnf :: ArithmeticCircuit a p i o -> () #

type BaseField (ArithmeticCircuit a p i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

type BaseField (ArithmeticCircuit a p i) = a
type WitnessField (ArithmeticCircuit a p i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

type Rep (ArithmeticCircuit a p i o) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

type Rep (ArithmeticCircuit a p i o) = D1 ('MetaData "ArithmeticCircuit" "ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal" "symbolic-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "ArithmeticCircuit" 'PrefixI 'True) ((S1 ('MetaSel ('Just "acSystem") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ByteString (Constraint a i))) :*: S1 ('MetaSel ('Just "acRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (MonoidalMap a (Set (SysVar i))))) :*: (S1 ('MetaSel ('Just "acWitness") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map ByteString (WitnessF a (WitVar p i)))) :*: S1 ('MetaSel ('Just "acOutput") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (o (Var a i))))))

type Constraint c i = Poly c (SysVar i) Natural Source #

The type that represents a constraint in the arithmetic circuit.

data Var a i Source #

Instances

Instances details
FromConstant a (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

fromConstant :: a -> Var a i Source #

(FromJSON (Rep i), FromJSON a) => FromJSON (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

parseJSON :: Value -> Parser (Var a i) #

parseJSONList :: Value -> Parser [Var a i] #

(FromJSON (Rep i), FromJSON a) => FromJSONKey (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

(ToJSON (Rep i), ToJSON a) => ToJSON (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

toJSON :: Var a i -> Value #

toEncoding :: Var a i -> Encoding #

toJSONList :: [Var a i] -> Value #

toEncodingList :: [Var a i] -> Encoding #

(ToJSON (Rep i), ToJSON a) => ToJSONKey (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Generic (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Associated Types

type Rep (Var a i) :: Type -> Type #

Methods

from :: Var a i -> Rep (Var a i) x #

to :: Rep (Var a i) x -> Var a i #

(Show (Rep i), Show a) => Show (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

showsPrec :: Int -> Var a i -> ShowS #

show :: Var a i -> String #

showList :: [Var a i] -> ShowS #

(NFData (Rep i), NFData a) => NFData (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

rnf :: Var a i -> () #

(Eq (Rep i), Eq a) => Eq (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

(==) :: Var a i -> Var a i -> Bool #

(/=) :: Var a i -> Var a i -> Bool #

(Ord (Rep i), Ord a) => Ord (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

compare :: Var a i -> Var a i -> Ordering #

(<) :: Var a i -> Var a i -> Bool #

(<=) :: Var a i -> Var a i -> Bool #

(>) :: Var a i -> Var a i -> Bool #

(>=) :: Var a i -> Var a i -> Bool #

max :: Var a i -> Var a i -> Var a i #

min :: Var a i -> Var a i -> Var a i #

(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), o ~ (U1 :: Type -> Type)) => MonadCircuit (Var a i) a (WitnessF a (WitVar p i)) (State (ArithmeticCircuit a p i o)) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

unconstrained :: WitnessF a (WitVar p i) -> State (ArithmeticCircuit a p i o) (Var a i) Source #

constraint :: ClosedPoly (Var a i) a -> State (ArithmeticCircuit a p i o) () Source #

rangeConstraint :: Var a i -> a -> State (ArithmeticCircuit a p i o) () Source #

newAssigned :: ClosedPoly (Var a i) a -> State (ArithmeticCircuit a p i o) (Var a i) Source #

Finite a => Witness (Var a i) (WitnessF a (WitVar p i)) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

Methods

at :: Var a i -> WitnessF a (WitVar p i) Source #

type Rep (Var a i) Source # 
Instance details

Defined in ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

type Rep (Var a i) = D1 ('MetaData "Var" "ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal" "symbolic-base-0.1.0.0-inplace" 'False) (C1 ('MetaCons "SysVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SysVar i))) :+: C1 ('MetaCons "ConstVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

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

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

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 #

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