Skip to content

Commit

Permalink
fix: Field comparisons (#4704)
Browse files Browse the repository at this point in the history
# Description

## Problem\*

Field comparisons could be tricked by a malicious prover by decomposing
0 as either (PLO,PHI) o (0,0). Now we reuse instead the assert_gt code
by extracting it to an assert_gt_limbs that is shared among decompose
(to check that the decomposition of x is less than the decomposition of
the field modulus, that is, that the decomposition of the field modulus
is greater than the decomposition of x) and assert_gt (to check that the
decomposition of a is greater than the decomposition of b)

## Summary\*



## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** Documentation to be submitted in a
separate PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
  • Loading branch information
sirasistant committed Apr 3, 2024
1 parent 386f6d0 commit 079cb2a
Showing 1 changed file with 19 additions and 18 deletions.
37 changes: 19 additions & 18 deletions noir_stdlib/src/field/bn254.nr
Original file line number Diff line number Diff line change
Expand Up @@ -21,11 +21,23 @@ unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) {
(low, high)
}

// Assert that (alo > blo && ahi >= bhi) || (alo <= blo && ahi > bhi)
fn assert_gt_limbs(a: (Field, Field), b: (Field, Field)) {
let (alo, ahi) = a;
let (blo, bhi) = b;
let borrow = lte_unsafe(alo, blo, 16);

let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
let rhi = ahi - bhi - (borrow as Field);

rlo.assert_max_bit_size(128);
rhi.assert_max_bit_size(128);
}

/// Decompose a single field into two 16 byte fields.
pub fn decompose(x: Field) -> (Field, Field) {
// Take hints of the decomposition
let (xlo, xhi) = decompose_unsafe(x);
let borrow = lt_unsafe(PLO, xlo, 16);

// Range check the limbs
xlo.assert_max_bit_size(128);
Expand All @@ -34,13 +46,8 @@ pub fn decompose(x: Field) -> (Field, Field) {
// Check that the decomposition is correct
assert_eq(x, xlo + TWO_POW_128 * xhi);

// Check that (xlo < plo && xhi <= phi) || (xlo >= plo && xhi < phi)
let rlo = PLO - xlo + (borrow as Field) * TWO_POW_128;
let rhi = PHI - xhi - (borrow as Field);

rlo.assert_max_bit_size(128);
rhi.assert_max_bit_size(128);

// Assert that the decomposition of P is greater than the decomposition of x
assert_gt_limbs((PLO, PHI), (xlo, xhi));
(xlo, xhi)
}

Expand Down Expand Up @@ -69,17 +76,11 @@ unconstrained fn lte_unsafe(x: Field, y: Field, num_bytes: u32) -> bool {

pub fn assert_gt(a: Field, b: Field) {
// Decompose a and b
let (alo, ahi) = decompose(a);
let (blo, bhi) = decompose(b);

let borrow = lte_unsafe(alo, blo, 16);
let a_limbs = decompose(a);
let b_limbs = decompose(b);

// Assert that (alo > blo && ahi >= bhi) || (alo <= blo && ahi > bhi)
let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
let rhi = ahi - bhi - (borrow as Field);

rlo.assert_max_bit_size(128);
rhi.assert_max_bit_size(128);
// Assert that a_limbs is greater than b_limbs
assert_gt_limbs(a_limbs, b_limbs)
}

pub fn assert_lt(a: Field, b: Field) {
Expand Down

0 comments on commit 079cb2a

Please sign in to comment.