feat(legalization): make llvm.add widening proof width-generic (bounded) - #1471
Merged
Merged
Conversation
naveen-seth
force-pushed
the
naveen/legalization-generic-widening
branch
from
September 15, 2026 10:24
26a1a9b to
dbb6e8e
Compare
luigirinaldi
left a comment
luigirinaldi
left a comment
Contributor
There was a problem hiding this comment.
LGTM! modulo the minor nit. The constructor ... is a bit ugly atm could also be replaced by:
refine ⟨by simp, fun _ _ => ?_⟩
intros
pbv_decide 16
bv_decide
More in general I should fix pbv_decide to handle it without any of this trickery.
naveen-seth
force-pushed
the
naveen/legalization-generic-widening
branch
from
September 16, 2026 16:57
ffbc5af to
3b3babe
Compare
Contributor
Author
|
After #1475 has landed, the performance should be good enough to increase this to 64 bit. |
This makes the add_widening proof generic over widths up to a bounded limit using pbv_decide. This is currently bounded to 16 bits for performance reasons; large widths (around 64 bits and above) time out. Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
naveen-seth
force-pushed
the
naveen/legalization-generic-widening
branch
from
September 22, 2026 10:43
4186fa8 to
833be49
Compare
naveen-seth
enabled auto-merge
September 22, 2026 10:43
axelcool1234
pushed a commit
to axelcool1234/veir
that referenced
this pull request
Sep 23, 2026
…c (bounded)" (opencompl#1524) Reverts opencompl#1471 Auto-merge seems to go through even when the CI fails.
tobiasgrosser
pushed a commit
that referenced
this pull request
Sep 24, 2026
…ed) (#1471) This makes the add_widening proof generic over widths up to a bounded limit using `pbv_decide`. This is currently bounded to 16 bits for performance reasons; large widths (around 64 bits and above) time out. --------- Co-authored-by: Luigi Rinaldi <82770895+luigirinaldi@users.noreply.github.com>
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
3 participants
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.
This makes the add_widening proof generic over widths up to a bounded limit using
pbv_decide.This is currently bounded to 16 bits for performance reasons; large widths (around 64 bits and above) time out.