design: deploy arch_requalify infrastructure

* make global_naming implicit (based on L4V_ARCH)
* avoid unnecessary Arch context interpretation (slow)
* change inclusion point of MachineExports to Types_H and eliminate
  duplicated requalifications
* migrate some Arch-theory requalifications to generic (more consistent
  interface)
* document some name clash disambiguations
* annotate vcpu type which can't be moved there, and leave vmrights
  which is needed for enum instantiations (can't be done in a locale)
* unify interface for initIRQController and maxIRQ by providing
  abbreviations in _H global_naming
* do not import generic constants sanitiseRegister and
  getSanitiseRegisterInfo; their definitions were never imported in lieu
  of using translated Arch versions that have the same type, causing
  aliasing warning during const requalification.
* update comments where requalify clobbers arch version from abstract
  spec.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

spec/design/skel/AARCH64/ArchFaultHandler_H.thy

@@ -10,7 +10,7 @@ theory ArchFaultHandler_H
 imports TCB_H Structures_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL_PREPARSE SEL4/API/Failures/AARCH64.hs
 

spec/design/skel/AARCH64/ArchFault_H.thy

@@ -12,7 +12,7 @@ theory ArchFault_H
 imports Types_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/Failures/AARCH64.hs CONTEXT AARCH64_H decls_only
 #INCLUDE_HASKELL SEL4/API/Failures/AARCH64.hs CONTEXT AARCH64_H bodies_only

spec/design/skel/AARCH64/ArchHypervisor_H.thy

@@ -15,7 +15,7 @@ imports
   FaultHandlerDecls_H
   InterruptDecls_H
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/VCPU/AARCH64.hs CONTEXT AARCH64_H decls_only \
   ONLY countTrailingZeros irqVPPIEventIndex

spec/design/skel/AARCH64/ArchInterruptDecls_H.thy

@@ -8,7 +8,7 @@ theory ArchInterruptDecls_H
 imports RetypeDecls_H CNode_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/Interrupt/AARCH64.hs CONTEXT AARCH64_H decls_only ArchInv= Arch=MachineOps NOT plic_complete_claim
 

spec/design/skel/AARCH64/ArchInterrupt_H.thy

@@ -13,7 +13,7 @@ imports
   ArchHypervisor_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/Interrupt/AARCH64.hs CONTEXT AARCH64_H bodies_only ArchInv= Arch= NOT plic_complete_claim
 

spec/design/skel/AARCH64/ArchInvocationLabels_H.thy

@@ -11,7 +11,7 @@ imports
   "Word_Lib.Enumeration"
   Setup_Locale
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 text \<open>
   An enumeration of arch-specific system call labels.
@@ -21,11 +21,12 @@ text \<open>
 
 end
 
-context begin interpretation Arch .
-requalify_types arch_invocation_label
-end
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
+arch_requalify_types (H)
+  arch_invocation_label
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/InvocationLabels/AARCH64.hs CONTEXT AARCH64_H instanceproofs ONLY ArchInvocationLabel
 

spec/design/skel/AARCH64/ArchLabelFuns_H.thy

@@ -10,7 +10,7 @@ chapter "Architecture-specific Invocation Label Functions"
 theory ArchLabelFuns_H
 imports InvocationLabels_H
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 text \<open>
   Arch-specific functions on invocation labels

spec/design/skel/AARCH64/ArchPSpace_H.thy

@@ -11,7 +11,7 @@ imports
   ObjectInstances_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/PSpace/AARCH64.hs decls_only ONLY pTablePartialOverlap
 #INCLUDE_HASKELL SEL4/Model/PSpace/AARCH64.hs NOT pTablePartialOverlap

spec/design/skel/AARCH64/ArchRetypeDecls_H.thy

@@ -16,7 +16,7 @@ imports
   ArchObjInsts_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures/AARCH64.hs
 

spec/design/skel/AARCH64/ArchRetype_H.thy

@@ -16,7 +16,7 @@ imports
   VCPU_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/ObjectType/AARCH64.hs CONTEXT AARCH64_H Arch.Types=ArchTypes_H ArchInv=ArchRetypeDecls_H NOT bodies_only
 #INCLUDE_HASKELL SEL4/API/Invocation/AARCH64.hs CONTEXT AARCH64_H bodies_only \

spec/design/skel/AARCH64/ArchStateData_H.thy

@@ -18,7 +18,7 @@ imports
   ArchStructures_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/AARCH64.hs CONTEXT AARCH64_H NOT ArmVSpaceRegionUse
 

spec/design/skel/AARCH64/ArchStructures_H.thy

@@ -12,7 +12,7 @@ imports
   Hardware_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
@@ -54,10 +54,8 @@ where
 
 end
 
-context begin interpretation Arch .
-
-requalify_types
+(* not possible to move this requalification to generic, as some arches don't have vcpu *)
+arch_requalify_types (H)
   vcpu
 
 end
-end

spec/design/skel/AARCH64/ArchTCB_H.thy

@@ -8,7 +8,7 @@ theory ArchTCB_H
 imports TCBDecls_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/TCB/AARCH64.hs RegisterSet= CONTEXT AARCH64_H
 

spec/design/skel/AARCH64/ArchThreadDecls_H.thy

@@ -17,7 +17,7 @@ imports
   KernelInitMonad_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Kernel/Thread/AARCH64.hs CONTEXT AARCH64_H decls_only
 

spec/design/skel/AARCH64/ArchThread_H.thy

@@ -15,7 +15,7 @@ imports
   ArchHypervisor_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Kernel/Thread/AARCH64.hs CONTEXT AARCH64_H Arch=MachineOps ArchReg=MachineTypes bodies_only
 

spec/design/skel/AARCH64/ArchTypes_H.thy

@@ -20,7 +20,7 @@ begin
 
 #INCLUDE_HASKELL SEL4/API/Types/Universal.lhs all_bits
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/Types/AARCH64.hs CONTEXT AARCH64_H
 
@@ -75,8 +75,4 @@ interpretation Arch .
 instance by (intro_classes, simp add: enum_alt_object_type)
 end
 
-context begin interpretation Arch .
-requalify_types object_type
-end
-
 end

spec/design/skel/AARCH64/ArchVSpaceDecls_H.thy

@@ -11,7 +11,7 @@ theory ArchVSpaceDecls_H
 imports ArchRetypeDecls_H InvocationLabels_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures.lhs CONTEXT AARCH64_H
 #INCLUDE_HASKELL_PREPARSE SEL4/API/InvocationLabels/AARCH64.hs CONTEXT AARCH64

spec/design/skel/AARCH64/ArchVSpace_H.thy

@@ -17,7 +17,7 @@ imports
   ArchHypervisor_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Kernel/VSpace/AARCH64.hs CONTEXT AARCH64_H bodies_only ArchInv=ArchRetypeDecls_H ONLY pteAtIndex getPPtrFromHWPTE isPageTablePTE ptBitsLeft
 

spec/design/skel/AARCH64/Arch_Structs_B.thy

@@ -13,7 +13,7 @@ theory Arch_Structs_B
 imports Setup_Locale
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/AARCH64.hs CONTEXT AARCH64_H ONLY ArmVSpaceRegionUse
 

spec/design/skel/AARCH64/Hardware_H.thy

@@ -11,7 +11,7 @@ imports
   State_H
 begin
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs Platform=Platform.AARCH64 CONTEXT AARCH64_H \
   NOT PT_Type plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices \
@@ -41,19 +41,18 @@ context Arch begin global_naming AARCH64_H
 
 end
 
-context begin interpretation Arch .
-requalify_types vmrights
-end
+arch_requalify_types (H)
+  vmrights
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64_H instanceproofs NOT plic_complete_claim HardwareASID VMFaultType VMPageSize VMPageEntry HypFaultType
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64_H ONLY wordFromPTE
 
 (* Kernel_Config provides a generic numeral, Haskell expects type irq *)
 abbreviation (input) maxIRQ :: irq where
-  "maxIRQ == Kernel_Config.maxIRQ"
+  "maxIRQ \<equiv> Kernel_Config.maxIRQ"
 
 end (* context AARCH64 *)
 

spec/design/skel/AARCH64/RegisterSet_H.thy

@@ -12,7 +12,7 @@ imports
   "Lib.HaskellLib_H"
   MachineOps
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 definition newFPUState :: "fpu_state" where
   "newFPUState \<equiv> FPUState (K 0) 0 0 "

spec/design/skel/AARCH64/State_H.thy

@@ -14,7 +14,7 @@ theory State_H
 imports
   RegisterSet_H
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 definition
   Word :: "machine_word \<Rightarrow> machine_word"
@@ -26,16 +26,14 @@ where
 
 end
 
-context begin interpretation Arch .
-
-requalify_consts
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
+arch_requalify_consts (H)
   wordBits
 
-end
-
 #INCLUDE_HASKELL Data/WordLib.lhs all_bits NOT wordBits
 
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Machine/RegisterSet.lhs Arch=AARCH64 CONTEXT AARCH64_H all_bits NOT UserContext UserMonad getRegister setRegister newContext mask Word PPtr
 

spec/design/skel/AARCH64/VCPU_H.thy

@@ -14,7 +14,7 @@ imports
   Invocations_H
   TCB_H
 begin
-context Arch begin global_naming AARCH64_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures.lhs CONTEXT AARCH64_H
 #INCLUDE_HASKELL SEL4/Object/VCPU/AARCH64.hs CONTEXT AARCH64_H ArchInv=Arch \

spec/design/skel/ARM/ArchFaultHandler_H.thy

@@ -10,7 +10,7 @@ theory ArchFaultHandler_H
 imports TCB_H Structures_H
 begin
 
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 
 #INCLUDE_HASKELL_PREPARSE SEL4/API/Failures/ARM.lhs

spec/design/skel/ARM/ArchFault_H.thy

@@ -11,7 +11,7 @@
 theory ArchFault_H
 imports Types_H
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 
 #INCLUDE_HASKELL SEL4/API/Failures/ARM.lhs CONTEXT ARM_H decls_only

spec/design/skel/ARM/ArchHypervisor_H.thy

@@ -14,7 +14,7 @@ imports
   KI_Decls_H
   InterruptDecls_H
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 
 #INCLUDE_HASKELL SEL4/Kernel/Hypervisor/ARM.lhs Arch= CONTEXT ARM_H decls_only ArchInv= ArchLabels=

spec/design/skel/ARM/ArchInterruptDecls_H.thy

@@ -8,7 +8,7 @@ theory ArchInterruptDecls_H
 imports RetypeDecls_H CNode_H
 begin
 
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs CONTEXT ARM_H decls_only ArchInv=
 

spec/design/skel/ARM/ArchInterrupt_H.thy

@@ -13,7 +13,7 @@ imports
   ArchHypervisor_H
 begin
 
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/Interrupt/ARM.lhs Arch= CONTEXT ARM_H bodies_only ArchInv=
 

spec/design/skel/ARM/ArchInvocationLabels_H.thy

@@ -11,7 +11,7 @@ imports
     "Word_Lib.Enumeration"
     Setup_Locale
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 text \<open>
   An enumeration of arch-specific system call labels.
@@ -21,11 +21,12 @@ text \<open>
 
 end
 
-context begin interpretation Arch .
-requalify_types arch_invocation_label
-end
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
+arch_requalify_types (H)
+  arch_invocation_label
 
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/InvocationLabels/ARM.lhs CONTEXT ARM_H instanceproofs ONLY ArchInvocationLabel
 

spec/design/skel/ARM/ArchLabelFuns_H.thy

@@ -9,7 +9,7 @@ chapter "Architecture-specific Invocation Label Functions"
 theory ArchLabelFuns_H
 imports InvocationLabels_H
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 text \<open>
   Arch-specific functions on invocation labels
 \<close>

spec/design/skel/ARM/ArchPSpace_H.thy

@@ -11,7 +11,7 @@ imports
   ObjectInstances_H
 begin
 
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/PSpace/ARM.hs
 

spec/design/skel/ARM/ArchRetypeDecls_H.thy

@@ -15,7 +15,7 @@ imports
   PSpaceFuns_H
   ArchObjInsts_H
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs CONTEXT ARM_H decls_only NOT isPageFlushLabel isPDFlushLabel Invocation IRQControlInvocation CopyRegisterSets
 

spec/design/skel/ARM/ArchRetype_H.thy

@@ -13,7 +13,7 @@ imports
   Hardware_H
   KI_Decls_H
 begin
-context Arch begin global_naming ARM_H
+context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/ObjectType/ARM.lhs CONTEXT ARM_H Arch.Types= ArchInv= bodies_only
 #INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs bodies_only CONTEXT ARM_H NOT isPDFlushLabel isPageFlushLabel