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.

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

Jump to bottom

feat: --pedantic-solving flag #6716

Merged
merged 51 commits into from
Jan 7, 2025
Merged

feat: --pedantic-solving flag #6716

merged 51 commits into from
Jan 7, 2025
+879 −300

Conversation

michaeljklein
Copy link
Contributor

Description

Problem*

Resolves #6275

Summary*

Adds a compile-time flag --pedantic-solving to run extra sanity-check assertions at the opcode level in ACVM.

Additional Context

  1. This is expected to be useful for fuzzing
  2. This will need a follow-up for similar types of assertions

Documentation*

Check one:

  • No documentation needed.
  • Documentation included in this PR.
  • [For Experimental Features] Documentation to be submitted in a separate PR.

PR Checklist*

  • I have tested the changes locally.
  • I have formatted the changes with Prettier and/or cargo fmt on default settings.

@michaeljklein
test input sizes and predicate values with --pedantic_solving flag, a…
b5ee668 
…dd method to check for valid bigint modulus, add error for predicate > 1, add cli option for pedantic solving
@michaeljklein
add pedantic_solving parameter wherever needed, default to true when …
f65a0b0 
…testing or constant-folding, add tests for pedantic_solving, test to ensure allowed bingint moduli are prime
aakoshh
aakoshh reviewed Dec 6, 2024
View reviewed changes
Copy link
Contributor

@aakoshh aakoshh left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Dec 6, 2024 •
edited
Loading

Peak Memory Sample

Program Peak Memory
keccak256 78.48M
workspace 123.59M
regression_4709 422.91M
ram_blowup_regression 1.58G
private-kernel-tail 201.60M
private-kernel-reset 716.87M
private-kernel-inner 291.67M
parity-root 171.93M

TomAFrench
TomAFrench reviewed Dec 9, 2024
View reviewed changes
Copy link
Member

@TomAFrench TomAFrench left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks sensible but we seem to be being pedantic all the time for memory ops.

acvm-repo/acvm/src/pwg/mod.rs Outdated Show resolved Hide resolved
acvm-repo/acvm/src/pwg/memory_op.rs Outdated Show resolved Hide resolved
@aakoshh aakoshh mentioned this pull request Dec 9, 2024
Merged
5 tasks
@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Dec 9, 2024 •
edited
Loading

Compilation Report

Program Compilation Time %
sha256_regression 1.306s -4%
regression_4709 0.768s -3%
ram_blowup_regression 14.800s -3%
rollup-root 3.640s -13%
rollup-block-merge 3.850s -8%
rollup-base-public 32.200s 6%
rollup-base-private 13.500s 2%
private-kernel-tail 1.010s -2%
private-kernel-reset 6.996s 2%
private-kernel-inner 2.220s 0%

@michaeljklein
wip debugging: use StubbedBlackBoxSolver::default to enable pedantic_…
4b0df94 
…solving, check grumpkin_integer and whether points are infinite for ec add and multi_scalar_mul
@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Jan 3, 2025 •
edited
Loading

Execution Memory Report

Program Peak Memory
keccak256 74.61M
workspace 123.84M
regression_4709 315.93M
ram_blowup_regression 512.47M
rollup-base-public 773.35M
rollup-base-private 424.90M
private-kernel-tail 182.01M
private-kernel-reset 255.58M
private-kernel-inner 215.19M

@github-actions GitHub Actions
Copy link
Contributor

github-actions bot commented Jan 3, 2025 •
edited
Loading

Compilation Memory Report

Program Peak Memory
keccak256 78.50M
workspace 123.67M
regression_4709 422.91M
ram_blowup_regression 1.58G
rollup-base-public 2.55G
rollup-base-private 1.25G
private-kernel-tail 201.97M
private-kernel-reset 716.57M
private-kernel-inner 292.25M

TomAFrench
TomAFrench approved these changes Jan 3, 2025
View reviewed changes
Copy link
Member

@TomAFrench TomAFrench left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM once merge conflicts fixed.

@TomAFrench TomAFrench added this pull request to the merge queue Jan 7, 2025
Merged via the queue into master with commit 5b9a113 Jan 7, 2025
88 checks passed
@TomAFrench TomAFrench deleted the michaeljklein/pedantic-flag branch January 7, 2025 20:29
@noirwhal noirwhal mentioned this pull request Jan 7, 2025
Open
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 7, 2025
@AztecBot
[1 changes] feat!: type-check trait default methods (noir-lang/noir#6645
311bc03 
)

feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 7, 2025
@AztecBot
feat!: type-check trait default methods (noir-lang/noir#6645)
438dcab 
feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
@AztecBot AztecBot mentioned this pull request Jan 7, 2025
Open
TomAFrench added a commit that referenced this pull request Jan 8, 2025
@TomAFrench
Merge branch 'master' into ab/optimize-array-get-for-if-else-value
294b39c 
* master: (51 commits)
  feat!: type-check trait default methods (#6645)
  feat: `--pedantic-solving` flag (#6716)
  feat!: update `aes128_encrypt` to return an array (#6973)
  fix: wrong module to lookup trait when using crate or super (#6974)
  fix: Start RC at 1 again (#6958)
  feat!: turn TypeIsMorePrivateThenItem into an error (#6953)
  fix: don't fail parsing macro if there are parser warnings (#6969)
  fix: error on missing function parameters (#6967)
  feat: don't report warnings for dependencies (#6926)
  chore: simplify boolean in a mul of a mul (#6951)
  feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (#6893)
  chore: Move comment as part of #6945 (#6959)
  chore: Separate unconstrained functions during monomorphization (#6894)
  feat!: turn CannotReexportItemWithLessVisibility into an error (#6952)
  feat: lock on Nargo.toml on several nargo commands (#6941)
  feat: don't simplify SSA instructions when creating them from a string (#6948)
  chore: add reproduction case for bignum test failure (#6464)
  chore: bump `noir-gates-diff` (#6949)
  feat(test): Enable the test fuzzer for Wasm (#6835)
  chore: also print test output to stdout in CI (#6930)
  ...
TomAFrench added a commit that referenced this pull request Jan 8, 2025
@TomAFrench
Merge branch 'master' into 6929-bytecode-blowup
1d2f3b7 
* master:
  feat!: type-check trait default methods (#6645)
  feat: `--pedantic-solving` flag (#6716)
  feat!: update `aes128_encrypt` to return an array (#6973)
  fix: wrong module to lookup trait when using crate or super (#6974)
  fix: Start RC at 1 again (#6958)
  feat!: turn TypeIsMorePrivateThenItem into an error (#6953)
  fix: don't fail parsing macro if there are parser warnings (#6969)
  fix: error on missing function parameters (#6967)
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 8, 2025
@AztecBot
[1 changes] feat!: type-check trait default methods (noir-lang/noir#6645
a755124 
)

feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 8, 2025
@AztecBot
feat!: type-check trait default methods (noir-lang/noir#6645)
94152d6 
feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
Rumata888 pushed a commit that referenced this pull request Jan 8, 2025
@michaeljklein @aakoshh
@TomAFrench @Rumata888
feat: --pedantic-solving flag (#6716)
9cca916 
Co-authored-by: Akosh Farkash <aakoshh@gmail.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 8, 2025
@AztecBot
[1 changes] feat: impl Default for U128 (noir-lang/noir#6984)
e96e6d1 
fix: Do not emit range check for multiplication by bool (noir-lang/noir#6983)
fix: do not panic on indices which are not valid `u32`s (noir-lang/noir#6976)
feat!: require trait method calls (`foo.bar()`) to have the trait in scope (imported) (noir-lang/noir#6895)
feat!: type-check trait default methods (noir-lang/noir#6645)
feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
AztecBot added a commit to AztecProtocol/aztec-packages that referenced this pull request Jan 8, 2025
@AztecBot
feat: impl Default for U128 (noir-lang/noir#6984)
f87034a 
fix: Do not emit range check for multiplication by bool (noir-lang/noir#6983)
fix: do not panic on indices which are not valid `u32`s (noir-lang/noir#6976)
feat!: require trait method calls (`foo.bar()`) to have the trait in scope (imported) (noir-lang/noir#6895)
feat!: type-check trait default methods (noir-lang/noir#6645)
feat: `--pedantic-solving` flag (noir-lang/noir#6716)
feat!: update `aes128_encrypt` to return an array (noir-lang/noir#6973)
fix: wrong module to lookup trait when using crate or super (noir-lang/noir#6974)
fix: Start RC at 1 again (noir-lang/noir#6958)
feat!: turn TypeIsMorePrivateThenItem into an error (noir-lang/noir#6953)
fix: don't fail parsing macro if there are parser warnings (noir-lang/noir#6969)
fix: error on missing function parameters (noir-lang/noir#6967)
feat: don't report warnings for dependencies (noir-lang/noir#6926)
chore: simplify boolean in a mul of a mul (noir-lang/noir#6951)
feat(ssa): Immediately simplify away RefCount instructions in ACIR functions (noir-lang/noir#6893)
chore: Move comment as part of #6945 (noir-lang/noir#6959)
chore: Separate unconstrained functions during monomorphization (noir-lang/noir#6894)
feat!: turn CannotReexportItemWithLessVisibility into an error (noir-lang/noir#6952)
feat: lock on Nargo.toml on several nargo commands (noir-lang/noir#6941)
feat: don't simplify SSA instructions when creating them from a string (noir-lang/noir#6948)
chore: add reproduction case for bignum test failure (noir-lang/noir#6464)
chore: bump `noir-gates-diff` (noir-lang/noir#6949)
feat(test): Enable the test fuzzer for Wasm (noir-lang/noir#6835)
chore: also print test output to stdout in CI (noir-lang/noir#6930)
fix: Non-determinism from under constrained checks (noir-lang/noir#6945)
chore: use logs for benchmarking (noir-lang/noir#6911)
chore: bump `noir-gates-diff` (noir-lang/noir#6944)
chore: bump `noir-gates-diff` (noir-lang/noir#6943)
fix: Show output of `test_program_is_idempotent` on failure (noir-lang/noir#6942)
chore: delete a bunch of dead code from `noirc_evaluator` (noir-lang/noir#6939)
feat: require trait function calls (`Foo::bar()`) to have the trait in scope (imported) (noir-lang/noir#6882)
chore: Bump arkworks to version `0.5.0` (noir-lang/noir#6871)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TomAFrench TomAFrench TomAFrench approved these changes

@aakoshh aakoshh Awaiting requested review from aakoshh

Assignees
No one assigned
Labels
run-external-checks Trigger CI job to run tests on external repos
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Compilation flag to add runtime checks for opcode assumptions
3 participants
@michaeljklein @TomAFrench @aakoshh