Skip to content

Commit

Permalink
early detection for constrain failure in recursion circuit
Browse files Browse the repository at this point in the history
Signed-off-by: noelwei <[email protected]>
  • Loading branch information
noel2004 committed Jul 18, 2024
1 parent 2a99204 commit 3fe82be
Showing 1 changed file with 14 additions and 2 deletions.
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

0 comments on commit 3fe82be

Please sign in to comment.