Faster requalify command for arch-split (`arch_requalify_*`?)

[Xaphiosis]

As seen in https://github.com/seL4/l4v/pull/771 there is a speed penalty for interpreting a locale. In the middle of AARCH64 AInvs doing this costs ~7.5s:

context begin interpretation Arch .

If we do one requalify per generic theory, that's going to add up, especially heading into Refine.

There is an alternative people have been using, which works only in Arch theories and thus needs to be duplicated for every arch, but is instant:

requalify_facts
  ARM.user_mem_dom_cong

This has the correct behaviour of exporting user_mem_dom_cong into the global context, having it still available as ARM.user_mem_dom_cong, and not available as Arch.user_mem_dom_cong.

The performance is nice, but having to put it into Arch files and duplicate it sucks, and is error-prone during the arch-splitting process. It would really be much better to have the requalifications all in non-Arch files, exactly once. This also makes sure we don't miss something, like if we need ioport-related constants to be introduced to other platforms for consistency, a requalify will catch their absence faster rather than in the middle of some downstream proof.

Proposal

We already have conventions for the default naming inside the Arch locale corresponding to $L4V_ARCH (e.g. ARM), the _A suffix for the abstract spec (ARM_A), and the _H suffix for the Haskell / design spec (ARM_H).

This means that even though the shortcut version of requalify_* appears to breach abstraction, it really doesn't, because it's roughly doing: requalify_facts $L4V_ARCH.user_mem_dom_cong

We can add new commands that correspond to requalify_facts, requalify_consts, requalify_types (less clear on the types than the others), which would do the correct expansion, i.e.

arch_requalify_facts user_mem_dom_cong (* requalify_facts ARM.user_mem_dom_cong *)
arch_requalify_consts blah (* requalify_facts ARM.blah *)
arch_requalify_types blah (* requalify_types ARM.blah *)
arch_requalify_facts (Haskell) user_mem_dom_cong (* requalify_facts ARM_H.user_mem_dom_cong *)
arch_requalify_facts (Abstract) user_mem_dom_cong (* requalify_facts ARM_A.user_mem_dom_cong *)

Issues

I made up the names and syntax of these commands, so feedback please.

The commands will error if the constant/fact/type isn't found, but it's less clear what we want when the name already exists in the global scope, because that will clobber the global name. Do we want a warning? In fact, do we want to add a warning to requalify_* commands when there's a collision? It's my understanding we never want a collision with the global/generic name and want to end up with Arch., meaning we don't do an interpretation and are supposed to do something like this instead:

context Arch begin

(* The following makes Arch.deriveCap refer to the architecture-specific constant. *)
requalify_consts deriveCap

(* This fixes naming order when the Arch context is interpreted so that it refers to the global/generic constant *)
context begin global_naming global
requalify_consts RetypeDecls_H.deriveCap
end
end

The above is somewhat painful to look at, though fortunately name collisions should be rare. There might be room here for improvement of the requalify_consts/facts command as well, but I don't yet see how, beyond adding that warning (if possible).

This might also lead us to have to have Arch_A and Arch_H (because how else would you disambiguate a collision where both names are exported as Arch.blah?), but I'm hoping it'll work out fine because we try to keep names_like_this separated from namesLikeThis for a reason.

@lsf37 @corlewis feedback please, @mbrcknl you might have some ideas/memories from when you were doing arch-splitting that you might want to throw our way too.

[Xaphiosis]

Preliminary version in progress in #788

[Xaphiosis]

arch_requalify_[consts|types|facts] deployment demonstrates non-trivial speedup for requalification without interpreting Arch locale.