fix constraints and counter, fix toolchain

Author: drcapybara

Cargo.lock

@@ -21,6 +21,7 @@ structopt = { version = "0.3.26", default-features = false }
 env_logger = "0.11.5"
 thiserror = "1.0.63"
 criterion = "0.3"
+hashbrown = "0.14"
 
 [dev-dependencies]
 debug_print = { version = "1.0.0" }

Cargo.toml

@@ -9,7 +9,7 @@ You can download the repo and run the main branch with:
 cargo test
 ```
 
-Which is run in release mode by default. This repo requires the nightly toolchain. If you are seeing errors related to:
+Which is run in release mode by default. This repo requires the nightly Rust toolchain. If you are seeing errors related to:
 
 ```bash
 6 | #![feature(specialization)]
@@ -26,7 +26,7 @@ error[E0554]: `#![feature]` may not be used on the stable release channel
   |                                             ^^^^^^^^^^^^^^^^^^
 ```
 
-Then please double check your toolchain. Otherwise, this repo should work out of the box.
+Then please double check your toolchain. You may need to run `rustup update nightly` and ensure the `rustc` component is installed. Otherwise, this repo should work out of the box.
 
 You can also run:
 
@@ -83,9 +83,9 @@ Our approach is to insert the following gates into the circuit with the requisit
                                                     │                      │
                                                     ▼                      │
                                           +-----------------------------+  │
-                                          | 6. process_recursive_layer  |──┘
+                                          | 6. evaluate_recursive_circuit|──┘
                                           |  Handle recursion, verify,  |
-                                          |  and loop through steps.    |
+                                          |  and loop through steps.     |
                                           +-----------------------------+
                                                     │
                                                     ▼
@@ -100,22 +100,22 @@ You can also view a rough sketch of a circuit diagram of the entire setup:
 
 
 ### Initial Setup
-- **Counter Initialization**: A counter gate is initialized to track the depth of recursion.
-- **Hash Initialization**: A virtual hash target gate is inserted and registered as a public input, marking the starting point of the hash chain.
-- **Hash Gate**: An updateable hash gate is added to enable hash updates as the recursion progresses.
+- **Counter Initialization**: A counter gate is initialized to track the depth of recursion. The counter starts at 1 after the base case performs the first hash iteration.
+- **Hash Initialization**: A virtual hash target gate is inserted and registered as a public input, marking the starting point of the hash chain. The initial hash is set to the zero hash `[F::ZERO; 4]` (all zeros).
+- **Hash Gate**: An updateable hash gate is added to enable hash updates as the recursion progresses. The circuit computes `current_hash_out = hash(current_hash_in)`, where `current_hash_in` is either the initial hash (base case) or the previous proof's output hash (recursive case).
 
 ### Recursive Hashing
-- **Verifier Data Setup**: Circuit common data is prepared, including configuration and partial witnesses required for recursion.
-- **Base Case Identification**: A condition is set to identify whether the current computation is the base case or a recursive case.
-- **Hash Chain Connection**: The current hash is connected to the previous hash output or set as the initial hash based on whether it's a base or recursive step.
+- **Verifier Data Setup**: Circuit common data is prepared, including configuration and partial witnesses required for recursion. This sets up the recursive proof structure using plonky2's cyclic recursion capabilities.
+- **Base Case Identification**: A condition flag is set to identify whether the current computation is the base case (`condition=false`) or a recursive case (`condition=true`). In the base case, the hash chain starts with the zero hash. In recursive cases, each proof verifies the previous proof and extends the chain.
+- **Hash Chain Connection**: The current hash input is connected to either the previous proof's output hash (when `condition=true`) or the initial hash (when `condition=false`). The circuit ensures proper chaining by verifying the inner cyclic proof and computing the next hash in the sequence.
 
 ### Recursive Proof Verification
-- **Circuit Building**: The circuit for the current step is built.
-- **Proof Generation**: A proof of the correctness of the current hash computation is generated using the circuit data.
-- **Proof Verification**: The generated proof is verified to ensure that the hash was computed correctly.
+- **Circuit Building**: The circuit for the current step is built with all necessary gates and constraints. The circuit structure remains constant regardless of the number of steps, enabling constant-size proofs.
+- **Proof Generation**: A proof of the correctness of the current hash computation is generated using the circuit data. Each recursive step produces a new proof that verifies the previous proof and extends the hash chain by one iteration.
+- **Proof Verification**: The generated proof is verified to ensure that the hash was computed correctly. The verification process checks both the proof's validity and that the hash chain was computed correctly by comparing against the expected hash value.
 
 ### Final Verification
-- **Final Hash Check**: After all recursive steps, the final hash is compared against the expected result to confirm the integrity of the entire hash chain.
+- **Final Hash Check**: After all recursive steps, the final hash is compared against the expected result to confirm the integrity of the entire hash chain. The `verify` function checks that `current_hash == hash^counter(initial_hash)` by iteratively hashing the initial hash `counter` times and comparing the result. This provides an additional validation beyond the proof verification itself.
 
 ## Usage:
 
@@ -148,29 +148,41 @@ let (proof, circuit_data) =
 
 // Verify
 let verification_result =
-    <CircuitBuilder<GoldilocksField, D> as HashChain<GoldilocksField, D, C>>::verify(proof, circuit_data);
+    <CircuitBuilder<GoldilocksField, D> as HashChain<GoldilocksField, D, C>>::verify(proof, &circuit_data);
 assert!(verification_result.is_ok());
 ```
 
 We observe a total uncompressed proof size of 133440 bytes, regardless of number of steps in the chain. We find this is very nice because this number stays the same no matter how many hashes we compute. In theory, recursively verifiable proofs of this nature can compress extremely large computations into a very small space. Think fully-succinct blockchains, in which light clients can verify the entire state of the chain trustlessly by verifying a small and simple proof in trivial amounts of time.
 
+### Public Inputs Structure
+
+The proof's public inputs follow this structure:
+- `[0..4]`: Initial hash (4 field elements) - remains constant throughout the chain, set to `[F::ZERO; 4]`
+- `[4..8]`: Current hash (4 field elements) - the hash after `counter` iterations
+- `[8]`: Counter (1 field element) - the number of hash iterations performed (starts at 1, increments by 1 each recursive step)
+- `[9..]`: Verifier data (variable length) - plonky2's verifier circuit data
+
+The verification function validates that `current_hash == hash^counter(initial_hash)`, ensuring the hash chain was computed correctly.
+
 ## Benches
 
 This crate uses criterion for formal benchmarks. Bench prover and verifier performance with:
 
 ```bash
 cargo bench
 ```
-Here are some prelimnary performance metrics observed thus far:
-
-| Circuit depth (steps) | Prover Runtime (s) | Verifier Runtime (ms)| System RAM Used (mb)|
-|-----------------------|--------------------|----------------------|---------------------|
-| 2                     | 3.3680 s           | 3.1013 ms            | 375.692             |
-| 4                     | 4.2126 s           | 3.1220 ms            | 381.536             |
-| 8                     | 5.7366 s           | 3.0812 ms            | 392.716             |
-| 16                    | 8.8146 s           | 3.1098 ms            | 405.516             |
-| 32                    | 14.957 s           | 3.0865 ms            | 417.704             |
-| 64                    | 27.294 s           | 3.1625 ms            | 436.424             |
+Here are some preliminary performance metrics observed on Apple M4 Pro (Darwin):
+
+| Circuit depth (steps) | Prover Runtime (s) | Verifier Runtime (ms)|
+|-----------------------|--------------------|----------------------|
+| 2                     | 2.629 s            | 2.474 ms             |
+| 4                     | 3.163 s            | 2.454 ms             |
+| 8                     | 4.196 s            | 2.491 ms             |
+| 16                    | 6.474 s            | 2.498 ms             |
+| 32                    | 10.77 s            | 2.496 ms             |
+| 64                    | 18.78 s            | 2.518 ms             |
+
+**Key Observation**: Verifier runtime remains constant (~2.5ms) regardless of chain length, demonstrating the succinctness property of recursive proofs. Prover time scales roughly linearly with the number of steps.
 
 
 ## Acknowledgments

README.md

@@ -83,6 +83,9 @@ pub trait HashChain<F: RichField + Extendable<D>, const D: usize, C: GenericConf
         proof: Proof<F, C, D>,
         verifier_data_target: VerifierCircuitTarget,
         cyclic_circuit_data: &CircuitMap<F, C, D>,
+        initial_hash_target: HashOutTarget,
+        current_hash_out: HashOutTarget,
+        counter: Target,
     ) -> Result<Proof<F, C, D>, HashChainError>;
 
     fn configure_layers() -> CommonData<F, D>;
@@ -93,6 +96,9 @@ pub trait HashChain<F: RichField + Extendable<D>, const D: usize, C: GenericConf
         common_data: CommonData<F, D>,
         cyclic_circuit_data: CircuitMap<F, C, D>,
         verifier_data_target: VerifierCircuitTarget,
+        initial_hash_target: HashOutTarget,
+        current_hash_out: HashOutTarget,
+        counter: Target,
         steps: usize,
     ) -> ProofAndCircuitResult<F, C, D>;
 }
@@ -143,7 +149,8 @@ where
     /// ```
     ///
     /// Following this approach, we can build a properly constrained recursive hash chain
-    /// circuit. (At least thats the plan!)
+    /// circuit. The implementation uses plonky2's cyclic recursion to create a constant-size
+    /// proof that verifies an arbitrary number of hash iterations.
     ///
     /// ## Usage
     /// ```
@@ -262,13 +269,22 @@ where
             common_data,
             cyclic_circuit_data,
             verifier_data_target,
+            initial_hash_target,
+            current_hash_out,
+            counter,
             steps,
         )
     }
 
     // Setup the recursive hashes structure by establishing the size of the inputs and outputs
     // and connecting them to each other appropriately. Additionally setup the conditional proof
     // verification depending on whether we are in the base layer or not.
+    //
+    // The circuit connects:
+    // - initial_hash_target to inner_cyclic_initial_hash (ensures initial hash stays constant)
+    // - current_hash_in to either inner_cyclic_latest_hash (if condition=true) or initial_hash_target (if condition=false)
+    // - counter to condition * inner_cyclic_counter + 1 (increments counter when condition=true)
+    // This ensures proper hash chaining: each recursive step uses the previous proof's output hash as input.
     fn setup_recursive_layers(
         &self,
         builder: &mut CircuitBuilder<F, D>,
@@ -338,11 +354,38 @@ where
         proof: ProofWithPublicInputs<F, C, D>,
         verifier_circuit_target: VerifierCircuitTarget,
         cyclic_circuit_data: &CircuitData<F, C, D>,
+        initial_hash_target: HashOutTarget,
+        _current_hash_out: HashOutTarget,
+        counter: Target,
     ) -> Result<ProofWithPublicInputs<F, C, D>, HashChainError> {
         let mut pw = PartialWitness::new();
         pw.set_bool_target(condition, true);
         pw.set_proof_with_pis_target(&inner_cyclic_proof_with_pub_inputs, &proof);
         pw.set_verifier_data_target(&verifier_circuit_target, &cyclic_circuit_data.verifier_only);
+
+        // Set the public inputs from the previous proof to ensure proper chaining
+        // Public inputs structure: [initial_hash (4), current_hash (4), counter (1), ...verifier_data...]
+        // Note: The circuit connects these via setup_recursive_layers, but we need to set
+        // the initial values to match the previous proof's outputs
+        let prev_initial_hash = &proof.public_inputs[0..4];
+        let prev_counter = proof.public_inputs[8];
+
+        // Set initial hash (should remain constant across all iterations)
+        for (i, &element) in prev_initial_hash.iter().enumerate() {
+            pw.set_target(initial_hash_target.elements[i], element);
+        }
+
+        // Set counter to match what the circuit will compute
+        // The circuit computes: counter = condition * inner_counter + 1
+        // Since condition=true, this becomes: counter = inner_counter + 1
+        // We need to set it to prev_counter + 1 to match the circuit's computation
+        let one = F::ONE;
+        pw.set_target(counter, prev_counter + one);
+
+        // Note: current_hash_out is computed by the circuit from current_hash_in,
+        // which is connected to inner_cyclic_latest_hash from the previous proof.
+        // We don't need to set it explicitly - the circuit handles the chaining.
+
         let proof = cyclic_circuit_data.prove(pw)?;
         check_cyclic_proof_verifier_data(
             &proof,
@@ -362,24 +405,50 @@ where
         common_data: CommonCircuitData<F, D>,
         cyclic_circuit_data: CircuitData<F, C, D>,
         verifier_data_target: VerifierCircuitTarget,
+        initial_hash_target: HashOutTarget,
+        current_hash_out: HashOutTarget,
+        counter: Target,
         steps: usize,
     ) -> Result<(ProofWithPublicInputs<F, C, D>, CircuitData<F, C, D>), HashChainError> {
         // Setup the partial witness for the proof, and set the
-        // initial public input wires with an array of field elements set to
-        // the empty hash
+        // initial public input wires with actual hash values
+        // Use zero hash as the starting point (all zeros)
         let mut pw = PartialWitness::new();
-        let initial_hash = [];
-        let initial_hash_pub_inputs = initial_hash.into_iter().enumerate().collect();
+        let initial_hash: [F; 4] = [F::ZERO; 4];
+
+        // Set the initial hash in the witness (starting point of the chain)
+        for (i, &element) in initial_hash.iter().enumerate() {
+            pw.set_target(initial_hash_target.elements[i], element);
+        }
+
+        // Compute the first hash (base case: hash the initial hash once)
+        let first_hash = hash_n_to_hash_no_pad::<F, PoseidonPermutation<F>>(&initial_hash);
+
+        // Set counter to 1 (we've done one hash iteration)
+        // Note: current_hash_out will be computed by the circuit from current_hash_in
+        // In the base case (condition=false), current_hash_in = initial_hash_target
+        // So current_hash_out = hash(initial_hash) = first_hash
+        let one = F::ONE;
+        pw.set_target(counter, one);
 
         // Set the condition wire to false because we are not in the recursive case
         // initially
         pw.set_bool_target(condition, false);
+
+        // Create base proof with proper public inputs: [initial_hash (4), current_hash (4), counter (1)]
+        let mut base_pub_inputs = Vec::new();
+        base_pub_inputs.extend_from_slice(&initial_hash);
+        base_pub_inputs.extend_from_slice(&first_hash.elements);
+        base_pub_inputs.push(one);
+        let base_pub_inputs_map: hashbrown::HashMap<usize, F> =
+            base_pub_inputs.into_iter().enumerate().collect();
+
         pw.set_proof_with_pis_target::<C, D>(
             &inner_cyclic_proof_with_pub_inputs,
             &cyclic_base_proof(
                 &common_data,
                 &cyclic_circuit_data.verifier_only,
-                initial_hash_pub_inputs,
+                base_pub_inputs_map,
             ),
         );
 
@@ -392,32 +461,38 @@ where
 
         // Setup the expected data for the verifier
         pw.set_verifier_data_target(&verifier_data_target, &cyclic_circuit_data.verifier_only);
-        let proof = cyclic_circuit_data.prove(pw)?;
+        let mut proof = cyclic_circuit_data.prove(pw)?;
         check_cyclic_proof_verifier_data(
             &proof,
             &cyclic_circuit_data.verifier_only,
             &cyclic_circuit_data.common,
         )?;
         cyclic_circuit_data.verify(proof.clone())?;
 
-        // Base case of the recursion
-        let mut proof = Self::prove_current_layer(
+        // Base case of the recursion - now prove with condition=true to start recursive chaining
+        proof = Self::prove_current_layer(
             condition,
             inner_cyclic_proof_with_pub_inputs.clone(),
             proof,
             verifier_data_target.clone(),
             &cyclic_circuit_data,
+            initial_hash_target,
+            current_hash_out,
+            counter,
         )?;
         cyclic_circuit_data.verify(proof.clone())?;
 
-        // Subsequent recursive steps
+        // Subsequent recursive steps - each step chains the previous hash
         for _ in 0..steps {
             proof = Self::prove_current_layer(
                 condition,
                 inner_cyclic_proof_with_pub_inputs.clone(),
                 proof,
                 verifier_data_target.clone(),
                 &cyclic_circuit_data,
+                initial_hash_target,
+                current_hash_out,
+                counter,
             )?;
         }
 
@@ -491,7 +566,7 @@ mod tests {
             GoldilocksField,
             D,
             C,
-        >>::build_hash_chain_circuit(&mut circuit, 2)
+        >>::build_hash_chain_circuit(&mut circuit, 128)
         .unwrap();
 
         let result =