[WIP] Opinionated deployment of enhanced Requalify capabilities on AInvs #791

Xaphiosis · 2024-07-11T10:02:37Z

🦆🦆🦆 Temporarily only dealing with AARCH64; want feedback before applying to other arches.
(look at the top relevant "[wip]" commits only for now! this is supposed to be on top of the requalify changes #788 that are not yet merged, but since I'm making these PRs from my fork I can't stack them, lesson learned).

This yields a performance improvement (possibly due to context begin interpretation Arch . not being parallalisable by Isabelle):

AInvs after deploying tweaks:
glow: ( 0:13:50 real,  1:15:34 cpu, 13.13GB)
      ( 0:14:07 real,  1:16:58 cpu, 17.06GB)
pcr:  ( 0:08:30 real,  0:44:48 cpu, 16.97GB)

AInvs before requalify tricks:
glow: ( 0:17:17 real,  1:24:48 cpu, 16.01GB)
      ( 0:17:15 real,  1:25:41 cpu, 17.21GB)
pcr:  ( 0:14:13 real,  1:07:29 cpu, 10.46GB)

Here's what I changed:

global_naming AARCH64 -> arch_global_naming
try get rid of interpretation Arch . (slow) in lieu of (in Arch) (faster) or proper requalifying (nearly instant)
get rid of requalifications that were already requalified, or were global (thanks to new warnings) TODO: some of these will turn out to be broken because they're not actually global/exported on other arches
put arch_global_naming on same line as context Arch begin
annotate requalifications in Arch theories that can be moved to generic
put FIXMEs on unusual global_naming practices

Tracking TODOs for this stage:

change all FIXME arch_split to FIXME arch-split in entire repo to match github/project labels
add FIXME arch_split to PR linter to stop people reintroducing it
add arch_global_naming to the strange/missing Arch-only parts and fix fallout
use feedback from this PR to update docs/arch-split.md
deploy on other arches once approach is confirmed

lsf37 · 2024-07-12T00:56:04Z

proof/invariant-abstract/AARCH64/ArchDetype_AI.thy

-context begin interpretation Arch .
-lemma delete_objects_invs[wp]:
+(* generic consequence of architecture-specific details *)
+lemma (in Arch) delete_objects_invs[wp]:
  "\<lbrace>(\<lambda>s. \<exists>slot. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s


This one is less weird than I originally thought. It's in an Arch file and usually would be inside the big context Arch block that spans the entire file, but here it needed to be after the interpretation part that comes above. So it's mostly a "usual" Arch lemma that is getting exported and requalified.

Looks all good to me, and the new handling of the wp attribute is better.

The issue here is that the qualified name of delete_objects_invs becomes Arch.delete_objects_invs, instead of what we normally would do via global_prefix (AARCH64.delete_objects_invs). In this case that should be ok, because it's immediately requalified into the theory context (and also tagged [wp] for that context), but it's still a bit of a finicky policy to try canonise.

Got it. We don't seem to have many of these, and for exceptional cases I think this is Ok.

Would the 'canonical' approach be to export enough facts so that this can be proved in a generic file outside of Arch?

Yeah, I think exporting enough facts would be the right idea. Alternatively, this entire lemma could be made an assumption.
I think someone took a shortcut here, but I'm not clear on why exactly.

lsf37 · 2024-07-12T00:59:56Z

proof/invariant-abstract/AARCH64/ArchRetype_AI.thy

+(* FIXME arch_split: is there any way to optimise this interpretation out? we can't nest contexts *)
 interpretation Arch .


This is a bit funky. Either retype_region_proofs is supposed to be generic or not. There is retype_region_proofs_arch just above, so you'd think retype_region_proofs is the generic one, in which case it shouldn't do interpretation Arch and the lemmas should instead be inside retype_region_proofs_arch.

Changing it probably breaks something down the line, but it looks like an abstraction violation to me. Definitely good to put a FIXME here.

This one is beyond me, I think I'll leave it as a FIXME.

proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy

proof/invariant-abstract/AARCH64/Machine_AI.thy

lsf37 · 2024-07-12T01:05:28Z

proof/invariant-abstract/BCorres_AI.thy

+context Arch begin arch_global_naming
+
+crunch arch_post_cap_deletion
+  for (bcorres) bcorres[wp]: truncate_state
+
+end


Kinda neat that we can do this now in generic files, but also a little bit dangerous. Then again, it does remove duplication.

It is a travesty, I agree. However, what we had before (context begin interpretation Arch .) was just as bad, and a lot slower :/

This is definitely nicer.

I don't think it's worth doing with the BCorres files already being a bit of a mess of dependencies, but would our current preference be to assume this in a locale and move the proof to the arch file?

Yes, absolutely. I think this is an example of "no one likes BCorres, so it doesn't get the nice new toys". It got the worst approach. Then the next approach was the "Pre" thing, which also wasn't great, and then someone discovered the locale assumptions approach which I think is the one we should go with in any new proofs, barring maybe esoteric moments in Invariants-like files.

lsf37 · 2024-07-12T01:11:00Z

proof/invariant-abstract/CSpaceInvPre_AI.thy

-context begin interpretation Arch .
-lemma free_index_update_test_function_stuff[simp]:
+(* FIXME arch_split: exports properties of functions that are not necessarily in global context,
+   and then they get placed in the global simpset *)
+lemma (in Arch) free_index_update_test_function_stuff[simp]:


This is the slightly stranger case. We probably should avoid this kind of Arch lemma inside generic files. Then again, it has the same kind of remove-duplication benefit as the crunch (bcorres) we had elsewhere, so maybe we don't need to be too strict.

Thumbs up to making the name available so it can be removed from [simp] again if needed.

I think this is a result of the early approaches and "Pre" tech, I think we would try to avoid this in new files.

proof/invariant-abstract/CSpace_AI.thy

proof/invariant-abstract/DetSchedAux_AI.thy

proof/invariant-abstract/InvariantsPre_AI.thy

lsf37

This is pretty neat, and I really like the speed-up. I agree with the opinionated choices in here, and green light from my side to deploy it to the other architectures.

I don't think the missing global_naming parts were intentional. Most likely just forgotten and things happened to work anyway. I would add arch_global_naming.

Xaphiosis · 2024-07-12T01:25:22Z

This is pretty neat, and I really like the speed-up. I agree with the opinionated choices in here, and green light from my side to deploy it to the other architectures.

I don't think the missing global_naming parts were intentional. Most likely just forgotten and things happened to work anyway. I would add arch_global_naming.

Yay. Glad to hear it. Added the missing global_naming parts to TODO list.

proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy

proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy

corlewis · 2024-07-18T06:48:39Z

proof/invariant-abstract/ADT_AI.thy

+arch_requalify_consts (A)
  empty_context
  init_A_st
+
+arch_requalify_consts
  ptable_lift


Hmm, I hadn't considered that the new approach of not doing the interpretation means that when requalifying we need to be more specific about the naming. I guess this would fix itself if we were consistent, which the new arch_global_naming helps with. Either way, it's still a trade-off that seems worth making.

It is a bit annoying. I thought about ways to work around it, but then it turns out that I like the aesthetic of knowing whether something came from ASpec/ExecSpec or the proofs. With a bunch of work we could make the command be able to take the (A/H) on a per-id level, e.g. arch_requalify_consts empty_context (A) ptable_lift init_A_st (A) or something, but I'm not sure about how beneficial that would be.

Ah right, I hadn't stopped to realise that the A/H is only on things from the specs. That's not as bad as I first thought then, I was thinking it was due to us not being consistent with naming.

Still a bit annoying but I agree, probably not worth making the command more complicated to handle it.

corlewis · 2024-07-18T07:03:57Z

proof/invariant-abstract/CSpaceInv_AI.thy

+(* There are multiple arch-dependent acap_rights_update_id, one for wellformed_acap,
+   one for valid_arch_cap. Prefer the latter. *)


Not as part of this PR, but this sounds like something we should fix.

I'll take a look, you're right, something is off here.

fixed and added to PR

corlewis

I like this, the improved consistency and performance is definitely very nice! I generally agree with all of the existing FIXMEs and comments.

Currently, my remaining questions are around when requalifications need to be in Arch files, and when we're ok with Arch proofs in generic files. For the latter, it sort of seems like a sign that we've gotten the abstraction wrong, and should be exporting whatever else is needed from Arch so that the proof could be properly generic.

corlewis · 2024-07-23T00:42:24Z

proof/invariant-abstract/AARCH64/ArchRetype_AI.thy

-context begin interpretation Arch .
-requalify_consts post_retype_invs_check
-end
+arch_requalify_consts post_retype_invs_check


Requalification in an Arch file

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

corlewis · 2024-07-23T00:42:40Z

proof/invariant-abstract/AARCH64/ArchRetype_AI.thy

-context begin interpretation Arch .
-requalify_consts region_in_kernel_window
-end
+arch_requalify_consts region_in_kernel_window


Requalification in an Arch file

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

corlewis · 2024-07-23T00:42:53Z

proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy

-context begin interpretation Arch .
-requalify_consts replaceable_or_arch_update
-end
+arch_requalify_consts replaceable_or_arch_update


Requalification in an Arch file

Unavoidable: const introduced in Arch locale that needs to be referenced generically in this theory.

proof/invariant-abstract/AARCH64/ArchCSpaceInv_AI.thy

Xaphiosis · 2024-07-23T02:49:11Z

I think I addressed everything I could for the AARCH64 test run of rolling out these strategies. Next steps will be documentation update, then deployment to other arches, possibly involving other PRs that are cross-platform.

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms ("asms" is rarely expected outside of ML code) Signed-off-by: Rafal Kolanski <[email protected]>

* add warnings when exporting a name that already exists in theory context, suppressable by `(aliasing)` option * add `arch` variants of requalify commands that implicitly add the value of L4V_ARCH before whatever you give them, with optional suffixes for abstract (A) and Haskell (H) spec global naming. * write hopefully-understandable documentation with commented examples Signed-off-by: Rafal Kolanski <[email protected]>

Also document that requalify commands will issue warnings. Signed-off-by: Rafal Kolanski <[email protected]>

Stops namespace pollution, allows us to use Arch locale as example. Signed-off-by: Rafal Kolanski <[email protected]>

Temporarily only dealing with AARCH64; want feedback before applying to other arches. * global_naming AARCH64 -> arch_global_naming * try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)` (faster) or proper requalifying (nearly instant) * get rid of requalifications that were already requalified, or were global (thanks to new warnings) TODO: some of these will turn out to be broken because they're not actually global/exported on other arches * put arch_global_naming on same line as `context Arch begin` * annotate requalifications in Arch theories that can be moved to generic * put FIXMEs on unusual global_naming practices Signed-off-by: Rafal Kolanski <[email protected]>

* get rid of `global_naming Arch`, this is no longer needed since we can requalify directly from `arch_global_naming` with `arch_requalify` commands * add missing `arch_global_naming` for `context Arch`, for consistency

Rename the wellformed_acap version to wf_acap_rights_update_id, and the valid_arch_cap version to valid_acap_rights_update_id. Signed-off-by: Rafal Kolanski <[email protected]>

* prevent duplication between arches by moving requalifications from Arch theories to generic ones * this strategy is not available for new constants that are introduced in the Arch locale that need to be referenced in generic definitions or locale instantiations

* prefer arch_global_naming * prefer arch_requalify commands over interpretation * indicate consts might need to be requalified in Arch theories * explain (in Arch) + requalify pattern for generic consequences of arch-specific properties

Xaphiosis · 2024-07-26T03:48:12Z

Closed, full deployment now at: #805

Xaphiosis added enhancement proof performance making the proofs faster cleanup proof engineering nicer, shorter, more maintainable etc proofs labels Jul 11, 2024

Xaphiosis requested review from lsf37 and corlewis July 11, 2024 10:02

Xaphiosis marked this pull request as draft July 11, 2024 10:03

Xaphiosis marked this pull request as ready for review July 11, 2024 10:03

lsf37 added the arch-split splitting proofs into generic and architecture dependent label Jul 12, 2024