Skip to content

Commit

Permalink
Merge pull request #319 from zkFold/vks4git/309/constraint_error
Browse files Browse the repository at this point in the history 
Vks4git/309/constraint error
  • Loading branch information
@TurtlePU
TurtlePU authored Oct 30, 2024
2 parents 30ad347 + 3ccfc12 commit 6566feb
Show file tree
Hide file tree
Showing 3 changed files with 45 additions and 20 deletions.
2 changes: 2 additions & 0 deletions symbolic-base/src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,8 @@ instance Polynomial c i j => AdditiveSemigroup (Poly c i j) where
go ls [] = ls
go [] rs = rs
go ((cl, ml):ls) ((cr, mr):rs)
| cl == zero = go ls ((cr, mr):rs)
| cr == zero = go ((cl, ml):ls) rs
| ml == mr =
if cl + cr == zero
then go ls rs
Expand Down
26 changes: 15 additions & 11 deletions symbolic-base/src/ZkFold/Base/Protocol/Plonkup/PlonkConstraint.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ 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 (..), mapMaybe)
import Data.Maybe (Maybe (..), fromMaybe, mapMaybe)
import Data.Ord (Ord)
import GHC.IsList (IsList (..))
import GHC.TypeNats (KnownNat)
Expand All @@ -21,7 +21,8 @@ import Test.QuickCheck (Arbitrary
import Text.Show (Show)

import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Polynomials.Multivariate (Poly, polynomial, var, variables)
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)
Expand Down Expand Up @@ -53,19 +54,19 @@ instance (Ord a, Arbitrary a, Binary a, KnownNat i) => Arbitrary (PlonkConstrain

toPlonkConstraint :: forall a i . (Ord a, FiniteField a, KnownNat i) => Poly a (Var a (Vector i)) Natural -> PlonkConstraint i a
toPlonkConstraint p =
let xs = toList (variables p)
let xs = Just <$> toList (variables p)
perms = nubOrd $ map (take 3) $ permutations $ case length xs of
0 -> [ConstVar one, ConstVar one, ConstVar one]
1 -> [ConstVar one, ConstVar one, head xs, head xs]
2 -> [ConstVar one] ++ xs ++ xs
0 -> [Nothing, Nothing, Nothing]
1 -> [Nothing, Nothing, head xs, head xs]
2 -> [Nothing] ++ xs ++ xs
_ -> xs ++ xs

getCoef :: Map (Var a (Vector i)) Natural -> a
getCoef m = case find (\(_, as) -> m == as) (toList p) of
getCoef :: Map (Maybe (Var a (Vector i))) Natural -> a
getCoef m = case find (\(_, as) -> m == Map.mapKeys Just as) (toList p) of
Just (c, _) -> c
_ -> zero

getCoefs :: [Var a (Vector i)] -> Maybe (PlonkConstraint i a)
getCoefs :: [Maybe (Var a (Vector i))] -> Maybe (PlonkConstraint i a)
getCoefs [a, b, c] = do
let xa = [(a, 1)]
xb = [(b, 1)]
Expand All @@ -77,8 +78,11 @@ toPlonkConstraint p =
qr = getCoef $ fromList xb
qo = getCoef $ fromList xc
qc = getCoef Map.empty
guard $ p - polynomial [(qm, fromList xaxb), (ql, fromList xa), (qr, fromList xb), (qo, fromList xc), (qc, one)] == zero
return $ PlonkConstraint qm ql qr qo qc a b c
guard $ evalPolynomial evalMonomial (var . Just) p - polynomial [(qm, fromList xaxb), (ql, fromList xa), (qr, fromList xb), (qo, fromList xc), (qc, one)] == zero
let va = fromMaybe (ConstVar one) a
vb = fromMaybe (ConstVar one) b
vc = fromMaybe (ConstVar one) c
return $ PlonkConstraint qm ql qr qo qc va vb vc
getCoefs _ = Nothing

in head $ mapMaybe getCoefs perms
Expand Down
37 changes: 28 additions & 9 deletions symbolic-base/test/Tests/Plonkup.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

module Tests.Plonkup (specPlonkup) where

import Control.Monad (forM_)
import Data.Bool (Bool)
import Data.ByteString (ByteString)
import Data.Eq (Eq (..))
Expand All @@ -18,13 +19,15 @@ import Test.QuickCheck

import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Basic.Field (fromZp)
import ZkFold.Base.Algebra.Basic.Number (KnownNat)
import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural)
import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_G1, BLS12_381_G2)
import ZkFold.Base.Algebra.EllipticCurve.Class (EllipticCurve (..))
import ZkFold.Base.Algebra.Polynomials.Multivariate as PM
import ZkFold.Base.Algebra.Polynomials.Univariate
import ZkFold.Base.Data.Vector (Vector, fromVector)
import ZkFold.Base.Protocol.NonInteractiveProof (HaskellCore, setupProve)
import ZkFold.Base.Protocol.Plonkup hiding (omega)
import ZkFold.Base.Protocol.Plonkup.PlonkConstraint
import ZkFold.Base.Protocol.Plonkup.Prover (plonkupProve)
import ZkFold.Base.Protocol.Plonkup.Prover.Secret
import ZkFold.Base.Protocol.Plonkup.Relation (PlonkupRelation (..))
Expand All @@ -33,10 +36,23 @@ import ZkFold.Base.Protocol.Plonkup.Utils (sortByList
import ZkFold.Base.Protocol.Plonkup.Witness (PlonkupWitnessInput)
import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

-- TODO: uncomment after refactoring
-- propPlonkConstraintConversion :: (Eq a, FiniteField a) => PlonkConstraint 1 a -> Bool
-- propPlonkConstraintConversion p =
-- toPlonkConstraint (fromPlonkConstraint p) == p
-- | Polynomial types and specific polynomials that were causing exceptions
--
problematicPolynomials :: (Ord a, FiniteField a) => [PM.Poly a (Var a (Vector 1)) Natural]
problematicPolynomials =
[ var (ConstVar one)
, var (ConstVar zero)
, var (ConstVar $ one + one)
, let v1 = SysVar (NewVar "y\ETX^\246\226\195\154S\130M\tL\146y\248\201\162\220 \237n6p\bC\151\186\241\US\136\225\139")
v2 = SysVar (NewVar "~\180\185\222\SOH!\t\254\155\v\SI\187\&9\227\163|^\168Z\184Q\129\rN\218\SYN\GSp\189\139~^")
in polynomial [(one, M $ fromList [(v1, 1), (v2, 1)])]
, polynomial [(one, M $ fromList [(SysVar (NewVar "v1"), 1), (SysVar (NewVar "v2"), 1)])]
, polynomial [(one, M $ fromList [(SysVar (NewVar "v1"), 1), (ConstVar one, 1)])]
]

propPlonkConstraintConversion :: (Ord a, FiniteField a) => PlonkConstraint 1 a -> Bool
propPlonkConstraintConversion p =
toPlonkConstraint (fromPlonkConstraint p) == p

propPlonkupRelationHolds :: forall i n l a . (KnownNat n, Arithmetic a) => PlonkupRelation i n l a -> Vector i a -> Bool
propPlonkupRelationHolds PlonkupRelation {..} w =
Expand Down Expand Up @@ -141,10 +157,13 @@ propLinearizationPolyEvaluation plonk witness secret =

specPlonkup :: IO ()
specPlonkup = hspec $ do
describe "Plonkup specification (SLOW)" $ do
-- TODO: uncomment after refactoring
-- describe "Conversion to Plonk constraints and back" $ do
-- it "produces equivalent polynomials" $ property $ propPlonkConstraintConversion @(ScalarField BLS12_381_G1)
describe "Plonkup specification" $ do
describe "Conversion to Plonk constraints and back" $ do
it "produces equivalent polynomials" $ property $ propPlonkConstraintConversion @(ScalarField BLS12_381_G1)
it "handcrafted polynomials do not cause exceptions " $
forM_ problematicPolynomials $ \p -> fromPlonkConstraint (toPlonkConstraint @(ScalarField BLS12_381_G1) p) `shouldBe` p
it "'ConstVar a' does not cause exceptions " $
property $ \v -> fromPlonkConstraint (toPlonkConstraint @(ScalarField BLS12_381_G1) @1 (var $ ConstVar v)) == var (ConstVar v)
describe "Sort by list is correct" $ do
it "should hold" $ property $ propSortByListIsCorrect @Int
describe "Plonkup relation" $ do
Expand Down

0 comments on commit 6566feb

Please sign in to comment.