diff --git a/compiler/noirc_evaluator/src/acir/call/intrinsics/vector_ops.rs b/compiler/noirc_evaluator/src/acir/call/intrinsics/vector_ops.rs index adf2372414f..3190f1542fd 100644 --- a/compiler/noirc_evaluator/src/acir/call/intrinsics/vector_ops.rs +++ b/compiler/noirc_evaluator/src/acir/call/intrinsics/vector_ops.rs @@ -386,8 +386,14 @@ impl Context<'_> { let vector_type = dfg.type_of_value(vector_contents_id); self.check_vector_result_count("vector_pop_back", result_ids, &vector_type)?; - // Check if we're trying to pop from a known empty vector. - if self.has_zero_length(vector_contents_id, dfg) { + let vector_length_var = vector_length_value.clone().into_var()?; + + // Check if we're trying to pop from a known empty vector: one whose backing store + // is empty, or one whose semantic length is known to be zero (its backing store may + // still be non-empty padding in that case). + if self.has_zero_length(vector_contents_id, dfg) + || self.vector_length_is_known_zero(dfg, vector_length_id, vector_length_var) + { // Make sure this code is disabled, or fail with the empty-vector pop message. let msg = "Attempt to pop from an empty vector".to_string(); self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?; @@ -451,6 +457,25 @@ impl Context<'_> { Ok(results) } + /// Whether the vector's semantic length is known to be zero at this point: either the + /// SSA value is the constant zero, or its ACIR expression has folded to zero (which + /// happens when the side-effects predicate it was multiplied by collapsed to a + /// constant). The backing store cannot answer this question — merging branch arms of + /// unequal lengths pads the shorter arm, so a semantically empty vector may still have + /// a non-empty backing store, and `has_zero_length` inspects that backing store. + fn vector_length_is_known_zero( + &self, + dfg: &DataFlowGraph, + vector_length_id: ValueId, + vector_length_var: AcirVar, + ) -> bool { + let length_const = dfg.get_numeric_constant(vector_length_id).or_else(|| { + let expr = self.acir_context.var_to_expression(vector_length_var).ok()?; + expr.to_const().copied() + }); + length_const.is_some_and(|length| length.is_zero()) + } + /// Compute the new vector length after popping one value from it. /// /// Assumes that we already handled the constant zero case. @@ -547,8 +572,14 @@ impl Context<'_> { self.check_vector_result_count("vector_pop_front", result_ids, &vector_type)?; let element_size = vector_type.element_size(); - // Check if we're trying to pop from a known empty vector. - if self.has_zero_length(vector_contents_id, dfg) { + let vector_length_var = vector_length_value.clone().into_var()?; + + // Check if we're trying to pop from a known empty vector: one whose backing store + // is empty, or one whose semantic length is known to be zero (its backing store may + // still be non-empty padding in that case). + if self.has_zero_length(vector_contents_id, dfg) + || self.vector_length_is_known_zero(dfg, vector_length_id, vector_length_var) + { // Make sure this code is disabled, or fail with the empty-vector pop message. let msg = "Attempt to pop from an empty vector".to_string(); self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?; @@ -873,8 +904,13 @@ impl Context<'_> { let vector_typ = dfg.type_of_value(vector_contents); self.check_vector_result_count("vector_remove", result_ids, &vector_typ)?; - // Check if we're trying to remove from an empty vector - if self.has_zero_length(vector_contents, dfg) { + // Check if we're trying to remove from a known empty vector: one whose backing store + // is empty, or one whose semantic length is known to be zero (its backing store may + // still be non-empty padding in that case). Without the semantic-length check a length + // that has folded to zero reaches the `sub_var(length, 1)` below and produces `p - 1`. + if self.has_zero_length(vector_contents, dfg) + || self.vector_length_is_known_zero(dfg, arguments[0], vector_length) + { // Make sure this code is disabled, or fail with "Index out of bounds". let msg = "Index out of bounds, vector has size 0".to_string(); self.acir_context.assert_zero_var(self.current_side_effects_enabled_var, msg)?; diff --git a/test_programs/execution_success/vector_ops_collapsed_predicate/Nargo.toml b/test_programs/execution_success/vector_ops_collapsed_predicate/Nargo.toml new file mode 100644 index 00000000000..234935b0be8 --- /dev/null +++ b/test_programs/execution_success/vector_ops_collapsed_predicate/Nargo.toml @@ -0,0 +1,6 @@ +[package] +name = "vector_ops_collapsed_predicate" +type = "bin" +authors = [""] + +[dependencies] diff --git a/test_programs/execution_success/vector_ops_collapsed_predicate/Prover.toml b/test_programs/execution_success/vector_ops_collapsed_predicate/Prover.toml new file mode 100644 index 00000000000..9b7b1ddae8d --- /dev/null +++ b/test_programs/execution_success/vector_ops_collapsed_predicate/Prover.toml @@ -0,0 +1,4 @@ +g0 = true +d = false +i = 0 +return = 0 diff --git a/test_programs/execution_success/vector_ops_collapsed_predicate/src/main.nr b/test_programs/execution_success/vector_ops_collapsed_predicate/src/main.nr new file mode 100644 index 00000000000..1fb519e4c68 --- /dev/null +++ b/test_programs/execution_success/vector_ops_collapsed_predicate/src/main.nr @@ -0,0 +1,23 @@ +// Popping from a statically-empty slice inside a conditional collapses the branch +// predicate to a constant zero at the ACIR level (the empty-pop assertion pins it), +// which in turn folds the length of an unrelated, still-live slice to a constant zero. +// A subsequent `remove` on that slice must not turn the folded length into `0 - 1` in +// the field: `push_back` consumes the result as a `u32` length, and the compiler must +// not crash converting it. With `g0 = true` the branch is inactive and `main` returns 0. +fn main(g0: bool, d: bool, i: u32) -> pub Field { + let v = @[1]; + let mut w = @[1]; + if d { + w = w.push_back(5); + } + let mut out = 0; + if !g0 { + let (v2, _a) = v.remove(i); + let (_v3, _b) = v2.pop_back(); + let (w2, _c) = w.pop_back(); + let (w3, _e) = w2.remove(i); + let w4 = w3.push_back(9); + out = w4[0]; + } + out +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__expanded.snap b/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__expanded.snap new file mode 100644 index 00000000000..b430cbb8d15 --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__expanded.snap @@ -0,0 +1,19 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: expanded_code +--- +fn main(g0: bool, d: bool, i: u32) -> pub Field { + let v: [Field] = @[1_Field]; + let mut w: [Field] = @[1_Field]; + if d { w = w.push_back(5_Field); }; + let mut out: Field = 0_Field; + if !g0 { + let (v2, _a): ([Field], Field) = v.remove(i); + let (_v3, _b): ([Field], Field) = v2.pop_back(); + let (w2, _c): ([Field], Field) = w.pop_back(); + let (w3, _e): ([Field], Field) = w2.remove(i); + let w4: [Field] = w3.push_back(9_Field); + out = w4[0_u32]; + }; + out +} diff --git a/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__stdout.snap b/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__stdout.snap new file mode 100644 index 00000000000..71eadd9acea --- /dev/null +++ b/tooling/nargo_cli/tests/snapshots/execution_success/vector_ops_collapsed_predicate/execute__tests__stdout.snap @@ -0,0 +1,5 @@ +--- +source: tooling/nargo_cli/tests/execute.rs +expression: stdout +--- +[vector_ops_collapsed_predicate] Circuit output: 0x00