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.

[corlewis]

Very nice job collecting and rationalising these locales!

Just trying to think of what might help us in the future, do we want a comment here with a quick explanation of what we mean by idempotence over field updates, and maybe with an explanation that the locales are actually populated and interpreted in Invariants_H? It would be harder to explain here, but it might also help to have a comment explaining that completing the lattice is helpful to avoid future 'landmines', even if some of the locales aren't used now.

More ambitious ideas that almost definitely aren't worth the time would be to have some sort of test that confirms that the lattice is complete, and to have a new tool that constructs the lattice given Arch and the base locales.

[Xaphiosis]

comments added

[lsf37]

I'm happy with the new comments.

[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]

Yes, I think that would be useful in proofs about those specific generic object types.

[Xaphiosis]

done, but check how I did it, it's a bit height-reduced

[lsf37]

I think that's fine. We'll have to remember to update the number in gen_objBitsT_simps when we add a generic object, but I think that's reasonable.

[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]

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.

[corlewis]

Suggested change

	This means that for every one the update locales, we have to add an additional Arch locale.
	This means that for every one of the update locales, we have to add an additional Arch locale.

[Xaphiosis]

Thanks, fixed, will include in next round.

[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]

Cool. In the distant future, this could potentially be the form that we do not unfold further in other proofs and that the tcb cases then use everywhere. With that, there would be at least some hope that it is symbolic enough to not reduce to the same terms in tcb_cte_cases_neqs and therefore get rid of the warning (and the additional simplification work Isabelle has to do in each proof).

[Xaphiosis]

I'm not following by what you mean here. If you mean that we don't unfold the tcbCTableSlot etc so we end up only needing these versions, then that would be nice, and would indeed not cause duplication in the _neqs lemma, which does normalise things around 0 and 1. Don't think Distinct_Cmd will help much with that, it will either give a result not in simp normal form, or if we use [simplified], duplicates as before.

[Xaphiosis]

I pushed a fix for this, which also removes the FIXMEs. Playing around with Distinct_Cmd didn't really improve over distinct [] and your attribute hack, but I guess it in theory could work around the attribute hack if it wasn't so awkward to use.

[lsf37]

If you mean that we don't unfold the tcbCTableSlot etc

Yup, that's what I meant. I don't know where exactly the unfoldings come in, but in old code it could already be at the spec level. In any case, that's for another time.

Nice work on removing the duplicates!

[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)