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

feat: Add intrinsic to get if running inside an unconstrained context #5098

Merged
merged 9 commits into from
May 24, 2024
Merged
Show file tree
Hide file tree
Changes from 2 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
1 change: 1 addition & 0 deletions compiler/noirc_evaluator/src/ssa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ pub(crate) fn optimize_into_acir(
.run_pass(Ssa::defunctionalize, "After Defunctionalization:")
.run_pass(Ssa::remove_paired_rc, "After Removing Paired rc_inc & rc_decs:")
.run_pass(Ssa::inline_functions, "After Inlining:")
.run_pass(Ssa::resolve_within_unconstrained, "After Resolving WithinUnconstrained:")
// Run mem2reg with the CFG separated into blocks
.run_pass(Ssa::mem2reg, "After Mem2Reg:")
.run_pass(Ssa::as_slice_optimization, "After `as_slice` optimization")
Expand Down
6 changes: 5 additions & 1 deletion compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ pub(crate) enum Intrinsic {
FromField,
AsField,
AsWitness,
WithinUnconstrained,
}

impl std::fmt::Display for Intrinsic {
Expand All @@ -89,6 +90,7 @@ impl std::fmt::Display for Intrinsic {
Intrinsic::FromField => write!(f, "from_field"),
Intrinsic::AsField => write!(f, "as_field"),
Intrinsic::AsWitness => write!(f, "as_witness"),
Intrinsic::WithinUnconstrained => write!(f, "within_unconstrained"),
}
}
}
Expand Down Expand Up @@ -116,7 +118,8 @@ impl Intrinsic {
| Intrinsic::SliceRemove
| Intrinsic::StrAsBytes
| Intrinsic::FromField
| Intrinsic::AsField => false,
| Intrinsic::AsField
| Intrinsic::WithinUnconstrained => false,

// Some black box functions have side-effects
Intrinsic::BlackBox(func) => matches!(func, BlackBoxFunc::RecursiveAggregation),
Expand Down Expand Up @@ -145,6 +148,7 @@ impl Intrinsic {
"from_field" => Some(Intrinsic::FromField),
"as_field" => Some(Intrinsic::AsField),
"as_witness" => Some(Intrinsic::AsWitness),
"within_unconstrained" => Some(Intrinsic::WithinUnconstrained),
other => BlackBoxFunc::lookup(other).map(Intrinsic::BlackBox),
}
}
Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,7 @@ pub(super) fn simplify_call(
SimplifyResult::SimplifiedToInstruction(instruction)
}
Intrinsic::AsWitness => SimplifyResult::None,
Intrinsic::WithinUnconstrained => SimplifyResult::None,
}
}

Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_evaluator/src/ssa/opt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,6 @@ mod rc;
mod remove_bit_shifts;
mod remove_enable_side_effects;
mod remove_if_else;
mod resolve_within_unconstrained;
mod simplify_cfg;
mod unrolling;
Original file line number Diff line number Diff line change
Expand Up @@ -158,7 +158,8 @@ impl Context {
| Intrinsic::FromField
| Intrinsic::AsField
| Intrinsic::AsSlice
| Intrinsic::AsWitness => false,
| Intrinsic::AsWitness
| Intrinsic::WithinUnconstrained => false,
},

// We must assume that functions contain a side effect as we cannot inspect more deeply.
Expand Down
3 changes: 2 additions & 1 deletion compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,7 @@ fn slice_capacity_change(
| Intrinsic::BlackBox(_)
| Intrinsic::FromField
| Intrinsic::AsField
| Intrinsic::AsWitness => SizeChange::None,
| Intrinsic::AsWitness
| Intrinsic::WithinUnconstrained => SizeChange::None,
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
use crate::ssa::{
ir::{
function::{Function, RuntimeType},
instruction::{Instruction, Intrinsic},
types::Type,
value::Value,
},
ssa_gen::Ssa,
};
use acvm::FieldElement;
use fxhash::FxHashSet as HashSet;

impl Ssa {
/// An SSA pass to find any calls to `Intrinsic::WithinUnconstrained` and replacing any uses of the result of the intrinsic
/// with the resoled boolean value.
sirasistant marked this conversation as resolved.
Show resolved Hide resolved
/// Note that this pass must run after the pass that does runtime separation, since in SSA generation an ACIR function can end up targeting brillig.
#[tracing::instrument(level = "trace", skip(self))]
pub(crate) fn resolve_within_unconstrained(mut self) -> Self {
for func in self.functions.values_mut() {
replace_within_unconstrained_result(func);
}
self
}
}

fn replace_within_unconstrained_result(func: &mut Function) {
let mut within_unconstrained_calls = HashSet::default();
// Collect all calls to within_unconstrained
for block_id in func.reachable_blocks() {
for &instruction_id in func.dfg[block_id].instructions() {
let target_func = match &func.dfg[instruction_id] {
Instruction::Call { func, .. } => *func,
_ => continue,
};

if let Value::Intrinsic(Intrinsic::WithinUnconstrained) = &func.dfg[target_func] {
within_unconstrained_calls.insert(instruction_id);
}
}
}

for instruction_id in within_unconstrained_calls {
let call_returns = func.dfg.instruction_results(instruction_id);
let original_return_id = call_returns[0];

// We replace the result with a fresh id. This will be unused, so the DIE pass will remove the leftover intrinsic call.
func.dfg.replace_result(instruction_id, original_return_id);

let is_within_unconstrained = func.dfg.make_constant(
FieldElement::from(matches!(func.runtime(), RuntimeType::Brillig)),
Type::bool(),
);
// Replace all uses of the original return value with the constant
func.dfg.set_value_from_id(original_return_id, is_within_unconstrained);
}
}
139 changes: 92 additions & 47 deletions noir_stdlib/src/field/bn254.nr
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
use crate::within_unconstrained;

// The low and high decomposition of the field modulus
global PLO: Field = 53438638232309528389504892708671455233;
global PHI: Field = 64323764613183177041862057485226039389;

global TWO_POW_128: Field = 0x100000000000000000000000000000000;

/// A hint for decomposing a single field into two 16 byte fields.
unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) {
// Decomposes a single field into two 16 byte fields.
fn compute_decomposition(x: Field) -> (Field, Field) {
let x_bytes = x.to_le_bytes(32);

let mut low: Field = 0;
Expand All @@ -21,11 +23,15 @@ unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) {
(low, high)
}

unconstrained fn decompose_hint(x: Field) -> (Field, Field) {
compute_decomposition(x)
}

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

let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
let rhi = ahi - bhi - (borrow as Field);
Expand All @@ -34,10 +40,9 @@ fn assert_gt_limbs(a: (Field, Field), b: (Field, Field)) {
rhi.assert_max_bit_size(128);
}

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

// Range check the limbs
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
xlo.assert_max_bit_size(128);
Expand All @@ -51,7 +56,7 @@ pub fn decompose(x: Field) -> (Field, Field) {
(xlo, xhi)
}

fn lt_unsafe_internal(x: Field, y: Field, num_bytes: u32) -> bool {
fn compute_lt(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;
Expand All @@ -70,44 +75,66 @@ fn lt_unsafe_internal(x: Field, y: Field, num_bytes: u32) -> bool {
x_is_lt
}

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

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

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

pub fn assert_gt(a: Field, b: Field) {
fn assert_gt_circuit_optimized(a: Field, b: Field) {
// Decompose a and b
let a_limbs = decompose(a);
let b_limbs = decompose(b);
let a_limbs = decompose_circuit_optimized(a);
let b_limbs = decompose_circuit_optimized(b);

// Assert that a_limbs is greater than b_limbs
assert_gt_limbs(a_limbs, b_limbs)
}

/// Decompose a single field into two 16 byte fields.
pub fn decompose(x: Field) -> (Field, Field) {
if within_unconstrained() {
compute_decomposition(x)
} else {
decompose_circuit_optimized(x)
}
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
}

pub fn assert_gt(a: Field, b: Field) {
if within_unconstrained() {
assert(compute_lt(b, a, 32));
} else {
assert_gt_circuit_optimized(a, b);
}
}

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_32(a, b) {
assert_gt(b, a);
if within_unconstrained() {
compute_lt(b, a, 32)
} else if a == b {
false
} else {
assert_gt(a, b);
true
} else {
// Take a hint of the comparison and verify it
if lt_32_hint(a, b) {
assert_gt(b, a);
false
} else {
assert_gt(a, b);
true
}
}
}

Expand All @@ -117,44 +144,41 @@ pub fn lt(a: Field, b: Field) -> bool {

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

#[test]
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));
}

#[test]
fn check_decompose() {
unconstrained fn check_decompose_unconstrained() {
assert_eq(decompose(TWO_POW_128), (0, 1));
assert_eq(decompose(TWO_POW_128 + 0x1234567890), (0x1234567890, 1));
assert_eq(decompose(0x1234567890), (0x1234567890, 0));
}

#[test]
fn check_lt_unsafe() {
assert(lt_unsafe_internal(0, 1, 16));
assert(lt_unsafe_internal(0, 0x100, 16));
assert(lt_unsafe_internal(0x100, TWO_POW_128 - 1, 16));
assert(!lt_unsafe_internal(0, TWO_POW_128, 16));
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_lte_unsafe() {
assert(lte_unsafe_internal(0, 1, 16));
assert(lte_unsafe_internal(0, 0x100, 16));
assert(lte_unsafe_internal(0x100, TWO_POW_128 - 1, 16));
assert(!lte_unsafe_internal(0, TWO_POW_128, 16));

assert(lte_unsafe_internal(0, 0, 16));
assert(lte_unsafe_internal(0x100, 0x100, 16));
assert(lte_unsafe_internal(TWO_POW_128 - 1, TWO_POW_128 - 1, 16));
assert(lte_unsafe_internal(TWO_POW_128, TWO_POW_128, 16));
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));
}

#[test]
Expand All @@ -166,6 +190,15 @@ mod tests {
assert_gt(0 - 1, 0);
}

#[test]
unconstrained fn check_assert_gt_unconstrained() {
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);
}
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved

#[test]
fn check_gt() {
assert(gt(1, 0));
Expand All @@ -178,6 +211,18 @@ mod tests {
assert(!gt(0 - 2, 0 - 1));
}

#[test]
unconstrained fn check_gt_unconstrained() {
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));
}

#[test]
fn check_plo_phi() {
assert_eq(PLO + PHI * TWO_POW_128, 0);
Expand Down
3 changes: 3 additions & 0 deletions noir_stdlib/src/lib.nr
Original file line number Diff line number Diff line change
Expand Up @@ -70,3 +70,6 @@ pub fn wrapping_mul<T>(x: T, y: T) -> T {

#[builtin(as_witness)]
pub fn as_witness(x: Field) {}

#[builtin(within_unconstrained)]
pub fn within_unconstrained() -> bool {}
sirasistant marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "within_unconstrained"
type = "bin"
authors = [""]

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@

Loading
Loading