Skip to content
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.

Commit

Permalink
fix modulo soundness due to overflow (#996)
Browse files Browse the repository at this point in the history
  • Loading branch information
Wu Sung Ming committed Dec 21, 2022
1 parent 82e6c87 commit 1fbec15
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 17 deletions.
2 changes: 1 addition & 1 deletion zkevm-circuits/src/evm_circuit/execution/mulmod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ impl<F: Field> ExecutionGadget<F> for MulModGadget<F> {
self.e.assign(region, offset, Some(e.to_le_bytes()))?;

self.modword
.assign(region, offset, a, n, a_reduced, block.randomness)?;
.assign(region, offset, a, n, a_reduced, k, block.randomness)?;
self.mul512_left
.assign(region, offset, [a_reduced, b, d, e], None)?;
self.mul512_right
Expand Down
46 changes: 34 additions & 12 deletions zkevm-circuits/src/evm_circuit/util/math_gadget/modulo.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use halo2_proofs::plonk::Error;
pub(crate) struct ModGadget<F> {
k: util::Word<F>,
a_or_zero: util::Word<F>,
mul: MulAddWordsGadget<F>,
mul_add_words: MulAddWordsGadget<F>,
n_is_zero: IsZeroGadget<F>,
a_or_is_zero: IsZeroGadget<F>,
eq: IsEqualGadget<F>,
Expand All @@ -33,11 +33,11 @@ impl<F: Field> ModGadget<F> {
let a_or_zero = cb.query_word();
let n_is_zero = IsZeroGadget::construct(cb, sum::expr(&n.cells));
let a_or_is_zero = IsZeroGadget::construct(cb, sum::expr(&a_or_zero.cells));
let mul = MulAddWordsGadget::construct(cb, [&k, n, r, &a_or_zero]);
let mul_add_words = MulAddWordsGadget::construct(cb, [&k, n, r, &a_or_zero]);
let eq = IsEqualGadget::construct(cb, a.expr(), a_or_zero.expr());
let lt = LtWordGadget::construct(cb, r, n);
// Constraint the aux variable a_or_zero to be =a or =0 if n==0:
// (a == a_zero) ^ (n == 0 & a_or_zero == 0)
// Constrain the aux variable a_or_zero to be =a or =0 if n==0:
// (a == a_or_zero) ^ (n == 0 & a_or_zero == 0)
cb.add_constraint(
" (1 - (a == a_or_zero)) * ( 1 - (n == 0) * (a_or_zero == 0)",
(1.expr() - eq.expr()) * (1.expr() - n_is_zero.expr() * a_or_is_zero.expr()),
Expand All @@ -49,10 +49,13 @@ impl<F: Field> ModGadget<F> {
1.expr() - lt.expr() - n_is_zero.expr(),
);

// Constrain k * n + r no overflow
cb.add_constraint("overflow == 0 for k * n + r", mul_add_words.overflow());

Self {
k,
a_or_zero,
mul,
mul_add_words,
n_is_zero,
a_or_is_zero,
eq,
Expand All @@ -67,9 +70,9 @@ impl<F: Field> ModGadget<F> {
a: Word,
n: Word,
r: Word,
k: Word,
randomness: F,
) -> Result<(), Error> {
let k = if n.is_zero() { Word::zero() } else { a / n };
let a_or_zero = if n.is_zero() { Word::zero() } else { a };

self.k.assign(region, offset, Some(k.to_le_bytes()))?;
Expand All @@ -80,7 +83,8 @@ impl<F: Field> ModGadget<F> {
self.n_is_zero.assign(region, offset, F::from(n_sum))?;
self.a_or_is_zero
.assign(region, offset, F::from(a_or_zero_sum))?;
self.mul.assign(region, offset, [k, n, r, a_or_zero])?;
self.mul_add_words
.assign(region, offset, [k, n, r, a_or_zero])?;
self.lt.assign(region, offset, r, n)?;
self.eq.assign(
region,
Expand All @@ -97,7 +101,7 @@ impl<F: Field> ModGadget<F> {
mod tests {
use super::test_util::*;
use super::*;
use eth_types::Word;
use eth_types::{Word, U256, U512};
use halo2_proofs::halo2curves::bn256::Fr;
use halo2_proofs::plonk::Error;

Expand Down Expand Up @@ -131,14 +135,19 @@ mod tests {
) -> Result<(), Error> {
let a = witnesses[0];
let n = witnesses[1];
let a_reduced = witnesses[2];
let r = witnesses[2];
let k = witnesses
.get(3)
.map(|x| x.clone())
.unwrap_or(if n.is_zero() { Word::zero() } else { a / n });

let offset = 0;

self.a.assign(region, offset, Some(a.to_le_bytes()))?;
self.n.assign(region, offset, Some(n.to_le_bytes()))?;
self.r
.assign(region, offset, Some(a_reduced.to_le_bytes()))?;
self.mod_gadget.assign(region, 0, a, n, a_reduced, F::one())
self.r.assign(region, offset, Some(r.to_le_bytes()))?;

self.mod_gadget.assign(region, 0, a, n, r, k, F::one())
}
}

Expand Down Expand Up @@ -183,6 +192,19 @@ mod tests {

#[test]
fn test_mod_n_unexpected_rem() {
// manipulate larger k to make a' = k * n + r and a' >= 2^256
// lead to overflow and trigger soundness bug: (a' != a) ^ a' ≡ a (mod 2^256)
try_test!(
ModGadgetTestContainer<Fr>,
vec![
Word::from(2),
Word::from(3),
Word::from(0),
U256::try_from((U512([0, 0, 0, 0, 1, 0, 0, 0]) + U512::from(2)) / U512::from(3))
.unwrap(), // magic number (2^256 + 2) / 3, and 2^256 + 2 divisible by 3
],
false,
);
try_test!(
ModGadgetTestContainer<Fr>,
vec![Word::from(1), Word::from(1), Word::from(1)],
Expand Down
21 changes: 17 additions & 4 deletions zkevm-circuits/src/evm_circuit/util/math_gadget/mul_add_words.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@ impl<F: Field> MulAddWordsGadget<F> {
+ a_limbs[2] * b_limbs[1]
+ a_limbs[3] * b_limbs[0];

let carry_lo = (t0 + (t1 << 64) + c_lo - d_lo) >> 128;
let carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo - d_hi) >> 128;
let carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128;
let carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128;

self.carry_lo
.iter()
Expand Down Expand Up @@ -347,7 +347,20 @@ mod tests {
false,
);

// 100 * 54 + low_max == low_max + 5400, no overflow
// 10 * 1 + 1 != 50, no underflow
try_test!(
MulAddGadgetContainer<Fr>,
vec![
Word::from(10),
Word::from(1),
Word::from(1),
Word::from(50),
Word::from(0)
],
false,
);

// 100 * 54 + high_max == high_max + 5400, no overflow
try_test!(
MulAddGadgetContainer<Fr>,
vec![
Expand All @@ -360,7 +373,7 @@ mod tests {
false,
);

// high_max + low_max + 1 == 0 with overflow 1
// (low_max + 1) * 1 + high_max == 0 with overflow 1
try_test!(
MulAddGadgetContainer<Fr>,
vec![
Expand Down

0 comments on commit 1fbec15

Please sign in to comment.