From d46edfd8ac8f35323a65197f4e1550f43e64a313 Mon Sep 17 00:00:00 2001 From: Luca Dall'Ava Date: Thu, 27 Mar 2025 16:10:30 +0100 Subject: [PATCH 1/4] wip improvements for testing IVC --- symbolic-base/test/Tests/Protocol/IVC.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/symbolic-base/test/Tests/Protocol/IVC.hs b/symbolic-base/test/Tests/Protocol/IVC.hs index 88f9abbc0..00f244082 100644 --- a/symbolic-base/test/Tests/Protocol/IVC.hs +++ b/symbolic-base/test/Tests/Protocol/IVC.hs @@ -7,7 +7,7 @@ import GHC.Generics (U1 (..), type (:*: import GHC.IsList (IsList (..)) import Prelude hiding (Num (..), pi, replicate, sum, (+)) import Test.Hspec (Spec, describe, it) -import Test.QuickCheck (property, withMaxSuccess) +import Test.QuickCheck (property, withMaxSuccess, (==>)) import ZkFold.Base.Algebra.Basic.Class (FromConstant (..), one, zero) import ZkFold.Base.Algebra.Basic.Field (Zp) @@ -132,6 +132,11 @@ specAccumulatorScheme = do describe "verifier" $ do it "must output zeros" $ do withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) + it "must reject on different predicates" $ do + withMaxSuccess 10 $ property $ \p q -> p!=q ==> testVerifierResult (testPredicate q) != testAccumulatorInstance (testPredicate p) + describe "decider" $ do + it "must output zeros" $ do + withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == -- vector of zeros: (Vector k (c f), c f) specIVC :: Spec specIVC = do From 67295d83b54db4c18a4d6709b1566e0508285ffc Mon Sep 17 00:00:00 2001 From: Luca Dall'Ava Date: Fri, 28 Mar 2025 15:52:38 +0100 Subject: [PATCH 2/4] - Added a couple of small tests in regarding the accumulator scheme - Tentative description of a function reiterating the prover --- symbolic-base/test/Tests/Protocol/IVC.hs | 58 +++++++++++++++++++----- 1 file changed, 46 insertions(+), 12 deletions(-) diff --git a/symbolic-base/test/Tests/Protocol/IVC.hs b/symbolic-base/test/Tests/Protocol/IVC.hs index 00f244082..91583a9be 100644 --- a/symbolic-base/test/Tests/Protocol/IVC.hs +++ b/symbolic-base/test/Tests/Protocol/IVC.hs @@ -89,31 +89,61 @@ testPublicInput phi = testAccumulatorScheme :: PHI -> AccumulatorScheme D 1 I C F testAccumulatorScheme = accumulatorScheme @(MiMCHash F) -testAccumulator :: PHI -> Accumulator K I C F +testAccumulator :: PHI -> Accumulator K I C F -- accumulator in prover output testAccumulator phi = let s = testAccumulatorScheme phi in fst $ prover s (initAccumulator phi) $ testInstanceProofPair phi +testProverMismsatch :: PHI -> PHI -> PHI -> Accumulator K I C F -- prover output +testProverMismsatch phi1 phi2 phi3 = + let s = testAccumulatorScheme phi1 + in prover s (initAccumulator phi2) $ testInstanceProofPair phi3 + testAccumulatorInstance :: PHI -> AccumulatorInstance K I C F testAccumulatorInstance phi = let Accumulator ai _ = testAccumulator phi in ai -testAccumulationProof :: PHI -> Vector (D - 1) (C F) +testAccumulationProof :: PHI -> Vector (D - 1) (C F) -- accumulation proof in prover output testAccumulationProof phi = let s = testAccumulatorScheme phi in snd $ prover s (initAccumulator phi) $ testInstanceProofPair phi --- testDeciderResult :: PHI -> (Vector K (C F), C F) --- testDeciderResult phi = --- let s = testAccumulatorScheme phi --- in decider s $ testAccumulator phi - testVerifierResult :: PHI -> AccumulatorInstance K I C F testVerifierResult phi = let s = testAccumulatorScheme phi in verifier s (testPublicInput phi) (testNarkProof phi) (initAccumulatorInstance phi) (testAccumulationProof phi) +testDeciderResult :: PHI -> (Vector K (C F), C F) +testDeciderResult phi = decider (testAccumulator phi) + --let s = testAccumulatorScheme phi + --in decider (testAccumulator phi) + +{-- Tentative code: I would like to itereate the prover to accumulate at each step a new proof associated with a new predicate and then output the vector of accumulator-proof pairs. Then we can call the verifier to check each iteration step and call teh decider on the last accumulator to check the final result. + +iterateProver :: [PHI] -> [(Accumulator K I C F, Vector (D - 1) (C F))] +iterateProver phis = + let s = testAccumulatorScheme (head phis) -- Use the scheme from the first PHI + initialAcc = initAccumulator (head phis) -- Initialize with the first PHI + iterateStep (acc, results) phi = + let (newAcc, proofVec) = prover s acc (testInstanceProofPair phi) -- Prover step + in (newAcc, results ++ [(newAcc, proofVec)]) -- Append the new accumulator and proof + in snd $ foldl iterateStep (initialAcc, []) phis + +iterateProverVerifier :: [PHI] -> (Accumulator K I C F, [Vector (D - 1) (C F)]) +iterateProverVerifier phis = + let s = testAccumulatorScheme (head phis) -- Use the scheme from the first PHI + initialAcc = initAccumulator (head phis) -- Initialize with the first PHI + iterateStep (acc, allProofs) phi = + let proof = testInstanceProofPair phi + (newAcc, proofVec) = prover s acc proof -- Prover step + verifierAcc = verifier s (testPublicInput phi) (testNarkProof phi) (AccumulatorInstance newAcc) proofVec + in if verifierAcc == AccumulatorInstance newAcc + then (newAcc, allProofs ++ [proofVec]) -- Append the proofVec to the list of proofs + else error "Verification failed: Prover and Verifier accumulators do not match" + in foldl iterateStep (initialAcc, []) phis +--} + specAlgebraicMap :: Spec specAlgebraicMap = do describe "Algebraic map specification" $ do @@ -123,22 +153,26 @@ specAlgebraicMap = do \p -> algebraicMap @D (testPredicate p) (testPublicInput $ testPredicate p) (testMessages $ testPredicate p) (unsafeToVector []) one == replicate (acSizeN $ testPredicateCircuit p) zero +zeroVector :: (Num (c f), KnownNat k) => (Vector k (c f), c f) +zeroVector = (replicate zero, zero) + specAccumulatorScheme :: Spec specAccumulatorScheme = do describe "Accumulator scheme specification" $ do - -- describe "decider" $ do - -- it "must output zeros" $ do - -- withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == (singleton zero, zero) describe "verifier" $ do it "must output zeros" $ do withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q -> p!=q ==> testVerifierResult (testPredicate q) != testAccumulatorInstance (testPredicate p) + it "must reject on different predicates" $ do + withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate p) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate q) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate r) describe "decider" $ do it "must output zeros" $ do - withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == -- vector of zeros: (Vector k (c f), c f) + withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == zeroVector (C F) C F + it "must reject on different predicates" $ do + withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ decider testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != zeroVector (C F) C F specIVC :: Spec specIVC = do specAlgebraicMap - specAccumulatorScheme + specAccumulatorScheme \ No newline at end of file From a5eb409606a891a2b39d19f2695c5437b615dc74 Mon Sep 17 00:00:00 2001 From: Luca-DallAva Date: Fri, 28 Mar 2025 15:06:38 +0000 Subject: [PATCH 3/4] stylish-haskell auto-commit --- symbolic-base/test/Tests/Protocol/IVC.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/symbolic-base/test/Tests/Protocol/IVC.hs b/symbolic-base/test/Tests/Protocol/IVC.hs index 91583a9be..93153a4cd 100644 --- a/symbolic-base/test/Tests/Protocol/IVC.hs +++ b/symbolic-base/test/Tests/Protocol/IVC.hs @@ -97,7 +97,7 @@ testAccumulator phi = testProverMismsatch :: PHI -> PHI -> PHI -> Accumulator K I C F -- prover output testProverMismsatch phi1 phi2 phi3 = let s = testAccumulatorScheme phi1 - in prover s (initAccumulator phi2) $ testInstanceProofPair phi3 + in prover s (initAccumulator phi2) $ testInstanceProofPair phi3 testAccumulatorInstance :: PHI -> AccumulatorInstance K I C F testAccumulatorInstance phi = @@ -164,15 +164,15 @@ specAccumulatorScheme = do withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q -> p!=q ==> testVerifierResult (testPredicate q) != testAccumulatorInstance (testPredicate p) - it "must reject on different predicates" $ do + it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate p) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate q) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate r) describe "decider" $ do it "must output zeros" $ do withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == zeroVector (C F) C F - it "must reject on different predicates" $ do + it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ decider testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != zeroVector (C F) C F specIVC :: Spec specIVC = do specAlgebraicMap - specAccumulatorScheme \ No newline at end of file + specAccumulatorScheme From 8cd271470f49d0066aa9d954c66baf0ba18c1687 Mon Sep 17 00:00:00 2001 From: Luca Dall'Ava Date: Mon, 31 Mar 2025 16:46:13 +0200 Subject: [PATCH 4/4] Completed specAccumulatorScheme, inital changes to decribe specIVCScheme --- symbolic-base/test/Tests/Protocol/IVC.hs | 59 +++++++++++++++--------- 1 file changed, 37 insertions(+), 22 deletions(-) diff --git a/symbolic-base/test/Tests/Protocol/IVC.hs b/symbolic-base/test/Tests/Protocol/IVC.hs index 91583a9be..d682f66af 100644 --- a/symbolic-base/test/Tests/Protocol/IVC.hs +++ b/symbolic-base/test/Tests/Protocol/IVC.hs @@ -25,6 +25,7 @@ import ZkFold.Base.Protocol.IVC.NARK (NARKInstanceProof import ZkFold.Base.Protocol.IVC.Oracle (MiMCHash) import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..), predicate) import ZkFold.Base.Protocol.IVC.SpecialSound (specialSoundProtocol) +import ZkFold.Base.Protocol.IVC.Internal (IVCProof (..), IVCAssumptions (..), noIVCProof, ivcSetup, ivcProve, ivcVerify) import ZkFold.Prelude (replicate) import ZkFold.Symbolic.Class (BaseField, Symbolic) import ZkFold.Symbolic.Compiler (ArithmeticCircuit, acSizeN) @@ -41,6 +42,11 @@ type SPS = FiatShamir 1 I P C [F] [F] F type D = 2 type PARDEG = 5 type PAR = PolyVec F PARDEG +type IVCPROOF = IVCProof K C F +-- type ctx0 +-- type ctx1 +-- type algo +-- type IVCASSUMPTIONS = IVCAssumptions ??? testFunction :: forall ctx . (Symbolic ctx, FromConstant F (BaseField ctx)) => PAR -> Vector 1 (FieldElement ctx) -> U1 (FieldElement ctx) -> Vector 1 (FieldElement ctx) @@ -119,30 +125,27 @@ testDeciderResult phi = decider (testAccumulator phi) --let s = testAccumulatorScheme phi --in decider (testAccumulator phi) -{-- Tentative code: I would like to itereate the prover to accumulate at each step a new proof associated with a new predicate and then output the vector of accumulator-proof pairs. Then we can call the verifier to check each iteration step and call teh decider on the last accumulator to check the final result. - -iterateProver :: [PHI] -> [(Accumulator K I C F, Vector (D - 1) (C F))] -iterateProver phis = - let s = testAccumulatorScheme (head phis) -- Use the scheme from the first PHI - initialAcc = initAccumulator (head phis) -- Initialize with the first PHI - iterateStep (acc, results) phi = - let (newAcc, proofVec) = prover s acc (testInstanceProofPair phi) -- Prover step - in (newAcc, results ++ [(newAcc, proofVec)]) -- Append the new accumulator and proof - in snd $ foldl iterateStep (initialAcc, []) phis - -iterateProverVerifier :: [PHI] -> (Accumulator K I C F, [Vector (D - 1) (C F)]) +iterateProverVerifier :: [PHI] -> (Accumulator K I C F, Vector (D - 1) (C F)) iterateProverVerifier phis = - let s = testAccumulatorScheme (head phis) -- Use the scheme from the first PHI - initialAcc = initAccumulator (head phis) -- Initialize with the first PHI + let initialAcc = initAccumulator (head phis) -- Initialize with the first PHI + initialProof = testAccumulationProof (head phis) -- Initialize with the first proof iterateStep (acc, allProofs) phi = - let proof = testInstanceProofPair phi + let s = testAccumulatorScheme (phi) -- Use the scheme from the first PHI + proof = testInstanceProofPair phi (newAcc, proofVec) = prover s acc proof -- Prover step verifierAcc = verifier s (testPublicInput phi) (testNarkProof phi) (AccumulatorInstance newAcc) proofVec in if verifierAcc == AccumulatorInstance newAcc - then (newAcc, allProofs ++ [proofVec]) -- Append the proofVec to the list of proofs + --then (newAcc, allProofs ++ [proofVec]) -- Append the proofVec to the list of proofs + then (newAcc, proofVec) else error "Verification failed: Prover and Verifier accumulators do not match" - in foldl iterateStep (initialAcc, []) phis ---} + in foldl iterateStep (initialAcc, initialProof) (tail phis) --foldl f s [x1, ..., xn] = f ( ... (f (f s x1) x2) ... ) xn + +testTrivialIVCProof :: K -> C -> F -> IVCPROOF +testTrivialIVCProof k c f = noIVCProof k f c + +testIVCProver :: PHI -> IVCPROOF + +-- testIVCProver :: PHI -> Accumulator K I C F specAlgebraicMap :: Spec specAlgebraicMap = do @@ -161,18 +164,30 @@ specAccumulatorScheme = do describe "Accumulator scheme specification" $ do describe "verifier" $ do it "must output zeros" $ do - withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) + withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) -- 1 iteration of prover 1 of verifier it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q -> p!=q ==> testVerifierResult (testPredicate q) != testAccumulatorInstance (testPredicate p) - it "must reject on different predicates" $ do + it "must reject on different predicates" $ do -- withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate p) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate q) && fst $ testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != testVerifierResult (testPredicate r) describe "decider" $ do - it "must output zeros" $ do + it "must output zeros" $ do -- test decider on 1 iteration withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == zeroVector (C F) C F it "must reject on different predicates" $ do withMaxSuccess 10 $ property $ \p q r -> p!=q || p!=r || q!=r ==> fst $ decider testProverMismsatch (testPredicate q) (testPredicate p) (testPredicate r) != zeroVector (C F) C F + describe "accumulator scheme" $ do + it "must not reject and output zeros" $ do + withMaxSuccess 10 $ property $ \p -> decider $ fst $ iterateProverVerifier (p) == zeroVector (C F) C F + it "verifier must reject on mismatched pairs accumulator--accumulation-proof" $ do + withMaxSuccess 10 $ property $ \p q -> p!=q ==> verifier (testAccumulatorScheme p) (testPublicInput p) (testNarkProof p) (initAccumulatorInstance p) (testAccumulationProof q) != testAccumulatorInstance (testPredicate p) && verifier (testAccumulatorScheme p) (testPublicInput p) (testNarkProof p) (initAccumulatorInstance p) (testAccumulationProof q) != testAccumulatorInstance (testPredicate q) + + +specIVCScheme :: Spec +specIVCScheme = do + describe "IVC protocol specification" $ do + it "IVC prover is well formed and verifier accpets" $ do + withMaxSuccess 10 $ property $ -- complete specIVC :: Spec specIVC = do - specAlgebraicMap + specAlgebraicMap specAccumulatorScheme \ No newline at end of file