Complete integration of Mavros (including lookups)

Cargo.toml

@@ -193,8 +193,8 @@ ark-ff = { version = "0.5", features = ["asm", "std"] }
 ark-poly = "0.5"
 ark-serialize = "0.5"
 ark-std = { version = "0.5", features = ["std"] }
-mavros-vm = { git = "https://github.com/reilabs/mavros", rev = "3e47fd58001a0109a0314bc080b5246fd807ba04" }
-mavros-artifacts = { git = "https://github.com/reilabs/mavros", rev = "3e47fd58001a0109a0314bc080b5246fd807ba04" }
+mavros-vm = { git = "https://github.com/reilabs/mavros", rev = "7550b42e03d35b44781ff37f15b50773eb2a6fa0" }
+mavros-artifacts = { git = "https://github.com/reilabs/mavros", rev = "7550b42e03d35b44781ff37f15b50773eb2a6fa0" }
 spongefish = { git = "https://github.com/arkworks-rs/spongefish", features = [
   "ark-ff",
   "sha2",

noir-examples/sha256_35/Nargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "sha256_35"
+type = "bin"
+authors = [""]
+compiler_version = ">=1.0.0"
+
+[dependencies]
+sha256 = { tag = "v0.3.0", git = "https://github.com/noir-lang/sha256" }

noir-examples/sha256_35/Prover.toml

@@ -0,0 +1 @@
+input = [104, 101, 108, 108, 111]

noir-examples/sha256_35/src/main.nr

@@ -0,0 +1,30 @@
+use std::hash::sha256_compression;
+
+global H: [u32; 8] = [
+    0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
+    0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19,
+];
+
+fn main(input: [u8; 5]) {
+    let mut block: [u32; 16] = [0; 16];
+    block[0] = (input[0] as u32) * 16777216
+        + (input[1] as u32) * 65536
+        + (input[2] as u32) * 256
+        + (input[3] as u32);
+    block[1] = (input[4] as u32) * 16777216 + 0x800000;
+    block[15] = 40;
+
+    let mut state = H;
+    for _ in 0..35 {
+        state = sha256_compression(block, state);
+    }
+
+    assert(state[0] == 0x2b431f1f);
+    assert(state[1] == 0x9f7ccc65);
+    assert(state[2] == 0xb39b5188);
+    assert(state[3] == 0x8b7e8689);
+    assert(state[4] == 0x8ad1bc84);
+    assert(state[5] == 0x09f78be6);
+    assert(state[6] == 0xf0431b8d);
+    assert(state[7] == 0x97fcfb9c);
+}

provekit/common/src/mavros.rs

@@ -51,10 +51,34 @@ mod wasm_stubs {
         pub lookups_data_size:   usize,
     }
 
+    impl WitnessLayout {
+        pub const fn size(&self) -> usize {
+            self.algebraic_size
+                + self.multiplicities_size
+                + self.challenges_size
+                + self.tables_data_size
+                + self.lookups_data_size
+        }
+
+        pub const fn pre_commitment_size(&self) -> usize {
+            self.algebraic_size + self.multiplicities_size
+        }
+
+        pub const fn post_commitment_size(&self) -> usize {
+            self.challenges_size + self.tables_data_size + self.lookups_data_size
+        }
+    }
+
     #[derive(Debug, Clone, Copy, Serialize, Deserialize)]
     pub struct ConstraintsLayout {
         pub algebraic_size:    usize,
         pub tables_data_size:  usize,
         pub lookups_data_size: usize,
     }
+
+    impl ConstraintsLayout {
+        pub const fn size(&self) -> usize {
+            self.algebraic_size + self.tables_data_size + self.lookups_data_size
+        }
+    }
 }

provekit/common/src/prover.rs

@@ -70,10 +70,7 @@ impl Prover {
     pub fn size(&self) -> (usize, usize) {
         match self {
             Prover::Noir(p) => (p.r1cs.num_constraints(), p.r1cs.num_witnesses()),
-            Prover::Mavros(p) => (
-                p.constraints_layout.algebraic_size,
-                p.witness_layout.algebraic_size,
-            ),
+            Prover::Mavros(p) => (p.constraints_layout.size(), p.witness_layout.size()),
         }
     }
 

provekit/prover/src/lib.rs

@@ -5,14 +5,14 @@ use {
         r1cs::{CompressedLayers, CompressedR1CS},
         whir_r1cs::WhirR1CSProver,
     },
+    ::tracing::{debug, info, info_span, instrument},
     acir::native_types::{Witness, WitnessMap},
     anyhow::{Context, Result},
     provekit_common::{
         utils::noir_to_native, FieldElement, NoirElement, NoirProof, NoirProver, Prover,
         PublicInputs, TranscriptSponge,
     },
-    std::mem::size_of,
-    tracing::{debug, info_span, instrument},
+    std::mem::{size_of, take},
     whir::transcript::ProverState,
 };
 #[cfg(all(feature = "witness-generation", not(target_arch = "wasm32")))]
@@ -31,6 +31,7 @@ pub(crate) mod ec_arith;
 #[cfg(not(target_arch = "wasm32"))]
 pub mod input_utils;
 pub(crate) mod r1cs;
+mod tracing;
 mod whir_r1cs;
 mod witness;
 
@@ -184,6 +185,7 @@ impl Prove for NoirProver {
                 .collect::<Result<Vec<_>>>()?
         };
 
+        crate::tracing::log_commit_input("noir_w1", &w1, 1usize << self.whir_for_witness.m);
         let commitment_1 = self
             .whir_for_witness
             .commit(&mut merlin, num_witnesses, num_constraints, w1, true)
@@ -221,6 +223,7 @@ impl Prove for NoirProver {
                     .collect::<Result<Vec<_>>>()?
             };
 
+            crate::tracing::log_commit_input("noir_w2", &w2, 1usize << self.whir_for_witness.m);
             let commitment_2 = self
                 .whir_for_witness
                 .commit(&mut merlin, num_witnesses, num_constraints, w2, false)
@@ -280,6 +283,7 @@ impl Prove for MavrosProver {
             self.constraints_layout,
             &params,
         );
+        drop(self.witgen_binary);
 
         let num_public_inputs = self.num_public_inputs;
         let public_inputs = if num_public_inputs == 0 {
@@ -296,56 +300,84 @@ impl Prove for MavrosProver {
             .instance(&instance);
         let mut merlin = ProverState::new(&ds, TranscriptSponge::from_config(self.hash_config));
 
+        info!(
+            algebraic_size = self.witness_layout.algebraic_size,
+            multiplicities_size = self.witness_layout.multiplicities_size,
+            challenges_size = self.witness_layout.challenges_size,
+            tables_data_size = self.witness_layout.tables_data_size,
+            lookups_data_size = self.witness_layout.lookups_data_size,
+            pre_commitment_size = self.witness_layout.pre_commitment_size(),
+            post_commitment_size = self.witness_layout.post_commitment_size(),
+            total_witness_size = self.witness_layout.size(),
+            constraints_algebraic_size = self.constraints_layout.algebraic_size,
+            constraints_total_size = self.constraints_layout.size(),
+            scheme_domain_len = 1usize << self.whir_for_witness.m,
+            "Mavros witness layout"
+        );
+
+        let w1 = phase1.out_wit_pre_comm.clone();
+        crate::tracing::log_commit_input(
+            "mavros_w1_pre_commitment",
+            &w1,
+            1usize << self.whir_for_witness.m,
+        );
         let commitment_1 = self
             .whir_for_witness
             .commit(
                 &mut merlin,
                 self.witness_layout.size(),
                 self.constraints_layout.algebraic_size,
-                phase1.out_wit_pre_comm.clone(),
+                w1,
                 true,
             )
             .context("While committing to w1")?;
 
-        let commitments = if self.whir_for_witness.num_challenges > 0 {
+        let (commitments, witgen_result) = if self.whir_for_witness.num_challenges > 0 {
             let challenges: Vec<FieldElement> = (0..self.witness_layout.challenges_size)
                 .map(|_| merlin.verifier_message())
                 .collect();
 
             let witgen_result = mavros_interpreter::run_phase2(
-                phase1.clone(),
+                phase1,
                 &challenges,
                 self.witness_layout,
                 self.constraints_layout,
             );
 
+            let mut witgen_result = witgen_result;
+            let w2 = take(&mut witgen_result.out_wit_post_comm);
+            crate::tracing::log_commit_input(
+                "mavros_w2_post_commitment",
+                &w2,
+                1usize << self.whir_for_witness.m,
+            );
             let commitment_2 = self
                 .whir_for_witness
                 .commit(
                     &mut merlin,
                     self.witness_layout.size(),
                     self.constraints_layout.algebraic_size,
-                    witgen_result.out_wit_post_comm.clone(),
+                    w2,
                     false,
                 )
                 .context("While committing to w2")?;
 
-            vec![commitment_1, commitment_2]
+            (vec![commitment_1, commitment_2], witgen_result)
         } else {
-            mavros_interpreter::run_phase2(
-                phase1.clone(),
+            let witgen_result = mavros_interpreter::run_phase2(
+                phase1,
                 &[],
                 self.witness_layout,
                 self.constraints_layout,
             );
-            vec![commitment_1]
+            (vec![commitment_1], witgen_result)
         };
 
         let whir_r1cs_proof = self
             .whir_for_witness
             .prove_mavros(
                 merlin,
-                phase1,
+                witgen_result,
                 commitments,
                 &public_inputs,
                 self.witness_layout,

provekit/prover/src/r1cs.rs

@@ -1,13 +1,13 @@
 use {
     crate::witness::witness_builder::WitnessBuilderSolver,
+    ::tracing::instrument,
     acir::native_types::WitnessMap,
     anyhow::{Context, Result},
     provekit_common::{
         utils::batch_inverse_montgomery,
         witness::{LayerType, LayeredWitnessBuilders, WitnessBuilder},
         FieldElement, NoirElement, TranscriptSponge, R1CS,
     },
-    tracing::instrument,
     whir::transcript::ProverState,
 };
 

provekit/prover/src/tracing.rs

@@ -0,0 +1,19 @@
+use {
+    ::tracing::{debug, enabled, Level},
+    ark_std::Zero,
+    provekit_common::FieldElement,
+};
+
+pub(crate) fn log_commit_input(label: &str, values: &[FieldElement], scheme_domain_len: usize) {
+    if !enabled!(Level::DEBUG) {
+        return;
+    }
+
+    let input_len = values.len();
+    let input_padded_len = input_len.max(1).next_power_of_two();
+    let nonzero_entries = values.iter().filter(|v| !v.is_zero()).count();
+    debug!(
+        label,
+        input_len, input_padded_len, scheme_domain_len, nonzero_entries, "WHIR commit input"
+    );
+}

provekit/prover/src/whir_r1cs.rs

@@ -1,4 +1,5 @@
 use {
+    ::tracing::instrument,
     anyhow::{ensure, Result},
     ark_ff::UniformRand,
     ark_std::{One, Zero},
@@ -21,7 +22,6 @@ use {
         WhirR1CSScheme, R1CS,
     },
     std::borrow::Cow,
-    tracing::instrument,
     whir::{
         algebra::{dot, linear_form::LinearForm},
         protocols::whir_zk::Witness as WhirZkWitness,
@@ -31,7 +31,7 @@ use {
 #[cfg(not(target_arch = "wasm32"))]
 use {
     mavros_artifacts::{ConstraintsLayout, WitnessLayout},
-    mavros_vm::interpreter::Phase1Result,
+    mavros_vm::interpreter::WitgenResult,
 };
 
 pub struct BlindingState {
@@ -68,7 +68,7 @@ pub trait WhirR1CSProver {
     fn prove_mavros(
         &self,
         merlin: ProverState<TranscriptSponge>,
-        phase1: Phase1Result,
+        witgen: WitgenResult,
         commitments: Vec<WhirR1CSCommitment>,
         public_inputs: &PublicInputs,
         witness_layout: WitnessLayout,
@@ -191,7 +191,7 @@ impl WhirR1CSProver for WhirR1CSScheme {
     fn prove_mavros(
         &self,
         mut merlin: ProverState<TranscriptSponge>,
-        phase1: Phase1Result,
+        witgen: WitgenResult,
         commitments: Vec<WhirR1CSCommitment>,
         public_inputs: &PublicInputs,
         witness_layout: WitnessLayout,
@@ -205,7 +205,7 @@ impl WhirR1CSProver for WhirR1CSScheme {
             .as_ref()
             .expect("c1 must carry blinding state");
 
-        let [a, b, c] = [phase1.out_a, phase1.out_b, phase1.out_c];
+        let [a, b, c] = [witgen.out_a, witgen.out_b, witgen.out_c];
         let (alpha, blinding_eval) = run_zk_sumcheck_prover(
             a,
             b,
@@ -221,7 +221,7 @@ impl WhirR1CSProver for WhirR1CSScheme {
             calculate_evaluations_over_boolean_hypercube_for_eq(&alpha, 1 << alpha.len());
         let (ad_a, ad_b, ad_c, _) = mavros_vm::interpreter::run_ad(
             ad_binary,
-            &eq_alpha[..constraints_layout.algebraic_size],
+            &eq_alpha[..constraints_layout.size()],
             witness_layout,
             constraints_layout,
         );