Repository navigation
perf(smt): memories as abstract values, local variables as functions of them - #1222
Merged
Merged
Conversation
…of them
A memory with local variables was translated as a why3 pair of the tuple
of all its locals and an abstract memory, and a local `x{m}` as a
projection of the first component. why3's `eliminate_algebraic` then
expands the tuple type in every task: for a Jasmin extraction with 162
locals (the `param_k`/`result_k` of the extracted procedures), a single
`x{hr}` in a hypothesis adds 162 projection definitions and a 27 000-line
inversion axiom, 3.4 MB of SMT-LIB per call, 2 s of printing and parsing
for goals the provers close in milliseconds.
A memory is now the abstract type `memory` whatever its memtype, and a
local variable an uninterpreted function `x : memory -> ty`, created once
per name and type (`te_lvar`), as global variables already are
(`te_xpath`). The argument variable `arg` is the tuple of the functions of
the declared parameters (a single parameter is `arg` itself); `glob M` and
`Pr[...]` take the whole memory. `tests/smt-memory-locals.ec` covers
locals, `arg` and its projections, a single parameter, `={arg}` in an
equiv, and the memories of `Pr` statements.
On the Keccak safety proofs of jasmin-nist, a prover call goes from 2.2 s
to 0.1 s (47 KB task), the AVX2 file from 140 s to 32 s and the scenario
of 49 files from 221 s to 135 s elapsed. `unit` and `stdlib` pass.
The loop-body step of PIR_s_uniform in examples/PIR.ec closed by a
prover call that found its instances of the restriction lemmas with some
prover versions only; two step lemmas (restr_addS_eq, restr_S_eq) now
rewrite the goal to a propositional one.
strub
force-pushed
the
perf/smt-memory-locals
branch
from
October 28, 2026 14:59
a57e282 to
773b750
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.
Found while speeding up the Keccak safety proofs of jasmin-nist: a prover call in a
hoaregoal costs about 2 s although the same arithmetic alone is closed in 30 ms. The SMT-LIB file sent (EC_SMT_DEBUG=1) is 3.4 MB, 166 000 lines.A memory with local variables is translated as a why3 pair of the tuple of all its locals and an abstract memory, and a local
x{m}as a projection of the first component (trans_memtype,trans_pvar). why3'seliminate_algebraicexpands the tuple type in every task: a Jasmin extraction has 162 locals (theparam_k/result_kof the extracted procedures), so a singlex{hr}in a hypothesis adds 162 projection definitions of 495 lines each and a 27 000-line inversion axiom. The provers close the goal in milliseconds; the time goes to printing and parsing.A memory is now the abstract type
memorywhatever its memtype, and a local variable an uninterpreted functionx : memory -> ty, created once per name and type (te_lvar), as global variables already are (te_xpath). The argument variableargis the tuple of the functions of the declared parameters (a single parameter isargitself);glob MandPr[...]take the whole memory. The abstraction is sound: any assignment of the locals is a choice of these functions.tests/smt-memory-locals.eccovers locals,argand its projections, a single parameter,={arg}in an equiv, and the memories ofPrstatements.Measured on the Keccak safety proofs: a prover call goes from 2.2 s to 0.1 s (47 KB task), the AVX2 file from 140 s to 32 s and the scenario of 49 files from 221 s to 135 s elapsed at 4 jobs (733 s to 465 s cumulative). Three closers of that scenario relied on an instance of a hint lemma the provers found in the old task on some runs only; they now state it.
unitandstdlibpass.The CI of the first push failed on two prover calls whose instances were found with some prover versions only: the loop-body step of PIR_s_uniform in examples/PIR.ec (fixed here: two step lemmas on restr rewrite the goal to a propositional one) and a map-invariant step of ec-xsalsa Cascades.eca (an explicit proof, passing with both binaries, is to be proposed to its maintainer).