From ce9f9ffe6041bd80593344c779fb10b6a78e075a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 17 Feb 2021 20:59:13 +1100 Subject: [PATCH] isabelle-2021: update DRefine Signed-off-by: Gerwin Klein --- proof/drefine/Arch_DR.thy | 37 +-- proof/drefine/CNode_DR.thy | 62 ++-- proof/drefine/Corres_D.thy | 25 +- proof/drefine/Finalise_DR.thy | 477 +++++++++++++-------------- proof/drefine/Intent_DR.thy | 7 +- proof/drefine/Ipc_DR.thy | 104 +++--- proof/drefine/KHeap_DR.thy | 12 +- proof/drefine/Schedule_DR.thy | 1 - proof/drefine/StateTranslation_D.thy | 7 +- proof/drefine/Syscall_DR.thy | 2 + proof/drefine/Untyped_DR.thy | 22 +- 11 files changed, 361 insertions(+), 395 deletions(-) diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index cd365d623..8a2417e6d 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -216,7 +216,7 @@ proof - have aligned_4_hd: "\r :: word32. is_aligned r 6 \ hd (map (\x. x + r) [0 , 4 .e. 0x3C]) = r" apply (subgoal_tac "r \ r + 0x3C") - apply (clarsimp simp: upto_enum_step_def less_def o_def | intro conjI)+ + apply (clarsimp simp: upto_enum_step_def o_def | intro conjI)+ apply (subst hd_map) apply (clarsimp simp:upto_enum_def) apply (clarsimp simp:upto_enum_def hd_map) @@ -1270,6 +1270,7 @@ lemma store_pte_page_inv_entries_safe: \\rv s. (\f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (hd bb && ~~ mask pt_bits) s \ (\slot\set (tl bb). f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE)) \ (\sl\set (tl bb). sl && ~~ mask pt_bits = hd bb && ~~ mask pt_bits)\" + including no_take_bit apply (simp add:store_pte_def set_pt_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp:obj_at_def page_inv_entries_safe_def split:if_splits) @@ -1286,11 +1287,11 @@ lemma store_pte_page_inv_entries_safe: apply simp apply (subst (asm) is_aligned_shiftr_add) apply (erule is_aligned_after_mask) - apply (simp add:pt_bits_def pageBits_def)+ - apply (simp add:is_aligned_shiftl_self) - apply (rule shiftl_less_t2n) - apply (rule word_of_nat_less,simp) - apply simp+ + apply (simp add:pt_bits_def pageBits_def)+ + apply (simp add:is_aligned_shiftl_self) + apply (rule shiftl_less_t2n) + apply (rule word_of_nat_less,simp) + apply simp+ apply (subst (asm) ucast_add) apply simp apply simp @@ -1298,7 +1299,7 @@ lemma store_pte_page_inv_entries_safe: apply simp apply (rule word_of_nat_less) apply simp - apply (simp add:ucast_of_nat_small of_nat_neq_0) + apply (simp add:ucast_of_nat_small of_nat_neq_0 del: word_of_nat_eq_0_iff) apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n image_def) apply (simp add:field_simps) @@ -1312,13 +1313,13 @@ lemma store_pde_page_inv_entries_safe: \\rv s. (\f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (hd bb && ~~ mask pd_bits) s \ (\slot\set (tl bb). f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE)) \ (\sl\set (tl bb). sl && ~~ mask pd_bits = hd bb && ~~ mask pd_bits)\" + including no_take_bit apply (simp add:store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp simp:obj_at_def page_inv_entries_safe_def split:if_splits) apply (intro conjI impI) - apply (clarsimp simp:hd_map_simp upto_enum_def - upto_enum_step_def drop_map - tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n) + apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def drop_map + tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n) apply (clarsimp simp add:field_simps) apply (subst (asm) shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric])+ apply (subst (asm) and_mask_plus[where a = "of_nat slot << 2"]) @@ -1328,11 +1329,11 @@ lemma store_pde_page_inv_entries_safe: apply simp apply (subst (asm) is_aligned_shiftr_add) apply (erule is_aligned_after_mask) - apply (simp add:pd_bits_def pageBits_def)+ - apply (simp add:is_aligned_shiftl_self) - apply (rule shiftl_less_t2n) - apply (rule word_of_nat_less,simp) - apply simp+ + apply (simp add:pd_bits_def pageBits_def)+ + apply (simp add:is_aligned_shiftl_self) + apply (rule shiftl_less_t2n) + apply (rule word_of_nat_less,simp) + apply simp+ apply (subst (asm) ucast_add) apply simp apply simp @@ -1340,7 +1341,7 @@ lemma store_pde_page_inv_entries_safe: apply simp apply (rule word_of_nat_less) apply simp - apply (simp add:ucast_of_nat_small of_nat_neq_0) + apply (simp add:ucast_of_nat_small of_nat_neq_0 del: word_of_nat_eq_0_iff) apply (clarsimp simp: hd_map_simp upto_enum_def upto_enum_step_def tl_map_simp map_eq_Cons_conv upt_eq_Cons_conv upto_0_to_n image_def) apply (simp add: field_simps) @@ -1676,10 +1677,6 @@ proof - apply (clarsimp simp:perform_asid_control_invocation_def) apply (simp add:arch_invocation_relation_def translate_arch_invocation_def) apply (cases asid_inv, clarsimp) - apply hypsubst_thin - apply (drule sym) - apply (drule sym) - apply clarsimp apply (rule corres_guard_imp) apply (rule corres_split_deprecated [OF _ delete_objects_dcorres]) apply (rule corres_symb_exec_r) diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index 1d0aaa883..ed4b9e346 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -916,7 +916,7 @@ lemma dcorres_ep_cancel_badge_sends: apply (rule corres_guard_imp[OF filter_modify_empty_corres]) apply (clarsimp simp:invs_def) apply (frule_tac epptr = epptr in get_endpoint_pick ,simp add:obj_at_def) - apply (cut_tac ep = epptr and s = "transform s'a" in is_thread_blocked_on_sth) + apply (cut_tac ep = epptr and s = "transform s'" in is_thread_blocked_on_sth) apply (drule_tac x = x in eqset_imp_iff) apply (clarsimp simp: valid_state_def valid_ep_abstract_def none_is_sending_ep_def none_is_receiving_ep_def) @@ -940,7 +940,7 @@ lemma dcorres_ep_cancel_badge_sends: apply (simp add:valid_ep_def) apply (simp add:inj_on_def) apply (simp add:is_thread_blocked_on_sth[simplified]) - apply (subgoal_tac "valid_idle s' \ valid_etcbs s'") + apply (subgoal_tac "valid_idle s'a \ valid_etcbs s'a") apply (clarsimp simp: ntfn_waiting_set_lift ep_waiting_set_send_lift ep_waiting_set_recv_lift) apply (subst ntfn_waiting_set_upd_kh) @@ -966,7 +966,7 @@ lemma dcorres_ep_cancel_badge_sends: get_thread_state_def) apply (rule_tac Q'="\s. valid_idle s \ valid_etcbs s \ not_idle_thread a s - \ idle_thread s = idle_thread s'a \ + \ idle_thread s = idle_thread s' \ st_tcb_at (\ts. \pl. ts = Structures_A.thread_state.BlockedOnSend epptr pl) a s" in corres_guard_imp[where Q=\]) apply (rule dcorres_absorb_gets_the) @@ -995,7 +995,7 @@ lemma dcorres_ep_cancel_badge_sends: dest!: get_tcb_rev) apply (rule ext) apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) - apply (case_tac "a=idle_thread s'", simp add: not_idle_thread_def) + apply (case_tac "a=idle_thread s'a", simp add: not_idle_thread_def) apply (drule (2) transform_objects_tcb) apply (clarsimp simp: transform_current_thread_def transform_def) apply (clarsimp simp: not_idle_thread_def transform_tcb_def transform_def @@ -1004,7 +1004,7 @@ lemma dcorres_ep_cancel_badge_sends: apply simp+ apply (clarsimp simp:bind_assoc not_idle_thread_def) apply (wp sts_st_tcb_at_neq) - apply (rule_tac Q="\r a. valid_idle a \ idle_thread a = idle_thread s'a \ + apply (rule_tac Q="\r a. valid_idle a \ idle_thread a = idle_thread s' \ st_tcb_at (\ts. \pl. ts = Structures_A.thread_state.BlockedOnSend epptr pl) y a \ y \ idle_thread a \ valid_etcbs a" in hoare_strengthen_post) apply wp @@ -1132,6 +1132,7 @@ lemma set_asid_pool_empty'_helper: "n < 1023 \ (if x = ucast ((1 :: word32) + of_nat n) then None else if x \ of_nat n then None else ap x) = (if (x :: 10 word) \ 1 + of_nat n then None else ap x)" + including no_take_bit apply (frule of_nat_mono_maybe[where x="2^10 - 1" and 'a=10, simplified]) apply (subgoal_tac "ucast (1 + of_nat n :: word32) = (1 + of_nat n :: 10 word)") prefer 2 @@ -1273,8 +1274,8 @@ lemma dcorres_set_asid_pool_empty: apply clarsimp apply (clarsimp simp del:set_map simp: suffix_def) apply (wp | clarsimp simp:swp_def)+ - apply (clarsimp simp:list_all2_iff transform_asid_def asid_low_bits_def set_zip) - apply (clarsimp simp:unat_ucast upto_enum_def unat_of_nat) + apply (clarsimp simp:list_all2_iff transform_asid_def asid_low_bits_def set_zip) + apply (clarsimp simp: upto_enum_def take_bit_nat_eq_self) done declare fun_upd_apply[simp] @@ -1321,9 +1322,8 @@ lemma dcorres_clear_object_caps_asid_pool: apply clarsimp apply (clarsimp simp:invs_def valid_state_def valid_cap_def obj_at_def a_type_def valid_pspace_def dest!: cte_wp_valid_cap) - apply (clarsimp split:Structures_A.kernel_object.split_asm - arch_kernel_obj.split_asm if_splits) - done + by (clarsimp split: Structures_A.kernel_object.split_asm + arch_kernel_obj.split_asm if_splits) lemmas valid_idle_invs_strg = invs_valid_idle_strg @@ -1565,27 +1565,26 @@ lemma copy_global_mappings_dwp: "is_aligned word pd_bits\ \\ps. valid_idle (ps :: det_state) \ transform ps = cs\ copy_global_mappings word \\r s. transform s = cs\" apply (simp add:copy_global_mappings_def) apply wp - apply (rule_tac Q = "\r s. valid_idle s \ transform s = cs" in hoare_strengthen_post) - apply (rule mapM_x_wp') - apply wp - apply (rule_tac Q="\s. valid_idle s \ transform s = cs" in hoare_vcg_precond_imp) - apply (rule dcorres_to_wp) - apply (rule corres_guard_imp[OF store_pde_set_cap_corres]) - apply (clarsimp simp:kernel_mapping_slots_def) - apply (simp add:ucast_def kernel_base_def pd_bits_def pageBits_def) - apply (simp add:mask_add_aligned) - apply (subst less_mask_eq,simp) - apply (simp add:shiftl_t2n) - apply (subst mult.commute) - apply (rule div_lt_mult,simp+,unat_arith,simp+) - apply (simp add:shiftl_shiftr1 word_size) - apply (subst less_mask_eq,simp) - apply unat_arith - apply (fold ucast_def) - apply (subst ucast_le_migrate[symmetric]) - apply (simp add:word_size,unat_arith) - apply (simp add:word_size)+ - apply (wp|clarsimp)+ + apply (rule_tac Q = "\r s. valid_idle s \ transform s = cs" in hoare_strengthen_post) + apply (rule mapM_x_wp') + apply wp + apply (rule_tac Q="\s. valid_idle s \ transform s = cs" in hoare_vcg_precond_imp) + apply (rule dcorres_to_wp) + apply (rule corres_guard_imp[OF store_pde_set_cap_corres]) + apply (clarsimp simp:kernel_mapping_slots_def) + apply (simp add: kernel_base_def pd_bits_def pageBits_def) + apply (simp add: mask_add_aligned) + apply (subst less_mask_eq,simp) + apply (simp add:shiftl_t2n) + apply (subst mult.commute) + apply (rule div_lt_mult,simp+,unat_arith,simp+) + apply (simp add:shiftl_shiftr1 word_size) + apply (subst less_mask_eq,simp) + apply unat_arith + apply (subst ucast_le_migrate[symmetric]) + apply (simp add:word_size,unat_arith) + apply (simp add:word_size)+ + apply (wp|clarsimp)+ done lemma opt_cap_pd_not_None: @@ -1683,6 +1682,7 @@ lemma dcorres_clear_object_caps_pt: "dcorres dc \ (invs and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageTableCap w option))) (a, b)) (clear_object_caps w) (mapM_x (swp store_pte ARM_A.pte.InvalidPTE) [w , w + 4 .e. w + 2 ^ pt_bits - 1])" + including no_take_bit apply (clarsimp simp: clear_object_caps_def gets_def) apply (rule dcorres_absorb_get_l) apply (subgoal_tac "\ptx. (ko_at (ArchObj (arch_kernel_obj.PageTable ptx)) w) s'") diff --git a/proof/drefine/Corres_D.thy b/proof/drefine/Corres_D.thy index 74eb017d9..6337600d1 100644 --- a/proof/drefine/Corres_D.thy +++ b/proof/drefine/Corres_D.thy @@ -227,19 +227,20 @@ lemma dcorres_gets_the: apply (simp add:gets_the_def) apply (simp add: gets_def) apply (subst bind_assoc)+ - apply (rule corres_split_keep_pfx - [where r'="\s s'. s = transform s'\ P s \ P' s'" and Q="\x s. x = s" and Q'="\x s. x = s "]) - apply (clarsimp simp: corres_underlying_def get_def) + apply (rule corres_split_keep_pfx[where r'="\s s'. s = transform s'\ P s \ P' s'" + and Q="\x s. x = s" and Q'="\x s. x = s "]) + apply (clarsimp simp: corres_underlying_def get_def) apply (simp add: assert_opt_def) - apply (case_tac "g' xa = None") - apply (clarsimp split:option.splits simp:corres_free_fail) - apply (subgoal_tac "\obj. g x \ None") - apply (clarsimp split:option.splits) - apply (rule_tac Q="(=)(transform xa)" and Q'="(=) xa" in corres_guard_imp) - apply (simp add: A)+ - using B - apply (wp|clarsimp)+ -done + apply (rename_tac x) + apply (case_tac "g' x = None") + apply (clarsimp split:option.splits simp:corres_free_fail) + apply (subgoal_tac "\obj. g (transform x) \ None") + apply (clarsimp split:option.splits) + apply (rule_tac Q="(=) (transform x)" and Q'="(=) x" in corres_guard_imp) + apply (simp add: A)+ + using B + apply (wp|clarsimp)+ + done lemma wpc_helper_dcorres: "dcorres r Q Q' f f' diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index 358881bbc..5fe9a329f 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/proof/drefine/Finalise_DR.thy @@ -866,13 +866,14 @@ lemma mask_pd_bits_less': done lemma mask_pd_bits_less: - "nat (uint ((y::word32) && mask pd_bits >> 2)) < 4096" - apply (clarsimp simp:pd_bits_def pageBits_def) + "unat ((y::word32) && mask pd_bits >> 2) < 4096" + apply (clarsimp simp:pd_bits_def pageBits_def simp del: nat_uint_eq) + apply (unfold unat_def) apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]]) - apply (simp) + apply (simp) using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] apply (clarsimp simp:mask_twice) -done + done lemma mask_pt_bits_less': "uint (((ptr::word32) && mask pt_bits) >> 2)< 256" @@ -882,13 +883,14 @@ lemma mask_pt_bits_less': done lemma mask_pt_bits_less: - "nat (uint ((y::word32) && mask pt_bits >> 2)) < 256" + "unat ((y::word32) && mask pt_bits >> 2) < 256" apply (clarsimp simp:pt_bits_def pageBits_def) + apply (unfold unat_def) apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]]) apply (simp) using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] apply (clarsimp simp:mask_twice) -done + done definition pd_pt_relation :: "word32\word32\word32\'z::state_ext state\bool" where "pd_pt_relation pd pt offset s \ @@ -927,27 +929,21 @@ lemma slot_with_pt_frame_relation: apply (frule(1) page_table_not_idle) apply (clarsimp simp:slots_with_def transform_def transform_objects_def restrict_map_def) apply (clarsimp simp:not_idle_thread_def has_slots_def object_slots_def) - apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def) - apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ) + apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def) apply (clarsimp simp:mask_pt_bits_less split:ARM_A.pte.split_asm) -done + done lemma below_kernel_base: "ucast (y && mask pd_bits >> 2) \ kernel_mapping_slots - \ kernel_pde_mask f (of_nat (unat (y && mask pd_bits >> 2))) + \ kernel_pde_mask f (ucast (y && mask pd_bits >> 2)) = f (of_nat (unat (y && mask pd_bits >> 2)))" - apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) - apply (simp add:ucast_nat_def[symmetric] unat_def) -done + by (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) -(* we need an int version for 2016 *) lemma below_kernel_base_int: "ucast (y && mask pd_bits >> 2) \ kernel_mapping_slots \ kernel_pde_mask f (of_int (uint (y && mask pd_bits >> 2))) = f (of_int (uint (y && mask pd_bits >> 2)))" - apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) - apply (simp add:ucast_nat_def[symmetric] unat_def) -done + by (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) lemma slot_with_pd_pt_relation: "\valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \ kernel_mapping_slots\ \ @@ -960,10 +956,8 @@ lemma slot_with_pd_pt_relation: apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) apply (clarsimp simp:has_slots_def object_slots_def) apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) - apply (clarsimp simp:ucast_def) - apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def below_kernel_base) apply (simp add:mask_pd_bits_less) -done + done lemma slot_with_pd_section_relation: "\valid_idle s; pd_super_section_relation a b y s \ pd_section_relation a b y s; @@ -971,15 +965,14 @@ lemma slot_with_pd_section_relation: (a, unat (y && mask pd_bits >> 2)) \ (slots_with (\x. \rights sz asid. x = cdl_cap.FrameCap False b rights sz Fake asid)) (transform s)" apply (erule disjE) - apply (clarsimp simp :pd_super_section_relation_def) - apply (frule page_directory_at_rev) - apply (frule(1) page_directory_not_idle) - apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) - apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) - apply (clarsimp simp:has_slots_def object_slots_def) - apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) - apply (clarsimp simp:ucast_def) - apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def mask_pd_bits_less) + apply (clarsimp simp :pd_super_section_relation_def) + apply (frule page_directory_at_rev) + apply (frule(1) page_directory_not_idle) + apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) + apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) + apply (clarsimp simp:has_slots_def object_slots_def) + apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) + apply (simp add: mask_pd_bits_less) apply (clarsimp simp :pd_section_relation_def) apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) @@ -987,67 +980,59 @@ lemma slot_with_pd_section_relation: apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) apply (clarsimp simp:has_slots_def object_slots_def) apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) - apply (clarsimp simp:ucast_def) - apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def) apply (simp add:mask_pd_bits_less) -done + done -lemma opt_cap_page_table:"\valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \ kernel_mapping_slots\\ -(opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s)) - = Some (cdl_cap.PageTableCap pt_id Fake None)" - apply (clarsimp simp:pd_pt_relation_def opt_cap_def transform_def unat_def slots_of_def) +lemma opt_cap_page_table: + "\ valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \ kernel_mapping_slots \ + \ opt_cap (a, unat (x && mask pd_bits >> 2)) (transform s) = Some (cdl_cap.PageTableCap pt_id Fake None)" + apply (clarsimp simp :pd_pt_relation_def opt_cap_def transform_def slots_of_def) apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) - apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle - restrict_map_def object_slots_def) - apply (clarsimp simp:transform_page_directory_contents_def unat_def[symmetric] unat_map_def | rule conjI )+ - apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def) - apply (clarsimp simp:below_kernel_base) - apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] unat_def ucast_def) - apply (simp add:mask_pd_bits_less unat_def) -done + apply (clarsimp simp: transform_objects_def not_idle_thread_def page_directory_not_idle + restrict_map_def object_slots_def) + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def | rule conjI )+ + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base) + apply (simp add: mask_pd_bits_less ) + done lemma opt_cap_page:"\valid_idle s;pt_page_relation a pg x S s \\ \f sz. (opt_cap (a, unat (x && mask pt_bits >> 2) ) (transform s)) = Some (cdl_cap.FrameCap False pg f sz Fake None)" - apply (clarsimp simp:pt_page_relation_def unat_def opt_cap_def transform_def slots_of_def) + apply (clarsimp simp: pt_page_relation_def opt_cap_def transform_def slots_of_def) apply (frule page_table_at_rev) apply (frule(1) page_table_not_idle) - apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle - restrict_map_def object_slots_def) - apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI )+ - apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def) - apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def mask_pt_bits_less)+ - apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def) -done + apply (clarsimp simp: transform_objects_def not_idle_thread_def page_directory_not_idle + restrict_map_def object_slots_def) + apply (clarsimp simp: transform_page_table_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI )+ + apply (clarsimp simp: transform_page_table_contents_def unat_map_def transform_pte_def) + apply (simp add: mask_pt_bits_less)+ + apply (clarsimp simp: transform_page_table_contents_def unat_map_def transform_pte_def) + done lemma opt_cap_section: "\valid_idle s;pd_section_relation a pg x s \ pd_super_section_relation a pg x s; ucast (x && mask pd_bits >> 2) \ kernel_mapping_slots\\ \f sz. (opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s)) = Some (cdl_cap.FrameCap False pg f sz Fake None)" - unfolding unat_def apply (erule disjE) - - apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def) - apply (frule page_directory_at_rev) - apply (frule(1) page_directory_not_idle) - apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle - restrict_map_def object_slots_def) - apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ - apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int) - apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+ - apply (simp add:mask_pd_bits_less) - apply (clarsimp simp:pd_super_section_relation_def opt_cap_def transform_def slots_of_def) + apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def) + apply (frule page_directory_at_rev) + apply (frule(1) page_directory_not_idle) + apply (clarsimp simp: transform_objects_def not_idle_thread_def page_directory_not_idle + restrict_map_def object_slots_def) + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base) + apply (simp add: mask_pd_bits_less) + apply (clarsimp simp: pd_super_section_relation_def opt_cap_def transform_def slots_of_def) apply (frule page_directory_at_rev) apply (frule(1) page_directory_not_idle) - apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle - restrict_map_def object_slots_def) - apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ - apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int) - apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+ - apply (simp add:mask_pd_bits_less) -done + apply (clarsimp simp: transform_objects_def not_idle_thread_def page_directory_not_idle + restrict_map_def object_slots_def) + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ + apply (clarsimp simp: transform_page_directory_contents_def unat_map_def transform_pde_def below_kernel_base) + apply (simp add: mask_pd_bits_less) + done lemma opt_object_page_table: "\valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\ @@ -1114,28 +1099,26 @@ lemma dcorres_set_pte_cap: (KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap) (KHeap_A.set_object a (ArchObj (arch_kernel_obj.PageTable (fun(ucast (ptr && mask pt_bits >> 2) := a_pte)))))" - apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def get_object_def gets_the_def gets_def bind_assoc unat_def) + apply (simp add: KHeap_D.set_cap_def KHeap_A.set_object_def get_object_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (rule dcorres_absorb_get_l) - apply (clarsimp simp:obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def) - apply (clarsimp simp:KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def bind_def - corres_underlying_def update_slots_def return_def object_slots_def) + apply (clarsimp simp: obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def) + apply (clarsimp simp: KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def bind_def + corres_underlying_def update_slots_def return_def object_slots_def) apply (rule sym) - apply (clarsimp simp:transform_def transform_current_thread_def) + apply (clarsimp simp: transform_def transform_current_thread_def) apply (rule ext) apply (clarsimp | rule conjI)+ - apply (frule page_table_at_rev) - apply (frule(1) page_table_not_idle) - apply (clarsimp simp:transform_objects_def not_idle_thread_def) - apply (rule ext) - apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def) - apply (clarsimp simp:word_of_int word_of_nat mask_pt_bits_less mask_pt_bits_less' ucast_def) - apply (subst (asm) word_of_int_inj) - apply (clarsimp simp:mask_pt_bits_less')+ - apply (clarsimp simp:uint_nat) - apply clarify + apply (frule page_table_at_rev) + apply (frule(1) page_table_not_idle) + apply (clarsimp simp: transform_objects_def not_idle_thread_def) + apply (rule ext) + apply (clarsimp simp: transform_page_table_contents_def transform_pte_def unat_map_def) + apply (clarsimp simp: mask_pt_bits_less mask_pt_bits_less') + apply (simp only: ucast_nat_def[symmetric]) + apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less) apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) -done + done lemma dcorres_delete_cap_simple_set_pt: "dcorres dc \ ((\s. mdb_cte_at (swp (cte_wp_at ((\) cap.NullCap)) s) (cdt s)) @@ -1163,44 +1146,39 @@ lemma dcorres_delete_cap_simple_set_pt: lemma transform_page_table_contents_upd: "transform_page_table_contents fun(unat (y && mask pt_bits >> 2) \ transform_pte pte) = - transform_page_table_contents - (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))" + transform_page_table_contents (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))" apply (rule ext) - apply (clarsimp simp:transform_page_table_contents_def unat_map_def ) - apply (clarsimp simp:ucast_nat_def[symmetric]) + apply (clarsimp simp: transform_page_table_contents_def unat_map_def) apply (subgoal_tac "unat (y && mask pt_bits >> 2) < 256") - apply (rule conjI|clarsimp)+ - apply (drule word_unat.Abs_eqD) - apply (simp add: unats_def)+ + apply (rule conjI|clarsimp)+ + apply (simp only: ucast_nat_def[symmetric]) + apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less) + apply simp apply (rule unat_less_helper) apply (subst shiftr_div_2n_w) apply (clarsimp simp:word_size)+ apply (rule word_div_mult,simp) apply (clarsimp simp:pt_bits_def pageBits_def) apply (rule and_mask_less_size[where n = 10,simplified],simp add:word_size) -done + done lemma transform_page_directory_contents_upd: "ucast ((ptr::word32) && mask pd_bits >> 2) \ kernel_mapping_slots \ transform_page_directory_contents f(unat (ptr && mask pd_bits >> 2) \ transform_pde a_pde) = transform_page_directory_contents (f(ucast (ptr && mask pd_bits >> 2) := a_pde))" apply (rule ext) - apply (simp (no_asm) add:transform_page_directory_contents_def unat_map_def) - apply (simp add:below_kernel_base) - apply (clarsimp simp: unat_def mask_pd_bits_less|rule conjI)+ - apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def) - apply (clarsimp simp:ucast_nat_def[symmetric]) - apply (drule sym) - apply (drule word_unat.Abs_eqD) - apply (simp add:unats_def unat_def[symmetric])+ - apply (rule unat_less_helper) - apply (subst shiftr_div_2n_w,(simp add:word_size)+) - apply (rule word_div_mult,simp) - apply (clarsimp simp:pt_bits_def pd_bits_def pageBits_def) - apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size) - apply (simp add:word_of_int unat_def) - apply (clarsimp simp:ucast_def word_of_int_nat[OF uint_ge_0,simplified]) -done + apply (simp (no_asm) add: transform_page_directory_contents_def unat_map_def) + apply (simp add: below_kernel_base) + apply (clarsimp simp: mask_pd_bits_less | rule conjI)+ + apply (clarsimp simp: kernel_pde_mask_def kernel_mapping_slots_def) + apply (simp only: ucast_nat_def[symmetric]) + apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less) + apply (rule unat_less_helper) + apply (subst shiftr_div_2n_w; simp add:word_size) + apply (rule word_div_mult, simp) + apply (clarsimp simp: pt_bits_def pd_bits_def pageBits_def) + apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size) + done lemma dcorres_set_pde_cap: "\ (x::word32) = (ptr && mask pd_bits >> 2);pde_cap = transform_pde a_pde; ucast (ptr && mask pd_bits >> 2) \ kernel_mapping_slots\\ @@ -1214,15 +1192,15 @@ lemma dcorres_set_pde_cap: apply (clarsimp simp: KHeap_D.set_object_def get_object_def in_monad simpler_modify_def put_def bind_def corres_underlying_def update_slots_def object_slots_def return_def) apply (clarsimp simp: transform_def transform_current_thread_def) - apply (rule ext) - apply (clarsimp | rule conjI)+ - apply (frule page_directory_at_rev) - apply (frule(1) page_directory_not_idle) - apply (clarsimp simp: transform_objects_def not_idle_thread_def) - apply (rule sym) - apply (erule transform_page_directory_contents_upd) - apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) -done + apply (rule ext) + apply (clarsimp | rule conjI)+ + apply (frule page_directory_at_rev) + apply (frule(1) page_directory_not_idle) + apply (clarsimp simp: transform_objects_def not_idle_thread_def) + apply (rule sym) + apply (erule transform_page_directory_contents_upd) + apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) + done lemma dcorres_delete_cap_simple_set_pde: " ucast (ptr && mask pd_bits >> 2) \ kernel_mapping_slots @@ -1359,13 +1337,9 @@ lemma shiftl_inj_if: done lemma ucast_inj_mask: - "((ucast (x::'a::len word)) :: ('b::len word)) = ((ucast (y::'a::len word)) :: ('b::len word)) - \ (x && mask (len_of TYPE('b))) = (y && mask (len_of TYPE('b)))" - apply (simp add:ucast_def) - apply (simp add:word_ubin.inverse_norm) - apply (simp add:word_ubin.eq_norm) - apply (simp add:and_mask_bintr) -done + "(ucast (x::'a::len word) :: 'b::len word) = (ucast (y::'a::len word) :: 'b::len word) + \ x && mask LENGTH('b) = y && mask LENGTH('b)" + by (metis ucast_ucast_mask) lemma split_word_noteq_on_mask: "(x \ y) = (x && mask k \ y && mask k \ x && ~~ mask k \ y && ~~ mask k)" @@ -2356,138 +2330,135 @@ lemma dcorres_unmap_page: apply (rule dcorres_expand_pfx) apply (clarsimp simp:valid_cap_def) apply (case_tac vmpage_size) -\ \ARMSmallPage\ - apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton - PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) - apply (rule corres_guard_imp) - apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" - in corres_split_catch [where f = dc and E = dc and E' =dc]) - apply simp - apply (rule corres_guard_imp) - apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) - apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib - pageBitsForSize_def bindE_assoc mapM_x_singleton) - apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) - apply (rule corres_splitEE[OF _ dcorres_might_throw]) - apply (rule corres_dummy_returnOk_l) - apply (rule corres_splitEE) -prefer 2 - apply (simp add:transform_pt_slot_ref_def) - apply (rule dcorres_store_invalid_pte[where pg_id = pg]) - apply (simp add:liftE_distrib[symmetric] returnOk_liftE) - apply (rule dcorres_symb_exec_r) - apply (rule dcorres_flush_page) - apply (wp do_machine_op_wp | clarsimp)+ - apply (simp add: imp_conjR) - apply ((wp check_mapping_pptr_pt_relation | wp (once) hoare_drop_imps)+)[1] - apply (simp | wp lookup_pt_slot_inv)+ - apply (simp add: dc_def - | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help - | rule conjI | clarify)+ + \ \ARMSmallPage\ + apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton + PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) + apply (rule corres_guard_imp) + apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" + in corres_split_catch [where f = dc and E = dc and E' =dc]) + apply simp + apply (rule corres_guard_imp) + apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) + apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib + pageBitsForSize_def bindE_assoc mapM_x_singleton) + apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) + apply (rule corres_splitEE[OF _ dcorres_might_throw]) + apply (rule corres_dummy_returnOk_l) + apply (rule corres_splitEE) + prefer 2 + apply (simp add:transform_pt_slot_ref_def) + apply (rule dcorres_store_invalid_pte[where pg_id = pg]) + apply (simp add:liftE_distrib[symmetric] returnOk_liftE) + apply (rule dcorres_symb_exec_r) + apply (rule dcorres_flush_page) + apply (wp do_machine_op_wp | clarsimp)+ + apply (simp add: imp_conjR) + apply ((wp check_mapping_pptr_pt_relation | wp (once) hoare_drop_imps)+)[1] + apply (simp | wp lookup_pt_slot_inv)+ + apply (simp add: dc_def + | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help + | rule conjI | clarify)+ -\ \ARMLargePage\ + \ \ARMLargePage\ - apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton - PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) - apply (rule corres_guard_imp) - apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" - in corres_split_catch [where f = dc and E = dc and E' =dc]) - apply simp - apply (rule corres_guard_imp) - apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) - apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib - pageBitsForSize_def bindE_assoc mapM_x_singleton) - apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) - apply (rule corres_splitEE[OF _ dcorres_might_throw]) - apply (rule dcorres_symb_exec_rE) - apply (rule corres_dummy_returnOk_l) - apply (rule corres_splitEE) -prefer 2 - apply simp - apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2) - apply (erule dcorres_unmap_large_page[where pg_id = pg]) - apply (simp add:liftE_distrib[symmetric] returnOk_liftE) - apply (rule dcorres_symb_exec_r) - apply (rule dcorres_flush_page[unfolded dc_def]) - apply (wp do_machine_op_wp | clarsimp)+ - apply (simp add: imp_conjR is_aligned_mask) - apply (rule hoare_vcg_conj_lift) - apply (wp hoare_drop_imps)[1] - apply (rule hoare_vcg_conj_lift) - apply (wp hoare_drop_imps)[1] - apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation]) - apply fastforce - apply (simp | wp lookup_pt_slot_inv)+ + apply (simp add: ARM_A.unmap_page_def bindE_assoc mapM_x_singleton + PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) + apply (rule corres_guard_imp) + apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" + in corres_split_catch [where f = dc and E = dc and E' =dc]) + apply simp + apply (rule corres_guard_imp) + apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) + apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib + pageBitsForSize_def bindE_assoc mapM_x_singleton) + apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) + apply (rule corres_splitEE[OF _ dcorres_might_throw]) + apply (rule dcorres_symb_exec_rE) + apply (rule corres_dummy_returnOk_l) + apply (rule corres_splitEE) + prefer 2 + apply simp + apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2) + apply (erule dcorres_unmap_large_page[where pg_id = pg]) + apply (simp add:liftE_distrib[symmetric] returnOk_liftE) + apply (rule dcorres_symb_exec_r) + apply (rule dcorres_flush_page[unfolded dc_def]) + apply (wp do_machine_op_wp | clarsimp)+ + apply (simp add: imp_conjR is_aligned_mask) + apply (rule hoare_vcg_conj_lift) + apply (wp hoare_drop_imps)[1] + apply (rule hoare_vcg_conj_lift) + apply (wp hoare_drop_imps)[1] + apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation]) + apply fastforce + apply (simp | wp lookup_pt_slot_inv)+ apply (simp add: dc_def - | wp lookup_pt_slot_inv hoare_drop_imps - find_pd_for_asid_kernel_mapping_help - | safe)+ + | wp lookup_pt_slot_inv hoare_drop_imps find_pd_for_asid_kernel_mapping_help + | safe)+ -\ \Section\ - apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton - PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) - apply (rule corres_guard_imp) - apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" - in corres_split_catch [where f = dc and E = dc and E' =dc]) - apply simp - apply (rule corres_guard_imp) - apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) - apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib - pageBitsForSize_def bindE_assoc mapM_x_singleton) - apply (rule corres_splitEE[OF _ dcorres_might_throw]) - apply (rule corres_dummy_returnOk_l) - apply (rule corres_splitEE) -prefer 2 - apply simp - apply (rule dcorres_delete_cap_simple_section[where oid = pg]) - apply (simp add:liftE_distrib[symmetric] returnOk_liftE) - apply (rule dcorres_symb_exec_r) - apply (rule dcorres_flush_page[unfolded dc_def]) - apply (wp do_machine_op_wp | clarsimp)+ - apply (simp add: imp_conjR) - apply ((wp check_mapping_pptr_section_relation | wp (once) hoare_drop_imps)+)[1] - apply (simp | wp lookup_pt_slot_inv)+ - apply (simp add: dc_def - | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help - | safe)+ - -\ \SuperSection\ - - apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton - PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) - apply (rule corres_guard_imp) - apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" - in corres_split_catch [where f = dc and E = dc and E' =dc]) - apply simp - apply (rule corres_guard_imp) - apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) - apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib - pageBitsForSize_def bindE_assoc mapM_x_singleton) + \ \Section\ + apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton + PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) + apply (rule corres_guard_imp) + apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" + in corres_split_catch [where f = dc and E = dc and E' =dc]) + apply simp + apply (rule corres_guard_imp) + apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) + apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib + pageBitsForSize_def bindE_assoc mapM_x_singleton) apply (rule corres_splitEE[OF _ dcorres_might_throw]) - apply (rule dcorres_symb_exec_rE) - apply (rule corres_dummy_returnOk_l) - apply (rule corres_splitEE) -prefer 2 - apply simp - apply (rule_tac F = "is_aligned pda 14" in corres_gen_asm2) - apply (erule(2) dcorres_unmap_large_section[where pg_id = pg]) - apply (simp add:liftE_distrib[symmetric] returnOk_liftE) - apply (rule dcorres_symb_exec_r) - apply (rule dcorres_flush_page[unfolded dc_def]) - apply (wp do_machine_op_wp | clarsimp)+ - apply (simp add: imp_conjR is_aligned_mask) - apply (rule hoare_vcg_conj_lift) - apply (wp hoare_drop_imps)[1] - apply (rule hoare_vcg_conj_lift) - apply (wp hoare_drop_imps)[1] - apply (rule hoare_vcg_conj_lift) - apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation]) - apply clarsimp + apply (rule corres_dummy_returnOk_l) + apply (rule corres_splitEE) + prefer 2 + apply simp + apply (rule dcorres_delete_cap_simple_section[where oid = pg]) + apply (simp add:liftE_distrib[symmetric] returnOk_liftE) + apply (rule dcorres_symb_exec_r) + apply (rule dcorres_flush_page[unfolded dc_def]) + apply (wp do_machine_op_wp | clarsimp)+ + apply (simp add: imp_conjR) + apply ((wp check_mapping_pptr_section_relation | wp (once) hoare_drop_imps)+)[1] + apply (simp | wp lookup_pt_slot_inv)+ + apply (simp add: dc_def + | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help + | safe)+ + + \ \SuperSection\ + apply (simp add: ARM_A.unmap_page_def bindE_assoc mapM_x_singleton + PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) + apply (rule corres_guard_imp) + apply (rule_tac P = "\x. x = transform s'" and P' = "(=) s'" + in corres_split_catch [where f = dc and E = dc and E' =dc]) + apply simp + apply (rule corres_guard_imp) + apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) + apply (simp_all add: cdl_page_mapping_entries_def liftE_distrib + pageBitsForSize_def bindE_assoc mapM_x_singleton) + apply (rule corres_splitEE[OF _ dcorres_might_throw]) + apply (rule dcorres_symb_exec_rE) + apply (rule corres_dummy_returnOk_l) + apply (rule corres_splitEE) + prefer 2 + apply simp + apply (rule_tac F = "is_aligned pd 14" in corres_gen_asm2) + apply (erule(2) dcorres_unmap_large_section[where pg_id = pg]) + apply (simp add:liftE_distrib[symmetric] returnOk_liftE) + apply (rule dcorres_symb_exec_r) + apply (rule dcorres_flush_page[unfolded dc_def]) + apply (wp do_machine_op_wp | clarsimp)+ + apply (simp add: imp_conjR is_aligned_mask) + apply (rule hoare_vcg_conj_lift) + apply (wp hoare_drop_imps)[1] + apply (rule hoare_vcg_conj_lift) + apply (wp hoare_drop_imps)[1] + apply (rule hoare_vcg_conj_lift) + apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation]) + apply clarsimp apply (simp add:is_aligned_mask[symmetric] dc_def - | wp lookup_pt_slot_inv hoare_drop_imps - find_pd_for_asid_kernel_mapping_help - | safe)+ -done + | wp lookup_pt_slot_inv hoare_drop_imps find_pd_for_asid_kernel_mapping_help + | safe)+ + done lemma dcorres_delete_asid_none: diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy index 1b6d9d54c..844235967 100644 --- a/proof/drefine/Intent_DR.thy +++ b/proof/drefine/Intent_DR.thy @@ -59,15 +59,14 @@ lemma tcb_cap_casesE: lemma tcb_cnode_index_def2: "n < 8 \ tcb_cnode_index n = bin_to_bl 3 (int n)" unfolding tcb_cnode_index_def to_bl_def + including no_take_bit by (simp add: uint_nat unat_of_nat) lemma bl_to_bin_tcb_cnode_index: "n < 8 \ nat (bl_to_bin (tcb_cnode_index n)) = n" unfolding tcb_cnode_index_def - apply simp - apply (fold unat_def) - apply (simp add: unat_of_nat) - done + including no_take_bit + by (simp add: unat_of_nat) (* LIFT LEMMAS: Lift the property from abstract spec to capdl model diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy index 13ccb7741..5ea803da2 100644 --- a/proof/drefine/Ipc_DR.thy +++ b/proof/drefine/Ipc_DR.thy @@ -1089,17 +1089,16 @@ lemma evalMonad_get_extra_cptrs: done lemma dcorres_symb_exec_r_evalMonad: -assumes wp:"\sa. \(=) sa\ f \\r. (=) sa\" -assumes corres:"\rv. evalMonad f s = Some rv \ dcorres r P ((=) s) h (g rv)" -shows "\empty_when_fail f;weak_det_spec ((=) s) f\ \ dcorres r P ((=) s) h (f>>=g)" + assumes wp:"\sa. \(=) sa\ f \\r. (=) sa\" + assumes corres:"\rv. evalMonad f s = Some rv \ dcorres r P ((=) s) h (g rv)" + shows "\ empty_when_fail f; weak_det_spec ((=) s) f \ \ dcorres r P ((=) s) h (f>>=g)" apply (rule_tac Q'="\r. (=) s and K_bind (evalMonad f s = Some r)" in corres_symb_exec_r) - apply (rule dcorres_expand_pfx) - using corres - apply (clarsimp simp:corres_underlying_def) - apply fastforce - apply (wp wp,simp,rule evalMonad_wp) - apply (simp add:wp)+ -done + apply (rule dcorres_expand_pfx) + using corres + apply (clarsimp simp:corres_underlying_def) + apply (wp wp, simp, rule evalMonad_wp) + apply (simp add:wp)+ + done lemma dcorres_store_word_offs_spec: "\within_page buf (base + of_nat (x * word_size)) sz\ \ @@ -1477,19 +1476,19 @@ lemma get_ipc_buffer_words_receive_slots: in is_aligned_weaken[OF is_aligned_after_mask]) apply (case_tac sz,simp_all add:msg_align_bits) apply (simp add:mask_add_aligned) - apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms) + apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric]) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_loadWord weak_det_spec_loadWord)+ using loadWord_functional[unfolded functional_def,simplified] apply fastforce apply (simp add:evalMonad_loadWord word_size_def mask_add_aligned) - apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms) + apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric]) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_loadWord weak_det_spec_loadWord)+ using loadWord_functional[unfolded functional_def,simplified] apply fastforce apply (simp add:evalMonad_loadWord word_size_def mask_add_aligned) - apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric] word_of_int_hom_syms) + apply (simp add:word_mod_2p_is_mask[where n = 2,symmetric]) done (* FIXME: MOVE *) @@ -1705,54 +1704,51 @@ lemma dcorres_lookup_extra_caps: (Ipc_A.lookup_extra_caps thread buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))" apply (clarsimp simp:lookup_extra_caps_def liftE_bindE Endpoint_D.lookup_extra_caps_def) apply (rule corres_symb_exec_r) - apply (rule_tac F = "evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv" - in corres_gen_asm2) - apply (rule corres_mapME[where S = "{(x,y). x = of_bl y \ length y = word_bits}"]) - prefer 3 + apply (rule_tac F = "evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv" + in corres_gen_asm2) + apply (rule corres_mapME[where S = "{(x,y). x = of_bl y \ length y = word_bits}"]) + prefer 3 apply simp - apply (erule conjE) - apply (drule_tac t="of_bl y" in sym, simp) - apply (rule dcorres_lookup_cap_and_slot[simplified]) - apply (clarsimp simp:transform_cap_list_def)+ - apply wp - apply simp - apply (case_tac buffer) - apply clarsimp - apply (simp add:transform_full_intent_def Let_def) - apply (rule get_ipc_buffer_words_empty) - apply (simp add:obj_at_def) - apply (erule get_tcb_SomeD) - apply simp + apply (rule dcorres_lookup_cap_and_slot[simplified]) + apply (clarsimp simp:transform_cap_list_def)+ + apply wp + apply simp + apply (case_tac buffer) + apply clarsimp + apply (simp add:transform_full_intent_def Let_def) + apply (rule get_ipc_buffer_words_empty) + apply (simp add:obj_at_def) + apply (erule get_tcb_SomeD) + apply simp apply clarify apply (subst evalMonad_get_extra_cptrs) - apply simp+ - apply (case_tac buffer) + apply simp+ + apply (case_tac buffer) apply clarsimp - apply clarify - apply (drule evalMonad_get_extra_cptrs) - apply (simp del:get_extra_cptrs.simps - add: zip_map_eqv[where g = "\x. x",simplified])+ - apply (simp add: word_bits_def del:get_extra_cptrs.simps) - apply (wp evalMonad_wp) - apply (case_tac buffer) - apply (simp add:get_extra_cptrs_def empty_when_fail_simps)+ - apply (simp add:liftM_def) - apply (rule empty_when_fail_compose) - apply (simp add:empty_when_fail_simps)+ - apply (rule empty_when_fail_mapM) - apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs) - apply (rule weak_det_spec_mapM) - apply (simp add:weak_det_spec_load_word_offs) - apply (case_tac buffer) - apply (simp add:get_extra_cptrs_def weak_det_spec_simps)+ + apply clarify + apply (drule evalMonad_get_extra_cptrs) + apply (simp del:get_extra_cptrs.simps add: zip_map_eqv[where g = "\x. x",simplified])+ + apply (simp add: word_bits_def del:get_extra_cptrs.simps) + apply (wp evalMonad_wp) + apply (case_tac buffer) + apply (simp add:get_extra_cptrs_def empty_when_fail_simps)+ + apply (simp add:liftM_def) + apply (rule empty_when_fail_compose) + apply (simp add:empty_when_fail_simps)+ + apply (rule empty_when_fail_mapM) + apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs) + apply (rule weak_det_spec_mapM) + apply (simp add:weak_det_spec_load_word_offs) + apply (case_tac buffer) + apply (simp add:get_extra_cptrs_def weak_det_spec_simps)+ apply (simp add:liftM_def) apply (rule weak_det_spec_compose) - apply (simp add:weak_det_spec_simps) + apply (simp add:weak_det_spec_simps) apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) - apply (clarsimp simp:valid_state_def valid_pspace_def cur_tcb_def)+ - apply (wp|clarsimp)+ -done + apply (clarsimp simp:valid_state_def valid_pspace_def cur_tcb_def)+ + apply (wp|clarsimp)+ + done lemma dcorres_copy_mrs': notes hoare_post_taut[wp] if_cong[cong] @@ -2680,7 +2676,7 @@ lemma send_sync_ipc_corres: apply (rename_tac list) apply (drule_tac s = "set list" in sym) apply (clarsimp simp: bind_assoc neq_Nil_conv split del:if_split) - apply (rule_tac P1="\" and P'="(=) s'a" and x1 = y + apply (rule_tac P1="\" and P'="(=) s'" and x1 = y in dcorres_absorb_pfx[OF select_pick_corres[OF dcorres_expand_pfx]]) defer apply (simp+)[3] diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy index 8c13fc3ab..309698b97 100644 --- a/proof/drefine/KHeap_DR.thy +++ b/proof/drefine/KHeap_DR.thy @@ -270,6 +270,7 @@ lemma nat_to_bl_dest: lemma bl_to_bin_tcb_cnode_index_le0: "n < 8 \ (bl_to_bin (tcb_cnode_index n) \ 0) = (n = 0)" + including no_take_bit by (simp add: tcb_cnode_index_def uint_nat unat_of_nat) lemma nat_bl_to_bin_lt2p: "nat(bl_to_bin b) < 2 ^ length b" @@ -3095,7 +3096,7 @@ lemma branch_map_simp2: apply (drule min.absorb2[where b = nata]) apply simp apply (clarsimp simp: add.commute) - apply (simp add:unat_def) + apply (simp only: unat_def) apply (rule iffD2[OF eq_nat_nat_iff]) apply (simp add:bl_to_bin_ge0 )+ apply (subst bl_to_bin_rep_F[symmetric]) @@ -3177,8 +3178,9 @@ lemma resolve_address_bits_terminate_corres: apply clarsimp apply (rule_tac Q="\x y. y = (transform s) \ x = (transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun))" in corres_symb_exec_l) apply (rule dcorres_expand_pfx) - apply (simp add: unat_def split: nat.splits) + apply (simp split: nat.splits) apply (clarsimp simp: returnOk_def return_def corres_underlying_def transform_cslot_ptr_def) + apply (simp only: unat_def) apply (subst eq_nat_nat_iff) apply (simp add:bl_to_bin_ge0)+ apply (subst to_bl_bin[symmetric]) @@ -3287,7 +3289,7 @@ proof (induct n arbitrary: cref cap' cap) apply (rule dcorres_expand_pfx) apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) - apply (rename_tac word list nat "fun") + apply (rename_tac word nat list "fun") apply (rule corres_guard_imp) apply (rule_tac radix_bits = nat and guard = list and s = s' in resolve_address_bits_error_corres[where ref="[]",simplified]) apply ((simp add:transform_cap_def in_terminate_branch_def in_recursive_branch_def valid_cap_def obj_at_def is_cap_table_def)+)[10] @@ -3313,7 +3315,7 @@ next apply (case_tac "\ in_recursive_branch cref cap'") apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits) apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits) - apply (rename_tac word list nat "fun") + apply (rename_tac word nat list "fun") apply (rule corres_guard_imp) apply (rule_tac s=s' and radix_bits = nat and guard = list in resolve_address_bits_error_corres) apply (simp_all | rule conjI)+ @@ -3323,7 +3325,7 @@ next apply (subst KHeap_DR.resolve_address_bits.simps,subst resolve_address_bits_recursive_branch) apply (clarsimp simp:cap_type_simps is_cap_simps)+ apply fastforce - apply (rename_tac word list nat "fun") + apply (rename_tac word nat list "fun") apply (simp add:cap_type_simps) apply (simp add:in_recursive_branch_def in_terminate_branch_def unlessE_def branch_map_simp1) apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE) diff --git a/proof/drefine/Schedule_DR.thy b/proof/drefine/Schedule_DR.thy index 717f3c68a..4943db5e5 100644 --- a/proof/drefine/Schedule_DR.thy +++ b/proof/drefine/Schedule_DR.thy @@ -404,7 +404,6 @@ lemma schedule_choose_new_thread_dcorres: apply (wp hoare_drop_imp| simp | clarsimp simp: valid_sched_def)+ apply (frule max_set_not_empty, fastforce) apply (wp hoare_drop_imp| simp)+ - apply (clarsimp simp: valid_sched_def) (* dom_t = 0 *) apply (simp only: schedule_def_2) apply (rule corres_guard_imp) diff --git a/proof/drefine/StateTranslation_D.thy b/proof/drefine/StateTranslation_D.thy index 5780e182d..24e957f0e 100644 --- a/proof/drefine/StateTranslation_D.thy +++ b/proof/drefine/StateTranslation_D.thy @@ -453,7 +453,8 @@ lemma transform_intent_isnot_UntypedIntent: apply(unfold transform_intent_untyped_retype_def) apply (clarsimp split: list.split, safe, simp_all)[1] apply (clarsimp simp: transform_type_def) - apply (simp add: linorder_not_less eval_nat_numeral le_Suc_eq unat_arith_simps) + apply (simp add: unat_arith_simps) + apply (simp add: eval_nat_numeral linorder_not_less le_Suc_eq) apply(erule disjE) apply(auto simp: transform_intent_def option_map_def split: gen_invocation_labels.split invocation_label.split arch_invocation_label.split @@ -663,9 +664,7 @@ where Some $ bin_to_bl bits (of_nat n)" lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)" - apply (clarsimp simp: nat_to_bl_def to_bl_def) - apply (auto simp: uint_nat le_def word_size) - done + by (clarsimp simp: nat_to_bl_def to_bl_def le_def word_size) (* FIXME: MOVE *) definition diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index cd1978a02..5c0f6287e 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -1393,6 +1393,7 @@ lemma handle_recv_corres: apply (rule corres_guard_imp) apply (rule corres_split_deprecated[OF _ get_cur_thread_corres]) apply (simp add:liftM_def select_f_get_register get_thread_def bind_assoc) + apply (rename_tac thread) apply (rule_tac P=\ and P'="invs and valid_etcbs and (\s. thread = cur_thread s \ not_idle_thread thread s \ st_tcb_at active thread s)" in dcorres_gets_the) @@ -1485,6 +1486,7 @@ lemma handle_reply_corres: apply (rule corres_guard_imp) apply (rule corres_split_deprecated [OF _ get_cur_thread_corres]) apply simp + apply (rename_tac thread) apply (rule_tac R="\_. \" and R'="\cap. invs and valid_etcbs and ct_running and tcb_at thread and not_idle_thread thread diff --git a/proof/drefine/Untyped_DR.thy b/proof/drefine/Untyped_DR.thy index a56f54270..9554ae7d6 100644 --- a/proof/drefine/Untyped_DR.thy +++ b/proof/drefine/Untyped_DR.thy @@ -668,7 +668,7 @@ lemma clearMemory_unused_corres_noop: apply (simp add: within_page_def) apply simp apply (clarsimp simp: obj_at_def) - apply (subgoal_tac "y && ~~ mask (obj_bits_api ty us) = p") + apply (subgoal_tac "x && ~~ mask (obj_bits_api ty us) = p") apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter split: cap.split_asm arch_cap.split_asm) apply (cut_tac t="(t, tcb_cnode_index 4)" and P="(=) cap" for t cap @@ -943,7 +943,7 @@ lemma retype_transform_ref_subseteq_strong: apply (clarsimp simp:range_cover_def) apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2]) apply (simp add:range_cover_def)+ - done + by (metis is_aligned_add is_aligned_mult_triv2 is_aligned_no_overflow_mask mask_2pm1) qed lemma generate_object_ids_exec: @@ -1271,6 +1271,7 @@ lemma reset_untyped_cap_corres: and (\s. descendants_of cref (cdt s) = {})) (Untyped_D.reset_untyped_cap (transform_cslot_ptr cref)) (Retype_A.reset_untyped_cap cref)" + including no_take_bit supply if_cong[cong] apply (rule dcorres_expand_pfx) apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) @@ -1284,7 +1285,8 @@ lemma reset_untyped_cap_corres: apply (simp add: whenE_def if_flip split del: if_split) apply (rule corres_if) apply (clarsimp simp: is_cap_simps free_range_of_untyped_def - cap_aligned_def free_index_of_def) + cap_aligned_def free_index_of_def + simp del: word_of_nat_eq_0_iff) apply (simp add: word_unat.Rep_inject[symmetric]) apply (subst unat_of_nat_eq, erule order_le_less_trans, rule power_strict_increasing, simp_all add: word_bits_def bits_of_def)[1] @@ -1634,6 +1636,7 @@ lemma corres_whenE_throwError_split_rhs: \ (\ G \ corres_underlying sr nf nf' r P Q a b))" by (simp add: whenE_bindE_throwError_to_if) + lemma nat_bl_to_bin_nat_to_cref: assumes asms: "x < 2 ^ bits" "bits < word_bits" shows "nat (bl_to_bin (nat_to_cref bits x)) = x" @@ -1651,11 +1654,8 @@ proof - apply (insert asms word_bits_conv, simp) done show ?thesis using of_bl lt_bl lt_x - apply (simp add: of_bl_def word_of_nat) - apply (drule word_uint.Abs_eqD) - apply (simp add: uints_num bl_to_bin_ge0) - apply (simp add: uints_num) - apply simp + apply (simp add: of_bl_def) + apply (erule word_of_int_word_of_nat_eqD; simp add: bl_to_bin_ge0) done qed @@ -1717,7 +1717,7 @@ lemma descendants_of_empty_lift : done lemma alignUp_gt_0: - "\is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \ 0 ; a \ x\ \ (0 < Word_Lib.alignUp a n) = (a \ 0)" + "\is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \ 0 ; a \ x\ \ (0 < alignUp a n) = (a \ 0)" apply (rule iffI) apply (rule ccontr) apply (clarsimp simp:not_less alignUp_def2 mask_def) @@ -1833,10 +1833,10 @@ lemma decode_untyped_corres: apply (rule corres_guard_imp) apply (rule_tac F="cap_aligned cnode_cap' \ is_cnode_cap cnode_cap'" in corres_gen_asm2) apply (subgoal_tac "map (Pair (cap_object (transform_cap cnode_cap'))) - [unat w4 ..< unat w4 + unat w5] + [unat w3 ..< unat w3 + unat w4] = map (\x. transform_cslot_ptr (obj_ref_of (cnode_cap'), (nat_to_cref (bits_of cnode_cap') x))) - [unat w4 ..< unat w4 + unat w5]") + [unat w3 ..< unat w3 + unat w4]") apply (simp del: map_eq_conv) apply (simp add: mapME_x_map_simp) apply (rule mapME_x_corres_inv)