module ZkFold.Base.Protocol.Plonkup.PlonkupConstraint where
import Prelude hiding (Num (..), drop, length, replicate, sum,
take, (!!), (/), (^))
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Basic.Number
import ZkFold.Base.Data.Vector (Vector)
import ZkFold.Base.Protocol.Plonkup.LookupConstraint (LookupConstraint (..))
import ZkFold.Base.Protocol.Plonkup.PlonkConstraint (PlonkConstraint (..), toPlonkConstraint)
import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
data PlonkupConstraint i a = ConsPlonk (PlonkConstraint i a) | ConsLookup (LookupConstraint i a) |
getPlonkConstraint :: (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> PlonkConstraint i a
getPlonkConstraint (ConsPlonk PlonkConstraint i a
c) = PlonkConstraint i a
c
getPlonkConstraint PlonkupConstraint i a
_ = Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero
isLookupConstraint :: FiniteField a => PlonkupConstraint i a -> a
isLookupConstraint :: forall a (i :: Nat). FiniteField a => PlonkupConstraint i a -> a
isLookupConstraint (ConsLookup LookupConstraint i a
_) = a
forall a. MultiplicativeMonoid a => a
one
isLookupConstraint PlonkupConstraint i a
_ = a
forall a. AdditiveMonoid a => a
zero
getA :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i)
getA :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getA (ConsPlonk PlonkConstraint i a
c) = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x1 PlonkConstraint i a
c
getA (ConsLookup LookupConstraint i a
c) = 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))
-> SysVar (Vector i) -> Var a (Vector i)
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar (Vector i)
forall {k} (i :: Nat) (a :: k).
LookupConstraint i a -> SysVar (Vector i)
lkVar LookupConstraint i a
c
getA PlonkupConstraint i a
ConsExtra = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x1 (forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint @a Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero)
getB :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i)
getB :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getB (ConsPlonk PlonkConstraint i a
c) = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x2 PlonkConstraint i a
c
getB (ConsLookup LookupConstraint i a
c) = 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))
-> SysVar (Vector i) -> Var a (Vector i)
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar (Vector i)
forall {k} (i :: Nat) (a :: k).
LookupConstraint i a -> SysVar (Vector i)
lkVar LookupConstraint i a
c
getB PlonkupConstraint i a
ConsExtra = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x2 (forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint @a Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero)
getC :: forall a i . (Ord a, FiniteField a, KnownNat i) => PlonkupConstraint i a -> Var a (Vector i)
getC :: forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
PlonkupConstraint i a -> Var a (Vector i)
getC (ConsPlonk PlonkConstraint i a
c) = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x3 PlonkConstraint i a
c
getC (ConsLookup LookupConstraint i a
c) = 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))
-> SysVar (Vector i) -> Var a (Vector i)
forall a b. (a -> b) -> a -> b
$ LookupConstraint i a -> SysVar (Vector i)
forall {k} (i :: Nat) (a :: k).
LookupConstraint i a -> SysVar (Vector i)
lkVar LookupConstraint i a
c
getC PlonkupConstraint i a
ConsExtra = PlonkConstraint i a -> Var a (Vector i)
forall (i :: Nat) a. PlonkConstraint i a -> Var a (Vector i)
x3 (forall a (i :: Nat).
(Ord a, FiniteField a, KnownNat i) =>
Poly a (Var a (Vector i)) Nat -> PlonkConstraint i a
toPlonkConstraint @a Poly a (Var a (Vector i)) Nat
forall a. AdditiveMonoid a => a
zero)