Skip to content

chore: remove unused predicate from mem-op solver #10079

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
asterite merged 3 commits into from
Oct 3, 2025
Merged

chore: remove unused predicate from mem-op solver #10079

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fcaefb3
chore: remove unused predicate from mem-op solver
TomAFrench Oct 3, 2025
e870588
More removals
asterite Oct 3, 2025
415ac64
Fix docs
asterite Oct 3, 2025
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
118 changes: 9 additions & 109 deletions acvm-repo/acvm/src/pwg/memory_op.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
use acir::{
AcirField,
circuit::opcodes::MemOp,
native_types::{Expression, Witness, WitnessMap},
native_types::{Witness, WitnessMap},
};

use super::{ErrorLocation, OpcodeResolutionError};
use super::{
arithmetic::ExpressionSolver, get_value, insert_value, is_predicate_false, witness_to_value,
};
use super::{arithmetic::ExpressionSolver, get_value, insert_value, witness_to_value};

type MemoryIndex = u32;

Expand Down Expand Up @@ -86,7 +84,7 @@ impl<F: AcirField> MemoryOpSolver<F> {
/// Update the 'block_values' by processing the provided Memory opcode
/// The opcode 'op' contains the index and value of the operation and the type
/// of the operation.
/// They are all stored as an [Expression]
/// They are all stored as an [acir::native_types::Expression]
/// The type of 'operation' is '0' for a read and '1' for a write. It must be a constant
/// expression.
/// Index is not required to be constant but it must reduce to a known value
Expand All @@ -105,8 +103,6 @@ impl<F: AcirField> MemoryOpSolver<F> {
&mut self,
op: &MemOp<F>,
initial_witness: &mut WitnessMap<F>,
predicate: &Option<Expression<F>>,
pedantic_solving: bool,
) -> Result<(), OpcodeResolutionError<F>> {
let operation = get_value(&op.operation, initial_witness)?;

Expand All @@ -123,11 +119,6 @@ impl<F: AcirField> MemoryOpSolver<F> {
// `operation == 0` implies a read operation. (`operation == 1` implies write operation).
let is_read_operation = operation.is_zero();

// Fetch whether or not the predicate is false (e.g. equal to zero)
let opcode_location = ErrorLocation::Unresolved;
let skip_operation =
is_predicate_false(initial_witness, predicate, pedantic_solving, &opcode_location)?;

if is_read_operation {
// `value_read = arr[memory_index]`
//
Expand All @@ -137,10 +128,7 @@ impl<F: AcirField> MemoryOpSolver<F> {
"Memory must be read into a specified witness index, encountered an Expression",
);

// A zero predicate indicates that we should skip the read operation
// and zero out the operation's output.
let value_in_array =
if skip_operation { F::zero() } else { self.read_memory_index(memory_index)? };
let value_in_array = self.read_memory_index(memory_index)?;
insert_value(&value_read_witness, value_in_array, initial_witness)
} else {
// `arr[memory_index] = value_write`
Expand All @@ -149,15 +137,8 @@ impl<F: AcirField> MemoryOpSolver<F> {
// into the memory block.
let value_write = value;

// A zero predicate indicates that we should skip the write operation.
if skip_operation {
// We only want to write to already initialized memory.
// Do nothing if the predicate is zero.
Ok(())
} else {
let value_to_write = get_value(&value_write, initial_witness)?;
self.write_memory_index(memory_index, value_to_write)
}
let value_to_write = get_value(&value_write, initial_witness)?;
self.write_memory_index(memory_index, value_to_write)
}
}
}
Expand All @@ -169,14 +150,11 @@ mod tests {
use acir::{
AcirField, FieldElement,
circuit::opcodes::MemOp,
native_types::{Expression, Witness, WitnessMap},
native_types::{Witness, WitnessMap},
};

use super::MemoryOpSolver;

// use pedantic_solving for tests
const PEDANTIC_SOLVING: bool = true;

#[test]
fn test_solver() {
let mut initial_witness = WitnessMap::from(BTreeMap::from_iter([
Expand All @@ -195,9 +173,7 @@ mod tests {
let mut block_solver = MemoryOpSolver::new(&init, &initial_witness).unwrap();

for op in trace {
block_solver
.solve_memory_op(&op, &mut initial_witness, &None, PEDANTIC_SOLVING)
.unwrap();
block_solver.solve_memory_op(&op, &mut initial_witness).unwrap();
}

assert_eq!(initial_witness[&Witness(4)], FieldElement::from(2u128));
Expand All @@ -221,9 +197,7 @@ mod tests {
let mut err = None;
for op in invalid_trace {
if err.is_none() {
err = block_solver
.solve_memory_op(&op, &mut initial_witness, &None, PEDANTIC_SOLVING)
.err();
err = block_solver.solve_memory_op(&op, &mut initial_witness).err();
}
}

Expand All @@ -236,78 +210,4 @@ mod tests {
}) if index == FieldElement::from(2u128)
));
}

#[test]
// TODO: to review after the serialization changes are merged because it will remove the predicate.
fn test_predicate_on_read() {
let mut initial_witness = WitnessMap::from(BTreeMap::from_iter([
(Witness(1), FieldElement::from(1u128)),
(Witness(2), FieldElement::from(1u128)),
(Witness(3), FieldElement::from(2u128)),
]));

let init = vec![Witness(1), Witness(2)];

let invalid_trace = vec![
MemOp::write_to_mem_index(FieldElement::from(1u128).into(), Witness(3).into()),
MemOp::read_at_mem_index(FieldElement::from(2u128).into(), Witness(4)),
];
let mut block_solver = MemoryOpSolver::new(&init, &initial_witness).unwrap();
let mut err = None;
for op in invalid_trace {
if err.is_none() {
err = block_solver
.solve_memory_op(
&op,
&mut initial_witness,
&Some(Expression::zero()),
PEDANTIC_SOLVING,
)
.err();
}
}

// Should have no index out of bounds error where predicate is zero
assert_eq!(err, None);
// The result of a read under a zero predicate should be zero
assert_eq!(initial_witness[&Witness(4)], FieldElement::from(0u128));
}

#[test]
// TODO: to review after the serialization changes are merged because it will remove the predicate.
fn test_predicate_on_write() {
let mut initial_witness = WitnessMap::from(BTreeMap::from_iter([
(Witness(1), FieldElement::from(1u128)),
(Witness(2), FieldElement::from(1u128)),
(Witness(3), FieldElement::from(2u128)),
]));

let init = vec![Witness(1), Witness(2)];

let invalid_trace = vec![
MemOp::write_to_mem_index(FieldElement::from(2u128).into(), Witness(3).into()),
MemOp::read_at_mem_index(FieldElement::from(0u128).into(), Witness(4)),
MemOp::read_at_mem_index(FieldElement::from(1u128).into(), Witness(5)),
];
let mut block_solver = MemoryOpSolver::new(&init, &initial_witness).unwrap();
let mut err = None;
for op in invalid_trace {
if err.is_none() {
err = block_solver
.solve_memory_op(
&op,
&mut initial_witness,
&Some(Expression::zero()),
PEDANTIC_SOLVING,
)
.err();
}
}

// Should have no index out of bounds error where predicate is zero
assert_eq!(err, None);
// The memory under a zero predicate should be zeroed out
assert_eq!(initial_witness[&Witness(4)], FieldElement::from(0u128));
assert_eq!(initial_witness[&Witness(5)], FieldElement::from(0u128));
}
}
7 changes: 1 addition & 6 deletions acvm-repo/acvm/src/pwg/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -524,12 +524,7 @@ impl<'a, F: AcirField, B: BlackBoxFunctionSolver<F>> ACVM<'a, F, B> {
.block_solvers
.get_mut(block_id)
.expect("Memory block should have been initialized before use");
solver.solve_memory_op(
op,
&mut self.witness_map,
&None,
self.backend.pedantic_solving(),
)
solver.solve_memory_op(op, &mut self.witness_map)
}
Opcode::BrilligCall { .. } => match self.solve_brillig_call_opcode() {
Ok(Some(foreign_call)) => return self.wait_for_foreign_call(foreign_call),
Expand Down
Loading