Repository navigation
perf(cbv): drop a dead let binding without evaluating its value - #1217
Merged
Merged
Conversation
strub
added
the
stacked
This was referenced Oct 26, 2026
strub
force-pushed
the
fix/dead-let-cbv
branch
2 times, most recently
from
October 26, 2026 12:05
5b02c9f to
31edecf
Compare
bgregoir
approved these changes
Oct 26, 2026
strub
force-pushed
the
fix/dead-let-cbv
branch
from
October 26, 2026 14:25
31edecf to
541f545
Compare
strub
removed
the
stacked
strub
enabled stacked auto-merge
October 26, 2026 14:38
github-merge-queue
Bot
removed this pull request from the merge queue due to a conflict with the base branch
Oct 26, 2026
The call-by-value normaliser evaluated the value of every let binding before its body. A binding introduced by wp for a dead assignment (the flags of an x86 instruction, a register accumulated across an unrolled loop) had its value fully evaluated before being discarded; on 256-bit vector code this took minutes where the rest of the goal takes seconds. A binding none of whose variables occurs in the body is now dropped at once, and a preliminary pass drops the dead bindings of the goal from the inside out, so that a chain of bindings only feeding a dead one disappears as well.
strub
force-pushed
the
fix/dead-let-cbv
branch
from
October 26, 2026 16:02
541f545 to
df096c5
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.
Second of a stack of three performance fixes (after #1216) found while checking safety proofs of Jasmin AVX2 implementations.
The call-by-value normaliser evaluated the value of every let binding before its body. A binding introduced by
wpfor a dead assignment (the flags of an x86 instruction, a register accumulated across an unrolled loop) had its value fully evaluated before being discarded; on 256-bit vector code this took minutes where the rest of the goal takes seconds. A binding none of whose variables occurs in the body is now dropped at once, and a preliminary pass drops the dead bindings of the goal from the inside out, so that a chain of bindings only feeding a dead one disappears as well.tests/reduction-dead-let.ecgains the same cases proved bycbv.