Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore!: use Brillig opcode when possible for less-than operations on fields #9416

Merged
merged 3 commits into from
Oct 28, 2024
Merged
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
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));
}
}
Loading