From eb2de995119e5987a6bccc0bc6a1653f202c4bad Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 2 Aug 2020 10:14:19 +0800 Subject: [PATCH] arm-hyp crefine: update to Isabelle2020 Signed-off-by: Gerwin Klein --- proof/crefine/ARM_HYP/ArchMove_C.thy | 2 +- proof/crefine/ARM_HYP/Arch_C.thy | 8 +++--- proof/crefine/ARM_HYP/CSpace_C.thy | 8 ++++-- proof/crefine/ARM_HYP/CSpace_RAB_C.thy | 14 ++++------ proof/crefine/ARM_HYP/Delete_C.thy | 5 ++-- proof/crefine/ARM_HYP/DetWP.thy | 2 +- proof/crefine/ARM_HYP/Fastpath_C.thy | 25 +++++++++++++---- proof/crefine/ARM_HYP/Finalise_C.thy | 13 +++++---- proof/crefine/ARM_HYP/Invoke_C.thy | 13 ++++----- proof/crefine/ARM_HYP/IpcCancel_C.thy | 4 +-- proof/crefine/ARM_HYP/Ipc_C.thy | 17 +++++++++--- .../crefine/ARM_HYP/IsolatedThreadAction.thy | 8 ++++-- proof/crefine/ARM_HYP/Recycle_C.thy | 1 + proof/crefine/ARM_HYP/Refine_C.thy | 1 + proof/crefine/ARM_HYP/Retype_C.thy | 19 ++++++------- proof/crefine/ARM_HYP/Schedule_C.thy | 4 +-- proof/crefine/ARM_HYP/SyscallArgs_C.thy | 1 + proof/crefine/ARM_HYP/Syscall_C.thy | 7 ++--- proof/crefine/ARM_HYP/VSpace_C.thy | 27 +++++++++++-------- 19 files changed, 110 insertions(+), 69 deletions(-) diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy index cb742e2fe..00df9c605 100644 --- a/proof/crefine/ARM_HYP/ArchMove_C.thy +++ b/proof/crefine/ARM_HYP/ArchMove_C.thy @@ -158,7 +158,7 @@ lemma setCTE_asidpool': apply (simp add: updateObject_cte) apply (clarsimp simp: updateObject_cte typeError_def magnitudeCheck_def in_monad split: kernel_object.splits if_splits option.splits) - apply (clarsimp simp: ps_clear_upd' lookupAround2_char1) + apply (clarsimp simp: ps_clear_upd lookupAround2_char1) done lemma udpateCap_asidpool': diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index cbd514f0f..2e2478b37 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/proof/crefine/ARM_HYP/Arch_C.thy @@ -2276,8 +2276,8 @@ lemma injection_handler_whenE: = (if a then (injection_handler Inl b) else (returnOk ()))" apply (subst injection_handler_returnOk[symmetric]) - apply (clarsimp simp:whenE_def injection_handler_def) - apply (fastforce simp:split:if_splits) + apply (clarsimp simp: whenE_def injection_handler_def cong: if_cong) + apply (fastforce split: if_splits) done lemma injection_handler_if_returnOk: @@ -2590,7 +2590,7 @@ lemma decodeARMFrameInvocation_ccorres: (decodeARMMMUInvocation label args cptr slot cp extraCaps >>= invocationCatch thread isBlocking isCall InvokeArchObject) (Call decodeARMFrameInvocation_'proc)" - + supply if_cong[cong] option.case_cong[cong] apply (clarsimp simp only: isCap_simps) apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' excaps_' cap_' buffer_' simp: decodeARMMMUInvocation_def decodeARMPageFlush_def) @@ -3155,7 +3155,7 @@ proof - using assms apply (subst AND_NOT_mask_plus_AND_mask_eq [where w = start,symmetric,where n = "pageBitsForSize a"]) - apply (simp add:sign_simps page_base_def) + apply (simp add: page_base_def) apply (drule word_le_minus_mono_left[where x= "start && ~~ mask (pageBitsForSize a)"]) apply (rule word_and_le2) apply (simp(no_asm_use), simp) diff --git a/proof/crefine/ARM_HYP/CSpace_C.thy b/proof/crefine/ARM_HYP/CSpace_C.thy index f3d99921f..2e99e6e35 100644 --- a/proof/crefine/ARM_HYP/CSpace_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_C.thy @@ -853,6 +853,7 @@ lemma update_freeIndex': have i'_bound_word: "(of_nat i' :: machine_word) \ 2 ^ maxUntypedSizeBits" using order_trans[OF i'_bound power_increasing[OF sz_bound], simplified] by (simp add: word_of_nat_le untypedBits_defs) + note option.case_cong[cong] if_cong[cong] show ?thesis apply (cinit lift: cap_ptr_' v32_') apply (rule ccorres_pre_getCTE) @@ -2319,7 +2320,7 @@ lemma heap_list_zero_Ball_intvl: lemma untypedZeroRange_not_device: "untypedZeroRange cap = Some r \ \ capIsDevice cap" - by (clarsimp simp: untypedZeroRange_def) + by (clarsimp simp: untypedZeroRange_def cong: if_cong) lemma updateTrackedFreeIndex_noop_ccorres: "ccorres dc xfdc (cte_wp_at' ((\cap. isUntypedCap cap @@ -2478,6 +2479,7 @@ lemma emptySlot_ccorres: [] (emptySlot slot info) (Call emptySlot_'proc)" + supply if_cong[cong] apply (cinit lift: slot_' cleanupInfo_' simp: case_Null_If) \ \--- handle the clearUntypedFreeIndex\ @@ -2740,6 +2742,7 @@ lemma Arch_sameRegionAs_spec: ccap_relation (ArchObjectCap capb) \cap_b \ Call Arch_sameRegionAs_'proc \ \ret__unsigned_long = from_bool (Arch.sameRegionAs capa capb) \" + supply if_cong[cong] apply vcg apply clarsimp @@ -3731,7 +3734,7 @@ lemma sameRegionAs_NotificationCap: done lemma isMDBParentOf_spec: - notes option.case_cong_weak [cong] + notes option.case_cong_weak [cong] if_cong[cong] shows "\ctea cte_a cteb cte_b. \ \ {s. cslift s (cte_a_' s) = Some cte_a \ ccte_relation ctea cte_a \ @@ -3829,6 +3832,7 @@ lemma updateCapData_spec: "\cap. \ \ \ ccap_relation cap \cap \ preserve = to_bool (\preserve) \ newData = \newData\ Call updateCapData_'proc \ ccap_relation (updateCapData preserve newData cap) \ret__struct_cap_C \" + supply if_cong[cong] apply (rule allI, rule conseqPre) apply vcg apply (clarsimp simp: if_1_0_0) diff --git a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy index eb3bb37e7..e427b36a8 100644 --- a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy @@ -79,7 +79,7 @@ next fix s s' assume "(s, s') \ rf_sr" and "(G and P) s" and "s' \ G'" thus "(G and (\_. \s. P s)) s \ s' \ G'" - by (clarsimp elim!: exI) + by fastforce qed (* MOVE, generalise *) @@ -102,10 +102,6 @@ lemma valid_cap_cte_at': done -declare ucast_id [simp] -declare resolveAddressBits.simps [simp del] - - lemma rightsFromWord_wordFromRights: "rightsFromWord (wordFromRights rghts) = rghts" apply (cases rghts) @@ -185,11 +181,11 @@ proof (cases "isCNodeCap cap'") \ \Exception stuff\ apply (rule ccorres_split_throws) apply (simp add: Collect_const cap_get_tag_isCap isCap_simps ccorres_cond_iffs - resolveAddressBits.simps scast_id) + resolveAddressBits.simps) apply (rule ccorres_from_vcg_throws [where P = \ and P' = UNIV]) apply (rule allI) apply (rule conseqPre) - apply (simp add: throwError_def return_def split) + apply (simp add: throwError_def return_def) apply vcg apply (clarsimp simp add: exception_defs lookup_fault_lift_def) apply (simp split: if_split) @@ -427,14 +423,14 @@ next apply (simp add: cap_simps) done - note if_cong[cong] + note if_cong[cong] option.case_cong[cong] show ?case using ind.prems apply - apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (subst resolveAddressBits.simps) apply (unfold case_into_if) - apply (simp add: Let_def ccorres_cond_iffs split del: if_split) + apply (simp add: Let_def ccorres_cond_iffs) apply (rule ccorres_rhs_assoc)+ apply (cinitlift nodeCap_' n_bits_') apply (erule_tac t = nodeCapa in ssubst) diff --git a/proof/crefine/ARM_HYP/Delete_C.thy b/proof/crefine/ARM_HYP/Delete_C.thy index 26d564cbc..bd5e49ec8 100644 --- a/proof/crefine/ARM_HYP/Delete_C.thy +++ b/proof/crefine/ARM_HYP/Delete_C.thy @@ -138,6 +138,7 @@ lemma capRemovable_spec: "\cap s. \\ \s. ccap_relation cap \cap \ (isZombie cap \ cap = NullCap) \ capAligned cap\ Call capRemovable_'proc {s'. ret__unsigned_long_' s' = from_bool (capRemovable cap (ptr_val (slot_' s)))}" + supply if_cong[cong] apply vcg apply (clarsimp simp: cap_get_tag_isCap(1-8)[THEN trans[OF eq_commute]]) apply (simp add: capRemovable_def from_bool_def[where b=True] true_def) @@ -157,6 +158,7 @@ lemma capCyclicZombie_spec: "\cap s. \\ \s. ccap_relation cap \cap \ isZombie cap \ capAligned cap\ Call capCyclicZombie_'proc {s'. ret__unsigned_long_' s' = from_bool (capCyclicZombie cap (ptr_val (slot_' s)))}" + supply if_cong[cong] apply vcg apply (clarsimp simp: from_bool_0) apply (frule(1) cap_get_tag_isCap [THEN iffD2], simp) @@ -393,8 +395,7 @@ lemma ccorres_cutMon_locateSlotCap_Zombie: apply (drule(1) rf_sr_gsCNodes_array_assertion) apply (erule notE, erule array_assertion_shrink_right) apply (frule valid_Zombie_number_word_bits, simp+) - by (simp add: unat_arith_simps unat_of_nat word_bits_def - valid_cap_simps') + by (simp add: unat_arith_simps unat_of_nat word_bits_def valid_cap_simps') lemma reduceZombie_ccorres1: assumes fs_cc: diff --git a/proof/crefine/ARM_HYP/DetWP.thy b/proof/crefine/ARM_HYP/DetWP.thy index 63e94adfc..ebd0aef2f 100644 --- a/proof/crefine/ARM_HYP/DetWP.thy +++ b/proof/crefine/ARM_HYP/DetWP.thy @@ -60,7 +60,7 @@ lemma det_wp_getTCB [wp]: apply (rule det_wp_pre) apply (wp|wpc)+ apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps - cong: conj_cong) + cong: conj_cong option.case_cong) apply (simp add: lookupAround2_known1) apply (rule ps_clear_lookupAround2, assumption+) apply simp diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 2d0e630e5..fd8968ba2 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -407,9 +407,10 @@ lemma lookup_fp_ccorres': have cap_get_tag_update_1: "\f cap. cap_get_tag (cap_C.words_C_update (\w. Arrays.update w (Suc 0) (f w)) cap) = cap_get_tag cap" - by (simp add: cap_get_tag_def) + by (simp add: cap_get_tag_def cong: if_cong) show ?case + supply if_cong[cong] apply (cinitlift cap_' bits_') apply (rename_tac cbits ccap) apply (elim conjE) @@ -502,7 +503,7 @@ lemma lookup_fp_ccorres': apply (rule ccorres_cutMon) apply (simp add: cutMon_walk_bindE unlessE_whenE del: Collect_const - split del: if_split cong: call_ignore_cong) + cong: call_ignore_cong) apply (rule ccorres_drop_cutMon_bindE) apply csymbr+ apply (rule ccorres_rhs_assoc2) @@ -2133,7 +2134,7 @@ lemma recv_ep_queued_st_tcb_at': done lemma fastpath_call_ccorres: - notes hoare_TrueI[simp] + notes hoare_TrueI[simp] if_cong[cong] option.case_cong[cong] shows "ccorres dc xfdc (\s. invs' s \ ct_in_state' ((=) Running) s \ obj_at' (\tcb. (atcbContextGet o tcbArch) tcb ARM_HYP_H.capRegister = cptr @@ -2947,7 +2948,7 @@ lemma fastpath_reply_cap_check_ccorres: done lemma fastpath_reply_recv_ccorres: - notes hoare_TrueI[simp] + notes hoare_TrueI[simp] if_cong[cong] option.case_cong[cong] shows "ccorres dc xfdc (\s. invs' s \ ct_in_state' ((=) Running) s \ obj_at' (\tcb. (atcbContextGet o tcbArch) tcb capRegister = cptr @@ -3842,9 +3843,13 @@ lemma setCTE_obj_at'_tcbIPCBuffer: unfolding setCTE_def by (rule setObject_cte_obj_at_tcb', simp+) +context +notes if_cong[cong] +begin crunches cteInsert, asUser for obj_at'_tcbIPCBuffer[wp]: "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest) +end crunch ksReadyQueues_inv[wp]: cteInsert "\s. P (ksReadyQueues s)" (wp: hoare_drop_imps) @@ -3889,6 +3894,7 @@ lemma fastpath_callKernel_SysCall_corres: and (\s. ksSchedulerAction s = ResumeCurrentThread) and (\s. ksDomainTime s \ 0)) (callKernel (SyscallEvent SysCall)) (fastpaths SysCall)" + supply if_cong[cong] option.case_cong[cong] apply (rule monadic_rewrite_introduce_alternative) apply (simp add: callKernel_def) apply (rule monadic_rewrite_imp) @@ -4649,7 +4655,7 @@ lemma setEndpoint_clearUntypedFreeIndex_pivot[unfolded K_bind_def]: setEndpoint_getCTE_pivot updateTrackedFreeIndex_def modify_setEndpoint_pivot - split: capability.split + split: capability.split cong: option.case_cong | rule bind_cong[OF refl] allI impI bind_apply_cong[OF refl])+ @@ -4882,8 +4888,12 @@ lemma tcbSchedEnqueue_tcbIPCBuffer: crunch obj_at'_tcbIPCBuffer[wp]: rescheduleRequired "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: crunch_wps tcbSchedEnqueue_tcbIPCBuffer simp: rescheduleRequired_def) +context +notes if_cong[cong] +begin crunch obj_at'_tcbIPCBuffer[wp]: setThreadState "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: crunch_wps threadSet_obj_at'_really_strongest) +end crunch obj_at'_tcbIPCBuffer[wp]: getCTE "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: setCTE_obj_at'_queued crunch_wps threadSet_obj_at'_really_strongest) @@ -4897,9 +4907,13 @@ crunch obj_at'_tcbIPCBuffer[wp]: transferCapsToSlots "obj_at' (\tcb. P ( crunch obj_at'_tcbIPCBuffer[wp]: asUser "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: crunch_wps) +context +notes if_cong[cong] +begin crunch obj_at'_tcbIPCBuffer[wp]: handleFault "obj_at' (\tcb. P (tcbIPCBuffer tcb)) t" (wp: crunch_wps constOnFailure_wp tcbSchedEnqueue_tcbIPCBuffer threadSet_obj_at'_really_strongest simp: zipWithM_x_mapM) +end lemma fastpath_callKernel_SysReplyRecv_corres: "monadic_rewrite True False @@ -4907,6 +4921,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: and cnode_caps_gsCNodes') (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)" including no_pre + supply if_cong[cong] option.case_cong[cong] apply (rule monadic_rewrite_introduce_alternative) apply ( simp add: callKernel_def) apply (rule monadic_rewrite_imp) diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy index f9f467abb..a1948f8be 100644 --- a/proof/crefine/ARM_HYP/Finalise_C.thy +++ b/proof/crefine/ARM_HYP/Finalise_C.thy @@ -791,6 +791,7 @@ lemma unbindNotification_ccorres: "ccorres dc xfdc (invs') (UNIV \ {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) [] (unbindNotification tcb) (Call unbindNotification_'proc)" + supply option.case_cong[cong] apply (cinit lift: tcb_') apply (rule_tac xf'=ntfnPtr_' and r'="\rv rv'. rv' = option_to_ptr rv \ rv \ Some 0" @@ -824,6 +825,7 @@ lemma unbindNotification_ccorres: lemma unbindMaybeNotification_ccorres: "ccorres dc xfdc (invs') (UNIV \ {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) [] (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)" + supply option.case_cong[cong] apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) @@ -1132,7 +1134,7 @@ lemma deleteASIDPool_ccorres: apply (erule is_aligned_add_less_t2n) apply (subst(asm) Suc_unat_diff_1) apply (simp add: asid_low_bits_def) - apply (simp add: unat_power_lower asid_low_bits_word_bits) + apply (simp add: asid_low_bits_word_bits) apply (erule of_nat_less_pow_32 [OF _ asid_low_bits_word_bits]) apply (simp add: asid_low_bits_def asid_bits_def) apply (simp add: asid_bits_def) @@ -2279,6 +2281,7 @@ lemma Arch_finaliseCap_ccorres: (UNIV \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} \ {s. final_' s = from_bool is_final}) [] (Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)" + supply if_cong[cong] apply (cinit lift: cap_' final_' cong: call_ignore_cong) apply csymbr apply (simp add: ARM_HYP_H.finaliseCap_def cap_get_tag_isCap_ArchObject) @@ -2322,7 +2325,7 @@ lemma Arch_finaliseCap_ccorres: apply (frule small_frame_cap_is_mapped_alt) apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def case_option_over_if - elim!: ccap_relationE simp del: Collect_const) + elim!: ccap_relationE) apply (simp add: split_def) apply (rule ccorres_rhs_assoc)+ apply csymbr @@ -2338,7 +2341,7 @@ lemma Arch_finaliseCap_ccorres: apply (frule small_frame_cap_is_mapped_alt) apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def case_option_over_if - elim!: ccap_relationE simp del: Collect_const) + elim!: ccap_relationE) apply (simp add: split_def) apply return_NullCap_pair_ccorres apply (clarsimp simp: isCap_simps) @@ -2356,7 +2359,7 @@ lemma Arch_finaliseCap_ccorres: apply (frule frame_cap_is_mapped_alt) apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def case_option_over_if - elim!: ccap_relationE simp del: Collect_const) + elim!: ccap_relationE) apply simp apply (rule ccorres_rhs_assoc)+ apply csymbr @@ -2373,7 +2376,7 @@ lemma Arch_finaliseCap_ccorres: apply (frule frame_cap_is_mapped_alt) apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def case_option_over_if - elim!: ccap_relationE simp del: Collect_const) + elim!: ccap_relationE) apply clarsimp apply return_NullCap_pair_ccorres apply (clarsimp simp: isCap_simps) diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy index 8d054d9ab..0bec2366c 100644 --- a/proof/crefine/ARM_HYP/Invoke_C.thy +++ b/proof/crefine/ARM_HYP/Invoke_C.thy @@ -587,6 +587,7 @@ lemma decodeCNodeInvocation_ccorres: (decodeCNodeInvocation lab args cp (map fst extraCaps) >>= invocationCatch thread isBlocking isCall InvokeCNode) (Call decodeCNodeInvocation_'proc)" + supply if_cong[cong] apply (cases "\isCNodeCap cp") apply (simp add: decodeCNodeInvocation_def cong: conj_cong) @@ -635,9 +636,8 @@ lemma decodeCNodeInvocation_ccorres: del: Collect_const cong: call_ignore_cong) apply (rule ccorres_split_throws) apply (rule ccorres_rhs_assoc | csymbr)+ - apply (simp add: invocationCatch_use_injection_handler - [symmetric, unfolded o_def] - if_1_0_0 dc_def[symmetric] + apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def] + dc_def[symmetric] del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add:if_P del: Collect_const) @@ -647,8 +647,7 @@ lemma decodeCNodeInvocation_ccorres: apply (simp add: syscall_error_to_H_cases) apply (simp add: linorder_not_less del: Collect_const cong: call_ignore_cong) apply csymbr - apply (simp add: if_1_0_0 interpret_excaps_test_null - excaps_map_def + apply (simp add: if_1_0_0 interpret_excaps_test_null excaps_map_def del: Collect_const) apply (rule ccorres_Cond_rhs_Seq) apply (simp add: throwError_bind invocationCatch_def) @@ -1837,7 +1836,7 @@ lemma byte_regions_unmodified_actually_heap_list: lemma resetUntypedCap_ccorres: notes upt.simps[simp del] Collect_const[simp del] replicate_numeral[simp del] - untypedBits_defs[simp] + untypedBits_defs[simp] if_cong[cong] option.case_cong[cong] shows "ccorres (cintr \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and sch_act_simple and ct_active' and cte_wp_at' (isUntypedCap o cteCap) slot @@ -2698,6 +2697,7 @@ lemma checkFreeIndex_ccorres: ;; \reset :== scast false) (\freeIndex :== 0 ;; \reset :== scast true)))" + supply if_cong[cong] apply (simp add: constOnFailure_def catch_def liftE_def bindE_bind_linearise bind_assoc case_sum_distrib) apply (rule ccorres_guard_imp2) apply (rule ccorres_split_nothrow_case_sum) @@ -2849,6 +2849,7 @@ lemma decodeUntypedInvocation_ccorres_helper: liftE (stateAssert (valid_untyped_inv' uinv) []); returnOk uinv odE) >>= invocationCatch thread isBlocking isCall InvokeUntyped) (Call decodeUntypedInvocation_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (rule ccorres_name_pre) apply (cinit' lift: invLabel_' length___unsigned_long_' cap_' slot_' excaps_' call_' buffer_' simp: decodeUntypedInvocation_def list_case_If2 diff --git a/proof/crefine/ARM_HYP/IpcCancel_C.thy b/proof/crefine/ARM_HYP/IpcCancel_C.thy index d968a3c91..ba5c4ce1f 100644 --- a/proof/crefine/ARM_HYP/IpcCancel_C.thy +++ b/proof/crefine/ARM_HYP/IpcCancel_C.thy @@ -91,8 +91,6 @@ lemma ntfn_ptr_get_queue_spec: apply clarsimp done -declare td_names_word8[simp] - abbreviation "cslift_all_but_tcb_C s t \ (cslift s :: cte_C typ_heap) = cslift t \ (cslift s :: endpoint_C typ_heap) = cslift t @@ -2300,7 +2298,7 @@ lemma possibleSwitchTo_ccorres: \ UNIV) [] (possibleSwitchTo t ) (Call possibleSwitchTo_'proc)" - supply if_split [split del] + supply if_split [split del] if_cong[cong] supply Collect_const [simp del] supply dc_simp [simp del] supply prio_and_dom_limit_helpers[simp] diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index e8bd2c4f8..b16829465 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -658,6 +658,7 @@ lemma handleFaultReply': msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (handleFaultReply' f s r)" + supply if_cong[cong] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -772,7 +773,6 @@ lemma handleFaultReply': split_def n_msgRegisters_def msgMaxLength_def bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric] word_size msgLengthBits_def n_syscallMessage_def Let_def - split del: if_split cong: if_weak_cong register.case_cong) @@ -1468,6 +1468,7 @@ lemma getRestartPC_ccorres [corres]: lemma asUser_tcbFault_obj_at: "\obj_at' (\tcb. P (tcbFault tcb)) t\ asUser t' m \\rv. obj_at' (\tcb. P (tcbFault tcb)) t\" + supply if_cong[cong] apply (simp add: asUser_def split_def) apply (wp threadGet_wp) apply simp @@ -4275,6 +4276,7 @@ lemma handleFaultReply_ccorres [corres]: msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (Call handleFaultReply_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (unfold K_def, rule ccorres_gen_asm) apply (rule monadic_rewrite_ccorres_assemble_nodrop[OF _ handleFaultReply',rotated], simp) apply (cinit lift: sender_' receiver_' simp: whileAnno_def) @@ -4384,6 +4386,10 @@ lemma handleFaultReply_ccorres [corres]: apply (fastforce simp: seL4_Faults seL4_Arch_Faults) done +context +notes if_cong[cong] +begin + crunch tcbFault: emptySlot, tcbSchedEnqueue, rescheduleRequired "obj_at' (\tcb. P (tcbFault tcb)) t" (wp: threadSet_obj_at'_strongish crunch_wps @@ -4393,12 +4399,14 @@ crunch tcbFault: setThreadState, cancelAllIPC, cancelAllSignals "obj_at' (\tcb. P (tcbFault tcb)) t" (wp: threadSet_obj_at'_strongish crunch_wps) +end + lemma sbn_tcbFault: "\obj_at' (\tcb. P (tcbFault tcb)) t\ setBoundNotification st t' \\_. obj_at' (\tcb. P (tcbFault tcb)) t\" apply (simp add: setBoundNotification_def) - apply (wp threadSet_obj_at' | simp)+ + apply (wp threadSet_obj_at' | simp cong: if_cong)+ done crunch tcbFault: unbindNotification, unbindMaybeNotification "obj_at' (\tcb. P (tcbFault tcb)) t" @@ -4431,7 +4439,7 @@ proof (rule hoare_gen_asm, induct caps arbitrary: x mi destSlots) next case (Cons cp cps) show ?case using Cons.prems - by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak) + by (wpsimp wp: Cons.hyps cteInsert_weak_cte_wp_at2 simp: Let_def split_def weak cong: if_cong) qed lemma transferCaps_local_slots: @@ -4534,7 +4542,7 @@ proof - apply ceqv apply csymbr apply wpc - apply (clarsimp simp: ccorres_cond_iffs split del: if_split) + apply (clarsimp simp: ccorres_cond_iffs) apply (fold dc_def)[1] apply (rule ccorres_rhs_assoc)+ apply (ctac(no_vcg)) @@ -6733,6 +6741,7 @@ lemma receiveSignal_ccorres [corres]: (receiveSignal thread cap is_blocking) (Call receiveSignal_'proc)" unfolding K_def + supply if_cong[cong] apply (rule ccorres_gen_asm) apply (cinit lift: thread_' cap_' isBlocking_') apply (rule ccorres_pre_getNotification, rename_tac ntfn) diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index e68dd8f1c..3819a35b2 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -808,6 +808,7 @@ lemma vcpuDisable_isolatable: lemma vcpuSwitch_isolatable: "thread_actions_isolatable idx (vcpuSwitch v)" + supply if_cong[cong] option.case_cong[cong] apply (clarsimp simp: vcpuSwitch_def when_def split: option.splits) apply (safe intro!: thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] @@ -966,6 +967,7 @@ lemma doIPCTransfer_simple_rewrite: y \ setMessageInfo rcvr ((messageInfoFromWord msgInfo) \msgCapsUnwrapped := 0\); asUser rcvr (setRegister ARM_HYP_H.badgeRegister badge) od)" + supply if_cong[cong] apply (rule monadic_rewrite_gen_asm) apply (simp add: doIPCTransfer_def bind_assoc doNormalTransfer_def getMessageInfo_def @@ -1420,6 +1422,7 @@ lemma assert_isolatable: lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" + supply if_cong[cong] apply (simp add: cteInsert_def updateCap_def updateMDB_def Let_def setUntypedCapAsFull_def) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)] @@ -1750,6 +1753,7 @@ lemma updateMDB_isolatable: lemma clearUntypedFreeIndex_isolatable: "thread_actions_isolatable idx (clearUntypedFreeIndex slot)" + supply option.case_cong[cong] apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) apply (rule thread_actions_isolatable_bind) apply (rule getCTE_isolatable) @@ -1787,6 +1791,7 @@ lemmas fastpath_isolate_rewrites lemma lookupIPCBuffer_isolatable: "thread_actions_isolatable idx (lookupIPCBuffer w t)" + supply if_cong[cong] apply (simp add: lookupIPCBuffer_def) apply (rule thread_actions_isolatable_bind) apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable @@ -1795,11 +1800,10 @@ lemma lookupIPCBuffer_isolatable: apply (rule thread_actions_isolatable_bind) apply (clarsimp simp: thread_actions_isolatable_return getCTE_isolatable - assert_isolatable split: capability.split arch_capability.split bool.split)+ apply (rule thread_actions_isolatable_if) apply (rule thread_actions_isolatable_bind) - apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+ + apply (simp add: thread_actions_isolatable_return | wp)+ done lemma setThreadState_rewrite_simple: diff --git a/proof/crefine/ARM_HYP/Recycle_C.thy b/proof/crefine/ARM_HYP/Recycle_C.thy index 778b37f9f..80286387e 100644 --- a/proof/crefine/ARM_HYP/Recycle_C.thy +++ b/proof/crefine/ARM_HYP/Recycle_C.thy @@ -1344,4 +1344,5 @@ lemma ccap_relation_isDeviceCap2: apply (frule cap_get_tag_UntypedCap) apply (simp add:cap_get_tag_isCap to_bool_def) done + end diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index 2dc196671..fbb21919a 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -839,6 +839,7 @@ lemma user_memory_update_corres_C: (\s. pspace_aligned' s \ pspace_distinct' s \ dom um \ dom (user_mem' s)) \ (doMachineOp (user_memory_update um)) (setUserMem_C um)" + supply option.case_cong[cong] apply (clarsimp simp: corres_underlying_def) apply (rule conjI) prefer 2 diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index b06149b58..ebfd190ba 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -871,6 +871,7 @@ lemma clift_ptr_retyps_gen_memset_same: = (\y. if y \ (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) o of_nat) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a :: mem_type)) 0)) else clift hrs y)" using sz + supply if_cong[cong] apply (simp add: nb liftt_if[folded hrs_mem_def hrs_htd_def] hrs_htd_update hrs_mem_update h_t_valid_ptr_retyps_gen_same[OF guard cleared not_byte] @@ -915,9 +916,9 @@ lemma clift_ptr_retyps_gen_other: = clift hrs" using sz cleared apply (cases p) - apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def] - h_t_valid_def hrs_htd_update - ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz]) + apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def] h_t_valid_def hrs_htd_update + ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz] + cong: if_cong) done lemma clift_heap_list_update_no_heap_other: @@ -2724,6 +2725,7 @@ lemma insertNewCap_ccorres1: \ {s. slot_' s = Ptr slot}) [] (insertNewCap parent slot cap) (Call insertNewCap_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (cinit (no_ignore_call) lift: cap_' parent_' slot_') apply (rule ccorres_liftM_getCTE_cte_at) apply (rule ccorres_move_c_guard_cte) @@ -3846,7 +3848,7 @@ lemma zero_ranges_are_zero_update_zero[simp]: \ zero_ranges_are_zero rs (hrs_mem_update (heap_update_list ptr (replicate n 0)) hrs)" apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update) apply (drule(1) bspec) - apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq) + apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq cong: if_cong) done lemma rf_sr_rep0: @@ -4957,8 +4959,7 @@ proof (intro impI allI) hence "cpspace_relation ?ks (underlying_memory (ksMachineState \)) ?ks'" unfolding cpspace_relation_def - using empty rc' szo - apply - + using empty rc' szo if_cong[cong] apply (clarsimp simp: rl' tag_disj_via_td_name cte_C_size ht_rl clift_ptr_retyps_gen_other foldr_upd_app_if [folded data_map_insert_def]) @@ -4975,10 +4976,9 @@ proof (intro impI allI) thus ?thesis using rf empty kdr rzo apply (simp add: rf_sr_def cstate_relation_def Let_def rl' tag_disj_via_td_name ) apply (simp add: carch_state_relation_def cmachine_state_relation_def) - apply (simp add: tag_disj_via_td_name rl' tcb_C_size h_t_valid_clift_Some_iff) + apply (simp add: tag_disj_via_td_name rl' h_t_valid_clift_Some_iff) apply (clarsimp simp: hrs_htd_update szo'[symmetric] cvariable_array_ptr_retyps[OF szo] rb') - apply (subst zero_ranges_ptr_retyps, simp_all only: szo'[symmetric] power_add, - simp) + apply (subst zero_ranges_ptr_retyps, simp_all only: szo'[symmetric] power_add, simp) apply (simp add:szo p2dist objBits_simps ko_def ptr_retyps_htd_safe_neg kernel_data_refs_domain_eq_rotate rl foldr_upd_app_if [folded data_map_insert_def] @@ -8221,6 +8221,7 @@ shows "ccorres dc xfdc ) [] (createNewObjects newType srcSlot destSlots ptr userSize isdev) (Call createNewObjects_'proc)" + supply if_cong[cong] apply (rule ccorres_gen_asm_state) apply clarsimp apply (subgoal_tac "unat (of_nat (getObjectSize newType userSize)) = getObjectSize newType userSize") diff --git a/proof/crefine/ARM_HYP/Schedule_C.thy b/proof/crefine/ARM_HYP/Schedule_C.thy index 72ceddf30..621b32fc5 100644 --- a/proof/crefine/ARM_HYP/Schedule_C.thy +++ b/proof/crefine/ARM_HYP/Schedule_C.thy @@ -393,8 +393,8 @@ lemma isHighestPrio_ccorres: supply prio_and_dom_limit_helpers[simp] supply Collect_const_mem [simp] (* FIXME: these should likely be in simpset for CRefine, or even in general *) - supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp] - ccorres_IF_True[simp] + supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] + ccorres_IF_True[simp] if_cong[cong] apply (cinit lift: dom_' prio_') apply clarsimp apply (rule ccorres_move_const_guard) diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index 7c08e4a7c..42ffe2194 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -1018,6 +1018,7 @@ lemma getMRs_user_word: \ msgLength info \ msgMaxLength \ i >= scast n_msgRegisters\ getMRs thread (Some buffer) info \\xs. user_word_at (xs ! unat i) (buffer + (i * 4 + 4))\" + supply if_cong[cong] apply (rule hoare_assume_pre) apply (elim conjE) apply (thin_tac "valid_ipc_buffer_ptr' x y" for x y) diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy index d480222f1..ba517e234 100644 --- a/proof/crefine/ARM_HYP/Syscall_C.thy +++ b/proof/crefine/ARM_HYP/Syscall_C.thy @@ -609,7 +609,7 @@ lemma sendFaultIPC_ccorres: \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr tptr}) [] (sendFaultIPC tptr fault) (Call sendFaultIPC_'proc)" - supply Collect_const[simp del] + supply Collect_const[simp del] if_cong[cong] apply (cinit lift: tptr_' cong: call_ignore_cong) apply (simp add: liftE_bindE del:Collect_const cong:call_ignore_cong) apply (rule ccorres_symb_exec_r) @@ -803,7 +803,7 @@ lemma getMRs_length: apply simp apply (wp mapM_length) apply (simp add: min_def length_msgRegisters) - apply (clarsimp simp: n_msgRegisters_def) + apply (clarsimp simp: n_msgRegisters_def cong: if_cong) apply (simp add: getMRs_def) apply (rule hoare_pre, wp) apply simp @@ -1254,7 +1254,7 @@ lemma not_obj_at'_ntfn: done lemma handleRecv_ccorres: - notes rf_sr_upd_safe[simp del] + notes rf_sr_upd_safe[simp del] if_cong[cong] shows "ccorres dc xfdc (\s. invs' s \ st_tcb_at' simple' (ksCurThread s) s @@ -1853,6 +1853,7 @@ proof - using word_ctz_le[where w=w, simplified] by (auto simp: unat_of_nat_eq) show ?thesis + supply if_cong[cong] apply (cinit) apply (rule ccorres_pre_getCurVCPU, rename_tac vcpuPtr_opt) apply wpc diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy index 38cafd012..c39079847 100644 --- a/proof/crefine/ARM_HYP/VSpace_C.thy +++ b/proof/crefine/ARM_HYP/VSpace_C.thy @@ -621,8 +621,8 @@ lemma generic_frame_cap_get_capFIsMapped_spec: Call generic_frame_cap_get_capFIsMapped_'proc \\ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \ 0 then 1 else 0)\" apply vcg - apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast]) -done + apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast] cong: if_cong) + done @@ -2032,6 +2032,7 @@ lemma vcpu_disable_ccorres: and (case v of None \ \ | Some new \ vcpu_at' new)) (UNIV \ {s. vcpu_' s = option_to_ptr v}) hs (vcpuDisable v) (Call vcpu_disable_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (cinit lift: vcpu_') apply (ctac (no_vcg) add: dsb_ccorres) apply (rule ccorres_split_nothrow_novcg) @@ -2274,6 +2275,7 @@ lemma vcpu_save_ccorres: (UNIV \ {s. vcpu_' s = case_option NULL (vcpu_Ptr \ fst) v} \ {s. active_' s = case_option 0 (from_bool \ snd) v}) hs (vcpuSave v) (Call vcpu_save_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (cinit lift: vcpu_' active_' simp: whileAnno_def) apply wpc (* v = None *) @@ -2377,6 +2379,7 @@ lemma vcpu_switch_ccorres_Some: and valid_arch_state' and vcpu_at' v) (UNIV \ {s. new_' s = vcpu_Ptr v}) hs (vcpuSwitch (Some v)) (Call vcpu_switch_'proc)" + supply if_cong[cong] option.case_cong[cong] apply (cinit lift: new_') (* v \ None *) apply simp @@ -3198,6 +3201,7 @@ lemma ccorres_return_void_C': lemma is_aligned_cache_preconds: "\is_aligned rva n; n \ 7\ \ rva \ rva + 0x7F \ addrFromPPtr rva \ addrFromPPtr rva + 0x7F \ rva && mask 6 = addrFromPPtr rva && mask 6" + supply if_cong[cong] apply (drule is_aligned_weaken, simp) apply (rule conjI) apply (drule is_aligned_no_overflow, simp, unat_arith)[1] @@ -3948,37 +3952,38 @@ lemma makeUserPDE_spec: HAP_CL = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), MemAttr_CL = memattr_from_cacheable (to_bool \<^bsup>s\<^esup>cacheable) \) \" + supply if_cong[cong] apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: hap_from_vm_rights_mask split: if_splits) apply (intro conjI impI allI | clarsimp )+ apply (simp only: pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def - Kernel_C.ARMLargePage_def) + Kernel_C.ARMLargePage_def) apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def - split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) + split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) apply (simp only: pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def - Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq) - apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def - split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) + Kernel_C.ARMLargePage_def) + apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def + split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) apply (clarsimp) apply (intro conjI impI allI) apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) apply (drule is_aligned_weaken[where y = 21]) apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def - Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ + Kernel_C.ARMLargePage_def)+ apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) apply (drule is_aligned_weaken[where y = 21]) apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def - Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ - apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def - split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) + Kernel_C.ARMLargePage_def)+ + apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def + split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) done lemma makeUserPTE_spec: