feat: integration constraints (#1455)

crates/core/machine/src/riscv/mod.rs

@@ -15,6 +15,9 @@ use sp1_stark::{
 use strum_macros::{EnumDiscriminants, EnumIter};
 use tracing::instrument;
 
+pub const MAX_LOG_NUMBER_OF_SHARDS: usize = 16;
+pub const MAX_NUMBER_OF_SHARDS: usize = 1 << MAX_LOG_NUMBER_OF_SHARDS;
+
 /// A module for importing all the different RISC-V chips.
 pub(crate) mod riscv_chips {
     pub use crate::{

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::{SP1CompressVerifier, SP1CompressWitnessValues};
+use sp1_recursion_circuit_v2::machine::{SP1CompressRootVerifier, SP1CompressWitnessValues};
 use sp1_recursion_compiler::{
     config::OuterConfig,
     constraints::{Constraint, ConstraintCompiler},
@@ -175,7 +175,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);
-    SP1CompressVerifier::verify(&mut builder, &wrap_machine, input);
+    SP1CompressRootVerifier::verify(&mut builder, &wrap_machine, input);
 
     let mut backend = ConstraintCompiler::<OuterConfig>::default();
     let operations = backend.emit(builder.into_operations());

crates/prover/src/lib.rs

@@ -72,10 +72,10 @@ use sp1_recursion_core_v2::{
 use sp1_recursion_circuit_v2::{
     hash::FieldHasher,
     machine::{
-        SP1CompressShape, SP1CompressVerifier, SP1CompressWithVKeyVerifier,
-        SP1CompressWithVKeyWitnessValues, SP1CompressWitnessValues, SP1DeferredVerifier,
-        SP1DeferredWitnessValues, SP1MerkleProofWitnessValues, SP1RecursionShape,
-        SP1RecursionWitnessValues, SP1RecursiveVerifier,
+        SP1CompressRootVerifier, SP1CompressRootVerifierWithVKey, SP1CompressShape,
+        SP1CompressWithVKeyVerifier, SP1CompressWithVKeyWitnessValues, SP1CompressWitnessValues,
+        SP1DeferredVerifier, SP1DeferredWitnessValues, SP1MerkleProofWitnessValues,
+        SP1RecursionShape, SP1RecursionWitnessValues, SP1RecursiveVerifier,
     },
     merkle_tree::MerkleTree,
     witness::Witnessable,
@@ -326,7 +326,24 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
         &self,
         input: &SP1CompressWithVKeyWitnessValues<InnerSC>,
     ) -> Arc<RecursionProgram<BabyBear>> {
-        self.compress_program(input)
+        // Get the operations.
+        let builder_span = tracing::debug_span!("build shrink program").entered();
+        let mut builder = Builder::<InnerConfig>::default();
+        let input = input.read(&mut builder);
+        SP1CompressRootVerifierWithVKey::verify(
+            &mut builder,
+            self.compress_prover.machine(),
+            input,
+        );
+        let operations = builder.into_operations();
+        builder_span.exit();
+
+        // Compile the program.
+        let compiler_span = tracing::debug_span!("compile shrink program").entered();
+        let mut compiler = AsmCompiler::<InnerConfig>::default();
+        let program = Arc::new(compiler.compile(operations));
+        compiler_span.exit();
+        program
     }
 
     pub fn wrap_program(
@@ -336,8 +353,11 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
         // Get the operations.
         let builder_span = tracing::debug_span!("build compress program").entered();
         let mut builder = Builder::<InnerConfig>::default();
+
         let input = input.read(&mut builder);
-        SP1CompressVerifier::verify(&mut builder, self.shrink_prover.machine(), input);
+        // Verify the proof.
+        SP1CompressRootVerifier::verify(&mut builder, self.shrink_prover.machine(), input);
+
         let operations = builder.into_operations();
         builder_span.exit();
 
@@ -388,7 +408,7 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
         vk.observe_into(&mut reconstruct_challenger);
 
         // Prepare the inputs for the recursion programs.
-        for batch in shard_proofs.chunks(batch_size) {
+        for (batch_idx, batch) in shard_proofs.chunks(batch_size).enumerate() {
             let proofs = batch.to_vec();
 
             core_inputs.push(SP1RecursionWitnessValues {
@@ -397,6 +417,7 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
                 leaf_challenger: leaf_challenger.clone(),
                 initial_reconstruct_challenger: reconstruct_challenger.clone(),
                 is_complete,
+                is_first_shard: batch_idx == 0,
             });
             assert_eq!(reconstruct_challenger.input_buffer.len(), 0);
             assert_eq!(reconstruct_challenger.sponge_state.len(), 16);

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

@@ -117,6 +117,10 @@ pub trait CircuitConfig: Config {
 
     fn read_ext(builder: &mut Builder<Self>) -> Ext<Self::F, Self::EF>;
 
+    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit);
+
+    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit);
+
     fn ext2felt(
         builder: &mut Builder<Self>,
         ext: Ext<<Self as Config>::F, <Self as Config>::EF>,
@@ -162,11 +166,26 @@ pub trait CircuitConfig: Config {
         first: impl IntoIterator<Item = Ext<<Self as Config>::F, <Self as Config>::EF>> + Clone,
         second: impl IntoIterator<Item = Ext<<Self as Config>::F, <Self as Config>::EF>> + Clone,
     ) -> Vec<Ext<<Self as Config>::F, <Self as Config>::EF>>;
+
+    fn range_check_felt(builder: &mut Builder<Self>, value: Felt<Self::F>, num_bits: usize) {
+        let bits = Self::num2bits(builder, value, 32);
+        for bit in bits.into_iter().skip(num_bits) {
+            Self::assert_bit_zero(builder, bit);
+        }
+    }
 }
 
 impl CircuitConfig for InnerConfig {
     type Bit = Felt<<Self as Config>::F>;
 
+    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit) {
+        builder.assert_felt_eq(bit, Self::F::zero());
+    }
+
+    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit) {
+        builder.assert_felt_eq(bit, Self::F::one());
+    }
+
     fn read_bit(builder: &mut Builder<Self>) -> Self::Bit {
         builder.hint_felt_v2()
     }
@@ -257,6 +276,14 @@ impl CircuitConfig for InnerConfig {
 impl CircuitConfig for OuterConfig {
     type Bit = Var<<Self as Config>::N>;
 
+    fn assert_bit_zero(builder: &mut Builder<Self>, bit: Self::Bit) {
+        builder.assert_var_eq(bit, Self::N::zero());
+    }
+
+    fn assert_bit_one(builder: &mut Builder<Self>, bit: Self::Bit) {
+        builder.assert_var_eq(bit, Self::N::one());
+    }
+
     fn read_bit(builder: &mut Builder<Self>) -> Self::Bit {
         builder.witness_var()
     }

crates/recursion/circuit-v2/src/machine/complete.rs

@@ -0,0 +1,72 @@
+use itertools::Itertools;
+use p3_field::AbstractField;
+
+use sp1_recursion_compiler::ir::{Builder, Config, Felt};
+use sp1_recursion_core_v2::air::RecursionPublicValues;
+
+/// Assertions on recursion public values which represent a complete proof.
+///
+/// The assertions consist of checking all the expected boundary conditions from a compress proof
+/// that represents the end of the recursion tower.
+pub(crate) fn assert_complete<C: Config>(
+    builder: &mut Builder<C>,
+    public_values: &RecursionPublicValues<Felt<C::F>>,
+    is_complete: Felt<C::F>,
+) {
+    let RecursionPublicValues {
+        deferred_proofs_digest,
+        next_pc,
+        start_shard,
+        next_shard,
+        start_execution_shard,
+        cumulative_sum,
+        start_reconstruct_deferred_digest,
+        end_reconstruct_deferred_digest,
+        leaf_challenger,
+        end_reconstruct_challenger,
+        ..
+    } = public_values;
+
+    // Assert that the `is_complete` flag is boolean.
+    builder.assert_felt_eq(is_complete * (is_complete - C::F::one()), C::F::zero());
+
+    // Assert that `next_pc` is equal to zero (so program execution has completed)
+    builder.assert_felt_eq(is_complete * *next_pc, C::F::zero());
+
+    // Assert that start shard is equal to 1.
+    builder.assert_felt_eq(is_complete * (*start_shard - C::F::one()), C::F::zero());
+
+    // Assert that the next shard is not equal to one. This guarantees that there is at least one
+    // shard that contains CPU.
+    //
+    // TODO: figure out if this is needed.
+    builder.assert_felt_ne(is_complete * *next_shard, C::F::one());
+
+    // Assert that the start execution shard is equal to 1.
+    builder.assert_felt_eq(is_complete * (*start_execution_shard - C::F::one()), C::F::zero());
+
+    // Assert that the end reconstruct challenger is equal to the leaf challenger.
+    for (end_challenger_d, leaf_challenger_d) in
+        end_reconstruct_challenger.into_iter().zip(*leaf_challenger)
+    {
+        builder.assert_felt_eq(is_complete * (end_challenger_d - leaf_challenger_d), C::F::zero());
+    }
+
+    // The start reconstruct deffered digest should be zero.
+    for start_digest_word in start_reconstruct_deferred_digest {
+        builder.assert_felt_eq(is_complete * *start_digest_word, C::F::zero());
+    }
+
+    // The end reconstruct deffered digest should be equal to the deferred proofs digest.
+    for (end_digest_word, deferred_digest_word) in
+        end_reconstruct_deferred_digest.iter().zip_eq(deferred_proofs_digest.iter())
+    {
+        builder
+            .assert_felt_eq(is_complete * (*end_digest_word - *deferred_digest_word), C::F::zero());
+    }
+
+    // Assert that the cumulative sum is zero.
+    for b in cumulative_sum.iter() {
+        builder.assert_felt_eq(is_complete * *b, C::F::zero());
+    }
+}