Binary solver for array equality constraints#520
Conversation
| let mut result = GateResolution::Skip; | ||
| if let Gate::Arithmetic(arith) = gate { | ||
| let partial_gate = | ||
| super::arithmetic::ArithmeticSolver::evaluate(arith, initial_witness); | ||
| result = self.solve_booleans(initial_witness, &partial_gate); | ||
| self.identify_booleans(&partial_gate); | ||
| } else { | ||
| self.identify_binaries(gate); | ||
| } | ||
| result |
There was a problem hiding this comment.
| let mut result = GateResolution::Skip; | |
| if let Gate::Arithmetic(arith) = gate { | |
| let partial_gate = | |
| super::arithmetic::ArithmeticSolver::evaluate(arith, initial_witness); | |
| result = self.solve_booleans(initial_witness, &partial_gate); | |
| self.identify_booleans(&partial_gate); | |
| } else { | |
| self.identify_binaries(gate); | |
| } | |
| result | |
| if let Gate::Arithmetic(arith) = gate { | |
| let partial_gate = | |
| super::arithmetic::ArithmeticSolver::evaluate(arith, initial_witness); | |
| let result = self.solve_booleans(initial_witness, &partial_gate); | |
| self.identify_booleans(&partial_gate); | |
| result | |
| } else { | |
| self.identify_binaries(gate); | |
| GateResolution::Skip | |
| } |
We can remove some indirection with the mutable result here.
| UnknownError(String), //Generic error | ||
| UnsupportedOpcode(OPCODE), //Unsupported Opcode | ||
| UnsatisfiedConstrain, //Gate is not satisfied | ||
| Solved, //Circuit is solved, after a number of passes |
There was a problem hiding this comment.
Can we remove the variant entirely? It is only returned by solve, but there is no reason solve could not return Resolved instead.
| self.invert_witness.insert(*x, *result); | ||
| } | ||
| Gate::Arithmetic(a) => { | ||
| self.identify_booleans(a); |
There was a problem hiding this comment.
When is this branch triggered?
seems identify_binaries is called when it is not an arithmetic gate
There was a problem hiding this comment.
Indeed, but still the function is correct like this, using unreachable! would make it fit for the current use and less versatile.
|
Can we close this now that #731 is merged or will this be useful in another context? We need to move this to ACVM anyway if so. |
Yes this is useful in another context, in fact the issue solved by #731 was because the solver is not able to solve array equality checks. This PR is solving this issue, while #731 worked around it by removing it in case of a return statement. |
|
Closing as this is no longer relevant |
5 participants
Related issue(s)
Resolves #455
Description
Summary of changes
This PR adds a binary solver which is able to solve the array equality constraints by identifying boolean constraints.
Dependency additions / changes
The binary solver is used only when the regular solver is stalled, so this has no impact when there is no array returned, and when there is, it will act only on the remaining unsolved gates.
Test additions / changes
sha256 and main_return tests are updated
Checklist
cargo fmtwith default settings.