test within unconstrained

noir/noir-repo/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")

noir/noir-repo/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),
         }
     }

noir/noir-repo/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,
     }
 }
 

noir/noir-repo/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;

noir/noir-repo/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.

noir/noir-repo/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,
     }
 }

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

noir/noir-repo/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 decompose_internal(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) {
+    decompose_internal(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 lt_internal(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 lte_internal(x: Field, y: Field, num_bytes: u32) -> bool {
     if x == y {
         true
     } else {
-        lt_unsafe_internal(x, y, num_bytes)
+        lt_internal(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 {
+    lt_internal(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 {
+    lte_internal(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() {
+        decompose_internal(x)
+    } else {
+        decompose_circuit_optimized(x)
+    }
+}
+
+pub fn assert_gt(a: Field, b: Field) {
+    if within_unconstrained() {
+        assert(lt_internal(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() {
+        lt_internal(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, lt_internal, assert_gt, gt, lt, TWO_POW_128, lte_internal, 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_lt_internal() {
+        assert(lt_internal(0, 1, 16));
+        assert(lt_internal(0, 0x100, 16));
+        assert(lt_internal(0x100, TWO_POW_128 - 1, 16));
+        assert(!lt_internal(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_lte_internal() {
+        assert(lte_internal(0, 1, 16));
+        assert(lte_internal(0, 0x100, 16));
+        assert(lte_internal(0x100, TWO_POW_128 - 1, 16));
+        assert(!lte_internal(0, TWO_POW_128, 16));
+
+        assert(lte_internal(0, 0, 16));
+        assert(lte_internal(0x100, 0x100, 16));
+        assert(lte_internal(TWO_POW_128 - 1, TWO_POW_128 - 1, 16));
+        assert(lte_internal(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);

noir/noir-repo/noir_stdlib/src/lib.nr

@@ -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 {}