From c7df823b1ce66605f7e9c26f4471f1b8ccb15f17 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Thu, 23 May 2024 13:40:41 +0000 Subject: [PATCH 1/9] feat: within unconstrained --- compiler/noirc_evaluator/src/ssa.rs | 1 + .../noirc_evaluator/src/ssa/ir/instruction.rs | 6 +- .../src/ssa/ir/instruction/call.rs | 1 + compiler/noirc_evaluator/src/ssa/opt/mod.rs | 1 + .../src/ssa/opt/remove_enable_side_effects.rs | 3 +- .../src/ssa/opt/remove_if_else.rs | 3 +- .../ssa/opt/resolve_within_unconstrained.rs | 55 +++++++ noir_stdlib/src/field/bn254.nr | 139 ++++++++++++------ noir_stdlib/src/lib.nr | 3 + .../within_unconstrained/Nargo.toml | 6 + .../within_unconstrained/Prover.toml | 1 + .../within_unconstrained/src/main.nr | 14 ++ tooling/debugger/ignored-tests.txt | 1 + 13 files changed, 184 insertions(+), 50 deletions(-) create mode 100644 compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs create mode 100644 test_programs/execution_success/within_unconstrained/Nargo.toml create mode 100644 test_programs/execution_success/within_unconstrained/Prover.toml create mode 100644 test_programs/execution_success/within_unconstrained/src/main.nr diff --git a/compiler/noirc_evaluator/src/ssa.rs b/compiler/noirc_evaluator/src/ssa.rs index 69e5f6ddfcc..751da93169b 100644 --- a/compiler/noirc_evaluator/src/ssa.rs +++ b/compiler/noirc_evaluator/src/ssa.rs @@ -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") diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index f136d3c5fb2..6e6e099c56d 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -65,6 +65,7 @@ pub(crate) enum Intrinsic { FromField, AsField, AsWitness, + WithinUnconstrained, } 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::WithinUnconstrained => write!(f, "within_unconstrained"), } } } @@ -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), @@ -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), } } diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs index 8e320de9337..6282c3ccd8b 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs @@ -294,6 +294,7 @@ pub(super) fn simplify_call( SimplifyResult::SimplifiedToInstruction(instruction) } Intrinsic::AsWitness => SimplifyResult::None, + Intrinsic::WithinUnconstrained => SimplifyResult::None, } } diff --git a/compiler/noirc_evaluator/src/ssa/opt/mod.rs b/compiler/noirc_evaluator/src/ssa/opt/mod.rs index 27536d59ea5..53c1de8ecd8 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/mod.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/mod.rs @@ -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; diff --git a/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs b/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs index 9309652d508..f560f852e81 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs @@ -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. diff --git a/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs b/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs index 3d2b5142219..035d6d72df2 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs @@ -232,6 +232,7 @@ fn slice_capacity_change( | Intrinsic::BlackBox(_) | Intrinsic::FromField | Intrinsic::AsField - | Intrinsic::AsWitness => SizeChange::None, + | Intrinsic::AsWitness + | Intrinsic::WithinUnconstrained => SizeChange::None, } } diff --git a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs new file mode 100644 index 00000000000..bc0bf74a105 --- /dev/null +++ b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs @@ -0,0 +1,55 @@ +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 { + /// A simple SSA pass to find any calls to `Intrinsic::WithinUnconstrained` and replacing any references to the result of the intrinsic + /// with the correct 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_within_unconstrained(mut self) -> Self { + for func in self.functions.values_mut() { + replace_within_unconstrained(func); + } + self + } +} + +fn replace_within_unconstrained(func: &mut Function) { + let mut within_unconstrained_calls = HashSet::default(); + 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, + }; + + match &func.dfg[target_func] { + Value::Intrinsic(Intrinsic::WithinUnconstrained) => { + within_unconstrained_calls.insert(instruction_id); + } + _ => continue, + }; + } + } + + for instruction_id in within_unconstrained_calls { + let call_returns = func.dfg.instruction_results(instruction_id); + let original_return_id = call_returns[0]; + + func.dfg.replace_result(instruction_id, original_return_id); + let known_value = func.dfg.make_constant( + FieldElement::from(matches!(func.runtime(), RuntimeType::Brillig)), + Type::bool(), + ); + func.dfg.set_value_from_id(original_return_id, known_value); + } +} diff --git a/noir_stdlib/src/field/bn254.nr b/noir_stdlib/src/field/bn254.nr index 2e82d9e7c23..2b80bbb3473 100644 --- a/noir_stdlib/src/field/bn254.nr +++ b/noir_stdlib/src/field/bn254.nr @@ -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; @@ -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); @@ -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 xlo.assert_max_bit_size(128); @@ -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; @@ -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) + } +} + +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 + } } } @@ -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] @@ -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); + } + #[test] fn check_gt() { assert(gt(1, 0)); @@ -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); diff --git a/noir_stdlib/src/lib.nr b/noir_stdlib/src/lib.nr index f11b21003ad..99f2e1062bd 100644 --- a/noir_stdlib/src/lib.nr +++ b/noir_stdlib/src/lib.nr @@ -70,3 +70,6 @@ pub fn wrapping_mul(x: T, y: T) -> T { #[builtin(as_witness)] pub fn as_witness(x: Field) {} + +#[builtin(within_unconstrained)] +pub fn within_unconstrained() -> bool {} diff --git a/test_programs/execution_success/within_unconstrained/Nargo.toml b/test_programs/execution_success/within_unconstrained/Nargo.toml new file mode 100644 index 00000000000..61f5323895d --- /dev/null +++ b/test_programs/execution_success/within_unconstrained/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "within_unconstrained" +type = "bin" +authors = [""] + +[dependencies] diff --git a/test_programs/execution_success/within_unconstrained/Prover.toml b/test_programs/execution_success/within_unconstrained/Prover.toml new file mode 100644 index 00000000000..8b137891791 --- /dev/null +++ b/test_programs/execution_success/within_unconstrained/Prover.toml @@ -0,0 +1 @@ + diff --git a/test_programs/execution_success/within_unconstrained/src/main.nr b/test_programs/execution_success/within_unconstrained/src/main.nr new file mode 100644 index 00000000000..3dfdc775270 --- /dev/null +++ b/test_programs/execution_success/within_unconstrained/src/main.nr @@ -0,0 +1,14 @@ +use dep::std::within_unconstrained; + +fn check(should_be_unconstrained: bool) { + assert_eq(should_be_unconstrained, within_unconstrained()); +} + +unconstrained fn unconstrained_intermediate() { + check(true); +} + +fn main() { + unconstrained_intermediate(); + check(false); +} diff --git a/tooling/debugger/ignored-tests.txt b/tooling/debugger/ignored-tests.txt index cda26169421..4492fcf15c3 100644 --- a/tooling/debugger/ignored-tests.txt +++ b/tooling/debugger/ignored-tests.txt @@ -25,3 +25,4 @@ fold_fibonacci fold_complex_outputs slice_init_with_complex_type hashmap +within_unconstrained \ No newline at end of file From 6b65829b1a5aadefe7e4677b1a7334fe99da1988 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 08:23:55 +0000 Subject: [PATCH 2/9] docs --- .../ssa/opt/resolve_within_unconstrained.rs | 25 ++++++++++--------- 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs index bc0bf74a105..5871d0d6309 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs @@ -11,20 +11,21 @@ use acvm::FieldElement; use fxhash::FxHashSet as HashSet; impl Ssa { - /// A simple SSA pass to find any calls to `Intrinsic::WithinUnconstrained` and replacing any references to the result of the intrinsic - /// with the correct boolean value. + /// 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. /// 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(func); + replace_within_unconstrained_result(func); } self } } -fn replace_within_unconstrained(func: &mut Function) { +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] { @@ -32,12 +33,9 @@ fn replace_within_unconstrained(func: &mut Function) { _ => continue, }; - match &func.dfg[target_func] { - Value::Intrinsic(Intrinsic::WithinUnconstrained) => { - within_unconstrained_calls.insert(instruction_id); - } - _ => continue, - }; + if let Value::Intrinsic(Intrinsic::WithinUnconstrained) = &func.dfg[target_func] { + within_unconstrained_calls.insert(instruction_id); + } } } @@ -45,11 +43,14 @@ fn replace_within_unconstrained(func: &mut Function) { 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 known_value = func.dfg.make_constant( + + let is_within_unconstrained = func.dfg.make_constant( FieldElement::from(matches!(func.runtime(), RuntimeType::Brillig)), Type::bool(), ); - func.dfg.set_value_from_id(original_return_id, known_value); + // Replace all uses of the original return value with the constant + func.dfg.set_value_from_id(original_return_id, is_within_unconstrained); } } From 98057e14febdaa1054bafc6732e518edb8fe3e9a Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 11:10:50 +0000 Subject: [PATCH 3/9] refactor: remove explicit circuit optimized functions --- noir_stdlib/src/field/bn254.nr | 66 +++++++++++++++------------------- 1 file changed, 29 insertions(+), 37 deletions(-) diff --git a/noir_stdlib/src/field/bn254.nr b/noir_stdlib/src/field/bn254.nr index 2b80bbb3473..8889539fb00 100644 --- a/noir_stdlib/src/field/bn254.nr +++ b/noir_stdlib/src/field/bn254.nr @@ -27,35 +27,6 @@ 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_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); -} - -fn decompose_circuit_optimized(x: Field) -> (Field, Field) { - // 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) -} - 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); @@ -91,13 +62,17 @@ unconstrained fn lte_16_hint(x: Field, y: Field) -> bool { compute_lte(x, y, 16) } -fn assert_gt_circuit_optimized(a: Field, b: Field) { - // Decompose a and b - let a_limbs = decompose_circuit_optimized(a); - let b_limbs = decompose_circuit_optimized(b); +// 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); - // Assert that a_limbs is greater than b_limbs - assert_gt_limbs(a_limbs, b_limbs) + rlo.assert_max_bit_size(128); + rhi.assert_max_bit_size(128); } /// Decompose a single field into two 16 byte fields. @@ -105,7 +80,19 @@ pub fn decompose(x: Field) -> (Field, Field) { if within_unconstrained() { compute_decomposition(x) } else { - decompose_circuit_optimized(x) + // 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) } } @@ -113,7 +100,12 @@ pub fn assert_gt(a: Field, b: Field) { if within_unconstrained() { assert(compute_lt(b, a, 32)); } else { - assert_gt_circuit_optimized(a, b); + // 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) } } From c6bfa6d48a3fa3ffaa4cc229cc6c4e4fb804d9b5 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 11:20:15 +0000 Subject: [PATCH 4/9] refactor: move within unconstrained to a runtime mod --- noir_stdlib/src/field/bn254.nr | 8 ++++---- noir_stdlib/src/lib.nr | 3 +-- noir_stdlib/src/runtime.nr | 2 ++ 3 files changed, 7 insertions(+), 6 deletions(-) create mode 100644 noir_stdlib/src/runtime.nr diff --git a/noir_stdlib/src/field/bn254.nr b/noir_stdlib/src/field/bn254.nr index 8889539fb00..bcdc23f80dc 100644 --- a/noir_stdlib/src/field/bn254.nr +++ b/noir_stdlib/src/field/bn254.nr @@ -1,4 +1,4 @@ -use crate::within_unconstrained; +use crate::runtime::is_unconstrained; // The low and high decomposition of the field modulus global PLO: Field = 53438638232309528389504892708671455233; @@ -77,7 +77,7 @@ fn assert_gt_limbs(a: (Field, Field), b: (Field, Field)) { /// Decompose a single field into two 16 byte fields. pub fn decompose(x: Field) -> (Field, Field) { - if within_unconstrained() { + if is_unconstrained() { compute_decomposition(x) } else { // Take hints of the decomposition @@ -97,7 +97,7 @@ pub fn decompose(x: Field) -> (Field, Field) { } pub fn assert_gt(a: Field, b: Field) { - if within_unconstrained() { + if is_unconstrained() { assert(compute_lt(b, a, 32)); } else { // Decompose a and b @@ -114,7 +114,7 @@ pub fn assert_lt(a: Field, b: Field) { } pub fn gt(a: Field, b: Field) -> bool { - if within_unconstrained() { + if is_unconstrained() { compute_lt(b, a, 32) } else if a == b { false diff --git a/noir_stdlib/src/lib.nr b/noir_stdlib/src/lib.nr index 99f2e1062bd..ad47171fa46 100644 --- a/noir_stdlib/src/lib.nr +++ b/noir_stdlib/src/lib.nr @@ -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 @@ -71,5 +72,3 @@ pub fn wrapping_mul(x: T, y: T) -> T { #[builtin(as_witness)] pub fn as_witness(x: Field) {} -#[builtin(within_unconstrained)] -pub fn within_unconstrained() -> bool {} diff --git a/noir_stdlib/src/runtime.nr b/noir_stdlib/src/runtime.nr new file mode 100644 index 00000000000..da231d197ac --- /dev/null +++ b/noir_stdlib/src/runtime.nr @@ -0,0 +1,2 @@ +#[builtin(within_unconstrained)] +pub fn is_unconstrained() -> bool {} From 5ed3f4970b6f668e399b2947d893475f3df3d51d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81lvaro=20Rodr=C3=ADguez?= Date: Fri, 24 May 2024 13:33:24 +0200 Subject: [PATCH 5/9] Update compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com> --- .../noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs index 5871d0d6309..d78f9828f74 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs @@ -12,7 +12,7 @@ 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. + /// 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_within_unconstrained(mut self) -> Self { From 6e2da762c5684f180d4783768c5add2de7ce7ea6 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 11:37:07 +0000 Subject: [PATCH 6/9] within_unconstrained => is_unconstrained --- compiler/noirc_evaluator/src/ssa.rs | 2 +- .../noirc_evaluator/src/ssa/ir/instruction.rs | 8 ++++---- .../src/ssa/ir/instruction/call.rs | 2 +- compiler/noirc_evaluator/src/ssa/opt/mod.rs | 2 +- .../src/ssa/opt/remove_enable_side_effects.rs | 2 +- .../src/ssa/opt/remove_if_else.rs | 2 +- ...onstrained.rs => resolve_is_unconstrained.rs} | 16 ++++++++-------- noir_stdlib/src/runtime.nr | 2 +- .../Nargo.toml | 2 +- .../Prover.toml | 0 .../src/main.nr | 4 ++-- tooling/debugger/ignored-tests.txt | 2 +- 12 files changed, 22 insertions(+), 22 deletions(-) rename compiler/noirc_evaluator/src/ssa/opt/{resolve_within_unconstrained.rs => resolve_is_unconstrained.rs} (76%) rename test_programs/execution_success/{within_unconstrained => is_unconstrained}/Nargo.toml (64%) rename test_programs/execution_success/{within_unconstrained => is_unconstrained}/Prover.toml (100%) rename test_programs/execution_success/{within_unconstrained => is_unconstrained}/src/main.nr (64%) diff --git a/compiler/noirc_evaluator/src/ssa.rs b/compiler/noirc_evaluator/src/ssa.rs index 751da93169b..c2fe7878bf8 100644 --- a/compiler/noirc_evaluator/src/ssa.rs +++ b/compiler/noirc_evaluator/src/ssa.rs @@ -56,7 +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_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") diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs index 6e6e099c56d..93ea703721f 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction.rs @@ -65,7 +65,7 @@ pub(crate) enum Intrinsic { FromField, AsField, AsWitness, - WithinUnconstrained, + IsUnconstrained, } impl std::fmt::Display for Intrinsic { @@ -90,7 +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"), + Intrinsic::IsUnconstrained => write!(f, "is_unconstrained"), } } } @@ -119,7 +119,7 @@ impl Intrinsic { | Intrinsic::StrAsBytes | Intrinsic::FromField | Intrinsic::AsField - | Intrinsic::WithinUnconstrained => false, + | Intrinsic::IsUnconstrained => false, // Some black box functions have side-effects Intrinsic::BlackBox(func) => matches!(func, BlackBoxFunc::RecursiveAggregation), @@ -148,7 +148,7 @@ impl Intrinsic { "from_field" => Some(Intrinsic::FromField), "as_field" => Some(Intrinsic::AsField), "as_witness" => Some(Intrinsic::AsWitness), - "within_unconstrained" => Some(Intrinsic::WithinUnconstrained), + "is_unconstrained" => Some(Intrinsic::IsUnconstrained), other => BlackBoxFunc::lookup(other).map(Intrinsic::BlackBox), } } diff --git a/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs b/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs index 6282c3ccd8b..8f57d9de368 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs @@ -294,7 +294,7 @@ pub(super) fn simplify_call( SimplifyResult::SimplifiedToInstruction(instruction) } Intrinsic::AsWitness => SimplifyResult::None, - Intrinsic::WithinUnconstrained => SimplifyResult::None, + Intrinsic::IsUnconstrained => SimplifyResult::None, } } diff --git a/compiler/noirc_evaluator/src/ssa/opt/mod.rs b/compiler/noirc_evaluator/src/ssa/opt/mod.rs index 53c1de8ecd8..f6c3f022bfc 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/mod.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/mod.rs @@ -17,6 +17,6 @@ mod rc; mod remove_bit_shifts; mod remove_enable_side_effects; mod remove_if_else; -mod resolve_within_unconstrained; +mod resolve_is_unconstrained; mod simplify_cfg; mod unrolling; diff --git a/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs b/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs index f560f852e81..464faa57323 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/remove_enable_side_effects.rs @@ -159,7 +159,7 @@ impl Context { | Intrinsic::AsField | Intrinsic::AsSlice | Intrinsic::AsWitness - | Intrinsic::WithinUnconstrained => false, + | Intrinsic::IsUnconstrained => false, }, // We must assume that functions contain a side effect as we cannot inspect more deeply. diff --git a/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs b/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs index 035d6d72df2..91b455dbf29 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs @@ -233,6 +233,6 @@ fn slice_capacity_change( | Intrinsic::FromField | Intrinsic::AsField | Intrinsic::AsWitness - | Intrinsic::WithinUnconstrained => SizeChange::None, + | Intrinsic::IsUnconstrained => SizeChange::None, } } diff --git a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs b/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs similarity index 76% rename from compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs rename to compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs index d78f9828f74..0da3a628d5b 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/resolve_within_unconstrained.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs @@ -15,17 +15,17 @@ impl Ssa { /// 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_within_unconstrained(mut self) -> Self { + pub(crate) fn resolve_is_unconstrained(mut self) -> Self { for func in self.functions.values_mut() { - replace_within_unconstrained_result(func); + replace_is_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 +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] { @@ -33,13 +33,13 @@ fn replace_within_unconstrained_result(func: &mut Function) { _ => continue, }; - if let Value::Intrinsic(Intrinsic::WithinUnconstrained) = &func.dfg[target_func] { - within_unconstrained_calls.insert(instruction_id); + if let Value::Intrinsic(Intrinsic::IsUnconstrained) = &func.dfg[target_func] { + is_unconstrained_calls.insert(instruction_id); } } } - for instruction_id in within_unconstrained_calls { + for instruction_id in is_unconstrained_calls { let call_returns = func.dfg.instruction_results(instruction_id); let original_return_id = call_returns[0]; diff --git a/noir_stdlib/src/runtime.nr b/noir_stdlib/src/runtime.nr index da231d197ac..c075107cd52 100644 --- a/noir_stdlib/src/runtime.nr +++ b/noir_stdlib/src/runtime.nr @@ -1,2 +1,2 @@ -#[builtin(within_unconstrained)] +#[builtin(is_unconstrained)] pub fn is_unconstrained() -> bool {} diff --git a/test_programs/execution_success/within_unconstrained/Nargo.toml b/test_programs/execution_success/is_unconstrained/Nargo.toml similarity index 64% rename from test_programs/execution_success/within_unconstrained/Nargo.toml rename to test_programs/execution_success/is_unconstrained/Nargo.toml index 61f5323895d..deef68c7f72 100644 --- a/test_programs/execution_success/within_unconstrained/Nargo.toml +++ b/test_programs/execution_success/is_unconstrained/Nargo.toml @@ -1,5 +1,5 @@ [package] -name = "within_unconstrained" +name = "is_unconstrained" type = "bin" authors = [""] diff --git a/test_programs/execution_success/within_unconstrained/Prover.toml b/test_programs/execution_success/is_unconstrained/Prover.toml similarity index 100% rename from test_programs/execution_success/within_unconstrained/Prover.toml rename to test_programs/execution_success/is_unconstrained/Prover.toml diff --git a/test_programs/execution_success/within_unconstrained/src/main.nr b/test_programs/execution_success/is_unconstrained/src/main.nr similarity index 64% rename from test_programs/execution_success/within_unconstrained/src/main.nr rename to test_programs/execution_success/is_unconstrained/src/main.nr index 3dfdc775270..af40af1029f 100644 --- a/test_programs/execution_success/within_unconstrained/src/main.nr +++ b/test_programs/execution_success/is_unconstrained/src/main.nr @@ -1,7 +1,7 @@ -use dep::std::within_unconstrained; +use dep::std::runtime::is_unconstrained; fn check(should_be_unconstrained: bool) { - assert_eq(should_be_unconstrained, within_unconstrained()); + assert_eq(should_be_unconstrained, is_unconstrained()); } unconstrained fn unconstrained_intermediate() { diff --git a/tooling/debugger/ignored-tests.txt b/tooling/debugger/ignored-tests.txt index 4492fcf15c3..a6d3c9a3a94 100644 --- a/tooling/debugger/ignored-tests.txt +++ b/tooling/debugger/ignored-tests.txt @@ -25,4 +25,4 @@ fold_fibonacci fold_complex_outputs slice_init_with_complex_type hashmap -within_unconstrained \ No newline at end of file +is_unconstrained \ No newline at end of file From c69f170925cc3fcf598d0760645fa8f90269ded3 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 11:38:19 +0000 Subject: [PATCH 7/9] fix comment --- .../noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs b/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs index 0da3a628d5b..2c9e33ae528 100644 --- a/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs +++ b/compiler/noirc_evaluator/src/ssa/opt/resolve_is_unconstrained.rs @@ -11,7 +11,7 @@ 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 + /// 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))] From 979bf257212cc2d91d8ec10254571a17a85a816c Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 15:09:47 +0200 Subject: [PATCH 8/9] added docs page --- .../noir/standard_library/is_unconstrained.md | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 docs/docs/noir/standard_library/is_unconstrained.md diff --git a/docs/docs/noir/standard_library/is_unconstrained.md b/docs/docs/noir/standard_library/is_unconstrained.md new file mode 100644 index 00000000000..284e5b35d04 --- /dev/null +++ b/docs/docs/noir/standard_library/is_unconstrained.md @@ -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. \ No newline at end of file From 0043db372ef5a2bf65eb662066c804721b4f73f2 Mon Sep 17 00:00:00 2001 From: sirasistant Date: Fri, 24 May 2024 15:11:12 +0200 Subject: [PATCH 9/9] typo --- docs/docs/noir/standard_library/is_unconstrained.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/docs/noir/standard_library/is_unconstrained.md b/docs/docs/noir/standard_library/is_unconstrained.md index 284e5b35d04..bb157e719dc 100644 --- a/docs/docs/noir/standard_library/is_unconstrained.md +++ b/docs/docs/noir/standard_library/is_unconstrained.md @@ -10,7 +10,7 @@ keywords: 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: +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