-
Notifications
You must be signed in to change notification settings - Fork 219
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Added efficient field comparisons for bn254 (#4042)
# Description Adds efficient field comparisons for the bn254 field. ## Problem\* Previously, field comparisons were made by decomposing to bytes. This PR optimizes this by decomposing the field in an unconstrained function. ## Summary\* Field comparisons via byte decomposing had a cost of ~850 constraints. This PR adds some bn254 specific functions to: - assert_gt / assert_lt : ~77 constraints - gt/lt: ~190 constraints ## Additional Context @zac-williamson explanation: decompose(x: field) returns xlo, xhi as fields The algorithm requires knowledge of the field modulus p , as well as it’s 128-bit components plo, phi such that p = plo + phi * 2^{128} plo, phi need to be defined as circuit constants in an unconstrained function: 1. compute xlo, xhi such that x = xlo + 2^{128}xhi 2. compute borrow: bool such that borrow = xlo > plo in a constrained function: 1. assert xlo < 2^{128} 2. assert xhi < 2^{128} 3. assert(x == xlo + 2^{128}xhi 4. let rlo = plo - xlo + borrow*2^{128} 5. let rhi = phi - xhi - borrow 6. assert rlo < 2^{128} 7. assert rhi < 2^{128} --- The purpose of rlo, rhi is to ensure that xlo + 2^{128}xhi does not wrap around the field modulus p With a decompose method implemented, a assert_gt(a, b) method can be built assert_gt(a: field, b: field) 1. let alo, ahi = decompose(a) 2. let blo, bhi = decompose(b) If a > b then we want a - b - 1 >= 0 . We can evaluate this relation over each of the 128-bit slices: in an unconstrained function, let borrow: bool = (alo <= blo) in a constrained function: 1. let rlo = alo - blo - 1 + borrow*2^{128} 2. let rhi = ahi - bhi - borrow 3. assert rlo < 2^{128} 4. assert rhi < 2^{128} --- Also a gt/lt method is provided leveraging a hint + assert_gt. ## Documentation\* Check one: - [ ] No documentation needed. - [ ] Documentation included in this PR. - [ ] **[Exceptional Case]** 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
1 parent
c631e1b
commit 1f9cad0
Showing
9 changed files
with
241 additions
and
20 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,92 @@ | ||
global PLO: Field = 53438638232309528389504892708671455233; | ||
global PHI: Field = 64323764613183177041862057485226039389; | ||
global TWO_POW_128: Field = 0x100000000000000000000000000000000; | ||
|
||
unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) { | ||
let x_bytes = x.to_le_bytes(32); | ||
|
||
let mut low: Field = 0; | ||
let mut high: Field = 0; | ||
|
||
let mut offset = 1; | ||
for i in 0..16 { | ||
low += (x_bytes[i] as Field) * offset; | ||
high += (x_bytes[i + 16] as Field) * offset; | ||
offset *= 256; | ||
} | ||
|
||
(low, high) | ||
} | ||
|
||
pub fn decompose(x: Field) -> (Field, Field) { | ||
let (xlo, xhi) = decompose_unsafe(x); | ||
let borrow = lt_unsafe(PLO, xlo, 16); | ||
|
||
xlo.assert_max_bit_size(128); | ||
xhi.assert_max_bit_size(128); | ||
|
||
assert_eq(x, xlo + TWO_POW_128 * xhi); | ||
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); | ||
|
||
(xlo, xhi) | ||
} | ||
|
||
unconstrained fn lt_unsafe(x: Field, y: Field, num_bytes: u32) -> bool { | ||
let x_bytes = x.__to_le_radix(256, num_bytes); | ||
let y_bytes = y.__to_le_radix(256, num_bytes); | ||
let mut x_is_lt = false; | ||
let mut done = false; | ||
for i in 0..num_bytes { | ||
if (!done) { | ||
let x_byte = x_bytes[num_bytes - 1 - i]; | ||
let y_byte = y_bytes[num_bytes - 1 - i]; | ||
let bytes_match = x_byte == y_byte; | ||
if !bytes_match { | ||
x_is_lt = x_byte < y_byte; | ||
done = true; | ||
} | ||
} | ||
} | ||
x_is_lt | ||
} | ||
|
||
unconstrained fn lte_unsafe(x: Field, y: Field, num_bytes: u32) -> bool { | ||
lt_unsafe(x, y, num_bytes) | (x == y) | ||
} | ||
|
||
pub fn assert_gt(a: Field, b: Field) { | ||
let (alo, ahi) = decompose(a); | ||
let (blo, bhi) = decompose(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); | ||
} | ||
|
||
pub fn assert_lt(a: Field, b: Field) { | ||
assert_gt(b, a); | ||
} | ||
|
||
pub fn gt(a: Field, b: Field) -> bool { | ||
if a == b { | ||
false | ||
} else if lt_unsafe(a, b, 32) { | ||
assert_gt(b, a); | ||
false | ||
} else { | ||
assert_gt(a, b); | ||
true | ||
} | ||
} | ||
|
||
pub fn lt(a: Field, b: Field) -> bool { | ||
gt(b, a) | ||
} |
6 changes: 6 additions & 0 deletions
6
test_programs/compile_success_empty/field_comparisons/Nargo.toml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
[package] | ||
name = "field_comparisons" | ||
type = "bin" | ||
authors = [""] | ||
|
||
[dependencies] |
1 change: 1 addition & 0 deletions
1
test_programs/compile_success_empty/field_comparisons/Prover.toml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
|
86 changes: 86 additions & 0 deletions
86
test_programs/compile_success_empty/field_comparisons/src/main.nr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,86 @@ | ||
use dep::std::field::bn254::{PLO, PHI, TWO_POW_128, decompose, decompose_unsafe, lt_unsafe, lte_unsafe, assert_gt, gt}; | ||
|
||
fn check_plo_phi() { | ||
assert_eq(PLO + PHI * TWO_POW_128, 0); | ||
let p_bytes = dep::std::field::modulus_le_bytes(); | ||
let mut p_low: Field = 0; | ||
let mut p_high: Field = 0; | ||
|
||
let mut offset = 1; | ||
for i in 0..16 { | ||
p_low += (p_bytes[i] as Field) * offset; | ||
p_high += (p_bytes[i + 16] as Field) * offset; | ||
offset *= 256; | ||
} | ||
assert_eq(p_low, PLO); | ||
assert_eq(p_high, PHI); | ||
} | ||
|
||
fn check_decompose_unsafe() { | ||
assert_eq(decompose_unsafe(TWO_POW_128), (0, 1)); | ||
assert_eq(decompose_unsafe(TWO_POW_128 + 0x1234567890), (0x1234567890, 1)); | ||
assert_eq(decompose_unsafe(0x1234567890), (0x1234567890, 0)); | ||
} | ||
|
||
fn check_decompose() { | ||
assert_eq(decompose(TWO_POW_128), (0, 1)); | ||
assert_eq(decompose(TWO_POW_128 + 0x1234567890), (0x1234567890, 1)); | ||
assert_eq(decompose(0x1234567890), (0x1234567890, 0)); | ||
} | ||
|
||
fn check_lt_unsafe() { | ||
assert(lt_unsafe(0, 1, 16)); | ||
assert(lt_unsafe(0, 0x100, 16)); | ||
assert(lt_unsafe(0x100, TWO_POW_128 - 1, 16)); | ||
assert(!lt_unsafe(0, TWO_POW_128, 16)); | ||
} | ||
|
||
fn check_lte_unsafe() { | ||
assert(lte_unsafe(0, 1, 16)); | ||
assert(lte_unsafe(0, 0x100, 16)); | ||
assert(lte_unsafe(0x100, TWO_POW_128 - 1, 16)); | ||
assert(!lte_unsafe(0, TWO_POW_128, 16)); | ||
|
||
assert(lte_unsafe(0, 0, 16)); | ||
assert(lte_unsafe(0x100, 0x100, 16)); | ||
assert(lte_unsafe(TWO_POW_128 - 1, TWO_POW_128 - 1, 16)); | ||
assert(lte_unsafe(TWO_POW_128, TWO_POW_128, 16)); | ||
} | ||
|
||
fn check_assert_gt() { | ||
assert_gt(1, 0); | ||
assert_gt(0x100, 0); | ||
assert_gt((0 - 1), (0 - 2)); | ||
assert_gt(TWO_POW_128, 0); | ||
assert_gt(0 - 1, 0); | ||
} | ||
|
||
fn check_gt() { | ||
assert(gt(1, 0)); | ||
assert(gt(0x100, 0)); | ||
assert(gt((0 - 1), (0 - 2))); | ||
assert(gt(TWO_POW_128, 0)); | ||
assert(!gt(0, 0)); | ||
assert(!gt(0, 0x100)); | ||
assert(gt(0 - 1, 0 - 2)); | ||
assert(!gt(0 - 2, 0 - 1)); | ||
} | ||
|
||
fn checks() { | ||
check_plo_phi(); | ||
check_decompose_unsafe(); | ||
check_decompose(); | ||
check_lt_unsafe(); | ||
check_lte_unsafe(); | ||
check_assert_gt(); | ||
check_gt(); | ||
} | ||
|
||
unconstrained fn checks_in_brillig() { | ||
checks(); | ||
} | ||
|
||
fn main() { | ||
checks(); | ||
checks_in_brillig(); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
[package] | ||
name = "field_comparisons" | ||
type = "bin" | ||
authors = [""] | ||
[dependencies] |
Empty file.
16 changes: 16 additions & 0 deletions
16
test_programs/noir_test_success/field_comparisons/src/main.nr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
use dep::std::field::bn254::{TWO_POW_128, assert_gt}; | ||
|
||
#[test(should_fail)] | ||
fn test_assert_gt_should_fail_eq() { | ||
assert_gt(0, 0); | ||
} | ||
|
||
#[test(should_fail)] | ||
fn test_assert_gt_should_fail_low_lt() { | ||
assert_gt(0, 0x100); | ||
} | ||
|
||
#[test(should_fail)] | ||
fn test_assert_gt_should_fail_high_lt() { | ||
assert_gt(TWO_POW_128, TWO_POW_128 + 0x100); | ||
} |