Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions aggregator/src/recursion/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -410,11 +410,13 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
// Verify initial_state is same as the first application snark in the
// first round of recursion.
(
"initial state equal to app's initial (first round)",
main_gate.mul(&mut ctx, Existing(st), Existing(first_round)),
main_gate.mul(&mut ctx, Existing(app_inst), Existing(first_round)),
),
// Propagate initial_state for subsequent rounds of recursion.
(
"initial state equal to prev_recursion's initial (not first round)",
main_gate.mul(&mut ctx, Existing(st), Existing(not_first_round)),
previous_st,
),
Expand All @@ -436,7 +438,7 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
.map(|i| &app_instances[i]),
),
)
.map(|(&st, &app_inst)| (st, app_inst))
.map(|(&st, &app_inst)| ("passing cur state to app", st, app_inst))
.collect::<Vec<_>>();

// Verify that the "previous state" (additional state not included) is the same
Expand All @@ -451,6 +453,7 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
)
.map(|(&st, &app_inst)| {
(
"chain prev state with cur init state (not first round)",
main_gate.mul(&mut ctx, Existing(app_inst), Existing(not_first_round)),
st,
)
Expand All @@ -459,9 +462,10 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {

// Finally apply the equality constraints between the (LHS, RHS) values constructed
// above.
for (lhs, rhs) in [
for (comment, lhs, rhs) in [
// Propagate the preprocessed digest.
(
"chain preprocessed digest",
main_gate.mul(
&mut ctx,
Existing(preprocessed_digest),
Expand All @@ -471,6 +475,7 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
),
// Verify that "round" increments by 1 when not the first round of recursion.
(
"round increment",
round,
main_gate.add(
&mut ctx,
Expand All @@ -484,6 +489,13 @@ impl<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
.chain(verify_app_state)
.chain(verify_app_init_state)
{
use halo2_proofs::dev::unwrap_value;
debug_assert_eq!(
unwrap_value(lhs.value()),
unwrap_value(rhs.value()),
"equality constraint fail: {}",
comment
);
ctx.region.constrain_equal(lhs.cell(), rhs.cell())?;
}

Expand Down