feat: --pedantic-solving flag
#6716
Conversation
…dd method to check for valid bigint modulus, add error for predicate > 1, add cli option for pedantic solving
…testing or constant-folding, add tests for pedantic_solving, test to ensure allowed bingint moduli are prime
| let skip_bitsize_checks = true; | ||
| let skip_bitsize_checks = !pedantic_solving; |
There was a problem hiding this comment.
I see we have stand-alone functions here, so the pedantic_solving can only be a function parameter. Would it make sense to create a LogicSolver similar to the BigintSolver and make it a config parameter, so as not to complicate the API methods?
There was a problem hiding this comment.
Or maybe introduce some kind os SolverContext that could contain the initial_witness and the pedantic_solving; most functions I look at take the &mut WitnessMap as parameters, and by wrapping these up we could have a bunch of ambient studd we always pass around.
There was a problem hiding this comment.
I looked into using WitnessMap, but 1) I don't want to modify a native type, and 2) WitnessMap is used more often than pedantic_solving. I already moved pedantic_solving to the blackbox/bigint solver structs, so will look into the remaining cases next.
There was a problem hiding this comment.
To be clear I did not want to suggest modifying WitnessMap but to create a struct SolverContext { initial_witness: WistnessMap, pedantic_solver: bool } which could be used by the numerous functions that take both of these. If something only takes one we could always pass e.g. self.ctx.initial_witness. Or it might just take ctx anyway, as you said you plan on expanding the number of checks, maybe other parameters will be added to the context later.
There was a problem hiding this comment.
I'd prefer to keep it as-is since there's only ~5 cases left where pedantic_solving is passed along with a WitnessMap and I'd have to modify a bunch of places where the WitnessMap is created/updated.
acvm-repo/acvm/src/pwg/mod.rs
Outdated
| if is_predicate_false( | ||
| &self.witness_map, | ||
| predicate, | ||
| self.pedantic_solving, | ||
| &opcode_location, | ||
| )? { |
There was a problem hiding this comment.
Maybe is_predicate_false could be added to that SolverContext I suggested, resulting in a ctx.is_predicate_false(predicate, &opcode_location) which is a bit less busy.
There was a problem hiding this comment.
General response above
There was a problem hiding this comment.
Well if it ain't pedantic_solving being true to its name, this is a pervasive setting!
I added a lot of comments about potentially trying to add it to the solvers, or a context that is passed to the solvers, but even then there is a lot of threading through. It sounds more of an ambient setting like the logging level, not something that varies per function call, yet it's present in each bigint method, logical function and such like.
For something that is an optional setting, I do wonder if a solution involving an env var, perhaps some global variable would be a lighter touch. Not sure if there would be a good candidate for a module that could hold it though.
Co-authored-by: Akosh Farkash <[email protected]>
Peak Memory Sample
|
…er, store pedantic_solving in the bigint and blackbox solver structs, use pedantic_solving for tests
There was a problem hiding this comment.
Do we not have pedantic checks for the EC operations? I'd expect that we'd want to check that the points are all on the curve (or are marked as points at infinity).
There was a problem hiding this comment.
Actually, we want to exclude any points at infinity. The set of assumptions we make are documented in the stdlib.
There was a problem hiding this comment.
Ok, we're currently checking that all points are on curves for multi_scalar_mul and embedded_curve_add here
I've added checks for points at infinity: it looks like we support them for multi_scalar_mul?
Compilation Sample
|
…solving, check grumpkin_integer and whether points are infinite for ec add and multi_scalar_mul
Co-authored-by: Akosh Farkash <[email protected]>
Co-authored-by: Tom French <[email protected]>
|
NOTE: the following test tests::compile_success_empty::test_embedded_curve_add_simplification::forcebrillig_false_inliner_0_expects |
Description
Problem*
Resolves #6275
Summary*
Adds a compile-time flag
--pedantic-solvingto run extra sanity-check assertions at the opcode level in ACVM.Additional Context
Documentation*
Check one:
PR Checklist*
cargo fmton default settings.