feat: public value validity assertions (#1532)

crates/prover/Cargo.toml

@@ -20,6 +20,7 @@ sp1-recursion-circuit-v2 = { workspace = true }
 sp1-recursion-gnark-ffi = { workspace = true }
 sp1-core-machine = { workspace = true }
 sp1-stark = { workspace = true }
+p3-symmetric = { workspace = true }
 sp1-core-executor = { workspace = true }
 sp1-primitives = { workspace = true }
 p3-field = { workspace = true }

crates/prover/src/build.rs

@@ -3,7 +3,7 @@ use std::{borrow::Borrow, path::PathBuf};
 use p3_baby_bear::BabyBear;
 use sp1_core_executor::SP1Context;
 use sp1_core_machine::io::SP1Stdin;
-use sp1_recursion_circuit_v2::machine::{SP1CompressRootVerifier, SP1CompressWitnessValues};
+use sp1_recursion_circuit_v2::machine::{SP1CompressWitnessValues, SP1WrapVerifier};
 use sp1_recursion_compiler::{
     config::OuterConfig,
     constraints::{Constraint, ConstraintCompiler},
@@ -179,7 +179,7 @@ fn build_outer_circuit(template_input: &SP1CompressWitnessValues<OuterSC>) -> Ve
     let wrap_span = tracing::debug_span!("build wrap circuit").entered();
     let mut builder = Builder::<OuterConfig>::default();
     let input = template_input.read(&mut builder);
-    SP1CompressRootVerifier::verify(&mut builder, &wrap_machine, input);
+    SP1WrapVerifier::verify(&mut builder, &wrap_machine, input);
 
     let mut backend = ConstraintCompiler::<OuterConfig>::default();
     let operations = backend.emit(builder.into_operations());

crates/prover/src/lib.rs

@@ -75,10 +75,10 @@ use sp1_recursion_core_v2::{
 use sp1_recursion_circuit_v2::{
     hash::FieldHasher,
     machine::{
-        SP1CompressRootVerifier, SP1CompressRootVerifierWithVKey, SP1CompressWithVKeyVerifier,
+        PublicValuesOutputDigest, SP1CompressRootVerifierWithVKey, SP1CompressWithVKeyVerifier,
         SP1CompressWithVKeyWitnessValues, SP1CompressWithVkeyShape, SP1CompressWitnessValues,
         SP1DeferredVerifier, SP1DeferredWitnessValues, SP1MerkleProofWitnessValues,
-        SP1RecursionShape, SP1RecursionWitnessValues, SP1RecursiveVerifier,
+        SP1RecursionShape, SP1RecursionWitnessValues, SP1RecursiveVerifier, SP1WrapVerifier,
     },
     merkle_tree::MerkleTree,
     witness::Witnessable,
@@ -371,6 +371,7 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
                     self.compress_prover.machine(),
                     input,
                     self.vk_verification,
+                    PublicValuesOutputDigest::Reduce,
                 );
                 let operations = builder.into_operations();
                 builder_span.exit();
@@ -426,7 +427,7 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
 
         let input = input.read(&mut builder);
         // Verify the proof.
-        SP1CompressRootVerifier::verify(&mut builder, self.shrink_prover.machine(), input);
+        SP1WrapVerifier::verify(&mut builder, self.shrink_prover.machine(), input);
 
         let operations = builder.into_operations();
         builder_span.exit();
@@ -1170,7 +1171,7 @@ pub mod tests {
 
     use crate::build::try_build_plonk_bn254_artifacts_dev;
     use anyhow::Result;
-    use build::try_build_groth16_bn254_artifacts_dev;
+    use build::{build_constraints_and_witness, try_build_groth16_bn254_artifacts_dev};
     use p3_field::PrimeField32;
 
     use sp1_recursion_core_v2::air::RecursionPublicValues;
@@ -1187,7 +1188,8 @@ pub mod tests {
         Compress,
         Shrink,
         Wrap,
-        Plonk,
+        CircuitTest,
+        All,
     }
 
     pub fn test_e2e_prover<C: SP1ProverComponents>(
@@ -1295,6 +1297,16 @@ pub mod tests {
         let vk_digest_bn254 = sp1_vkey_digest_bn254(&wrapped_bn254_proof);
         assert_eq!(vk_digest_bn254, vk.hash_bn254());
 
+        tracing::info!("Test the outer Plonk circuit");
+        let (constraints, witness) =
+            build_constraints_and_witness(&wrapped_bn254_proof.vk, &wrapped_bn254_proof.proof);
+        PlonkBn254Prover::test(constraints, witness);
+        tracing::info!("Circuit test succedded");
+
+        if test_kind == Test::CircuitTest {
+            return Ok(());
+        }
+
         tracing::info!("generate plonk bn254 proof");
         let artifacts_dir = try_build_plonk_bn254_artifacts_dev(
             &wrapped_bn254_proof.vk,
@@ -1417,29 +1429,6 @@ pub mod tests {
         println!("verify wrap bn254 {:#?}", wrapped_bn254_proof.vk.commit);
         prover.verify_wrap_bn254(&wrapped_bn254_proof, &verify_vk).unwrap();
 
-        // tracing::info!("checking vkey hash babybear");
-        // let vk_digest_babybear = wrapped_bn254_proof.sp1_vkey_digest_babybear();
-        // assert_eq!(vk_digest_babybear, verify_vk.hash_babybear());
-
-        // tracing::info!("checking vkey hash bn254");
-        // let vk_digest_bn254 = wrapped_bn254_proof.sp1_vkey_digest_bn254();
-        // assert_eq!(vk_digest_bn254, verify_vk.hash_bn254());
-
-        // tracing::info!("generate groth16 bn254 proof");
-        // let artifacts_dir = try_build_groth16_bn254_artifacts_dev(
-        //     &wrapped_bn254_proof.vk,
-        //     &wrapped_bn254_proof.proof,
-        // );
-        // let groth16_bn254_proof = prover.wrap_groth16_bn254(wrapped_bn254_proof, &artifacts_dir);
-        // println!("{:?}", groth16_bn254_proof);
-
-        // prover.verify_groth16_bn254(
-        //     &groth16_bn254_proof,
-        //     &verify_vk,
-        //     &public_values,
-        //     &artifacts_dir,
-        // )?;
-
         Ok(())
     }
 
@@ -1464,7 +1453,7 @@ pub mod tests {
             elf,
             SP1Stdin::default(),
             opts,
-            Test::Plonk,
+            Test::All,
         )
     }
 

crates/prover/src/utils.rs

@@ -5,15 +5,20 @@ use std::{
     iter::{Skip, Take},
 };
 
+use itertools::Itertools;
 use p3_baby_bear::BabyBear;
 use p3_bn254_fr::Bn254Fr;
 use p3_field::{AbstractField, PrimeField32};
+use p3_symmetric::CryptographicHasher;
 use sp1_core_executor::{Executor, Program};
 use sp1_core_machine::{io::SP1Stdin, reduce::SP1ReduceProof};
-use sp1_recursion_core_v2::{air::RecursionPublicValues, stark::config::BabyBearPoseidon2Outer};
-use sp1_stark::{SP1CoreOpts, Word};
+use sp1_recursion_core_v2::{
+    air::{RecursionPublicValues, NUM_PV_ELMS_TO_HASH},
+    stark::config::BabyBearPoseidon2Outer,
+};
+use sp1_stark::{baby_bear_poseidon2::MyHash as InnerHash, SP1CoreOpts, Word};
 
-use crate::SP1CoreProofData;
+use crate::{InnerSC, SP1CoreProofData};
 
 /// Get the SP1 vkey BabyBear Poseidon2 digest this reduce proof is representing.
 pub fn sp1_vkey_digest_babybear(proof: &SP1ReduceProof<BabyBearPoseidon2Outer>) -> [BabyBear; 8] {
@@ -27,6 +32,27 @@ pub fn sp1_vkey_digest_bn254(proof: &SP1ReduceProof<BabyBearPoseidon2Outer>) ->
     babybears_to_bn254(&sp1_vkey_digest_babybear(proof))
 }
 
+/// Compute the digest of the public values.
+pub fn recursion_public_values_digest(
+    config: &InnerSC,
+    public_values: &RecursionPublicValues<BabyBear>,
+) -> [BabyBear; 8] {
+    let hash = InnerHash::new(config.perm.clone());
+    let pv_array = public_values.as_array();
+    hash.hash_slice(&pv_array[0..NUM_PV_ELMS_TO_HASH])
+}
+
+/// Assert that the digest of the public values is correct.
+pub fn assert_recursion_public_values_valid(
+    config: &InnerSC,
+    public_values: &RecursionPublicValues<BabyBear>,
+) {
+    let expected_digest = recursion_public_values_digest(config, public_values);
+    for (value, expected) in public_values.digest.iter().copied().zip_eq(expected_digest) {
+        assert_eq!(value, expected);
+    }
+}
+
 /// Get the committed values Bn Poseidon2 digest this reduce proof is representing.
 pub fn sp1_commited_values_digest_bn254(proof: &SP1ReduceProof<BabyBearPoseidon2Outer>) -> Bn254Fr {
     let proof = &proof.proof;

crates/prover/src/verify.rs

@@ -20,8 +20,8 @@ use sp1_stark::{
 use thiserror::Error;
 
 use crate::{
-    components::SP1ProverComponents, CoreSC, HashableKey, OuterSC, SP1CoreProofData, SP1Prover,
-    SP1VerifyingKey,
+    components::SP1ProverComponents, utils::assert_recursion_public_values_valid, CoreSC,
+    HashableKey, OuterSC, SP1CoreProofData, SP1Prover, SP1VerifyingKey,
 };
 
 #[derive(Error, Debug)]
@@ -298,6 +298,10 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
 
         // Validate public values
         let public_values: &RecursionPublicValues<_> = proof.public_values.as_slice().borrow();
+        assert_recursion_public_values_valid(
+            self.compress_prover.machine().config(),
+            public_values,
+        );
 
         // `is_complete` should be 1. In the reduce program, this ensures that the proof is fully
         // reduced.
@@ -311,14 +315,6 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
             return Err(MachineVerificationError::InvalidPublicValues("sp1 vk hash mismatch"));
         }
 
-        // // Verify that the reduce program is the one we are expecting.
-        // let recursion_vkey_hash = self.compress_vk().hash_babybear();
-        // if public_values.compress_vk_digest != recursion_vkey_hash {
-        //     return Err(MachineVerificationError::InvalidPublicValues(
-        //         "recursion vk hash mismatch",
-        //     ));
-        // }
-
         Ok(())
     }
 
@@ -335,6 +331,10 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
         // Validate public values
         let public_values: &RecursionPublicValues<_> =
             proof.proof.public_values.as_slice().borrow();
+        // assert_recursion_public_values_valid(
+        //     self.compress_prover.machine().config(),
+        //     public_values,
+        // );
 
         // `is_complete` should be 1. In the reduce program, this ensures that the proof is fully
         // reduced.
@@ -364,6 +364,10 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
         // Validate public values
         let public_values: &RecursionPublicValues<_> =
             proof.proof.public_values.as_slice().borrow();
+        // assert_recursion_public_values_valid(
+        //     self.compress_prover.machine().config(),
+        //     public_values,
+        // );
 
         // `is_complete` should be 1. In the reduce program, this ensures that the proof is fully
         // reduced.

crates/recursion/circuit-v2/Cargo.toml

@@ -28,6 +28,7 @@ p3-baby-bear = { workspace = true }
 sp1-core-machine = { workspace = true }
 sp1-core-executor = { workspace = true }
 sp1-stark = { workspace = true }
+sp1-derive = { workspace = true }
 sp1-recursion-core-v2 = { workspace = true }
 sp1-recursion-derive = { workspace = true }
 sp1-recursion-compiler = { workspace = true }

crates/recursion/circuit-v2/src/challenger.rs

@@ -87,22 +87,6 @@ impl<C: Config> DuplexChallengerVariable<C> {
         }
     }
 
-    // /// Asserts that the state of this challenger is equal to the state of another challenger.
-    // fn assert_eq(&self, builder: &mut Builder<C>, other: &Self) {
-    //     zip(&self.sponge_state, &other.sponge_state)
-    //         .chain(zip(&self.input_buffer, &other.input_buffer))
-    //         .chain(zip(&self.output_buffer, &other.output_buffer))
-    //         .for_each(|(&element, &other_element)| {
-    //             builder.assert_felt_eq(element, other_element);
-    //         });
-    // }
-
-    // fn reset(&mut self, builder: &mut Builder<C>) {
-    //     self.sponge_state.fill(builder.eval(C::F::zero()));
-    //     self.input_buffer.clear();
-    //     self.output_buffer.clear();
-    // }
-
     fn observe(&mut self, builder: &mut Builder<C>, value: Felt<C::F>) {
         self.output_buffer.clear();
 
@@ -113,12 +97,6 @@ impl<C: Config> DuplexChallengerVariable<C> {
         }
     }
 
-    // fn observe_commitment(&mut self, builder: &mut Builder<C>, commitment: DigestVariable<C>) {
-    //     for element in commitment {
-    //         self.observe(builder, element);
-    //     }
-    // }
-
     fn sample(&mut self, builder: &mut Builder<C>) -> Felt<C::F> {
         if !self.input_buffer.is_empty() || self.output_buffer.is_empty() {
             self.duplexing(builder);

crates/recursion/circuit-v2/src/hash.rs

@@ -13,11 +13,13 @@ use sp1_recursion_compiler::{
 };
 use sp1_recursion_core_v2::stark::config::outer_perm;
 use sp1_recursion_core_v2::{stark::config::BabyBearPoseidon2Outer, DIGEST_SIZE};
+use sp1_recursion_core_v2::{HASH_RATE, PERMUTATION_WIDTH};
 use sp1_stark::baby_bear_poseidon2::BabyBearPoseidon2;
 use sp1_stark::inner_perm;
 
+use crate::challenger::SPONGE_SIZE;
 use crate::{
-    challenger::{reduce_32, RATE, SPONGE_SIZE},
+    challenger::{reduce_32, RATE},
     select_chain, CircuitConfig,
 };
 
@@ -27,6 +29,27 @@ pub trait FieldHasher<F: Field> {
     fn constant_compress(input: [Self::Digest; 2]) -> Self::Digest;
 }
 
+pub trait Posedion2BabyBearHasherVariable<C: CircuitConfig> {
+    fn poseidon2_permute(
+        builder: &mut Builder<C>,
+        state: [Felt<C::F>; PERMUTATION_WIDTH],
+    ) -> [Felt<C::F>; PERMUTATION_WIDTH];
+
+    /// Applies the Poseidon2 hash function to the given array.
+    ///
+    /// Reference: [p3_symmetric::PaddingFreeSponge]
+    fn poseidon2_hash(builder: &mut Builder<C>, input: &[Felt<C::F>]) -> [Felt<C::F>; DIGEST_SIZE] {
+        // static_assert(RATE < WIDTH)
+        let mut state = core::array::from_fn(|_| builder.eval(C::F::zero()));
+        for input_chunk in input.chunks(HASH_RATE) {
+            state[..input_chunk.len()].copy_from_slice(input_chunk);
+            state = Self::poseidon2_permute(builder, state);
+        }
+        let digest: [Felt<C::F>; DIGEST_SIZE] = state[..DIGEST_SIZE].try_into().unwrap();
+        digest
+    }
+}
+
 pub trait FieldHasherVariable<C: CircuitConfig>: FieldHasher<C::F> {
     type DigestVariable: Clone + Copy;
 
@@ -58,13 +81,33 @@ impl FieldHasher<BabyBear> for BabyBearPoseidon2 {
     }
 }
 
+impl<C: CircuitConfig> Posedion2BabyBearHasherVariable<C> for BabyBearPoseidon2 {
+    fn poseidon2_permute(
+        builder: &mut Builder<C>,
+        input: [Felt<<C>::F>; PERMUTATION_WIDTH],
+    ) -> [Felt<<C>::F>; PERMUTATION_WIDTH] {
+        builder.poseidon2_permute_v2(input)
+    }
+}
+
+impl<C: CircuitConfig> Posedion2BabyBearHasherVariable<C> for BabyBearPoseidon2Outer {
+    fn poseidon2_permute(
+        builder: &mut Builder<C>,
+        state: [Felt<<C>::F>; PERMUTATION_WIDTH],
+    ) -> [Felt<<C>::F>; PERMUTATION_WIDTH] {
+        let state: [Felt<_>; PERMUTATION_WIDTH] = state.map(|x| builder.eval(x));
+        builder.push_op(DslIr::CircuitPoseidon2PermuteBabyBear(Box::new(state)));
+        state
+    }
+}
+
 impl<C: CircuitConfig<F = BabyBear, Bit = Felt<BabyBear>>> FieldHasherVariable<C>
     for BabyBearPoseidon2
 {
     type DigestVariable = [Felt<BabyBear>; DIGEST_SIZE];
 
     fn hash(builder: &mut Builder<C>, input: &[Felt<<C as Config>::F>]) -> Self::DigestVariable {
-        builder.poseidon2_hash_v2(input)
+        <Self as Posedion2BabyBearHasherVariable<C>>::poseidon2_hash(builder, input)
     }
 
     fn compress(
@@ -181,7 +224,3 @@ impl<C: CircuitConfig<F = BabyBear, N = Bn254Fr, Bit = Var<Bn254Fr>>> FieldHashe
         }
     }
 }
-
-// impl<C: Config<F = BabyBear>> FieldHasherVariable<C> for OuterHash {
-
-// }