Add merkle verify gate

.github/workflows/ci.yml

@@ -54,7 +54,7 @@ jobs:
       - name: Run examples
         run: |
           cargo run --package p3-circuit-prover --example fibonacci
-          cargo run --package p3-circuit-prover --example fake_merkle_verify
+          cargo run --package p3-circuit-prover --example mmcs_verify
 
   check_embedded:
     name: Build embedded
@@ -91,7 +91,7 @@ jobs:
           # cargo build --verbose --target ${{ env.target }} -p p3-field-air
           # cargo build --verbose --target ${{ env.target }} -p p3-fri-air
           # cargo build --verbose --target ${{ env.target }} -p p3-interpolation-air
-          cargo build --verbose --target ${{ env.target }} -p p3-merkle-tree-air
+          cargo build --verbose --target ${{ env.target }} -p p3-mmcs-air
           cargo build --verbose --target ${{ env.target }} -p p3-symmetric-air
           cargo build --verbose --target ${{ env.target }} -p p3-recursion
 

Cargo.toml

@@ -8,7 +8,7 @@ members = [
     "field-air",
     "fri-air",
     "interpolation-air",
-    "merkle-tree-air",
+    "mmcs-air",
     "recursion",
     "symmetric-air",
 ]
@@ -49,7 +49,10 @@ itertools = { version = "0.14.0", default-features = false, features = [
     "use_alloc",
 ] }
 rand = { version = "0.9.2", default-features = false, features = ["small_rng"] }
-serde = { version = "1.0", default-features = false, features = ["derive", "alloc"] }
+serde = { version = "1.0", default-features = false, features = [
+    "derive",
+    "alloc",
+] }
 thiserror = { version = "2.0", default-features = false }
 tracing = { version = "0.1.37", default-features = false, features = [
     "attributes",
@@ -66,7 +69,7 @@ p3-circuit-prover = { path = "circuit-prover", version = "0.1.0" }
 p3-field-air = { path = "field-air", version = "0.1.0" }
 p3-fri-air = { path = "fri-air", version = "0.1.0" }
 p3-interpolation-air = { path = "interpolation-air", version = "0.1.0" }
-p3-merkle-tree-air = { path = "merkle-tree-air", version = "0.1.0" }
+p3-mmcs-air = { path = "mmcs-air", version = "0.1.0" }
 p3-recursion = { path = "recursion", version = "0.1.0" }
 p3-symmetric-air = { path = "symmetric-air", version = "0.1.0" }
 

README.md

@@ -14,7 +14,7 @@ for a walkthrough of the recursion approach.
 
 ## Modular circuit builder & runtime policy
 
-The `CircuitBuilder<F>` uses a runtime policy to control which non-primitive operations (Merkle, FRI, etc.) are allowed. Primitive ops like `Const`, `Public`, `Add` are always available.
+The `CircuitBuilder<F>` uses a runtime policy to control which non-primitive operations (MMCS, FRI, etc.) are allowed. Primitive ops like `Const`, `Public`, `Add` are always available.
 
 By default, all non-primitive ops are disabled with `DefaultProfile`.
 Define a custom policy to enable them, or use `AllowAllProfile` to activate them all.

book/src/construction.md

@@ -86,7 +86,7 @@ each operation and the interaction between them, the `Witness` table can be enti
 
 ## Operation-specific STARK Chips
 
-Each operation family (e.g. addition, multiplication, Merkle path verification, FRI folding) has its own chip.
+Each operation family (e.g. addition, multiplication, MMCS path verification, FRI folding) has its own chip.
 
 A chip contains:
 
@@ -96,7 +96,7 @@ A chip contains:
 
 We distinguish two kind of chips: those representing native, i.e. primitive operations, and additional non-primitive ones, defined at runtime, that serve as precompiles to optimize certain operations.
 The recursion machine contains 4 primitive chips: `CONST` / `PUBLIC_INPUT` / `ADD` and `MUL`, with `SUB` and `DIV` being emulated via the `ADD` and `MUL` chips. This library aims at providing a certain
-number of non-primary chips so that projects can natively inherit from full recursive verifiers, which implies chips for FRI, Merkle paths verification, etc. Specific applications can also build their own
+number of non-primary chips so that projects can natively inherit from full recursive verifiers, which implies chips for FRI, MMCS path verification, etc. Specific applications can also build their own
 non-primitive chips and plug them at runtime.
 
 Going back to the previous example, prover and verifier can agree on the following logic for each chip:

circuit-prover/Cargo.toml

@@ -10,6 +10,7 @@ keywords.workspace = true
 categories.workspace = true
 
 [dependencies]
+itertools.workspace = true
 p3-air.workspace = true
 p3-baby-bear.workspace = true
 p3-challenger.workspace = true
@@ -20,13 +21,14 @@ p3-dft.workspace = true
 p3-field.workspace = true
 p3-fri.workspace = true
 p3-goldilocks.workspace = true
+p3-keccak.workspace = true
 p3-koala-bear.workspace = true
 p3-matrix.workspace = true
 p3-maybe-rayon.workspace = true
 p3-merkle-tree.workspace = true
+p3-mmcs-air.workspace = true
 p3-symmetric.workspace = true
 p3-uni-stark.workspace = true
-postcard = { version = "1.0", default-features = false, features = ["alloc"] }
 rand.workspace = true
 thiserror.workspace = true
 tracing.workspace = true
@@ -45,5 +47,5 @@ name = "fibonacci"
 path = "examples/fibonacci.rs"
 
 [[example]]
-name = "fake_merkle_verify"
-path = "examples/fake_merkle_verify.rs"
+name = "mmcs_verify"
+path = "examples/mmcs_verify.rs"

circuit-prover/examples/fibonacci.rs

@@ -3,7 +3,7 @@ use std::env;
 /// Fibonacci circuit: Compute F(n) and prove correctness
 /// Public input: expected_result (F(n))
 use p3_baby_bear::BabyBear;
-use p3_circuit::builder::CircuitBuilder;
+use p3_circuit::CircuitBuilder;
 use p3_circuit_prover::config::babybear_config::build_standard_config_babybear;
 use p3_circuit_prover::prover::ProverError;
 use p3_circuit_prover::{MultiTableProver, TablePacking};
@@ -35,7 +35,7 @@ fn main() -> Result<(), ProverError> {
         .and_then(|s| s.parse().ok())
         .unwrap_or(100);
 
-    let mut builder = CircuitBuilder::<F>::new();
+    let mut builder = CircuitBuilder::new();
 
     // Public input: expected F(n)
     let expected_result = builder.add_public_input();

circuit-prover/examples/mmcs_verify.rs

@@ -0,0 +1,128 @@
+use std::env;
+
+/// Mmcs verification circuit: Prove knowledge of a leaf in a Mmcs tree
+/// Public inputs: leaf_hash, leaf_index, expected_root
+/// Private inputs: mmcs path (siblings + directions)
+use p3_baby_bear::BabyBear;
+use p3_circuit::op::MmcsVerifyConfig;
+use p3_circuit::tables::MmcsPrivateData;
+use p3_circuit::{CircuitBuilder, ExprId, MmcsOps, NonPrimitiveOpPrivateData};
+use p3_circuit_prover::MultiTableProver;
+use p3_circuit_prover::config::babybear_config::{
+    baby_bear_standard_compression_function, build_standard_config_babybear,
+};
+use p3_circuit_prover::prover::ProverError;
+use p3_field::PrimeCharacteristicRing;
+use p3_field::extension::BinomialExtensionField;
+
+type F = BinomialExtensionField<BabyBear, 4>;
+
+fn main() -> Result<(), ProverError> {
+    let depth = env::args().nth(1).and_then(|s| s.parse().ok()).unwrap_or(3);
+    let config = build_standard_config_babybear();
+    let compress = baby_bear_standard_compression_function();
+    let mmcs_config = MmcsVerifyConfig::babybear_quartic_extension_default(false);
+
+    let mut builder = CircuitBuilder::new();
+    builder.enable_mmcs(&mmcs_config);
+
+    // Public inputs: leaf hash and expected root hash
+    let leaf_hash = (0..mmcs_config.ext_field_digest_elems)
+        .map(|_| builder.add_public_input())
+        .collect::<Vec<ExprId>>();
+    let index = builder.add_public_input();
+    let expected_root = (0..mmcs_config.ext_field_digest_elems)
+        .map(|_| builder.add_public_input())
+        .collect::<Vec<ExprId>>();
+    // Add a Mmcs verification operation
+    // This declares that leaf_hash and expected_root are connected to witness bus
+    // The AIR constraints will verify the Mmcs path is valid
+    let mmcs_op_id = builder.add_mmcs_verify(&leaf_hash, &index, &expected_root)?;
+
+    let circuit = builder.build()?;
+    let mut runner = circuit.runner();
+
+    // Set public inputs
+    let leaf_value = [
+        F::ZERO,
+        F::ZERO,
+        F::ZERO,
+        F::ZERO,
+        F::ZERO,
+        F::ZERO,
+        F::ZERO,
+        F::from_u64(42),
+    ]; // Our leaf value
+    let siblings: Vec<(Vec<F>, Option<Vec<F>>)> = (0..depth)
+        .map(|i| {
+            (
+                vec![
+                    F::ZERO,
+                    F::ZERO,
+                    F::ZERO,
+                    F::ZERO,
+                    F::ZERO,
+                    F::ZERO,
+                    F::ZERO,
+                    F::from_u64((i + 1) * 10),
+                ],
+                if i % 2 == 0 {
+                    None
+                } else {
+                    Some(vec![
+                        F::ZERO,
+                        F::ZERO,
+                        F::ZERO,
+                        F::ZERO,
+                        F::ZERO,
+                        F::ZERO,
+                        F::ZERO,
+                        F::from_u64(i + 1),
+                    ])
+                },
+            )
+        })
+        .collect(); // The siblings, containing extra siblings every other level
+    let directions: Vec<bool> = (0..depth).map(|i| i % 2 == 0).collect();
+    // the index is 0b1010...
+    let index_value = F::from_u64(
+        (0..32)
+            .zip(directions.iter())
+            .filter(|(_, dir)| **dir)
+            .map(|(i, _)| 1 << i)
+            .sum(),
+    );
+    let MmcsPrivateData {
+        path_states: intermediate_states,
+        ..
+    } = MmcsPrivateData::new(&compress, &mmcs_config, &leaf_value, &siblings, &directions)?;
+    let expected_root_value = intermediate_states
+        .last()
+        .expect("There is always at least the leaf hash")
+        .clone();
+
+    let mut public_inputs = vec![];
+    public_inputs.extend(leaf_value);
+    public_inputs.push(index_value);
+    public_inputs.extend(&expected_root_value);
+
+    runner.set_public_inputs(&public_inputs)?;
+    // Set private Mmcs path data
+    runner.set_non_primitive_op_private_data(
+        mmcs_op_id,
+        NonPrimitiveOpPrivateData::MmcsVerify(MmcsPrivateData::new(
+            &compress,
+            &mmcs_config,
+            &leaf_value,
+            &siblings,
+            &directions,
+        )?),
+    )?;
+
+    let traces = runner.run()?;
+    let multi_prover = MultiTableProver::new(config).with_mmcs_table(mmcs_config.into());
+    let proof = multi_prover.prove_all_tables(&traces)?;
+    multi_prover.verify_all_tables(&proof)?;
+
+    Ok(())
+}