arch-split Refine up to Invariants_H for AARCH64 (Draft)

[Xaphiosis]

🦆🦆🦆 This PR needs feedback before I deploy anything to the other arches or move further. In an attempt to make the diff a bit more useful for reviewing than "new files added with stuff", Invariants_H got duplicated into each of the new files, and then clobbered by the actual file contents.
Do not attempt to review the whole thing at once, or the "duplicate and move Invariants_H" commit which will be squashed into once all this works.
The Refine fixup commit is not really indicative of any policies I'm aiming for in the future, it's just there so Refine builds.
The plan is: once we are OK with the way things are done, I'll expand this PR with deployment to other arches, fix up CRefine, and then we can merge it to master before continuing the arch-split train.

Invariants_H gets split into 4 files processed in this order:
- InvariantsPre_H: initial setup
- ArchInvsDefs_H: arch-specific invariant property definitions
- Invariants_H: remains to store arch-generic
invariants/properties/lemmas
- ArchInvsLemmas: locale interpretations and arch-specific
invariant-related lemmas

Several lemmas/interpretations/locales got moved to InvariantUpdates_H in order to resolve dependencies without introducing more files.

AARCH64 Refine will build, but CRefine is currently broken.

[lsf37]

With the numbers unfolded, these would be arch specific (or at least mode/machine word size specific). If we could avoid unfolding cteLevelBits in the proofs, then the lemma would stay generic or would not even be needed. Not sure it's worth the hassle at this point, but might be worth a FIXME.

[lsf37]

Thinking more about it, the main reason why we tend to unfold these is because it is automatic for Isabelle to decide that e.g. 0 != 32, but it can't automatically decide that 0 * cteLevelBits != 1 * cteLevelBits. There is a mechanism somewhere for turning a concrete distinct list into a set of inequality simp lemmas. We could use that here, and prove distinct [0 * cteLevelBits, 1 * cteLevelBits, ...] once and use that. Then Isabelle should be able to do symbolically what it now needs the numbers for. I'll try find what that tool is called.

[lsf37]

Right, it's not a tool, and it's not merged yet, it's just an application of simplified. Here is an example:

l4v/proof/crefine/ARM/CSpace_C.thy

Lines 3064 to 3088 in dc2fd26

	lemma cap_tags_distinct:
	"distinct [
	cap_page_directory_cap,
	cap_notification_cap,
	cap_asid_control_cap,
	cap_small_frame_cap,
	cap_irq_handler_cap,
	cap_irq_control_cap,
	cap_sgi_signal_cap,
	cap_page_table_cap,
	cap_asid_pool_cap,
	cap_endpoint_cap,
	cap_untyped_cap,
	cap_zombie_cap,
	cap_thread_cap,
	cap_domain_cap,
	cap_reply_cap,
	cap_frame_cap,
	cap_cnode_cap,
	cap_null_cap
	]"
	by (simp add: cap_tag_defs)
	lemmas cap_tag_neqs =
	cap_tags_distinct[simplified] distinct_rev[THEN iffD2, OF cap_tags_distinct, simplified]

[Xaphiosis]

I've deployed something, it'll need review once I push it

[Xaphiosis]

Please see the eventual infrastructure and the FIXMEs about overlapping lemmas. It follows on from our discussion on MM about being unable to sort the conjuncts and remove the redundant ones, and I still don't know how to do that.

[lsf37]

👍 Happy with that for now. To make it nice, we probably have to adjust some of these TCB/CTE proofs quite a bit, which may even reach into spec changes. Something for some time in the future, but not for the current arch split pass.

[lsf37]

The setup overall looks good from my side. Nice job with the update locales! I have minor comments only. If we can keep the main cte cases lemmas generic (they should be if we can abstract the lemma over the word size), then I think we'll save ourselves some pain down the road in CSpace theories that should be mostly generic, but won't be if tcb_cte_case is not.

[corlewis]

Huh, not relevant for this PR but I'm mildly surprised that we don't have a Refine equivalent to AInvs' iarch_tcb. In AInvs that lets us reuse the pred_tcb_at machinery for vcpus as well.

[Xaphiosis]

Then no one did such a thing in rt either?

[corlewis]

Nope, rt so far has only been for architectures without hypervisor support, so there's never been a need for pred_tcb_at of an arch_tcb property.

[Xaphiosis]

This strikes fear into my heart

[Xaphiosis]

I fixed up non-proof items (including reverting the copyright changes) and added an explanation for the locale hierarchy based partly on Gerwin's explanation. Now I'll be looking at the proof changes, which will take longer.

[Xaphiosis]

I've attempted to address all the issues raised so far, responded to the comments and fixed up Refine so it builds again. I will try to fix up CRefine next while I'm waiting for round 2 of reviewing.

[Xaphiosis]

AARCH64 CRefine should be fixed now. That took longer than expected.

[lsf37]

I'm happy with the second round and with the proof changes.

[corlewis]

Out of curiosity, do you remember why this is needed?

[Xaphiosis]

It's needed in the two lemmas below, where we have that Isabellism of

[| blah ==> thesis; asm1; asm2 |] ==> thesis

and this rule is what I came up with to unscrew that. If there's a nicer way, please let me know. This pattern comes up when using obtain which is from Isar. The HOL way, we'd get an existential.

[Xaphiosis]

@corlewis I have squashed the commits resulting from PR discussion, so we're back to disjoint commits for your review:

1. clone Invariants_H
2. interesting arch-split updates to split Invariants_H
3. boring Refine updates to make Refine work
4. mostly boring updates to make CRefine work (some excitement in Move_C)

[corlewis]

It's a bit complicated since it depends on what is now an arch lemma, but should this be generic?

Looking ahead, it's declared [simp] in Schedule_R, so I think at the very least at some point it will need to be requalified. It might even be worth making it [simp] to start with, although as always that might cause extra pain if we do it at the same time as everything else.

[Xaphiosis]

Good catch. Yes, that should become an interface lemma and be requalified, it's a generic consequence partly based arch-specific results, something we expect all arch stuff to conform to

[Xaphiosis]

I will probably leave the [simp] for now, and re-examine when I get to the declare

[corlewis]

Probably not worth doing and definitely not as part of this PR, but some of these pspaceI_assms lemmas feel like they would have the same proof on all architectures and could be generic if the interface was a bit lower down.

[Xaphiosis]

That's very possible, but it will require effort and I'm thinking it won't save all that many lines. We'll see if any other arch comes into conflict, I'll keep your comment in mind.

[corlewis]

A note for the distant future, I think that this will be a problem in rt with the more complicated typ_at_lifts setup we have there. I think for that we might want to add locales and do the arch-split dance between Invariants_H and ArchInvsLemas_H.

Probably not worth the effort, but in a perfect world it would be nice to pull that setup back to master to test out arch-splitting it there (and to reduce the difference between the two branches).

[Xaphiosis]

I don't quite understand. What kind of setup does rt have? If it cheers you up, gen_typ_at_lifts is so far unused, it's only the consequence of hiding the arch-specific ones under typ_at_lifts in Arch, and I left this behind as a precaution.

[Xaphiosis]

Given your comment and how it's unused, should I remove it to prevent a derp later?

[corlewis]

In rt we have a couple of locales that contain all of the typ_at' lifting rules and that are then interpreted as needed for any function that preserves typ_at'. See the whole section building up to https://github.com/seL4/l4v/blob/rt/proof/refine/RISCV64/Invariants_H.thy#L2777 if you're particularly curious. When it comes time for it to be arch-split, I imagine we'll want to keep as much of that generic as possible to reduce duplication and risk of de-sync.

[corlewis]

Given your comment and how it's unused, should I remove it to prevent a derp later?

Hmm, sorry, it wasn't actually specifically gen_typ_at_lifts that I was commenting on, more the general approach with typ_at_lifts being in Arch. I just put this here as the place where some of it is made generic again, I don't think removing it is relevant to my thoughts.

[Xaphiosis]

In that case, they'll end up more like the _upd locale hierarchy? I.e. locales get declared, we do what we can in generic, then add on the rest in Arch, and then (sigh) any stragglers that need the Arch ones in the next generic theory ... hmm. I wish there was a nicer way.

[corlewis]

Right, comparing it to the _upd locales makes sense and that does give us an approach to follow when we get up to that. Hopefully it ends up being not too bad.

[corlewis]

Hmm, I understand that this is a convenient location due to the import graph, but these requalifies being put here does feel like a bit of a negative consequence of how we're doing this arch-split. They don't really have any connection with the rest of this file and feel pretty disconnected to Invariants_H and ArchInvsLemmas_H, which are the files that actually relate to them.

I don't have any better suggestions so am fine to leave them here for now, but I can imagine negative consequences going forwards, where we make changes or add new lemmas to ArchInvsLemmas_H and don't think to change here as well, resulting in a new, inconsistent approach.

[Xaphiosis]

I agree it's not ideal. The issue is the second best place to put them is inside the Arch file, and then there's a risk of de-sync between arches (not that bad in general, but not fun when doing the arch-split itself).
Another way is to use locales, which is something that I'll be aiming for for the rest of the files, but for invariants the dependency graph was a bit much. Maybe I can add a comment to clarify or something?

[corlewis]

Ah right, I hadn't thought of this being specifically an artefact of the complicated invariants files.

[corlewis]

This looks good to me as well and I just have minor comments or notes for the future. Thanks for also taking the opportunity to move things around to be more localised and have a better structure overall!