From c6281810d4d6027714687343d55426a96fb41429 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 4 Jul 2023 12:46:41 +1000 Subject: [PATCH] aarch64 aspec+ainvs: add valid_asid_map invariant Refine needs slightly stricter information about asid maps, in particular we need to know explicitly that asid 0 never maps to a VSpace. This is the reverse of valid_vmid_table, but unfortunately does not fully follow from valid_vmid_table, because there can be VSpaces mapped without an assigned VMID. We shift the test for 0 < asid from entry_for_asid to vspace_for_asid so we can use entry_for_asid in the formulation of the invariant. Signed-off-by: Gerwin Klein --- .../invariant-abstract/AARCH64/ArchAcc_AI.thy | 22 ++++--- .../AARCH64/ArchArch_AI.thy | 6 +- .../AARCH64/ArchCNodeInv_AI.thy | 6 +- .../AARCH64/ArchDetype_AI.thy | 11 +++- .../AARCH64/ArchInvariants_AI.thy | 16 +++-- .../AARCH64/ArchKHeap_AI.thy | 13 ++++- .../AARCH64/ArchKernelInit_AI.thy | 5 +- .../AARCH64/ArchRetype_AI.thy | 13 ++++- .../AARCH64/ArchVSpace_AI.thy | 58 +++++++++++++++---- spec/abstract/AARCH64/ArchVSpace_A.thy | 2 +- 10 files changed, 116 insertions(+), 36 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy index 45bd52f4e..95f26f016 100644 --- a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy @@ -1180,13 +1180,9 @@ lemma set_pt_global_objs [wp]: crunch v_ker_map[wp]: set_pt "valid_kernel_mappings" (ignore: set_object wp: set_object_v_ker_map crunch_wps) - -lemma set_pt_asid_map [wp]: - "\valid_asid_map\ set_pt p pt \\_. valid_asid_map\" - apply (simp add: valid_asid_map_def vspace_at_asid_def) - apply (rule hoare_lift_Pf2 [where f="arch_state"]) - apply wp+ - done +lemma set_pt_asid_map[wp]: + "set_pt p pt \valid_asid_map\" + by (wp valid_asid_map_lift_strong) crunches store_pte for pred_tcb[wp]: "\s. Q (pred_tcb_at proj P t s)" @@ -1988,6 +1984,16 @@ lemma set_asid_pool_valid_asid_pool_caps[wp]: unfolding valid_asid_pool_caps_def by (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift') +lemma set_asid_pool_None_valid_asid_map[wp]: + "\ valid_asid_map and (\s. asid_pools_of s p = Some ap) \ + set_asid_pool p (ap (asid_low := None)) + \\_. valid_asid_map\" + unfolding valid_asid_map_def entry_for_asid_def + apply (clarsimp simp: obind_None_eq pool_for_asid_def) + apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift get_object_wp) + apply (fastforce simp: entry_for_pool_def obind_None_eq in_omonad split: if_split_asm) + done + lemma set_asid_pool_invs_unmap: "\invs and (\s. asid_pools_of s p = Some ap) and @@ -1996,7 +2002,7 @@ lemma set_asid_pool_invs_unmap: set_asid_pool p (ap (asid_low := None)) \\_. invs\" apply (simp add: invs_def valid_state_def valid_pspace_def - valid_arch_caps_def valid_asid_map_def) + valid_arch_caps_def) apply (wp valid_irq_node_typ set_asid_pool_typ_at set_asid_pool_vspace_objs_unmap valid_irq_handlers_lift diff --git a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy index 2c15e67eb..4d8c95525 100644 --- a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy @@ -438,7 +438,8 @@ lemma valid_arch_caps: lemma valid_asid_map': "valid_asid_map s \ valid_asid_map s'" - by (clarsimp simp: valid_asid_map_def) + by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def s'_def + entry_for_pool_def ko) lemma vspace_for_asid[simp]: "vspace_for_asid asid s' = vspace_for_asid asid s" @@ -624,7 +625,8 @@ lemma valid_asid_map_asid_upd_strg: asid_pools_of s ap = Some Map.empty \ asid_table s asid = None \ valid_asid_map (asid_table_update asid ap s)" - by (simp add: valid_asid_map_def) + by (simp add: valid_asid_map_def entry_for_asid_def obind_None_eq entry_for_pool_def + pool_for_asid_def) lemma valid_vspace_objs_asid_upd_strg: "valid_vspace_objs s \ diff --git a/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy b/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy index 182941905..049391739 100644 --- a/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy @@ -410,10 +410,8 @@ lemma cap_swap_asid_map[wp, CNodeInv_AI_assms]: cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\ cap_swap c a c' b \\rv. valid_asid_map\" - apply (simp add: cap_swap_def set_cdt_def valid_asid_map_def vspace_at_asid_def) - apply (rule hoare_pre) - apply (wp set_cap.vs_lookup|simp - |rule hoare_lift_Pf [where f=arch_state])+ + apply (simp add: cap_swap_def set_cdt_def vspace_at_asid_def) + apply (wp set_cap.vs_lookup|simp|rule hoare_lift_Pf [where f=arch_state])+ done diff --git a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy index 570eeb085..899b51d9d 100644 --- a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy @@ -496,8 +496,15 @@ proof - thus ?thesis by (simp add: valid_kernel_mappings_def detype_def ball_ran_eq) qed -lemma valid_asid_map_detype[detype_invs_proofs]: "valid_asid_map (detype (untyped_range cap) s)" - by (simp add: valid_asid_map_def) +lemma valid_asid_map_detype[detype_invs_proofs]: + "valid_asid_map (detype (untyped_range cap) s)" +proof - + have "valid_asid_map s" + using invs by (simp add: invs_def valid_state_def) + thus ?thesis + by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def + entry_for_pool_def) +qed lemma equal_kernel_mappings_detype[detype_invs_proofs]: "equal_kernel_mappings (detype (untyped_range cap) s)" diff --git a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy index 26708f3cf..af95b40d7 100644 --- a/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy @@ -633,7 +633,7 @@ definition valid_vmid_table_2 :: "(vmid \ asid) \ bo "valid_vmid_table_2 table \ \vmid. table vmid \ Some 0" locale_abbrev valid_vmid_table :: "'z::state_ext state \ bool" where - "valid_vmid_table s \ valid_vmid_table_2 (arm_vmid_table (arch_state s))" + "valid_vmid_table s \ valid_vmid_table_2 (vmid_table s)" lemmas valid_vmid_table_def = valid_vmid_table_2_def @@ -710,10 +710,10 @@ definition state_hyp_refs_of :: "'z::state_ext state \ obj_ref \ \s p. case_option {} (hyp_refs_of) (kheap s p)" -(* covered by ASIDPool case of valid_vspace_obj, vmid_inv, and definition of - vspace_for_asid (asid 0 never mapped) *) +(* Mostly covered by ASIDPool case of valid_vspace_obj and vmid_inv, but we still need to make sure + that ASID 0 is never mapped. *) definition valid_asid_map :: "'z::state_ext state \ bool" where - "valid_asid_map \ \" + "valid_asid_map \ \s. entry_for_asid 0 s = None" definition valid_global_objs :: "'z::state_ext state \ bool" where "valid_global_objs \ \" @@ -2599,7 +2599,7 @@ lemma vspace_for_asid_lift: apply (simp add: obind_def pool_for_asid_def o_def split del: if_split) apply (rule hoare_lift_Pf[where f=asid_table]) apply (rule hoare_lift_Pf[where f=asid_pools_of]) - apply (wpsimp wp: assms entry_for_asid_lift split: option.splits)+ + apply (wpsimp wp: assms entry_for_asid_lift split: option.splits split_del: if_split)+ done lemma valid_global_arch_objs_lift: @@ -2914,6 +2914,12 @@ lemma hyp_refs_of_rev: vcpu_tcb_refs_def refs_of_ao_def split: kernel_object.splits arch_kernel_obj.splits option.split) +lemma valid_asid_map_lift_strong: + assumes "\P. f \\s. P (asid_table s)\" + assumes "\P. f \\s. P (asid_pools_of s)\" + shows "f \valid_asid_map\" + by (wpsimp simp: valid_asid_map_def wp: entry_for_asid_lift assms) + end locale Arch_asid_table_update_eq = Arch + diff --git a/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy b/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy index 0cf607afb..52bea5306 100644 --- a/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy @@ -739,6 +739,12 @@ lemma valid_arch_caps_lift: apply (wpsimp wp: cap archvspace asidtable pts)+ done +lemma valid_asid_map_lift_strong: + assumes "\P. f \\s. P (asid_table s)\" + assumes "\P. f \\s. P (asid_pools_of s)\" + shows "f \valid_asid_map\" + by (wpsimp simp: valid_asid_map_def wp: entry_for_asid_lift assms) + context fixes f :: "'a::state_ext state \ ('b \ 'a state) set \ bool" assumes arch: "\P. f \\s. P (arch_state s)\" @@ -754,6 +760,9 @@ private lemma pred_vspace_objs_of_lift: "f \ \s. P (vspace_objs_ private lemma pred_pts_of_lift: "f \ \s. P (pts_of s) \" by (intro vspace_objs_of_pts_lift pred_vspace_objs_of_lift) +private lemma pred_asid_pools_of_lift: "f \ \s. P (asid_pools_of s) \" + by (intro vspace_objs_of_aps_lift pred_vspace_objs_of_lift) + lemma valid_global_vspace_mappings_lift: "f \valid_global_vspace_mappings\" unfolding valid_global_vspace_mappings_def @@ -770,8 +779,8 @@ lemma valid_global_objs_lift_weak: unfolding valid_global_objs_def by wp lemma valid_asid_map_lift: - "\valid_asid_map\ f \\rv. valid_asid_map\" - by (wpsimp simp: valid_asid_map_def) + "f \valid_asid_map\" + by (wp valid_asid_map_lift_strong arch pred_asid_pools_of_lift) lemma valid_kernel_mappings_lift: "\valid_kernel_mappings\ f \\rv. valid_kernel_mappings\" diff --git a/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy b/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy index d80db35e5..353e5f761 100644 --- a/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy @@ -390,9 +390,12 @@ lemma invs_A: apply (clarsimp simp: valid_arch_caps_def valid_asid_pool_caps_def unique_table_caps_def caps_of_state_init_A_st_Null valid_table_caps_def unique_table_refs_def) apply (clarsimp simp: state_defs) - apply (clarsimp simp: valid_global_objs_def valid_kernel_mappings_def valid_asid_map_def) + apply (clarsimp simp: valid_global_objs_def valid_kernel_mappings_def) apply (rule conjI) apply (clarsimp simp: equal_kernel_mappings_def) + apply (rule conjI) + apply (clarsimp simp: valid_asid_map_def entry_for_asid_def init_A_st_def init_arch_state_def + obind_def pool_for_asid_def) apply (simp add: pspace_in_kernel_window_init_A_st cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null valid_refs_def[unfolded cte_wp_at_caps_of_state]) done diff --git a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy index 4e4f75b43..12791169b 100644 --- a/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchRetype_AI.thy @@ -309,6 +309,14 @@ lemma asid_pools: by (clarsimp simp: in_opt_map_eq s'_def ps_def) (erule pspace_no_overlapC [OF orth _ _ cover vp]) +lemma asid_pools_of': + "asid_pools_of s' p = Some ap \ + asid_pools_of s p = Some ap \ ap = Map.empty \ p \ set (retype_addrs ptr ty n us)" + apply (clarsimp simp: in_opt_map_eq s'_def ps_def split: if_split_asm) + apply (auto simp: default_object_def default_arch_object_def empty_pt_def tyunt + split: apiobject_type.splits aobject_type.splits) + done + lemma pts_of: "pts_of s p = Some pt \ pts_of s' p = Some pt" by (clarsimp simp: in_opt_map_eq s'_def ps_def) @@ -716,7 +724,10 @@ lemma valid_kernel_mappings: lemma valid_asid_map: "valid_asid_map s \ valid_asid_map s'" - by (clarsimp simp: valid_asid_map_def) + apply (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def + entry_for_pool_def) + apply (fastforce dest!: asid_pools_of') + done lemma vspace_for_asid: "vspace_for_asid asid s' = Some pt \ vspace_for_asid asid s = Some pt" diff --git a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy index 0f2915ab3..f2da93553 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy @@ -13,6 +13,14 @@ theory ArchVSpace_AI imports VSpacePre_AI begin +context Arch_p_asid_table_update_eq begin (* FIXME AARCh64: move to ArchInvariants_AI *) + +lemma valid_asid_map_upd[simp]: + "valid_asid_map (f s) = valid_asid_map s" + by (simp add: valid_asid_map_def) + +end + context Arch begin global_naming AARCH64 sublocale @@ -182,7 +190,7 @@ lemma asid_high_bits_shl: lemma valid_asid_map_unmap: "valid_asid_map s \ is_aligned base asid_low_bits \ valid_asid_map(s\arch_state := arch_state s\arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\\)" - by (clarsimp simp: valid_asid_map_def) + by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def) lemma asid_low_bits_word_bits: "asid_low_bits < word_bits" @@ -715,7 +723,7 @@ lemma find_free_vmid_valid_arch [wp]: unfolding valid_arch_state_def by wpsimp lemma entry_for_asid_Some_vmidD: - "entry_for_asid asid s = Some entry \ ap_vmid entry = vmid_for_asid s asid \ 0 < asid" + "entry_for_asid asid s = Some entry \ ap_vmid entry = vmid_for_asid s asid" unfolding entry_for_asid_def vmid_for_asid_def entry_for_pool_def pool_for_asid_def by (auto simp: obind_def opt_map_def if_option split: option.splits) @@ -836,6 +844,22 @@ lemma valid_vmid_table_None_upd: "valid_vmid_table_2 table \ valid_vmid_table_2 (table(vmid := None))" by (simp add: valid_vmid_table_2_def) +lemma valid_vmid_table_Some_upd: + "\ valid_vmid_table_2 table; asid \ 0 \ \ valid_vmid_table_2 (table (vmid \ asid))" + by (simp add: valid_vmid_table_2_def) + +crunches update_asid_pool_entry, set_asid_pool + for pool_for_asid[wp]: "\s. P (pool_for_asid as s)" + (simp: pool_for_asid_def) + +lemma update_asid_pool_entry_valid_asid_map[wp]: + "update_asid_pool_entry f asid \valid_asid_map\" + unfolding valid_asid_map_def entry_for_asid_def + apply (clarsimp simp: obind_None_eq) + apply (wpsimp wp: hoare_vcg_disj_lift hoare_vcg_ex_lift) + apply (clarsimp simp: pool_for_asid_def entry_for_pool_def obind_None_eq split: if_split_asm) + done + lemma invalidate_asid_entry_invs[wp]: "invalidate_asid_entry asid \invs\" unfolding invalidate_asid_entry_def invalidate_asid_def invalidate_vmid_entry_def invs_def @@ -843,7 +867,7 @@ lemma invalidate_asid_entry_invs[wp]: supply fun_upd_apply[simp del] apply (wpsimp wp: load_vmid_wp valid_irq_handlers_lift valid_irq_node_typ valid_irq_states_triv valid_arch_caps_lift pspace_in_kernel_window_atyp_lift_strong - simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def + simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_global_vspace_mappings_def | wps)+ apply (clarsimp simp: valid_irq_node_def valid_global_refs_def global_refs_def valid_arch_state_def @@ -852,18 +876,17 @@ lemma invalidate_asid_entry_invs[wp]: valid_vmid_table_None_upd) done +crunches find_free_vmid, store_vmid + for valid_asid_map[wp]: valid_asid_map + lemma find_free_vmid_invs[wp]: "find_free_vmid \invs\" unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: load_vmid_wp valid_irq_handlers_lift valid_irq_node_typ valid_arch_caps_lift pspace_in_kernel_window_atyp_lift_strong - simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def + simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_global_vspace_mappings_def) -lemma valid_vmid_table_Some_upd: - "\ valid_vmid_table_2 table; asid \ 0 \ \ valid_vmid_table_2 (table (vmid \ asid))" - by (simp add: valid_vmid_table_2_def) - lemma store_hw_asid_valid_arch[wp]: "\valid_arch_state and (\s. asid_map s asid = None \ arm_vmid_table (arch_state s) vmid = None \ asid \ 0)\ store_vmid asid vmid @@ -881,7 +904,7 @@ lemma store_vmid_invs[wp]: unfolding invs_def valid_state_def valid_pspace_def by (wpsimp wp: valid_irq_node_typ valid_irq_handlers_lift valid_arch_caps_lift pspace_in_kernel_window_atyp_lift_strong - simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def + simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_global_vspace_mappings_def) lemma invalidate_vmid_entry_None[wp]: @@ -2394,6 +2417,20 @@ lemma set_asid_pool_valid_arch_state: unfolding valid_arch_state_def by (wpsimp wp: set_asid_pool_vmid_inv|wps)+ +lemma set_asid_pool_invs_valid_asid_map[wp]: + "\valid_asid_map and valid_asid_table and + (\s. asid_pools_of s ap = Some pool \ pool_for_asid asid s = Some ap \ asid \ 0)\ + set_asid_pool ap (pool(asid_low_bits_of asid \ ape)) + \\_. valid_asid_map\" + unfolding valid_asid_map_def entry_for_asid_def + apply (clarsimp simp: obind_None_eq) + apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift) + apply (fastforce simp: asid_high_low_inj pool_for_asid_def valid_asid_table_def entry_for_pool_def + obind_None_eq + dest: inj_on_domD + split: if_split_asm) + done + lemma set_asid_pool_invs_map: "\invs and (\s. asid_pools_of s ap = Some pool \ pool_for_asid asid s = Some ap \ @@ -2403,10 +2440,11 @@ lemma set_asid_pool_invs_map: and K (pool (asid_low_bits_of asid) = None \ 0 < asid \ ap_vmid ape = None)\ set_asid_pool ap (pool(asid_low_bits_of asid \ ape)) \\rv. invs\" - apply (simp add: invs_def valid_state_def valid_pspace_def valid_asid_map_def) + apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wpsimp wp: valid_irq_node_typ set_asid_pool_typ_at set_asid_pool_arch_objs_map valid_irq_handlers_lift set_asid_pool_valid_arch_caps_map set_asid_pool_valid_arch_state) + apply (clarsimp simp: valid_arch_state_def) done lemma ako_asid_pools_of: diff --git a/spec/abstract/AARCH64/ArchVSpace_A.thy b/spec/abstract/AARCH64/ArchVSpace_A.thy index b9df0bd59..14804557c 100644 --- a/spec/abstract/AARCH64/ArchVSpace_A.thy +++ b/spec/abstract/AARCH64/ArchVSpace_A.thy @@ -50,7 +50,6 @@ definition vspace_for_pool :: "obj_ref \ asid \ (obj_ref (* this is what asid_map encodes in ARM/ARM_HYP; getASIDPoolEntry in Haskell *) definition entry_for_asid :: "asid \ 'z::state_ext state \ asid_pool_entry option" where "entry_for_asid asid = do { - oassert (0 < asid); pool_ptr \ pool_for_asid asid; entry_for_pool pool_ptr asid \ asid_pools_of }" @@ -68,6 +67,7 @@ definition update_asid_pool_entry :: definition vspace_for_asid :: "asid \ 'z::state_ext state \ obj_ref option" where "vspace_for_asid asid = do { + oassert (0 < asid); entry \ entry_for_asid asid; oreturn $ ap_vspace entry }"