Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 5 additions & 10 deletions src/fns/constrained_ops.nr
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ use crate::fns::{
expressions::{evaluate_quadratic_expression, validate_udiv_mod_expression},
unconstrained_helpers::{
__add_with_flags, __from_field, __neg_with_flags, __sub_with_flags,
__validate_gte_with_flags, __validate_in_field_compute_borrow_flags,
__validate_gt_with_flags, __validate_gte_with_flags,
__validate_in_field_compute_borrow_flags,
},
unconstrained_ops::{__add, __div, __mul, __neg, __sqr, __sub, __udiv_mod},
};
Expand Down Expand Up @@ -481,16 +482,10 @@ pub(crate) fn validate_quotient_in_range<let N: u32, let MOD_BITS: u32>(limbs: [
/// `assert_is_not_zero_integer(result)` is crucial. Without it, we could always provide
/// two identical inputs `x`, `x` and set `borrow_flags = [false; N]`,
/// which would satisfy the limb constraints.
///
/// Also note that `underflow` is not properly constrained, so it just hangs there for
/// completeness
pub(crate) fn validate_gt<let N: u32, let MOD_BITS: u32>(lhs: [u128; N], rhs: [u128; N]) {
// Safety: compute borrow flags out-of-circuit
let (underflow, result, borrow_flags): (bool, [u128; N], [bool; N - 1]) =
unsafe { __validate_gte_with_flags(lhs, rhs) };

// Completeness: require that no underflow occurred
assert(!underflow, "validate_gt fail");
// Safety: compute witness values out-of-circuit
let (result, borrow_flags): ([u128; N], [bool; N - 1]) =
unsafe { __validate_gt_with_flags(lhs, rhs) };

// Constrain the `result` to be a valid `BigNum` value
validate_in_range::<u128, N, MOD_BITS>(result);
Expand Down
49 changes: 28 additions & 21 deletions src/fns/unconstrained_helpers.nr
Original file line number Diff line number Diff line change
Expand Up @@ -189,34 +189,19 @@ pub(crate) unconstrained fn __validate_in_field_compute_borrow_flags<let N: u32,
borrow_flags
}

/// Validate that lhs - rhs does not underflow (unconstrained)
///
/// Compute underflow flag (lhs < rhs)
/// then perform subtraction with borrow flags
///
/// ## Note
/// The `borrow` must be equal to 0 at the end of the loop.
/// And it can't be nonzero, since we swap the terms at the beginning
pub(crate) unconstrained fn __validate_gte_with_flags<let N: u32>(
/// Compute `lhs - rhs` with borrow flags (unconstrained)
/// Return the result of the subtraction and the borrow flags
pub(crate) unconstrained fn __validate_gt_with_flags<let N: u32>(
lhs: [u128; N],
rhs: [u128; N],
) -> (bool, [u128; N], [bool; N - 1]) {
let mut a: [u128; N] = lhs;
let mut b: [u128; N] = rhs;

let underflow: bool = !__gte(lhs, rhs);
// swap a and b if there's an underflow
let (a, b): ([u128; N], [u128; N]) = if underflow { (b, a) } else { (a, b) };

) -> ([u128; N], [bool; N - 1]) {
let mut result: [u128; N] = [0; N];

let mut borrow_flags: [bool; N - 1] = [false; N - 1];

let mut borrow: u128 = 0;
for i in 0..N {
let mut add_term: u128 = a[i];

let sub_term: u128 = b[i] + borrow;
let add_term: u128 = lhs[i];
let sub_term: u128 = rhs[i] + borrow;
borrow = (sub_term > add_term) as u128;

result[i] = borrow * TWO_POW_120 + add_term - sub_term;
Expand All @@ -225,6 +210,28 @@ pub(crate) unconstrained fn __validate_gte_with_flags<let N: u32>(
borrow_flags[i] = borrow != 0;
}
}
(result, borrow_flags)
}

/// Validate that lhs - rhs does not underflow (unconstrained)
///
/// Compute underflow flag (lhs < rhs), then perform subtraction with borrow flags.
/// Always computes max(lhs, rhs) - min(lhs, rhs) by swapping if needed.
///
/// ## Note
/// The `borrow` must be equal to 0 at the end of the loop
/// And it can't be nonzero, since we swap the terms at the beginning
pub(crate) unconstrained fn __validate_gte_with_flags<let N: u32>(
lhs: [u128; N],
rhs: [u128; N],
) -> (bool, [u128; N], [bool; N - 1]) {
let underflow: bool = !__gte(lhs, rhs);
// swap a and b if there's an underflow
let (a, b): ([u128; N], [u128; N]) = if underflow { (rhs, lhs) } else { (lhs, rhs) };

// Compute max - min using the basic subtraction helper
let (result, borrow_flags) = __validate_gt_with_flags(a, b);

(underflow, result, borrow_flags)
}

Expand Down
4 changes: 2 additions & 2 deletions src/tests/bignum_test.nr
Original file line number Diff line number Diff line change
Expand Up @@ -383,7 +383,7 @@ fn test_to_field_three_digits() {
assert(result == field);
}

#[test(should_fail_with = "validate_gt fail")]
#[test(should_fail_with = "call to assert_max_bit_size")]
fn test_to_field_three_digits_overflow() {
let bn: BN254_Fq = BN254_Fq::from_limbs([
0x4e6405505a33bb9b9c0563df2bd59a,
Expand All @@ -393,7 +393,7 @@ fn test_to_field_three_digits_overflow() {
let _: Field = to_field(bn);
}

#[test(should_fail_with = "validate_gt fail")]
#[test(should_fail_with = "call to assert_max_bit_size")]
fn test_to_field_too_many_digits() {
let bn: BLS12_381_Fq = BLS12_381_Fq::from_limbs([
0xea1742447ee9d92f9f18e1c80a481e,
Expand Down