[wip] gen+aarch64 ainvs: move requalifies to generic theories

* prevent duplication between arches by moving requalifications from
  Arch theories to generic ones
  * this strategy is not available for new constants that are introduced
    in the Arch locale that need to be referenced in generic definitions
    or locale instantiations

proof/invariant-abstract/AARCH64/ArchAInvsPre.thy

@@ -140,10 +140,4 @@ proof goal_cases
   case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?)
 qed
 
-(* FIXME arch_split: move to global theory *)
-arch_requalify_facts
-  user_mem_dom_cong
-  device_mem_dom_cong
-  device_frame_in_device_region
-
 end

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1726,18 +1726,4 @@ lemma arch_pinv_st_tcb_at:
 
 end
 
-(* FIXME arch_split: move to global theory *)
-arch_requalify_consts
-  valid_arch_inv
-
-arch_requalify_facts
-  invoke_arch_tcb
-  invoke_arch_invs
-  sts_valid_arch_inv
-  arch_decode_inv_wf
-  arch_pinv_st_tcb_at
-
-declare invoke_arch_invs[wp]
-declare arch_decode_inv_wf[wp]
-
 end

proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy

@@ -45,9 +45,4 @@ 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]
-
 end

proof/invariant-abstract/AARCH64/ArchCSpaceInv_AI.thy

@@ -210,6 +210,4 @@ lemmas cap_vptr_simps [simp] =
 
 end
 
-arch_requalify_facts replace_cap_invs
-
 end

proof/invariant-abstract/AARCH64/ArchCSpace_AI.thy

@@ -599,9 +599,4 @@ lemma set_cap_kernel_window_simple:
 
 end
 
-(* FIXME arch_split: move to non-Arch theory? *)
-arch_requalify_facts
-  set_cap_valid_arch_caps_simple
-  set_cap_kernel_window_simple
-
 end

proof/invariant-abstract/AARCH64/ArchTcb_AI.thy

@@ -383,8 +383,4 @@ proof goal_cases
   case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?)
 qed
 
-(* FIXME arch_split: move to global theory *)
-arch_requalify_consts is_cnode_or_valid_arch
-arch_requalify_facts invoke_tcb_typ_at
-
 end

proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy

@@ -3142,8 +3142,4 @@ crunch vcpu_switch
 
 end
 
-(* FIXME arch_split: move to generic theory? *)
-arch_requalify_facts
-  do_machine_op_valid_kernel_mappings
-
 end

proof/invariant-abstract/AARCH64/Machine_AI.thy

@@ -423,10 +423,4 @@ lemma dmo_gets_inv[wp]:
 
 end
 
-arch_requalify_facts
-  det_getRegister
-  det_setRegister
-  det_getRestartPC
-  det_setNextPC
-
 end

proof/invariant-abstract/AInvs.thy

@@ -12,6 +12,11 @@ theory AInvs
 imports ArchAInvsPre
 begin
 
+arch_requalify_facts
+  user_mem_dom_cong
+  device_mem_dom_cong
+  device_frame_in_device_region
+
 lemma st_tcb_at_nostate_upd:
   "\<lbrakk> get_tcb t s = Some y; tcb_state y = tcb_state y' \<rbrakk> \<Longrightarrow>
   st_tcb_at P t' (s \<lparr>kheap := (kheap s)(t \<mapsto> TCB y')\<rparr>) = st_tcb_at P t' s"

proof/invariant-abstract/CSpacePre_AI.thy

@@ -20,6 +20,9 @@ arch_requalify_consts
   cap_asid_base
   cap_vptr
 
+arch_requalify_facts
+  replace_cap_invs
+
 lemma fun_upd_Some:
   "ms p = Some k \<Longrightarrow> (ms(a \<mapsto> b)) p = Some (if a = p then b else k)"
   by auto

proof/invariant-abstract/KHeapPre_AI.thy

@@ -8,6 +8,12 @@ theory KHeapPre_AI
 imports Machine_AI
 begin
 
+arch_requalify_facts
+  det_getRegister
+  det_setRegister
+  det_getRestartPC
+  det_setNextPC
+
 primrec
   same_caps :: "Structures_A.kernel_object \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
 where

proof/invariant-abstract/LevityCatch_AI.thy

@@ -19,9 +19,13 @@ arch_requalify_consts
 arch_requalify_facts
   ptrFormPAddr_addFromPPtr
   aobj_ref_arch_cap
+  arch_finalise_cap_bcorres
+  prepare_thread_delete_bcorres
 
 lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap
 
+lemmas [wp] = arch_finalise_cap_bcorres prepare_thread_delete_bcorres
+
 lemma detype_arch_state:
   "arch_state (detype S s) = arch_state s"
   by (simp add: detype_def)

proof/invariant-abstract/Schedule_AI.thy

@@ -8,10 +8,13 @@ theory Schedule_AI
 imports VSpace_AI
 begin
 
+arch_requalify_facts
+  no_irq
+  no_irq_storeWord
+
 abbreviation
   "activatable \<equiv> \<lambda>st. runnable st \<or> idle st"
 
-
 locale Schedule_AI =
     fixes state_ext :: "('a::state_ext) itself"
     assumes dmo_mapM_storeWord_0_invs[wp]:
@@ -27,12 +30,6 @@ locale Schedule_AI =
     assumes stit_activatable:
       "\<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 requalified. *)
-arch_requalify_facts
-  no_irq
-  no_irq_storeWord
-
 crunch schedule_switch_thread_fastfail
   for inv[wp]: P
 

proof/invariant-abstract/Syscall_AI.thy

@@ -22,16 +22,28 @@ begin
 arch_requalify_facts (A)
   data_to_cptr_def
 
+arch_requalify_consts
+  is_cnode_or_valid_arch
+  valid_arch_inv
+
 arch_requalify_facts
   resetTimer_device_state_inv
   arch_decode_invocation_inv
   arch_post_cap_deletion_cur_thread
   arch_post_cap_deletion_state_refs_of
   arch_invoke_irq_handler_typ_at
+  invoke_tcb_typ_at
+  invoke_arch_tcb
+  invoke_arch_invs
+  sts_valid_arch_inv
+  arch_decode_inv_wf
+  arch_pinv_st_tcb_at
 
 lemmas [wp] =
   arch_decode_invocation_inv
   lookup_cap_and_slot_inv
+  invoke_arch_invs
+  arch_decode_inv_wf
 
 lemmas [simp] =
   data_to_cptr_def

proof/invariant-abstract/TcbAcc_AI.thy

@@ -13,6 +13,8 @@ arch_requalify_facts
   as_user_inv
   getRegister_inv
   user_getreg_inv
+  set_cap_valid_arch_caps_simple
+  set_cap_kernel_window_simple
 
 declare user_getreg_inv[wp]
 

proof/invariant-abstract/VSpace_AI.thy

@@ -13,6 +13,7 @@ imports ArchVSpace_AI
 begin
 
 arch_requalify_facts
+  do_machine_op_valid_kernel_mappings
   ackInterrupt_device_state_inv
   pspace_respects_device_region_dmo
   cap_refs_respects_device_region_dmo