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

Commit d0e7a07

Browse files
lightsinglightsing
authored
fix LtChip range check (#690)
* add range check * add range table * replace Range256Table of rlp_circuit_fsm * replace u16_table of tx_circuit * use TableColumn * merge #694 * add type alias * use type alias * fix import * missing q_enable * annotate lookup column * fix dev table load * revert to u8 table lookup * fix dev_load * revert degree changes * the degree should fit in u8 table * the degree should fit in u8 table
1 parent 70ccef7 commit d0e7a07

File tree

7 files changed

+144
-65
lines changed

7 files changed

+144
-65
lines changed

‎gadgets/src/comparator.rs‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,14 @@ use eth_types::Field;
55
use halo2_proofs::{
66
arithmetic::FieldExt,
77
circuit::{Chip, Region, Value},
8-
plonk::{ConstraintSystem, Error, Expression, VirtualCells},
8+
plonk::{ConstraintSystem, Error, Expression, TableColumn, VirtualCells},
99
poly::Rotation,
1010
};
1111

12-
use crate::{is_equal::IsEqualInstruction, less_than::LtInstruction};
13-
14-
use super::{is_equal::IsEqualChip, less_than::LtChip};
12+
use crate::{
13+
is_equal::{IsEqualChip, IsEqualInstruction},
14+
less_than::{LtChip, LtInstruction},
15+
};
1516

1617
/// Instruction that the Comparator chip needs to implement.
1718
pub trait ComparatorInstruction<F: FieldExt> {
@@ -61,8 +62,10 @@ impl<F: Field, const N_BYTES: usize> ComparatorChip<F, N_BYTES> {
6162
q_enable: impl FnOnce(&mut VirtualCells<F>) -> Expression<F> + Clone,
6263
lhs: impl FnOnce(&mut VirtualCells<F>) -> Expression<F> + Clone,
6364
rhs: impl FnOnce(&mut VirtualCells<F>) -> Expression<F> + Clone,
65+
u8_table: TableColumn,
6466
) -> ComparatorConfig<F, N_BYTES> {
65-
let lt_config = LtChip::configure(meta, q_enable.clone(), lhs.clone(), rhs.clone());
67+
let lt_config =
68+
LtChip::configure(meta, q_enable.clone(), lhs.clone(), rhs.clone(), u8_table);
6669
let eq_config = IsEqualChip::configure(meta, q_enable, lhs, rhs);
6770

6871
ComparatorConfig {

‎gadgets/src/less_than.rs‎

Lines changed: 62 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4,15 +4,13 @@ use eth_types::Field;
44
use halo2_proofs::{
55
arithmetic::FieldExt,
66
circuit::{Chip, Region, Value},
7-
plonk::{Advice, Column, ConstraintSystem, Error, Expression, VirtualCells},
7+
plonk::{Advice, Column, ConstraintSystem, Error, Expression, TableColumn, VirtualCells},
88
poly::Rotation,
99
};
1010

11-
use crate::util::sum;
12-
13-
use super::{
11+
use crate::{
1412
bool_check,
15-
util::{expr_from_bytes, pow_of_two},
13+
util::{expr_from_bytes, pow_of_two, sum},
1614
};
1715

1816
/// Instruction that the Lt chip needs to implement.
@@ -25,6 +23,11 @@ pub trait LtInstruction<F: FieldExt> {
2523
lhs: F,
2624
rhs: F,
2725
) -> Result<(), Error>;
26+
27+
#[cfg(test)]
28+
/// Load the u8 lookup table.
29+
fn dev_load(&self, layouter: &mut impl halo2_proofs::circuit::Layouter<F>)
30+
-> Result<(), Error>;
2831
}
2932

3033
/// Config for the Lt chip.
@@ -33,8 +36,9 @@ pub struct LtConfig<F, const N_BYTES: usize> {
3336
/// Denotes the lt outcome. If lhs < rhs then lt == 1, otherwise lt == 0.
3437
pub lt: Column<Advice>,
3538
/// Denotes the bytes representation of the difference between lhs and rhs.
36-
/// Note that the range of each byte is not checked by this config.
3739
pub diff: [Column<Advice>; N_BYTES],
40+
/// Denotes the range within which each byte should lie.
41+
pub u8_table: TableColumn,
3842
/// Denotes the range within which both lhs and rhs lie.
3943
pub range: F,
4044
}
@@ -62,16 +66,17 @@ impl<F: Field, const N_BYTES: usize> LtChip<F, N_BYTES> {
6266
/// Configures the Lt chip.
6367
pub fn configure(
6468
meta: &mut ConstraintSystem<F>,
65-
q_enable: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F>,
69+
q_enable: impl FnOnce(&mut VirtualCells<'_, F>) -> Expression<F> + Clone,
6670
lhs: impl FnOnce(&mut VirtualCells<F>) -> Expression<F>,
6771
rhs: impl FnOnce(&mut VirtualCells<F>) -> Expression<F>,
72+
u8_table: TableColumn,
6873
) -> LtConfig<F, N_BYTES> {
6974
let lt = meta.advice_column();
7075
let diff = [(); N_BYTES].map(|_| meta.advice_column());
7176
let range = pow_of_two(N_BYTES * 8);
7277

7378
meta.create_gate("lt gate", |meta| {
74-
let q_enable = q_enable(meta);
79+
let q_enable = q_enable.clone()(meta);
7580
let lt = meta.query_advice(lt, Rotation::cur());
7681

7782
let diff_bytes = diff
@@ -89,7 +94,22 @@ impl<F: Field, const N_BYTES: usize> LtChip<F, N_BYTES> {
8994
.map(move |poly| q_enable.clone() * poly)
9095
});
9196

92-
LtConfig { lt, diff, range }
97+
for cell_column in diff {
98+
meta.lookup("range check for u8", |meta| {
99+
let q_enable = q_enable.clone()(meta);
100+
vec![(
101+
q_enable * meta.query_advice(cell_column, Rotation::cur()),
102+
u8_table,
103+
)]
104+
});
105+
}
106+
107+
LtConfig {
108+
lt,
109+
diff,
110+
u8_table,
111+
range,
112+
}
93113
}
94114

95115
/// Constructs a Lt chip given a config.
@@ -129,6 +149,29 @@ impl<F: Field, const N_BYTES: usize> LtInstruction<F> for LtChip<F, N_BYTES> {
129149

130150
Ok(())
131151
}
152+
153+
#[cfg(test)]
154+
fn dev_load(
155+
&self,
156+
layouter: &mut impl halo2_proofs::circuit::Layouter<F>,
157+
) -> Result<(), Error> {
158+
const RANGE: usize = u8::MAX as usize;
159+
160+
layouter.assign_table(
161+
|| "load u8 range check table",
162+
|mut table| {
163+
for i in 0..=RANGE {
164+
table.assign_cell(
165+
|| "assign cell in fixed column",
166+
self.config.u8_table,
167+
i,
168+
|| Value::known(F::from(i as u64)),
169+
)?;
170+
}
171+
Ok(())
172+
},
173+
)
174+
}
132175
}
133176

134177
impl<F: Field, const N_BYTES: usize> Chip<F> for LtChip<F, N_BYTES> {
@@ -164,7 +207,7 @@ mod test {
164207

165208
// TODO: remove zk blinding factors in halo2 to restore the
166209
// correct k (without the extra + 2).
167-
let k = usize::BITS - $values.len().leading_zeros() + 2;
210+
let k = (usize::BITS - $values.len().leading_zeros() + 2).max(9);
168211
let circuit = TestCircuit::<Fp> {
169212
values: Some($values),
170213
checks: Some($checks),
@@ -181,7 +224,7 @@ mod test {
181224

182225
// TODO: remove zk blinding factors in halo2 to restore the
183226
// correct k (without the extra + 2).
184-
let k = usize::BITS - $values.len().leading_zeros() + 2;
227+
let k = (usize::BITS - $values.len().leading_zeros() + 2).max(9);
185228
let circuit = TestCircuit::<Fp> {
186229
values: Some($values),
187230
checks: Some($checks),
@@ -222,12 +265,14 @@ mod test {
222265
let q_enable = meta.complex_selector();
223266
let value = meta.advice_column();
224267
let check = meta.advice_column();
268+
let u8_table = meta.lookup_table_column();
225269

226270
let lt = LtChip::configure(
227271
meta,
228272
|meta| meta.query_selector(q_enable),
229273
|meta| meta.query_advice(value, Rotation::prev()),
230274
|meta| meta.query_advice(value, Rotation::cur()),
275+
u8_table,
231276
);
232277

233278
let config = Self::Config {
@@ -265,6 +310,8 @@ mod test {
265310
let (first_value, values) = values.split_at(1);
266311
let first_value = first_value[0];
267312

313+
chip.dev_load(&mut layouter)?;
314+
268315
layouter.assign_region(
269316
|| "witness",
270317
|mut region| {
@@ -340,12 +387,14 @@ mod test {
340387
let q_enable = meta.complex_selector();
341388
let (value_a, value_b) = (meta.advice_column(), meta.advice_column());
342389
let check = meta.advice_column();
390+
let u16_table = meta.lookup_table_column();
343391

344392
let lt = LtChip::configure(
345393
meta,
346394
|meta| meta.query_selector(q_enable),
347395
|meta| meta.query_advice(value_a, Rotation::cur()),
348396
|meta| meta.query_advice(value_b, Rotation::cur()),
397+
u16_table,
349398
);
350399

351400
let config = Self::Config {
@@ -387,6 +436,8 @@ mod test {
387436
.ok_or(Error::Synthesis)?;
388437
let checks = self.checks.as_ref().ok_or(Error::Synthesis)?;
389438

439+
chip.dev_load(&mut layouter)?;
440+
390441
layouter.assign_region(
391442
|| "witness",
392443
|mut region| {

‎zkevm-circuits/src/rlp_circuit_fsm.rs‎

Lines changed: 21 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,21 @@ mod dev;
55
#[cfg(any(feature = "test", test))]
66
mod test;
77

8-
use std::marker::PhantomData;
9-
10-
use crate::util::is_zero::{IsZeroChip, IsZeroConfig};
8+
use crate::{
9+
evm_circuit::util::constraint_builder::{BaseConstraintBuilder, ConstrainBuilderCommon},
10+
table::{LookupTable, RlpFsmRlpTable, U8Table},
11+
util::{
12+
is_zero::{IsZeroChip, IsZeroConfig},
13+
Challenges, SubCircuit, SubCircuitConfig,
14+
},
15+
witness::{
16+
Block, DataTable, Format, RlpFsmWitnessGen, RlpFsmWitnessRow, RlpTag, RomTableRow, State,
17+
State::{DecodeTagStart, End},
18+
Tag,
19+
Tag::{BeginList, EndList, TxType},
20+
Transaction,
21+
},
22+
};
1123
use eth_types::Field;
1224
use gadgets::{
1325
binary_number::{BinaryNumberChip, BinaryNumberConfig},
@@ -23,21 +35,9 @@ use halo2_proofs::{
2335
poly::Rotation,
2436
};
2537
use itertools::Itertools;
38+
use std::marker::PhantomData;
2639
use strum::IntoEnumIterator;
2740

28-
use crate::{
29-
evm_circuit::util::constraint_builder::{BaseConstraintBuilder, ConstrainBuilderCommon},
30-
table::{LookupTable, RlpFsmRlpTable, U8Table},
31-
util::{Challenges, SubCircuit, SubCircuitConfig},
32-
witness::{
33-
Block, DataTable, Format, RlpFsmWitnessGen, RlpFsmWitnessRow, RlpTag, RomTableRow, State,
34-
State::{DecodeTagStart, End},
35-
Tag,
36-
Tag::{BeginList, EndList, TxType},
37-
Transaction,
38-
},
39-
};
40-
4141
/// Data table allows us a lookup argument from the RLP circuit to check the byte value at an index
4242
/// while decoding a tx of a given format.
4343
#[derive(Clone, Copy, Debug)]
@@ -279,7 +279,7 @@ pub struct RlpCircuitConfig<F> {
279279
data_table: RlpFsmDataTable,
280280
/// ROM table
281281
rom_table: RlpFsmRomTable,
282-
/// Range256 table
282+
/// Range u8 table
283283
u8_table: U8Table,
284284
}
285285

@@ -619,6 +619,7 @@ impl<F: Field> RlpCircuitConfig<F> {
619619
cmp_enabled,
620620
|meta| meta.query_advice(byte_value, Rotation::cur()),
621621
|_| $value.expr(),
622+
u8_table.into(),
622623
);
623624
};
624625
}
@@ -629,6 +630,7 @@ impl<F: Field> RlpCircuitConfig<F> {
629630
cmp_enabled,
630631
|_| $value.expr(),
631632
|meta| meta.query_advice(byte_value, Rotation::cur()),
633+
u8_table.into(),
632634
);
633635
};
634636
}
@@ -711,12 +713,14 @@ impl<F: Field> RlpCircuitConfig<F> {
711713
cmp_enabled,
712714
|meta| meta.query_advice(tag_idx, Rotation::cur()),
713715
|meta| meta.query_advice(tag_length, Rotation::cur()),
716+
u8_table.into(),
714717
);
715718
let mlength_lte_0x20 = ComparatorChip::configure(
716719
meta,
717720
cmp_enabled,
718721
|meta| meta.query_advice(max_length, Rotation::cur()),
719722
|_meta| 0x20.expr(),
723+
u8_table.into(),
720724
);
721725
let depth_check = IsEqualChip::configure(
722726
meta,

‎zkevm-circuits/src/rlp_circuit_fsm/test.rs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ fn test_eip_155_tx() {
5252
_marker: Default::default(),
5353
};
5454

55-
let mock_prover = MockProver::run(14, &rlp_circuit, vec![]);
55+
let mock_prover = MockProver::run(17, &rlp_circuit, vec![]);
5656
assert!(mock_prover.is_ok());
5757
let mock_prover = mock_prover.unwrap();
5858
if let Err(errors) = mock_prover.verify_par() {
@@ -72,7 +72,7 @@ fn test_pre_eip155_tx() {
7272
_marker: Default::default(),
7373
};
7474

75-
let mock_prover = MockProver::run(16, &rlp_circuit, vec![]);
75+
let mock_prover = MockProver::run(17, &rlp_circuit, vec![]);
7676
assert!(mock_prover.is_ok());
7777
let mock_prover = mock_prover.unwrap();
7878
if let Err(errors) = mock_prover.verify_par() {
@@ -99,7 +99,7 @@ fn test_l1_msg_tx() {
9999
_marker: Default::default(),
100100
};
101101

102-
let mock_prover = MockProver::run(16, &rlp_circuit, vec![]);
102+
let mock_prover = MockProver::run(14, &rlp_circuit, vec![]);
103103
assert!(mock_prover.is_ok());
104104

105105
let mock_prover = mock_prover.unwrap();
@@ -126,7 +126,7 @@ fn test_eip1559_tx() {
126126
_marker: Default::default(),
127127
};
128128

129-
let mock_prover = MockProver::run(16, &rlp_circuit, vec![]);
129+
let mock_prover = MockProver::run(14, &rlp_circuit, vec![]);
130130
assert!(mock_prover.is_ok());
131131
let mock_prover = mock_prover.unwrap();
132132
if let Err(errors) = mock_prover.verify_par() {

‎zkevm-circuits/src/super_circuit.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -255,6 +255,7 @@ impl SubCircuitConfig<Fr> for SuperCircuitConfig<Fr> {
255255
keccak_table: keccak_table.clone(),
256256
rlp_table,
257257
sig_table,
258+
u8_table,
258259
u16_table,
259260
challenges: challenges_expr.clone(),
260261
},

0 commit comments

Comments
 (0)