From 4237bc713b36391731408004fb4243f0044bacdf Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Thu, 11 Jul 2024 17:29:53 +1000 Subject: [PATCH] [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 --- .../invariant-abstract/AARCH64/ArchADT_AI.thy | 2 +- .../AARCH64/ArchAInvsPre.thy | 13 +++-- .../invariant-abstract/AARCH64/ArchAcc_AI.thy | 2 +- .../AARCH64/ArchArch_AI.thy | 14 ++--- .../AARCH64/ArchBCorres2_AI.thy | 4 +- .../AARCH64/ArchBCorres_AI.thy | 4 +- .../AARCH64/ArchBits_AI.thy | 2 +- .../AARCH64/ArchCNodeInv_AI.thy | 10 ++-- .../AARCH64/ArchCSpaceInvPre_AI.thy | 2 +- .../AARCH64/ArchCSpaceInv_AI.thy | 6 +-- .../AARCH64/ArchCSpacePre_AI.thy | 2 +- .../AARCH64/ArchCSpace_AI.thy | 13 ++--- .../AARCH64/ArchCrunchSetup_AI.thy | 2 +- .../AARCH64/ArchDetSchedAux_AI.thy | 2 +- .../AARCH64/ArchDetSchedDomainTime_AI.thy | 4 +- .../AARCH64/ArchDetSchedSchedule_AI.thy | 4 +- .../AARCH64/ArchDeterministic_AI.thy | 4 +- .../AARCH64/ArchDetype_AI.thy | 10 ++-- .../AARCH64/ArchEmptyFail_AI.thy | 10 ++-- .../AARCH64/ArchFinalise_AI.thy | 18 +++---- .../AARCH64/ArchInterruptAcc_AI.thy | 2 +- .../AARCH64/ArchInterrupt_AI.thy | 2 +- .../AARCH64/ArchInvariants_AI.thy | 4 +- .../AARCH64/ArchIpcCancel_AI.thy | 2 +- .../invariant-abstract/AARCH64/ArchIpc_AI.thy | 4 +- .../AARCH64/ArchKHeap_AI.thy | 4 +- .../AARCH64/ArchKernelInit_AI.thy | 2 +- .../AARCH64/ArchLevityCatch_AI.thy | 2 +- .../AARCH64/ArchRetype_AI.thy | 22 ++++---- .../AARCH64/ArchSchedule_AI.thy | 3 +- .../AARCH64/ArchSyscall_AI.thy | 2 +- .../AARCH64/ArchTcbAcc_AI.thy | 2 +- .../invariant-abstract/AARCH64/ArchTcb_AI.thy | 13 +++-- .../AARCH64/ArchUntyped_AI.thy | 2 +- .../AARCH64/ArchVCPU_AI.thy | 2 +- .../AARCH64/ArchVSpaceEntries_AI.thy | 2 +- .../AARCH64/ArchVSpace_AI.thy | 9 ++-- .../invariant-abstract/AARCH64/Machine_AI.thy | 13 ++--- proof/invariant-abstract/ADT_AI.thy | 10 ++-- proof/invariant-abstract/BCorres_AI.thy | 20 ++++---- proof/invariant-abstract/CNodeInv_AI.thy | 6 +-- proof/invariant-abstract/CSpaceInvPre_AI.thy | 19 ++++--- proof/invariant-abstract/CSpaceInv_AI.thy | 22 ++++---- proof/invariant-abstract/CSpacePre_AI.thy | 4 +- proof/invariant-abstract/CSpace_AI.thy | 15 +++--- proof/invariant-abstract/DetSchedAux_AI.thy | 5 +- proof/invariant-abstract/Deterministic_AI.thy | 4 +- proof/invariant-abstract/Detype_AI.thy | 6 +-- proof/invariant-abstract/EmptyFail_AI.thy | 5 +- proof/invariant-abstract/Finalise_AI.thy | 15 +++--- proof/invariant-abstract/Interrupt_AI.thy | 8 +-- proof/invariant-abstract/InvariantsPre_AI.thy | 11 ++-- proof/invariant-abstract/Invariants_AI.thy | 51 ++++++++++--------- proof/invariant-abstract/IpcCancel_AI.thy | 9 ++-- proof/invariant-abstract/Ipc_AI.thy | 27 +++++----- proof/invariant-abstract/KHeap_AI.thy | 14 +++-- proof/invariant-abstract/LevityCatch_AI.thy | 10 ++-- proof/invariant-abstract/Retype_AI.thy | 8 ++- proof/invariant-abstract/Schedule_AI.thy | 6 +-- proof/invariant-abstract/Syscall_AI.thy | 12 +++-- proof/invariant-abstract/TcbAcc_AI.thy | 7 +-- proof/invariant-abstract/Tcb_AI.thy | 6 +-- proof/invariant-abstract/Untyped_AI.thy | 17 +------ proof/invariant-abstract/VSpacePre_AI.thy | 6 +-- proof/invariant-abstract/VSpace_AI.thy | 10 ++-- 65 files changed, 235 insertions(+), 318 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchADT_AI.thy b/proof/invariant-abstract/AARCH64/ArchADT_AI.thy index c0376b854c..753c5e8949 100644 --- 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 \Constructing a virtual-memory view\ diff --git a/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy b/proof/invariant-abstract/AARCH64/ArchAInvsPre.thy index 5dce18b02c..4bb6bc441e 100644 --- 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 index df5aa1ef06..7ff2c2d231 100644 --- 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]:"\valid_vso_at level p\ f \\ case aci of MakePool frame slot parent base \ @@ -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: "\ asid_table s asid_high = None; asid_pools_of s ap = Some Map.empty \ \ @@ -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 index 94caa7b577..6259833c46 100644 --- 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 index 41388b855a..8364a914dd 100644 --- 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 index f5afcbc3fb..ff173a2570 100644 --- 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 index 04467df833..2a9184bd13 100644 --- 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': "\valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \ NullCap\ @@ -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 \\s. revoke_progress_ord m (\x. map_option cap_to_rpo (caps_of_state s x))\" @@ -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]: "\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: "\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 index 3e3e165547..9be7754f33 100644 --- 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 index b2c600a167..ba702cde24 100644 --- 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 \ cap \ 'a::state_ext state \ 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 index 7fdac5a929..2080df6b50 100644 --- 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 index 42b0e4cfff..05759f6b54 100644 --- 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]: "\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 = (\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 index 0f783df33d..5cc6c4d7d3 100644 --- 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 index 8d56752005..2439b153b8 100644 --- 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 index 949773c328..44790fee8d 100644 --- 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]: "\s. P (domain_time s)" diff --git a/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy index 84f6d9fb1b..b168ce488f 100644 --- 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]: "\scheduler_act_sane\ do_machine_op f \\rv. scheduler_act_sane\" diff --git a/proof/invariant-abstract/AARCH64/ArchDeterministic_AI.thy b/proof/invariant-abstract/AARCH64/ArchDeterministic_AI.thy index 360d38f0f7..72360b387e 100644 --- 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 index d00dbc5846..b7a66c2305 100644 --- 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]: "\(\s. \slot. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s \ descendants_range (cap.UntypedCap dev ptr bits f) slot s) and invs and ct_active\ @@ -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 diff --git a/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy index 3d8fc10556..8e229505a0 100644 --- a/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy @@ -9,7 +9,7 @@ theory ArchEmptyFail_AI imports EmptyFail_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems EmptyFail_AI_assms @@ -30,7 +30,7 @@ global_interpretation EmptyFail_AI_load_word?: EmptyFail_AI_load_word case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming crunch handle_fault for (empty_fail) empty_fail[wp, EmptyFail_AI_assms] @@ -128,7 +128,7 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma empty_fail_pt_lookup_from_level[wp]: "empty_fail (pt_lookup_from_level level pt_ptr vptr target_pt_ptr)" @@ -158,7 +158,7 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming crunch cap_delete, choose_thread for (empty_fail) empty_fail[wp, EmptyFail_AI_assms] @@ -182,7 +182,7 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact EmptyFail_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma plic_complete_claim_empty_fail[wp, EmptyFail_AI_assms]: "empty_fail (plic_complete_claim irq)" diff --git a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy index 1390c0a215..f45618a637 100644 --- a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy @@ -9,12 +9,10 @@ theory ArchFinalise_AI imports Finalise_AI begin -context Arch begin +context Arch begin arch_global_naming named_theorems Finalise_AI_assms -global_naming AARCH64 - lemma valid_global_refs_asid_table_udapte [iff]: "valid_global_refs (s\arch_state := arm_asid_table_update f (arch_state s)\) = valid_global_refs s" @@ -1581,7 +1579,7 @@ interpretation Finalise_AI_1?: Finalise_AI_1 by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma fast_finalise_replaceable[wp]: "\\s. s \ cap \ x = is_final_cap' cap s @@ -1620,7 +1618,7 @@ interpretation Finalise_AI_2?: Finalise_AI_2 case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming crunch vcpu_update, vgic_update, vcpu_disable, vcpu_restore, vcpu_save_reg_range, vgic_update_lr, @@ -1753,7 +1751,7 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin global_naming AARCH64 (*FIXME: arch_split*) +context Arch begin arch_global_naming (*FIXME: arch_split*) lemma do_machine_op_reachable_pg_cap[wp]: "\\s. P (reachable_frame_cap cap s)\ @@ -1900,9 +1898,7 @@ lemma (* dmo_replaceable_or_arch_update *) [Finalise_AI_assms,wp]: end -context begin interpretation Arch . -requalify_consts replaceable_or_arch_update -end +arch_requalify_consts replaceable_or_arch_update interpretation Finalise_AI_3?: Finalise_AI_3 where replaceable_or_arch_update = replaceable_or_arch_update @@ -1912,7 +1908,7 @@ interpretation Finalise_AI_3?: Finalise_AI_3 by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma typ_at_data_at_wp: assumes typ_wp: "\a.\typ_at a p \ g \\s. typ_at a p\" @@ -1930,7 +1926,7 @@ interpretation Finalise_AI_4?: Finalise_AI_4 case 1 show ?case by (intro_locales; (unfold_locales; fact Finalise_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma set_asid_pool_obj_at_ptr: "\\s. P (ArchObj (arch_kernel_obj.ASIDPool mp))\ diff --git a/proof/invariant-abstract/AARCH64/ArchInterruptAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchInterruptAcc_AI.thy index 89d96eedf9..b1ad88de5d 100644 --- a/proof/invariant-abstract/AARCH64/ArchInterruptAcc_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInterruptAcc_AI.thy @@ -12,7 +12,7 @@ theory ArchInterruptAcc_AI imports InterruptAcc_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems InterruptAcc_AI_assms diff --git a/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy b/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy index 7a880be79a..d3948582f8 100644 --- a/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy @@ -9,7 +9,7 @@ theory ArchInterrupt_AI imports Interrupt_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming primrec arch_irq_control_inv_valid_real :: "arch_irq_control_invocation \ 'a::state_ext state \ bool" diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy index a9f92a1061..75d8ba5d37 100644 --- a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy @@ -9,7 +9,7 @@ theory ArchInvariants_AI imports InvariantsPre_AI "Eisbach_Tools.Apply_Trace_Cmd" begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming (* compatibility with other architectures, input only *) abbreviation @@ -29,7 +29,7 @@ record iarch_tcb = itcb_vcpu :: "obj_ref option" end_qualify -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming definition arch_tcb_to_iarch_tcb :: "arch_tcb \ iarch_tcb" where "arch_tcb_to_iarch_tcb arch_tcb \ \ itcb_vcpu = tcb_vcpu arch_tcb \" diff --git a/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy b/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy index fe7b74429a..1a33884511 100644 --- a/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchIpcCancel_AI.thy @@ -8,7 +8,7 @@ theory ArchIpcCancel_AI imports IpcCancel_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems IpcCancel_AI_assms diff --git a/proof/invariant-abstract/AARCH64/ArchIpc_AI.thy b/proof/invariant-abstract/AARCH64/ArchIpc_AI.thy index 448c7690d0..0c3835fe49 100644 --- a/proof/invariant-abstract/AARCH64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchIpc_AI.thy @@ -9,7 +9,7 @@ theory ArchIpc_AI imports Ipc_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Ipc_AI_assms @@ -499,7 +499,7 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact Ipc_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Ipc_AI_cont_assms diff --git a/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy b/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy index 4ec61c00b0..bcd7840fc9 100644 --- a/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy @@ -9,7 +9,7 @@ theory ArchKHeap_AI imports KHeapPre_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming definition non_vspace_obj :: "kernel_object \ bool" where "non_vspace_obj ko \ case ko of @@ -129,7 +129,7 @@ locale vspace_only_obj_pred = Arch + sublocale vspace_only_obj_pred < arch_only_obj_pred using vspace_pred_imp[OF vspace_only] by unfold_locales -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma valid_vspace_obj_lift: assumes "\T p. T \ AVCPU \ f \typ_at (AArch T) p\" diff --git a/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy b/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy index 5b0a5e6c44..c9e7d1dfc1 100644 --- a/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy @@ -12,7 +12,7 @@ imports Arch_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming text \ Showing that there is a state that satisfies the abstract invariants. diff --git a/proof/invariant-abstract/AARCH64/ArchLevityCatch_AI.thy b/proof/invariant-abstract/AARCH64/ArchLevityCatch_AI.thy index 925b19f736..8b22b3fd86 100644 --- a/proof/invariant-abstract/AARCH64/ArchLevityCatch_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchLevityCatch_AI.thy @@ -12,7 +12,7 @@ imports "Lib.SplitRule" begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma asid_high_bits_of_shift[simp]: "asid_high_bits_of (ucast x << asid_low_bits) = x" diff --git a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy index 1ed3288e1f..f8497bb8ad 100644 --- a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy @@ -13,7 +13,7 @@ theory ArchRetype_AI imports Retype_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Retype_AI_assms @@ -125,10 +125,7 @@ declare post_retype_invs_check_def[simp] end - -context begin interpretation Arch . -requalify_consts post_retype_invs_check -end +arch_requalify_consts post_retype_invs_check definition post_retype_invs :: "apiobject_type \ obj_ref list \ 'z::state_ext state \ bool" @@ -144,7 +141,7 @@ global_interpretation Retype_AI_post_retype_invs?: Retype_AI_post_retype_invs by (unfold_locales; fact post_retype_invs_def) -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma init_arch_objects_invs_from_restricted: "\post_retype_invs new_type refs @@ -177,7 +174,7 @@ global_interpretation Retype_AI_slot_bits?: Retype_AI_slot_bits qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma valid_untyped_helper [Retype_AI_assms]: assumes valid_c : "s \ c" @@ -274,6 +271,7 @@ locale retype_region_proofs_arch context retype_region_proofs begin +(* FIXME arch_split: is there any way to optimise this interpretation out? we can't nest contexts *) interpretation Arch . lemma valid_cap: @@ -580,7 +578,7 @@ sublocale retype_region_proofs_gen?: retype_region_proofs_gen end -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma unique_table_caps_null: "unique_table_caps_2 (null_filter caps) @@ -683,9 +681,7 @@ lemma cap_range_respects_device_region_cong[cong]: by (clarsimp simp: cap_range_respects_device_region_def) -context begin interpretation Arch . -requalify_consts region_in_kernel_window -end +arch_requalify_consts region_in_kernel_window context retype_region_proofs_arch begin @@ -875,7 +871,7 @@ lemmas post_retype_invs_axioms = retype_region_proofs_invs_axioms end -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Retype_AI_assms' @@ -905,7 +901,7 @@ global_interpretation Retype_AI?: Retype_AI qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma retype_region_plain_invs: "\invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz diff --git a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy index 29af15a82c..61c7cee033 100644 --- a/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchSchedule_AI.thy @@ -9,7 +9,7 @@ theory ArchSchedule_AI imports Schedule_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Schedule_AI_assms @@ -28,6 +28,7 @@ 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]: diff --git a/proof/invariant-abstract/AARCH64/ArchSyscall_AI.thy b/proof/invariant-abstract/AARCH64/ArchSyscall_AI.thy index 4293491321..6c673e874c 100644 --- a/proof/invariant-abstract/AARCH64/ArchSyscall_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchSyscall_AI.thy @@ -14,7 +14,7 @@ imports Syscall_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Syscall_AI_assms diff --git a/proof/invariant-abstract/AARCH64/ArchTcbAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchTcbAcc_AI.thy index 71494de427..99ad83388e 100644 --- a/proof/invariant-abstract/AARCH64/ArchTcbAcc_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchTcbAcc_AI.thy @@ -8,7 +8,7 @@ theory ArchTcbAcc_AI imports TcbAcc_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems TcbAcc_AI_assms diff --git a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy index 5ad151b3e7..6c37465baa 100644 --- a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy @@ -9,7 +9,7 @@ theory ArchTcb_AI imports Tcb_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Tcb_AI_assms @@ -159,7 +159,7 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact Tcb_AI_assms)?) qed -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma use_no_cap_to_obj_asid_strg: (* arch specific *) "(cte_at p s \ no_cap_to_obj_dr_emp cap s \ valid_cap cap s \ invs s) @@ -376,11 +376,6 @@ crunch invoke_tcb end -context begin interpretation Arch . -requalify_consts is_cnode_or_valid_arch -requalify_facts invoke_tcb_typ_at -end - global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = AARCH64.is_cnode_or_valid_arch proof goal_cases @@ -388,4 +383,8 @@ 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 diff --git a/proof/invariant-abstract/AARCH64/ArchUntyped_AI.thy b/proof/invariant-abstract/AARCH64/ArchUntyped_AI.thy index 3a046586e8..4c92fcba10 100644 --- a/proof/invariant-abstract/AARCH64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchUntyped_AI.thy @@ -9,7 +9,7 @@ theory ArchUntyped_AI imports Untyped_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming named_theorems Untyped_AI_assms diff --git a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy index 85de8526a7..aaeac4a458 100644 --- a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy @@ -9,7 +9,7 @@ theory ArchVCPU_AI imports AInvs begin -context Arch begin global_naming AARCH64 (*FIXME: arch_split*) +context Arch begin arch_global_naming (*FIXME: arch_split*) (* This is similar to cur_vcpu_2, but not close enough to reuse. *) definition active_cur_vcpu_of :: "'z state \ obj_ref option" where diff --git a/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy index f03ba67b39..816b92285f 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy @@ -9,7 +9,7 @@ theory ArchVSpaceEntries_AI imports VSpaceEntries_AI begin -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming (* Since we're not doing anything with the index apart from returning it, this definition works for both, NormalPTs and VSRootPTs *) diff --git a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy index d1fc5e4588..973d7e1ae6 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy @@ -21,7 +21,7 @@ lemma valid_asid_map_upd[simp]: end -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming sublocale set_vcpu: non_vspace_non_cap_non_mem_op "set_vcpu p vcpu" + @@ -2324,7 +2324,7 @@ lemma valid_vspace_obj: end -context Arch begin global_naming AARCH64 +context Arch begin arch_global_naming lemma set_asid_pool_arch_objs_map: "\valid_vspace_objs and valid_arch_state and valid_global_objs and @@ -3142,9 +3142,8 @@ crunch vcpu_switch end -context begin interpretation Arch . -requalify_facts +(* FIXME arch_split: move to generic theory? *) +arch_requalify_facts do_machine_op_valid_kernel_mappings -end end diff --git a/proof/invariant-abstract/AARCH64/Machine_AI.thy b/proof/invariant-abstract/AARCH64/Machine_AI.thy index 7fb8d8b961..200404b0ea 100644 --- a/proof/invariant-abstract/AARCH64/Machine_AI.thy +++ b/proof/invariant-abstract/AARCH64/Machine_AI.thy @@ -69,6 +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 text \Deterministic\ @@ -423,14 +424,10 @@ lemma dmo_gets_inv[wp]: end -context begin interpretation Arch . - requalify_facts - det_getRegister - det_setRegister - det_getRestartPC - det_setNextPC - -end + Arch.det_getRegister + Arch.det_setRegister + Arch.det_getRestartPC + Arch.det_setNextPC end diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index 2a898cbba6..9ae0cf8f98 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -11,17 +11,13 @@ imports ArchADT_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts (A) empty_context init_A_st + +arch_requalify_consts ptable_lift ptable_rights - addrFromPPtr - ptrFromPAddr - -end text \ The general refinement calculus (see theory Simulation) requires diff --git a/proof/invariant-abstract/BCorres_AI.thy b/proof/invariant-abstract/BCorres_AI.thy index 2649bf34c4..66a525cbad 100644 --- a/proof/invariant-abstract/BCorres_AI.thy +++ b/proof/invariant-abstract/BCorres_AI.thy @@ -16,6 +16,16 @@ abbreviation "bcorres \ bcorres_underlying truncate_state" abbreviation "s_bcorres \ s_bcorres_underlying truncate_state" +context Arch begin arch_global_naming + +crunch arch_post_cap_deletion + for (bcorres) bcorres[wp]: truncate_state + +end + +arch_requalify_facts + arch_post_cap_deletion_bcorres + lemma dxo_bcorres[wp]: "bcorres (do_extended_op f) (do_extended_op f)" apply (simp add: do_extended_op_def) @@ -63,16 +73,6 @@ lemma bcorres_select_ext[wp]: by (clarsimp simp: select_ext_def bind_def gets_def return_def select_def assert_def get_def select_switch_unit_def bcorres_underlying_def s_bcorres_underlying_def fail_def) -context Arch begin - -crunch arch_post_cap_deletion - for (bcorres) bcorres[wp]: truncate_state - -end - -requalify_facts - Arch.arch_post_cap_deletion_bcorres - crunch set_original, set_object, set_cap, set_irq_state, deleted_irq_handler, get_cap,set_cdt, empty_slot for (bcorres) bcorres[wp]: truncate_state diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index ac470e88d1..c41336582f 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -13,14 +13,10 @@ theory CNodeInv_AI imports ArchIpc_AI begin - -context begin interpretation Arch . -requalify_facts - set_cap_arch +arch_requalify_facts cte_at_length_limit arch_derive_cap_untyped valid_arch_mdb_cap_swap -end declare set_cap_arch[wp] diff --git a/proof/invariant-abstract/CSpaceInvPre_AI.thy b/proof/invariant-abstract/CSpaceInvPre_AI.thy index 3af1af7515..5e7956ee72 100644 --- a/proof/invariant-abstract/CSpaceInvPre_AI.thy +++ b/proof/invariant-abstract/CSpaceInvPre_AI.thy @@ -8,18 +8,13 @@ theory CSpaceInvPre_AI imports ArchAcc_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts table_cap_ref empty_table -requalify_facts +arch_requalify_facts empty_table_def -end - - lemma set_cap_caps_of_state[wp]: "\\s. P ((caps_of_state s) (ptr \ cap))\ set_cap cap ptr \\rv s. P (caps_of_state s)\" apply (cases ptr) @@ -141,8 +136,9 @@ lemma empty_table_caps_of: "empty_table S ko \ caps_of ko = {}" by (cases ko, simp_all add: empty_table_def caps_of_def cap_of_def) -context begin interpretation Arch . -lemma free_index_update_test_function_stuff[simp]: +(* FIXME arch_split: exports properties of functions that are not necessarily in global context, + and then they get placed in the global simpset *) +lemma (in Arch) free_index_update_test_function_stuff[simp]: "cap_asid (src_cap\free_index := a\) = cap_asid src_cap" "gen_obj_refs (src_cap\free_index := a\) = gen_obj_refs src_cap" "vs_cap_ref (src_cap\free_index := a\) = vs_cap_ref src_cap" @@ -152,6 +148,9 @@ lemma free_index_update_test_function_stuff[simp]: by (auto simp: cap_asid_def free_index_update_def vs_cap_ref_def is_cap_simps gen_obj_refs_def split: cap.splits arch_cap.splits) -end + +requalify_facts Arch.free_index_update_test_function_stuff + +lemmas [simp] = free_index_update_test_function_stuff end diff --git a/proof/invariant-abstract/CSpaceInv_AI.thy b/proof/invariant-abstract/CSpaceInv_AI.thy index 538d6d0a7f..3596331e20 100644 --- a/proof/invariant-abstract/CSpaceInv_AI.thy +++ b/proof/invariant-abstract/CSpaceInv_AI.thy @@ -12,31 +12,31 @@ theory CSpaceInv_AI imports ArchCSpaceInvPre_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts cap_master_arch_cap replaceable_final_arch_cap replaceable_non_final_arch_cap unique_table_refs -requalify_facts +(* There are multiple arch-dependent acap_rights_update_id, one for wellformed_acap, + one for valid_arch_cap. Prefer the latter. *) +arch_requalify_facts (aliasing) + acap_rights_update_id + +arch_requalify_facts aobj_ref_acap_rights_update arch_obj_size_acap_rights_update valid_arch_cap_acap_rights_update - valid_validate_vm_rights cap_master_arch_inv unique_table_refs_def valid_ipc_buffer_cap_def acap_rights_update_idem cap_master_arch_cap_rights - acap_rights_update_id is_nondevice_page_cap_simps set_cap_hyp_refs_of state_hyp_refs_of_revokable set_cap_hyp_refs_of is_valid_vtable_root_is_arch_cap -end lemma is_valid_vtable_root_simps[simp]: "\ is_valid_vtable_root (UntypedCap a b c d)" @@ -1053,17 +1053,15 @@ lemma get_cap_caps_of_state: "(fst (get_cap p s) = {(cap, s)}) = (Some cap = caps_of_state s p)" by (clarsimp simp: caps_of_state_def eq_commute) -context Arch begin - -lemma abj_ref_none_no_refs: +(* generic consequence of architecture-specific details *) +(* FIXME arch_split: no global naming? *) +lemma (in Arch) abj_ref_none_no_refs: "obj_refs c = {} \ table_cap_ref c = None" unfolding table_cap_ref_def apply (cases c; simp) subgoal for ac by (cases ac; simp) done -end - requalify_facts Arch.abj_ref_none_no_refs lemma no_cap_to_obj_with_diff_ref_Null: diff --git a/proof/invariant-abstract/CSpacePre_AI.thy b/proof/invariant-abstract/CSpacePre_AI.thy index f94098cb0d..9cc07003ef 100644 --- a/proof/invariant-abstract/CSpacePre_AI.thy +++ b/proof/invariant-abstract/CSpacePre_AI.thy @@ -12,15 +12,13 @@ theory CSpacePre_AI imports ArchCSpaceInv_AI begin -context begin interpretation Arch . -requalify_consts +arch_requalify_consts cap_asid is_simple_cap_arch is_derived_arch safe_parent_for_arch cap_asid_base cap_vptr -end lemma fun_upd_Some: "ms p = Some k \ (ms(a \ b)) p = Some (if a = p then b else k)" diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index 5d043c1782..9f9d26a088 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -12,25 +12,28 @@ theory CSpace_AI imports ArchCSpacePre_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts irq_state_update irq_state 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 is_derived_arch_non_arch ups_of_heap_non_arch_upd master_arch_cap_obj_refs master_arch_cap_cap_class same_aobject_as_commute arch_derive_cap_inv - loadWord_inv valid_global_refsD2 arch_derived_is_device - update_cnode_cap_data_def safe_parent_for_arch_not_arch safe_parent_cap_range_arch valid_arch_mdb_simple @@ -44,8 +47,6 @@ requalify_facts valid_arch_mdb_null_filter valid_arch_mdb_untypeds -end - declare set_cap_update_free_index_valid_arch_mdb[wp] (* Proofs don't want to see these details. *) diff --git a/proof/invariant-abstract/DetSchedAux_AI.thy b/proof/invariant-abstract/DetSchedAux_AI.thy index 2223ed31cf..046b794ec7 100644 --- a/proof/invariant-abstract/DetSchedAux_AI.thy +++ b/proof/invariant-abstract/DetSchedAux_AI.thy @@ -8,10 +8,9 @@ theory DetSchedAux_AI imports DetSchedInvs_AI begin -context begin interpretation Arch . +(* (* FIXME arch_split: check it's global on other arches *) requalify_facts - invoke_untyped_st_tcb_at -end + invoke_untyped_st_tcb_at *) crunch_ignore (del: cap_swap_ext cap_move_ext cap_insert_ext empty_slot_ext create_cap_ext tcb_sched_action diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index f9452d06bf..c4db9f5153 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -8,14 +8,12 @@ theory Deterministic_AI imports AInvs begin -context begin interpretation Arch . -requalify_facts +arch_requalify_facts update_work_units_empty_fail reset_work_units_empty_fail set_domain_empty_fail thread_set_domain_empty_fail arch_post_cap_deletion_valid_list -end lemmas [wp] = update_work_units_empty_fail diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 0e61737e84..6fe4089048 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -8,9 +8,7 @@ theory Detype_AI imports ArchRetype_AI begin -context begin interpretation Arch . - -requalify_facts +arch_requalify_facts valid_arch_mdb_detype clearMemory_invs invs_irq_state_independent @@ -18,8 +16,6 @@ requalify_facts caps_region_kernel_window_imp init_arch_objects_wps -end - declare clearMemory_invs[wp] declare invs_irq_state_independent[intro!, simp] diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index 126a8d275e..744447a57f 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -8,10 +8,9 @@ theory EmptyFail_AI imports ArchTcb_AI begin -context begin interpretation Arch . +(* FIXME arch_split: no global_naming *) requalify_facts - ef_machine_op_lift -end + Arch.ef_machine_op_lift lemmas [wp] = ef_ignore_failure ef_machine_op_lift diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 9361002b75..b1fcf80039 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -20,27 +20,26 @@ where | cap.Zombie r zb n \ {(r, replicate (zombie_cte_bits zb) False)} | _ \ {})" -context begin interpretation Arch . +arch_requalify_consts (A) + unmap_page -requalify_consts +arch_requalify_consts vs_cap_ref - unmap_page - clearMemory arch_post_cap_delete_pre +(* FIXME arch_split: no global_naming *) requalify_facts + Arch.no_irq_clearMemory + +arch_requalify_facts final_cap_lift - no_irq_clearMemory valid_global_refsD - valid_global_refsD2 arch_post_cap_deletion_valid_objs arch_post_cap_deletion_cte_wp_at arch_post_cap_deletion_caps_of_state arch_post_cap_deletion_irq_node arch_post_cap_deletion_invs -end - definition "post_cap_delete_pre cap cs \ case cap of IRQHandlerCap irq \ cap \ ran cs diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 2b94ccc0d0..9400285444 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -12,14 +12,8 @@ theory Interrupt_AI imports ArchIpc_AI begin - -context begin interpretation Arch . -requalify_consts - maxIRQ - -requalify_facts +arch_requalify_facts arch_post_cap_deletion_mdb_inv -end definition interrupt_derived :: "cap \ cap \ bool" diff --git a/proof/invariant-abstract/InvariantsPre_AI.thy b/proof/invariant-abstract/InvariantsPre_AI.thy index 0201647a67..3fc6876f9e 100644 --- a/proof/invariant-abstract/InvariantsPre_AI.thy +++ b/proof/invariant-abstract/InvariantsPre_AI.thy @@ -8,15 +8,12 @@ theory InvariantsPre_AI imports LevityCatch_AI begin -context begin interpretation Arch . - -requalify_types - aa_type - -requalify_consts +(* FIXME RAF: these already appear exported to global context?! +arch_requalify_types (A) aa_type -end +arch_requalify_consts (A) + aa_type *) (* FIXME: move *) declare ranI [intro] diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 09fbb5a5d3..845908d66b 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -9,16 +9,24 @@ theory Invariants_AI imports ArchInvariants_AI begin -context begin interpretation Arch . - -requalify_types +arch_requalify_types iarch_tcb -requalify_consts +arch_requalify_consts (A) + arch_cap_is_device + ASIDPoolObj + +(* we need to know the sizes of arch objects in the generic context *) +arch_requalify_facts (A) + cte_level_bits_def + tcb_bits_def + endpoint_bits_def + ntfn_bits_def + +arch_requalify_consts not_kernel_window global_refs arch_obj_bits_type - arch_cap_is_device is_nondevice_page_cap state_hyp_refs_of hyp_refs_of @@ -45,8 +53,6 @@ requalify_consts valid_global_vspace_mappings pspace_in_kernel_window - ASIDPoolObj - valid_vs_lookup user_mem device_mem @@ -59,7 +65,7 @@ requalify_consts vs_lookup vs_lookup_pages -requalify_facts +arch_requalify_facts valid_arch_sizes aobj_bits_T valid_arch_cap_def2 @@ -93,12 +99,13 @@ requalify_facts wellformed_arch_typ valid_arch_tcb_pspaceI valid_arch_tcb_lift - cte_level_bits_def obj_ref_not_arch_gen_ref arch_gen_ref_not_obj_ref arch_gen_obj_refs_inD same_aobject_same_arch_gen_refs valid_arch_mdb_eqI + iarch_tcb_context_set + iarch_tcb_set_registers lemmas [simp] = tcb_bits_def @@ -107,12 +114,10 @@ lemmas [simp] = iarch_tcb_context_set iarch_tcb_set_registers -end - -lemmas [intro!] = idle_global acap_rights_update_id +lemmas [intro!] = idle_global acap_rights_update_id -lemmas [simp] = acap_rights_update_id state_hyp_refs_update - tcb_arch_ref_simps hyp_live_tcb_simps hyp_refs_of_simps +lemmas [simp] = acap_rights_update_id state_hyp_refs_update + tcb_arch_ref_simps hyp_live_tcb_simps hyp_refs_of_simps \ \---------------------------------------------------------------------------\ @@ -1686,17 +1691,13 @@ lemma cte_wp_at_pspaceI: "\ cte_wp_at P slot s; kheap s = kheap s' \ \ cte_wp_at P slot s'" by (simp add: cte_wp_at_cases) -context Arch begin -lemma valid_arch_cap_pspaceI: +(* generic consequence of architecture-specific details *) +lemma (in Arch) valid_arch_cap_pspaceI: "\ valid_arch_cap acap s; kheap s = kheap s' \ \ valid_arch_cap acap s'" unfolding valid_arch_cap_def by (auto intro: obj_at_pspaceI split: arch_cap.split) -end -context begin interpretation Arch . -requalify_facts - valid_arch_cap_pspaceI -end +requalify_facts Arch.valid_arch_cap_pspaceI lemma valid_cap_pspaceI: "\ s \ cap; kheap s = kheap s' \ \ s' \ cap" @@ -2953,11 +2954,11 @@ lemma valid_idle_lift: lemmas caps_of_state_valid_cap = cte_wp_valid_cap [OF caps_of_state_cteD] - +(* generic consequence of architecture-specific details *) lemma (in Arch) obj_ref_is_arch: "\aobj_ref c = Some r; valid_arch_cap c s\ \ \ ako. kheap s r = Some (ArchObj ako)" -by (auto simp add: valid_arch_cap_def obj_at_def valid_arch_cap_ref_def split: arch_cap.splits if_splits) - + by (auto simp: valid_arch_cap_def obj_at_def valid_arch_cap_ref_def + split: arch_cap.splits if_splits) requalify_facts Arch.obj_ref_is_arch @@ -3264,7 +3265,7 @@ lemma invs_sym_refs [elim!]: "invs s \ sym_refs (state_refs_of s)" by (simp add: invs_def valid_state_def valid_pspace_def) -lemma invs_hyp_sym_refs [elim!]: (* ARMHYP move and requalify *) +lemma invs_hyp_sym_refs [elim!]: "invs s \ sym_refs (state_hyp_refs_of s)" by (simp add: invs_def valid_state_def valid_pspace_def) diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 613971c5c1..fbd43920f4 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -8,13 +8,12 @@ theory IpcCancel_AI imports ArchSchedule_AI begin -context begin interpretation Arch . - +(* FIXME arch_split: strange global_naming *) requalify_facts - arch_stit_invs - arch_post_cap_deletion_pred_tcb_at + Arch.arch_stit_invs -end +arch_requalify_facts + arch_post_cap_deletion_pred_tcb_at declare arch_post_cap_deletion_pred_tcb_at[wp] diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index d47d10b33d..af16acb055 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -10,25 +10,26 @@ imports "Monads.WPBang" begin -context begin interpretation Arch . -requalify_consts +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 lookup_ipc_buffer_inv set_mi_invs as_user_hyp_refs_of valid_arch_arch_tcb_set_registers - 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 - -end declare lookup_ipc_buffer_inv[wp] declare set_mi_invs[wp] diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index 937070e540..9294d03014 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -8,15 +8,18 @@ theory KHeap_AI imports ArchKHeap_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts obj_is_device valid_vso_at 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 pspace_in_kernel_window_atyp_lift valid_vspace_objs_lift_weak vs_lookup_vspace_obj_at_lift @@ -57,15 +60,10 @@ requalify_facts default_arch_object_not_live default_tcb_not_live - getActiveIRQ_neq_non_kernel - dmo_getActiveIRQ_non_kernel - valid_arch_tcb_same_type valid_arch_tcb_typ_at valid_tcb_arch_ref_lift -end - lemmas cap_is_device_obj_is_device[simp] = cap_is_device_obj_is_device lemmas storeWord_device_state_hoare[wp] = storeWord_device_state_inv diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index 10b229f813..fa3f444e8a 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -13,16 +13,13 @@ begin (* FIXME: eliminate mapM_UNIV_wp, use mapM_wp' directly *) lemmas mapM_UNIV_wp = mapM_wp' -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts ptrFromPAddr addrFromPPtr -requalify_facts + +arch_requalify_facts ptrFormPAddr_addFromPPtr aobj_ref_arch_cap -end - lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap lemma detype_arch_state: @@ -46,7 +43,6 @@ lemmas cap_irqs_simps[simp] = declare liftE_wp[wp] declare case_sum_True[simp] -declare select_singleton[simp] crunch_ignore (add: do_extended_op) diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index 08fb0e5487..6091a83335 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -15,14 +15,12 @@ begin abbreviation "up_aligned_area ptr sz \ {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}" abbreviation "down_aligned_area ptr sz \ {(ptr && ~~ mask sz) + (2 ^ sz - 1) .. ptr}" -context begin interpretation Arch . -requalify_facts +arch_requalify_facts global_refs_kheap valid_vspace_obj_default -requalify_consts - clearMemory + +arch_requalify_consts clearMemoryVM -end declare global_refs_kheap[simp] diff --git a/proof/invariant-abstract/Schedule_AI.thy b/proof/invariant-abstract/Schedule_AI.thy index f471e9a01f..b3e4be88fd 100644 --- a/proof/invariant-abstract/Schedule_AI.thy +++ b/proof/invariant-abstract/Schedule_AI.thy @@ -27,13 +27,11 @@ locale Schedule_AI = assumes stit_activatable: "\invs\ switch_to_idle_thread \\rv . (ct_in_state activatable :: 'a state \ bool)\" -context begin interpretation Arch . (* FIXME arch_split: some of these could be moved to generic theories so they don't need to be unqualified. *) requalify_facts - no_irq - no_irq_storeWord -end + Arch.no_irq + Arch.no_irq_storeWord crunch schedule_switch_thread_fastfail for inv[wp]: P diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 22715346a5..71e4197069 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -16,16 +16,18 @@ imports ArchInterrupt_AI begin -context begin interpretation Arch . requalify_facts - arch_decode_invocation_inv - lookup_cap_and_slot_inv + (* lookup_cap_and_slot_inv (* FIXME arch_split: check other arches to make sure this is global *) *) + Arch.resetTimer_device_state_inv + +arch_requalify_facts (A) data_to_cptr_def + +arch_requalify_facts + arch_decode_invocation_inv arch_post_cap_deletion_cur_thread arch_post_cap_deletion_state_refs_of arch_invoke_irq_handler_typ_at - resetTimer_device_state_inv -end lemmas [wp] = arch_decode_invocation_inv diff --git a/proof/invariant-abstract/TcbAcc_AI.thy b/proof/invariant-abstract/TcbAcc_AI.thy index 85c17f7675..7494233a23 100644 --- a/proof/invariant-abstract/TcbAcc_AI.thy +++ b/proof/invariant-abstract/TcbAcc_AI.thy @@ -8,9 +8,7 @@ theory TcbAcc_AI imports ArchCSpace_AI begin -context begin interpretation Arch . - -requalify_facts +arch_requalify_facts valid_arch_arch_tcb_context_set as_user_inv getRegister_inv @@ -18,8 +16,6 @@ requalify_facts declare user_getreg_inv[wp] -end - locale TcbAcc_AI_storeWord_invs = fixes state_ext_t :: "'state_ext::state_ext itself" assumes storeWord_invs[wp]: @@ -1130,7 +1126,6 @@ lemma kheap_Some_state_hyp_refs_ofD: "kheap s p = Some ko \ state_hyp_refs_of s p = hyp_refs_of ko" by (rule ko_at_state_hyp_refs_ofD; simp add: obj_at_def) -(* FIXME should be able to prove this in the generic context *) lemma sts_hyp_refs_of[wp]: "\\s. P (state_hyp_refs_of s)\ set_thread_state t st diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 55406a0718..bb98806023 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -8,13 +8,9 @@ theory Tcb_AI imports ArchCNodeInv_AI begin -context begin interpretation Arch . - -requalify_facts +arch_requalify_facts arch_derive_is_arch -end - locale Tcb_AI_1 = fixes state_ext_t :: "('state_ext::state_ext) itself" fixes is_cnode_or_valid_arch :: "cap \ bool" diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index c832c114c6..8ba8f5ebef 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -15,22 +15,14 @@ begin unbundle l4v_word_context (* because of Lib.MonadicRewrite *) -context begin interpretation Arch . - -requalify_consts - region_in_kernel_window - arch_default_cap +arch_requalify_consts second_level_tables safe_ioport_insert -requalify_facts - set_cap_valid_arch_caps_simple - set_cap_kernel_window_simple +arch_requalify_facts set_cap_ioports' safe_ioport_insert_triv -end - primrec valid_untyped_inv_wcap :: "Invocations_A.untyped_invocation \ cap option \ 'z::state_ext state \ bool" @@ -528,11 +520,6 @@ lemma range_cover_stuff: done qed (simp add: word_bits_def) -context Arch begin - (*FIXME: generify proof that uses this *) - lemmas range_cover_stuff_arch = range_cover_stuff[unfolded word_bits_def, simplified] -end - lemma cte_wp_at_range_cover: "\bits < word_bits; rv\ 2^ sz; invs s; diff --git a/proof/invariant-abstract/VSpacePre_AI.thy b/proof/invariant-abstract/VSpacePre_AI.thy index e4e17075f3..bec3a0b40c 100644 --- a/proof/invariant-abstract/VSpacePre_AI.thy +++ b/proof/invariant-abstract/VSpacePre_AI.thy @@ -12,13 +12,9 @@ theory VSpacePre_AI imports ArchTcbAcc_AI begin -context begin interpretation Arch . - -requalify_facts +arch_requalify_facts cap_master_cap_tcb_cap_valid_arch -end - lemma throw_on_false_wp[wp]: "\P\ f \\rv s. (rv \ Q () s) \ (\ rv \ E x s)\ \ \P\ throw_on_false x f \Q\,\E\" diff --git a/proof/invariant-abstract/VSpace_AI.thy b/proof/invariant-abstract/VSpace_AI.thy index 2e8513cb81..54a7294310 100644 --- a/proof/invariant-abstract/VSpace_AI.thy +++ b/proof/invariant-abstract/VSpace_AI.thy @@ -11,14 +11,14 @@ Architecture-independent VSpace invariant proofs theory VSpace_AI imports ArchVSpace_AI begin -context begin interpretation Arch . +(* FIXME arch_split: this should maybe have global_naming *) requalify_facts - pspace_respects_device_region_dmo - cap_refs_respects_device_region_dmo - ackInterrupt_device_state_inv + Arch.ackInterrupt_device_state_inv -end +arch_requalify_facts + pspace_respects_device_region_dmo + cap_refs_respects_device_region_dmo lemmas device_region_dmos = pspace_respects_device_region_dmo