{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wno-orphans     #-}

module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Instance where

import           Data.Aeson                                                hiding (Bool)
import           Data.Map                                                  hiding (drop, foldl, foldl', foldr, map,
                                                                            null, splitAt, take)
import           Data.Zip                                                  (zipWith)
import           Numeric.Natural                                           (Natural)
import           Prelude                                                   (Integer, const, error, mempty, pure, return,
                                                                            show, ($), (++), (<$>), (<*>), (>>=))
import qualified Prelude                                                   as Haskell
import           System.Random                                             (mkStdGen)
import           Test.QuickCheck                                           (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Combinators    (embed, expansion, horner, invertC, isZeroC)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal       hiding (constraint)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.MonadBlueprint (MonadBlueprint (..), circuit, circuits)
import           ZkFold.Symbolic.Compiler.Arithmetizable                   (SymbolicData (..))
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.DiscreteField
import           ZkFold.Symbolic.Data.Eq

------------------------------------- Instances -------------------------------------

instance Arithmetic a => SymbolicData a (ArithmeticCircuit a) where
    pieces :: ArithmeticCircuit a -> [ArithmeticCircuit a]
pieces ArithmeticCircuit a
r = [ArithmeticCircuit a
r]

    restore :: [ArithmeticCircuit a] -> ArithmeticCircuit a
restore [ArithmeticCircuit a
r] = ArithmeticCircuit a
r
    restore [ArithmeticCircuit a]
_   = [Char] -> ArithmeticCircuit a
forall a. HasCallStack => [Char] -> a
error [Char]
"restore ArithmeticCircuit: wrong number of arguments"

    typeSize :: Natural
typeSize = Natural
1

instance FiniteField a => Finite (ArithmeticCircuit a) where
    type Order (ArithmeticCircuit a) = Order a

instance Arithmetic a => AdditiveSemigroup (ArithmeticCircuit a) where
    ArithmeticCircuit a
r1 + :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
+ ArithmeticCircuit a
r2 = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r1
        i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r2
        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
x -> i -> x
x i
i x -> x -> x
forall a. AdditiveSemigroup a => a -> a -> a
+ i -> x
x i
j)

instance (Arithmetic a, Scale c a) => Scale c (ArithmeticCircuit a) where
    scale :: c -> ArithmeticCircuit a -> ArithmeticCircuit a
scale c
c ArithmeticCircuit a
r = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r
        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
x -> (c
c c -> a -> a
forall b a. Scale b a => b -> a -> a
`scale` a
forall a. MultiplicativeMonoid a => a
one :: a) a -> x -> x
forall b a. Scale b a => b -> a -> a
`scale` i -> x
x i
i)

instance Arithmetic a => AdditiveMonoid (ArithmeticCircuit a) where
    zero :: ArithmeticCircuit a
zero = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (x -> (i -> x) -> x
forall a b. a -> b -> a
const x
forall a. AdditiveMonoid a => a
zero)

instance Arithmetic a => AdditiveGroup (ArithmeticCircuit a) where
    negate :: ArithmeticCircuit a -> ArithmeticCircuit a
negate ArithmeticCircuit a
r = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r
        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
x -> x -> x
forall a. AdditiveGroup a => a -> a
negate (i -> x
x i
i))

    ArithmeticCircuit a
r1 - :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
- ArithmeticCircuit a
r2 = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r1
        i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r2
        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
x -> i -> x
x i
i x -> x -> x
forall a. AdditiveGroup a => a -> a -> a
- i -> x
x i
j)

instance Arithmetic a => MultiplicativeSemigroup (ArithmeticCircuit a) where
    ArithmeticCircuit a
r1 * :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
* ArithmeticCircuit a
r2 = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ do
        i
i <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r1
        i
j <- ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r2
        ClosedPoly i a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ClosedPoly i a -> m i
newAssigned (\i -> x
x -> i -> x
x i
i x -> x -> x
forall a. MultiplicativeSemigroup a => a -> a -> a
* i -> x
x i
j)

instance Arithmetic a => Exponent (ArithmeticCircuit a) Natural where
    ^ :: ArithmeticCircuit a -> Natural -> ArithmeticCircuit a
(^) = ArithmeticCircuit a -> Natural -> ArithmeticCircuit a
forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow

instance Arithmetic a => MultiplicativeMonoid (ArithmeticCircuit a) where
    one :: ArithmeticCircuit a
one = ArithmeticCircuit a
forall a. Monoid a => a
mempty

instance (Arithmetic a, FromConstant b a) => FromConstant b (ArithmeticCircuit a) where
    fromConstant :: b -> ArithmeticCircuit a
fromConstant b
c = a -> ArithmeticCircuit a
forall a. Arithmetic a => a -> ArithmeticCircuit a
embed (b -> a
forall a b. FromConstant a b => a -> b
fromConstant b
c)

instance Arithmetic a => Semiring (ArithmeticCircuit a)

instance Arithmetic a => Ring (ArithmeticCircuit a)

instance Arithmetic a => Exponent (ArithmeticCircuit a) Integer where
    ^ :: ArithmeticCircuit a -> Integer -> ArithmeticCircuit a
(^) = ArithmeticCircuit a -> Integer -> ArithmeticCircuit a
forall a. Field a => a -> Integer -> a
intPowF

instance Arithmetic a => Field (ArithmeticCircuit a) where
    finv :: ArithmeticCircuit a -> ArithmeticCircuit a
finv = ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
ArithmeticCircuit a -> ArithmeticCircuit a
invertC
    rootOfUnity :: Natural -> Maybe (ArithmeticCircuit a)
rootOfUnity Natural
n = a -> ArithmeticCircuit a
forall a. Arithmetic a => a -> ArithmeticCircuit a
embed (a -> ArithmeticCircuit a)
-> Maybe a -> Maybe (ArithmeticCircuit a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Natural -> Maybe a
forall a. Field a => Natural -> Maybe a
rootOfUnity Natural
n

instance Arithmetic a => BinaryExpansion (ArithmeticCircuit a) where
    binaryExpansion :: ArithmeticCircuit a -> [ArithmeticCircuit a]
binaryExpansion ArithmeticCircuit a
r = (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a (f :: Type -> Type).
(Arithmetic a, Functor f) =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m (f i))
-> f (ArithmeticCircuit a)
circuits ((forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
 -> [ArithmeticCircuit a])
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m [i])
-> [ArithmeticCircuit a]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit ArithmeticCircuit a
r m i -> (i -> m [i]) -> m [i]
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Natural -> i -> m [i]
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
Natural -> i -> m [i]
expansion (forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits @a)
    fromBinary :: [ArithmeticCircuit a] -> ArithmeticCircuit a
fromBinary [ArithmeticCircuit a]
bits = (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a.
Arithmetic a =>
(forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
circuit ((forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
 -> ArithmeticCircuit a)
-> (forall i (m :: Type -> Type). MonadBlueprint i a m => m i)
-> ArithmeticCircuit a
forall a b. (a -> b) -> a -> b
$ (ArithmeticCircuit a -> m i) -> [ArithmeticCircuit a] -> m [i]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
Haskell.traverse ArithmeticCircuit a -> m i
forall i a (m :: Type -> Type).
MonadBlueprint i a m =>
ArithmeticCircuit a -> m i
runCircuit [ArithmeticCircuit a]
bits m [i] -> ([i] -> m i) -> m i
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= [i] -> m i
forall i a (m :: Type -> Type). MonadBlueprint i a m => [i] -> m i
horner

instance Arithmetic a => DiscreteField' (ArithmeticCircuit a) where
    equal :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
equal ArithmeticCircuit a
r1 ArithmeticCircuit a
r2 = ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
ArithmeticCircuit a -> ArithmeticCircuit a
isZeroC (ArithmeticCircuit a
r1 ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
r2)

instance Arithmetic a => TrichotomyField (ArithmeticCircuit a) where
    trichotomy :: ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
trichotomy ArithmeticCircuit a
r1 ArithmeticCircuit a
r2 =
        let
            bits1 :: [ArithmeticCircuit a]
bits1 = ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion ArithmeticCircuit a
r1
            bits2 :: [ArithmeticCircuit a]
bits2 = ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion ArithmeticCircuit a
r2
            zipWith0 :: (t -> t -> a) -> [t] -> [t] -> [a]
zipWith0 t -> t -> a
_ [] []         = []
            zipWith0 t -> t -> a
f [] [t]
ys         = (t -> t -> a) -> [t] -> [t] -> [a]
zipWith0 t -> t -> a
f [t
forall a. AdditiveMonoid a => a
zero] [t]
ys
            zipWith0 t -> t -> a
f [t]
xs []         = (t -> t -> a) -> [t] -> [t] -> [a]
zipWith0 t -> t -> a
f [t]
xs [t
forall a. AdditiveMonoid a => a
zero]
            zipWith0 t -> t -> a
f (t
x:[t]
xs) (t
y:[t]
ys) = t -> t -> a
f t
x t
y a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (t -> t -> a) -> [t] -> [t] -> [a]
zipWith0 t -> t -> a
f [t]
xs [t]
ys
            -- zip pairs of bits in {0,1} to orderings in {-1,0,1}
            comparedBits :: [ArithmeticCircuit a]
comparedBits = (ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
forall {t} {t} {a}.
(AdditiveMonoid t, AdditiveMonoid t) =>
(t -> t -> a) -> [t] -> [t] -> [a]
zipWith0 (-) [ArithmeticCircuit a]
bits1 [ArithmeticCircuit a]
bits2
            -- least significant bit first,
            -- reverse lexicographical ordering
            reverseLexicographical :: a -> a -> a
reverseLexicographical a
x a
y = a
y a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
y a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* (a
y a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
x) a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
x
        in
            (ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> ArithmeticCircuit a
-> [ArithmeticCircuit a]
-> ArithmeticCircuit a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Haskell.foldl ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall {a}.
(MultiplicativeSemigroup a, AdditiveGroup a) =>
a -> a -> a
reverseLexicographical ArithmeticCircuit a
forall a. AdditiveMonoid a => a
zero [ArithmeticCircuit a]
comparedBits

instance Arithmetic a => SymbolicData a (Bool (ArithmeticCircuit a)) where
    pieces :: Bool (ArithmeticCircuit a) -> [ArithmeticCircuit a]
pieces (Bool ArithmeticCircuit a
b) = ArithmeticCircuit a -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces ArithmeticCircuit a
b
    restore :: [ArithmeticCircuit a] -> Bool (ArithmeticCircuit a)
restore = ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
forall x. x -> Bool x
Bool (ArithmeticCircuit a -> Bool (ArithmeticCircuit a))
-> ([ArithmeticCircuit a] -> ArithmeticCircuit a)
-> [ArithmeticCircuit a]
-> Bool (ArithmeticCircuit a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
Haskell.. [ArithmeticCircuit a] -> ArithmeticCircuit a
forall a x. SymbolicData a x => [ArithmeticCircuit a] -> x
restore
    typeSize :: Natural
typeSize = Natural
1

instance Arithmetic a => DiscreteField (Bool (ArithmeticCircuit a)) (ArithmeticCircuit a) where
    isZero :: ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
isZero ArithmeticCircuit a
x = ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
forall x. x -> Bool x
Bool (ArithmeticCircuit a -> ArithmeticCircuit a
forall a.
Arithmetic a =>
ArithmeticCircuit a -> ArithmeticCircuit a
isZeroC ArithmeticCircuit a
x)

instance Arithmetic a => Eq (Bool (ArithmeticCircuit a)) (ArithmeticCircuit a) where
    ArithmeticCircuit a
x == :: ArithmeticCircuit a
-> ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
== ArithmeticCircuit a
y = ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
forall b a. DiscreteField b a => a -> b
isZero (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
y)
    ArithmeticCircuit a
x /= :: ArithmeticCircuit a
-> ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
/= ArithmeticCircuit a
y = Bool (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall b. BoolType b => b -> b
not (Bool (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a))
-> Bool (ArithmeticCircuit a) -> Bool (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a -> Bool (ArithmeticCircuit a)
forall b a. DiscreteField b a => a -> b
isZero (ArithmeticCircuit a
x ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
y)

instance {-# OVERLAPPING #-} SymbolicData a x => Conditional (Bool (ArithmeticCircuit a)) x where
    bool :: x -> x -> Bool (ArithmeticCircuit a) -> x
bool x
brFalse x
brTrue (Bool ArithmeticCircuit a
b) =
        let f' :: [ArithmeticCircuit a]
f' = x -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces x
brFalse
            t' :: [ArithmeticCircuit a]
t' = x -> [ArithmeticCircuit a]
forall a x. SymbolicData a x => x -> [ArithmeticCircuit a]
pieces x
brTrue
        in [ArithmeticCircuit a] -> x
forall a x. SymbolicData a x => [ArithmeticCircuit a] -> x
restore ([ArithmeticCircuit a] -> x) -> [ArithmeticCircuit a] -> x
forall a b. (a -> b) -> a -> b
$ (ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a)
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
-> [ArithmeticCircuit a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (\ArithmeticCircuit a
f ArithmeticCircuit a
t -> ArithmeticCircuit a
b ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ArithmeticCircuit a
t ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveGroup a => a -> a -> a
- ArithmeticCircuit a
f) ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. AdditiveSemigroup a => a -> a -> a
+ ArithmeticCircuit a
f) [ArithmeticCircuit a]
f' [ArithmeticCircuit a]
t'

-- TODO: make a proper implementation of Arbitrary
instance Arithmetic a => Arbitrary (ArithmeticCircuit a) where
    arbitrary :: Gen (ArithmeticCircuit a)
arbitrary = do
        let ac :: ArithmeticCircuit a
ac = ArithmeticCircuit a
forall a. Monoid a => a
mempty { acOutput = 1} ArithmeticCircuit a -> ArithmeticCircuit a -> ArithmeticCircuit a
forall a. MultiplicativeSemigroup a => a -> a -> a
* ArithmeticCircuit a
forall a. Monoid a => a
mempty { acOutput = 2}
        ArithmeticCircuit a -> Gen (ArithmeticCircuit a)
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ArithmeticCircuit a
ac

-- TODO: make it more readable
instance (FiniteField a, Haskell.Eq a, Haskell.Show a) => Haskell.Show (ArithmeticCircuit a) where
    show :: ArithmeticCircuit a -> [Char]
show ArithmeticCircuit a
r = [Char]
"ArithmeticCircuit { acSystem = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Map Natural (Constraint a) -> [Char]
forall a. Show a => a -> [Char]
show (ArithmeticCircuit a -> Map Natural (Constraint a)
forall a. ArithmeticCircuit a -> Map Natural (Constraint a)
acSystem ArithmeticCircuit a
r) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", acInput = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Natural] -> [Char]
forall a. Show a => a -> [Char]
show (ArithmeticCircuit a -> [Natural]
forall a. ArithmeticCircuit a -> [Natural]
acInput ArithmeticCircuit a
r) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", acOutput = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show (ArithmeticCircuit a -> Natural
forall a. ArithmeticCircuit a -> Natural
acOutput ArithmeticCircuit a
r) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", acVarOrder = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Map (Natural, Natural) Natural -> [Char]
forall a. Show a => a -> [Char]
show (ArithmeticCircuit a -> Map (Natural, Natural) Natural
forall a. ArithmeticCircuit a -> Map (Natural, Natural) Natural
acVarOrder ArithmeticCircuit a
r) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" }"

-- TODO: add witness generation info to the JSON object
instance ToJSON a => ToJSON (ArithmeticCircuit a) where
    toJSON :: ArithmeticCircuit a -> Value
toJSON ArithmeticCircuit a
r = [Pair] -> Value
object
        [
            Key
"system" Key -> Map Natural (Constraint a) -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ArithmeticCircuit a -> Map Natural (Constraint a)
forall a. ArithmeticCircuit a -> Map Natural (Constraint a)
acSystem ArithmeticCircuit a
r,
            Key
"input"  Key -> [Natural] -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ArithmeticCircuit a -> [Natural]
forall a. ArithmeticCircuit a -> [Natural]
acInput ArithmeticCircuit a
r,
            Key
"output" Key -> Natural -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ArithmeticCircuit a -> Natural
forall a. ArithmeticCircuit a -> Natural
acOutput ArithmeticCircuit a
r,
            Key
"order"  Key -> Map (Natural, Natural) Natural -> Pair
forall v. ToJSON v => Key -> v -> Pair
forall e kv v. (KeyValue e kv, ToJSON v) => Key -> v -> kv
.= ArithmeticCircuit a -> Map (Natural, Natural) Natural
forall a. ArithmeticCircuit a -> Map (Natural, Natural) Natural
acVarOrder ArithmeticCircuit a
r
        ]

-- TODO: properly restore the witness generation function
instance FromJSON a => FromJSON (ArithmeticCircuit a) where
    parseJSON :: Value -> Parser (ArithmeticCircuit a)
parseJSON = [Char]
-> (Object -> Parser (ArithmeticCircuit a))
-> Value
-> Parser (ArithmeticCircuit a)
forall a. [Char] -> (Object -> Parser a) -> Value -> Parser a
withObject [Char]
"ArithmeticCircuit" ((Object -> Parser (ArithmeticCircuit a))
 -> Value -> Parser (ArithmeticCircuit a))
-> (Object -> Parser (ArithmeticCircuit a))
-> Value
-> Parser (ArithmeticCircuit a)
forall a b. (a -> b) -> a -> b
$ \Object
v -> Map Natural (Constraint a)
-> [Natural]
-> (Map Natural a -> Map Natural a)
-> Natural
-> Map (Natural, Natural) Natural
-> StdGen
-> ArithmeticCircuit a
forall a.
Map Natural (Constraint a)
-> [Natural]
-> (Map Natural a -> Map Natural a)
-> Natural
-> Map (Natural, Natural) Natural
-> StdGen
-> ArithmeticCircuit a
ArithmeticCircuit
        (Map Natural (Constraint a)
 -> [Natural]
 -> (Map Natural a -> Map Natural a)
 -> Natural
 -> Map (Natural, Natural) Natural
 -> StdGen
 -> ArithmeticCircuit a)
-> Parser (Map Natural (Constraint a))
-> Parser
     ([Natural]
      -> (Map Natural a -> Map Natural a)
      -> Natural
      -> Map (Natural, Natural) Natural
      -> StdGen
      -> ArithmeticCircuit a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Key -> Parser (Map Natural (Constraint a))
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"system"
        Parser
  ([Natural]
   -> (Map Natural a -> Map Natural a)
   -> Natural
   -> Map (Natural, Natural) Natural
   -> StdGen
   -> ArithmeticCircuit a)
-> Parser [Natural]
-> Parser
     ((Map Natural a -> Map Natural a)
      -> Natural
      -> Map (Natural, Natural) Natural
      -> StdGen
      -> ArithmeticCircuit a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser [Natural]
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"input"
        Parser
  ((Map Natural a -> Map Natural a)
   -> Natural
   -> Map (Natural, Natural) Natural
   -> StdGen
   -> ArithmeticCircuit a)
-> Parser (Map Natural a -> Map Natural a)
-> Parser
     (Natural
      -> Map (Natural, Natural) Natural -> StdGen -> ArithmeticCircuit a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Map Natural a -> Map Natural a)
-> Parser (Map Natural a -> Map Natural a)
forall a. a -> Parser a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Map Natural a -> Map Natural a -> Map Natural a
forall a b. a -> b -> a
const Map Natural a
forall k a. Map k a
empty)
        Parser
  (Natural
   -> Map (Natural, Natural) Natural -> StdGen -> ArithmeticCircuit a)
-> Parser Natural
-> Parser
     (Map (Natural, Natural) Natural -> StdGen -> ArithmeticCircuit a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser Natural
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"output"
        Parser
  (Map (Natural, Natural) Natural -> StdGen -> ArithmeticCircuit a)
-> Parser (Map (Natural, Natural) Natural)
-> Parser (StdGen -> ArithmeticCircuit a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Object
v Object -> Key -> Parser (Map (Natural, Natural) Natural)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"order"
        Parser (StdGen -> ArithmeticCircuit a)
-> Parser StdGen -> Parser (ArithmeticCircuit a)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> StdGen -> Parser StdGen
forall a. a -> Parser a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Int -> StdGen
mkStdGen Int
0)