Refine+AInvs: performance improvements (clear_named_theorems, avoid interpretation Arch and interpret Arch) - #1047
Open
Xaphiosis wants to merge 7 commits into
Open
Refine+AInvs: performance improvements (clear_named_theorems, avoid interpretation Arch and interpret Arch)#1047Xaphiosis wants to merge 7 commits into
Xaphiosis wants to merge 7 commits into
Conversation
Allows an existing named_theorems to be cleared and then re-used, allowing the construction of re-usable theorem accumulators. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
By using clear_named_theorems, we will re-use this dynamic named theorems set to satisfy Arch interface locale assumptions. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
added
the
arch-split
Clear out uses of `named_theorems *_assms` and adding theorems to these assms in lieu of clearing + using Arch_assms. Greatly reduces attribute namespace pollution. Additionally: * remove all remaining occurrences of `interpret Arch .` in Refine * export Arch_assms to appropriate lemmas set for use in interpreting Arch interface locales * add some missing (* Arch *) tags * clean up confused naming of KHeap_R_assms_2 * named_theorems used to perturb naming schemes; now that we don't introduce new named_theorems, global.some_def now gets picked up as the default again Use `fact L4V_ARCH.whatever_assms` instead of `fact whatever_assms` when satisfying locale assumptions. Since `whatever_assms` no longer exists, we use a `lemmas` statement to exfiltrate the assumptions from the Arch locale without interpretation, resulting in a performance improvement. Used the following .sed script for removing named_theorems and relevant _assms references. Please recombine commands into a single line, the first is split to satisfy gitlint: ``` /Arch_assms/!s/named_theorems \([A-Z]\w\+\)_assms/ clear_named_theorems Arch_assms (* accumulate assumptions for \1 locale *)/ /Arch_assms/!s/\(\[\)[A-Z]\w\+_assms/\1Arch_assms/ /Arch_assms/!s/[A-Z]\w\+_assms\(\]\)/Arch_assms\1/ ``` Used the following sed command to add the specific arch prefix to `fact whatever_assms`; e.g. for AARCH64 it ends up as AARCH64.whatever_assms when we do this in proof/refine: ``` sed -i -e '/Arch_assms/!s/fact \([A-Z]\w\+_assms\))?/fact AARCH64.\1)?/' \ AARCH64/*.thy ``` Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
The ones in LevityCatch did not need exporting, and the ones in ArchInvsLemmas only needed importing a simp rule or two from Arch. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Clear out uses of `named_theorems *_assms` and adding theorems to these assms in lieu of clearing + using Arch_assms. Greatly reduces attribute namespace pollution. Additionally: * remove all remaining occurrences of `interpret Arch .` in AInvs * export Arch_assms to appropriate lemmas set for use in interpreting Arch interface locales; for AInvs, this required a bit of creativity in places Please see recent "refine: use Arch_assms in lieu of named_theorems" commit for the sed scripts and commands used as a base for these changes. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
For ArchRetype_AI we are still left with the two instances of `interpretation retype_region_proofs_arch ..` which are slow. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Due to cleanup of `interpretation Arch .` in AInvs certain facts were not leaked by default. In this case, vs_lookup_table' did not make it from retype_region_proofs_arch to retype_region_proofs. This solves the immediate issue, and doing an arch-based locale interpretation right after a `interpretation Arch .` does not incur a slowdown. In the longer term, `interpretation Arch .` is slow, and the interaction between retype_region_proofs_arch and retype_region_proofs should be overhauled. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Xaphiosis
changed the title
lsf37
reviewed
Aug 23, 2026
| Going via Local_Theory.declaration does work, even if we have to give it a "morphism" that | ||
| doesn't actually contain a morphism. *) | ||
| fun alt_proof_map f = | ||
| Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn _ => f); |
Member
There was a problem hiding this comment.
I'd probably replace (fn _ => f) by (K f) as the more usual form in the Isabelle sources.
alt_proof_map is not really the right name, because proof_map is exactly not the thing we're doing. Looking at the code of Local_Theory.declaration, proof_map is just one of multiple primitive steps in there. Basically proof_map is a primitive lifting operation, and declaration does all of the actual context handling of the locale. What we're doing really is a declaration command like a declare (and we're also giving the keyword type thy_decl, which is correct), so maybe local_declare as a name? The morphism is safe to ignore in this case, because we are not referring to any locale fixes or anything like that, so there is nothing to transform.
lsf37
reviewed
Aug 23, 2026
| val _ = | ||
| Outer_Syntax.local_theory \<^command_keyword>\<open>clear_named_theorems\<close> | ||
| "clear named collection of theorems" | ||
| ((Parse.name_position) >> |
Member
There was a problem hiding this comment.
(Parse.name_position) -> Parse.name_position
lsf37
reviewed
Aug 23, 2026
Comment on lines
+570
to
+571
| (* FIXME arch-split: koType_asidpool and koType_pte are somehow [simp] even outside Arch on AARCH64 | ||
| due to how pre_storable *) |
Member
There was a problem hiding this comment.
The sentence is cut off. Due to how pre_storable works?
lsf37
reviewed
Aug 23, 2026
Comment on lines
+575
to
+576
| instance by intro_classes | ||
| (auto simp: AARCH64_H.arch_kernel_object_type.distinct) |
Member
There was a problem hiding this comment.
Indent seems slightly off in the second line in GitHub view. The ( should be under the I of intro_classes (globally in this commit). If that's the case already, please ignore.
lsf37
approved these changes
Aug 23, 2026
lsf37
left a comment
lsf37
left a comment
Member
There was a problem hiding this comment.
Very nice!
So much name space pollution removed, I'm glad you pushed for looking into this.
Member
Author
|
Updated PR description with benchmark. Will deal with PR comments after weekend. |
Member
|
Those are some pretty nice numbers, X64 is getting a real boost. Not sure why RISCV64 isn't seeing that much improvement, but overall it is an excellent picture. |
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.
Please review commit-by-commit. The "big" commits really consist of tiny changes to many files.
Introduce the
clear_named_theoremscommand plus tests/documentation, then use it to get rid of all the named_theorems declarations throughout Refine, in lieu of a single Arch_assms which we re-use every time we want to accumulate Arch interface locale assumptions. Then we export it to a lemma name which we can access directly from outside Arch in order to interpret the interface locale.This means
print_attributesisn't going to be a flood of all the named_theorems.The name perturbations that named_theorems produced are now gone, so I had to put back the arch prefixes I previously had to remove when I introduced the named_theorems uses in Refine.
A few small cleanups snuck in, and then I managed to remove every single
interpret Arch .andinterpretation Arch .in Refine.Then I did the same thing for AInvs. There was more turbulence, but once again, no more
interpret Arch .orinterpretation Arch .remains.Benchmarks are in progress (I wrote a tool, Corey is helping me test it), but it's definitely an improvement. E.g. internal isabelle timing reports around 8.5 minutes for RISCV64 Refine vs around 9 before this change (on my fast main machine).
@ryybrr : tagging you since you'll probably want to copy this for InfoFlow at some point; I can assist.
Benchmark
Comparison of current master (f494027) and named_theorems optimisation branch (August 2026). Times are session processing times as reported by Isabelle in seconds, do not confuse them with run_tests times. Benchmark ran on
pcr( i9-12900K) using 8 max threads. Times are average of 5 runs after an initial warm-up.Benchmark Discussion
Overall, this saves 9.2 minutes of real time across the three images, and 57 minutes of CPU time. As expected, the major improvement is Refine, with between 5.8% to 16% real time speedup. AInvs still benefited, with 0.3% to 4.9% speedup, and CBaseRefine got a marginal boost.
Apparently, clearing the pipeline stall during an
interpret Arch .when interpreting an interface locale only results in a larger improvement when there is something to shove into the pipes before the next stall. InCBaseRefinewhich is running with skip proofs on, there isn't a lot. InAInvs, theinterpretdoesn't take as long, it only really becomes more expensive when we hitRefine. Nonetheless the 0.3% improvement on RISCV64 AInvs is unexpectedly low. Standard deviation on that run is under 1s, so it's not jitter.Another possibility is that the Refine arch-split is very aggressive, significantly reducing the amount of arch-specific proofs, and so relying on interfaces more.