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

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal (
        ArithmeticCircuit(..),
        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
    ) where

import           Control.DeepSeq                                       (NFData)
import           Control.Monad.State                                   (State, modify, runState)
import           Data.Aeson
import           Data.Binary                                           (Binary)
import           Data.ByteString                                       (ByteString)
import           Data.Foldable                                         (fold, toList)
import           Data.Functor.Rep
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.Witness
import           ZkFold.Symbolic.MonadCircuit

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

-- | 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 (WitnessF a (WitVar p i))
acWitness :: Map ByteString (WitnessF a (WitVar p i)),
        -- ^ The witness generation functions
        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, NFData (o (Var a i)), NFData (Rep i))
    => NFData (ArithmeticCircuit a p i o)

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

data SysVar i
  = InVar (Rep i)
  | NewVar ByteString
  deriving (forall x. SysVar i -> Rep (SysVar i) x)
-> (forall x. Rep (SysVar i) x -> SysVar i) -> Generic (SysVar i)
forall x. Rep (SysVar i) x -> SysVar i
forall x. SysVar i -> Rep (SysVar i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (i :: Type -> Type) x. Rep (SysVar i) x -> SysVar i
forall (i :: Type -> Type) x. SysVar i -> Rep (SysVar i) x
$cfrom :: forall (i :: Type -> Type) x. SysVar i -> Rep (SysVar i) x
from :: forall x. SysVar i -> Rep (SysVar i) x
$cto :: forall (i :: Type -> Type) x. Rep (SysVar i) x -> SysVar i
to :: forall x. Rep (SysVar i) x -> SysVar i
Generic
deriving anyclass instance FromJSON (Rep i) => FromJSON (SysVar i)
deriving anyclass instance FromJSON (Rep i) => FromJSONKey (SysVar i)
deriving anyclass instance ToJSON (Rep i) => ToJSONKey (SysVar i)
deriving anyclass instance ToJSON (Rep i) => ToJSON (SysVar i)
deriving stock instance Show (Rep i) => Show (SysVar i)
deriving stock instance Eq (Rep i) => Eq (SysVar i)
deriving stock instance Ord (Rep i) => Ord (SysVar i)
deriving instance NFData (Rep i) => NFData (SysVar i)

imapSysVar ::
  (Representable i, Representable j) =>
  (forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar :: forall (i :: Type -> Type) (j :: Type -> Type).
(Representable i, Representable j) =>
(forall x. j x -> i x) -> SysVar i -> SysVar j
imapSysVar forall x. j x -> i x
f (InVar Rep i
r)  = i (SysVar j) -> Rep i -> SysVar j
forall a. i a -> Rep i -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
index (j (SysVar j) -> i (SysVar j)
forall x. j x -> i x
f ((Rep j -> SysVar j) -> j (SysVar j)
forall a. (Rep j -> a) -> j a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate Rep j -> SysVar j
forall (i :: Type -> Type). Rep i -> SysVar i
InVar)) Rep i
r
imapSysVar forall x. j x -> i x
_ (NewVar ByteString
b) = ByteString -> SysVar j
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar ByteString
b

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

data Var a i
  = SysVar (SysVar i)
  | ConstVar a
  deriving (forall x. Var a i -> Rep (Var a i) x)
-> (forall x. Rep (Var a i) x -> Var a i) -> Generic (Var a i)
forall x. Rep (Var a i) x -> Var a i
forall x. Var a i -> Rep (Var a i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a (i :: Type -> Type) x. Rep (Var a i) x -> Var a i
forall a (i :: Type -> Type) x. Var a i -> Rep (Var a i) x
$cfrom :: forall a (i :: Type -> Type) x. Var a i -> Rep (Var a i) x
from :: forall x. Var a i -> Rep (Var a i) x
$cto :: forall a (i :: Type -> Type) x. Rep (Var a i) x -> Var a i
to :: forall x. Rep (Var a i) x -> Var a i
Generic
deriving anyclass instance (FromJSON (Rep i), FromJSON a) => FromJSON (Var a i)
deriving anyclass instance (FromJSON (Rep i), FromJSON a) => FromJSONKey (Var a i)
deriving anyclass instance (ToJSON (Rep i), ToJSON a) => ToJSONKey (Var a i)
deriving anyclass instance (ToJSON (Rep i), ToJSON a) => ToJSON (Var a i)
deriving stock instance (Show (Rep i), Show a) => Show (Var a i)
deriving stock instance (Eq (Rep i), Eq a) => Eq (Var a i)
deriving stock instance (Ord (Rep i), Ord a) => Ord (Var a i)
deriving instance (NFData (Rep i), NFData a) => NFData (Var a i)
instance FromConstant a (Var a i) where
    fromConstant :: a -> Var a i
fromConstant = a -> Var a i
forall a (i :: Type -> Type). a -> Var a i
ConstVar

imapVar ::
  (Representable i, Representable j) =>
  (forall x. j x -> i x) -> Var a i -> Var a j
imapVar :: 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 forall x. j x -> i x
f (SysVar SysVar i
s)   = SysVar j -> Var a j
forall a (i :: Type -> Type). SysVar i -> Var a i
SysVar ((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
s)
imapVar forall x. j x -> i x
_ (ConstVar a
c) = a -> Var a j
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
c

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

acInput :: Representable i => i (Var a i)
acInput :: forall (i :: Type -> Type) a. Representable i => 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). SysVar i -> Var a i
SysVar (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 (WitnessF a (WitVar p i)) -> [ByteString]
forall k a. Map k a -> [k]
keys (Map ByteString (WitnessF a (WitVar p i)) -> [ByteString])
-> Map ByteString (WitnessF a (WitVar p i)) -> [ByteString]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a p i o
-> Map ByteString (WitnessF a (WitVar p i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o
-> Map ByteString (WitnessF a (WitVar 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
  SysVar (InVar Rep i
inV) -> 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
  SysVar (NewVar ByteString
newV) -> a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe
    (String -> a
forall a. HasCallStack => String -> a
error (String
"no such NewVar: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ByteString -> String
forall a. Show a => a -> String
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 (WitnessF a (WitVar p i))
w 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 (WitnessF a (WitVar p j))
acWitness = (WitVar p i -> WitVar p j)
-> WitnessF a (WitVar p i) -> WitnessF a (WitVar 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) (WitnessF a (WitVar p i) -> WitnessF a (WitVar p j))
-> Map ByteString (WitnessF a (WitVar p i))
-> Map ByteString (WitnessF a (WitVar p j))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Map ByteString (WitnessF a (WitVar p i))
w
  , 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 }

--------------------------- 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
c, f (Var a i)
o)) = f (Var a i)
o f (Var a i)
-> (Var a i -> WitnessF a (WitVar p i))
-> f (WitnessF a (WitVar p i))
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      ConstVar a
cv -> a -> WitnessF a (WitVar p i)
forall a b. FromConstant a b => a -> b
fromConstant a
cv
      SysVar (InVar Rep i
iv) -> 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))
-> Var a i -> WitnessF a (WitVar p i)
forall a b. (a -> b) -> a -> b
$ SysVar i -> Var a i
forall a (i :: Type -> Type). SysVar i -> Var a i
SysVar (Rep i -> SysVar i
forall (i :: Type -> Type). Rep i -> SysVar i
InVar Rep i
iv)
      SysVar (NewVar ByteString
nv) -> ArithmeticCircuit a p i U1
-> Map ByteString (WitnessF a (WitVar p i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o
-> Map ByteString (WitnessF a (WitVar p i))
acWitness ArithmeticCircuit a p i U1
c Map ByteString (WitnessF a (WitVar p i))
-> ByteString -> WitnessF a (WitVar p i)
forall k a. Ord k => Map k a -> k -> a
! ByteString
nv
    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) (WitnessF a (WitVar p i)) where
  at :: Var a i -> WitnessF a (WitVar p i)
at (ConstVar a
cV) = a -> WitnessF a (WitVar p i)
forall a b. FromConstant a b => a -> b
fromConstant a
cV
  at (SysVar SysVar i
sV)   = (forall n w. IsWitness a n w => (WitVar p i -> w) -> w)
-> WitnessF a (WitVar p i)
forall a v.
(forall n w. IsWitness a n w => (v -> w) -> w) -> WitnessF a v
WitnessF (\WitVar p i -> w
x -> WitVar p i -> w
x (SysVar i -> WitVar p i
forall (p :: Type -> Type) (i :: Type -> Type).
SysVar i -> WitVar p i
WSysVar SysVar i
sV))

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

    unconstrained :: WitnessF a (WitVar p i)
-> State (ArithmeticCircuit a p i o) (Var a i)
unconstrained WitnessF a (WitVar p i)
wf = case WitnessF a (WitVar 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 WitnessF a (WitVar p i)
wf ((WitVar p i -> Maybe a) -> Maybe a)
-> (WitVar p i -> Maybe a) -> Maybe a
forall a b. (a -> b) -> a -> b
$ Maybe a -> WitVar p i -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing of
      Just a
cV -> 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
cV)
      Maybe a
Nothing -> 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
toVar @a WitnessF a (WitVar p i)
wf
        -- TODO: forbid reassignment of variables
        Optic'
  A_Lens
  NoIx
  (ArithmeticCircuit a p i U1)
  (Map ByteString (WitnessF a (WitVar p i)))
-> StateT (Map ByteString (WitnessF a (WitVar 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 (WitnessF a (WitVar p i)))
-> StateT (Map ByteString (WitnessF a (WitVar 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 (WitnessF a (WitVar p i)))
#acWitness (StateT (Map ByteString (WitnessF a (WitVar p i))) Identity ()
 -> State (ArithmeticCircuit a p i o) ())
-> StateT (Map ByteString (WitnessF a (WitVar p i))) Identity ()
-> State (ArithmeticCircuit a p i o) ()
forall a b. (a -> b) -> a -> b
$ (Map ByteString (WitnessF a (WitVar p i))
 -> Map ByteString (WitnessF a (WitVar p i)))
-> StateT (Map ByteString (WitnessF a (WitVar p i))) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (ByteString
-> WitnessF a (WitVar p i)
-> Map ByteString (WitnessF a (WitVar p i))
-> Map ByteString (WitnessF a (WitVar p i))
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert ByteString
v WitnessF a (WitVar 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). SysVar i -> Var a i
SysVar (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
            SysVar SysVar i
sysV -> SysVar i -> Constraint a i
forall c i j. Polynomial c i j => i -> Poly c i j
var SysVar i
sysV
            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
            SysVar SysVar i
_ -> Maybe a
forall a. Maybe a
Nothing
            ConstVar a
cV -> a -> Maybe a
forall a. a -> Maybe a
Just a
cV
      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 String -> State (ArithmeticCircuit a p i o) ()
forall a. HasCallStack => String -> a
error String
"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
toVar @_ @p ((Var a i -> WitnessF a (WitVar p i)) -> WitnessF a (WitVar p i)
ClosedPoly (Var a i) a
p Var a i -> WitnessF a (WitVar 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 (SysVar SysVar i
v) a
upperBound =
      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)
    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 String -> State (ArithmeticCircuit a p i o) ()
forall a. HasCallStack => String -> a
error String
"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.
toVar ::
  forall a p i. (Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
  WitnessF a (WitVar p i) -> ByteString
toVar :: forall a (p :: Type -> Type) (i :: Type -> Type).
(Finite a, Binary a, Binary (Rep p), Binary (Rep i)) =>
WitnessF a (WitVar p i) -> ByteString
toVar (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 (WitnessF a (WitVar p i))
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
ArithmeticCircuit a p i o
-> Map ByteString (WitnessF a (WitVar p i))
acWitness ArithmeticCircuit a p i o
circuit Map ByteString (WitnessF a (WitVar p i))
-> (WitnessF a (WitVar p i) -> a) -> Map ByteString a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \WitnessF a (WitVar p i)
k -> WitnessF a (WitVar 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 WitnessF a (WitVar 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) =>
  i a -> ArithmeticCircuit a p (i :*: j) U1 -> ArithmeticCircuit a p j U1
apply :: forall a (j :: Type -> Type) (i :: Type -> Type)
       (p :: Type -> Type).
(Eq a, Field a, Ord (Rep j), Representable i) =>
i a
-> ArithmeticCircuit a p (i :*: j) U1 -> ArithmeticCircuit a p j U1
apply i a
xs ArithmeticCircuit a p (i :*: j) U1
ac = ArithmeticCircuit a p (i :*: j) U1
ac
  { acSystem = fmap (evalPolynomial evalMonomial varF) (acSystem ac)
  , acRange = S.fromList . catMaybes . toList . filterSet <$> acRange ac
  , acWitness = (>>= witF) <$> acWitness ac
  , acOutput = U1
  }
  where
    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