Skip to content

Commit

Permalink
chore!: use Brillig opcode when possible for less-than operations on …
Browse files Browse the repository at this point in the history
…fields (#9416)

Co-authored-by: Tom French <[email protected]>
Co-authored-by: Álvaro Rodríguez <[email protected]>
  • Loading branch information
3 people authored Oct 28, 2024
1 parent c6437cc commit e50303d
Show file tree
Hide file tree
Showing 10 changed files with 115 additions and 71 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -604,7 +604,31 @@ impl<'block> BrilligBlock<'block> {
// `Intrinsic::AsWitness` is used to provide hints to acir-gen on optimal expression splitting.
// It is then useless in the brillig runtime and so we can ignore it
Value::Intrinsic(Intrinsic::AsWitness) => (),
Value::Intrinsic(Intrinsic::FieldLessThan) => {
let lhs = self.convert_ssa_single_addr_value(arguments[0], dfg);
assert!(lhs.bit_size == FieldElement::max_num_bits());
let rhs = self.convert_ssa_single_addr_value(arguments[1], dfg);
assert!(rhs.bit_size == FieldElement::max_num_bits());

let results = dfg.instruction_results(instruction_id);
let destination = self
.variables
.define_variable(
self.function_context,
self.brillig_context,
results[0],
dfg,
)
.extract_single_addr();
assert!(destination.bit_size == 1);

self.brillig_context.binary_instruction(
lhs,
rhs,
destination,
BrilligBinaryOp::LessThan,
);
}
_ => {
unreachable!("unsupported function call type {:?}", dfg[*func])
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2789,6 +2789,9 @@ impl<'a> Context<'a> {
Intrinsic::DerivePedersenGenerators => {
unreachable!("DerivePedersenGenerators can only be called with constants")
}
Intrinsic::FieldLessThan => {
unreachable!("FieldLessThan can only be called in unconstrained")
}
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,8 @@ impl Context {
| Intrinsic::StaticAssert
| Intrinsic::StrAsBytes
| Intrinsic::ToBits(..)
| Intrinsic::ToRadix(..) => {
| Intrinsic::ToRadix(..)
| Intrinsic::FieldLessThan => {
self.value_sets.push(instruction_arguments_and_results);
}
},
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ pub(crate) enum Intrinsic {
AsWitness,
IsUnconstrained,
DerivePedersenGenerators,
FieldLessThan,
}

impl std::fmt::Display for Intrinsic {
Expand Down Expand Up @@ -100,6 +101,7 @@ impl std::fmt::Display for Intrinsic {
Intrinsic::AsWitness => write!(f, "as_witness"),
Intrinsic::IsUnconstrained => write!(f, "is_unconstrained"),
Intrinsic::DerivePedersenGenerators => write!(f, "derive_pedersen_generators"),
Intrinsic::FieldLessThan => write!(f, "field_less_than"),
}
}
}
Expand Down Expand Up @@ -131,7 +133,8 @@ impl Intrinsic {
| Intrinsic::FromField
| Intrinsic::AsField
| Intrinsic::IsUnconstrained
| Intrinsic::DerivePedersenGenerators => false,
| Intrinsic::DerivePedersenGenerators
| Intrinsic::FieldLessThan => false,

// Some black box functions have side-effects
Intrinsic::BlackBox(func) => matches!(
Expand Down Expand Up @@ -169,6 +172,8 @@ impl Intrinsic {
"as_witness" => Some(Intrinsic::AsWitness),
"is_unconstrained" => Some(Intrinsic::IsUnconstrained),
"derive_pedersen_generators" => Some(Intrinsic::DerivePedersenGenerators),
"field_less_than" => Some(Intrinsic::FieldLessThan),

other => BlackBoxFunc::lookup(other).map(Intrinsic::BlackBox),
}
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -355,6 +355,16 @@ pub(super) fn simplify_call(
unreachable!("Derive Pedersen Generators must return an array");
}
}
Intrinsic::FieldLessThan => {
if let Some(constants) = constant_args {
let lhs = constants[0];
let rhs = constants[1];
let result = dfg.make_constant((lhs < rhs).into(), Type::bool());
SimplifyResult::SimplifiedTo(result)
} else {
SimplifyResult::None
}
}
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,8 @@ impl Context {
| Intrinsic::AsSlice
| Intrinsic::AsWitness
| Intrinsic::IsUnconstrained
| Intrinsic::DerivePedersenGenerators => false,
| Intrinsic::DerivePedersenGenerators
| Intrinsic::FieldLessThan => false,
},

// We must assume that functions contain a side effect as we cannot inspect more deeply.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -237,6 +237,7 @@ fn slice_capacity_change(
| Intrinsic::IsUnconstrained
| Intrinsic::DerivePedersenGenerators
| Intrinsic::ToBits(_)
| Intrinsic::ToRadix(_) => SizeChange::None,
| Intrinsic::ToRadix(_)
| Intrinsic::FieldLessThan => SizeChange::None,
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ impl<'local, 'context> Interpreter<'local, 'context> {
"expr_is_continue" => expr_is_continue(interner, arguments, location),
"expr_resolve" => expr_resolve(self, arguments, location),
"is_unconstrained" => Ok(Value::Bool(true)),
"field_less_than" => field_less_than(arguments, location),
"fmtstr_as_ctstring" => fmtstr_as_ctstring(interner, arguments, location),
"fmtstr_quoted_contents" => fmtstr_quoted_contents(interner, arguments, location),
"fresh_type_variable" => fresh_type_variable(interner),
Expand Down Expand Up @@ -2849,3 +2850,12 @@ fn derive_generators(

Ok(Value::Array(results, return_type))
}

fn field_less_than(arguments: Vec<(Value, Location)>, location: Location) -> IResult<Value> {
let (lhs, rhs) = check_two_arguments(arguments, location)?;

let lhs = get_field(lhs)?;
let rhs = get_field(rhs)?;

Ok(Value::Bool(lhs < rhs))
}
73 changes: 19 additions & 54 deletions noir/noir-repo/noir_stdlib/src/field/bn254.nr
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use crate::field::field_less_than;
use crate::runtime::is_unconstrained;

// The low and high decomposition of the field modulus
Expand Down Expand Up @@ -25,47 +26,20 @@ pub(crate) unconstrained fn decompose_hint(x: Field) -> (Field, Field) {
compute_decomposition(x)
}

fn compute_lt(x: Field, y: Field, num_bytes: u32) -> bool {
let x_bytes: [u8; 32] = x.to_le_bytes();
let y_bytes: [u8; 32] = y.to_le_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
}

fn compute_lte(x: Field, y: Field, num_bytes: u32) -> bool {
unconstrained fn lte_hint(x: Field, y: Field) -> bool {
if x == y {
true
} else {
compute_lt(x, y, num_bytes)
field_less_than(x, y)
}
}

unconstrained fn lt_32_hint(x: Field, y: Field) -> bool {
compute_lt(x, y, 32)
}

unconstrained fn lte_16_hint(x: Field, y: Field) -> bool {
compute_lte(x, y, 16)
}

// 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;
unsafe {
let borrow = lte_16_hint(alo, blo);
let borrow = lte_hint(alo, blo);

let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
let rhi = ahi - bhi - (borrow as Field);
Expand Down Expand Up @@ -100,7 +74,7 @@ pub fn decompose(x: Field) -> (Field, Field) {

pub fn assert_gt(a: Field, b: Field) {
if is_unconstrained() {
assert(compute_lt(b, a, 32));
assert(unsafe { field_less_than(b, a) });
} else {
// Decompose a and b
let a_limbs = decompose(a);
Expand All @@ -117,13 +91,15 @@ pub fn assert_lt(a: Field, b: Field) {

pub fn gt(a: Field, b: Field) -> bool {
if is_unconstrained() {
compute_lt(b, a, 32)
unsafe {
field_less_than(b, a)
}
} else if a == b {
false
} else {
// Take a hint of the comparison and verify it
unsafe {
if lt_32_hint(a, b) {
if field_less_than(a, b) {
assert_gt(b, a);
false
} else {
Expand All @@ -140,9 +116,7 @@ pub fn lt(a: Field, b: Field) -> bool {

mod tests {
// TODO: Allow imports from "super"
use crate::field::bn254::{
assert_gt, compute_lt, compute_lte, decompose, gt, PHI, PLO, TWO_POW_128,
};
use crate::field::bn254::{assert_gt, decompose, gt, lte_hint, PHI, PLO, TWO_POW_128};

#[test]
fn check_decompose() {
Expand All @@ -159,24 +133,15 @@ mod tests {
}

#[test]
fn check_compute_lt() {
assert(compute_lt(0, 1, 16));
assert(compute_lt(0, 0x100, 16));
assert(compute_lt(0x100, TWO_POW_128 - 1, 16));
assert(!compute_lt(0, TWO_POW_128, 16));
}

#[test]
fn check_compute_lte() {
assert(compute_lte(0, 1, 16));
assert(compute_lte(0, 0x100, 16));
assert(compute_lte(0x100, TWO_POW_128 - 1, 16));
assert(!compute_lte(0, TWO_POW_128, 16));

assert(compute_lte(0, 0, 16));
assert(compute_lte(0x100, 0x100, 16));
assert(compute_lte(TWO_POW_128 - 1, TWO_POW_128 - 1, 16));
assert(compute_lte(TWO_POW_128, TWO_POW_128, 16));
unconstrained fn check_lte_hint() {
assert(lte_hint(0, 1));
assert(lte_hint(0, 0x100));
assert(lte_hint(0x100, TWO_POW_128 - 1));
assert(!lte_hint(0 - 1, 0));

assert(lte_hint(0, 0));
assert(lte_hint(0x100, 0x100));
assert(lte_hint(0 - 1, 0 - 1));
}

#[test]
Expand Down
50 changes: 37 additions & 13 deletions noir/noir-repo/noir_stdlib/src/field/mod.nr
Original file line number Diff line number Diff line change
Expand Up @@ -211,6 +211,14 @@ pub comptime fn modulus_be_bytes() -> [u8] {}
#[builtin(modulus_le_bytes)]
pub comptime fn modulus_le_bytes() -> [u8] {}

/// An unconstrained only built in to efficiently compare fields.
#[builtin(field_less_than)]
unconstrained fn __field_less_than(x: Field, y: Field) -> bool {}

pub(crate) unconstrained fn field_less_than(x: Field, y: Field) -> bool {
__field_less_than(x, y)
}

// Convert a 32 byte array to a field element by modding
pub fn bytes32_to_field(bytes32: [u8; 32]) -> Field {
// Convert it to a field element
Expand All @@ -228,25 +236,33 @@ pub fn bytes32_to_field(bytes32: [u8; 32]) -> Field {
}

fn lt_fallback(x: Field, y: Field) -> bool {
let x_bytes: [u8; 32] = x.to_le_bytes();
let y_bytes: [u8; 32] = y.to_le_bytes();
let mut x_is_lt = false;
let mut done = false;
for i in 0..32 {
if (!done) {
let x_byte = x_bytes[32 - 1 - i] as u8;
let y_byte = y_bytes[32 - 1 - i] as u8;
let bytes_match = x_byte == y_byte;
if !bytes_match {
x_is_lt = x_byte < y_byte;
done = true;
if is_unconstrained() {
unsafe {
field_less_than(x, y)
}
} else {
let x_bytes: [u8; 32] = x.to_le_bytes();
let y_bytes: [u8; 32] = y.to_le_bytes();
let mut x_is_lt = false;
let mut done = false;
for i in 0..32 {
if (!done) {
let x_byte = x_bytes[32 - 1 - i] as u8;
let y_byte = y_bytes[32 - 1 - i] as u8;
let bytes_match = x_byte == y_byte;
if !bytes_match {
x_is_lt = x_byte < y_byte;
done = true;
}
}
}
x_is_lt
}
x_is_lt
}

mod tests {
use super::field_less_than;

#[test]
// docs:start:to_be_bits_example
fn test_to_be_bits() {
Expand Down Expand Up @@ -304,4 +320,12 @@ mod tests {
assert_eq(Field::from_le_bytes::<8>(bits), field);
}
// docs:end:to_le_radix_example

#[test]
unconstrained fn test_field_less_than() {
assert(field_less_than(0, 1));
assert(field_less_than(0, 0x100));
assert(field_less_than(0x100, 0 - 1));
assert(!field_less_than(0 - 1, 0));
}
}

0 comments on commit e50303d

Please sign in to comment.