Skip to content
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.

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

feat: decompose Instruction::Constrain into multiple more basic constraints #3892

Merged
merged 26 commits into from
Jan 10, 2024
Merged
Show file tree
Hide file tree
Changes from 19 commits
Commits
Show all changes
26 commits
Select commit Hold shift + click to select a range
247d71b
feat: decompose constraints on boolean multiplications
TomAFrench Dec 20, 2023
d369b95
fix: add missing check for multiplication to equal 1
TomAFrench Dec 20, 2023
a3e4e8e
chore: avoid needing multiple rounds of constant folding
TomAFrench Dec 21, 2023
bd258a8
chore: handle constraining `(x | y) == 0`
TomAFrench Dec 21, 2023
cc324d2
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Dec 21, 2023
776a8b7
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Dec 21, 2023
6e656e3
chore: add test to track struct equality opcode counts
TomAFrench Jan 2, 2024
c7f97ed
chore: got my foos and bars mixed up
TomAFrench Jan 2, 2024
24565ad
chore: fix foo value
TomAFrench Jan 2, 2024
079b51d
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 2, 2024
178f2eb
chore: add constraints on usage of `SimplifyResult::SimplifiedToInstr…
TomAFrench Jan 2, 2024
b28b878
fix: prevent instructions iterator being consumed when checking length
TomAFrench Jan 2, 2024
85253af
chore: clippy
TomAFrench Jan 2, 2024
b428b81
Update compiler/noirc_evaluator/src/ssa/ir/instruction.rs
TomAFrench Jan 3, 2024
67d6a63
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 4, 2024
e339657
chore: remove broken import
TomAFrench Jan 4, 2024
0056e7c
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 5, 2024
b4ddf14
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 8, 2024
4e4e054
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 8, 2024
09190a7
Update compiler/noirc_evaluator/src/ssa/ir/dfg.rs
TomAFrench Jan 8, 2024
d1db6d4
chore: fix compilation
TomAFrench Jan 8, 2024
519b97b
chore: add test for constraint decomposition in rust
TomAFrench Jan 8, 2024
d77aecb
chore: remove struct equality test
TomAFrench Jan 8, 2024
765bbfb
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 9, 2024
d29cfe7
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 9, 2024
a91d0cc
Merge branch 'master' into tf/decompose-asserted-boolean-multiplications
TomAFrench Jan 10, 2024
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
33 changes: 27 additions & 6 deletions compiler/noirc_evaluator/src/ssa/ir/dfg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -166,12 +166,33 @@ impl DataFlowGraph {
SimplifiedToMultiple(simplification)
}
SimplifyResult::Remove => InstructionRemoved,
result @ (SimplifyResult::SimplifiedToInstruction(_) | SimplifyResult::None) => {
let instruction = result.instruction().unwrap_or(instruction);
let id = self.make_instruction(instruction, ctrl_typevars);
self.blocks[block].insert_instruction(id);
self.locations.insert(id, call_stack);
InsertInstructionResult::Results(id, self.instruction_results(id))
result @ (SimplifyResult::SimplifiedToInstruction(_)
| SimplifyResult::SimplifiedToInstructionMultiple(_)
| SimplifyResult::None) => {
let instructions = result.instructions().unwrap_or(vec![instruction]);

if instructions.len() > 1 {
// There's currently no way to pass results from one instruction in `instructions` on to the next.
// We then restrict this to only support multiple instructions if they're all `Instruction::Constrain`
// as this instruction type does not have any results.
assert!(
instructions.iter().all(|instruction| matches!(instruction, Instruction::Constrain(..))),
"`SimplifyResult::SimplifiedToInstructionMultiple` only supports `Constrain` instructions"
);
}
jfecher marked this conversation as resolved.
Show resolved Hide resolved

let mut instructions = instructions.into_iter().peekable();

while let Some(instruction) = instructions.next() {
let id = self.make_instruction(instruction, ctrl_typevars.clone());
self.blocks[block].insert_instruction(id);
self.locations.insert(id, call_stack.clone());

if instructions.peek().is_none() {
return InsertInstructionResult::Results(id, self.instruction_results(id));
}
}
unreachable!("At least one instruction must be returned. To not insert an instruction, use `SimplifyResult::Remove`")
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
}
}
}
Expand Down
202 changes: 134 additions & 68 deletions compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -432,73 +432,11 @@ impl Instruction {
}
}
Instruction::Constrain(lhs, rhs, msg) => {
if dfg.resolve(*lhs) == dfg.resolve(*rhs) {
// Remove trivial case `assert_eq(x, x)`
SimplifyResult::Remove
let constraints = decompose_constrain(*lhs, *rhs, msg.clone(), dfg);
if constraints.is_empty() {
Remove
} else {
match (&dfg[dfg.resolve(*lhs)], &dfg[dfg.resolve(*rhs)]) {
(
Value::NumericConstant { constant, typ },
Value::Instruction { instruction, .. },
)
| (
Value::Instruction { instruction, .. },
Value::NumericConstant { constant, typ },
) if *typ == Type::bool() => {
match dfg[*instruction] {
Instruction::Binary(Binary {
lhs,
rhs,
operator: BinaryOp::Eq,
}) if constant.is_one() => {
// Replace an explicit two step equality assertion
//
// v2 = eq v0, u32 v1
// constrain v2 == u1 1
//
// with a direct assertion of equality between the two values
//
// v2 = eq v0, u32 v1
// constrain v0 == v1
//
// Note that this doesn't remove the value `v2` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.

SimplifiedToInstruction(Instruction::Constrain(
lhs,
rhs,
msg.clone(),
))
}
Instruction::Not(value) => {
// Replace an assertion that a not instruction is truthy
//
// v1 = not v0
// constrain v1 == u1 1
//
// with an assertion that the not instruction input is falsy
//
// v1 = not v0
// constrain v0 == u1 0
//
// Note that this doesn't remove the value `v1` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.
let reversed_constant = FieldElement::from(!constant.is_one());
let reversed_constant =
dfg.make_constant(reversed_constant, Type::bool());
SimplifiedToInstruction(Instruction::Constrain(
value,
reversed_constant,
msg.clone(),
))
}

_ => None,
}
}

_ => None,
}
SimplifiedToInstructionMultiple(constraints)
}
}
Instruction::ArrayGet { array, index } => {
Expand Down Expand Up @@ -619,6 +557,129 @@ fn simplify_cast(value: ValueId, dst_typ: &Type, dfg: &mut DataFlowGraph) -> Sim
}
}

/// Try to decompose this constrain instruction. This constraint will be broken down such that it instead constrains
/// all the values which are used to compute the values which were being constrained.
fn decompose_constrain(
lhs: ValueId,
rhs: ValueId,
msg: Option<String>,
dfg: &mut DataFlowGraph,
) -> Vec<Instruction> {
let lhs = dfg.resolve(lhs);
let rhs = dfg.resolve(rhs);

if lhs == rhs {
// Remove trivial case `assert_eq(x, x)`
Vec::new()
} else {
match (&dfg[lhs], &dfg[rhs]) {
(Value::NumericConstant { constant, typ }, Value::Instruction { instruction, .. })
| (Value::Instruction { instruction, .. }, Value::NumericConstant { constant, typ })
if *typ == Type::bool() =>
{
match dfg[*instruction] {
Instruction::Binary(Binary { lhs, rhs, operator: BinaryOp::Eq })
if constant.is_one() =>
{
// Replace an explicit two step equality assertion
//
// v2 = eq v0, u32 v1
// constrain v2 == u1 1
//
// with a direct assertion of equality between the two values
//
// v2 = eq v0, u32 v1
// constrain v0 == v1
//
// Note that this doesn't remove the value `v2` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.

vec![Instruction::Constrain(lhs, rhs, msg)]
}

Instruction::Binary(Binary { lhs, rhs, operator: BinaryOp::Mul })
if constant.is_one() && dfg.type_of_value(lhs) == Type::bool() =>
{
// Replace an equality assertion on a boolean multiplication
//
// v2 = mul v0, v1
// constrain v2 == u1 1
//
// with a direct assertion that each value is equal to 1
//
// v2 = mul v0, v1
// constrain v0 == 1
// constrain v1 == 1
//
// This is due to the fact that for `v2` to be 1 then both `v0` and `v1` are 1.
//
// Note that this doesn't remove the value `v2` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.
let one = FieldElement::one();
let one = dfg.make_constant(one, Type::bool());

[
decompose_constrain(lhs, one, msg.clone(), dfg),
decompose_constrain(rhs, one, msg, dfg),
]
.concat()
}

Instruction::Binary(Binary { lhs, rhs, operator: BinaryOp::Or })
if constant.is_zero() =>
{
// Replace an equality assertion on an OR
//
// v2 = or v0, v1
// constrain v2 == u1 0
//
// with a direct assertion that each value is equal to 0
//
// v2 = or v0, v1
// constrain v0 == 0
// constrain v1 == 0
//
// This is due to the fact that for `v2` to be 0 then both `v0` and `v1` are 0.
//
// Note that this doesn't remove the value `v2` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.
let zero = FieldElement::zero();
let zero = dfg.make_constant(zero, dfg.type_of_value(lhs));

[
decompose_constrain(lhs, zero, msg.clone(), dfg),
decompose_constrain(rhs, zero, msg, dfg),
]
.concat()
}

Instruction::Not(value) => {
// Replace an assertion that a not instruction is truthy
//
// v1 = not v0
// constrain v1 == u1 1
//
// with an assertion that the not instruction input is falsy
//
// v1 = not v0
// constrain v0 == u1 0
//
// Note that this doesn't remove the value `v1` as it may be used in other instructions, but it
// will likely be removed through dead instruction elimination.
let reversed_constant = FieldElement::from(!constant.is_one());
let reversed_constant = dfg.make_constant(reversed_constant, Type::bool());
decompose_constrain(value, reversed_constant, msg, dfg)
}

_ => vec![Instruction::Constrain(lhs, rhs, msg)],
}
}

_ => vec![Instruction::Constrain(lhs, rhs, msg)],
}
}
}

/// The possible return values for Instruction::return_types
pub(crate) enum InstructionResultType {
/// The result type of this instruction matches that of this operand
Expand Down Expand Up @@ -1107,6 +1168,10 @@ pub(crate) enum SimplifyResult {
/// Replace this function with an simpler but equivalent instruction.
SimplifiedToInstruction(Instruction),

/// Replace this function with a set of simpler but equivalent instructions.
/// This is currently only to be used for [`Instruction::Constrain`].
SimplifiedToInstructionMultiple(Vec<Instruction>),

/// Remove the instruction, it is unnecessary
Remove,

Expand All @@ -1115,9 +1180,10 @@ pub(crate) enum SimplifyResult {
}

impl SimplifyResult {
pub(crate) fn instruction(self) -> Option<Instruction> {
pub(crate) fn instructions(self) -> Option<Vec<Instruction>> {
match self {
SimplifyResult::SimplifiedToInstruction(instruction) => Some(instruction),
SimplifyResult::SimplifiedToInstruction(instruction) => Some(vec![instruction]),
SimplifyResult::SimplifiedToInstructionMultiple(instructions) => Some(instructions),
_ => None,
}
}
Expand Down
6 changes: 6 additions & 0 deletions test_programs/execution_success/struct_equality/Nargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "struct_equality"
type = "bin"
authors = [""]

[dependencies]
4 changes: 4 additions & 0 deletions test_programs/execution_success/struct_equality/Prover.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
[x]
bar = true
baz = [1, 2, 3]
foo = 42
19 changes: 19 additions & 0 deletions test_programs/execution_success/struct_equality/src/main.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// This test demonstrates how SSA optimizations breaks down a struct equality assertion
// to assert directly on the struct's fields rather than using a predicate.

struct MyStruct {
foo: Field,
bar: bool,
baz: [u8; 3]
}

impl Eq for MyStruct {
fn eq(self, other: MyStruct) -> bool {
(self.foo == other.foo) & (self.bar == other.bar) & (self.baz == other.baz)
}
}

fn main(x: MyStruct) {
let y = MyStruct { foo: 42, bar: true, baz: [1, 2, 3] };
assert(x.eq(y));
}
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
Loading