{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE NoStarIsType         #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (
        ArithmeticCircuit(..),
        CircuitFold (..),
        Var (..),
        SysVar (..),
        WitVar (..),
        VarField,
        Arithmetic,
        Constraint,
        -- variable getters and setters
        acInput,
        getAllVars,
        crown,
        -- input mapping
        hlmap,
        hpmap,
        -- evaluation functions
        witnessGenerator,
        eval,
        eval1,
        exec,
        exec1,
        apply,
        indexW,
        witToVar
    ) where

import           Control.DeepSeq                                              (NFData (..), NFData1 (..))
import           Control.Monad.State                                          (State, modify, runState)
import           Data.Bifunctor                                               (Bifunctor (..))
import           Data.Binary                                                  (Binary)
import           Data.ByteString                                              (ByteString)
import           Data.Foldable                                                (fold, toList)
import           Data.Functor.Rep
import           Data.List.Infinite                                           (Infinite)
import           Data.Map.Monoidal                                            (MonoidalMap, insertWith)
import           Data.Map.Strict                                              hiding (drop, foldl, foldr, insertWith,
                                                                               map, null, splitAt, take, toList)
import           Data.Maybe                                                   (catMaybes, fromMaybe)
import           Data.Semialign                                               (unzipDefault)
import           Data.Semigroup.Generic                                       (GenericSemigroupMonoid (..))
import qualified Data.Set                                                     as S
import           GHC.Generics                                                 (Generic, Par1 (..), U1 (..), (:*:) (..))
import           Optics                                                       hiding (at)
import           Prelude                                                      hiding (Num (..), drop, length, product,
                                                                               splitAt, sum, take, (!!), (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field                              (Zp)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.Polynomials.Multivariate                 (Poly, evalMonomial, evalPolynomial,
                                                                               mapVars, var)
import           ZkFold.Base.Control.HApplicative
import           ZkFold.Base.Data.HFunctor
import           ZkFold.Base.Data.Package
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.MerkleHash
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Var
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Witness
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.WitnessEstimation
import           ZkFold.Symbolic.MonadCircuit

-- | The type that represents a constraint in the arithmetic circuit.
type Constraint c i = Poly c (SysVar i) Natural

type CircuitWitness a p i = WitnessF a (WitVar p i)

data CircuitFold a v w =
  forall s j.
  ( Functor s, NFData1 s, Binary (Rep s), NFData (Rep s), Ord (Rep s)
  , Functor j, Binary (Rep j), NFData (Rep j), Ord (Rep j)) =>
    CircuitFold
      { ()
foldStep   :: ArithmeticCircuit a U1 (j :*: s) s
      , ()
foldSeed   :: s v
      , ()
foldStream :: Infinite (j w)
      , forall a v w. CircuitFold a v w -> v
foldCount  :: v
      , ()
foldResult :: s v
      }

instance Functor (CircuitFold a v) where
  fmap :: forall a b. (a -> b) -> CircuitFold a v a -> CircuitFold a v b
fmap = (a -> b) -> CircuitFold a v a -> CircuitFold a v b
forall b c a. (b -> c) -> CircuitFold a a b -> CircuitFold a a c
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second

instance Bifunctor (CircuitFold a) where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> CircuitFold a a c -> CircuitFold a b d
bimap a -> b
f c -> d
g CircuitFold {a
s a
Infinite (j c)
ArithmeticCircuit a U1 (j :*: s) s
foldStep :: ()
foldSeed :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldResult :: ()
foldStep :: ArithmeticCircuit a U1 (j :*: s) s
foldSeed :: s a
foldStream :: Infinite (j c)
foldCount :: a
foldResult :: s a
..} = CircuitFold
    { foldStep :: ArithmeticCircuit a U1 (j :*: s) s
foldStep = ArithmeticCircuit a U1 (j :*: s) s
foldStep
    , foldSeed :: s b
foldSeed = a -> b
f (a -> b) -> s a -> s b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> s a
foldSeed
    , foldStream :: Infinite (j d)
foldStream = (c -> d) -> j c -> j d
forall a b. (a -> b) -> j a -> j b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> d
g (j c -> j d) -> Infinite (j c) -> Infinite (j d)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Infinite (j c)
foldStream
    , foldCount :: b
foldCount = a -> b
f a
foldCount
    , foldResult :: s b
foldResult = a -> b
f (a -> b) -> s a -> s b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> s a
foldResult
    }

instance (NFData a, NFData v) => NFData (CircuitFold a v w) where
  rnf :: CircuitFold a v w -> ()
rnf CircuitFold {v
s v
Infinite (j w)
ArithmeticCircuit a U1 (j :*: s) s
foldStep :: ()
foldSeed :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldResult :: ()
foldStep :: ArithmeticCircuit a U1 (j :*: s) s
foldSeed :: s v
foldStream :: Infinite (j w)
foldCount :: v
foldResult :: s v
..} =
    (ArithmeticCircuit a U1 (j :*: s) s, v) -> ()
forall a. NFData a => a -> ()
rnf (ArithmeticCircuit a U1 (j :*: s) s
foldStep, v
foldCount)
      () -> () -> ()
forall a b. a -> b -> b
`seq` (v -> ()) -> s v -> ()
forall a. (a -> ()) -> s a -> ()
forall (f :: Type -> Type) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf v -> ()
forall a. NFData a => a -> ()
rnf s v
foldSeed
      () -> () -> ()
forall a b. a -> b -> b
`seq` (v -> ()) -> s v -> ()
forall a. (a -> ()) -> s a -> ()
forall (f :: Type -> Type) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf v -> ()
forall a. NFData a => a -> ()
rnf s v
foldResult

-- | Arithmetic circuit in the form of a system of polynomial constraints.
data ArithmeticCircuit a p i o = ArithmeticCircuit
    {
        forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> Map ByteString (Constraint a i)
acSystem  :: Map ByteString (Constraint a i),
        -- ^ The system of polynomial constraints
        forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> MonoidalMap a (Set (SysVar i))
acRange   :: MonoidalMap a (S.Set (SysVar i)),
        -- ^ The range constraints [0, a] for the selected variables
        forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
acWitness :: Map ByteString (CircuitWitness a p i),
        -- ^ The witness generation functions
        forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o
-> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
acFold    :: Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i)),
        -- ^ The set of folding operations
        forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput  :: o (Var a i)
        -- ^ The output variables
    } deriving ((forall x.
 ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x)
-> (forall x.
    Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o)
-> Generic (ArithmeticCircuit a p i o)
forall x.
Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o
forall x.
ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type) x.
Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type) x.
ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x
$cfrom :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type) x.
ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x
from :: forall x.
ArithmeticCircuit a p i o -> Rep (ArithmeticCircuit a p i o) x
$cto :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type) x.
Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o
to :: forall x.
Rep (ArithmeticCircuit a p i o) x -> ArithmeticCircuit a p i o
Generic)

deriving via (GenericSemigroupMonoid (ArithmeticCircuit a p i o))
  instance (Ord a, Ord (Rep i), o ~ U1) => Semigroup (ArithmeticCircuit a p i o)

deriving via (GenericSemigroupMonoid (ArithmeticCircuit a p i o))
  instance (Ord a, Ord (Rep i), o ~ U1) => Monoid (ArithmeticCircuit a p i o)

instance (NFData a, NFData1 o, NFData (Rep i))
    => NFData (ArithmeticCircuit a p i o) where
  rnf :: ArithmeticCircuit a p i o -> ()
rnf (ArithmeticCircuit Map ByteString (Constraint a i)
s MonoidalMap a (Set (SysVar i))
r Map ByteString (CircuitWitness a p i)
w Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
f o (Var a i)
o) = (Map ByteString (Constraint a i), MonoidalMap a (Set (SysVar i)),
 Map ByteString (CircuitWitness a p i),
 Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i)))
-> ()
forall a. NFData a => a -> ()
rnf (Map ByteString (Constraint a i)
s, MonoidalMap a (Set (SysVar i))
r, Map ByteString (CircuitWitness a p i)
w, Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
f) () -> () -> ()
forall a b. a -> b -> b
`seq` (Var a i -> ()) -> o (Var a i) -> ()
forall a. (a -> ()) -> o a -> ()
forall (f :: Type -> Type) a. NFData1 f => (a -> ()) -> f a -> ()
liftRnf Var a i -> ()
forall a. NFData a => a -> ()
rnf o (Var a i)
o

-- | Variables are SHA256 digests (32 bytes)
type VarField = Zp (2 ^ (32 * 8))

data WitVar p i
  = WExVar (Rep p)
  | WSysVar (SysVar i)

imapWitVar ::
  (Representable i, Representable j) =>
  (forall x. j x -> i x) -> WitVar p i -> WitVar p j
imapWitVar :: forall (i :: Type -> Type) (j :: Type -> Type) (p :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> WitVar p i -> WitVar p j
imapWitVar forall x. j x -> i x
_ (WExVar Rep p
r)  = Rep p -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type). Rep p -> WitVar p i
WExVar Rep p
r
imapWitVar forall x. j x -> i x
f (WSysVar SysVar i
v) = SysVar j -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar ((forall x. j x -> i x) -> SysVar i -> SysVar j
forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar j x -> i x
forall x. j x -> i x
f SysVar i
v)

pmapWitVar ::
  (Representable p, Representable q) =>
  (forall x. q x -> p x) -> WitVar p i -> WitVar q i
pmapWitVar :: forall (p :: Type -> Type) (q :: Type -> Type) (i :: Type -> Type).
(Representable p, Representable q) =>
(forall x. q x -> p x) -> WitVar p i -> WitVar q i
pmapWitVar forall x. q x -> p x
f (WExVar Rep p
r)  = p (WitVar q i) -> Rep p -> WitVar q i
forall a. p a -> Rep p -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index (q (WitVar q i) -> p (WitVar q i)
forall x. q x -> p x
f ((Rep q -> WitVar q i) -> q (WitVar q i)
forall a. (Rep q -> a) -> q a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep q -> WitVar q i
forall (p :: Type -> Type) (i :: Type -> Type). Rep p -> WitVar p i
WExVar)) Rep p
r
pmapWitVar forall x. q x -> p x
_ (WSysVar SysVar i
v) = SysVar i -> WitVar q i
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar SysVar i
v

---------------------------------- Variables -----------------------------------

acInput :: (Representable i, Semiring a) => i (Var a i)
acInput :: forall (i :: Type -> Type) a.
(Representable i, Semiring a) =>
i (Var a i)
acInput = (Rep i -> Var a i) -> i (Rep i) -> i (Var a i)
forall (f :: Type -> Type) a b.
Representable f =>
(a -> b) -> f a -> f b
fmapRep (SysVar i -> Var a i
forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar (SysVar i -> Var a i) -> (Rep i -> SysVar i) -> Rep i -> Var a i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep i -> SysVar i
forall (i :: Type -> Type). Rep i -> SysVar i
InVar) ((Rep i -> Rep i) -> i (Rep i)
forall a. (Rep i -> a) -> i a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep i -> Rep i
forall a. a -> a
id)

getAllVars :: forall a p i o. (Representable i, Foldable i) => ArithmeticCircuit a p i o -> [SysVar i]
getAllVars :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Representable i, Foldable i) =>
ArithmeticCircuit a p i o -> [SysVar i]
getAllVars ArithmeticCircuit a p i o
ac = i (SysVar i) -> [SysVar i]
forall a. i a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList i (SysVar i)
acInput0 [SysVar i] -> [SysVar i] -> [SysVar i]
forall a. [a] -> [a] -> [a]
++ (ByteString -> SysVar i) -> [ByteString] -> [SysVar i]
forall a b. (a -> b) -> [a] -> [b]
map ByteString -> SysVar i
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar (Map ByteString (CircuitWitness a p i) -> [ByteString]
forall k a. Map k a -> [k]
keys (Map ByteString (CircuitWitness a p i) -> [ByteString])
-> Map ByteString (CircuitWitness a p i) -> [ByteString]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
acWitness ArithmeticCircuit a p i o
ac) where
  acInput0 :: i (SysVar i)
  acInput0 :: i (SysVar i)
acInput0 = (Rep i -> SysVar i) -> i (Rep i) -> i (SysVar i)
forall (f :: Type -> Type) a b.
Representable f =>
(a -> b) -> f a -> f b
fmapRep Rep i -> SysVar i
forall (i :: Type -> Type). Rep i -> SysVar i
InVar (forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate @i Rep i -> Rep i
forall a. a -> a
id)

indexW ::
  (Arithmetic a, Representable p, Representable i) =>
  ArithmeticCircuit a p i o -> p a -> i a -> Var a i -> a
indexW :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Var a i -> a
indexW ArithmeticCircuit a p i o
circuit p a
payload i a
inputs = \case
  LinVar a
k (InVar Rep i
inV) a
b -> (\a
t -> a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
t a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
b) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ i a -> Rep i -> a
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index i a
inputs Rep i
inV
  LinVar a
k (NewVar ByteString
newV) a
b -> (\a
t -> a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
t a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
b) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe
    ([Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"no such NewVar: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ByteString -> [Char]
forall a. Show a => a -> [Char]
show ByteString
newV))
    (ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a
witnessGenerator ArithmeticCircuit a p i o
circuit p a
payload i a
inputs Map ByteString a -> ByteString -> Maybe a
forall k a. Ord k => Map k a -> k -> Maybe a
!? ByteString
newV)
  ConstVar a
cV -> a
cV

-------------------------------- "HProfunctor" ---------------------------------

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
hlmap :: forall (i :: Type -> Type) (j :: Type -> Type) (o :: Type -> Type)
       a (p :: Type -> Type).
(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
hlmap forall x. j x -> i x
f (ArithmeticCircuit Map ByteString (Constraint a i)
s MonoidalMap a (Set (SysVar i))
r Map ByteString (CircuitWitness a p i)
w Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
d o (Var a i)
o) = ArithmeticCircuit
  { acSystem :: Map ByteString (Constraint a j)
acSystem = (SysVar i -> SysVar j) -> Constraint a i -> Constraint a j
forall i2 i1 c j.
Variable i2 =>
(i1 -> i2) -> Poly c i1 j -> Poly c i2 j
mapVars ((forall x. j x -> i x) -> SysVar i -> SysVar j
forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar j x -> i x
forall x. j x -> i x
f) (Constraint a i -> Constraint a j)
-> Map ByteString (Constraint a i)
-> Map ByteString (Constraint a j)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map ByteString (Constraint a i)
s
  , acRange :: MonoidalMap a (Set (SysVar j))
acRange = (SysVar i -> SysVar j) -> Set (SysVar i) -> Set (SysVar j)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map ((forall x. j x -> i x) -> SysVar i -> SysVar j
forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar j x -> i x
forall x. j x -> i x
f) (Set (SysVar i) -> Set (SysVar j))
-> MonoidalMap a (Set (SysVar i)) -> MonoidalMap a (Set (SysVar j))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MonoidalMap a (Set (SysVar i))
r
  , acWitness :: Map ByteString (CircuitWitness a p j)
acWitness = (WitVar p i -> WitVar p j)
-> CircuitWitness a p i -> CircuitWitness a p j
forall a b. (a -> b) -> WitnessF a a -> WitnessF a b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall x. j x -> i x) -> WitVar p i -> WitVar p j
forall (i :: Type -> Type) (j :: Type -> Type) (p :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> WitVar p i -> WitVar p j
imapWitVar j x -> i x
forall x. j x -> i x
f) (CircuitWitness a p i -> CircuitWitness a p j)
-> Map ByteString (CircuitWitness a p i)
-> Map ByteString (CircuitWitness a p j)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map ByteString (CircuitWitness a p i)
w
  , acFold :: Map ByteString (CircuitFold a (Var a j) (CircuitWitness a p j))
acFold = (Var a i -> Var a j)
-> (CircuitWitness a p i -> CircuitWitness a p j)
-> CircuitFold a (Var a i) (CircuitWitness a p i)
-> CircuitFold a (Var a j) (CircuitWitness a p j)
forall a b c d.
(a -> b) -> (c -> d) -> CircuitFold a a c -> CircuitFold a b d
forall (p :: Type -> Type -> Type) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((forall x. j x -> i x) -> Var a i -> Var a j
forall (i :: Type -> Type) (j :: Type -> Type) a.
(Representable i, Representable j) =>
(forall x. j x -> i x) -> Var a i -> Var a j
imapVar j x -> i x
forall x. j x -> i x
f) ((forall x. j x -> i x) -> WitVar p i -> WitVar p j
forall (i :: Type -> Type) (j :: Type -> Type) (p :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> WitVar p i -> WitVar p j
imapWitVar j x -> i x
forall x. j x -> i x
f (WitVar p i -> WitVar p j)
-> CircuitWitness a p i -> CircuitWitness a p j
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>) (CircuitFold a (Var a i) (CircuitWitness a p i)
 -> CircuitFold a (Var a j) (CircuitWitness a p j))
-> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
-> Map ByteString (CircuitFold a (Var a j) (CircuitWitness a p j))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
d
  , acOutput :: o (Var a j)
acOutput = (forall x. j x -> i x) -> Var a i -> Var a j
forall (i :: Type -> Type) (j :: Type -> Type) a.
(Representable i, Representable j) =>
(forall x. j x -> i x) -> Var a i -> Var a j
imapVar j x -> i x
forall x. j x -> i x
f (Var a i -> Var a j) -> o (Var a i) -> o (Var a j)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> o (Var a i)
o
  }

hpmap ::
  (Representable p, Representable q) => (forall x. q x -> p x) ->
  ArithmeticCircuit a p i o -> ArithmeticCircuit a q i o
hpmap :: forall (p :: Type -> Type) (q :: Type -> Type) a
       (i :: Type -> Type) (o :: Type -> Type).
(Representable p, Representable q) =>
(forall x. q x -> p x)
-> ArithmeticCircuit a p i o -> ArithmeticCircuit a q i o
hpmap forall x. q x -> p x
f ArithmeticCircuit a p i o
ac = ArithmeticCircuit a p i o
ac
  { acWitness = fmap (pmapWitVar f) <$> acWitness ac
  , acFold = fmap (pmapWitVar f <$>) <$> acFold ac
  }

--------------------------- Symbolic compiler context --------------------------

crown :: ArithmeticCircuit a p i g -> f (Var a i) -> ArithmeticCircuit a p i f
crown :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (g :: Type -> Type) (f :: Type -> Type).
ArithmeticCircuit a p i g
-> f (Var a i) -> ArithmeticCircuit a p i f
crown = (f (Var a i)
 -> ArithmeticCircuit a p i g -> ArithmeticCircuit a p i f)
-> ArithmeticCircuit a p i g
-> f (Var a i)
-> ArithmeticCircuit a p i f
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i g)
  (ArithmeticCircuit a p i f)
  (g (Var a i))
  (f (Var a i))
-> f (Var a i)
-> ArithmeticCircuit a p i g
-> ArithmeticCircuit a p i f
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i g)
  (ArithmeticCircuit a p i f)
  (g (Var a i))
  (f (Var a i))
#acOutput)

behead :: ArithmeticCircuit a p i f -> (ArithmeticCircuit a p i U1, f (Var a i))
behead :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead = (ArithmeticCircuit a p i U1
 -> f (Var a i) -> (ArithmeticCircuit a p i U1, f (Var a i)))
-> (ArithmeticCircuit a p i f -> ArithmeticCircuit a p i U1)
-> (ArithmeticCircuit a p i f -> f (Var a i))
-> ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
forall a b c.
(a -> b -> c)
-> (ArithmeticCircuit a p i f -> a)
-> (ArithmeticCircuit a p i f -> b)
-> ArithmeticCircuit a p i f
-> c
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i f)
  (ArithmeticCircuit a p i U1)
  (f (Var a i))
  (U1 (Var a i))
-> U1 (Var a i)
-> ArithmeticCircuit a p i f
-> ArithmeticCircuit a p i U1
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i f)
  (ArithmeticCircuit a p i U1)
  (f (Var a i))
  (U1 (Var a i))
#acOutput U1 (Var a i)
forall k (p :: k). U1 p
U1) ArithmeticCircuit a p i f -> f (Var a i)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput

instance HFunctor (ArithmeticCircuit a p i) where
    hmap :: forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a)
-> ArithmeticCircuit a p i f -> ArithmeticCircuit a p i g
hmap = Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i f)
  (ArithmeticCircuit a p i g)
  (f (Var a i))
  (g (Var a i))
-> (f (Var a i) -> g (Var a i))
-> ArithmeticCircuit a p i f
-> ArithmeticCircuit a p i g
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i f)
  (ArithmeticCircuit a p i g)
  (f (Var a i))
  (g (Var a i))
#acOutput

instance (Ord (Rep i), Ord a) => HApplicative (ArithmeticCircuit a p i) where
    hpure :: forall (f :: Type -> Type).
(forall a. f a) -> ArithmeticCircuit a p i f
hpure = ArithmeticCircuit a p i U1
-> f (Var a i) -> ArithmeticCircuit a p i f
forall a (p :: Type -> Type) (i :: Type -> Type)
       (g :: Type -> Type) (f :: Type -> Type).
ArithmeticCircuit a p i g
-> f (Var a i) -> ArithmeticCircuit a p i f
crown ArithmeticCircuit a p i U1
forall a. Monoid a => a
mempty
    hliftA2 :: forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type).
(forall a. f a -> g a -> h a)
-> ArithmeticCircuit a p i f
-> ArithmeticCircuit a p i g
-> ArithmeticCircuit a p i h
hliftA2 forall a. f a -> g a -> h a
f (ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (ArithmeticCircuit a p i U1
c, f (Var a i)
o)) (ArithmeticCircuit a p i g
-> (ArithmeticCircuit a p i U1, g (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (ArithmeticCircuit a p i U1
d, g (Var a i)
p)) = ArithmeticCircuit a p i U1
-> h (Var a i) -> ArithmeticCircuit a p i h
forall a (p :: Type -> Type) (i :: Type -> Type)
       (g :: Type -> Type) (f :: Type -> Type).
ArithmeticCircuit a p i g
-> f (Var a i) -> ArithmeticCircuit a p i f
crown (ArithmeticCircuit a p i U1
c ArithmeticCircuit a p i U1
-> ArithmeticCircuit a p i U1 -> ArithmeticCircuit a p i U1
forall a. Semigroup a => a -> a -> a
<> ArithmeticCircuit a p i U1
d) (f (Var a i) -> g (Var a i) -> h (Var a i)
forall a. f a -> g a -> h a
f f (Var a i)
o g (Var a i)
p)

instance (Ord (Rep i), Ord a) => Package (ArithmeticCircuit a p i) where
    unpackWith :: forall (f :: Type -> Type) (h :: Type -> Type) (g :: Type -> Type).
Functor f =>
(forall a. h a -> f (g a))
-> ArithmeticCircuit a p i h -> f (ArithmeticCircuit a p i g)
unpackWith forall a. h a -> f (g a)
f (ArithmeticCircuit a p i h
-> (ArithmeticCircuit a p i U1, h (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (ArithmeticCircuit a p i U1
c, h (Var a i)
o)) = ArithmeticCircuit a p i U1
-> g (Var a i) -> ArithmeticCircuit a p i g
forall a (p :: Type -> Type) (i :: Type -> Type)
       (g :: Type -> Type) (f :: Type -> Type).
ArithmeticCircuit a p i g
-> f (Var a i) -> ArithmeticCircuit a p i f
crown ArithmeticCircuit a p i U1
c (g (Var a i) -> ArithmeticCircuit a p i g)
-> f (g (Var a i)) -> f (ArithmeticCircuit a p i g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> h (Var a i) -> f (g (Var a i))
forall a. h a -> f (g a)
f h (Var a i)
o
    packWith :: forall (f :: Type -> Type) (g :: Type -> Type) (h :: Type -> Type).
(Foldable f, Functor f) =>
(forall a. f (g a) -> h a)
-> f (ArithmeticCircuit a p i g) -> ArithmeticCircuit a p i h
packWith forall a. f (g a) -> h a
f (f (ArithmeticCircuit a p i U1, g (Var a i))
-> (f (ArithmeticCircuit a p i U1), f (g (Var a i)))
forall (f :: Type -> Type) a b. Functor f => f (a, b) -> (f a, f b)
unzipDefault (f (ArithmeticCircuit a p i U1, g (Var a i))
 -> (f (ArithmeticCircuit a p i U1), f (g (Var a i))))
-> (f (ArithmeticCircuit a p i g)
    -> f (ArithmeticCircuit a p i U1, g (Var a i)))
-> f (ArithmeticCircuit a p i g)
-> (f (ArithmeticCircuit a p i U1), f (g (Var a i)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArithmeticCircuit a p i g
 -> (ArithmeticCircuit a p i U1, g (Var a i)))
-> f (ArithmeticCircuit a p i g)
-> f (ArithmeticCircuit a p i U1, g (Var a i))
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ArithmeticCircuit a p i g
-> (ArithmeticCircuit a p i U1, g (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (f (ArithmeticCircuit a p i U1)
cs, f (g (Var a i))
os)) = ArithmeticCircuit a p i U1
-> h (Var a i) -> ArithmeticCircuit a p i h
forall a (p :: Type -> Type) (i :: Type -> Type)
       (g :: Type -> Type) (f :: Type -> Type).
ArithmeticCircuit a p i g
-> f (Var a i) -> ArithmeticCircuit a p i f
crown (f (ArithmeticCircuit a p i U1) -> ArithmeticCircuit a p i U1
forall m. Monoid m => f m -> m
forall (t :: Type -> Type) m. (Foldable t, Monoid m) => t m -> m
fold f (ArithmeticCircuit a p i U1)
cs) (f (g (Var a i)) -> h (Var a i)
forall a. f (g a) -> h a
f f (g (Var a i))
os)

instance
  (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), NFData (Rep i)) =>
  Symbolic (ArithmeticCircuit a p i) where
    type BaseField (ArithmeticCircuit a p i) = a
    type WitnessField (ArithmeticCircuit a p i) = WitnessF a (WitVar p i)
    witnessF :: forall (f :: Type -> Type).
Functor f =>
ArithmeticCircuit a p i f
-> f (WitnessField (ArithmeticCircuit a p i))
witnessF (ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (ArithmeticCircuit a p i U1
_, f (Var a i)
o)) = Var a i -> WitnessF a (WitVar p i)
forall i w. Witness i w => i -> w
at (Var a i -> WitnessF a (WitVar p i))
-> f (Var a i) -> f (WitnessF a (WitVar p i))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Var a i)
o
    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
fromCircuitF (ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (f :: Type -> Type).
ArithmeticCircuit a p i f
-> (ArithmeticCircuit a p i U1, f (Var a i))
behead -> (ArithmeticCircuit a p i U1
c, f (Var a i)
o)) CircuitFun '[f] g (ArithmeticCircuit a p i)
f = (g (Var a i)
 -> ArithmeticCircuit a p i U1 -> ArithmeticCircuit a p i g)
-> (g (Var a i), ArithmeticCircuit a p i U1)
-> ArithmeticCircuit a p i g
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (ArithmeticCircuit a p i g)
  (U1 (Var a i))
  (g (Var a i))
-> g (Var a i)
-> ArithmeticCircuit a p i U1
-> ArithmeticCircuit a p i g
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (ArithmeticCircuit a p i g)
  (U1 (Var a i))
  (g (Var a i))
#acOutput) (State (ArithmeticCircuit a p i U1) (g (Var a i))
-> ArithmeticCircuit a p i U1
-> (g (Var a i), ArithmeticCircuit a p i U1)
forall s a. State s a -> s -> (a, s)
runState (FunBody
  '[f] g (Var a i) (StateT (ArithmeticCircuit a p i U1) Identity)
f (Var a i) -> State (ArithmeticCircuit a p i U1) (g (Var a i))
CircuitFun '[f] g (ArithmeticCircuit a p i)
f f (Var a i)
o) ArithmeticCircuit a p i U1
c)

----------------------------- MonadCircuit instance ----------------------------

instance Finite a => Witness (Var a i) (CircuitWitness a p i) where
  at :: Var a i -> CircuitWitness a p i
at (ConstVar a
cV)   = a -> CircuitWitness a p i
forall a b. FromConstant a b => a -> b
fromConstant a
cV
  at (LinVar a
k SysVar i
sV a
b) = a -> CircuitWitness a p i
forall a b. FromConstant a b => a -> b
fromConstant a
k CircuitWitness a p i
-> CircuitWitness a p i -> CircuitWitness a p i
forall a. MultiplicativeSemigroup a => a -> a -> a
* WitVar p i -> CircuitWitness a p i
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SysVar i -> WitVar p i
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar SysVar i
sV) CircuitWitness a p i
-> CircuitWitness a p i -> CircuitWitness a p i
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> CircuitWitness a p i
forall a b. FromConstant a b => a -> b
fromConstant a
b

instance
  (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), o ~ U1)
  => MonadCircuit (Var a i) a (CircuitWitness a p i) (State (ArithmeticCircuit a p i o)) where

    unconstrained :: CircuitWitness a p i -> State (ArithmeticCircuit a p i o) (Var a i)
unconstrained CircuitWitness a p i
wf = case CircuitWitness a p i
-> forall n w. IsWitness a n w => (WitVar p i -> w) -> w
forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF CircuitWitness a p i
wf ((WitVar p i -> UVar a i) -> UVar a i)
-> (WitVar p i -> UVar a i) -> UVar a i
forall a b. (a -> b) -> a -> b
$ \case
      WSysVar SysVar i
sV -> a -> SysVar i -> a -> UVar a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> UVar a i
LinUVar a
forall a. MultiplicativeMonoid a => a
one SysVar i
sV a
forall a. AdditiveMonoid a => a
zero
      WitVar p i
_          -> UVar a i
forall a (i :: Type -> Type). UVar a i
More of
        ConstUVar a
c -> Var a i -> State (ArithmeticCircuit a p i o) (Var a i)
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a -> Var a i
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
c)
        LinUVar a
k SysVar i
x a
b -> Var a i -> State (ArithmeticCircuit a p i o) (Var a i)
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (a -> SysVar i -> a -> Var a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
k SysVar i
x a
b)
        UVar a i
_ -> do
          let v :: ByteString
v = forall a (p :: Type -> Type) (i :: Type -> Type).
(Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
WitnessF a (WitVar p i) -> ByteString
witToVar @a CircuitWitness a p i
wf
          -- TODO: forbid reassignment of variables
          Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall k (is :: IxList) c.
Is k A_Lens =>
Optic'
  k
  is
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity c
-> StateT (ArithmeticCircuit a p i o) Identity c
forall (m :: Type -> Type) (n :: Type -> Type) s t k (is :: IxList)
       c.
(Zoom m n s t, Is k A_Lens) =>
Optic' k is t s -> m c -> n c
zoom Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
#acWitness (StateT (Map ByteString (CircuitWitness a p i)) Identity ()
 -> State (ArithmeticCircuit a p i o) ())
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall a b. (a -> b) -> a -> b
$ (Map ByteString (CircuitWitness a p i)
 -> Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (ByteString
-> CircuitWitness a p i
-> Map ByteString (CircuitWitness a p i)
-> Map ByteString (CircuitWitness a p i)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert ByteString
v CircuitWitness a p i
wf)
          Var a i -> State (ArithmeticCircuit a p i o) (Var a i)
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Var a i -> State (ArithmeticCircuit a p i o) (Var a i))
-> Var a i -> State (ArithmeticCircuit a p i o) (Var a i)
forall a b. (a -> b) -> a -> b
$ SysVar i -> Var a i
forall a (i :: Type -> Type). Semiring a => SysVar i -> Var a i
toVar (ByteString -> SysVar i
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v)

    constraint :: ClosedPoly (Var a i) a -> State (ArithmeticCircuit a p i o) ()
constraint ClosedPoly (Var a i) a
p =
      let evalConstVar :: Var a i -> Constraint a i
evalConstVar = \case
            LinVar a
k SysVar i
sysV a
b -> a -> Constraint a i
forall a b. FromConstant a b => a -> b
fromConstant a
k Constraint a i -> Constraint a i -> Constraint a i
forall a. MultiplicativeSemigroup a => a -> a -> a
* SysVar i -> Constraint a i
forall c i j. Polynomial c i j => i -> Poly c i j
var SysVar i
sysV Constraint a i -> Constraint a i -> Constraint a i
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> Constraint a i
forall a b. FromConstant a b => a -> b
fromConstant a
b
            ConstVar a
cV -> a -> Constraint a i
forall a b. FromConstant a b => a -> b
fromConstant a
cV
          evalMaybe :: Var a i -> Maybe a
evalMaybe = \case
            ConstVar a
cV -> a -> Maybe a
forall a. a -> Maybe a
Just a
cV
            Var a i
_ -> Maybe a
forall a. Maybe a
Nothing
      in case (Var a i -> Maybe a) -> Maybe a
ClosedPoly (Var a i) a
p Var a i -> Maybe a
forall {a} {i :: Type -> Type}. Var a i -> Maybe a
evalMaybe of
        Just a
c -> if a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero
                    then () -> State (ArithmeticCircuit a p i o) ()
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
                    else [Char] -> State (ArithmeticCircuit a p i o) ()
forall a. HasCallStack => [Char] -> a
error [Char]
"The constraint is non-zero"
        Maybe a
Nothing -> Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (Constraint a i))
-> StateT (Map ByteString (Constraint a i)) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall k (is :: IxList) c.
Is k A_Lens =>
Optic'
  k is (ArithmeticCircuit a p i U1) (Map ByteString (Constraint a i))
-> StateT (Map ByteString (Constraint a i)) Identity c
-> StateT (ArithmeticCircuit a p i o) Identity c
forall (m :: Type -> Type) (n :: Type -> Type) s t k (is :: IxList)
       c.
(Zoom m n s t, Is k A_Lens) =>
Optic' k is t s -> m c -> n c
zoom Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (Constraint a i))
#acSystem (StateT (Map ByteString (Constraint a i)) Identity ()
 -> State (ArithmeticCircuit a p i o) ())
-> ((Map ByteString (Constraint a i)
     -> Map ByteString (Constraint a i))
    -> StateT (Map ByteString (Constraint a i)) Identity ())
-> (Map ByteString (Constraint a i)
    -> Map ByteString (Constraint a i))
-> State (ArithmeticCircuit a p i o) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ByteString (Constraint a i)
 -> Map ByteString (Constraint a i))
-> StateT (Map ByteString (Constraint a i)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((Map ByteString (Constraint a i)
  -> Map ByteString (Constraint a i))
 -> State (ArithmeticCircuit a p i o) ())
-> (Map ByteString (Constraint a i)
    -> Map ByteString (Constraint a i))
-> State (ArithmeticCircuit a p i o) ()
forall a b. (a -> b) -> a -> b
$ ByteString
-> Constraint a i
-> Map ByteString (Constraint a i)
-> Map ByteString (Constraint a i)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert (forall a (p :: Type -> Type) (i :: Type -> Type).
(Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
WitnessF a (WitVar p i) -> ByteString
witToVar @_ @p ((Var a i -> CircuitWitness a p i) -> CircuitWitness a p i
ClosedPoly (Var a i) a
p Var a i -> CircuitWitness a p i
forall i w. Witness i w => i -> w
at)) ((Var a i -> Constraint a i) -> Constraint a i
ClosedPoly (Var a i) a
p Var a i -> Constraint a i
evalConstVar)

    rangeConstraint :: Var a i -> a -> State (ArithmeticCircuit a p i o) ()
rangeConstraint (LinVar a
k SysVar i
x a
b) a
upperBound = do
      SysVar i
v <- StateT (ArithmeticCircuit a p i o) Identity (SysVar i)
preparedVar
      Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (MonoidalMap a (Set (SysVar i)))
-> StateT (MonoidalMap a (Set (SysVar i))) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall k (is :: IxList) c.
Is k A_Lens =>
Optic'
  k is (ArithmeticCircuit a p i U1) (MonoidalMap a (Set (SysVar i)))
-> StateT (MonoidalMap a (Set (SysVar i))) Identity c
-> StateT (ArithmeticCircuit a p i o) Identity c
forall (m :: Type -> Type) (n :: Type -> Type) s t k (is :: IxList)
       c.
(Zoom m n s t, Is k A_Lens) =>
Optic' k is t s -> m c -> n c
zoom Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (MonoidalMap a (Set (SysVar i)))
#acRange (StateT (MonoidalMap a (Set (SysVar i))) Identity ()
 -> State (ArithmeticCircuit a p i o) ())
-> ((MonoidalMap a (Set (SysVar i))
     -> MonoidalMap a (Set (SysVar i)))
    -> StateT (MonoidalMap a (Set (SysVar i))) Identity ())
-> (MonoidalMap a (Set (SysVar i))
    -> MonoidalMap a (Set (SysVar i)))
-> State (ArithmeticCircuit a p i o) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MonoidalMap a (Set (SysVar i)) -> MonoidalMap a (Set (SysVar i)))
-> StateT (MonoidalMap a (Set (SysVar i))) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify ((MonoidalMap a (Set (SysVar i)) -> MonoidalMap a (Set (SysVar i)))
 -> State (ArithmeticCircuit a p i o) ())
-> (MonoidalMap a (Set (SysVar i))
    -> MonoidalMap a (Set (SysVar i)))
-> State (ArithmeticCircuit a p i o) ()
forall a b. (a -> b) -> a -> b
$ (Set (SysVar i) -> Set (SysVar i) -> Set (SysVar i))
-> a
-> Set (SysVar i)
-> MonoidalMap a (Set (SysVar i))
-> MonoidalMap a (Set (SysVar i))
forall k a.
Ord k =>
(a -> a -> a) -> k -> a -> MonoidalMap k a -> MonoidalMap k a
insertWith Set (SysVar i) -> Set (SysVar i) -> Set (SysVar i)
forall a. Ord a => Set a -> Set a -> Set a
S.union a
upperBound (SysVar i -> Set (SysVar i)
forall a. a -> Set a
S.singleton SysVar i
v)
      where
        preparedVar :: StateT (ArithmeticCircuit a p i o) Identity (SysVar i)
preparedVar = if a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. MultiplicativeMonoid a => a
one Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
|| a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. AdditiveGroup a => a -> a
negate a
forall a. MultiplicativeMonoid a => a
one Bool -> Bool -> Bool
&& a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
upperBound
          then SysVar i -> StateT (ArithmeticCircuit a p i o) Identity (SysVar i)
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SysVar i
x
          else do
            let
              wf :: CircuitWitness a p i
wf = Var a i -> CircuitWitness a p i
forall i w. Witness i w => i -> w
at (Var a i -> CircuitWitness a p i)
-> Var a i -> CircuitWitness a p i
forall a b. (a -> b) -> a -> b
$ a -> SysVar i -> a -> Var a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
k SysVar i
x a
b
              v :: ByteString
v = forall a (p :: Type -> Type) (i :: Type -> Type).
(Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
WitnessF a (WitVar p i) -> ByteString
witToVar @a CircuitWitness a p i
wf
            -- TODO: forbid reassignment of variables
            Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall k (is :: IxList) c.
Is k A_Lens =>
Optic'
  k
  is
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity c
-> StateT (ArithmeticCircuit a p i o) Identity c
forall (m :: Type -> Type) (n :: Type -> Type) s t k (is :: IxList)
       c.
(Zoom m n s t, Is k A_Lens) =>
Optic' k is t s -> m c -> n c
zoom Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (CircuitWitness a p i))
#acWitness (StateT (Map ByteString (CircuitWitness a p i)) Identity ()
 -> State (ArithmeticCircuit a p i o) ())
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall a b. (a -> b) -> a -> b
$ (Map ByteString (CircuitWitness a p i)
 -> Map ByteString (CircuitWitness a p i))
-> StateT (Map ByteString (CircuitWitness a p i)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (ByteString
-> CircuitWitness a p i
-> Map ByteString (CircuitWitness a p i)
-> Map ByteString (CircuitWitness a p i)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert ByteString
v CircuitWitness a p i
wf)
            SysVar i -> StateT (ArithmeticCircuit a p i o) Identity (SysVar i)
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ByteString -> SysVar i
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v)

    rangeConstraint (ConstVar a
c) a
upperBound =
      if a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
upperBound
        then () -> State (ArithmeticCircuit a p i o) ()
forall a. a -> StateT (ArithmeticCircuit a p i o) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
        else [Char] -> State (ArithmeticCircuit a p i o) ()
forall a. HasCallStack => [Char] -> a
error [Char]
"The constant does not belong to the interval"

-- | Generates new variable index given a witness for it.
--
-- It is a root hash (sha256) of a Merkle tree which is obtained from witness:
--
-- 1. Due to parametricity, the only operations inside witness are
--    operations from 'WitnessField' interface;
--
-- 2. Thus witness can be viewed as an AST of a 'WitnessField' "language" where:
--
--     * leafs are 'fromConstant' calls and variables;
--     * nodes are algebraic operations;
--     * root is the witness value for new variable.
--
-- 3. To inspect this AST, we instantiate witness with a special inspector type
--    whose 'WitnessField' instances perform inspection.
--
-- 4. Inspector type used here, 'MerkleHash', treats AST as a Merkle tree and
--    performs the calculation of hashes for it.
--
-- 5. Thus the result of running the witness with 'MerkleHash' as a
--    'WitnessField' is a root hash of a Merkle tree for a witness.
witToVar ::
  forall a p i. (Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
  WitnessF a (WitVar p i) -> ByteString
witToVar :: forall a (p :: Type -> Type) (i :: Type -> Type).
(Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
WitnessF a (WitVar p i) -> ByteString
witToVar (WitnessF forall n w. IsWitness a n w => (WitVar p i -> w) -> w
w) = forall (n :: Maybe Natural). MerkleHash n -> ByteString
runHash @(Just (Order a)) (MerkleHash ('Just (Order a)) -> ByteString)
-> MerkleHash ('Just (Order a)) -> ByteString
forall a b. (a -> b) -> a -> b
$ (WitVar p i -> MerkleHash ('Just (Order a)))
-> MerkleHash ('Just (Order a))
forall n w. IsWitness a n w => (WitVar p i -> w) -> w
w ((WitVar p i -> MerkleHash ('Just (Order a)))
 -> MerkleHash ('Just (Order a)))
-> (WitVar p i -> MerkleHash ('Just (Order a)))
-> MerkleHash ('Just (Order a))
forall a b. (a -> b) -> a -> b
$ \case
  WExVar Rep p
exV -> Rep p -> MerkleHash ('Just (Order a))
forall a (n :: Maybe Natural). Binary a => a -> MerkleHash n
merkleHash Rep p
exV
  WSysVar (InVar Rep i
inV) -> Rep i -> MerkleHash ('Just (Order a))
forall a (n :: Maybe Natural). Binary a => a -> MerkleHash n
merkleHash Rep i
inV
  WSysVar (NewVar ByteString
newV) -> ByteString -> MerkleHash ('Just (Order a))
forall (n :: Maybe Natural). ByteString -> MerkleHash n
M ByteString
newV

----------------------------- Evaluation functions -----------------------------

witnessGenerator ::
  (Arithmetic a, Representable p, Representable i) =>
  ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a
witnessGenerator :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Map ByteString a
witnessGenerator ArithmeticCircuit a p i o
circuit p a
payload i a
inputs =
  let result :: Map ByteString a
result = ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
acWitness ArithmeticCircuit a p i o
circuit Map ByteString (CircuitWitness a p i)
-> (CircuitWitness a p i -> a) -> Map ByteString a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \CircuitWitness a p i
k -> CircuitWitness a p i
-> forall n w. IsWitness a n w => (WitVar p i -> w) -> w
forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF CircuitWitness a p i
k ((WitVar p i -> a) -> a) -> (WitVar p i -> a) -> a
forall a b. (a -> b) -> a -> b
$ \case
        WExVar Rep p
eV -> p a -> Rep p -> a
forall a. p a -> Rep p -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index p a
payload Rep p
eV
        WSysVar (InVar Rep i
iV) -> i a -> Rep i -> a
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index i a
inputs Rep i
iV
        WSysVar (NewVar ByteString
nV) -> Map ByteString a
result Map ByteString a -> ByteString -> a
forall k a. Ord k => Map k a -> k -> a
! ByteString
nV
  in Map ByteString a
result

-- | Evaluates the arithmetic circuit with one output using the supplied input map.
eval1 ::
  (Arithmetic a, Representable p, Representable i) =>
  ArithmeticCircuit a p i Par1 -> p a -> i a -> a
eval1 :: forall a (p :: Type -> Type) (i :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i Par1 -> p a -> i a -> a
eval1 ArithmeticCircuit a p i Par1
ctx p a
p i a
i = Par1 a -> a
forall p. Par1 p -> p
unPar1 (ArithmeticCircuit a p i Par1 -> p a -> i a -> Par1 a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i, Functor o) =>
ArithmeticCircuit a p i o -> p a -> i a -> o a
eval ArithmeticCircuit a p i Par1
ctx p a
p i a
i)

-- | Evaluates the arithmetic circuit using the supplied input map.
eval ::
  (Arithmetic a, Representable p, Representable i, Functor o) =>
  ArithmeticCircuit a p i o -> p a -> i a -> o a
eval :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i, Functor o) =>
ArithmeticCircuit a p i o -> p a -> i a -> o a
eval ArithmeticCircuit a p i o
ctx p a
p i a
i = ArithmeticCircuit a p i o -> p a -> i a -> Var a i -> a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Var a i -> a
indexW ArithmeticCircuit a p i o
ctx p a
p i a
i (Var a i -> a) -> o (Var a i) -> o a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithmeticCircuit a p i o -> o (Var a i)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput ArithmeticCircuit a p i o
ctx

-- | Evaluates the arithmetic circuit with no inputs and one output.
exec1 :: Arithmetic a => ArithmeticCircuit a U1 U1 Par1 -> a
exec1 :: forall a. Arithmetic a => ArithmeticCircuit a U1 U1 Par1 -> a
exec1 ArithmeticCircuit a U1 U1 Par1
ac = ArithmeticCircuit a U1 U1 Par1 -> U1 a -> U1 a -> a
forall a (p :: Type -> Type) (i :: Type -> Type).
(Arithmetic a, Representable p, Representable i) =>
ArithmeticCircuit a p i Par1 -> p a -> i a -> a
eval1 ArithmeticCircuit a U1 U1 Par1
ac U1 a
forall k (p :: k). U1 p
U1 U1 a
forall k (p :: k). U1 p
U1

-- | Evaluates the arithmetic circuit with no inputs.
exec :: (Arithmetic a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a
exec :: forall a (o :: Type -> Type).
(Arithmetic a, Functor o) =>
ArithmeticCircuit a U1 U1 o -> o a
exec ArithmeticCircuit a U1 U1 o
ac = ArithmeticCircuit a U1 U1 o -> U1 a -> U1 a -> o a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Representable p, Representable i, Functor o) =>
ArithmeticCircuit a p i o -> p a -> i a -> o a
eval ArithmeticCircuit a U1 U1 o
ac U1 a
forall k (p :: k). U1 p
U1 U1 a
forall k (p :: k). U1 p
U1

-- | Applies the values of the first couple of inputs to the arithmetic circuit.
apply ::
  (Eq a, Field a, Ord (Rep j), Representable i, Functor o) =>
  i a -> ArithmeticCircuit a p (i :*: j) o -> ArithmeticCircuit a p j o
apply :: forall a (j :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type) (p :: Type -> Type).
(Eq a, Field a, Ord (Rep j), Representable i, Functor o) =>
i a
-> ArithmeticCircuit a p (i :*: j) o -> ArithmeticCircuit a p j o
apply i a
xs ArithmeticCircuit a p (i :*: j) o
ac = ArithmeticCircuit a p (i :*: j) o
ac
  { acSystem = fmap (evalPolynomial evalMonomial varF) (acSystem ac)
  , acRange = S.fromList . catMaybes . toList . filterSet <$> acRange ac
  , acWitness = (>>= witF) <$> acWitness ac
  , acFold = bimap outF (>>= witF) <$> acFold ac
  , acOutput = outF <$> acOutput ac
  }
  where
    outF :: Var a (i :*: j) -> Var a j
outF (LinVar a
k (InVar (Left Rep i
v)) a
b)  = a -> Var a j
forall a (i :: Type -> Type). a -> Var a i
ConstVar (a
k a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* i a -> Rep i -> a
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index i a
xs Rep i
v a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
b)
    outF (LinVar a
k (InVar (Right Rep j
v)) a
b) = a -> SysVar j -> a -> Var a j
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
k (Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar Rep j
v) a
b
    outF (LinVar a
k (NewVar ByteString
v) a
b)        = a -> SysVar j -> a -> Var a j
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
k (ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v) a
b
    outF (ConstVar a
a)                   = a -> Var a j
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
a

    varF :: SysVar (i :*: j) -> Poly a (SysVar j) Natural
varF (InVar (Left Rep i
v))  = a -> Poly a (SysVar j) Natural
forall a b. FromConstant a b => a -> b
fromConstant (i a -> Rep i -> a
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index i a
xs Rep i
v)
    varF (InVar (Right Rep j
v)) = SysVar j -> Poly a (SysVar j) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var (Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar Rep j
v)
    varF (NewVar ByteString
v)        = SysVar j -> Poly a (SysVar j) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var (ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v)

    witF :: WitVar p (i :*: j) -> WitnessF a (WitVar p j)
witF (WSysVar (InVar (Left Rep i
v)))  = (forall n w. IsWitness a n w => (WitVar p j -> w) -> w)
-> WitnessF a (WitVar p j)
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF ((forall n w. IsWitness a n w => (WitVar p j -> w) -> w)
 -> WitnessF a (WitVar p j))
-> (forall n w. IsWitness a n w => (WitVar p j -> w) -> w)
-> WitnessF a (WitVar p j)
forall a b. (a -> b) -> a -> b
$ w -> (WitVar p j -> w) -> w
forall a b. a -> b -> a
const (w -> (WitVar p j -> w) -> w) -> w -> (WitVar p j -> w) -> w
forall a b. (a -> b) -> a -> b
$ a -> w
forall a b. FromConstant a b => a -> b
fromConstant (i a -> Rep i -> a
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index i a
xs Rep i
v)
    witF (WSysVar (InVar (Right Rep j
v))) = WitVar p j -> WitnessF a (WitVar p j)
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WitVar p j -> WitnessF a (WitVar p j))
-> WitVar p j -> WitnessF a (WitVar p j)
forall a b. (a -> b) -> a -> b
$ SysVar j -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar (Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar Rep j
v)
    witF (WSysVar (NewVar ByteString
v))        = WitVar p j -> WitnessF a (WitVar p j)
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WitVar p j -> WitnessF a (WitVar p j))
-> WitVar p j -> WitnessF a (WitVar p j)
forall a b. (a -> b) -> a -> b
$ SysVar j -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar (ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v)
    witF (WExVar Rep p
v)                  = WitVar p j -> WitnessF a (WitVar p j)
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Rep p -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type). Rep p -> WitVar p i
WExVar Rep p
v)

    filterSet :: Ord (Rep j) => S.Set (SysVar (i :*: j)) ->  S.Set (Maybe (SysVar j))
    filterSet :: forall (j :: Type -> Type) (i :: Type -> Type).
Ord (Rep j) =>
Set (SysVar (i :*: j)) -> Set (Maybe (SysVar j))
filterSet = (SysVar (i :*: j) -> Maybe (SysVar j))
-> Set (SysVar (i :*: j)) -> Set (Maybe (SysVar j))
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\case
                    NewVar ByteString
v        -> SysVar j -> Maybe (SysVar j)
forall a. a -> Maybe a
Just (ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
v)
                    InVar (Right Rep j
v) -> SysVar j -> Maybe (SysVar j)
forall a. a -> Maybe a
Just (Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar Rep j
v)
                    SysVar (i :*: j)
_               -> Maybe (SysVar j)
forall a. Maybe a
Nothing)

-- TODO: Add proper symbolic application functions

-- applySymOne :: ArithmeticCircuit a -> State (ArithmeticCircuit a) ()
-- applySymOne x = modify (\(f :: ArithmeticCircuit a) ->
--     let ins = acInput f
--     in f
--     {
--         acInput = tail ins,
--         acWitness = acWitness f . (singleton (head ins) (eval x empty)  `union`)
--     })

-- applySym :: [ArithmeticCircuit a] -> State (ArithmeticCircuit a) ()
-- applySym = foldr ((>>) . applySymOne) (return ())

-- applySymArgs :: ArithmeticCircuit a -> [ArithmeticCircuit a] -> ArithmeticCircuit a
-- applySymArgs x xs = execState (applySym xs) x