From 3e1c0fb99492ee9cc13d5ba9a5a891416d74e483 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 10 Jan 2025 19:36:42 +1100 Subject: [PATCH] arm-hyp crefine: minimal fixups for arch-split up to InvariantUpdates_H Most of the changes were ported from ARM (which were adapted from AARCH64). Signed-off-by: Rafal Kolanski --- proof/crefine/ARM_HYP/ADT_C.thy | 5 +-- proof/crefine/ARM_HYP/ArchMove_C.thy | 14 ++++---- proof/crefine/ARM_HYP/Detype_C.thy | 17 +++++----- proof/crefine/ARM_HYP/Fastpath_C.thy | 12 +++---- proof/crefine/ARM_HYP/Fastpath_Equiv.thy | 4 +-- proof/crefine/ARM_HYP/Finalise_C.thy | 6 ++-- proof/crefine/ARM_HYP/Ipc_C.thy | 12 +++---- .../crefine/ARM_HYP/IsolatedThreadAction.thy | 4 +-- proof/crefine/ARM_HYP/Recycle_C.thy | 4 +-- proof/crefine/ARM_HYP/Refine_C.thy | 2 +- proof/crefine/ARM_HYP/Retype_C.thy | 32 ++++++++++++------- proof/crefine/ARM_HYP/SR_lemmas_C.thy | 4 +-- proof/crefine/ARM_HYP/Schedule_C.thy | 2 +- proof/crefine/ARM_HYP/Syscall_C.thy | 2 +- proof/crefine/ARM_HYP/Tcb_C.thy | 13 +++++++- 15 files changed, 78 insertions(+), 55 deletions(-) diff --git a/proof/crefine/ARM_HYP/ADT_C.thy b/proof/crefine/ARM_HYP/ADT_C.thy index 0ca2bcd27d..6b22b11b82 100644 --- a/proof/crefine/ARM_HYP/ADT_C.thy +++ b/proof/crefine/ARM_HYP/ADT_C.thy @@ -111,7 +111,7 @@ lemma setTCBContext_C_corres: apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def carch_state_relation_def cmachine_state_relation_def typ_heap_simps' update_tcb_map_tos) - apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def + apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def tcb_cte_cases_neqs cvariable_relation_upd_const ko_at_projectKO_opt) apply (simp add: cep_relations_drop_fun_upd) apply (drule ko_at_projectKO_opt) @@ -780,6 +780,7 @@ lemma map_to_ctes_tcb_ctes: "ctes_of s' = ctes_of s \ ko_at' tcb p s \ ko_at' tcb' p s' \ \x\ran tcb_cte_cases. fst x tcb' = fst x tcb" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (clarsimp simp add: ran_tcb_cte_cases) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb split: kernel_object.splits) @@ -1366,7 +1367,7 @@ lemma ksPSpace_eq_imp_typ_at'_eq: lemma ksPSpace_eq_imp_valid_cap'_eq: assumes ksPSpace: "ksPSpace s' = ksPSpace s" shows "valid_cap' c s' = valid_cap' c s" - by (auto simp: valid_cap'_def page_table_at'_def page_directory_at'_def + by (auto simp: valid_cap'_def valid_arch_cap'_def page_table_at'_def page_directory_at'_def valid_untyped'_def ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace] ksPSpace_eq_imp_typ_at'_eq[OF ksPSpace] diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy index 31054c9437..33ca0fbc8a 100644 --- a/proof/crefine/ARM_HYP/ArchMove_C.thy +++ b/proof/crefine/ARM_HYP/ArchMove_C.thy @@ -28,6 +28,8 @@ lemma vaddr_segment_nonsense6: apply (rule shiftr_less_t2n'[where m=11 and n=21 and 'a=machine_word_len, simplified]) done +context begin interpretation Arch . + (* Short-hand for unfolding cumbersome machine constants *) (* FIXME MOVE these should be in refine, and the _eq forms should NOT be declared [simp]! *) (* FIXME YUCK where did you come from *) @@ -119,8 +121,6 @@ lemma addToBitmap_sets_L1Bitmap_same_dom: apply wpsimp by (metis nth_0 prioToL1Index_bit_set word_or_zero) -context begin interpretation Arch . - lemma setCTE_asidpool': "\ ko_at' (ASIDPool pool) p \ setCTE c p' \\_. ko_at' (ASIDPool pool) p\" apply (clarsimp simp: setCTE_def) @@ -463,7 +463,7 @@ lemma fromEnum_maxBound_vppievent_irq_def: (* FIXME move *) lemma ps_clear_entire_slotI: "({p..p + 2 ^ n - 1}) \ dom (ksPSpace s) = {} \ ps_clear p n s" - by (fastforce simp: ps_clear_def) + by (fastforce simp: ps_clear_def mask_def add_diff_eq) lemma ps_clear_ksPSpace_upd_same[simp]: "ps_clear p n (s\ksPSpace := (ksPSpace s)(p \ v)\) = ps_clear p n s" @@ -531,6 +531,7 @@ lemma valid_untyped': apply (frule pspace_distinctD'[OF _ pspace_distinct']) apply simp apply (frule aligned_ranges_subset_or_disjoint[OF al]) + apply (simp only: add_mask_fold) apply (fold obj_range'_def) apply (rule iffI) apply auto[1] @@ -538,14 +539,15 @@ lemma valid_untyped': apply (rule ccontr, simp) apply (simp add: Set.psubset_eq) apply (erule conjE) - apply (case_tac "obj_range' ptr' ko \ {ptr..ptr + 2 ^ bits - 1} \ {}", simp) + apply (case_tac "obj_range' ptr' ko \ mask_range ptr bits \ {}", simp) apply (cut_tac is_aligned_no_overflow[OF al]) - apply (auto simp add: obj_range'_def)[1] + apply (auto simp add: obj_range'_def add_mask_fold)[1] apply (clarsimp simp add: usableUntypedRange.simps Int_commute) - apply (case_tac "obj_range' ptr' ko \ {ptr..ptr + 2 ^ bits - 1} \ {}", simp+) + apply (case_tac "obj_range' ptr' ko \ mask_range ptr bits \ {}", simp) apply (cut_tac is_aligned_no_overflow[OF al]) apply (clarsimp simp add: obj_range'_def) apply (frule is_aligned_no_overflow) + apply (simp add: mask_def add_diff_eq) by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1 nat_le_linear power_overflow sub_wrap add_0 add_0_right word_add_increasing word_less_1 word_less_sub_1) diff --git a/proof/crefine/ARM_HYP/Detype_C.thy b/proof/crefine/ARM_HYP/Detype_C.thy index a2634411f7..593bd9f0fb 100644 --- a/proof/crefine/ARM_HYP/Detype_C.thy +++ b/proof/crefine/ARM_HYP/Detype_C.thy @@ -396,13 +396,14 @@ proof - using vu unfolding valid_cap'_def valid_untyped'_def apply clarsimp apply (drule_tac x = x in spec) - apply (clarsimp simp:ko_wp_at'_def) + apply (clarsimp simp:ko_wp_at'_def add_mask_fold) done with koat have "\ {ptr..ptr + 2 ^ bits - 1} \ {x..x + 2 ^ objBits ko - 1}" apply - apply (erule obj_atE')+ - apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject) + apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject + add_mask_fold) done thus ?thesis using subset1 @@ -570,7 +571,7 @@ proof - apply simp apply clarsimp apply (drule_tac y = n in aligned_add_aligned [where m = 4]) - apply (simp add: tcb_cte_cases_def is_aligned_def split: if_split_asm) + apply (simp add: tcb_cte_cases_def cteSizeBits_def is_aligned_def split: if_split_asm) apply (simp add: word_bits_conv) apply simp done @@ -1645,7 +1646,7 @@ proof - hence "cpspace_relation ?ks' (underlying_memory (ksMachineState s)) ?th_s" unfolding cpspace_relation_def using cendpoint_relation_restrict [OF D.valid_untyped invs rl] - cnotification_relation_restrict [OF D.valid_untyped invs rl] + cnotification_relation_restrict [OF D.valid_untyped invs rl] b2 using cmap_array[simplified table_bits_defs] apply - apply (elim conjE) @@ -1793,7 +1794,7 @@ proof - apply (frule pspace_distinctD'[OF _ pspace_distinct']) apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def) apply (drule_tac x=x in spec) - apply (simp add: obj_range'_def objBitsKO_def) + apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq) apply (simp only: not_le) apply (cut_tac is_aligned_no_overflow[OF al]) apply (case_tac "ptr \ x + 2 ^ pageBits - 1", @@ -1846,7 +1847,7 @@ proof - apply (frule pspace_distinctD'[OF _ pspace_distinct']) apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def) apply (drule_tac x=x in spec) - apply (simp add: obj_range'_def objBitsKO_def) + apply (simp add: obj_range'_def objBitsKO_def mask_def add_diff_eq) apply (simp only: not_le) apply (cut_tac is_aligned_no_overflow[OF al]) apply (case_tac "ptr \ x + 2 ^ pageBits - 1", @@ -1872,9 +1873,9 @@ proof - \ {p ..+ 2 ^ objBitsT TCBT} \ {ptr..+2 ^ bits} = {}" apply (clarsimp simp: valid_cap'_def) apply (drule(1) map_to_ko_atI') - apply (clarsimp simp: obj_at'_def valid_untyped'_def2) + apply (clarsimp simp: obj_at'_def valid_untyped'_def2 mask_2pm1 add_diff_eq) apply (elim allE, drule(1) mp) - apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al) + apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al add_mask_fold[symmetric]) apply (subgoal_tac "objBitsKO ko = objBitsT TCBT") apply (subgoal_tac "p \ {p ..+ 2 ^ objBitsT TCBT}") apply simp diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 1402c6eb42..5ba460dc59 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -1756,7 +1756,7 @@ proof - apply (clarsimp simp:tcbs_of_def cte_at'_obj_at' split:if_splits) apply (drule_tac x = "0x10 * tcbVTableSlot" in bspec) - apply (simp add:tcb_cte_cases_def tcbVTableSlot_def) + apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbVTableSlot_def) apply simp done @@ -1766,7 +1766,7 @@ proof - apply (clarsimp simp:tcbs_of_def cte_at'_obj_at' split:if_splits) apply (drule_tac x = "0x10 * tcbCallerSlot" in bspec) - apply (simp add:tcb_cte_cases_def tcbCallerSlot_def) + apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbCallerSlot_def) apply simp done @@ -2303,7 +2303,7 @@ proof - threadSet_st_tcb_at_state threadSet_cte_wp_at' threadSet_cur | simp add: cur_tcb'_def[symmetric])+ - apply (simp add: valid_tcb'_def tcb_cte_cases_def + apply (simp add: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def valid_tcb_state'_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_ep_valid_objs' @@ -2512,7 +2512,7 @@ lemma threadSet_tcbState_valid_objs: threadSet (tcbState_update (\_. st)) t \\rv. valid_objs'\" apply (wp threadSet_valid_objs') - apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) + apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) done lemmas array_assertion_abs_tcb_ctes_add @@ -2564,7 +2564,7 @@ lemma fastpath_reply_recv_ccorres: apply (clarsimp simp:tcbs_of_def cte_at'_obj_at' split:if_splits) apply (drule_tac x = "0x10 * tcbVTableSlot" in bspec) - apply (simp add:tcb_cte_cases_def tcbVTableSlot_def) + apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbVTableSlot_def) apply simp done @@ -2574,7 +2574,7 @@ lemma fastpath_reply_recv_ccorres: apply (clarsimp simp:tcbs_of_def cte_at'_obj_at' split:if_splits) apply (drule_tac x = "0x10 * tcbCallerSlot" in bspec) - apply (simp add:tcb_cte_cases_def tcbCallerSlot_def) + apply (simp add:tcb_cte_cases_def cteSizeBits_def tcbCallerSlot_def) apply simp done diff --git a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy index b62ef16970..dd3fe2a797 100644 --- a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy +++ b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy @@ -305,7 +305,7 @@ lemma threadSet_tcbState_valid_objs: threadSet (tcbState_update (\_. st)) t \\rv. valid_objs'\" apply (wp threadSet_valid_objs') - apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) + apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs) done lemma possibleSwitchTo_rewrite: @@ -1766,7 +1766,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: in cte_wp_at_valid_objs_valid_cap', clarsimp+) apply (clarsimp simp: valid_cap_simps') apply (subst tcb_at_cte_at_offset, - assumption, simp add: tcb_cte_cases_def cte_level_bits_def tcbSlots) + assumption, simp add: tcb_cte_cases_def cteSizeBits_def cte_level_bits_def tcbSlots) apply (clarsimp simp: inj_case_bool cte_wp_at_ctes_of length_msgRegisters order_less_imp_le diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy index 24322083b4..43dfecf112 100644 --- a/proof/crefine/ARM_HYP/Finalise_C.thy +++ b/proof/crefine/ARM_HYP/Finalise_C.thy @@ -832,7 +832,7 @@ lemma doUnbindNotification_ccorres: apply simp apply (erule(1) rf_sr_tcb_update_no_queue2) apply (simp add: typ_heap_simps')+ - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) apply (simp add: invs'_def valid_state'_def) apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ @@ -882,7 +882,7 @@ lemma doUnbindNotification_ccorres': apply simp apply (erule(1) rf_sr_tcb_update_no_queue2) apply (simp add: typ_heap_simps')+ - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) apply (simp add: invs'_def valid_state'_def) apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ @@ -1896,7 +1896,7 @@ lemma archThreadSet_tcbVCPU_Basic_ccorres: update_tcb_map_to_tcb cmachine_state_relation_def update_tcb_map_tos)?) - apply (subst map_to_ctes_upd_tcb_no_ctes; simp add: tcb_cte_cases_def) + apply (subst map_to_ctes_upd_tcb_no_ctes; simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (erule cmap_relation_updI, erule ko_at_projectKO_opt, simp+) apply (clarsimp simp: ctcb_relation_def carch_tcb_relation_def ccontext_relation_def atcbContextGet_def) apply clarsimp diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index 8777d9b3c6..4b9b60e98a 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -4860,7 +4860,7 @@ lemma sendIPC_block_ccorres_helper: rf_sr_tcb_update_twice) apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps')+)[1] - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: ctcb_relation_def cthread_state_relation_def ThreadState_defs mask_def) apply ceqv @@ -4870,7 +4870,7 @@ lemma sendIPC_block_ccorres_helper: threadSet_valid_objs') apply (clarsimp simp: guard_is_UNIV_def) apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def - tcb_cte_cases_def) + tcb_cte_cases_def tcb_cte_cases_neqs) apply clarsimp done @@ -5416,7 +5416,7 @@ lemma receiveIPC_block_ccorres_helper: apply (frule h_t_valid_c_guard) apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice cap_get_tag_isCap) apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps)+) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: ctcb_relation_def cthread_state_relation_def ccap_relation_ep_helpers ThreadState_defs mask_def cap_get_tag_isCap) apply ceqv @@ -5426,7 +5426,7 @@ lemma receiveIPC_block_ccorres_helper: threadSet_weak_sch_act_wf_runnable') apply (clarsimp simp: guard_is_UNIV_def) apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def - tcb_cte_cases_def) + tcb_cte_cases_def tcb_cte_cases_neqs) apply clarsimp done @@ -6421,7 +6421,7 @@ lemma receiveSignal_block_ccorres_helper: apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice) apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps')+) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: ctcb_relation_def cthread_state_relation_def ThreadState_defs mask_def) apply ceqv @@ -6430,7 +6430,7 @@ lemma receiveSignal_block_ccorres_helper: apply (wp hoare_vcg_all_lift threadSet_valid_objs' threadSet_weak_sch_act_wf_runnable') apply (clarsimp simp: guard_is_UNIV_def) - apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def + apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def tcb_cte_cases_neqs valid_tcb_state'_def) done diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index 4e0d5d49fd..9b2c5fd10e 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -139,11 +139,11 @@ lemma getObject_return: lemmas getObject_return_tcb = getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb, - unfolded objBits_simps', simplified] + unfolded gen_objBits_simps tcbBlockSizeBits_def, simplified] lemmas setObject_modify_tcb = setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb, - unfolded objBits_simps', simplified] + unfolded gen_objBits_simps tcbBlockSizeBits_def, simplified] lemma partial_overwrite_fun_upd: "inj idx \ diff --git a/proof/crefine/ARM_HYP/Recycle_C.thy b/proof/crefine/ARM_HYP/Recycle_C.thy index 2db441b729..3d1aadc6a4 100644 --- a/proof/crefine/ARM_HYP/Recycle_C.thy +++ b/proof/crefine/ARM_HYP/Recycle_C.thy @@ -555,10 +555,10 @@ lemma heap_to_user_data_in_user_mem'[simp]: apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 2]) apply (erule aligned_add_aligned) apply (simp add: is_aligned_mult_triv2[where n = 2,simplified]) - apply (clarsimp simp: objBits_simps ARM_HYP.pageBits_def) + apply (clarsimp simp: ARM_HYP.objBits_simps ARM_HYP.pageBits_def) apply simp apply (rule is_aligned_add_helper[THEN conjunct2]) - apply (simp add: ARM_HYP.pageBits_def objBits_simps) + apply (simp add: ARM_HYP.pageBits_def ARM_HYP.objBits_simps) apply (rule word_less_power_trans2[where k = 2,simplified]) apply (rule less_le_trans[OF ucast_less]) apply simp+ diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 1c73871530..0330262eb5 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -662,7 +662,7 @@ lemma threadSet_all_invs_triv': apply (simp add: tcb_relation_def arch_tcb_context_set_def atcbContextSet_def arch_tcb_relation_def) apply (simp add: tcb_cap_cases_def) - apply (simp add: tcb_cte_cases_def) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs) apply fastforce apply fastforce apply fastforce diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index a960eb388c..34fa1aad9b 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -1402,7 +1402,7 @@ lemma zero_ranges_ptr_retyps: apply (erule disjoint_subset[rotated]) apply (subst intvl_plus_unat_eq) apply clarsimp - apply clarsimp + apply (clarsimp simp: mask_def add_diff_eq) apply (clarsimp simp: word_unat.Rep_inject[symmetric] valid_cap_simps' capAligned_def unat_of_nat @@ -2850,7 +2850,7 @@ qed lemma dom_tcb_cte_cases_iff: "(x \ dom tcb_cte_cases) = (\y < 5. unat x = y * 16)" unfolding tcb_cte_cases_def - by (auto simp: unat_arith_simps) + by (auto simp: unat_arith_simps cteSizeBits_def) lemma cmap_relation_retype2: assumes cm: "cmap_relation mp mp' Ptr rel" @@ -5536,7 +5536,7 @@ proof - apply (clarsimp simp: ps_clear_def) apply (subst dom_fun_upd[simplified fun_upd_def]) apply (simp only: option.distinct if_False) - apply (subgoal_tac "({x..x + 2 ^ objBitsKO y - 1} - {x}) \ {p} = {}") + apply (subgoal_tac "({x..x + mask (objBitsKO y)} - {x}) \ {p} = {}") apply fastforce apply (drule (2) pspace_no_overlapD3') apply (simp only: obj_range'_def) @@ -6132,7 +6132,7 @@ lemma threadSet_domain_ccorres [corres]: apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def) apply (clarsimp simp: update_tcb_map_tos typ_heap_simps') - apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def) + apply (simp add: map_to_ctes_upd_tcb_no_ctes map_to_tcbs_upd tcb_cte_cases_def tcb_cte_cases_neqs) apply (simp add: cep_relations_drop_fun_upd cvariable_relation_upd_const ko_at_projectKO_opt) apply (drule ko_at_projectKO_opt) @@ -6596,6 +6596,10 @@ lemma pspace_no_overlap_induce_vcpu: apply (erule (1) disjoint_subset[OF vcpu_range_subseteq[simplified]]) done +lemma add_abc_bac: + "a + b + c = b + a + (c::'a::semiring)" + by (simp add: field_simps) + lemma ctes_of_ko_at_strong: "\ctes_of s p = Some a; is_aligned p cteSizeBits\ \ (\ptr ko. (ksPSpace s ptr = Some ko \ {p ..+ 2^cteSizeBits} \ obj_range' ptr ko))" @@ -6605,7 +6609,7 @@ lemma ctes_of_ko_at_strong: apply (subst intvl_range_conv[where bits=cteSizeBits]) apply simp apply (simp add: word_bits_def objBits_defs) - apply (simp add: field_simps) + apply (simp add: field_simps mask_def) apply (intro exI conjI, assumption) apply (clarsimp simp: objBits_simps obj_range'_def word_and_le2) apply (cut_tac intvl_range_conv[where bits=cteSizeBits and ptr=p, simplified]) @@ -6618,11 +6622,14 @@ lemma ctes_of_ko_at_strong: apply clarsimp apply (thin_tac "P \ Q" for P Q) apply (erule order_trans) - apply (subst word_plus_and_or_coroll2[where x=p and w="mask tcbBlockSizeBits",symmetric]) - apply (clarsimp simp: tcb_cte_cases_def field_simps split: if_split_asm; - simp only: p_assoc_help; - rule word_plus_mono_right[OF _ is_aligned_no_wrap', OF _ Aligned.is_aligned_neg_mask[OF le_refl]]; - simp add: objBits_defs) + apply (simp add: add_mask_fold) + apply (subst and_plus_not_and[where x=p and y="mask tcbBlockSizeBits",symmetric]) + (* we want "(p && ~~ ...)" on the left *) + apply (subst add_abc_bac, subst add.assoc) + apply (rule word_plus_mono_right[OF _ is_aligned_no_wrap', + OF _ Aligned.is_aligned_neg_mask[OF le_refl]]) + apply (clarsimp simp: tcb_cte_cases_def cteSizeBits_def objBits_defs mask_def split: if_split_asm) + apply (simp add: objBits_defs mask_def) done lemma pspace_no_overlap_induce_cte: @@ -6652,7 +6659,7 @@ lemma pspace_no_overlap_induce_cte: apply (subst intvl_range_conv) apply simp apply (simp add: word_bits_def) - apply (simp add: obj_range'_def) + apply (simp add: obj_range'_def ptr_range_mask_range del: Int_atLeastAtMost) done lemma pspace_no_overlap_induce_asidpool: @@ -7129,6 +7136,7 @@ lemma tcb_ctes_typ_region_bytes: pspace_no_overlap'_def is_aligned_neg_mask_eq simp_thms field_simps upto_intvl_eq[symmetric]) apply (elim allE, drule(1) mp) + apply (simp add: mask_def add_diff_eq upto_intvl_eq[symmetric] del: Int_atLeastAtMost) apply (drule(1) pspace_alignedD') apply (erule disjoint_subset[rotated]) apply (simp add: upto_intvl_eq[symmetric]) @@ -7186,7 +7194,7 @@ lemma ccorres_typ_region_bytes_dummy: tcb_ctes_typ_region_bytes[OF _ _ invs_pspace_aligned']) apply (simp add: cmap_array_typ_region_bytes_triv invs_pspace_aligned' table_bits_defs - objBitsT_simps word_bits_def + objBitsT_simps word_bits_def[simplified word_size_bits_def] zero_ranges_are_zero_typ_region_bytes) apply (rule htd_safe_typ_region_bytes, simp) apply blast diff --git a/proof/crefine/ARM_HYP/SR_lemmas_C.thy b/proof/crefine/ARM_HYP/SR_lemmas_C.thy index 8e3d15e72b..97a573cdcc 100644 --- a/proof/crefine/ARM_HYP/SR_lemmas_C.thy +++ b/proof/crefine/ARM_HYP/SR_lemmas_C.thy @@ -911,9 +911,9 @@ proof - apply (rule is_aligned_weaken[OF _ bits]) apply (erule cte_wp_atE') apply assumption - apply (simp add: tcb_cte_cases_def field_simps split: if_split_asm) + apply (simp add: tcb_cte_cases_def tcb_cte_cases_neqs field_simps split: if_split_asm) apply (fastforce elim: aligned_add_aligned[OF _ _ cte_bits_le_tcb_bits] - simp: is_aligned_def cte_level_bits_def)+ + simp: is_aligned_def cte_level_bits_def cteSizeBits_def)+ apply (erule is_aligned_weaken[OF _ cte_bits_le_tcb_bits]) done qed diff --git a/proof/crefine/ARM_HYP/Schedule_C.thy b/proof/crefine/ARM_HYP/Schedule_C.thy index be16239f3f..6e0670e9a3 100644 --- a/proof/crefine/ARM_HYP/Schedule_C.thy +++ b/proof/crefine/ARM_HYP/Schedule_C.thy @@ -736,7 +736,7 @@ lemma threadSet_timeSlice_ccorres [corres]: apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (clarsimp simp: cmachine_state_relation_def carch_state_relation_def cpspace_relation_def) apply (clarsimp simp: update_tcb_map_tos typ_heap_simps') - apply (simp add: map_to_ctes_upd_tcb_no_ctes tcb_cte_cases_def + apply (simp add: map_to_ctes_upd_tcb_no_ctes tcb_cte_cases_def tcb_cte_cases_neqs map_to_tcbs_upd) apply (simp add: cep_relations_drop_fun_upd cvariable_relation_upd_const ko_at_projectKO_opt) diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy index 8631445958..fdbe0863ec 100644 --- a/proof/crefine/ARM_HYP/Syscall_C.thy +++ b/proof/crefine/ARM_HYP/Syscall_C.thy @@ -591,7 +591,7 @@ lemma rf_sr_tcb_update_twice: lemma tcb_cte_cases_tcbFault_update_simp: "(f, u) \ ran tcb_cte_cases \ f (tcbFault_update (\_. Some fault) tcb) = f tcb" unfolding tcb_cte_cases_def - by auto + by (auto simp: tcb_cte_cases_neqs) lemma hrs_mem_update_use_hrs_mem: "hrs_mem_update f = (\hrs. (hrs_mem_update $ (\_. f (hrs_mem hrs))) hrs)" diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index 9f710990d7..547330b5c0 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -115,6 +115,7 @@ lemma getObject_state: apply clarsimp apply (erule impE) apply simp + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow, simp add: word_bits_def) @@ -135,6 +136,7 @@ lemma getObject_state: apply clarsimp apply (erule impE) apply simp + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -145,6 +147,7 @@ lemma getObject_state: apply fastforce apply clarsimp apply (erule impE) + apply (simp flip: add_mask_fold) apply (rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -210,6 +213,7 @@ lemma asUser_state: apply fastforce apply clarsimp apply (erule impE, simp) + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -237,6 +241,7 @@ lemma asUser_state: apply fastforce apply clarsimp apply (erule impE, simp) + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -248,6 +253,7 @@ lemma asUser_state: apply fastforce apply clarsimp apply (erule impE) + apply (simp flip: add_mask_fold) apply (rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -967,7 +973,7 @@ lemma invokeTCB_ThreadControl_ccorres: apply (subgoal_tac "s \' capability.ThreadCap target") apply (clarsimp simp: cte_level_bits_def Kernel_C.tcbCTable_def Kernel_C.tcbVTable_def tcbCTableSlot_def tcbVTableSlot_def size_of_def - tcb_cte_cases_def isCap_simps + tcb_cte_cases_def cteSizeBits_def isCap_simps split: option.split_asm dest!: isValidVTableRootD) apply (clarsimp simp: valid_cap'_def capAligned_def word_bits_conv @@ -1293,6 +1299,7 @@ lemma getObject_context: apply clarsimp apply (erule impE) apply simp + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -1314,6 +1321,7 @@ lemma getObject_context: apply clarsimp apply (erule impE) apply simp + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -1324,6 +1332,7 @@ lemma getObject_context: apply fastforce apply clarsimp apply (erule impE) + apply (simp flip: add_mask_fold) apply (rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -1389,6 +1398,7 @@ lemma asUser_context: apply fastforce apply clarsimp apply (erule impE, simp) + apply (simp flip: add_mask_fold) apply (erule notE, rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow) @@ -1400,6 +1410,7 @@ lemma asUser_context: apply fastforce apply clarsimp apply (erule impE) + apply (simp flip: add_mask_fold) apply (rule word_diff_ls'(3)) apply unat_arith apply (drule is_aligned_no_overflow)