{-# LANGUAGE NoStarIsType         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Plonkup.Relation where

import           Data.Binary                                         (Binary)
import           Data.Bool                                           (bool)
import           Data.Constraint                                     (withDict)
import           Data.Constraint.Nat                                 (timesNat)
import           Data.Map                                            (elems, keys)
import           Data.Maybe                                          (fromJust)
import           GHC.IsList                                          (IsList (..))
import           Prelude                                             hiding (Num (..), drop, length, replicate, sum,
                                                                      take, (!!), (/), (^))
import           Test.QuickCheck                                     (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.Basic.Permutations              (Permutation, fromCycles, mkIndexPartition)
import           ZkFold.Base.Algebra.Polynomials.Multivariate        (evalMonomial, evalPolynomial, var)
import           ZkFold.Base.Algebra.Polynomials.Univariate          (PolyVec, toPolyVec)
import           ZkFold.Base.Data.Vector                             (Vector, fromVector)
import           ZkFold.Base.Protocol.Plonkup.Internal               (PlonkupPermutationSize)
import           ZkFold.Base.Protocol.Plonkup.LookupConstraint       (LookupConstraint (..))
import           ZkFold.Base.Protocol.Plonkup.PlonkConstraint        (PlonkConstraint (..), toPlonkConstraint)
import           ZkFold.Base.Protocol.Plonkup.PlonkupConstraint
import           ZkFold.Prelude                                      (length, replicate)
import           ZkFold.Symbolic.Compiler
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

-- Here `n` is the total number of constraints, `i` is the number of inputs to the circuit, and `a` is the field type.
data PlonkupRelation i n l a = PlonkupRelation
    { forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qM       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qL       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qR       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qO       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qC       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qK       :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
t        :: PolyVec a n
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> Permutation (3 * n)
sigma    :: Permutation (3 * n)
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a
-> Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
witness  :: Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
    , forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> Vector i a -> Vector l a
pubInput :: Vector i a -> Vector l a
    }

instance Show a => Show (PlonkupRelation i n l a) where
    show :: PlonkupRelation i n l a -> String
show PlonkupRelation {PolyVec a n
Permutation (3 * n)
Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
Vector i a -> Vector l a
qM :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qL :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qR :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qO :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qC :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qK :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
t :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
sigma :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> Permutation (3 * n)
witness :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a
-> Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
pubInput :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> Vector i a -> Vector l a
qM :: PolyVec a n
qL :: PolyVec a n
qR :: PolyVec a n
qO :: PolyVec a n
qC :: PolyVec a n
qK :: PolyVec a n
t :: PolyVec a n
sigma :: Permutation (3 * n)
witness :: Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
pubInput :: Vector i a -> Vector l a
..} =
        String
"Plonkup Relation: "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qM String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qL String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qR String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qO String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qC String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
qK String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec a n -> String
forall a. Show a => a -> String
show PolyVec a n
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Permutation (3 * n) -> String
forall a. Show a => a -> String
show Permutation (3 * n)
sigma

instance
        ( KnownNat i
        , KnownNat n
        , KnownNat (PlonkupPermutationSize n)
        , KnownNat l
        , Arbitrary a
        , Arithmetic a
        , Binary a
        ) => Arbitrary (PlonkupRelation i n l a) where
    arbitrary :: Gen (PlonkupRelation i n l a)
arbitrary = Maybe (PlonkupRelation i n l a) -> PlonkupRelation i n l a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (PlonkupRelation i n l a) -> PlonkupRelation i n l a)
-> (ArithmeticCircuit a (Vector i) (Vector l)
    -> Maybe (PlonkupRelation i n l a))
-> ArithmeticCircuit a (Vector i) (Vector l)
-> PlonkupRelation i n l a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArithmeticCircuit a (Vector i) (Vector l)
-> Maybe (PlonkupRelation i n l a)
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
(KnownNat i, KnownNat n, KnownNat l, Arithmetic a) =>
ArithmeticCircuit a (Vector i) (Vector l)
-> Maybe (PlonkupRelation i n l a)
toPlonkupRelation (ArithmeticCircuit a (Vector i) (Vector l)
 -> PlonkupRelation i n l a)
-> Gen (ArithmeticCircuit a (Vector i) (Vector l))
-> Gen (PlonkupRelation i n l a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ArithmeticCircuit a (Vector i) (Vector l))
forall a. Arbitrary a => Gen a
arbitrary

toPlonkupRelation :: forall i n l a .
       KnownNat i
    => KnownNat n
    => KnownNat l
    => Arithmetic a
    => ArithmeticCircuit a (Vector i) (Vector l)
    -> Maybe (PlonkupRelation i n l a)
toPlonkupRelation :: forall (i :: Natural) (n :: Natural) (l :: Natural) a.
(KnownNat i, KnownNat n, KnownNat l, Arithmetic a) =>
ArithmeticCircuit a (Vector i) (Vector l)
-> Maybe (PlonkupRelation i n l a)
toPlonkupRelation ArithmeticCircuit a (Vector i) (Vector l)
ac =
    let xPub :: Vector l (Var a (Vector i))
xPub                = ArithmeticCircuit a (Vector i) (Vector l)
-> Vector l (Var a (Vector i))
forall a (i :: Type -> Type) (o :: Type -> Type).
ArithmeticCircuit a i o -> o (Var a i)
acOutput ArithmeticCircuit a (Vector i) (Vector l)
ac
        pubInputConstraints :: [Poly a (Var a (Vector i)) Natural]
pubInputConstraints = (Var a (Vector i) -> Poly a (Var a (Vector i)) Natural)
-> [Var a (Vector i)] -> [Poly a (Var a (Vector i)) Natural]
forall a b. (a -> b) -> [a] -> [b]
map 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 (Vector l (Var a (Vector i)) -> [Var a (Vector i)]
forall (size :: Natural) a. Vector size a -> [a]
fromVector Vector l (Var a (Vector i))
xPub)
        plonkConstraints :: [Poly a (Var a (Vector i)) Natural]
plonkConstraints    = (Poly a (SysVar (Vector i)) Natural
 -> Poly a (Var a (Vector i)) Natural)
-> [Poly a (SysVar (Vector i)) Natural]
-> [Poly a (Var a (Vector i)) Natural]
forall a b. (a -> b) -> [a] -> [b]
map (((SysVar (Vector i) -> Poly a (Var a (Vector i)) Natural)
 -> Mono (SysVar (Vector i)) Natural
 -> Poly a (Var a (Vector i)) Natural)
-> (SysVar (Vector i) -> Poly a (Var a (Vector i)) Natural)
-> Poly a (SysVar (Vector i)) Natural
-> Poly a (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 (SysVar (Vector i) -> Poly a (Var a (Vector i)) Natural)
-> Mono (SysVar (Vector i)) Natural
-> Poly a (Var a (Vector i)) Natural
forall i j b.
(MultiplicativeMonoid b, Exponent b j) =>
(i -> b) -> Mono i j -> b
evalMonomial (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) -> Poly a (Var a (Vector i)) Natural)
-> (SysVar (Vector i) -> Var a (Vector i))
-> SysVar (Vector i)
-> Poly a (Var a (Vector i)) Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SysVar (Vector i) -> Var a (Vector i)
forall a (i :: Type -> Type). SysVar i -> Var a i
SysVar)) (Map ByteString (Poly a (SysVar (Vector i)) Natural)
-> [Poly a (SysVar (Vector i)) Natural]
forall k a. Map k a -> [a]
elems (ArithmeticCircuit a (Vector i) (Vector l)
-> Map ByteString (Poly a (SysVar (Vector i)) Natural)
forall a (i :: Type -> Type) (o :: Type -> Type).
ArithmeticCircuit a i o -> Map ByteString (Constraint a i)
acSystem ArithmeticCircuit a (Vector i) (Vector l)
ac))
        rs :: [Natural]
rs = (a -> Natural) -> [a] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
map a -> Natural
a -> Const a
forall a. ToConstant a => a -> Const a
toConstant ([a] -> [Natural]) -> [a] -> [Natural]
forall a b. (a -> b) -> a -> b
$ Map (SysVar (Vector i)) a -> [a]
forall k a. Map k a -> [a]
elems (Map (SysVar (Vector i)) a -> [a])
-> Map (SysVar (Vector i)) a -> [a]
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit a (Vector i) (Vector l)
-> Map (SysVar (Vector i)) a
forall a (i :: Type -> Type) (o :: Type -> Type).
ArithmeticCircuit a i o -> Map (SysVar i) a
acRange ArithmeticCircuit a (Vector i) (Vector l)
ac
        -- TODO: We are expecting at most one range.
        t :: PolyVec a n
t = Vector a -> PolyVec a n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (Natural -> Item (Vector a)) -> [Natural] -> [Item (Vector a)]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> a
Natural -> Item (Vector a)
forall a b. FromConstant a b => a -> b
fromConstant ([Natural] -> [Item (Vector a)]) -> [Natural] -> [Item (Vector a)]
forall a b. (a -> b) -> a -> b
$ [Natural] -> [Natural] -> Bool -> [Natural]
forall a. a -> a -> Bool -> a
bool [] (Natural -> Natural -> [Natural]
forall a. Natural -> a -> [a]
replicate (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! [Natural] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [Natural]
rs Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural
0 [Natural] -> [Natural] -> [Natural]
forall a. [a] -> [a] -> [a]
++ [ Natural
0 .. [Natural] -> Natural
forall a. HasCallStack => [a] -> a
head [Natural]
rs ]) (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Natural] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Natural]
rs)
        -- Number of elements in the set `t`.
        nLookup :: Natural
nLookup = Natural -> Natural -> Bool -> Natural
forall a. a -> a -> Bool -> a
bool Natural
0 ([Natural] -> Natural
forall a. HasCallStack => [a] -> a
head [Natural]
rs Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Natural] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Natural]
rs)
        -- Lookup queries.
        xLookup :: [SysVar (Vector i)]
xLookup = Map (SysVar (Vector i)) a -> [SysVar (Vector i)]
forall k a. Map k a -> [k]
keys (ArithmeticCircuit a (Vector i) (Vector l)
-> Map (SysVar (Vector i)) a
forall a (i :: Type -> Type) (o :: Type -> Type).
ArithmeticCircuit a i o -> Map (SysVar i) a
acRange ArithmeticCircuit a (Vector i) (Vector l)
ac)

        -- The total number of constraints in the relation.
        n' :: Natural
n'      = ArithmeticCircuit a (Vector i) (Vector l) -> Natural
forall a (i :: Type -> Type) (o :: Type -> Type).
ArithmeticCircuit a i o -> Natural
acSizeN ArithmeticCircuit a (Vector i) (Vector l)
ac Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ forall (n :: Natural). KnownNat n => Natural
value @l Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ [SysVar (Vector i)] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [SysVar (Vector i)]
xLookup

        plonkupSystem :: [PlonkupConstraint i a]
plonkupSystem = [[PlonkupConstraint i a]] -> [PlonkupConstraint i a]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
            [ (Poly a (Var a (Vector i)) Natural -> PlonkupConstraint i a)
-> [Poly a (Var a (Vector i)) Natural] -> [PlonkupConstraint i a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> PlonkupConstraint i a
forall (i :: Natural) a.
PlonkConstraint i a -> PlonkupConstraint i a
ConsPlonk (PlonkConstraint i a -> PlonkupConstraint i a)
-> (Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a)
-> Poly a (Var a (Vector i)) Natural
-> PlonkupConstraint i a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a
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]
pubInputConstraints [Poly a (Var a (Vector i)) Natural]
-> [Poly a (Var a (Vector i)) Natural]
-> [Poly a (Var a (Vector i)) Natural]
forall a. [a] -> [a] -> [a]
++ [Poly a (Var a (Vector i)) Natural]
plonkConstraints)
            , LookupConstraint i a -> PlonkupConstraint i a
forall (i :: Natural) a.
LookupConstraint i a -> PlonkupConstraint i a
ConsLookup (LookupConstraint i a -> PlonkupConstraint i a)
-> (SysVar (Vector i) -> LookupConstraint i a)
-> SysVar (Vector i)
-> PlonkupConstraint i a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SysVar (Vector i) -> LookupConstraint i a
forall {k} (i :: Natural) (a :: k).
SysVar (Vector i) -> LookupConstraint i a
LookupConstraint (SysVar (Vector i) -> PlonkupConstraint i a)
-> [SysVar (Vector i)] -> [PlonkupConstraint i a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [SysVar (Vector i)]
xLookup
            , Natural -> PlonkupConstraint i a -> [PlonkupConstraint i a]
forall a. Natural -> a -> [a]
replicate (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
n') PlonkupConstraint i a
forall (i :: Natural) a. PlonkupConstraint i a
ConsExtra
            ]

        qM :: PolyVec a n
qM = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> a
forall (i :: Natural) a. PlonkConstraint i a -> a
qm (PlonkConstraint i a -> a)
-> (PlonkupConstraint i a -> PlonkConstraint i a)
-> PlonkupConstraint i a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlonkupConstraint i a -> PlonkConstraint i a
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint) [PlonkupConstraint i a]
plonkupSystem
        qL :: PolyVec a n
qL = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> a
forall (i :: Natural) a. PlonkConstraint i a -> a
ql (PlonkConstraint i a -> a)
-> (PlonkupConstraint i a -> PlonkConstraint i a)
-> PlonkupConstraint i a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlonkupConstraint i a -> PlonkConstraint i a
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint) [PlonkupConstraint i a]
plonkupSystem
        qR :: PolyVec a n
qR = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> a
forall (i :: Natural) a. PlonkConstraint i a -> a
qr (PlonkConstraint i a -> a)
-> (PlonkupConstraint i a -> PlonkConstraint i a)
-> PlonkupConstraint i a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlonkupConstraint i a -> PlonkConstraint i a
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint) [PlonkupConstraint i a]
plonkupSystem
        qO :: PolyVec a n
qO = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> a
forall (i :: Natural) a. PlonkConstraint i a -> a
qo (PlonkConstraint i a -> a)
-> (PlonkupConstraint i a -> PlonkConstraint i a)
-> PlonkupConstraint i a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlonkupConstraint i a -> PlonkConstraint i a
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint) [PlonkupConstraint i a]
plonkupSystem
        qC :: PolyVec a n
qC = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (PlonkConstraint i a -> a
forall (i :: Natural) a. PlonkConstraint i a -> a
qc (PlonkConstraint i a -> a)
-> (PlonkupConstraint i a -> PlonkConstraint i a)
-> PlonkupConstraint i a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PlonkupConstraint i a -> PlonkConstraint i a
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint) [PlonkupConstraint i a]
plonkupSystem
        qK :: PolyVec a n
qK = forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @a @n (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (PlonkupConstraint i a -> a) -> [PlonkupConstraint i a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map PlonkupConstraint i a -> a
forall a (i :: Natural).
FiniteField a =>
PlonkupConstraint i a -> a
isLookupConstraint [PlonkupConstraint i a]
plonkupSystem

        a :: [Var a (Vector i)]
a  = (PlonkupConstraint i a -> Var a (Vector i))
-> [PlonkupConstraint i a] -> [Var a (Vector i)]
forall a b. (a -> b) -> [a] -> [b]
map PlonkupConstraint i a -> Var a (Vector i)
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getA [PlonkupConstraint i a]
plonkupSystem
        b :: [Var a (Vector i)]
b  = (PlonkupConstraint i a -> Var a (Vector i))
-> [PlonkupConstraint i a] -> [Var a (Vector i)]
forall a b. (a -> b) -> [a] -> [b]
map PlonkupConstraint i a -> Var a (Vector i)
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getB [PlonkupConstraint i a]
plonkupSystem
        c :: [Var a (Vector i)]
c  = (PlonkupConstraint i a -> Var a (Vector i))
-> [PlonkupConstraint i a] -> [Var a (Vector i)]
forall a b. (a -> b) -> [a] -> [b]
map PlonkupConstraint i a -> Var a (Vector i)
forall a (i :: Natural).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getC [PlonkupConstraint i a]
plonkupSystem
        -- TODO: Permutation code is not particularly safe. We rely on the list being of length 3*n.
        sigma :: Permutation (3 * n)
sigma = ((KnownNat 3, KnownNat n) :- KnownNat (3 * n))
-> (KnownNat (3 * n) => Permutation (3 * n)) -> Permutation (3 * n)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural).
(KnownNat n, KnownNat m) :- KnownNat (n * m)
timesNat @3 @n) (forall (n :: Natural) a.
KnownNat n =>
IndexPartition a -> Permutation n
fromCycles @(3*n) (IndexPartition (Var a (Vector i)) -> Permutation (3 * n))
-> IndexPartition (Var a (Vector i)) -> Permutation (3 * n)
forall a b. (a -> b) -> a -> b
$ Vector (Var a (Vector i)) -> IndexPartition (Var a (Vector i))
forall a. Ord a => Vector a -> IndexPartition a
mkIndexPartition (Vector (Var a (Vector i)) -> IndexPartition (Var a (Vector i)))
-> Vector (Var a (Vector i)) -> IndexPartition (Var a (Vector i))
forall a b. (a -> b) -> a -> b
$ [Item (Vector (Var a (Vector i)))] -> Vector (Var a (Vector i))
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (Var a (Vector i)))] -> Vector (Var a (Vector i)))
-> [Item (Vector (Var a (Vector i)))] -> Vector (Var a (Vector i))
forall a b. (a -> b) -> a -> b
$ [Var a (Vector i)]
a [Var a (Vector i)] -> [Var a (Vector i)] -> [Var a (Vector i)]
forall a. [a] -> [a] -> [a]
++ [Var a (Vector i)]
b [Var a (Vector i)] -> [Var a (Vector i)] -> [Var a (Vector i)]
forall a. [a] -> [a] -> [a]
++ [Var a (Vector i)]
c)

        w1 :: Vector i a -> PolyVec a n
w1 Vector i a
i   = Vector a -> PolyVec a n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (Var a (Vector i) -> a) -> [Var a (Vector i)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArithmeticCircuit a (Vector i) (Vector l)
-> Vector i a -> Var a (Vector i) -> a
forall (i :: Type -> Type) a (o :: Type -> Type).
Representable i =>
ArithmeticCircuit a i o -> i a -> Var a i -> a
indexW ArithmeticCircuit a (Vector i) (Vector l)
ac Vector i a
i) [Var a (Vector i)]
a
        w2 :: Vector i a -> PolyVec a n
w2 Vector i a
i   = Vector a -> PolyVec a n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (Var a (Vector i) -> a) -> [Var a (Vector i)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArithmeticCircuit a (Vector i) (Vector l)
-> Vector i a -> Var a (Vector i) -> a
forall (i :: Type -> Type) a (o :: Type -> Type).
Representable i =>
ArithmeticCircuit a i o -> i a -> Var a i -> a
indexW ArithmeticCircuit a (Vector i) (Vector l)
ac Vector i a
i) [Var a (Vector i)]
b
        w3 :: Vector i a -> PolyVec a n
w3 Vector i a
i   = Vector a -> PolyVec a n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector a -> PolyVec a n) -> Vector a -> PolyVec a n
forall a b. (a -> b) -> a -> b
$ [Item (Vector a)] -> Vector a
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector a)] -> Vector a) -> [Item (Vector a)] -> Vector a
forall a b. (a -> b) -> a -> b
$ (Var a (Vector i) -> a) -> [Var a (Vector i)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArithmeticCircuit a (Vector i) (Vector l)
-> Vector i a -> Var a (Vector i) -> a
forall (i :: Type -> Type) a (o :: Type -> Type).
Representable i =>
ArithmeticCircuit a i o -> i a -> Var a i -> a
indexW ArithmeticCircuit a (Vector i) (Vector l)
ac Vector i a
i) [Var a (Vector i)]
c
        witness :: Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
witness Vector i a
i  = (Vector i a -> PolyVec a n
w1 Vector i a
i, Vector i a -> PolyVec a n
w2 Vector i a
i, Vector i a -> PolyVec a n
w3 Vector i a
i)
        pubInput :: Vector i a -> Vector l a
pubInput Vector i a
i = (Var a (Vector i) -> a)
-> Vector l (Var a (Vector i)) -> Vector l a
forall a b. (a -> b) -> Vector l a -> Vector l b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArithmeticCircuit a (Vector i) (Vector l)
-> Vector i a -> Var a (Vector i) -> a
forall (i :: Type -> Type) a (o :: Type -> Type).
Representable i =>
ArithmeticCircuit a i o -> i a -> Var a i -> a
indexW ArithmeticCircuit a (Vector i) (Vector l)
ac Vector i a
i) Vector l (Var a (Vector i))
xPub

    in if Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
max Natural
n' Natural
nLookup Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= forall (n :: Natural). KnownNat n => Natural
value @n
        then PlonkupRelation i n l a -> Maybe (PlonkupRelation i n l a)
forall a. a -> Maybe a
Just (PlonkupRelation i n l a -> Maybe (PlonkupRelation i n l a))
-> PlonkupRelation i n l a -> Maybe (PlonkupRelation i n l a)
forall a b. (a -> b) -> a -> b
$ PlonkupRelation {PolyVec a n
Permutation (3 * n)
Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
Vector i a -> Vector l a
qM :: PolyVec a n
qL :: PolyVec a n
qR :: PolyVec a n
qO :: PolyVec a n
qC :: PolyVec a n
qK :: PolyVec a n
t :: PolyVec a n
sigma :: Permutation (3 * n)
witness :: Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
pubInput :: Vector i a -> Vector l a
t :: PolyVec a n
qM :: PolyVec a n
qL :: PolyVec a n
qR :: PolyVec a n
qO :: PolyVec a n
qC :: PolyVec a n
qK :: PolyVec a n
sigma :: Permutation (3 * n)
witness :: Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
pubInput :: Vector i a -> Vector l a
..}
        else Maybe (PlonkupRelation i n l a)
forall a. Maybe a
Nothing