Repository navigation
perf(pv): walk the call graph once in the read and write sets of a procedure - #1218
Merged
Merged
Conversation
strub
force-pushed
the
perf/pv-call-graph
branch
from
October 26, 2026 12:02
f59abcc to
9d0b8db
Compare
strub
force-pushed
the
perf/pv-call-graph
branch
from
October 26, 2026 12:05
9d0b8db to
a99024a
Compare
bgregoir
approved these changes
Oct 26, 2026
strub
force-pushed
the
perf/pv-call-graph
branch
from
October 26, 2026 14:25
a99024a to
4781a6d
Compare
strub
enabled stacked auto-merge
October 26, 2026 14:38
github-merge-queue
Bot
removed this pull request from the merge queue because a pull request earlier in the stack was removed
Oct 26, 2026
strub
force-pushed
the
perf/pv-call-graph
branch
from
October 26, 2026 16:02
4781a6d to
31cf80b
Compare
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.
…ocedure The variables read or written by a procedure were collected by a walk of its call graph as a tree: a procedure reached through several callees was visited once per path, so the walk was exponential in the depth of the sharing. On a program whose procedures share many helpers (an implementation extracted from Jasmin), the computation of these sets by `call`, `seq`, `while` or `conseq` took longer than the proof itself. The walk now skips the procedures already visited.
strub
force-pushed
the
perf/pv-call-graph
branch
from
October 26, 2026 16:06
31cf80b to
616a21b
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.
Last of a stack of three performance fixes (after #1216 and #1217) found while checking safety proofs of Jasmin AVX2 implementations, whose procedures share many helpers.
The variables read or written by a procedure (
EcPV.f_write,f_read) were collected by a walk of the call graph as a tree: a procedure reached through several callees was visited once per path, so the walk was exponential in the depth of the sharing. On the ML-DSA safety model (about 300 procedures, 900 call sites), the frame computed bycalltook longer than the rest of the proof. The walk now threads the set of procedures already visited and skips them; the public functions keep their signature.With the three fixes, the ML-DSA-65 safety proof checks in two minutes; lemmas did not finish in 20 minutes before. The
unit,preludeandstdlibscenarios pass on the stack.