{-# LANGUAGE OverloadedLists      #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Plonkup.PlonkConstraint where

import           Control.Monad                                       (guard, replicateM, return)
import           Data.Binary                                         (Binary)
import           Data.Containers.ListUtils                           (nubOrd)
import           Data.Eq                                             (Eq (..))
import           Data.Function                                       (($), (.))
import           Data.Functor                                        ((<$>))
import           Data.List                                           (find, head, map, permutations, sort, (!!), (++))
import           Data.Map                                            (Map)
import qualified Data.Map                                            as Map
import           Data.Maybe                                          (Maybe (..), fromMaybe, mapMaybe)
import           Data.Ord                                            (Ord)
import           GHC.IsList                                          (IsList (..))
import           GHC.TypeNats                                        (KnownNat)
import           Numeric.Natural                                     (Natural)
import           Test.QuickCheck                                     (Arbitrary (..))
import           Text.Show                                           (Show)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Polynomials.Multivariate        (Poly, evalMonomial, evalPolynomial, polynomial,
                                                                      var, variables)
import           ZkFold.Base.Data.ByteString                         (toByteString)
import           ZkFold.Base.Data.Vector                             (Vector)
import           ZkFold.Prelude                                      (length, take)
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

data PlonkConstraint i a = PlonkConstraint
    { forall (i :: Natural) a. PlonkConstraint i a -> a
qm :: a
    , forall (i :: Natural) a. PlonkConstraint i a -> a
ql :: a
    , forall (i :: Natural) a. PlonkConstraint i a -> a
qr :: a
    , forall (i :: Natural) a. PlonkConstraint i a -> a
qo :: a
    , forall (i :: Natural) a. PlonkConstraint i a -> a
qc :: a
    , forall (i :: Natural) a. PlonkConstraint i a -> Var a (Vector i)
x1 :: Var a (Vector i)
    , forall (i :: Natural) a. PlonkConstraint i a -> Var a (Vector i)
x2 :: Var a (Vector i)
    , forall (i :: Natural) a. PlonkConstraint i a -> Var a (Vector i)
x3 :: Var a (Vector i)
    }
    deriving (Int -> PlonkConstraint i a -> ShowS
[PlonkConstraint i a] -> ShowS
PlonkConstraint i a -> String
(Int -> PlonkConstraint i a -> ShowS)
-> (PlonkConstraint i a -> String)
-> ([PlonkConstraint i a] -> ShowS)
-> Show (PlonkConstraint i a)
forall (i :: Natural) a.
Show a =>
Int -> PlonkConstraint i a -> ShowS
forall (i :: Natural) a. Show a => [PlonkConstraint i a] -> ShowS
forall (i :: Natural) a. Show a => PlonkConstraint i a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (i :: Natural) a.
Show a =>
Int -> PlonkConstraint i a -> ShowS
showsPrec :: Int -> PlonkConstraint i a -> ShowS
$cshow :: forall (i :: Natural) a. Show a => PlonkConstraint i a -> String
show :: PlonkConstraint i a -> String
$cshowList :: forall (i :: Natural) a. Show a => [PlonkConstraint i a] -> ShowS
showList :: [PlonkConstraint i a] -> ShowS
Show, PlonkConstraint i a -> PlonkConstraint i a -> Bool
(PlonkConstraint i a -> PlonkConstraint i a -> Bool)
-> (PlonkConstraint i a -> PlonkConstraint i a -> Bool)
-> Eq (PlonkConstraint i a)
forall (i :: Natural) a.
(Eq a, KnownNat i) =>
PlonkConstraint i a -> PlonkConstraint i a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (i :: Natural) a.
(Eq a, KnownNat i) =>
PlonkConstraint i a -> PlonkConstraint i a -> Bool
== :: PlonkConstraint i a -> PlonkConstraint i a -> Bool
$c/= :: forall (i :: Natural) a.
(Eq a, KnownNat i) =>
PlonkConstraint i a -> PlonkConstraint i a -> Bool
/= :: PlonkConstraint i a -> PlonkConstraint i a -> Bool
Eq)

instance (Ord a, Arbitrary a, Binary a, KnownNat i) => Arbitrary (PlonkConstraint i a) where
    arbitrary :: Gen (PlonkConstraint i a)
arbitrary = do
        a
qm <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
        a
ql <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
        a
qr <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
        a
qo <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
        a
qc <- Gen a
forall a. Arbitrary a => Gen a
arbitrary
        let arbitraryNewVar :: Gen (Var a (Vector i))
arbitraryNewVar = SysVar (Vector i) -> Var a (Vector i)
forall a (i :: Type -> Type). SysVar i -> Var a i
SysVar (SysVar (Vector i) -> Var a (Vector i))
-> (a -> SysVar (Vector i)) -> a -> Var a (Vector i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> SysVar (Vector i)
forall (i :: Type -> Type). ByteString -> SysVar i
NewVar (ByteString -> SysVar (Vector i))
-> (a -> ByteString) -> a -> SysVar (Vector i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binary a => a -> ByteString
toByteString @a (a -> Var a (Vector i)) -> Gen a -> Gen (Var a (Vector i))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen a
forall a. Arbitrary a => Gen a
arbitrary
        [Var a (Vector i)]
xs <- [Var a (Vector i)] -> [Var a (Vector i)]
forall a. Ord a => [a] -> [a]
sort ([Var a (Vector i)] -> [Var a (Vector i)])
-> Gen [Var a (Vector i)] -> Gen [Var a (Vector i)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (Var a (Vector i)) -> Gen [Var a (Vector i)]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
3 Gen (Var a (Vector i))
arbitraryNewVar
        let x1 :: Var a (Vector i)
x1 = [Var a (Vector i)]
xs [Var a (Vector i)] -> Int -> Var a (Vector i)
forall a. HasCallStack => [a] -> Int -> a
!! Int
0; x2 :: Var a (Vector i)
x2 = [Var a (Vector i)]
xs [Var a (Vector i)] -> Int -> Var a (Vector i)
forall a. HasCallStack => [a] -> Int -> a
!! Int
1; x3 :: Var a (Vector i)
x3 = [Var a (Vector i)]
xs [Var a (Vector i)] -> Int -> Var a (Vector i)
forall a. HasCallStack => [a] -> Int -> a
!! Int
2
        PlonkConstraint i a -> Gen (PlonkConstraint i a)
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PlonkConstraint i a -> Gen (PlonkConstraint i a))
-> PlonkConstraint i a -> Gen (PlonkConstraint i a)
forall a b. (a -> b) -> a -> b
$ a
-> a
-> a
-> a
-> a
-> Var a (Vector i)
-> Var a (Vector i)
-> Var a (Vector i)
-> PlonkConstraint i a
forall (i :: Natural) a.
a
-> a
-> a
-> a
-> a
-> Var a (Vector i)
-> Var a (Vector i)
-> Var a (Vector i)
-> PlonkConstraint i a
PlonkConstraint a
qm a
ql a
qr a
qo a
qc Var a (Vector i)
x1 Var a (Vector i)
x2 Var a (Vector i)
x3

toPlonkConstraint :: forall a i . (Ord a, FiniteField a, KnownNat i) => Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a
toPlonkConstraint :: forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a (Vector i)) Natural
p =
    let xs :: [Maybe (Var a (Vector i))]
xs    = Var a (Vector i) -> Maybe (Var a (Vector i))
forall a. a -> Maybe a
Just (Var a (Vector i) -> Maybe (Var a (Vector i)))
-> [Var a (Vector i)] -> [Maybe (Var a (Vector i))]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Var a (Vector i)) -> [Item (Set (Var a (Vector i)))]
forall l. IsList l => l -> [Item l]
toList (Poly a (Var a (Vector i)) Natural -> Set (Var a (Vector i))
forall c v. Ord v => Poly c v Natural -> Set v
variables Poly a (Var a (Vector i)) Natural
p)
        perms :: [[Maybe (Var a (Vector i))]]
perms = [[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]]
forall a. Ord a => [a] -> [a]
nubOrd ([[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]])
-> [[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]]
forall a b. (a -> b) -> a -> b
$ ([Maybe (Var a (Vector i))] -> [Maybe (Var a (Vector i))])
-> [[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]]
forall a b. (a -> b) -> [a] -> [b]
map (Natural -> [Maybe (Var a (Vector i))] -> [Maybe (Var a (Vector i))]
forall a. HasCallStack => Natural -> [a] -> [a]
take Natural
3) ([[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]])
-> [[Maybe (Var a (Vector i))]] -> [[Maybe (Var a (Vector i))]]
forall a b. (a -> b) -> a -> b
$ [Maybe (Var a (Vector i))] -> [[Maybe (Var a (Vector i))]]
forall a. [a] -> [[a]]
permutations ([Maybe (Var a (Vector i))] -> [[Maybe (Var a (Vector i))]])
-> [Maybe (Var a (Vector i))] -> [[Maybe (Var a (Vector i))]]
forall a b. (a -> b) -> a -> b
$ case [Maybe (Var a (Vector i))] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [Maybe (Var a (Vector i))]
xs of
            Natural
0 -> [Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing, Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing, Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing]
            Natural
1 -> [Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing, Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing, [Maybe (Var a (Vector i))] -> Maybe (Var a (Vector i))
forall a. HasCallStack => [a] -> a
head [Maybe (Var a (Vector i))]
xs, [Maybe (Var a (Vector i))] -> Maybe (Var a (Vector i))
forall a. HasCallStack => [a] -> a
head [Maybe (Var a (Vector i))]
xs]
            Natural
2 -> [Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
forall a. Maybe a
Nothing] [Maybe (Var a (Vector i))]
-> [Maybe (Var a (Vector i))] -> [Maybe (Var a (Vector i))]
forall a. [a] -> [a] -> [a]
++ [Maybe (Var a (Vector i))]
xs [Maybe (Var a (Vector i))]
-> [Maybe (Var a (Vector i))] -> [Maybe (Var a (Vector i))]
forall a. [a] -> [a] -> [a]
++ [Maybe (Var a (Vector i))]
xs
            Natural
_ -> [Maybe (Var a (Vector i))]
xs [Maybe (Var a (Vector i))]
-> [Maybe (Var a (Vector i))] -> [Maybe (Var a (Vector i))]
forall a. [a] -> [a] -> [a]
++ [Maybe (Var a (Vector i))]
xs

        getCoef :: Map (Maybe (Var a (Vector i))) Natural -> a
        getCoef :: Map (Maybe (Var a (Vector i))) Natural -> a
getCoef Map (Maybe (Var a (Vector i))) Natural
m = case ((a, Map (Var a (Vector i)) Natural) -> Bool)
-> [(a, Map (Var a (Vector i)) Natural)]
-> Maybe (a, Map (Var a (Vector i)) Natural)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
find (\(a
_, Map (Var a (Vector i)) Natural
as) -> Map (Maybe (Var a (Vector i))) Natural
m Map (Maybe (Var a (Vector i))) Natural
-> Map (Maybe (Var a (Vector i))) Natural -> Bool
forall a. Eq a => a -> a -> Bool
== (Var a (Vector i) -> Maybe (Var a (Vector i)))
-> Map (Var a (Vector i)) Natural
-> Map (Maybe (Var a (Vector i))) Natural
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Var a (Vector i) -> Maybe (Var a (Vector i))
forall a. a -> Maybe a
Just Map (Var a (Vector i)) Natural
as) (Poly a (Var a (Vector i)) Natural
-> [Item (Poly a (Var a (Vector i)) Natural)]
forall l. IsList l => l -> [Item l]
toList Poly a (Var a (Vector i)) Natural
p) of
            Just (a
c, Map (Var a (Vector i)) Natural
_) -> a
c
            Maybe (a, Map (Var a (Vector i)) Natural)
_           -> a
forall a. AdditiveMonoid a => a
zero

        getCoefs :: [Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a)
        getCoefs :: [Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a)
getCoefs [Item [Maybe (Var a (Vector i))]
a, Item [Maybe (Var a (Vector i))]
b, Item [Maybe (Var a (Vector i))]
c] = do
            let xa :: [(Maybe (Var a (Vector i)), Natural)]
xa = [(Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
a, Natural
1)]
                xb :: [(Maybe (Var a (Vector i)), Natural)]
xb = [(Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
b, Natural
1)]
                xc :: [(Maybe (Var a (Vector i)), Natural)]
xc = [(Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
c, Natural
1)]
                xaxb :: [(Maybe (Var a (Vector i)), Natural)]
xaxb = [(Maybe (Var a (Vector i)), Natural)]
xa [(Maybe (Var a (Vector i)), Natural)]
-> [(Maybe (Var a (Vector i)), Natural)]
-> [(Maybe (Var a (Vector i)), Natural)]
forall a. [a] -> [a] -> [a]
++ [(Maybe (Var a (Vector i)), Natural)]
xb

                qm :: a
qm = Map (Maybe (Var a (Vector i))) Natural -> a
getCoef (Map (Maybe (Var a (Vector i))) Natural -> a)
-> Map (Maybe (Var a (Vector i))) Natural -> a
forall a b. (a -> b) -> a -> b
$ (Natural -> Natural -> Natural)
-> [(Maybe (Var a (Vector i)), Natural)]
-> Map (Maybe (Var a (Vector i))) Natural
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
(+) [(Maybe (Var a (Vector i)), Natural)]
xaxb
                ql :: a
ql = Map (Maybe (Var a (Vector i))) Natural -> a
getCoef (Map (Maybe (Var a (Vector i))) Natural -> a)
-> Map (Maybe (Var a (Vector i))) Natural -> a
forall a b. (a -> b) -> a -> b
$ [Item (Map (Maybe (Var a (Vector i))) Natural)]
-> Map (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Map (Maybe (Var a (Vector i))) Natural)]
xa
                qr :: a
qr = Map (Maybe (Var a (Vector i))) Natural -> a
getCoef (Map (Maybe (Var a (Vector i))) Natural -> a)
-> Map (Maybe (Var a (Vector i))) Natural -> a
forall a b. (a -> b) -> a -> b
$ [Item (Map (Maybe (Var a (Vector i))) Natural)]
-> Map (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Map (Maybe (Var a (Vector i))) Natural)]
xb
                qo :: a
qo = Map (Maybe (Var a (Vector i))) Natural -> a
getCoef (Map (Maybe (Var a (Vector i))) Natural -> a)
-> Map (Maybe (Var a (Vector i))) Natural -> a
forall a b. (a -> b) -> a -> b
$ [Item (Map (Maybe (Var a (Vector i))) Natural)]
-> Map (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Map (Maybe (Var a (Vector i))) Natural)]
xc
                qc :: a
qc = Map (Maybe (Var a (Vector i))) Natural -> a
getCoef Map (Maybe (Var a (Vector i))) Natural
forall k a. Map k a
Map.empty
            Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ ((Var a (Vector i) -> Poly a (Maybe (Var a (Vector i))) Natural)
 -> Mono (Var a (Vector i)) Natural
 -> Poly a (Maybe (Var a (Vector i))) Natural)
-> (Var a (Vector i) -> Poly a (Maybe (Var a (Vector i))) Natural)
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Maybe (Var a (Vector i))) Natural
forall c i j b.
(AdditiveMonoid b, Scale c b) =>
((i -> b) -> Mono i j -> b) -> (i -> b) -> Poly c i j -> b
evalPolynomial (Var a (Vector i) -> Poly a (Maybe (Var a (Vector i))) Natural)
-> Mono (Var a (Vector i)) Natural
-> Poly a (Maybe (Var a (Vector i))) Natural
forall i j b.
(MultiplicativeMonoid b, Exponent b j) =>
(i -> b) -> Mono i j -> b
evalMonomial (Maybe (Var a (Vector i))
-> Poly a (Maybe (Var a (Vector i))) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var (Maybe (Var a (Vector i))
 -> Poly a (Maybe (Var a (Vector i))) Natural)
-> (Var a (Vector i) -> Maybe (Var a (Vector i)))
-> Var a (Vector i)
-> Poly a (Maybe (Var a (Vector i))) Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a (Vector i) -> Maybe (Var a (Vector i))
forall a. a -> Maybe a
Just) Poly a (Var a (Vector i)) Natural
p Poly a (Maybe (Var a (Vector i))) Natural
-> Poly a (Maybe (Var a (Vector i))) Natural
-> Poly a (Maybe (Var a (Vector i))) Natural
forall a. AdditiveGroup a => a -> a -> a
- [(a, Mono (Maybe (Var a (Vector i))) Natural)]
-> Poly a (Maybe (Var a (Vector i))) Natural
forall c i j. Polynomial c i j => [(c, Mono i j)] -> Poly c i j
polynomial [(a
qm, [Item (Mono (Maybe (Var a (Vector i))) Natural)]
-> Mono (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Mono (Maybe (Var a (Vector i))) Natural)]
xaxb), (a
ql, [Item (Mono (Maybe (Var a (Vector i))) Natural)]
-> Mono (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Mono (Maybe (Var a (Vector i))) Natural)]
xa), (a
qr, [Item (Mono (Maybe (Var a (Vector i))) Natural)]
-> Mono (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Mono (Maybe (Var a (Vector i))) Natural)]
xb), (a
qo, [Item (Mono (Maybe (Var a (Vector i))) Natural)]
-> Mono (Maybe (Var a (Vector i))) Natural
forall l. IsList l => [Item l] -> l
fromList [(Maybe (Var a (Vector i)), Natural)]
[Item (Mono (Maybe (Var a (Vector i))) Natural)]
xc), (a
qc, Mono (Maybe (Var a (Vector i))) Natural
forall a. MultiplicativeMonoid a => a
one)] Poly a (Maybe (Var a (Vector i))) Natural
-> Poly a (Maybe (Var a (Vector i))) Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Poly a (Maybe (Var a (Vector i))) Natural
forall a. AdditiveMonoid a => a
zero
            let va :: Var a (Vector i)
va = Var a (Vector i) -> Maybe (Var a (Vector i)) -> Var a (Vector i)
forall a. a -> Maybe a -> a
fromMaybe (a -> Var a (Vector i)
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
forall a. MultiplicativeMonoid a => a
one) Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
a
                vb :: Var a (Vector i)
vb = Var a (Vector i) -> Maybe (Var a (Vector i)) -> Var a (Vector i)
forall a. a -> Maybe a -> a
fromMaybe (a -> Var a (Vector i)
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
forall a. MultiplicativeMonoid a => a
one) Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
b
                vc :: Var a (Vector i)
vc = Var a (Vector i) -> Maybe (Var a (Vector i)) -> Var a (Vector i)
forall a. a -> Maybe a -> a
fromMaybe (a -> Var a (Vector i)
forall a (i :: Type -> Type). a -> Var a i
ConstVar a
forall a. MultiplicativeMonoid a => a
one) Maybe (Var a (Vector i))
Item [Maybe (Var a (Vector i))]
c
            PlonkConstraint i a -> Maybe (PlonkConstraint i a)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PlonkConstraint i a -> Maybe (PlonkConstraint i a))
-> PlonkConstraint i a -> Maybe (PlonkConstraint i a)
forall a b. (a -> b) -> a -> b
$ a
-> a
-> a
-> a
-> a
-> Var a (Vector i)
-> Var a (Vector i)
-> Var a (Vector i)
-> PlonkConstraint i a
forall (i :: Natural) a.
a
-> a
-> a
-> a
-> a
-> Var a (Vector i)
-> Var a (Vector i)
-> Var a (Vector i)
-> PlonkConstraint i a
PlonkConstraint a
qm a
ql a
qr a
qo a
qc Var a (Vector i)
va Var a (Vector i)
vb Var a (Vector i)
vc
        getCoefs [Maybe (Var a (Vector i))]
_ = Maybe (PlonkConstraint i a)
forall a. Maybe a
Nothing

    in [PlonkConstraint i a] -> PlonkConstraint i a
forall a. HasCallStack => [a] -> a
head ([PlonkConstraint i a] -> PlonkConstraint i a)
-> [PlonkConstraint i a] -> PlonkConstraint i a
forall a b. (a -> b) -> a -> b
$ ([Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a))
-> [[Maybe (Var a (Vector i))]] -> [PlonkConstraint i a]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a)
getCoefs [[Maybe (Var a (Vector i))]]
perms

fromPlonkConstraint :: (Ord a, Field a, KnownNat i) => PlonkConstraint i a -> Poly a (Var a (Vector i)) Natural
fromPlonkConstraint :: forall a (i :: Natural).
(Ord a, Field a, KnownNat i) =>
PlonkConstraint i a -> Poly a (Var a (Vector i)) Natural
fromPlonkConstraint (PlonkConstraint a
qm a
ql a
qr a
qo a
qc Var a (Vector i)
a Var a (Vector i)
b Var a (Vector i)
c) =
    let xa :: Poly a (Var a (Vector i)) Natural
xa = Var a (Vector i) -> Poly a (Var a (Vector i)) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var Var a (Vector i)
a
        xb :: Poly a (Var a (Vector i)) Natural
xb = Var a (Vector i) -> Poly a (Var a (Vector i)) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var Var a (Vector i)
b
        xc :: Poly a (Var a (Vector i)) Natural
xc = Var a (Vector i) -> Poly a (Var a (Vector i)) Natural
forall c i j. Polynomial c i j => i -> Poly c i j
var Var a (Vector i)
c
        xaxb :: Poly a (Var a (Vector i)) Natural
xaxb = Poly a (Var a (Vector i)) Natural
xa Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Poly a (Var a (Vector i)) Natural
xb
    in
              a
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall b a. Scale b a => b -> a -> a
scale a
qm Poly a (Var a (Vector i)) Natural
xaxb
            Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ a
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall b a. Scale b a => b -> a -> a
scale a
ql Poly a (Var a (Vector i)) Natural
xa
            Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ a
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall b a. Scale b a => b -> a -> a
scale a
qr Poly a (Var a (Vector i)) Natural
xb
            Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ a
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall b a. Scale b a => b -> a -> a
scale a
qo Poly a (Var a (Vector i)) Natural
xc
            Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> Poly a (Var a (Vector i)) Natural
forall a b. FromConstant a b => a -> b
fromConstant a
qc