Reject unsupported zero-result ops in ZKLean conversion#496
Open
Kuhai9801 wants to merge 6 commits into
Open
Conversation
b85c69a to
3e599cd
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR fixes a correctness hole in the LLZK → ZKLean conversion pass (--convert-llzk-to-zklean) where unsupported operations that produce zero SSA results could be silently ignored, allowing constraint semantics to be dropped without diagnostics (Fixes #495).
Changes:
- Reject all unhandled operations during conversion (including zero-result ops), except for an empty
function.returntreated as an intentional no-op. - Reject multi-block
function.defbodies up-front since the converter only processes a single block. - Add lit regression tests for dropped zero-result constraint ops / calls and for result-bearing
function.return, plus a changelog entry.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
backends/zklean/lib/Conversions/LLZKToZKLean.cpp |
Tightens error handling to fail on unhandled ops (including zero-result), treats only empty function.return as no-op, rejects multi-block functions, and emits a module-level failure when nothing is converted. |
test/Conversions/llzk_to_zklean_unsupported_zero_result_fail.llzk |
Adds regression coverage to ensure unsupported zero-result ops and value-returning function.return fail with diagnostics. |
test/Conversions/llzk_to_zklean_no_eligible_fail.llzk |
Verifies the pass fails when no eligible functions are converted (no ZKLean module produced). |
changelogs/unreleased/reject-unsupported-zklean-ops.yaml |
Documents the fix in the unreleased changelog. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+401
to
+405
| if (!func.getBody().hasOneBlock()) { | ||
| func.emitError("ZKLean conversion only supports single-block functions").report(); | ||
| state.hadError = true; | ||
| return false; | ||
| } |
tim-hoffman
requested changes
Jun 1, 2026
Member
|
@benoitrazet, this PR revealed a few scenarios that are not handled in the
|
91fd3be to
788f14b
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Fixes #495.
--convert-llzk-to-zkleanpreviously rejected unsupported operations only when they produced SSA results. Unsupported zero-result operations could therefore fall through without diagnostics, allowing constraint operations such asconstrain.inor zero-resultfunction.callto be omitted from the emitted ZKLean module while conversion still succeeded.This change makes the converter fail on every unhandled operation except an empty
function.return.Changes
function.returnas an intentional no-op during LLZK-to-ZKLean conversion.constrain.infunction.returnTesting
git diff --check