Skip to content
Open
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
119 changes: 115 additions & 4 deletions compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,13 @@
//! multiplication (or an equivalent `IfElse` merge, which gates each branch by
//! its own condition).
//!
//! One escape is deliberate and allowed: calls to `no_predicates` functions.
//! Flattening wraps them in `enable_side_effects u1 1` so the callee runs
//! unpredicated, which means a predicated argument reaches the call without a

Check warning on line 29 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (unpredicated)
//! guard. That is safe — the callee cannot be over-constrained by a
//! disabled-branch value — but its results are arbitrary on the disabled
//! branch, so they inherit the argument's predicate and stay tracked.
//!
//! As a result, any optimization on `requires_acir_gen_predicate` done after
//! flattening is ensured to be sound.
//!
Expand All @@ -44,7 +51,7 @@
ir::{
basic_block::BasicBlockId,
dfg::DataFlowGraph,
function::Function,
function::{Function, FunctionId},
instruction::{Binary, BinaryOp, Instruction, TerminatorInstruction},
types::Type,
value::{Value, ValueId},
Expand All @@ -53,13 +60,15 @@
};

pub(crate) fn verify_side_effect_predicates(ssa: &Ssa) -> RtResult<()> {
let no_predicates: HashSet<FunctionId> =
ssa.functions.values().filter(|f| f.is_no_predicates()).map(|f| f.id()).collect();
for function in ssa.functions.values() {
verify_function(function)?;
verify_function(function, &no_predicates)?;
}
Ok(())
}

fn verify_function(function: &Function) -> RtResult<()> {
fn verify_function(function: &Function, no_predicates: &HashSet<FunctionId>) -> RtResult<()> {
// Brillig functions do not have `enable_side_effects` instructions
if function.runtime().is_brillig() {
return Ok(());
Expand Down Expand Up @@ -101,6 +110,14 @@
continue;
}

// Flattening wraps a call to a `no_predicates` function in
// `enable_side_effects u1 1`, so a predicated value legitimately flows
// into the call ungated: the callee is run unpredicated by design, and

Check warning on line 115 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (unpredicated)

Check warning on line 115 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (ungated)
// consuming a disabled-branch value cannot over-constrain it. The
// call's results still inherit the operand's predicate below, so they
// stay tracked until guarded.
let consumes_ungated = is_call_to_no_predicates_function(dfg, instruction, no_predicates);

Check warning on line 119 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (ungated)

// Match instructions for
// - using predicated operands
// - using predicate operands outside enable-side-effect context
Expand All @@ -118,7 +135,7 @@
} else {
// Propagate the predicate to the current instruction
use_a_predicated_value.get_or_insert(p);
if current.is_none() {
if current.is_none() && !consumes_ungated {

Check warning on line 138 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (ungated)
// The `predicated_value` operand is not used under a predicate,
// flag it as an error.
violation.get_or_insert(operand);
Expand Down Expand Up @@ -213,7 +230,7 @@
}

/// Whether predicate `p` is `1` in every satisfying assignment, in which case a value
/// computed under it is never the disabled-branch value and may escape ungated.

Check warning on line 233 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (ungated)
///
/// This is what keeps the decomposition of a guarded assertion valid. `decompose_constrain`
/// rewrites a boolean `constrain (p * value) == 1` into `constrain p == 1` and
Expand Down Expand Up @@ -281,6 +298,25 @@
}
}

/// Whether `instruction` is a call to a `no_predicates` function.
///
/// Such calls run their callee unpredicated: flattening wraps them in

Check warning on line 303 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (unpredicated)
/// `enable_side_effects u1 1` and only restores the enclosing predicate
/// afterwards, so predicated arguments reach them without a guard.
fn is_call_to_no_predicates_function(
dfg: &DataFlowGraph,
instruction: &Instruction,
no_predicates: &HashSet<FunctionId>,
) -> bool {
let Instruction::Call { func, .. } = instruction else {
return false;
};
let Value::Function(id) = &dfg[*func] else {
return false;
};
no_predicates.contains(id)
}

/// True if `instruction` re-applies predicate `p` to `operand`, zeroing it
/// whenever `p` is false: `mul p, operand` (either order), or a branch of an
/// `IfElse` whose condition is `p` and whose value is `operand`. A merge gates
Expand Down Expand Up @@ -416,7 +452,7 @@
}

#[test]
fn rejects_ungated_escape_to_return() {

Check warning on line 455 in compiler/noirc_evaluator/src/ssa/validation/flatten_post_check.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (ungated)
// A checked add under `enable_side_effects v0`
// is returned directly, so its disabled-branch zeroing is observable.
let src = "
Expand Down Expand Up @@ -717,6 +753,81 @@
}
}

#[test]
fn accepts_tainted_argument_to_no_predicates_call() {
// Flattening wraps a call to a `no_predicates` function in
// `enable_side_effects u1 1` (running the callee unpredicated is the
// point of the attribute), so a value computed under a predicate
// legitimately reaches the call ungated. The result is arbitrary on
// the disabled branch and stays tainted — here it is guarded by
// `mul (cast v0), v5` before escaping, so nothing actually leaks.
let src = "
acir(inline) fn main f0 {
b0(v0: u1, v1: Field):
enable_side_effects v0
v2, v3 = call f1(v1) -> (Field, Field)
v4 = make_array [v2, v3] : [Field; 2]
enable_side_effects u1 1
v5 = call f2(v4) -> Field
v6 = cast v0 as Field
v7 = mul v6, v5
return v7
}
brillig(inline) fn get f1 {
b0(v0: Field):
return v0, v0
}
acir(no_predicates) fn hash f2 {
b0(v0: [Field; 2]):
v1 = array_get v0, index u32 0 -> Field
return v1
}
";
let ssa = Ssa::from_str_no_validation(src).unwrap();
if let Err(error) = verify_side_effect_predicates(&ssa) {
panic!(
"expected the tainted argument to the no_predicates call to be accepted, \
but validation rejected it: {error:?}"
);
}
}

#[test]
fn rejects_unguarded_result_of_no_predicates_call() {
// The exemption is only for the *arguments* flowing into the call: its
// result is a function of disabled-branch values, so it is arbitrary
// when the predicate is false and must still be guarded before it can
// escape. Same SSA as `accepts_tainted_argument_to_no_predicates_call`
// minus the `mul (cast v0), v5` guard, so a flip here means the
// exemption leaked to the results and nothing else.
let src = "
acir(inline) fn main f0 {
b0(v0: u1, v1: Field):
enable_side_effects v0
v2, v3 = call f1(v1) -> (Field, Field)
v4 = make_array [v2, v3] : [Field; 2]
enable_side_effects u1 1
v5 = call f2(v4) -> Field
return v5
}
brillig(inline) fn get f1 {
b0(v0: Field):
return v0, v0
}
acir(no_predicates) fn hash f2 {
b0(v0: [Field; 2]):
v1 = array_get v0, index u32 0 -> Field
return v1
}
";
let ssa = Ssa::from_str_no_validation(src).unwrap();
assert!(
verify_side_effect_predicates(&ssa).is_err(),
"expected the unguarded result of the no_predicates call to be rejected, \
but validation accepted it"
);
}

#[test]
fn accepts_arithmetic_outside_any_region() {
let src = "
Expand Down
Loading