Improve reasoning about heaps #3931
Open
unp1 wants to merge 15 commits into
Open
Conversation
unp1
marked this pull request as ready for review
July 14, 2026 19:31
unp1
force-pushed
the
bubel/heap-simplification
branch
6 times, most recently
from
July 21, 2026 09:22
8febe7a to
ab6eaa7
Compare
unp1
force-pushed
the
bubel/heap-simplification
branch
2 times, most recently
from
July 21, 2026 20:35
82d2622 to
5424fff
Compare
unp1
enabled auto-merge
July 21, 2026 20:35
Drodt
self-requested a review
July 22, 2026 08:19
Drodt
requested changes
Jul 22, 2026
unp1
disabled auto-merge
July 22, 2026 20:45
unp1
force-pushed
the
bubel/heap-simplification
branch
4 times, most recently
from
July 22, 2026 23:33
76d70f4 to
7a6553a
Compare
…not supported by the taclet soundness po generator)
The rule-application queue returns mostly bases: candidates whose \assumes
formula is not yet present in the sequent. On large proofs about 97% of all
queue pops are such bases, and re-matching them almost never yields an
applicable rule, so the queue spends most of its time confirming that
nothing changed.
A base is now parked: set aside under wake keys that describe the formula it
waits for, and woken exactly in the round in which a matching formula is
added or changed. The keys are derived from the taclet's own compiled
matcher (PatternKeySource, computed from the same per-operator dispatch the
matching runs on), so what a key accepts cannot drift from what the matcher
accepts. Four key kinds refine precision, from the top operator family down
to the renaming-invariant hash of a concrete first argument; modality-headed
formulas stay on the coarse operator key so no hash ever walks a program.
The parked state lives in ParkedBases, one instance per goal, with
insertion-ordered containers throughout: operator hash codes differ between
runs, and a hash-ordered iteration would leak that difference into the wake
order and the proof. Dead bases are swept periodically to bound the memory
they hold. Waking too eagerly is harmless, the base fails to match and is
parked again; the class comment argues why a wake is never late. The proofs
found are statistics-identical to the unparked queue across the RunAllProofs
suite.
Wake keys speak one vocabulary, operator families
(JavaMatchPlanBuilder.matchFamilyOf): an operator stands for itself, a
parametric function instance for its base, a modality for its kind, and only
schematic operators name nothing. The family is position-relative in one
respect: the top of a candidate is observed after its leading updates are
removed (they are the find's update context), every other position as
written. An \assumes whose first argument is an update application, as in
\assumes(p({u}x) ==>), therefore parks under the update application family
and is woken exactly by the formulas whose first argument carries one;
without the update family such a base was stored under a key no formula
produces and was never woken. No shipped taclet has this shape, so the
RunAllProofs suite is rule-application-identical; the shape is reachable
through user-loaded taclets and is pinned by the self-wake test.
The parked counts are checked against the map in the dead-base sweep, which
walks the map anyway, and the wake order carries an assertion that it lists
every kind: a kind missing there would silently never wake its bases.
The wake cycle, the wake order, the release on waking and the sibling
locality of the per-head counts are pinned by unit tests over real taclet
applications.
with AI tooling support
The deterministic tie-break on equal-cost rule applications compares sequent formulas by walking their operator names. On large sequents these walks compare the same formulas over and over. JTerm.nameHash() folds the operator names and arities of all subterms into a cached hash and contains nothing else. Unlike hashCode() it excludes term labels, whose hash can embed object identity, so the value is identical across JVM runs, which every key in the proof-search order must be. The formula comparison orders by this hash first and falls back to the name walk only on equal hashes. The comparators are package-visible, so the order property tests call them directly. with AI tooling support
An anonymous class cannot be annotated, so the locality lookup climbs to the first named class for anonymous ones. Named classes still declare their own locality, because a subclass's overrides may change what the cost depends on. with AI tooling support
Two bugfixes in TermImpl. depth() compared each subterm's depth against the cache field, which is -1 while the value is being computed, so every comparison succeeded and the result was the depth of the last subterm plus one instead of the maximum. A regression test pins both argument orders. containsJavaBlockRecursive() answered false for a modality whose program has no statements. The modality is still part of the term and its JavaBlock still carries meta information such as PositionInfos, so such terms must not be treated as program-free (they are excluded from term caching for exactly that reason). The marker now reports every modality; a regression test covers the empty-program case.
Five independent changes on hot paths of the proof search, none of which changes any proof. OneStepSimplifier spreads its replace-known map over the renaming-invariant term hash instead of a coarser key, so lookups hit fewer collisions. CountOccurrencesFeature counts occurrences with a direct depth-pruned walk of the sequent instead of instantiating the generic term-generator machinery per query. TypeConverter looks up theories by class instead of scanning a list, and PredictCostProver fetches the integer theory once per prediction run instead of per literal. The duplicate-application veto rejects unequal terms by their cached renaming-invariant hash before entering the label-insensitive comparison walks; terms carrying a program are excluded, their hash would walk the whole program. ContainsExecutableCodeTermFeature answers false without walking the term when the cached contains-program marker already says the term is program-free (the query variant keeps walking, queries are function symbols and not covered by the marker). partially with AI tooling support
One is only termporart. But all of them have been proven to improve performance significantly (not just by a few percent) with AI tooling support
Makes triggers theory aware and improves the quality of the produced instantiation candidates by rejecting unhelpful ones and improving precision on detecting helpful instantiations. It also assigns cost tiers to found candidates to distinguish candidates more likely to help from others. The congruence orientation, the polarity walk and the minimal-cover search are pinned by unit tests. with AI tooling support
- The classic option is the safe fallback (which might go away once trust into the new ones is established) The option is resolved once when a strategy is built, like every other strategy option: the instantiation generator, the prediction feature and the tie-break feature receive it at construction instead of reading the proof settings per candidate, and the trigger-set cache records which supports built an entry, so a lookup under the other setting rebuilds it. with AI tooling support
…rprint The veto that rejects a rule application already performed on the branch scans a bucket of applied applications that share the candidate's focus-term fingerprint. The fingerprint has to agree with the equality the bucket is probed with, which compares focus terms modulo irrelevant term labels: a duplicate whose focus differs only in a label (origin labels, for instance, carry where a term came from) must land in the candidate's bucket, or it escapes the veto. A not so nice caveat is that we introduce another cached hashcode. The field will only be temporary and can be removed once the normal hashcode is label agnostic PR #3884. The hash discriminator invariant of the tie-break, the agreement of its two comparators and the label blindness of both ordering hashes are pinned by a property test. with AI tooling support
This reduces the locking overhead for single core and also multi-threaded proving significantly. Contrary to intuition the loss of cache sharing between goals (and workers) does not hurt performance, but improves it.
…autopilot only and a saved proof
unp1
force-pushed
the
bubel/heap-simplification
branch
from
July 23, 2026 05:38
7a6553a to
6d8a1af
Compare
unp1
enabled auto-merge
July 23, 2026 10:11
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
2 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.
Intended Change
General performance improvements in particular for heap heavier programs. Its improvements contribute to finding smaller proofs.
This PR consoliates the previous performance PRs (cleaning out the last remnants of my AI stint ;-).
It provides SC and MC speed-up compared to current main. The focus is in particular on verification of heap-heavy programs with lots of heap manipulations
(M: Main, P: This PR, SC: Single Core, MT 4x: Multithreading 4x; measurements taken on a warm JVM; all times are proving times (automode))
(Main, SC)
(PR, SC)
(Main, MT 4x)
(PR, MT 4x)
(no forks,
does not include bike/bet)
Type of pull request
Ensuring quality
Additional information and contact(s)
Parts done with AI tooling support.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.