Skip to content

chore(ssa): Initial validation module#8765

Merged
vezenovm merged 16 commits intomasterfrom
mv/validation-module
Jun 9, 2025
Merged

chore(ssa): Initial validation module#8765
vezenovm merged 16 commits intomasterfrom
mv/validation-module

Conversation

@vezenovm
Copy link
Contributor

@vezenovm vezenovm commented Jun 2, 2025

Description

Problem*

Working towards #8705. It has multiple sub-issues so once those are resolved I think we could close the issue.

Summary*

This PR simply makes an initial validation module that moves over some of our assertions on Function to a separate Validator struct. This felt like the simplest solution for our current validation plans. We can then expand this validator in the future as needed (e.g. extra state like the CFG and DominatorTree).

Additional Context

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.

@vezenovm vezenovm requested a review from a team June 2, 2025 21:02
@vezenovm vezenovm changed the title feat(ssa): Initial validation module chore(ssa): Initial validation module Jun 2, 2025
Copy link
Contributor

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Test Suite Duration'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite Current: 8d6e7a2 Previous: bf1dbdb Ratio
test_report_zkpassport_noir_rsa_ 2 s 1 s 2

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

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.

Would it make sense to run this between SSA passes if some CLI flag is on? Maybe in integration tests?

@TomAFrench
Copy link
Member

TomAFrench commented Jun 3, 2025

One thing to note here is that there's various validations which make sense to check on the initial SSA (even if we're starting halfway through the SSA optimization pipeline) and validations which we expect to hold after each and every SSA pass.

I mention this as we can have cases where we assert that the initial SSA must follow rules like "all arithmetic must be checked" however SSA optimizations may convert checked arithmetic to unchecked later on so it would be good to have the validator flexible enough to handle this.

@vezenovm
Copy link
Contributor Author

vezenovm commented Jun 3, 2025

Would it make sense to run this between SSA passes if some CLI flag is on? Maybe in integration tests?

Yeah a CLI command for this would be useful. Although this verifier is just on the initial SSA at the moment. I think we can extend the CLI in a follow-up. To start I think this on its own provides a nice benefit to fuzzing as it helps check that the SSA generated is well formed.

@vezenovm
Copy link
Contributor Author

vezenovm commented Jun 3, 2025

One thing to note here is that there's various validations which make sense to check on the initial SSA (even if we're starting halfway through the SSA optimization pipeline) and validations which we expect to hold after each and every SSA pass

I will add configurations to the Validator to enable handling validation of different stages of the compilation pipeline. I will build off of this branch. For now, this PR is ready for review again.

@vezenovm vezenovm requested review from TomAFrench and aakoshh June 3, 2025 16:40
@vezenovm
Copy link
Contributor Author

vezenovm commented Jun 4, 2025

One thing to note here is that there's various validations which make sense to check on the initial SSA (even if we're starting halfway through the SSA optimization pipeline) and validations which we expect to hold after each and every SSA pass.

I mention this as we can have cases where we assert that the initial SSA must follow rules like "all arithmetic must be checked" however SSA optimizations may convert checked arithmetic to unchecked later on so it would be good to have the validator flexible enough to handle this.

I was starting to add some configuration settings but at the moment I wasn't sure what invariants we apply to the initial SSA that we don't apply after other passes. There are per pass invariants (e.g. no more function types in parameters after defunctionalize) and I started on marking different stages of the compilation pipeline in the validator. However, I was thinking this may be good to keep localized in each pass. We can then have a hybrid approach where we apply per-pass localized checks, while this Validator can be for invariants that should hold about the SSA form no matter the pass. I feel this may be a better separation of concerns.

Copy link
Collaborator

@asterite asterite left a comment

Choose a reason for hiding this comment

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

Looks good! I left a comment for something that might need a fix.

Copy link
Contributor

@github-actions github-actions bot left a comment

Choose a reason for hiding this comment

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

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Execution Time'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.

Benchmark suite Current: 84c9529 Previous: bf1dbdb Ratio
rollup-merge 0.004 s 0.003 s 1.33

This comment was automatically generated by workflow using github-action-benchmark.

CC: @TomAFrench

@vezenovm vezenovm enabled auto-merge June 9, 2025 14:08
@vezenovm vezenovm added this pull request to the merge queue Jun 9, 2025
Merged via the queue into master with commit 85dba2c Jun 9, 2025
117 checks passed
@vezenovm vezenovm deleted the mv/validation-module branch June 9, 2025 15:10
github-merge-queue bot pushed a commit to AztecProtocol/aztec-packages that referenced this pull request Jun 10, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
github-merge-queue bot pushed a commit to AztecProtocol/aztec-packages that referenced this pull request Jun 10, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
danielntmd pushed a commit to danielntmd/aztec-packages that referenced this pull request Jul 16, 2025
Automated pull of nightly from the
[noir](https://github.com/noir-lang/noir) programming language, a
dependency of Aztec.
BEGIN_COMMIT_OVERRIDE
chore(docs): Update noirjs app page to use to beta.6
(noir-lang/noir#8853)
fix: support recursive call to main function in SSA parser
(noir-lang/noir#8760)
chore(SSA): validate that constrain values have the same type
(noir-lang/noir#8850)
fix: Comptime field division should error when the rhs is zero
(noir-lang/noir#8845)
chore: redo typo PR by osrm
(noir-lang/noir#8840)
fix: (SSA interpreter) to_le_bits returns [u1; _], not [u8; _]
(noir-lang/noir#8837)
chore(ssa): Initial validation module
(noir-lang/noir#8765)
chore: bump external pinned commits
(noir-lang/noir#8834)
feat(fuzz): Generate arbitrary constraints
(noir-lang/noir#8820)
fix: bind self generic type in trait calls via a concrete type in more
cases (noir-lang/noir#8827)
fix(comptime): Overflow on shl
(noir-lang/noir#8829)
fix(interpreter): Return -1 for negative shr signed overflow or 0 for
positive shr signed overflow
(noir-lang/noir#8828)
feat(ssa_fuzzer): branching + constrains
(noir-lang/noir#8599)
chore(docs): Add experimental warning in Debugger docs
(noir-lang/noir#8824)
fix: Thread errors through remove_if_else instead of panicing when the
value merger finds reference values
(noir-lang/noir#8783)
fix(interpreter): Do not overflow on signed checked ops
(noir-lang/noir#8806)
feat: short circuit creation of `Type::InfixExpr` containing errors
(noir-lang/noir#8826)
fix(mem2reg): Keep last stores used in array returned from a function
(noir-lang/noir#8801)
chore(ci): `cargo clippy` CI script to save time
(noir-lang/noir#8787)
chore: only follow bindings on interface to `arithmetic` module
(noir-lang/noir#8822)
fix: bind self generic type in trait calls via a concrete type
(noir-lang/noir#8825)
chore(docs): Reorder tooling docs
(noir-lang/noir#8742)
chore: small fix for outdated docs
(noir-lang/noir#8821)
fix(mem2reg): Keep last stores used in MakeArray
(noir-lang/noir#8743)
fix!: Error when re-assigning a mutable reference
(noir-lang/noir#8790)
fix!: indexing arrays with non-u32 is now an error
(noir-lang/noir#8804)
fix: signed right shift overflows to 0 or -1
(noir-lang/noir#8805)
chore(fuzz): Tool to minimize Noir programs with `cvise`
(noir-lang/noir#8789)
END_COMMIT_OVERRIDE

---------

Co-authored-by: AztecBot <tech@aztecprotocol.com>
Co-authored-by: Tom French <15848336+TomAFrench@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants