{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE UndecidableInstances #-} module ZkFold.Base.Protocol.Plonkup.Setup where import Data.Binary (Binary) import Data.Functor.Rep (Rep, Representable) import Data.Maybe (fromJust) import qualified Data.Vector as V import GHC.IsList (IsList (..)) import Prelude hiding (Num (..), drop, length, sum, take, (!!), (/), (^)) import ZkFold.Base.Algebra.Basic.Class import ZkFold.Base.Algebra.Basic.Number (KnownNat, value) import ZkFold.Base.Algebra.Basic.Permutations (fromPermutation) import ZkFold.Base.Algebra.EllipticCurve.Class (CyclicGroup (..), Pairing) import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec, polyVecInLagrangeBasis, toPolyVec) import ZkFold.Base.Data.Vector (Vector (..)) import ZkFold.Base.Protocol.NonInteractiveProof.Internal (CoreFunction (..)) import ZkFold.Base.Protocol.Plonkup.Internal (Plonkup (..), PlonkupPermutationSize, PlonkupPolyExtendedLength, with4n6) import ZkFold.Base.Protocol.Plonkup.Prover.Polynomials (PlonkupCircuitPolynomials (..)) import ZkFold.Base.Protocol.Plonkup.Relation (PlonkupRelation (..), toPlonkupRelation) import ZkFold.Base.Protocol.Plonkup.Verifier.Commitments (PlonkupCircuitCommitments (..)) import ZkFold.Symbolic.Class (Arithmetic) data PlonkupSetup p i n l g1 g2 = PlonkupSetup { forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 omega :: ScalarFieldOf g1 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 k1 :: ScalarFieldOf g1 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 k2 :: ScalarFieldOf g1 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> Vector g1 gs :: V.Vector g1 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> g2 h0 :: g2 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> g2 h1 :: g2 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n sigma1s :: PolyVec (ScalarFieldOf g1) n , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n sigma2s :: PolyVec (ScalarFieldOf g1) n , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n sigma3s :: PolyVec (ScalarFieldOf g1) n , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupRelation p i n l (ScalarFieldOf g1) relation :: PlonkupRelation p i n l (ScalarFieldOf g1) , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1 polynomials :: PlonkupCircuitPolynomials n g1 , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1 commitments :: PlonkupCircuitCommitments g1 } instance ( Show g1 , Show g2 , Show (ScalarFieldOf g1) , Show (PlonkupRelation p i n l (ScalarFieldOf g1)) ) => Show (PlonkupSetup p i n l g1 g2) where show :: PlonkupSetup p i n l g1 g2 -> String show PlonkupSetup {g2 Vector g1 PlonkupCircuitCommitments g1 PolyVec (ScalarFieldOf g1) n ScalarFieldOf g1 PlonkupRelation p i n l (ScalarFieldOf g1) PlonkupCircuitPolynomials n g1 omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1 gs :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> Vector g1 h0 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> g2 h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> g2 sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupRelation p i n l (ScalarFieldOf g1) polynomials :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1 commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2. PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1 omega :: ScalarFieldOf g1 k1 :: ScalarFieldOf g1 k2 :: ScalarFieldOf g1 gs :: Vector g1 h0 :: g2 h1 :: g2 sigma1s :: PolyVec (ScalarFieldOf g1) n sigma2s :: PolyVec (ScalarFieldOf g1) n sigma3s :: PolyVec (ScalarFieldOf g1) n relation :: PlonkupRelation p i n l (ScalarFieldOf g1) polynomials :: PlonkupCircuitPolynomials n g1 commitments :: PlonkupCircuitCommitments g1 ..} = String "Setup: " String -> ShowS forall a. [a] -> [a] -> [a] ++ ScalarFieldOf g1 -> String forall a. Show a => a -> String show ScalarFieldOf g1 omega String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ ScalarFieldOf g1 -> String forall a. Show a => a -> String show ScalarFieldOf g1 k1 String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ ScalarFieldOf g1 -> String forall a. Show a => a -> String show ScalarFieldOf g1 k2 String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ Vector g1 -> String forall a. Show a => a -> String show Vector g1 gs String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ g2 -> String forall a. Show a => a -> String show g2 h0 String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ g2 -> String forall a. Show a => a -> String show g2 h1 String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PolyVec (ScalarFieldOf g1) n -> String forall a. Show a => a -> String show PolyVec (ScalarFieldOf g1) n sigma1s String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PolyVec (ScalarFieldOf g1) n -> String forall a. Show a => a -> String show PolyVec (ScalarFieldOf g1) n sigma2s String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PolyVec (ScalarFieldOf g1) n -> String forall a. Show a => a -> String show PolyVec (ScalarFieldOf g1) n sigma3s String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PlonkupRelation p i n l (ScalarFieldOf g1) -> String forall a. Show a => a -> String show PlonkupRelation p i n l (ScalarFieldOf g1) relation String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PlonkupCircuitPolynomials n g1 -> String forall a. Show a => a -> String show PlonkupCircuitPolynomials n g1 polynomials String -> ShowS forall a. [a] -> [a] -> [a] ++ String " " String -> ShowS forall a. [a] -> [a] -> [a] ++ PlonkupCircuitCommitments g1 -> String forall a. Show a => a -> String show PlonkupCircuitCommitments g1 commitments plonkupSetup :: forall i p n l g1 g2 gt ts core. ( KnownNat n , Representable p , Representable i , Representable l , Foldable l , Ord (Rep i) , Arithmetic (ScalarFieldOf g1) , Binary (ScalarFieldOf g2) , Pairing g1 g2 gt , CoreFunction g1 core) => Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2 plonkupSetup :: forall {k} {k} (i :: Type -> Type) (p :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 gt (ts :: k) (core :: k). (KnownNat n, Representable p, Representable i, Representable l, Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1), Binary (ScalarFieldOf g2), Pairing g1 g2 gt, CoreFunction g1 core) => Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2 plonkupSetup Plonkup {g2 Vector (n + 5) g1 ArithmeticCircuit (ScalarFieldOf g1) p i l ScalarFieldOf g1 omega :: ScalarFieldOf g1 k1 :: ScalarFieldOf g1 k2 :: ScalarFieldOf g1 ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l h1 :: g2 gs' :: Vector (n + 5) g1 omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1 k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1 k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1 ac :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> ArithmeticCircuit (ScalarFieldOf g1) p i l h1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> g2 gs' :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) g1 g2 (transcript :: k). Plonkup p i n l g1 g2 transcript -> Vector (n + 5) g1 ..} = let gs :: Vector g1 gs = Vector (n + 5) g1 -> Vector g1 forall (size :: Natural) a. Vector size a -> Vector a toV Vector (n + 5) g1 gs' h0 :: g2 h0 = g2 forall g. CyclicGroup g => g pointGen relation :: PlonkupRelation p i n l (ScalarFieldOf g1) relation@PlonkupRelation{PolyVec (ScalarFieldOf g1) n Permutation (3 * n) p (ScalarFieldOf g1) -> i (ScalarFieldOf g1) -> l (ScalarFieldOf g1) p (ScalarFieldOf g1) -> i (ScalarFieldOf g1) -> (PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n) qM :: PolyVec (ScalarFieldOf g1) n qL :: PolyVec (ScalarFieldOf g1) n qR :: PolyVec (ScalarFieldOf g1) n qO :: PolyVec (ScalarFieldOf g1) n qC :: PolyVec (ScalarFieldOf g1) n qK :: PolyVec (ScalarFieldOf g1) n t :: PolyVec (ScalarFieldOf g1) n sigma :: Permutation (3 * n) witness :: p (ScalarFieldOf g1) -> i (ScalarFieldOf g1) -> (PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n) pubInput :: p (ScalarFieldOf g1) -> i (ScalarFieldOf g1) -> l (ScalarFieldOf g1) qM :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n qL :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n qR :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n qO :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n qC :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n qK :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n t :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> PolyVec a n sigma :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> Permutation (3 * n) witness :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> p a -> i a -> (PolyVec a n, PolyVec a n, PolyVec a n) pubInput :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. PlonkupRelation p i n l a -> p a -> i a -> l a ..} = Maybe (PlonkupRelation p i n l (ScalarFieldOf g1)) -> PlonkupRelation p i n l (ScalarFieldOf g1) forall a. HasCallStack => Maybe a -> a fromJust (Maybe (PlonkupRelation p i n l (ScalarFieldOf g1)) -> PlonkupRelation p i n l (ScalarFieldOf g1)) -> Maybe (PlonkupRelation p i n l (ScalarFieldOf g1)) -> PlonkupRelation p i n l (ScalarFieldOf g1) forall a b. (a -> b) -> a -> b $ ArithmeticCircuit (ScalarFieldOf g2) p i l -> Maybe (PlonkupRelation p i n l (ScalarFieldOf g2)) forall (i :: Type -> Type) (p :: Type -> Type) (n :: Natural) (l :: Type -> Type) a. (KnownNat n, Arithmetic a, Binary a, Ord (Rep i), Representable p, Representable i, Representable l, Foldable l) => ArithmeticCircuit a p i l -> Maybe (PlonkupRelation p i n l a) toPlonkupRelation ArithmeticCircuit (ScalarFieldOf g1) p i l ArithmeticCircuit (ScalarFieldOf g2) p i l ac :: PlonkupRelation p i n l (ScalarFieldOf g1) f :: Natural -> ScalarFieldOf g2 f Natural i = case (Natural iNatural -> Natural -> Natural -!Natural 1) Natural -> Natural -> Natural forall a. Integral a => a -> a -> a `Prelude.div` forall (n :: Natural). KnownNat n => Natural value @n of Natural 0 -> ScalarFieldOf g1 ScalarFieldOf g2 omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2 forall a b. Exponent a b => a -> b -> a ^Natural i Natural 1 -> ScalarFieldOf g1 ScalarFieldOf g2 k1 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2 forall a. MultiplicativeSemigroup a => a -> a -> a * (ScalarFieldOf g1 ScalarFieldOf g2 omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2 forall a b. Exponent a b => a -> b -> a ^Natural i) Natural 2 -> ScalarFieldOf g1 ScalarFieldOf g2 k2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2 forall a. MultiplicativeSemigroup a => a -> a -> a * (ScalarFieldOf g1 ScalarFieldOf g2 omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2 forall a b. Exponent a b => a -> b -> a ^Natural i) Natural _ -> String -> ScalarFieldOf g2 forall a. HasCallStack => String -> a error String "setup: invalid index" s :: Vector (ScalarFieldOf g2) s = [Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2) forall l. IsList l => [Item l] -> l fromList ([Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2)) -> [Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2) forall a b. (a -> b) -> a -> b $ (Natural -> Item (Vector (ScalarFieldOf g2))) -> [Natural] -> [Item (Vector (ScalarFieldOf g2))] forall a b. (a -> b) -> [a] -> [b] map Natural -> Item (Vector (ScalarFieldOf g2)) Natural -> ScalarFieldOf g2 f ([Natural] -> [Item (Vector (ScalarFieldOf g2))]) -> [Natural] -> [Item (Vector (ScalarFieldOf g2))] forall a b. (a -> b) -> a -> b $ forall (n :: Natural). Permutation n -> [Natural] fromPermutation @(PlonkupPermutationSize n) (Permutation (3 * n) -> [Natural]) -> Permutation (3 * n) -> [Natural] forall a b. (a -> b) -> a -> b $ Permutation (3 * n) sigma sigma1s :: PolyVec (ScalarFieldOf g2) n sigma1s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall c (size :: Natural). (Ring c, KnownNat size) => Vector c -> PolyVec c size toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n) -> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall a b. (a -> b) -> a -> b $ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a. Int -> Vector a -> Vector a V.take (Natural -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Natural -> Int) -> Natural -> Int forall a b. (a -> b) -> a -> b $ forall (n :: Natural). KnownNat n => Natural value @n) Vector (ScalarFieldOf g2) s sigma2s :: PolyVec (ScalarFieldOf g2) n sigma2s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall c (size :: Natural). (Ring c, KnownNat size) => Vector c -> PolyVec c size toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n) -> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall a b. (a -> b) -> a -> b $ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a. Int -> Vector a -> Vector a V.take (Natural -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Natural -> Int) -> Natural -> Int forall a b. (a -> b) -> a -> b $ forall (n :: Natural). KnownNat n => Natural value @n) (Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)) -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a b. (a -> b) -> a -> b $ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a. Int -> Vector a -> Vector a V.drop (Natural -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Natural -> Int) -> Natural -> Int forall a b. (a -> b) -> a -> b $ forall (n :: Natural). KnownNat n => Natural value @n) Vector (ScalarFieldOf g2) s sigma3s :: PolyVec (ScalarFieldOf g2) n sigma3s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall c (size :: Natural). (Ring c, KnownNat size) => Vector c -> PolyVec c size toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n) -> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n forall a b. (a -> b) -> a -> b $ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a. Int -> Vector a -> Vector a V.take (Natural -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Natural -> Int) -> Natural -> Int forall a b. (a -> b) -> a -> b $ forall (n :: Natural). KnownNat n => Natural value @n) (Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)) -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a b. (a -> b) -> a -> b $ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2) forall a. Int -> Vector a -> Vector a V.drop (Natural -> Int forall a b. (Integral a, Num b) => a -> b fromIntegral (Natural -> Int) -> Natural -> Int forall a b. (a -> b) -> a -> b $ Natural 2 Natural -> Natural -> Natural forall a. MultiplicativeSemigroup a => a -> a -> a * forall (n :: Natural). KnownNat n => Natural value @n) Vector (ScalarFieldOf g2) s qmX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qmX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qM) qlX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qlX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qL) qrX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qrX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qR) qoX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qoX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qO) qcX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qcX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qC) qkX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qkX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n qK) s1X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s1X = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n PolyVec (ScalarFieldOf g2) n sigma1s) s2X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s2X = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n PolyVec (ScalarFieldOf g2) n sigma2s) s3X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s3X = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n PolyVec (ScalarFieldOf g2) n sigma3s) tX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) tX = forall (n :: Natural) {r}. KnownNat n => (KnownNat ((4 * n) + 6) => r) -> r with4n6 @n (forall c (n :: Natural) (size :: Natural). (Field c, Eq c, KnownNat n, KnownNat size) => c -> PolyVec c n -> PolyVec c size polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1 omega PolyVec (ScalarFieldOf g1) n t) polynomials :: PlonkupCircuitPolynomials n g1 polynomials = PlonkupCircuitPolynomials {PolyVec (ScalarFieldOf g1) ((4 * n) + 6) PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qmX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qlX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qrX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qoX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qcX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qkX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s1X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s2X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s3X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) tX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qlX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) qrX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) qoX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) qmX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) qcX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) qkX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) s1X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) s2X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) s3X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) tX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6) ..} com :: Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 com = forall g (core :: k) f (size :: Natural). (CoreFunction g core, f ~ ScalarFieldOf g) => Vector g -> PolyVec f size -> g forall {k} g (core :: k) f (size :: Natural). (CoreFunction g core, f ~ ScalarFieldOf g) => Vector g -> PolyVec f size -> g msm @g1 @core cmQl :: g1 cmQl = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qlX cmQr :: g1 cmQr = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qrX cmQo :: g1 cmQo = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qoX cmQm :: g1 cmQm = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qmX cmQc :: g1 cmQc = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qcX cmQk :: g1 cmQk = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) qkX cmS1 :: g1 cmS1 = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s1X cmS2 :: g1 cmS2 = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s2X cmS3 :: g1 cmS3 = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) s3X cmT1 :: g1 cmT1 = Vector g1 gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1 `com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6) tX commitments :: PlonkupCircuitCommitments g1 commitments = PlonkupCircuitCommitments {g1 cmQl :: g1 cmQr :: g1 cmQo :: g1 cmQm :: g1 cmQc :: g1 cmQk :: g1 cmS1 :: g1 cmS2 :: g1 cmS3 :: g1 cmT1 :: g1 cmQl :: g1 cmQr :: g1 cmQo :: g1 cmQm :: g1 cmQc :: g1 cmQk :: g1 cmS1 :: g1 cmS2 :: g1 cmS3 :: g1 cmT1 :: g1 ..} in PlonkupSetup {g2 Vector g1 PlonkupCircuitCommitments g1 PolyVec (ScalarFieldOf g1) n PolyVec (ScalarFieldOf g2) n ScalarFieldOf g1 PlonkupRelation p i n l (ScalarFieldOf g1) PlonkupCircuitPolynomials n g1 omega :: ScalarFieldOf g1 k1 :: ScalarFieldOf g1 k2 :: ScalarFieldOf g1 gs :: Vector g1 h0 :: g2 h1 :: g2 sigma1s :: PolyVec (ScalarFieldOf g1) n sigma2s :: PolyVec (ScalarFieldOf g1) n sigma3s :: PolyVec (ScalarFieldOf g1) n relation :: PlonkupRelation p i n l (ScalarFieldOf g1) polynomials :: PlonkupCircuitPolynomials n g1 commitments :: PlonkupCircuitCommitments g1 omega :: ScalarFieldOf g1 k1 :: ScalarFieldOf g1 k2 :: ScalarFieldOf g1 h1 :: g2 gs :: Vector g1 h0 :: g2 relation :: PlonkupRelation p i n l (ScalarFieldOf g1) sigma1s :: PolyVec (ScalarFieldOf g2) n sigma2s :: PolyVec (ScalarFieldOf g2) n sigma3s :: PolyVec (ScalarFieldOf g2) n polynomials :: PlonkupCircuitPolynomials n g1 commitments :: PlonkupCircuitCommitments g1 ..}