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

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (
        ArithmeticCircuit(..),
        CircuitFold (..),
        Var (..),
        SysVar (..),
        NewVar (..),
        WitVar (..),
        VarField,
        Arithmetic,
        Constraint,
        -- circuit constructors
        emptyCircuit,
        naturalCircuit,
        idCircuit,
        -- 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, foldl', toList)
import           Data.Functor.Rep
import           Data.List.Infinite                                           (Infinite)
import qualified Data.List.Infinite                                           as I
import           Data.Map.Monoidal                                            (MonoidalMap)
import qualified Data.Map.Monoidal                                            as MM
import           Data.Map.Strict                                              (Map)
import qualified Data.Map.Strict                                              as M
import           Data.Maybe                                                   (catMaybes, fromJust, fromMaybe)
import           Data.Semialign                                               (unzipDefault)
import           Data.Semigroup.Generic                                       (GenericSemigroupMonoid (..))
import qualified Data.Set                                                     as S
import           Data.Traversable                                             (for)
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.ByteString                                  (fromByteString, toByteString)
import           ZkFold.Base.Data.HFunctor
import           ZkFold.Base.Data.Package
import           ZkFold.Base.Data.Product
import           ZkFold.Prelude                                               (take)
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.Fold
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 p s j.
  ( Binary (Rep p), Representable p
  , Traversable s, Representable s, NFData1 s
  , Binary (Rep s), NFData (Rep s), Ord (Rep s)
  , Representable j, Binary (Rep j), NFData (Rep j), Ord (Rep j)) =>
    CircuitFold
      { ()
foldStep   :: ArithmeticCircuit a p (s :*: j) s
      , ()
foldStepP  :: p (CircuitWitness a p (s :*: j))
      , ()
foldSeed   :: s v
      , ()
foldSeedP  :: p w
      , ()
foldStream :: Infinite (j w)
      , forall a v w. CircuitFold a v w -> v
foldCount  :: 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
p c
p (CircuitWitness a p (s :*: j))
s a
Infinite (j c)
ArithmeticCircuit a p (s :*: j) s
foldStep :: ()
foldStepP :: ()
foldSeed :: ()
foldSeedP :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldStep :: ArithmeticCircuit a p (s :*: j) s
foldStepP :: p (CircuitWitness a p (s :*: j))
foldSeed :: s a
foldSeedP :: p c
foldStream :: Infinite (j c)
foldCount :: a
..} = CircuitFold
    { foldStep :: ArithmeticCircuit a p (s :*: j) s
foldStep = ArithmeticCircuit a p (s :*: j) s
foldStep
    , foldStepP :: p (CircuitWitness a p (s :*: j))
foldStepP = p (CircuitWitness a p (s :*: j))
foldStepP
    , 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
    , foldSeedP :: p d
foldSeedP = c -> d
g (c -> d) -> p c -> p d
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> p c
foldSeedP
    , 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
    }

instance (NFData a, NFData v) => NFData (CircuitFold a v w) where
  rnf :: CircuitFold a v w -> ()
rnf CircuitFold {v
p w
p (CircuitWitness a p (s :*: j))
s v
Infinite (j w)
ArithmeticCircuit a p (s :*: j) s
foldStep :: ()
foldStepP :: ()
foldSeed :: ()
foldSeedP :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldStep :: ArithmeticCircuit a p (s :*: j) s
foldStepP :: p (CircuitWitness a p (s :*: j))
foldSeed :: s v
foldSeedP :: p w
foldStream :: Infinite (j w)
foldCount :: v
..} = (ArithmeticCircuit a p (s :*: j) s, v) -> ()
forall a. NFData a => a -> ()
rnf (ArithmeticCircuit a p (s :*: j) 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

-- | 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)
  | WFoldVar ByteString ByteString
  | 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
_ (WFoldVar ByteString
b ByteString
c) = ByteString -> ByteString -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type).
ByteString -> ByteString -> WitVar p i
WFoldVar ByteString
b ByteString
c
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
_ (WFoldVar ByteString
b ByteString
c) = ByteString -> ByteString -> WitVar q i
forall (p :: Type -> Type) (i :: Type -> Type).
ByteString -> ByteString -> WitVar p i
WFoldVar ByteString
b ByteString
c
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

----------------------------- Circuit constructors -----------------------------

emptyCircuit :: ArithmeticCircuit a p i U1
emptyCircuit :: forall a (p :: Type -> Type) (i :: Type -> Type).
ArithmeticCircuit a p i U1
emptyCircuit = 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))
-> U1 (Var a i)
-> ArithmeticCircuit a p i U1
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
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))
-> o (Var a i)
-> ArithmeticCircuit a p i o
ArithmeticCircuit Map ByteString (Constraint a i)
forall k a. Map k a
M.empty MonoidalMap a (Set (SysVar i))
forall k a. MonoidalMap k a
MM.empty Map ByteString (CircuitWitness a p i)
forall k a. Map k a
M.empty Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
forall k a. Map k a
M.empty U1 (Var a i)
forall k (p :: k). U1 p
U1

-- | 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.
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
naturalCircuit :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(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
naturalCircuit forall x. p x -> i x -> o x
f = (o (Var a i)
 -> ArithmeticCircuit a p i U1 -> ArithmeticCircuit a p i o)
-> (o (Var a i), ArithmeticCircuit a p i U1)
-> ArithmeticCircuit a p i o
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Optic
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (ArithmeticCircuit a p i o)
  (U1 (Var a i))
  (o (Var a i))
-> o (Var a i)
-> ArithmeticCircuit a p i U1
-> ArithmeticCircuit a p i o
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 o)
  (U1 (Var a i))
  (o (Var a i))
#acOutput) ((o (Var a i), ArithmeticCircuit a p i U1)
 -> ArithmeticCircuit a p i o)
-> (o (Var a i), ArithmeticCircuit a p i U1)
-> ArithmeticCircuit a p i o
forall a b. (a -> b) -> a -> b
$ (State (ArithmeticCircuit a p i U1) (o (Var a i))
 -> ArithmeticCircuit a p i U1
 -> (o (Var a i), ArithmeticCircuit a p i U1))
-> ArithmeticCircuit a p i U1
-> State (ArithmeticCircuit a p i U1) (o (Var a i))
-> (o (Var a i), ArithmeticCircuit a p i U1)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (ArithmeticCircuit a p i U1) (o (Var a i))
-> ArithmeticCircuit a p i U1
-> (o (Var a i), ArithmeticCircuit a p i U1)
forall s a. State s a -> s -> (a, s)
runState ArithmeticCircuit a p i U1
forall a (p :: Type -> Type) (i :: Type -> Type).
ArithmeticCircuit a p i U1
emptyCircuit (State (ArithmeticCircuit a p i U1) (o (Var a i))
 -> (o (Var a i), ArithmeticCircuit a p i U1))
-> State (ArithmeticCircuit a p i U1) (o (Var a i))
-> (o (Var a i), ArithmeticCircuit a p i U1)
forall a b. (a -> b) -> a -> b
$
  o (Either (Rep p) (Rep i))
-> (Either (Rep p) (Rep i)
    -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> State (ArithmeticCircuit a p i U1) (o (Var a i))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for (p (Either (Rep p) (Rep i))
-> i (Either (Rep p) (Rep i)) -> o (Either (Rep p) (Rep i))
forall x. p x -> i x -> o x
f ((Rep p -> Either (Rep p) (Rep i)) -> p (Either (Rep p) (Rep i))
forall a. (Rep p -> a) -> p a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep p -> Either (Rep p) (Rep i)
forall a b. a -> Either a b
Left) ((Rep i -> Either (Rep p) (Rep i)) -> i (Either (Rep p) (Rep i))
forall a. (Rep i -> a) -> i a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep i -> Either (Rep p) (Rep i)
forall a b. b -> Either a b
Right)) ((Either (Rep p) (Rep i)
  -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
 -> State (ArithmeticCircuit a p i U1) (o (Var a i)))
-> (Either (Rep p) (Rep i)
    -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> State (ArithmeticCircuit a p i U1) (o (Var a i))
forall a b. (a -> b) -> a -> b
$
    (Rep p -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> (Rep i
    -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> Either (Rep p) (Rep i)
-> StateT (ArithmeticCircuit a p i U1) Identity (Var a i)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (WitnessF a (WitVar p i)
-> StateT (ArithmeticCircuit a p i U1) Identity (Var a i)
forall var a w (m :: Type -> Type).
MonadCircuit var a w m =>
w -> m var
unconstrained (WitnessF a (WitVar p i)
 -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> (Rep p -> WitnessF a (WitVar p i))
-> Rep p
-> StateT (ArithmeticCircuit a p i U1) Identity (Var a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WitVar p i -> WitnessF a (WitVar p i)
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WitVar p i -> WitnessF a (WitVar p i))
-> (Rep p -> WitVar p i) -> Rep p -> WitnessF a (WitVar p i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep p -> WitVar p i
forall (p :: Type -> Type) (i :: Type -> Type). Rep p -> WitVar p i
WExVar) (Var a i -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i)
forall a. a -> StateT (ArithmeticCircuit a p i U1) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Var a i -> StateT (ArithmeticCircuit a p i U1) Identity (Var a i))
-> (Rep i -> Var a i)
-> Rep i
-> StateT (ArithmeticCircuit a p i U1) Identity (Var a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)

-- | Identity circuit which returns its input @i@ and doesn't use the payload.
idCircuit :: (Representable i, Semiring a) => ArithmeticCircuit a p i i
idCircuit :: forall (i :: Type -> Type) a (p :: Type -> Type).
(Representable i, Semiring a) =>
ArithmeticCircuit a p i i
idCircuit = ArithmeticCircuit a p i U1
forall a (p :: Type -> Type) (i :: Type -> Type).
ArithmeticCircuit a p i U1
emptyCircuit { acOutput = acInput }

---------------------------------- 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 (NewVar -> SysVar i
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar (NewVar -> SysVar i)
-> (ByteString -> NewVar) -> ByteString -> SysVar i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> NewVar
EqVar) (Map ByteString (CircuitWitness a p i) -> [ByteString]
forall k a. Map k a -> [k]
M.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)
  [SysVar i] -> [SysVar i] -> [SysVar i]
forall a. [a] -> [a] -> [a]
++ (NewVar -> SysVar i) -> [NewVar] -> [SysVar i]
forall a b. (a -> b) -> [a] -> [b]
map NewVar -> SysVar i
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar ((ByteString
 -> CircuitFold a (Var a i) (CircuitWitness a p i) -> [NewVar])
-> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
-> [NewVar]
forall m k a. Monoid m => (k -> a -> m) -> Map k a -> m
M.foldMapWithKey (\ByteString
fi -> (ByteString -> NewVar) -> [ByteString] -> [NewVar]
forall a b. (a -> b) -> [a] -> [b]
map (ByteString -> ByteString -> NewVar
FoldVar ByteString
fi) ([ByteString] -> [NewVar])
-> (CircuitFold a (Var a i) (CircuitWitness a p i) -> [ByteString])
-> CircuitFold a (Var a i) (CircuitWitness a p i)
-> [NewVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CircuitFold a (Var a i) (CircuitWitness a p i) -> [ByteString]
forall v w. CircuitFold a v w -> [ByteString]
keys) (Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
 -> [NewVar])
-> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
-> [NewVar]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a p i o
-> Map ByteString (CircuitFold a (Var a i) (CircuitWitness a p i))
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 ArithmeticCircuit a p i o
ac)
  where
    acInput0 :: i (SysVar i)
    acInput0 :: i (SysVar i)
acInput0 = (Rep i -> SysVar i) -> i (SysVar i)
forall a. (Rep i -> a) -> i a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep i -> SysVar i
forall (i :: Type -> Type). Rep i -> SysVar i
InVar
    keys :: CircuitFold a v w -> [ByteString]
    keys :: forall v w. CircuitFold a v w -> [ByteString]
keys CircuitFold {v
p w
p (CircuitWitness a p (s :*: j))
s v
Infinite (j w)
ArithmeticCircuit a p (s :*: j) s
foldStep :: ()
foldStepP :: ()
foldSeed :: ()
foldSeedP :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldStep :: ArithmeticCircuit a p (s :*: j) s
foldStepP :: p (CircuitWitness a p (s :*: j))
foldSeed :: s v
foldSeedP :: p w
foldStream :: Infinite (j w)
foldCount :: v
..} = s ByteString -> [ByteString]
forall a. s a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (s ByteString -> [ByteString]) -> s ByteString -> [ByteString]
forall a b. (a -> b) -> a -> b
$ (Rep s -> v -> ByteString) -> s v -> s ByteString
forall (r :: Type -> Type) a a'.
Representable r =>
(Rep r -> a -> a') -> r a -> r a'
imapRep (\Rep s
r v
_ -> Rep s -> ByteString
forall a. Binary a => a -> ByteString
toByteString Rep s
r) s v
foldSeed

indexW ::
  (Arithmetic a, Binary 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, Binary 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 =
  Map NewVar a -> i a -> Var a i -> a
forall (i :: Type -> Type) a.
(Representable i, Arithmetic a) =>
Map NewVar a -> i a -> Var a i -> a
indexG (ArithmeticCircuit a p i o -> p a -> i a -> Map NewVar a
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Binary a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Map NewVar a
witnessGenerator ArithmeticCircuit a p i o
circuit p a
payload i a
inputs) i a
inputs

indexG :: (Representable i, Arithmetic a) => Map NewVar a -> i a -> Var a i -> a
indexG :: forall (i :: Type -> Type) a.
(Representable i, Arithmetic a) =>
Map NewVar a -> i a -> Var a i -> a
indexG Map NewVar a
witGen 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 NewVar
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
<> NewVar -> [Char]
forall a. Show a => a -> [Char]
show NewVar
newV))
    (Map NewVar a
witGen Map NewVar a -> NewVar -> Maybe a
forall k a. Ord k => Map k a -> k -> Maybe a
M.!? NewVar
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)

instance
  (Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i), Ord (Rep i), NFData (Rep i)) =>
  SymbolicFold (ArithmeticCircuit a p i) where
    sfoldl :: forall (f :: Type -> Type) (p :: Type -> Type) (g :: Type -> Type)
       (h :: Type -> Type) wc.
(Binary (Rep f), NFData (Rep f), Ord (Rep f),
 forall a. Binary a => Binary (f a), Representable f, NFData1 f,
 Traversable f, Binary (Rep p), Representable p, Binary (Rep g),
 NFData (Rep g), Ord (Rep g), Representable g,
 forall a. Binary a => Binary (h a),
 WitnessField (ArithmeticCircuit a p i) ~ wc) =>
(forall (s :: (Type -> Type) -> Type).
 (SymbolicFold s,
  BaseField s ~ BaseField (ArithmeticCircuit a p i)) =>
 s f -> p (WitnessField s) -> s g -> (s f, p (WitnessField s)))
-> ArithmeticCircuit a p i f
-> p wc
-> ArithmeticCircuit a p i h
-> Infinite (g wc)
-> ArithmeticCircuit a p i Par1
-> (ArithmeticCircuit a p i f, p wc)
sfoldl forall (s :: (Type -> Type) -> Type).
(SymbolicFold s,
 BaseField s ~ BaseField (ArithmeticCircuit a p i)) =>
s f -> p (WitnessField s) -> s g -> (s f, p (WitnessField s))
fun (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
sc, f (Var a i)
foldSeed)) p wc
foldSeedP ArithmeticCircuit a p i h
streamHash
           Infinite (g wc)
foldStream (ArithmeticCircuit a p i Par1
-> (ArithmeticCircuit a p i U1, Par1 (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
cc, Par1 Var a i
foldCount)) =
        let (ArithmeticCircuit a p (f :*: g) f
foldStep, p (WitnessField (ArithmeticCircuit a p (f :*: g)))
foldStepP) =
              ArithmeticCircuit a p (f :*: g) f
-> p (WitnessField (ArithmeticCircuit a p (f :*: g)))
-> ArithmeticCircuit a p (f :*: g) g
-> (ArithmeticCircuit a p (f :*: g) f,
    p (WitnessField (ArithmeticCircuit a p (f :*: g))))
forall (s :: (Type -> Type) -> Type).
(SymbolicFold s,
 BaseField s ~ BaseField (ArithmeticCircuit a p i)) =>
s f -> p (WitnessField s) -> s g -> (s f, p (WitnessField s))
fun ((forall a. (:*:) f g a -> f a)
-> ArithmeticCircuit a p (f :*: g) (f :*: g)
-> ArithmeticCircuit a p (f :*: g) f
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a)
-> ArithmeticCircuit a p (f :*: g) f
-> ArithmeticCircuit a p (f :*: g) g
hmap (:*:) f g a -> f a
forall a. (:*:) f g a -> f a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> f a
fstP ArithmeticCircuit a p (f :*: g) (f :*: g)
forall (i :: Type -> Type) a (p :: Type -> Type).
(Representable i, Semiring a) =>
ArithmeticCircuit a p i i
idCircuit)
                  ((Rep p -> WitnessField (ArithmeticCircuit a p (f :*: g)))
-> p (WitnessField (ArithmeticCircuit a p (f :*: g)))
forall a. (Rep p -> a) -> p a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ((Rep p -> WitnessField (ArithmeticCircuit a p (f :*: g)))
 -> p (WitnessField (ArithmeticCircuit a p (f :*: g))))
-> (Rep p -> WitnessField (ArithmeticCircuit a p (f :*: g)))
-> p (WitnessField (ArithmeticCircuit a p (f :*: g)))
forall a b. (a -> b) -> a -> b
$ WitVar p (f :*: g) -> WitnessF a (WitVar p (f :*: g))
forall a. a -> WitnessF a a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (WitVar p (f :*: g) -> WitnessF a (WitVar p (f :*: g)))
-> (Rep p -> WitVar p (f :*: g))
-> Rep p
-> WitnessF a (WitVar p (f :*: g))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep p -> WitVar p (f :*: g)
forall (p :: Type -> Type) (i :: Type -> Type). Rep p -> WitVar p i
WExVar)
                  ((forall a. (:*:) f g a -> g a)
-> ArithmeticCircuit a p (f :*: g) (f :*: g)
-> ArithmeticCircuit a p (f :*: g) g
forall {k} (c :: (k -> Type) -> Type) (f :: k -> Type)
       (g :: k -> Type).
HFunctor c =>
(forall (a :: k). f a -> g a) -> c f -> c g
forall (f :: Type -> Type) (g :: Type -> Type).
(forall a. f a -> g a)
-> ArithmeticCircuit a p (f :*: g) f
-> ArithmeticCircuit a p (f :*: g) g
hmap (:*:) f g a -> g a
forall a. (:*:) f g a -> g a
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
(:*:) f g a -> g a
sndP ArithmeticCircuit a p (f :*: g) (f :*: g)
forall (i :: Type -> Type) a (p :: Type -> Type).
(Representable i, Semiring a) =>
ArithmeticCircuit a p i i
idCircuit)
            fldID :: ByteString
fldID = MerkleHash Any -> ByteString
forall (n :: Maybe Natural). MerkleHash n -> ByteString
runHash (MerkleHash Any -> ByteString) -> MerkleHash Any -> ByteString
forall a b. (a -> b) -> a -> b
$ (f (Var a (f :*: g)), f (Var a i), h (Var a i), Var a i)
-> MerkleHash Any
forall a (n :: Maybe Natural). Binary a => a -> MerkleHash n
merkleHash
              (ArithmeticCircuit a p (f :*: g) f -> f (Var a (f :*: g))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput ArithmeticCircuit a p (f :*: g) f
foldStep, f (Var a i)
foldSeed, ArithmeticCircuit a p i h -> h (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 h
streamHash, Var a i
foldCount)
            (f (Var a i)
resultC :*: p (Var a i)
resultP) = (Rep (f :*: p) -> Var a i) -> (:*:) f p (Var a i)
forall a. (Rep (f :*: p) -> a) -> (:*:) f p a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (\Rep (f :*: p)
r -> a -> SysVar i -> a -> Var a i
forall a (i :: Type -> Type). a -> SysVar i -> a -> Var a i
LinVar a
forall a. MultiplicativeMonoid a => a
one (NewVar -> SysVar i
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar (ByteString -> ByteString -> NewVar
FoldVar ByteString
fldID (Either (Rep f) (Rep p) -> ByteString
forall a. Binary a => a -> ByteString
toByteString Either (Rep f) (Rep p)
Rep (f :*: p)
r))) a
forall a. AdditiveMonoid a => a
zero)
            fc :: ArithmeticCircuit a p i U1
fc = ArithmeticCircuit a p i U1
forall a (p :: Type -> Type) (i :: Type -> Type).
ArithmeticCircuit a p i U1
emptyCircuit { acFold = M.singleton fldID CircuitFold {..} }
        in ((ArithmeticCircuit a p i U1
sc 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
cc 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
fc) { acOutput = resultC }, Var a i -> wc
forall i w. Witness i w => i -> w
at (Var a i -> wc) -> p (Var a i) -> p wc
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> p (Var a i)
resultP)

----------------------------- 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
M.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 (NewVar -> SysVar i
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar (ByteString -> NewVar
EqVar 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
M.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
MM.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
M.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 (NewVar -> SysVar i
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar (ByteString -> NewVar
EqVar 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
  WFoldVar ByteString
fldID ByteString
fldV -> (ByteString, Bool, ByteString) -> MerkleHash ('Just (Order a))
forall a (n :: Maybe Natural). Binary a => a -> MerkleHash n
merkleHash (ByteString
fldID, Bool
True, ByteString
fldV)
  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 (EqVar ByteString
eqV)) -> ByteString -> MerkleHash ('Just (Order a))
forall (n :: Maybe Natural). ByteString -> MerkleHash n
M ByteString
eqV
  WSysVar (NewVar (FoldVar ByteString
fldID ByteString
fldV)) -> (ByteString, Bool, ByteString) -> MerkleHash ('Just (Order a))
forall a (n :: Maybe Natural). Binary a => a -> MerkleHash n
merkleHash (ByteString
fldID, Bool
False, ByteString
fldV)

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

witnessGenerator ::
  (Arithmetic a, Binary a, Representable p, Representable i) =>
  ArithmeticCircuit a p i o -> p a -> i a -> Map NewVar a
witnessGenerator :: forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Binary a, Representable p, Representable i) =>
ArithmeticCircuit a p i o -> p a -> i a -> Map NewVar a
witnessGenerator ArithmeticCircuit a p i o
circ p a
p i a
i = (Map NewVar a, Map ByteString (ByteString -> a)) -> Map NewVar a
forall a b. (a, b) -> a
fst (ArithmeticCircuit a p i o
-> p a -> i a -> (Map NewVar a, Map ByteString (ByteString -> a))
forall b (q :: Type -> Type) (j :: Type -> Type)
       (n :: Type -> Type).
(Arithmetic b, Binary b, Representable q, Representable j) =>
ArithmeticCircuit b q j n
-> q b -> j b -> (Map NewVar b, Map ByteString (ByteString -> b))
allWitnesses ArithmeticCircuit a p i o
circ p a
p i a
i)
  where
    allWitnesses ::
      (Arithmetic b, Binary b, Representable q, Representable j) =>
      ArithmeticCircuit b q j n -> q b -> j b ->
      (Map NewVar b, Map ByteString (ByteString -> b))
    allWitnesses :: forall b (q :: Type -> Type) (j :: Type -> Type)
       (n :: Type -> Type).
(Arithmetic b, Binary b, Representable q, Representable j) =>
ArithmeticCircuit b q j n
-> q b -> j b -> (Map NewVar b, Map ByteString (ByteString -> b))
allWitnesses ArithmeticCircuit b q j n
circuit q b
payload j b
inputs =
      let evalSysVar :: SysVar j -> b
evalSysVar = \case
            InVar Rep j
iV -> j b -> Rep j -> b
forall a. j a -> Rep j -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index j b
inputs Rep j
iV
            NewVar (EqVar ByteString
eqV) -> Map ByteString b
eqVars Map ByteString b -> ByteString -> b
forall k a. Ord k => Map k a -> k -> a
M.! ByteString
eqV
            NewVar (FoldVar ByteString
fldID ByteString
fldV) -> (Map ByteString b, ByteString -> b) -> Map ByteString b
forall a b. (a, b) -> a
fst (Map ByteString (Map ByteString b, ByteString -> b)
foldVars Map ByteString (Map ByteString b, ByteString -> b)
-> ByteString -> (Map ByteString b, ByteString -> b)
forall k a. Ord k => Map k a -> k -> a
M.! ByteString
fldID) Map ByteString b -> ByteString -> b
forall k a. Ord k => Map k a -> k -> a
M.! ByteString
fldV
          evalVar :: Var b j -> b
evalVar = \case
            LinVar b
k SysVar j
sV b
b -> b
k b -> b -> b
forall a. MultiplicativeSemigroup a => a -> a -> a
* SysVar j -> b
evalSysVar SysVar j
sV b -> b -> b
forall a. AdditiveSemigroup a => a -> a -> a
+ b
b
            ConstVar b
c -> b
c
          evalWitness :: CircuitWitness b q j -> b
evalWitness CircuitWitness b q j
k = CircuitWitness b q j
-> forall n w. IsWitness b n w => (WitVar q j -> w) -> w
forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF CircuitWitness b q j
k \case
            WExVar Rep q
eV -> q b -> Rep q -> b
forall a. q a -> Rep q -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index q b
payload Rep q
eV
            WFoldVar ByteString
fldID ByteString
fldV -> (Map ByteString b, ByteString -> b) -> ByteString -> b
forall a b. (a, b) -> b
snd (Map ByteString (Map ByteString b, ByteString -> b)
foldVars Map ByteString (Map ByteString b, ByteString -> b)
-> ByteString -> (Map ByteString b, ByteString -> b)
forall k a. Ord k => Map k a -> k -> a
M.! ByteString
fldID) ByteString
fldV
            WSysVar SysVar j
sV -> SysVar j -> b
evalSysVar SysVar j
sV
          eqVars :: Map ByteString b
eqVars = CircuitWitness b q j -> b
evalWitness (CircuitWitness b q j -> b)
-> Map ByteString (CircuitWitness b q j) -> Map ByteString b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithmeticCircuit b q j n -> Map ByteString (CircuitWitness b q j)
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> Map ByteString (CircuitWitness a p i)
acWitness ArithmeticCircuit b q j n
circuit
          foldVars :: Map ByteString (Map ByteString b, ByteString -> b)
foldVars = ArithmeticCircuit b q j n
-> Map ByteString (CircuitFold b (Var b j) (CircuitWitness b q j))
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 ArithmeticCircuit b q j n
circuit Map ByteString (CircuitFold b (Var b j) (CircuitWitness b q j))
-> (CircuitFold b (Var b j) (CircuitWitness b q j)
    -> (Map ByteString b, ByteString -> b))
-> Map ByteString (Map ByteString b, ByteString -> b)
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \CircuitFold {p (CircuitWitness b q j)
p (CircuitWitness b p (s :*: j))
s (Var b j)
Infinite (j (CircuitWitness b q j))
Var b j
ArithmeticCircuit b p (s :*: j) s
foldStep :: ()
foldStepP :: ()
foldSeed :: ()
foldSeedP :: ()
foldStream :: ()
foldCount :: forall a v w. CircuitFold a v w -> v
foldStep :: ArithmeticCircuit b p (s :*: j) s
foldStepP :: p (CircuitWitness b p (s :*: j))
foldSeed :: s (Var b j)
foldSeedP :: p (CircuitWitness b q j)
foldStream :: Infinite (j (CircuitWitness b q j))
foldCount :: Var b j
..} ->
            let foldList :: [j (CircuitWitness b q j)]
foldList =
                  Natural -> [j (CircuitWitness b q j)] -> [j (CircuitWitness b q j)]
forall a. HasCallStack => Natural -> [a] -> [a]
take (b -> Const b
forall a. ToConstant a => a -> Const a
toConstant (b -> Const b) -> b -> Const b
forall a b. (a -> b) -> a -> b
$ Var b j -> b
evalVar Var b j
foldCount) (Infinite (j (CircuitWitness b q j)) -> [j (CircuitWitness b q j)]
forall a. Infinite a -> [a]
I.toList Infinite (j (CircuitWitness b q j))
foldStream)
                (s b
resultL, p b
resultP) =
                  ((s b, p b) -> j (CircuitWitness b q j) -> (s b, p b))
-> (s b, p b) -> [j (CircuitWitness b q j)] -> (s b, p b)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\(s b
xc, p b
xp) j (CircuitWitness b q j)
y ->
                    let input :: (:*:) s j b
input = s b
xc s b -> j b -> (:*:) s j b
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: (CircuitWitness b q j -> b) -> j (CircuitWitness b q j) -> j b
forall a b. (a -> b) -> j a -> j b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap CircuitWitness b q j -> b
evalWitness j (CircuitWitness b q j)
y
                        (Map NewVar b
wg, Map ByteString (ByteString -> b)
pg) = ArithmeticCircuit b p (s :*: j) s
-> p b
-> (:*:) s j b
-> (Map NewVar b, Map ByteString (ByteString -> b))
forall b (q :: Type -> Type) (j :: Type -> Type)
       (n :: Type -> Type).
(Arithmetic b, Binary b, Representable q, Representable j) =>
ArithmeticCircuit b q j n
-> q b -> j b -> (Map NewVar b, Map ByteString (ByteString -> b))
allWitnesses ArithmeticCircuit b p (s :*: j) s
foldStep p b
xp (:*:) s j b
input
                    in (Map NewVar b -> (:*:) s j b -> Var b (s :*: j) -> b
forall (i :: Type -> Type) a.
(Representable i, Arithmetic a) =>
Map NewVar a -> i a -> Var a i -> a
indexG Map NewVar b
wg (:*:) s j b
input (Var b (s :*: j) -> b) -> s (Var b (s :*: j)) -> s b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ArithmeticCircuit b p (s :*: j) s -> s (Var b (s :*: j))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o -> o (Var a i)
acOutput ArithmeticCircuit b p (s :*: j) s
foldStep
                        , p (CircuitWitness b p (s :*: j))
foldStepP p (CircuitWitness b p (s :*: j))
-> (CircuitWitness b p (s :*: j) -> b) -> p b
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> (CircuitWitness b p (s :*: j) -> (WitVar p (s :*: j) -> b) -> b)
-> (WitVar p (s :*: j) -> b) -> CircuitWitness b p (s :*: j) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip CircuitWitness b p (s :*: j) -> (WitVar p (s :*: j) -> b) -> b
CircuitWitness b p (s :*: j)
-> forall n w. IsWitness b n w => (WitVar p (s :*: j) -> w) -> w
forall a v.
WitnessF a v -> forall n w. IsWitness a n w => (v -> w) -> w
runWitnessF \case
                            WExVar Rep p
pV -> p b -> Rep p -> b
forall a. p a -> Rep p -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index p b
xp Rep p
pV
                            WFoldVar ByteString
fldID ByteString
fldV -> (Map ByteString (ByteString -> b)
pg Map ByteString (ByteString -> b) -> ByteString -> ByteString -> b
forall k a. Ord k => Map k a -> k -> a
M.! ByteString
fldID) ByteString
fldV
                            WSysVar (InVar Rep (s :*: j)
inV) -> (:*:) s j b -> Rep (s :*: j) -> b
forall a. (:*:) s j a -> Rep (s :*: j) -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index (:*:) s j b
input Rep (s :*: j)
inV
                            WSysVar (NewVar NewVar
nV) -> Map NewVar b
wg Map NewVar b -> NewVar -> b
forall k a. Ord k => Map k a -> k -> a
M.! NewVar
nV
                        ))
                     (Var b j -> b
evalVar (Var b j -> b) -> s (Var b j) -> s b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> s (Var b j)
foldSeed, CircuitWitness b q j -> b
evalWitness (CircuitWitness b q j -> b) -> p (CircuitWitness b q j) -> p b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> p (CircuitWitness b q j)
foldSeedP)
                     [j (CircuitWitness b q j)]
foldList
            in ([(ByteString, b)] -> Map ByteString b
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(ByteString, b)] -> Map ByteString b)
-> [(ByteString, b)] -> Map ByteString b
forall a b. (a -> b) -> a -> b
$ s (ByteString, b) -> [(ByteString, b)]
forall a. s a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (s (ByteString, b) -> [(ByteString, b)])
-> s (ByteString, b) -> [(ByteString, b)]
forall a b. (a -> b) -> a -> b
$ s ByteString -> s b -> s (ByteString, b)
forall (f :: Type -> Type) a b.
Representable f =>
f a -> f b -> f (a, b)
mzipRep ((Rep s -> ByteString) -> s ByteString
forall a. (Rep s -> a) -> s a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep s -> ByteString
forall a. Binary a => a -> ByteString
toByteString) s b
resultL,
                p b -> Rep p -> b
forall a. p a -> Rep p -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index p b
resultP (Rep p -> b) -> (ByteString -> Rep p) -> ByteString -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (Rep p) -> Rep p
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Rep p) -> Rep p)
-> (ByteString -> Maybe (Rep p)) -> ByteString -> Rep p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Maybe (Rep p)
forall a. Binary a => ByteString -> Maybe a
fromByteString)
        in ((ByteString -> NewVar) -> Map ByteString b -> Map NewVar b
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeysMonotonic ByteString -> NewVar
EqVar Map ByteString b
eqVars
            Map NewVar b -> Map NewVar b -> Map NewVar b
forall a. Semigroup a => a -> a -> a
<> Map ByteString (Map NewVar b) -> Map NewVar b
forall (f :: Type -> Type) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ((ByteString -> (Map ByteString b, ByteString -> b) -> Map NewVar b)
-> Map ByteString (Map ByteString b, ByteString -> b)
-> Map ByteString (Map NewVar b)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (((Map ByteString b -> Map NewVar b)
-> ((Map ByteString b, ByteString -> b) -> Map ByteString b)
-> (Map ByteString b, ByteString -> b)
-> Map NewVar b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ByteString b, ByteString -> b) -> Map ByteString b
forall a b. (a, b) -> a
fst) ((Map ByteString b -> Map NewVar b)
 -> (Map ByteString b, ByteString -> b) -> Map NewVar b)
-> (ByteString -> Map ByteString b -> Map NewVar b)
-> ByteString
-> (Map ByteString b, ByteString -> b)
-> Map NewVar b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ByteString -> NewVar) -> Map ByteString b -> Map NewVar b
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeysMonotonic ((ByteString -> NewVar) -> Map ByteString b -> Map NewVar b)
-> (ByteString -> ByteString -> NewVar)
-> ByteString
-> Map ByteString b
-> Map NewVar b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString -> NewVar
FoldVar) Map ByteString (Map ByteString b, ByteString -> b)
foldVars),
            (Map ByteString b, ByteString -> b) -> ByteString -> b
forall a b. (a, b) -> b
snd ((Map ByteString b, ByteString -> b) -> ByteString -> b)
-> Map ByteString (Map ByteString b, ByteString -> b)
-> Map ByteString (ByteString -> b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map ByteString (Map ByteString b, ByteString -> b)
foldVars)

-- | Evaluates the arithmetic circuit with one output using the supplied input map.
eval1 ::
  (Arithmetic a, Binary 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, Binary 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, Binary 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, Binary 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, Binary 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, Binary 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, Binary a) => ArithmeticCircuit a U1 U1 Par1 -> a
exec1 :: forall a.
(Arithmetic a, Binary 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, Binary 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, Binary a, Functor o) => ArithmeticCircuit a U1 U1 o -> o a
exec :: forall a (o :: Type -> Type).
(Arithmetic a, Binary 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, Binary 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 NewVar
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 (NewVar -> SysVar j
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar NewVar
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 NewVar
v)        = SysVar j -> Poly a (SysVar j) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var (NewVar -> SysVar j
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar NewVar
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 NewVar
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 (NewVar -> SysVar j
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar NewVar
v)
    witF (WFoldVar ByteString
i 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 (ByteString -> ByteString -> WitVar p j
forall (p :: Type -> Type) (i :: Type -> Type).
ByteString -> ByteString -> WitVar p i
WFoldVar ByteString
i 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 NewVar
v        -> SysVar j -> Maybe (SysVar j)
forall a. a -> Maybe a
Just (NewVar -> SysVar j
forall (i :: Type -> Type). NewVar -> SysVar i
NewVar NewVar
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