doc: recursive program docs (#855)

recursion/program/src/commit.rs

@@ -3,6 +3,7 @@ use sp1_recursion_compiler::ir::{Array, Builder, Config, Ext, FromConstant, Usiz
 
 use crate::fri::types::{FriConfigVariable, TwoAdicPcsRoundVariable};
 
+/// Reference: [p3_commit::PolynomialSpace]
 pub trait PolynomialSpaceVariable<C: Config>: Sized + FromConstant<C> {
     type Constant: PolynomialSpace<Val = C::F>;
 
@@ -33,6 +34,7 @@ pub trait PolynomialSpaceVariable<C: Config>: Sized + FromConstant<C> {
     ) -> Self;
 }
 
+/// Reference: [p3_commit::Pcs]
 pub trait PcsVariable<C: Config, Challenger> {
     type Domain: PolynomialSpaceVariable<C>;
 

recursion/program/src/machine/compress.rs

@@ -96,6 +96,8 @@ where
             deferred_vk,
         );
 
+        builder.halt();
+
         builder.compile_program()
     }
 }
@@ -472,7 +474,5 @@ where
         );
 
         commit_public_values(builder, reduce_public_values);
-
-        builder.halt();
     }
 }

recursion/program/src/machine/core.rs

@@ -71,6 +71,8 @@ impl SP1RecursiveVerifier<InnerConfig, BabyBearPoseidon2> {
         };
         SP1RecursiveVerifier::verify(&mut builder, &pcs, machine, input);
 
+        builder.halt();
+
         builder.compile_program()
     }
 }
@@ -90,13 +92,39 @@ where
     /// This program represents a first recursive step in the verification of an SP1 proof
     /// consisting of one or more shards. Each shard proof is verified and its public values are
     /// aggregated into a single set representing the start and end state of the program execution
-    /// across all shards.  
+    /// across all shards.
+    ///
+    /// # Constraints
+    ///
+    /// ## Verifying the STARK proofs.
+    /// For each shard, the verifier asserts the correctness of the STARK proof which is composed
+    /// of verifying the FRI proof for openings and verifying the constraints.
+    ///
+    /// ## Aggregating the shard public values.
+    ///
+    /// See [SP1Prover::verify] for the verification algorithm of a complete SP1 proof. In this
+    /// function, we are aggregating several shard proofs and attesting to an aggregated state which
+    /// reprersents all the shards. The consistency conditions of the aggregated state are
+    /// asserted in the following way:
+    ///
+    /// - Start pc for every shardf should be what the next pc declared in the previous shard was.
+    /// - Public input, deferred proof digests, and exit code should be the same in all shards.
+    ///
+    /// ## The leaf challenger.
+    /// A key difference between the recursive tree verification and the complete one in
+    /// [SP1Prover::verify] is that the recursive verifier has no way of reconstructiing the
+    /// chanllenger only from a part of the shard proof. Therefoee, the value of the leaf challenger
+    /// is witnessed in the program and the verifier assertds correctness given this challenger.
+    /// In the course of the recursive verification, the challenger is reconstructed by observing
+    /// the commitments one by one, and in the final step, the challenger is asserted to be the same
+    /// as the one witnessed here.
     pub fn verify(
         builder: &mut Builder<C>,
         pcs: &TwoAdicFriPcsVariable<C>,
         machine: &StarkMachine<SC, RiscvAir<SC::Val>>,
         input: SP1RecursionMemoryLayoutVariable<C>,
     ) {
+        // Read input.
         let SP1RecursionMemoryLayoutVariable {
             vk,
             shard_proofs,
@@ -212,6 +240,8 @@ where
             });
 
             // Assert compatibility of the shard values.
+
+            // Assert that the committed value digests are all the same.
             for (word, current_word) in committed_value_digest
                 .iter()
                 .zip_eq(public_values.committed_value_digest.iter())
@@ -243,16 +273,19 @@ where
                 builder.assert_felt_eq(*digest, *current_digest);
             }
 
-            // Update the reconstruct challenger, cumulative sum, shard number, and program counter.
+            // Update the loop variables: the reconstruct challenger, cumulative sum, shard number,
+            // and program counter.
+
+            // Increment the shard index by one.
+            builder.assign(current_shard, current_shard + C::F::one());
+
+            // Update the reconstruct challenger.
             reconstruct_challenger.observe(builder, proof.commitment.main_commit);
             for j in 0..machine.num_pv_elts() {
                 let element = builder.get(&proof.public_values, j);
                 reconstruct_challenger.observe(builder, element);
             }
 
-            // Increment the shard count by one.
-            builder.assign(current_shard, current_shard + C::F::one());
-
             // Update current_pc to be the end_pc of the current proof.
             builder.assign(current_pc, public_values.next_pc);
 
@@ -267,6 +300,8 @@ where
                 });
         });
 
+        // Write all values to the public values struct and commit to them.
+
         // Compute vk digest.
         let vk_digest = hash_vkey(builder, &vk);
         let vk_digest: [Felt<_>; DIGEST_SIZE] = array::from_fn(|i| builder.get(&vk_digest, i));
@@ -281,6 +316,7 @@ where
         let cumulative_sum_arrray = array::from_fn(|i| builder.get(&cumulative_sum_arrray, i));
 
         let zero: Felt<_> = builder.eval(C::F::zero());
+
         // Initialize the public values we will commit to.
         let mut recursion_public_values_stream = [zero; RECURSIVE_PROOF_NUM_PV_ELTS];
 
@@ -317,7 +353,5 @@ where
         });
 
         commit_public_values(builder, recursion_public_values);
-
-        builder.halt();
     }
 }

recursion/program/src/machine/deferred.rs

@@ -91,6 +91,8 @@ where
 
         SP1DeferredVerifier::verify(&mut builder, &pcs, machine, input);
 
+        builder.halt();
+
         builder.compile_program()
     }
 }
@@ -114,7 +116,7 @@ where
     /// - Asserts that each of these proofs is valid as a `compress` proof.
     /// - Asserts that each of these proofs is complete by checking the `is_complete` flag in the
     ///  proof's public values.
-    /// - Aggregates the proof information into an accumulated deferred digest.
+    /// - Aggregates the proof information into the accumulated deferred digest.
     pub fn verify(
         builder: &mut Builder<C>,
         pcs: &TwoAdicFriPcsVariable<C>,
@@ -289,7 +291,5 @@ where
         deferred_public_values.is_complete = var2felt(builder, is_complete);
 
         commit_public_values(builder, deferred_public_values);
-
-        builder.halt();
     }
 }

recursion/program/src/machine/utils.rs

@@ -22,6 +22,8 @@ use crate::{
 };
 
 /// Assertions on the public values describing a complete recursive proof state.
+///
+/// See [SP1Prover::verify] for the verification algorithm of a complete SP1 proof.
 pub(crate) fn assert_complete<C: Config>(
     builder: &mut Builder<C>,
     public_values: &RecursionPublicValues<Felt<C::F>>,