[wip] gen+aarch64 ainvs: deploy requalify infrastructure

Temporarily only dealing with AARCH64; want feedback before applying to other arches. * global_naming AARCH64 -> arch_global_naming * try get rid of `interpretation Arch .` (slow) in lieu of `(in Arch)` (faster) or proper requalifying (nearly instant) * get rid of requalifications that were already requalified, or were global (thanks to new warnings) TODO: some of these will turn out to be broken because they're not actually global/exported on other arches * put arch_global_naming on same line as `context Arch begin` * annotate requalifications in Arch theories that can be moved to generic * put FIXMEs on unusual global_naming practices Signed-off-by: Rafal Kolanski <[email protected]>
Xaphiosis · Jul 11, 2024 · b6b14a2 · b6b14a2
1 parent 8386cb8
commit b6b14a2
Show file tree

Hide file tree

Showing 65 changed files with 235 additions and 318 deletions.
diff --git a/proof/invariant-abstract/AARCH64/ArchADT_AI.thy b/proof/invariant-abstract/AARCH64/ArchADT_AI.thy
@@ -12,7 +12,7 @@ imports
   "Lib.Simulation"
   Invariants_AI
 begin
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 subsection \<open>Constructing a virtual-memory view\<close>
 

diff --git a/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy b/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy
@@ -11,9 +11,7 @@ begin
 
 unbundle l4v_word_context
 
-context Arch begin
-
-global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma ucast_ucast_mask_low: "(ucast (x && mask asid_low_bits) :: asid_low_index) = ucast x"
   by (rule ucast_mask_drop, simp add: asid_low_bits_def)
@@ -143,9 +141,10 @@ proof goal_cases
   case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?)
 qed
 
-requalify_facts
-  AARCH64.user_mem_dom_cong
-  AARCH64.device_mem_dom_cong
-  AARCH64.device_frame_in_device_region
+(* FIXME arch_split: move to global theory *)
+arch_requalify_facts
+  user_mem_dom_cong
+  device_mem_dom_cong
+  device_frame_in_device_region
 
 end
diff --git a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy
@@ -17,7 +17,7 @@ lemma valid_vso_at[wp]:"\<lbrace>valid_vso_at level p\<rbrace> f \<lbrace>\<lamb
 
 end
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 (* Is there a lookup that leads to a page table at (level, p)? *)
 locale_abbrev ex_vs_lookup_table ::

diff --git a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy
@@ -11,7 +11,7 @@ begin
 
 unbundle l4v_word_context
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 definition
   "valid_aci aci \<equiv> case aci of MakePool frame slot parent base \<Rightarrow>
@@ -414,7 +414,7 @@ lemma equal_kernel_mappings:
 end
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma vmid_for_asid_empty_update:
   "\<lbrakk> asid_table s asid_high = None; asid_pools_of s ap = Some Map.empty \<rbrakk> \<Longrightarrow>
@@ -1726,21 +1726,17 @@ lemma arch_pinv_st_tcb_at:
 
 end
 
-
-context begin interpretation Arch .
-
-requalify_consts
+(* FIXME arch_split: move to global theory *)
+arch_requalify_consts
   valid_arch_inv
 
-requalify_facts
+arch_requalify_facts
   invoke_arch_tcb
   invoke_arch_invs
   sts_valid_arch_inv
   arch_decode_inv_wf
   arch_pinv_st_tcb_at
 
-end
-
 declare invoke_arch_invs[wp]
 declare arch_decode_inv_wf[wp]
 

diff --git a/proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy b/proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy
@@ -10,7 +10,7 @@ imports
   BCorres2_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems BCorres2_AI_assms
 
@@ -89,7 +89,7 @@ interpretation BCorres2_AI?: BCorres2_AI
 
 lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch send_ipc,send_signal,do_reply_transfer,arch_perform_invocation
   for (bcorres) bcorres[wp]: truncate_state

diff --git a/proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy b/proof/invariant-abstract/AARCH64/ArchBCorres_AI.thy
@@ -11,7 +11,7 @@ imports
   ArchBitSetup_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma entry_for_asid_truncate[simp]:
   "entry_for_asid asid (truncate_state s) = entry_for_asid asid s"
@@ -45,7 +45,7 @@ crunch prepare_thread_delete
 
 end
 
-requalify_facts AARCH64.arch_finalise_cap_bcorres AARCH64.prepare_thread_delete_bcorres
+arch_requalify_facts arch_finalise_cap_bcorres prepare_thread_delete_bcorres
 
 declare arch_finalise_cap_bcorres[wp] prepare_thread_delete_bcorres[wp]
 

diff --git a/proof/invariant-abstract/AARCH64/ArchBits_AI.thy b/proof/invariant-abstract/AARCH64/ArchBits_AI.thy
@@ -9,7 +9,7 @@ theory ArchBits_AI
 imports Invariants_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 (* arch-specific interpretations of update locales: *)
 

diff --git a/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy
@@ -9,7 +9,7 @@ theory ArchCNodeInv_AI
 imports CNodeInv_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems CNodeInv_AI_assms
 
@@ -538,7 +538,7 @@ qed
 termination rec_del by (rule rec_del_termination)
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma post_cap_delete_pre_is_final_cap':
   "\<lbrakk>valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \<noteq> NullCap\<rbrakk>
@@ -800,7 +800,7 @@ global_interpretation CNodeInv_AI_2?: CNodeInv_AI_2
   qed
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma finalise_cap_rvk_prog [CNodeInv_AI_assms]:
    "finalise_cap cap f \<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>"
@@ -905,7 +905,7 @@ termination cap_revoke by (rule cap_revoke_termination)
 declare cap_revoke.simps[simp del]
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch finalise_slot
   for typ_at[wp, CNodeInv_AI_assms]: "\<lambda>s. P (typ_at T p s)"
@@ -930,7 +930,7 @@ global_interpretation CNodeInv_AI_4?: CNodeInv_AI_4
   qed
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma cap_move_ioports:
   "\<lbrace>valid_ioports and cte_wp_at ((=) cap.NullCap) ptr'

diff --git a/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpaceInvPre_AI.thy
@@ -14,7 +14,7 @@ imports CSpaceInvPre_AI
 begin
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma aobj_ref_acap_rights_update[simp]:
   "aobj_ref (acap_rights_update f x) = aobj_ref x"

diff --git a/proof/invariant-abstract/AARCH64/ArchCSpaceInv_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpaceInv_AI.thy
@@ -12,7 +12,7 @@ theory ArchCSpaceInv_AI
 imports CSpaceInv_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 definition
    safe_ioport_insert :: "cap \<Rightarrow> cap \<Rightarrow> 'a::state_ext state \<Rightarrow> bool"
@@ -210,8 +210,6 @@ lemmas cap_vptr_simps [simp] =
 
 end
 
-context begin interpretation Arch .
-requalify_facts replace_cap_invs
-end
+arch_requalify_facts replace_cap_invs
 
 end
diff --git a/proof/invariant-abstract/AARCH64/ArchCSpacePre_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpacePre_AI.thy
@@ -13,7 +13,7 @@ theory ArchCSpacePre_AI
 imports CSpacePre_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemmas typ_at_eq_kheap_obj = typ_at_eq_kheap_obj atyp_at_eq_kheap_obj
 

diff --git a/proof/invariant-abstract/AARCH64/ArchCSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchCSpace_AI.thy
@@ -12,7 +12,7 @@ theory ArchCSpace_AI
 imports CSpace_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems CSpace_AI_assms
 
@@ -304,7 +304,7 @@ end
 global_interpretation cap_insert_crunches?: cap_insert_crunches .
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma cap_insert_cap_refs_in_kernel_window[wp, CSpace_AI_assms]:
   "\<lbrace>cap_refs_in_kernel_window
@@ -496,7 +496,7 @@ proof goal_cases
 qed
 
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma is_cap_simps':
   "is_cnode_cap cap = (\<exists>r bits g. cap = cap.CNodeCap r bits g)"
@@ -599,12 +599,9 @@ lemma set_cap_kernel_window_simple:
 
 end
 
-context begin interpretation Arch .
-
-requalify_facts
+(* FIXME arch_split: move to non-Arch theory? *)
+arch_requalify_facts
   set_cap_valid_arch_caps_simple
   set_cap_kernel_window_simple
 
 end
-
-end
diff --git a/proof/invariant-abstract/AARCH64/ArchCrunchSetup_AI.thy b/proof/invariant-abstract/AARCH64/ArchCrunchSetup_AI.thy
@@ -10,7 +10,7 @@ imports
   "Lib.Crunch_Instances_NonDet"
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch_ignore (add: debugPrint clearMemory pt_lookup_from_level)
 

diff --git a/proof/invariant-abstract/AARCH64/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetSchedAux_AI.thy
@@ -9,7 +9,7 @@ theory ArchDetSchedAux_AI
 imports DetSchedAux_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems DetSchedAux_AI_assms
 

diff --git a/proof/invariant-abstract/AARCH64/ArchDetSchedDomainTime_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetSchedDomainTime_AI.thy
@@ -9,7 +9,7 @@ theory ArchDetSchedDomainTime_AI
 imports DetSchedDomainTime_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems DetSchedDomainTime_AI_assms
 
@@ -62,7 +62,7 @@ proof goal_cases
   case 1 show ?case by (unfold_locales; (fact DetSchedDomainTime_AI_assms)?)
 qed
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch arch_perform_invocation
   for domain_time_inv[wp, DetSchedDomainTime_AI_assms]: "\<lambda>s. P (domain_time s)"

diff --git a/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy
@@ -9,7 +9,7 @@ theory ArchDetSchedSchedule_AI
 imports DetSchedSchedule_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems DetSchedSchedule_AI_assms
 
@@ -498,7 +498,7 @@ proof goal_cases
   case 1 show ?case by (unfold_locales; (fact DetSchedSchedule_AI_assms)?)
 qed
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 lemma dmo_scheduler_act_sane[wp]:
   "\<lbrace>scheduler_act_sane\<rbrace> do_machine_op f \<lbrace>\<lambda>rv. scheduler_act_sane\<rbrace>"

diff --git a/proof/invariant-abstract/AARCH64/ArchDeterministic_AI.thy b/proof/invariant-abstract/AARCH64/ArchDeterministic_AI.thy
@@ -11,7 +11,7 @@ begin
 
 declare dxo_wp_weak[wp del]
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems Deterministic_AI_assms
 
@@ -40,7 +40,7 @@ proof goal_cases
   case 1 show ?case by (unfold_locales; (fact Deterministic_AI_assms)?)
 qed
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 crunch arch_invoke_irq_handler
   for valid_list[wp,Deterministic_AI_assms]: valid_list

diff --git a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy
@@ -9,7 +9,7 @@ theory ArchDetype_AI
 imports Detype_AI
 begin
 
-context Arch begin global_naming AARCH64
+context Arch begin arch_global_naming
 
 named_theorems Detype_AI_assms
 
@@ -636,8 +636,8 @@ interpretation Detype_AI_2
         Detype_AI_2.intro
         by blast
 
-context begin interpretation Arch .
-lemma delete_objects_invs[wp]:
+(* generic consequence of architecture-specific details *)
+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
     invs and ct_active\<rbrace>
@@ -657,6 +657,8 @@ lemma delete_objects_invs[wp]:
   apply (drule (1) cte_wp_valid_cap)
   apply (simp add: valid_cap_def cap_aligned_def word_size_bits_def untyped_min_bits_def)
   done
-end
+
+requalify_facts Arch.delete_objects_invs
+lemmas [wp] = delete_objects_invs
 
 end