Repository navigation
perf(reduction): drop a dead let binding without reducing its value - #1216
Merged
Merged
Conversation
strub
force-pushed
the
fix/dead-let-reduction
branch
2 times, most recently
from
October 26, 2026 08:21
501e4ee to
022840b
Compare
This was referenced Oct 26, 2026
strub
added
the
stacked
strub
changed the title
strub
force-pushed
the
fix/dead-let-reduction
branch
from
October 26, 2026 12:02
022840b to
f89c677
Compare
bgregoir
reviewed
Oct 26, 2026
The iota rule for a let-tuple required the bound value to be a syntactic tuple and otherwise asked for the reduction of the value, even when none of the bound variables occurs in the body; a dead let introduced by wp for a tuple assignment (the flags of an x86 instruction) was then fully evaluated before being thrown away. The zeta, let-tuple and let-record rules now return the body at once when the binding is dead.
strub
force-pushed
the
fix/dead-let-reduction
branch
from
October 26, 2026 14:25
f89c677 to
66394a1
Compare
strub
removed
the
stacked
strub
enabled stacked auto-merge
October 26, 2026 14:38
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.
First of a stack of three performance fixes found while checking safety proofs of Jasmin AVX2 implementations (ML-KEM, ML-DSA), where the goals produced by
wpon unrolled vector code hold thousands of let bindings.A let binding none of whose variables occurs in the body is dropped without its value being reduced. The let-tuple iota rule required the value to be a syntactic tuple and otherwise reduced it, even when the binding was dead (the flags of an x86 instruction bound by
wp); the zeta and let-record rules substituted or reduced as well. The three head rules now return the body at once when the binding is dead; the sub-term reduction of a let is unchanged (value first, then body).tests/reduction-dead-let.ecexercises the rules insimplify; it fails onmainat its first lemma.Stack: this PR, then #1217 (
cbv), then #1218 (read/write sets).