Skip to content

Commit

Permalink
feat: Add intrinsic to get if running inside an unconstrained context (
Browse files Browse the repository at this point in the history
…#5098)

# Description

## Problem\*

Currently, when creating a regular (not marked with unconstrained)
function, it can end up running in both a constrained and unconstrained
context.

## Summary\*

This intrinsic is resolved at compile time a provides a way for
developers to dispatch to different implementations in library code for
constrained and unconstrained context. This intrinsic has been used in
stdlib's field comparison code as demonstration.

## Additional Context

It's very typical for the constrained version of a calculation to take a
hint of a computed value and verify it. However, in the unconstrained
version of that calculation we just need to compute the value, there is
no point in verifying what we just did. This intrinsic provides a tool
for devs to optimize a function for unconstrained removing these
verifications.

## Documentation\*

Check one:
- [ ] No documentation needed.
- [x] Documentation included in this PR.
- [ ] **[For Experimental Features]** 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.

---------

Co-authored-by: Tom French <[email protected]>
sirasistant and TomAFrench authored May 24, 2024
1 parent 86fd0ac commit 281ebf2
Showing 15 changed files with 263 additions and 76 deletions.
1 change: 1 addition & 0 deletions compiler/noirc_evaluator/src/ssa.rs
Original file line number Diff line number Diff line change
@@ -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_is_unconstrained, "After Resolving IsUnconstrained:")
// Run mem2reg with the CFG separated into blocks
.run_pass(Ssa::mem2reg, "After Mem2Reg:")
.run_pass(Ssa::as_slice_optimization, "After `as_slice` optimization")
6 changes: 5 additions & 1 deletion compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
@@ -65,6 +65,7 @@ pub(crate) enum Intrinsic {
FromField,
AsField,
AsWitness,
IsUnconstrained,
}

impl std::fmt::Display for Intrinsic {
@@ -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::IsUnconstrained => write!(f, "is_unconstrained"),
}
}
}
@@ -116,7 +118,8 @@ impl Intrinsic {
| Intrinsic::SliceRemove
| Intrinsic::StrAsBytes
| Intrinsic::FromField
| Intrinsic::AsField => false,
| Intrinsic::AsField
| Intrinsic::IsUnconstrained => false,

// Some black box functions have side-effects
Intrinsic::BlackBox(func) => matches!(func, BlackBoxFunc::RecursiveAggregation),
@@ -145,6 +148,7 @@ impl Intrinsic {
"from_field" => Some(Intrinsic::FromField),
"as_field" => Some(Intrinsic::AsField),
"as_witness" => Some(Intrinsic::AsWitness),
"is_unconstrained" => Some(Intrinsic::IsUnconstrained),
other => BlackBoxFunc::lookup(other).map(Intrinsic::BlackBox),
}
}
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
@@ -294,6 +294,7 @@ pub(super) fn simplify_call(
SimplifyResult::SimplifiedToInstruction(instruction)
}
Intrinsic::AsWitness => SimplifyResult::None,
Intrinsic::IsUnconstrained => SimplifyResult::None,
}
}

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

// We must assume that functions contain a side effect as we cannot inspect more deeply.
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
@@ -232,6 +232,7 @@ fn slice_capacity_change(
| Intrinsic::BlackBox(_)
| Intrinsic::FromField
| Intrinsic::AsField
| Intrinsic::AsWitness => SizeChange::None,
| Intrinsic::AsWitness
| Intrinsic::IsUnconstrained => SizeChange::None,
}
}
56 changes: 56 additions & 0 deletions compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs
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::IsUnconstrained` and replacing any uses of the result of the intrinsic
/// with the resolved boolean value.
/// 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_is_unconstrained(mut self) -> Self {
for func in self.functions.values_mut() {
replace_is_unconstrained_result(func);
}
self
}
}

fn replace_is_unconstrained_result(func: &mut Function) {
let mut is_unconstrained_calls = HashSet::default();
// Collect all calls to is_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::IsUnconstrained) = &func.dfg[target_func] {
is_unconstrained_calls.insert(instruction_id);
}
}
}

for instruction_id in is_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);
}
}
59 changes: 59 additions & 0 deletions docs/docs/noir/standard_library/is_unconstrained.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
---
title: Is Unconstrained Function
description:
The is_unconstrained function returns wether the context at that point of the program is unconstrained or not.
keywords:
[
unconstrained
]
---

It's very common for functions in circuits to take unconstrained hints of an expensive computation and then verify it. This is done by running the hint in an unconstrained context and then verifying the result in a constrained context.

When a function is marked as unconstrained, any subsequent functions that it calls will also be run in an unconstrained context. However, if we are implementing a library function, other users might call it within an unconstrained context or a constrained one. Generally, in an unconstrained context we prefer just computing the result instead of taking a hint of it and verifying it, since that'd mean doing the same computation twice:

```rust

fn my_expensive_computation(){
...
}

unconstrained fn my_expensive_computation_hint(){
my_expensive_computation()
}

pub fn external_interface(){
my_expensive_computation_hint();
// verify my_expensive_computation: If external_interface is called from unconstrained, this is redundant
...
}

```

In order to improve the performance in an unconstrained context you can use the function at `std::runtime::is_unconstrained() -> bool`:


```rust
use dep::std::runtime::is_unconstrained;

fn my_expensive_computation(){
...
}

unconstrained fn my_expensive_computation_hint(){
my_expensive_computation()
}

pub fn external_interface(){
if is_unconstrained() {
my_expensive_computation();
} else {
my_expensive_computation_hint();
// verify my_expensive_computation
...
}
}

```

The is_unconstrained result is resolved at compile time, so in unconstrained contexts the compiler removes the else branch, and in constrained contexts the compiler removes the if branch, reducing the amount of compute necessary to run external_interface.
183 changes: 110 additions & 73 deletions noir_stdlib/src/field/bn254.nr
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
use crate::runtime::is_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;
@@ -21,37 +23,11 @@ unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) {
(low, high)
}

// 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 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);
}

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

// Range check the limbs
xlo.assert_max_bit_size(128);
xhi.assert_max_bit_size(128);

// Check that the decomposition is correct
assert_eq(x, xlo + TWO_POW_128 * xhi);

// Assert that the decomposition of P is greater than the decomposition of x
assert_gt_limbs((PLO, PHI), (xlo, xhi));
(xlo, xhi)
unconstrained fn decompose_hint(x: Field) -> (Field, Field) {
compute_decomposition(x)
}

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;
@@ -70,44 +46,87 @@ 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)
}

// 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_16_hint(alo, blo);

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);
}

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

// Range check the limbs
xlo.assert_max_bit_size(128);
xhi.assert_max_bit_size(128);

// Check that the decomposition is correct
assert_eq(x, xlo + TWO_POW_128 * xhi);

// Assert that the decomposition of P is greater than the decomposition of x
assert_gt_limbs((PLO, PHI), (xlo, xhi));
(xlo, xhi)
}
}

pub fn assert_gt(a: Field, b: Field) {
// Decompose a and b
let a_limbs = decompose(a);
let b_limbs = decompose(b);
if is_unconstrained() {
assert(compute_lt(b, a, 32));
} else {
// Decompose a and b
let a_limbs = decompose(a);
let b_limbs = decompose(b);

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

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 is_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
}
}
}

@@ -117,44 +136,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]
@@ -166,6 +182,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);
}

#[test]
fn check_gt() {
assert(gt(1, 0));
@@ -178,6 +203,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);
2 changes: 2 additions & 0 deletions noir_stdlib/src/lib.nr
Original file line number Diff line number Diff line change
@@ -25,6 +25,7 @@ mod default;
mod prelude;
mod uint128;
mod bigint;
mod runtime;

// Oracle calls are required to be wrapped in an unconstrained function
// Thus, the only argument to the `println` oracle is expected to always be an ident
@@ -70,3 +71,4 @@ pub fn wrapping_mul<T>(x: T, y: T) -> T {

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

2 changes: 2 additions & 0 deletions noir_stdlib/src/runtime.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#[builtin(is_unconstrained)]
pub fn is_unconstrained() -> bool {}
6 changes: 6 additions & 0 deletions test_programs/execution_success/is_unconstrained/Nargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "is_unconstrained"
type = "bin"
authors = [""]

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

14 changes: 14 additions & 0 deletions test_programs/execution_success/is_unconstrained/src/main.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
use dep::std::runtime::is_unconstrained;

fn check(should_be_unconstrained: bool) {
assert_eq(should_be_unconstrained, is_unconstrained());
}

unconstrained fn unconstrained_intermediate() {
check(true);
}

fn main() {
unconstrained_intermediate();
check(false);
}
1 change: 1 addition & 0 deletions tooling/debugger/ignored-tests.txt
Original file line number Diff line number Diff line change
@@ -25,3 +25,4 @@ fold_fibonacci
fold_complex_outputs
slice_init_with_complex_type
hashmap
is_unconstrained

0 comments on commit 281ebf2

Please sign in to comment.