From de8ebe7219cb210ed8b7907bf0f09542685509ba Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 8 Jul 2022 12:32:06 +1000 Subject: [PATCH] aarch64 ainvs: reduce sorries in ArchAcc_AI Co-authored-by: Rafal Kolanski Signed-off-by: Gerwin Klein --- .../invariant-abstract/AARCH64/ArchAcc_AI.thy | 119 +++++++----------- 1 file changed, 44 insertions(+), 75 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy index 92fb9fd67..c04d50c38 100644 --- a/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchAcc_AI.thy @@ -1083,16 +1083,20 @@ lemma set_pt_table_caps[wp]: apply (clarsimp simp: opt_map_def fun_upd_apply split: option.splits) done +(* FIXME AARCH64: move *) +lemma pt_upd_empty_InvalidPTE[simp]: + "pt_upd (empty_pt pt_t) idx InvalidPTE = empty_pt pt_t" + by (auto simp: pt_upd_def empty_pt_def split: pt.splits) + lemma store_pte_valid_table_caps: "\ valid_table_caps and (\s. valid_caps (caps_of_state s) s) and (\s. (\slot asidopt. caps_of_state s slot = Some (ArchObjectCap (PageTableCap (table_base pt_t p) pt_t asidopt)) - \ asidopt = None \ pte = InvalidPTE)) \ + \ asidopt = None \ pte = InvalidPTE)) \ store_pte pt_t p pte \\rv. valid_table_caps\" unfolding store_pte_def - sorry (* FIXME AARCH64 by wpsimp - (fastforce simp: valid_table_caps_def pts_of_ko_at obj_at_def) *) + (fastforce simp: valid_table_caps_def pts_of_ko_at obj_at_def) lemma set_object_caps_of_state: "\(\s. \tcb_at p s \ \(\n. cap_table_at n p s)) and @@ -1173,7 +1177,7 @@ lemma pt_walk_eqI: level < level' \ pt_walk top_level level' pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts) = Some (level', pt_ptr') \ pts' pt_ptr' = pts pt_ptr'; - is_aligned pt_ptr (pt_bits top_level) \ + is_aligned pt_ptr (pt_bits top_level); top_level \ max_pt_level \ \ pt_walk top_level level pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts') = pt_walk top_level level pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts)" apply (induct top_level arbitrary: pt_ptr; clarsimp) @@ -1186,21 +1190,18 @@ lemma pt_walk_eqI: apply clarsimp apply (rename_tac pte) apply (drule_tac x="pptr_from_pte pte" in meta_spec) - apply (erule meta_impE; simp?) + apply (erule meta_impE; (simp add: pptr_from_pte_aligned_pt_bits)?) apply clarsimp - sorry (* FIXME AARCH64 - apply (subgoal_tac "is_aligned pt_ptr pt_bits \ pts' pt_ptr = pts pt_ptr") - prefer 2 + apply (prop_tac "is_aligned pt_ptr (pt_bits (level_type top_level)) \ pts' pt_ptr = pts pt_ptr") subgoal by simp apply (erule_tac x=level' in allE, simp) apply (erule_tac x=pt_ptr' in allE) apply (erule impE; assumption?) apply (subst pt_walk.simps) - apply (subgoal_tac "level' < top_level") - prefer 2 + apply (prop_tac "level' < top_level") apply (fastforce dest!: pt_walk_max_level simp: le_less_trans) apply (fastforce simp: level_pte_of_def in_omonad) - done *) + done lemma valid_vspace_obj_valid_pte_upd: "\ valid_vspace_obj level (PageTable pt) s; valid_pte level pte s \ @@ -1220,21 +1221,20 @@ lemma pte_of_pt_slot_offset_of_empty_pt: lemma pt_walk_non_empty_ptD: "\ pt_walk level bot_level pt_ptr vref (\pt_t p. level_pte_of pt_t p pts) = Some (level', p); pts pt_ptr = Some pt; is_aligned pt_ptr (pt_bits level) \ - \ (pt \ empty_pt pt_t \ (level' = level \ p = pt_ptr))" + \ (pt \ empty_pt (level_type level) \ (level' = level \ p = pt_ptr))" apply (subst (asm) pt_walk.simps) apply (case_tac "bot_level < level") apply (clarsimp simp: in_omonad) apply (prop_tac "v' = InvalidPTE") - sorry (* FIXME AARCH64 apply (drule_tac vref=vref and level=level in pte_of_pt_slot_offset_of_empty_pt, clarsimp+) - done *) + done lemma pt_walk_pt_upd_idem: "\ \level' pt_ptr'. level < level' \ pt_walk top_level level' pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts) = Some (level', pt_ptr') \ pt_ptr' \ obj_ref; - is_aligned pt_ptr (pt_bits top_level) \ + is_aligned pt_ptr (pt_bits top_level); top_level \ max_pt_level \ \ pt_walk top_level level pt_ptr vptr (\pt_t p. level_pte_of pt_t p (pts(obj_ref := pt))) = pt_walk top_level level pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts)" by (rule pt_walk_eqI; auto) @@ -1244,7 +1244,7 @@ lemma pt_walk_upd_idem: level < level' \ pt_walk top_level level' pt_ptr vptr (ptes_of s) = Some (level', pt_ptr') \ pt_ptr' \ obj_ref; - is_aligned pt_ptr (pt_bits top_level) \ + is_aligned pt_ptr (pt_bits top_level); top_level \ max_pt_level \ \ pt_walk top_level level pt_ptr vptr (ptes_of (s\kheap := kheap s(obj_ref \ ko)\)) = pt_walk top_level level pt_ptr vptr (ptes_of s)" by (rule pt_walk_eqI; simp split del: if_split) @@ -1290,21 +1290,21 @@ lemma vs_lookup_table_eqI: apply (clarsimp simp: asid_pool_level_eq[symmetric] vs_lookup_table_def in_omonad pool_for_asid_def) apply (rule obind_eqI; fastforce simp: pool_for_asid_def) + (* pt_walk case: *) apply (simp (no_asm) add: vs_lookup_table_def in_omonad) apply (rule obind_eqI_full; simp add: pool_for_asid_def) apply (rename_tac pool_ptr) apply (rule obind_eqI_full; clarsimp) apply (erule_tac x=asid_pool_level in allE) - sorry (* FIXME AARCH64 apply (fastforce simp: pool_for_asid_vs_lookup pool_for_asid_def vspace_for_pool_def obind_def - order.not_eq_order_implies_strict) + entry_for_pool_def order.not_eq_order_implies_strict + split: option.splits) apply (rename_tac root) - apply (rule pt_walk_eqI) - apply clarsimp + apply (rule pt_walk_eqI; clarsimp) apply (frule pt_walk_max_level) - apply (fastforce simp add: vs_lookup_table_def in_omonad asid_pool_level_eq pool_for_asid_def) - apply (rule vspace_for_pool_is_aligned; fastforce simp add: pool_for_asid_def) - done *) + apply (fastforce simp: vs_lookup_table_def in_omonad asid_pool_level_eq pool_for_asid_def) + apply (rule vspace_for_pool_is_aligned; fastforce simp: pool_for_asid_def) + done lemma vs_lookup_table_upd_idem: "\ \level' p'. @@ -1362,13 +1362,11 @@ lemma pt_walk_Some_finds_pt: done lemma pte_of_pt_slot_offset_upd_idem: - "\ is_aligned pt_ptr (pt_bits pt_t); obj_ref \ pt_ptr \ + "\ is_aligned pt_ptr (pt_bits pt_t); obj_ref \ pt_ptr; pt_t = level_type level \ \ level_pte_of pt_t (pt_slot_offset level pt_ptr vptr) (pts(obj_ref := pt')) = level_pte_of pt_t (pt_slot_offset level pt_ptr vptr) pts" unfolding level_pte_of_def - sorry (* FIXME AARCH64: might need (level_type level) instead of pt_t by (rule obind_eqI; clarsimp simp: in_omonad)+ - *) lemma pt_lookup_target_pt_eqI: "\ \level' pt_ptr'. @@ -1382,9 +1380,10 @@ lemma pt_lookup_target_pt_eqI: = pt_walk max_pt_level level pt_ptr vptr (\pt_t p. level_pte_of pt_t p pts)") prefer 2 apply (rule pt_walk_eqI; assumption?) - apply (intro allI impI) - apply (erule_tac x=level' in allE) - apply fastforce + apply (intro allI impI) + apply (erule_tac x=level' in allE) + apply fastforce + apply simp apply (rule obind_eqI, assumption) apply (rule obind_eqI; clarsimp) apply (rule obind_eqI; clarsimp) @@ -1493,28 +1492,17 @@ lemma set_pt_caps_respects_device_region[wp]: arch_kernel_obj.split_asm) done - lemma set_pt_valid_ioc[wp]: - "\valid_ioc\ set_pt p pt \\_. valid_ioc\" - apply (simp add: set_pt_def) - apply (wp set_object_valid_ioc_no_caps get_object_wp) - sorry (* FIXME AARCH64 - by (clarsimp simp: a_type_simps obj_at_def is_tcb is_cap_table - split: kernel_object.splits arch_kernel_obj.splits) *) - - + "set_pt p pt \valid_ioc\" + unfolding set_pt_def + by (wpsimp wp: set_object_wp_strong) + (fastforce simp: valid_ioc_def cte_wp_at_cases obj_at_def) lemma valid_machine_stateE: assumes vm: "valid_machine_state s" - assumes e: "\in_user_frame p s - \ underlying_memory (machine_state s) p = 0 \ \ E " + assumes e: "\in_user_frame p s \ underlying_memory (machine_state s) p = 0 \ \ E" shows E - using vm - apply (clarsimp simp: valid_machine_state_def) - apply (drule_tac x = p in spec) - apply (rule e) - apply auto - done + using vm by (auto simp: valid_machine_state_def intro: e) lemma in_user_frame_same_type_upd: "\typ_at type p s; type = a_type obj; in_user_frame q s\ @@ -1532,22 +1520,11 @@ lemma in_device_frame_same_type_upd: apply (auto simp: a_type_simps) done -lemma store_word_offs_in_user_frame[wp]: - "\\s. in_user_frame p s\ store_word_offs a x w \\_ s. in_user_frame p s\" - unfolding in_user_frame_def - by (wp hoare_vcg_ex_lift) - lemma store_word_offs_in_device_frame[wp]: "\\s. in_device_frame p s\ store_word_offs a x w \\_ s. in_device_frame p s\" unfolding in_device_frame_def by (wp hoare_vcg_ex_lift) - -lemma as_user_in_user_frame[wp]: - "\\s. in_user_frame p s\ as_user t m \\_ s. in_user_frame p s\" - unfolding in_user_frame_def - by (wp hoare_vcg_ex_lift) - lemma as_user_in_device_frame[wp]: "\\s. in_device_frame p s\ as_user t m \\_ s. in_device_frame p s\" unfolding in_device_frame_def @@ -1561,18 +1538,11 @@ lemma load_word_offs_in_user_frame[wp]: by (wp hoare_vcg_ex_lift) lemma valid_machine_state_heap_updI: -assumes vm : "valid_machine_state s" -assumes tyat : "typ_at type p s" -shows - " a_type obj = type \ valid_machine_state (s\kheap := kheap s(p \ obj)\)" - apply (clarsimp simp: valid_machine_state_def) - subgoal for p - apply (rule valid_machine_stateE[OF vm,where p = p]) - apply (elim disjE,simp_all) - apply (drule(1) in_user_frame_same_type_upd[OF tyat]) - apply simp+ - done - done + "\ valid_machine_state s; typ_at type p s; a_type obj = type \ + \ valid_machine_state (s\kheap := kheap s(p \ obj)\)" + by (fastforce simp: valid_machine_state_def + intro: in_user_frame_same_type_upd + elim: valid_machine_stateE) lemma set_pt_vms[wp]: "\valid_machine_state\ set_pt p pt \\_. valid_machine_state\" @@ -1753,9 +1723,8 @@ lemma vs_lookup_target_unreachable_upd_idem: (* level' = asid_pool_level *) apply (rename_tac pool_ptr) apply (drule vs_lookup_level, drule vs_lookup_level) - apply (clarsimp simp: pool_for_asid_vs_lookup vspace_for_pool_def in_omonad) - apply (rule obind_eqI[rotated], fastforce) - sorry (* FIXME AARCH64 + apply (clarsimp simp: pool_for_asid_vs_lookup vspace_for_pool_def entry_for_pool_def in_omonad) + apply (rule obind_eqI[rotated], fastforce)+ apply (case_tac "pool_ptr = obj_ref"; clarsimp) apply (erule_tac x=asid_pool_level in allE) apply (fastforce simp: pool_for_asid_vs_lookup) @@ -1765,11 +1734,11 @@ lemma vs_lookup_target_unreachable_upd_idem: apply (rename_tac pt_ptr level') apply (case_tac "pt_ptr = obj_ref") apply (fastforce dest: vs_lookup_level) - apply (rule pte_refs_of_eqI, rule ptes_of_eqI) - apply (prop_tac "is_aligned pt_ptr pt_bits") + apply (rule pte_refs_of_eqI, rule level_ptes_of_eqI) + apply (prop_tac "is_aligned pt_ptr (pt_bits (level_type level'))") apply (erule vs_lookup_table_is_aligned; fastforce) apply (clarsimp simp: fun_upd_def opt_map_def split: option.splits) - done *) + done lemma vs_lookup_target_unreachable_upd_idem': "\ \(\level. \\ (level, obj_ref) s);