Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.

Commit 191b61f

Browse files
roynalnarutoroynalnaruto
authored
feat: bool advice column for improved soundness (#1288)
1 parent 452fab5 commit 191b61f

File tree

9 files changed

+533
-463
lines changed

9 files changed

+533
-463
lines changed

‎aggregator/src/aggregation.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ mod config;
1212
mod decoder;
1313
/// config for RLC circuit
1414
mod rlc;
15+
/// Utility module
16+
mod util;
1517

1618
pub(crate) use barycentric::{
1719
interpolate, AssignedBarycentricEvaluationConfig, BarycentricEvaluationConfig, BLS_MODULUS,

‎aggregator/src/aggregation/decoder.rs‎

Lines changed: 213 additions & 180 deletions
Large diffs are not rendered by default.

‎aggregator/src/aggregation/decoder/seq_exec.rs‎

Lines changed: 37 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
use super::tables;
2-
use crate::aggregation::decoder::witgen;
31
use gadgets::util::{and, not, select, Expr};
42
use halo2_proofs::{
53
circuit::{AssignedCell, Layouter, Region, Value},
@@ -16,6 +14,9 @@ use zkevm_circuits::{
1614
util::Field,
1715
};
1816

17+
use super::tables;
18+
use crate::aggregation::{decoder::witgen, util::BooleanAdvice};
19+
1920
/// TODO: This is in fact part of the `BlockConfig` in
2021
/// Decoder, we can use BlockConfig if it is decoupled
2122
/// from Decoder module later
@@ -272,13 +273,13 @@ pub struct SeqExecConfig<F: Field> {
272273

273274
// the flag indicate current seq is the special one
274275
// (copying the rest bytes in literal section)
275-
s_last_lit_cp_phase: Column<Advice>,
276+
s_last_lit_cp_phase: BooleanAdvice,
276277
// the flag indicate the execution is under
277278
// "literal copying" phase
278-
s_lit_cp_phase: Column<Advice>,
279+
s_lit_cp_phase: BooleanAdvice,
279280
// the flag indicate the execution is under
280281
// back reference phase
281-
s_back_ref_phase: Column<Advice>,
282+
s_back_ref_phase: BooleanAdvice,
282283
// the copied index in literal section
283284
literal_pos: Column<Advice>,
284285
// the back-ref pos
@@ -306,10 +307,12 @@ impl<F: Field> SeqExecConfig<F> {
306307
let decoded_len = meta.advice_column();
307308
let decoded_byte = meta.advice_column();
308309
let decoded_rlc = meta.advice_column_in(SecondPhase);
309-
//let decoded_len_acc = meta.advice_column();
310-
let s_last_lit_cp_phase = meta.advice_column();
311-
let s_lit_cp_phase = meta.advice_column();
312-
let s_back_ref_phase = meta.advice_column();
310+
let s_last_lit_cp_phase =
311+
BooleanAdvice::construct(meta, |meta| meta.query_fixed(q_enabled, Rotation::cur()));
312+
let s_lit_cp_phase =
313+
BooleanAdvice::construct(meta, |meta| meta.query_fixed(q_enabled, Rotation::cur()));
314+
let s_back_ref_phase =
315+
BooleanAdvice::construct(meta, |meta| meta.query_fixed(q_enabled, Rotation::cur()));
313316
let backref_offset = meta.advice_column();
314317
let backref_progress = meta.advice_column();
315318
let literal_pos = meta.advice_column();
@@ -361,15 +364,12 @@ impl<F: Field> SeqExecConfig<F> {
361364
meta.create_gate("phases", |meta| {
362365
let mut cb = BaseConstraintBuilder::default();
363366

364-
let s_lit_cp_phase_next = meta.query_advice(s_lit_cp_phase, Rotation::next());
365-
let s_back_ref_phase_next = meta.query_advice(s_back_ref_phase, Rotation::next());
366-
let s_lit_cp_phase_prev = meta.query_advice(s_lit_cp_phase, Rotation::prev());
367-
let s_back_ref_phase_prev = meta.query_advice(s_back_ref_phase, Rotation::prev());
368-
let s_lit_cp_phase = meta.query_advice(s_lit_cp_phase, Rotation::cur());
369-
let s_back_ref_phase = meta.query_advice(s_back_ref_phase, Rotation::cur());
370-
371-
cb.require_boolean("phase is boolean", s_lit_cp_phase.expr());
372-
cb.require_boolean("phase is boolean", s_back_ref_phase.expr());
367+
let s_lit_cp_phase_next = s_lit_cp_phase.expr_at(meta, Rotation::next());
368+
let s_back_ref_phase_next = s_back_ref_phase.expr_at(meta, Rotation::next());
369+
let s_lit_cp_phase_prev = s_lit_cp_phase.expr_at(meta, Rotation::prev());
370+
let s_back_ref_phase_prev = s_back_ref_phase.expr_at(meta, Rotation::prev());
371+
let s_lit_cp_phase = s_lit_cp_phase.expr_at(meta, Rotation::cur());
372+
let s_back_ref_phase = s_back_ref_phase.expr_at(meta, Rotation::cur());
373373

374374
is_padding = 1.expr() - s_lit_cp_phase.expr() - s_back_ref_phase.expr();
375375
// constraint padding is boolean, so cp/back_ref phase is excluded
@@ -421,9 +421,8 @@ impl<F: Field> SeqExecConfig<F> {
421421
meta.create_gate("last literal cp phase", |meta| {
422422
let mut cb = BaseConstraintBuilder::default();
423423

424-
let s_last_lit_cp_phase_prev = meta.query_advice(s_last_lit_cp_phase, Rotation::prev());
425-
let s_last_lit_cp_phase = meta.query_advice(s_last_lit_cp_phase, Rotation::cur());
426-
cb.require_boolean("last lit_cp phase is boolean", s_last_lit_cp_phase.expr());
424+
let s_last_lit_cp_phase_prev = s_last_lit_cp_phase.expr_at(meta, Rotation::prev());
425+
let s_last_lit_cp_phase = s_last_lit_cp_phase.expr_at(meta, Rotation::cur());
427426

428427
cb.condition(
429428
and::expr([
@@ -456,7 +455,7 @@ impl<F: Field> SeqExecConfig<F> {
456455
cb.condition(s_last_lit_cp_phase.expr(), |cb| {
457456
cb.require_equal(
458457
"lit cp must actived if last lit cp is actived",
459-
meta.query_advice(s_lit_cp_phase, Rotation::cur()),
458+
s_lit_cp_phase.expr_at(meta, Rotation::cur()),
460459
1.expr(),
461460
);
462461
});
@@ -470,7 +469,7 @@ impl<F: Field> SeqExecConfig<F> {
470469

471470
let literal_pos_prev = meta.query_advice(literal_pos, Rotation::prev());
472471
let literal_pos = meta.query_advice(literal_pos, Rotation::cur());
473-
let s_lit_cp_phase = meta.query_advice(s_lit_cp_phase, Rotation::cur());
472+
let s_lit_cp_phase = s_lit_cp_phase.expr_at(meta, Rotation::cur());
474473

475474
cb.require_equal(
476475
"lit cp is increment in one block",
@@ -487,7 +486,7 @@ impl<F: Field> SeqExecConfig<F> {
487486
let backref_progress_prev = meta.query_advice(backref_progress, Rotation::prev());
488487
let backref_progress = meta.query_advice(backref_progress, Rotation::cur());
489488

490-
let s_back_ref_phase = meta.query_advice(s_back_ref_phase, Rotation::cur());
489+
let s_back_ref_phase = s_back_ref_phase.expr_at(meta, Rotation::cur());
491490

492491
cb.require_equal(
493492
"backref progress is increment in one inst",
@@ -559,8 +558,7 @@ impl<F: Field> SeqExecConfig<F> {
559558

560559
let block_index = meta.query_advice(block_index, Rotation::prev());
561560
let seq_index = meta.query_advice(seq_index, Rotation::prev());
562-
let not_last_lit_cp =
563-
not::expr(meta.query_advice(s_last_lit_cp_phase, Rotation::prev()));
561+
let not_last_lit_cp = not::expr(s_last_lit_cp_phase.expr_at(meta, Rotation::prev()));
564562
let literal_pos_at_inst_end = meta.query_advice(literal_pos, Rotation::prev());
565563
let backref_offset_at_inst_end = meta.query_advice(backref_offset, Rotation::prev());
566564
let backref_len_at_inst_end = meta.query_advice(backref_progress, Rotation::prev());
@@ -588,7 +586,7 @@ impl<F: Field> SeqExecConfig<F> {
588586
debug_assert!(meta.degree() <= 9);
589587
meta.lookup_any("lit cp char", |meta| {
590588
let enabled = meta.query_fixed(q_enabled, Rotation::cur())
591-
* meta.query_advice(s_lit_cp_phase, Rotation::cur());
589+
* s_lit_cp_phase.expr_at(meta, Rotation::cur());
592590

593591
let block_index = meta.query_advice(block_index, Rotation::cur());
594592
let literal_pos = meta.query_advice(literal_pos, Rotation::cur());
@@ -624,9 +622,7 @@ impl<F: Field> SeqExecConfig<F> {
624622
.zip([1.expr(), ref_pos, cp_byte])
625623
.map(|(lookup_expr, src_expr)| {
626624
(
627-
src_expr
628-
* enabled.expr()
629-
* meta.query_advice(s_back_ref_phase, Rotation::cur()),
625+
src_expr * enabled.expr() * s_back_ref_phase.expr_at(meta, Rotation::cur()),
630626
lookup_expr,
631627
)
632628
})
@@ -666,7 +662,7 @@ impl<F: Field> SeqExecConfig<F> {
666662
let seq_index_at_block_end = meta.query_advice(seq_index, Rotation::prev())
667663
// if we have a additional literal copying phase, we
668664
// in fact has one extra instruction
669-
- meta.query_advice(s_last_lit_cp_phase, Rotation::prev());
665+
- s_last_lit_cp_phase.expr_at(meta, Rotation::prev());
670666

671667
seq_config
672668
.lookup_tbl(meta)
@@ -730,9 +726,9 @@ impl<F: Field> SeqExecConfig<F> {
730726

731727
for col in [
732728
self.decoded_byte,
733-
self.s_last_lit_cp_phase,
734-
self.s_lit_cp_phase,
735-
self.s_back_ref_phase,
729+
self.s_last_lit_cp_phase.column,
730+
self.s_lit_cp_phase.column,
731+
self.s_back_ref_phase.column,
736732
self.backref_offset,
737733
self.backref_progress,
738734
self.literal_pos,
@@ -797,7 +793,7 @@ impl<F: Field> SeqExecConfig<F> {
797793
(self.block_index, F::from(block_ind as u64)),
798794
(self.seq_index, F::from(inst_ind as u64)),
799795
(
800-
self.s_last_lit_cp_phase,
796+
self.s_last_lit_cp_phase.column,
801797
if inst_ind > seq_info.num_sequences {
802798
F::one()
803799
} else {
@@ -865,15 +861,15 @@ impl<F: Field> SeqExecConfig<F> {
865861

866862
for (col, val) in base_rows.into_iter().chain(decodes).chain(if is_literal {
867863
[
868-
(self.s_lit_cp_phase, F::one()),
869-
(self.s_back_ref_phase, F::zero()),
864+
(self.s_lit_cp_phase.column, F::one()),
865+
(self.s_back_ref_phase.column, F::zero()),
870866
(self.literal_pos, F::from(pos as u64)),
871867
(self.backref_progress, F::zero()),
872868
]
873869
} else {
874870
[
875-
(self.s_lit_cp_phase, F::zero()),
876-
(self.s_back_ref_phase, F::one()),
871+
(self.s_lit_cp_phase.column, F::zero()),
872+
(self.s_back_ref_phase.column, F::one()),
877873
(self.literal_pos, F::from(cur_literal_cp as u64)),
878874
(self.backref_progress, F::from(i as u64 + 1)),
879875
]
@@ -915,9 +911,8 @@ impl<F: Field> SeqExecConfig<F> {
915911
self.decoded_rlc,
916912
self.block_index,
917913
self.seq_index,
918-
self.s_back_ref_phase,
919-
self.s_lit_cp_phase,
920-
self.s_back_ref_phase,
914+
self.s_back_ref_phase.column,
915+
self.s_lit_cp_phase.column,
921916
self.backref_offset,
922917
self.literal_pos,
923918
self.backref_progress,

0 commit comments

Comments
 (0)