[wip] gen+aarch64 ainvs:

* 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

proof/invariant-abstract/AARCH64/ArchAInvsPre.thy

@@ -79,7 +79,6 @@ lemma device_frame_in_device_region:
   \<Longrightarrow> device_state (machine_state s) p \<noteq> None"
   by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
 
-global_naming Arch
 named_theorems AInvsPre_assms
 
 lemma get_vspace_of_thread_asid_or_global_pt:

proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy

@@ -45,6 +45,7 @@ crunch prepare_thread_delete
 
 end
 
+(* FIXME arch_split: move to generic theory *)
 arch_requalify_facts arch_finalise_cap_bcorres prepare_thread_delete_bcorres
 
 declare arch_finalise_cap_bcorres[wp] prepare_thread_delete_bcorres[wp]

proof/invariant-abstract/AARCH64/ArchDetype_AI.thy

@@ -637,6 +637,7 @@ interpretation Detype_AI_2
         by blast
 
 (* generic consequence of architecture-specific details *)
+(* FIXME arch-split: can't this be done without this strange requalification? *)
 lemma (in Arch) delete_objects_invs[wp]:
   "\<lbrace>(\<lambda>s. \<exists>slot. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s
     \<and> descendants_range (cap.UntypedCap dev ptr bits f) slot s) and

proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy

@@ -217,8 +217,6 @@ lemma unmap_page_tcb_cap_valid:
   done
 
 
-global_naming Arch
-
 lemma (* replaceable_cdt_update *)[simp,Finalise_AI_assms]:
   "replaceable (cdt_update f s) = replaceable s"
   by (fastforce simp: replaceable_def tcb_cap_valid_def
@@ -1400,7 +1398,6 @@ lemma arch_finalise_cap_replaceable:
   apply (clarsimp simp: valid_cap_def wellformed_mapdata_def cap_aligned_def obj_at_def)
   done
 
-global_naming Arch
 lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_assms]:
   "\<lbrace>if_unsafe_then_cap and valid_global_refs
            and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl\<rbrace>
@@ -1600,7 +1597,6 @@ lemma fast_finalise_replaceable[wp]:
   apply (clarsimp simp: cap_irqs_def cap_irq_opt_def split: cap.split_asm)
   done
 
-global_naming Arch
 lemma (* cap_delete_one_invs *) [Finalise_AI_assms,wp]:
   "\<lbrace>invs and emptyable ptr\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. invs\<rbrace>"
   apply (simp add: cap_delete_one_def unless_def is_final_cap_def)
@@ -1771,9 +1767,6 @@ lemma replaceable_or_arch_update_pg:
   apply (auto simp: is_cap_simps is_arch_update_def cap_master_cap_simps)
   done
 
-
-global_naming Arch
-
 crunch prepare_thread_delete
   for invs[wp]: invs
   (ignore: set_object do_machine_op wp: dmo_invs_lift)
@@ -1961,8 +1954,6 @@ lemma arch_finalise_cap_valid_cap[wp]:
   unfolding arch_finalise_cap_def
   by (wpsimp split: arch_cap.split option.split bool.split)
 
-global_naming Arch
-
 lemmas clearMemory_invs[wp,Finalise_AI_assms] = clearMemory_invs
 
 lemma valid_idle_has_null_cap_ARCH[Finalise_AI_assms]:

proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy

@@ -28,9 +28,6 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_assms]:
    apply wp
   by (simp add: upto.simps word_bits_def)
 
-(* FIXME arch_split: why not arch global naming? this doesn't make sense *)
-global_naming Arch
-
 lemma arch_stt_invs [wp,Schedule_AI_assms]:
   "arch_switch_to_thread t' \<lbrace>invs\<rbrace>"
   apply (wpsimp simp: arch_switch_to_thread_def)

proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy

@@ -9,7 +9,7 @@ theory ArchVCPU_AI
 imports AInvs
 begin
 
-context Arch begin arch_global_naming (*FIXME: arch_split*)
+context Arch begin arch_global_naming
 
 (* This is similar to cur_vcpu_2, but not close enough to reuse. *)
 definition active_cur_vcpu_of :: "'z state \<Rightarrow> obj_ref option" where

proof/invariant-abstract/AARCH64/Machine_AI.thy

@@ -69,8 +69,7 @@ crunch_ignore (no_irq) (add:
   handleE' handleE handle_elseE forM forM_x
   zipWithM ignore_failure)
 
-(* FIXME arch_split: no global_naming? *)
-context Arch begin
+context Arch begin arch_global_naming
 
 text \<open>Deterministic\<close>
 
@@ -424,10 +423,10 @@ lemma dmo_gets_inv[wp]:
 
 end
 
-requalify_facts
-  Arch.det_getRegister
-  Arch.det_setRegister
-  Arch.det_getRestartPC
-  Arch.det_setNextPC
+arch_requalify_facts
+  det_getRegister
+  det_setRegister
+  det_getRestartPC
+  det_setNextPC
 
 end

proof/invariant-abstract/CSpaceInv_AI.thy

@@ -1054,7 +1054,7 @@ lemma get_cap_caps_of_state:
   by (clarsimp simp: caps_of_state_def eq_commute)
 
 (* generic consequence of architecture-specific details *)
-(* FIXME arch_split: no global naming? *)
+(* FIXME arch_split: no global naming, immediately requalified *)
 lemma (in Arch) abj_ref_none_no_refs:
   "obj_refs c = {} \<Longrightarrow> table_cap_ref c = None"
   unfolding table_cap_ref_def

proof/invariant-abstract/CSpace_AI.thy

@@ -18,14 +18,11 @@ arch_requalify_consts
   final_matters_arch
   ups_of_heap
 
-(* FIXME arch_split: this should maybe have a global_naming *)
-requalify_facts
-  Arch.loadWord_inv
-
 arch_requalify_facts (A)
   update_cnode_cap_data_def
 
 arch_requalify_facts
+  loadWord_inv
   is_derived_arch_non_arch
   ups_of_heap_non_arch_upd
   master_arch_cap_obj_refs

proof/invariant-abstract/EmptyFail_AI.thy

@@ -8,9 +8,8 @@ theory EmptyFail_AI
 imports ArchTcb_AI
 begin
 
-(* FIXME arch_split: no global_naming *)
-requalify_facts
-  Arch.ef_machine_op_lift
+arch_requalify_facts
+  ef_machine_op_lift
 
 lemmas [wp] = ef_ignore_failure ef_machine_op_lift
 

proof/invariant-abstract/Finalise_AI.thy

@@ -27,11 +27,8 @@ arch_requalify_consts
   vs_cap_ref
   arch_post_cap_delete_pre
 
-(* FIXME arch_split: no global_naming *)
-requalify_facts
-  Arch.no_irq_clearMemory
-
 arch_requalify_facts
+  no_irq_clearMemory
   final_cap_lift
   valid_global_refsD
   arch_post_cap_deletion_valid_objs

proof/invariant-abstract/InvariantsPre_AI.thy

@@ -8,13 +8,6 @@ theory InvariantsPre_AI
 imports LevityCatch_AI
 begin
 
-(* FIXME RAF: these already appear exported to global context?!
-arch_requalify_types (A)
-  aa_type
-
-arch_requalify_consts (A)
-  aa_type *)
-
 (* FIXME: move *)
 declare ranI [intro]
 

proof/invariant-abstract/IpcCancel_AI.thy

@@ -8,11 +8,8 @@ theory IpcCancel_AI
 imports ArchSchedule_AI
 begin
 
-(* FIXME arch_split: strange global_naming *)
-requalify_facts
-  Arch.arch_stit_invs
-
 arch_requalify_facts
+  arch_stit_invs
   arch_post_cap_deletion_pred_tcb_at
 
 declare arch_post_cap_deletion_pred_tcb_at[wp]

proof/invariant-abstract/Ipc_AI.thy

@@ -13,19 +13,16 @@ begin
 arch_requalify_consts
   in_device_frame
 
-(* FIXME arch_split: unclear why not arch global_naming *)
-requalify_facts
-  Arch.setup_caller_cap_ioports
-  Arch.set_mrs_ioports
-  Arch.as_user_ioports
-  Arch.set_message_info_ioports
-  Arch.copy_mrs_ioports
-  Arch.store_word_offs_ioports
-  Arch.make_arch_fault_msg_ioports
-  Arch.arch_derive_cap_notzombie
-  Arch.arch_derive_cap_notIRQ
-
 arch_requalify_facts
+  setup_caller_cap_ioports
+  set_mrs_ioports
+  as_user_ioports
+  set_message_info_ioports
+  copy_mrs_ioports
+  store_word_offs_ioports
+  make_arch_fault_msg_ioports
+  arch_derive_cap_notzombie
+  arch_derive_cap_notIRQ
   lookup_ipc_buffer_inv
   set_mi_invs
   as_user_hyp_refs_of

proof/invariant-abstract/KHeap_AI.thy

@@ -14,12 +14,9 @@ arch_requalify_consts
   non_vspace_obj
   vspace_obj_pred
 
-(* FIXME arch_split: these should probably be in an arch-named context *)
-requalify_facts
-  Arch.getActiveIRQ_neq_non_kernel
-  Arch.dmo_getActiveIRQ_non_kernel
-
 arch_requalify_facts
+  getActiveIRQ_neq_non_kernel
+  dmo_getActiveIRQ_non_kernel
   pspace_in_kernel_window_atyp_lift
   valid_vspace_objs_lift_weak
   vs_lookup_vspace_obj_at_lift

proof/invariant-abstract/Schedule_AI.thy

@@ -28,10 +28,10 @@ locale Schedule_AI =
       "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . (ct_in_state activatable :: 'a state \<Rightarrow> bool)\<rbrace>"
 
 (* FIXME arch_split: some of these could be moved to generic theories
-   so they don't need to be unqualified. *)
-requalify_facts
-  Arch.no_irq
-  Arch.no_irq_storeWord
+   so they don't need to be requalified. *)
+arch_requalify_facts
+  no_irq
+  no_irq_storeWord
 
 crunch schedule_switch_thread_fastfail
   for inv[wp]: P

proof/invariant-abstract/Syscall_AI.thy

@@ -16,14 +16,14 @@ imports
   ArchInterrupt_AI
 begin
 
-requalify_facts
-  (* lookup_cap_and_slot_inv (* FIXME arch_split: check other arches to make sure this is global *) *)
-  Arch.resetTimer_device_state_inv
+(* requalify_facts
+  lookup_cap_and_slot_inv (* FIXME arch_split: check other arches to make sure this is global *) *)
 
 arch_requalify_facts (A)
   data_to_cptr_def
 
 arch_requalify_facts
+  resetTimer_device_state_inv
   arch_decode_invocation_inv
   arch_post_cap_deletion_cur_thread
   arch_post_cap_deletion_state_refs_of

proof/invariant-abstract/VSpace_AI.thy

@@ -12,11 +12,8 @@ theory VSpace_AI
 imports ArchVSpace_AI
 begin
 
-(* FIXME arch_split: this should maybe have global_naming *)
-requalify_facts
-  Arch.ackInterrupt_device_state_inv
-
 arch_requalify_facts
+  ackInterrupt_device_state_inv
   pspace_respects_device_region_dmo
   cap_refs_respects_device_region_dmo