Merge pull request #345 from worldfnd/adds-spark-squashed

Adds SPARK

Author: batmendbar

.gitignore

@@ -14,11 +14,16 @@
 *.pkp
 *.pkv
 *.np
+*.sp
+*.spc
+*.spctx
+spark_proofs/
 params_for_recursive_verifier
 params
 artifacts/
 spartan_vm_debug/
 mavros_debug/
+mavros/
 
 # Don't ignore benchmarking artifacts
 !tooling/provekit-bench/benches/*

Cargo.lock

@@ -20,6 +20,7 @@ members = [
   "tooling/provekit-wasm",
   "tooling/verifier-server",
   "ntt",
+  "provekit/spark",
   "poseidon2",
   "playground/passport-input-gen",
 ]
@@ -107,6 +108,7 @@ provekit-ffi = { path = "tooling/provekit-ffi" }
 provekit-gnark = { path = "tooling/provekit-gnark" }
 provekit-prover = { path = "provekit/prover", default-features = false }
 provekit-r1cs-compiler = { path = "provekit/r1cs-compiler" }
+provekit-spark = { path = "provekit/spark" }
 provekit-verifier = { path = "provekit/verifier" }
 provekit-verifier-server = { path = "tooling/verifier-server" }
 provekit-wasm = { path = "tooling/provekit-wasm" }

Cargo.toml

@@ -16,6 +16,7 @@ mod prove;
 mod scheme;
 mod skyscraper;
 mod solver;
+pub mod spark;
 mod transcript_sponge;
 mod verify;
 pub mod witness;
@@ -35,6 +36,7 @@ pub use {
     },
     skyscraper::SkyscraperPoW,
     solver::solve_witness_vec,
+    spark::{MatrixDimensions, SparkSetup, SparkWhirConfigs},
     transcript_sponge::TranscriptSponge,
     verify::Verify,
 };

provekit/backend/bn254/src/lib.rs

@@ -16,12 +16,16 @@ use {
         utils::sumcheck::calculate_evaluations_over_boolean_hypercube_for_eq, PublicInputs,
         WhirR1CSProof, WhirR1CSScheme,
     },
-    provekit_prover::{prove_from_alphas, run_zk_sumcheck_prover, WhirR1CSCommitment},
+    provekit_prover::{
+        prove_from_alphas_ctx, run_zk_sumcheck_prover, ProveFromAlphasCtx, SparkQueryData,
+        WhirR1CSCommitment,
+    },
     tracing::instrument,
     whir::{algebra::embedding::Identity, transcript::ProverState},
 };
 
 pub trait MavrosR1CSProver {
+    #[allow(clippy::too_many_arguments)]
     fn prove_mavros(
         &self,
         merlin: ProverState<TranscriptSponge>,
@@ -32,58 +36,128 @@ pub trait MavrosR1CSProver {
         constraints_layout: ConstraintsLayout,
         binary: &[u64],
     ) -> Result<WhirR1CSProof>;
+
+    /// Like [`Self::prove_mavros`], but also produces the SPARK query data as
+    /// a side output (the transcript is identical either way).
+    #[allow(clippy::too_many_arguments)]
+    fn prove_mavros_with_spark(
+        &self,
+        merlin: ProverState<TranscriptSponge>,
+        witgen: WitgenResult,
+        commitments: Vec<WhirR1CSCommitment<Bn254Field>>,
+        public_inputs: &PublicInputs<FieldElement>,
+        witness_layout: WitnessLayout,
+        constraints_layout: ConstraintsLayout,
+        binary: &[u64],
+    ) -> Result<(WhirR1CSProof, SparkQueryData<Bn254Field>)>;
 }
 
 impl MavrosR1CSProver for WhirR1CSScheme<Bn254Field> {
     #[instrument(skip_all)]
     fn prove_mavros(
         &self,
-        mut merlin: ProverState<TranscriptSponge>,
+        merlin: ProverState<TranscriptSponge>,
         witgen: WitgenResult,
         commitments: Vec<WhirR1CSCommitment<Bn254Field>>,
         public_inputs: &PublicInputs<FieldElement>,
         witness_layout: WitnessLayout,
         constraints_layout: ConstraintsLayout,
         binary: &[u64],
     ) -> Result<WhirR1CSProof> {
-        ensure!(!commitments.is_empty(), "Need at least one commitment");
-
-        let blinding = commitments[0]
-            .blinding
-            .as_ref()
-            .ok_or_else(|| anyhow::anyhow!("c1 must carry blinding state"))?;
-
-        // `g` is committed separately in the extension field; open `blinding_eval`
-        // against the blinding vector (g flattened at offset 0).
-        let (alpha, blinding_eval) = run_zk_sumcheck_prover(
-            &Identity::new(),
-            [witgen.out_a, witgen.out_b, witgen.out_c],
-            &mut merlin,
-            self.m_0,
-            &blinding.polynomial,
-            &blinding.vector,
-        );
-
-        let eq_alpha =
-            calculate_evaluations_over_boolean_hypercube_for_eq(&alpha, 1 << alpha.len());
-        let (ad_a, ad_b, ad_c, _) = run_ad(
-            binary,
-            &eq_alpha[..constraints_layout.size()],
+        let (proof, _) = prove_mavros_inner(
+            self,
+            merlin,
+            witgen,
+            commitments,
+            public_inputs,
             witness_layout,
             constraints_layout,
+            binary,
+            false,
         )?;
-        let alphas = [ad_a, ad_b, ad_c];
-
-        let blinding_weights = expand_powers::<4, _>(&alpha);
+        Ok(proof)
+    }
 
-        prove_from_alphas(
+    #[instrument(skip_all)]
+    fn prove_mavros_with_spark(
+        &self,
+        merlin: ProverState<TranscriptSponge>,
+        witgen: WitgenResult,
+        commitments: Vec<WhirR1CSCommitment<Bn254Field>>,
+        public_inputs: &PublicInputs<FieldElement>,
+        witness_layout: WitnessLayout,
+        constraints_layout: ConstraintsLayout,
+        binary: &[u64],
+    ) -> Result<(WhirR1CSProof, SparkQueryData<Bn254Field>)> {
+        let (proof, queries) = prove_mavros_inner(
             self,
             merlin,
+            witgen,
+            commitments,
+            public_inputs,
+            witness_layout,
+            constraints_layout,
+            binary,
+            true,
+        )?;
+        let queries = queries
+            .ok_or_else(|| anyhow::anyhow!("SPARK query data must be produced when requested"))?;
+        Ok((proof, queries))
+    }
+}
+
+#[instrument(skip_all)]
+#[allow(clippy::too_many_arguments)]
+fn prove_mavros_inner(
+    scheme: &WhirR1CSScheme<Bn254Field>,
+    mut merlin: ProverState<TranscriptSponge>,
+    witgen: WitgenResult,
+    commitments: Vec<WhirR1CSCommitment<Bn254Field>>,
+    public_inputs: &PublicInputs<FieldElement>,
+    witness_layout: WitnessLayout,
+    constraints_layout: ConstraintsLayout,
+    binary: &[u64],
+    produce_spark_query: bool,
+) -> Result<(WhirR1CSProof, Option<SparkQueryData<Bn254Field>>)> {
+    ensure!(!commitments.is_empty(), "Need at least one commitment");
+
+    let blinding = commitments[0]
+        .blinding
+        .as_ref()
+        .ok_or_else(|| anyhow::anyhow!("c1 must carry blinding state"))?;
+
+    // `g` is committed separately in the extension field; open `blinding_eval`
+    // against the blinding vector (g flattened at offset 0).
+    let (alpha, blinding_eval) = run_zk_sumcheck_prover(
+        &Identity::new(),
+        [witgen.out_a, witgen.out_b, witgen.out_c],
+        &mut merlin,
+        scheme.m_0,
+        &blinding.polynomial,
+        &blinding.vector,
+    );
+
+    let eq_alpha = calculate_evaluations_over_boolean_hypercube_for_eq(&alpha, 1 << alpha.len());
+    let (ad_a, ad_b, ad_c, _) = run_ad(
+        binary,
+        &eq_alpha[..constraints_layout.size()],
+        witness_layout,
+        constraints_layout,
+    )?;
+    let alphas = [ad_a, ad_b, ad_c];
+
+    let blinding_weights = expand_powers::<4, _>(&alpha);
+
+    prove_from_alphas_ctx(
+        scheme,
+        merlin,
+        ProveFromAlphasCtx {
             alphas,
             blinding_eval,
             blinding_weights,
             commitments,
-            public_inputs,
-        )
-    }
+            spark_row: produce_spark_query.then_some(alpha),
+        },
+        public_inputs,
+    )
 }