diff --git a/docs/setup.md b/docs/setup.md index d477d7b9ab..29abf3de03 100644 --- a/docs/setup.md +++ b/docs/setup.md @@ -91,12 +91,13 @@ pip3 install --user sel4-deps After installing [haskell-stack](https://docs.haskellstack.org/en/stable/) (already included in the packages above on Mac and Ubuntu), make sure you've -adjusted your `PATH` to include `$HOME/.local/bin`, and that you're running an -up-to-date version: +adjusted your `PATH` to include `$HOME/.local/bin`, that you're running an +up-to-date version, and that you have installed cabal: ```bash stack upgrade --binary-only which stack # should be $HOME/.local/bin/stack +stack install cabal-install ``` ## Checking out the repository collection diff --git a/lib/Monads/NonDetMonadVCG.thy b/lib/Monads/NonDetMonadVCG.thy index 2cc8f4ed47..189bdff69e 100644 --- a/lib/Monads/NonDetMonadVCG.thy +++ b/lib/Monads/NonDetMonadVCG.thy @@ -306,6 +306,8 @@ lemma hoare_gen_asm: "(P \ \P'\ f \Q\) \ \P' and K P\ f \Q\" by (fastforce simp add: valid_def) +lemmas hoare_gen_asm_single = hoare_gen_asm[where P'="\", simplified pred_conj_def simp_thms] + lemma hoare_gen_asm_lk: "(P \ \P'\ f \Q\) \ \K P and P'\ f \Q\" by (fastforce simp add: valid_def) diff --git a/lib/Monads/OptionMonadWP.thy b/lib/Monads/OptionMonadWP.thy index d64169548f..2d60bc52d2 100644 --- a/lib/Monads/OptionMonadWP.thy +++ b/lib/Monads/OptionMonadWP.thy @@ -21,8 +21,10 @@ begin TODO: design a sensible syntax for them. *) (* Partial correctness. *) -definition ovalid :: "('s \ bool) \ ('s \ 'a option) \ ('a \ 's \ bool) \ bool" where - "ovalid P f Q \ \s r. P s \ f s = Some r \ Q r s" +definition ovalid :: "('s \ bool) \ ('s \ 'a option) \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /\_\") where + "\P\ f \Q\ \ \s r. P s \ f s = Some r \ Q r s" + (* Total correctness. *) definition ovalidNF :: "('s \ bool) \ ('s \ 'a option) \ ('a \ 's \ bool) \ bool" where "ovalidNF P f Q \ \s. P s \ (f s \ None \ (\r. f s = Some r \ Q r s))" @@ -57,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric] (* WP rules for ovalid. *) +lemma ovalid_inv[wp]: + "ovalid P f (\_. P)" + by (simp add: ovalid_def) + lemma obind_wp[wp]: "\ \r. ovalid (R r) (g r) Q; ovalid P f R \ \ ovalid P (obind f g) Q" by (simp add: ovalid_def obind_def split: option.splits, fast) diff --git a/lib/Monads/WhileLoopRules.thy b/lib/Monads/WhileLoopRules.thy index e83507f53b..a7c2c7f7e5 100644 --- a/lib/Monads/WhileLoopRules.thy +++ b/lib/Monads/WhileLoopRules.thy @@ -383,6 +383,22 @@ lemma whileLoop_wp: \ I r \ whileLoop C B r \ Q \" by (rule valid_whileLoop) +lemma whileLoop_valid_inv: + "(\r. \ \s. I r s \ C r s \ B r \ I \) \ \ I r \ whileLoop C B r \ I \" + apply (fastforce intro: whileLoop_wp) + done + +lemma valid_whileLoop_cond_fail: + assumes pre_implies_post: "\s. P r s \ Q r s" + and pre_implies_fail: "\s. P r s \ \ C r s" + shows "\ P r \ whileLoop C B r \ Q \" + using assms + apply (clarsimp simp: valid_def) + apply (subst (asm) whileLoop_cond_fail) + apply blast + apply (clarsimp simp: return_def) + done + lemma whileLoop_wp_inv [wp]: "\ \r. \\s. I r s \ C r s\ B r \I\; \r s. \I r s; \ C r s\ \ Q r s \ \ \ I r \ whileLoop_inv C B r I M \ Q \" diff --git a/lib/clib/CCorres_Rewrite.thy b/lib/clib/CCorres_Rewrite.thy index 86455e345b..6fd0f053f7 100644 --- a/lib/clib/CCorres_Rewrite.thy +++ b/lib/clib/CCorres_Rewrite.thy @@ -17,7 +17,7 @@ lemma ccorres_com_eq_hom: elim: ccorres_semantic_equivD2) method ccorres_rewrite declares C_simp C_simp_pre C_simp_simps C_simp_throws - = simpl_rewrite hom: ccorres_com_eq_hom + = (simpl_rewrite hom: ccorres_com_eq_hom, no_name_eta) lemma hoarep_com_eq_hom: "com_eq_hom \ (\c. hoarep \ {} F P c Q A)" diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy index 240640c2fd..516e609e78 100644 --- a/proof/crefine/ARM/Arch_C.thy +++ b/proof/crefine/ARM/Arch_C.thy @@ -397,7 +397,9 @@ shows apply (rule ccorres_rhs_assoc2) apply (rule ccorres_abstract_cleanup) apply (rule ccorres_symb_exec_l) - apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm) + apply (rename_tac pcap) + apply (rule_tac P = "pcap = (capability.UntypedCap isdev frame pageBits idx)" + in ccorres_gen_asm) apply (simp add: hrs_htd_update del:fun_upd_apply) apply (rule ccorres_split_nothrow) @@ -1466,13 +1468,13 @@ lemma pdeCheckIfMapped_ccorres: (Call pdeCheckIfMapped_'proc)" apply (cinit lift: pde___ptr_to_struct_pde_C_') apply (rule ccorres_pre_getObject_pde) - apply (rule_tac P'="{s. \pde'. cslift s (pde_Ptr slot) = Some pde' \ cpde_relation rv pde'}" + apply (rule_tac P'="{s. \pde'. cslift s (pde_Ptr slot) = Some pde' \ cpde_relation pd pde'}" in ccorres_from_vcg_throws[where P="\s. True"]) apply simp_all apply clarsimp apply (rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps' return_def) - apply (case_tac rv, simp_all add: cpde_relation_invalid isInvalidPDE_def + apply (case_tac pd, simp_all add: cpde_relation_invalid isInvalidPDE_def split: if_split) done @@ -1793,7 +1795,7 @@ lemma performPageInvocationMapPDE_ccorres: apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def) apply vcg apply simp - apply (wp valid_pde_slots_lift2) + apply (wpsimp wp: valid_pde_slots_lift2) apply clarsimp apply (clarsimp simp: pde_range_relation_def ptr_range_to_list_def) apply (rule order_less_le_trans) diff --git a/proof/crefine/ARM/CSpace_C.thy b/proof/crefine/ARM/CSpace_C.thy index 1d74e44102..a928638687 100644 --- a/proof/crefine/ARM/CSpace_C.thy +++ b/proof/crefine/ARM/CSpace_C.thy @@ -770,7 +770,7 @@ lemma update_freeIndex': supply if_cong[cong] apply (cinit lift: cap_ptr_' v32_') apply (rule ccorres_pre_getCTE) - apply (rule_tac P="\s. ctes_of s srcSlot = Some rv \ (\i. cteCap rv = UntypedCap d p sz i)" + apply (rule_tac P="\s. ctes_of s srcSlot = Some cte \ (\i. cteCap cte = UntypedCap d p sz i)" in ccorres_from_vcg[where P' = UNIV]) apply (rule allI) apply (rule conseqPre) @@ -2055,8 +2055,7 @@ lemma emptySlot_ccorres: apply csymbr apply (rule ccorres_move_c_guard_cte) \ \--- instruction y \ updateMDB slot (\a. nullMDBNode);\ - apply (ctac (no_vcg) - add: ccorres_updateMDB_const [unfolded const_def]) + apply (ctac (no_vcg) add: ccorres_updateMDB_const) \ \the post_cap_deletion case\ @@ -2132,7 +2131,7 @@ lemma capSwapForDelete_ccorres: \ \--- instruction: when (slot1 \ slot2) \ / IF Ptr slot1 = Ptr slot2 THEN \\ apply (simp add:when_def) apply (rule ccorres_if_cond_throws2 [where Q = \ and Q' = \]) - apply (case_tac "slot1=slot2", simp+) + apply (case_tac "slot1=slot2"; simp) apply (rule ccorres_return_void_C) \ \***Main goal***\ diff --git a/proof/crefine/ARM/Finalise_C.thy b/proof/crefine/ARM/Finalise_C.thy index 4ac20f6165..b72f830bd7 100644 --- a/proof/crefine/ARM/Finalise_C.thy +++ b/proof/crefine/ARM/Finalise_C.thy @@ -277,10 +277,10 @@ lemma cancelAllIPC_ccorres: apply (cinit lift: epptr_') apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) apply (rule_tac xf'=ret__unsigned_' - and val="case rv of IdleEP \ scast EPState_Idle + and val="case ep of IdleEP \ scast EPState_Idle | RecvEP _ \ scast EPState_Recv | SendEP _ \ scast EPState_Send" - and R="ko_at' rv epptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ep epptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ep]) @@ -289,8 +289,8 @@ lemma cancelAllIPC_ccorres: apply (simp add: cendpoint_relation_def Let_def split: endpoint.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv epptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ep epptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (rename_tac list) apply (simp add: endpoint_state_defs @@ -404,10 +404,10 @@ lemma cancelAllSignals_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac xf'=ret__unsigned_' - and val="case ntfnObj rv of IdleNtfn \ scast NtfnState_Idle + and val="case ntfnObj ntfn of IdleNtfn \ scast NtfnState_Idle | ActiveNtfn _ \ scast NtfnState_Active | WaitingNtfn _ \ scast NtfnState_Waiting" - and R="ko_at' rv ntfnptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ntfn ntfnptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) @@ -416,8 +416,8 @@ lemma cancelAllSignals_ccorres: apply (simp add: cnotification_relation_def Let_def split: ntfn.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv ntfnptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ntfn ntfnptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (simp add: notification_state_defs ccorres_cond_iffs) apply (rule ccorres_return_Skip) @@ -432,8 +432,8 @@ lemma cancelAllSignals_ccorres: apply csymbr apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule_tac P="ko_at' rv ntfnptr and invs'" - in ccorres_from_vcg[where P'=UNIV]) + apply (rule_tac P="ko_at' ntfn ntfnptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) @@ -643,8 +643,8 @@ lemma doUnbindNotification_ccorres: (Call doUnbindNotification_'proc)" apply (cinit' lift: ntfnPtr_' tcbptr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV - in ccorres_split_nothrow_novcg) + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_to_ptr_def option_to_0_def) @@ -663,7 +663,7 @@ lemma doUnbindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) + apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4]) subgoal by (simp add: carch_state_relation_def typ_heap_simps') subgoal by (simp add: cmachine_state_relation_def) subgoal by (simp add: h_t_valid_clift_Some_iff) @@ -778,13 +778,13 @@ lemma unbindMaybeNotification_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) - apply (rule_tac P="ntfnBoundTCB rv \ None \ - option_to_ctcb_ptr (ntfnBoundTCB rv) \ NULL" - in ccorres_gen_asm) + apply (rule_tac P="ntfnBoundTCB ntfn \ None \ + option_to_ctcb_ptr (ntfnBoundTCB ntfn) \ NULL" + in ccorres_gen_asm) apply (rule_tac xf'=boundTCB_' - and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" - and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)" + and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1[OF cmap_relation_ntfn]) diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy index 5940149186..1d4e0ff3eb 100644 --- a/proof/crefine/ARM/Invoke_C.thy +++ b/proof/crefine/ARM/Invoke_C.thy @@ -65,7 +65,7 @@ lemma setDomain_ccorres: apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply (simp add: when_def) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. curThread = ksCurThread s" in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) @@ -76,14 +76,16 @@ lemma setDomain_ccorres: apply simp apply wp apply (rule_tac Q="\_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s)" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s)" + in hoare_strengthen_post) apply (wp threadSet_all_invs_but_sch_extra) apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric] sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" + in hoare_strengthen_post) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) @@ -619,7 +621,7 @@ 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] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add:if_P del: Collect_const) @@ -1089,7 +1091,7 @@ lemma decodeCNodeInvocation_ccorres: apply (simp add: throwError_def return_def exception_defs syscall_error_rel_def syscall_error_to_H_cases) apply clarsimp - apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const) apply csymbr apply (simp add: interpret_excaps_test_null excaps_map_def diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy index 271211851b..2867a8d91c 100644 --- a/proof/crefine/ARM/Ipc_C.thy +++ b/proof/crefine/ARM/Ipc_C.thy @@ -2951,9 +2951,10 @@ proof - del: Collect_const) apply csymbr apply (rename_tac "lngth") - apply (simp add: mi_from_H_def mapME_def del: Collect_const cong: bind_apply_cong) + apply (unfold mapME_def)[1] + apply (simp add: mi_from_H_def del: Collect_const) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="length rv = unat word2" in ccorres_gen_asm) + apply (rule_tac P="length xs = unat word2" in ccorres_gen_asm) apply csymbr apply (rule ccorres_rhs_assoc2) apply (rule ccorres_add_returnOk2, @@ -2963,7 +2964,7 @@ proof - and Q="UNIV" and F="\n s. valid_pspace' s \ tcb_at' thread s \ (case buffer of Some x \ valid_ipc_buffer_ptr' x | _ \ \) s \ - (\m < length rv. user_word_at (rv ! m) + (\m < length xs. user_word_at (xs ! m) (x2 + (of_nat m + (msgMaxLength + 2)) * 4) s)" in ccorres_sequenceE_while') apply (simp add: split_def) @@ -2973,7 +2974,7 @@ proof - apply (rule_tac xf'=cptr_' in ccorres_abstract, ceqv) apply (ctac add: capFaultOnFailure_ccorres [OF lookupSlotForThread_ccorres']) - apply (rule_tac P="is_aligned rva 4" in ccorres_gen_asm) + apply (rule_tac P="is_aligned rv 4" in ccorres_gen_asm) apply (simp add: ccorres_cond_iffs liftE_bindE) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_getSlotCap]) apply (rule_tac P'="UNIV \ {s. excaps_map ys @@ -2994,7 +2995,7 @@ proof - apply (clarsimp simp: ccorres_cond_iffs) apply (rule_tac P= \ and P'="{x. errstate x= lu_ret___struct_lookupSlot_raw_ret_C \ - rv' = (rv ! length ys)}" + rv' = (xs ! length ys)}" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def) @@ -3035,7 +3036,7 @@ proof - apply ceqv apply (simp del: Collect_const) apply (rule_tac P'="{s. snd rv'=?curr s}" - and P="\s. length rva = length rv \ (\x \ set rva. snd x \ 0)" + and P="\s. length rv = length xs \ (\x \ set rv. snd x \ 0)" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def @@ -3357,7 +3358,7 @@ proof - apply (rule ccorres_rhs_assoc2) apply (simp add: MessageID_Exception_def) apply ccorres_rewrite - apply (subst bind_return_unit) + apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_zipWithM_x_while) apply clarsimp diff --git a/proof/crefine/ARM/Recycle_C.thy b/proof/crefine/ARM/Recycle_C.thy index 697875e0dd..f3f5c1cda7 100644 --- a/proof/crefine/ARM/Recycle_C.thy +++ b/proof/crefine/ARM/Recycle_C.thy @@ -583,8 +583,8 @@ lemma cancelBadgedSends_ccorres: cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong del: Collect_const) apply (rule ccorres_pre_getEndpoint) - apply (rule_tac R="ko_at' rv ptr" and xf'="ret__unsigned_'" - and val="case rv of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle + apply (rule_tac R="ko_at' ep ptr" and xf'="ret__unsigned_'" + and val="case ep of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle | SendEP q \ scast EPState_Send" in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg @@ -604,12 +604,12 @@ lemma cancelBadgedSends_ccorres: del: Collect_const cong: call_ignore_cong) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr) - apply (drule_tac s = rv in sym, simp only:) - apply (rule_tac P="ko_at' rv ptr and invs'" in ccorres_cross_over_guard) + apply (drule_tac s = ep in sym, simp only:) + apply (rule_tac P="ko_at' ep ptr and invs'" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]) - apply (rule_tac P="ko_at' rv ptr" + apply (rule_tac P="ko_at' ep ptr" in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp @@ -719,7 +719,7 @@ lemma cancelBadgedSends_ccorres: subgoal by (simp add: rf_sr_def) apply simp apply ceqv - apply (rule_tac P="ret__unsigned=blockingIPCBadge rva" in ccorres_gen_asm2) + apply (rule_tac P="ret__unsigned=blockingIPCBadge rv" in ccorres_gen_asm2) apply (rule ccorres_if_bind, rule ccorres_if_lhs) apply (simp add: bind_assoc) apply (rule ccorres_rhs_assoc)+ diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy index d5f84263fc..79c7abffb1 100644 --- a/proof/crefine/ARM/Retype_C.thy +++ b/proof/crefine/ARM/Retype_C.thy @@ -3638,17 +3638,17 @@ lemma copyGlobalMappings_ccorres: apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState) apply csymbr apply (rule ccorres_rel_imp) - apply (rule_tac F="\_ s. rv = armKSGlobalPD (ksArchState s) - \ is_aligned rv pdBits \ valid_pde_mappings' s + apply (rule_tac F="\_ s. globalPD = armKSGlobalPD (ksArchState s) + \ is_aligned globalPD pdBits \ valid_pde_mappings' s \ page_directory_at' pd s \ page_directory_at' (armKSGlobalPD (ksArchState s)) s" - and i="0xE00" - in ccorres_mapM_x_while') + and i="0xE00" + in ccorres_mapM_x_while') apply (clarsimp simp del: Collect_const) apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getObject_pde) apply (simp add: storePDE_def del: Collect_const) - apply (rule_tac P="\s. ko_at' rva (armKSGlobalPD (ksArchState s) + apply (rule_tac P="\s. ko_at' rv (armKSGlobalPD (ksArchState s) + ((0xE00 + of_nat n) << 2)) s \ page_directory_at' pd s \ valid_pde_mappings' s \ page_directory_at' (armKSGlobalPD (ksArchState s)) s" @@ -3663,7 +3663,7 @@ lemma copyGlobalMappings_ccorres: apply (rule cmap_relationE1[OF rf_sr_cpde_relation], assumption, erule_tac ko=ko' in ko_at_projectKO_opt) apply (rule cmap_relationE1[OF rf_sr_cpde_relation], - assumption, erule_tac ko=rva in ko_at_projectKO_opt) + assumption, erule_tac ko=rv in ko_at_projectKO_opt) apply (clarsimp simp: typ_heap_simps') apply (drule(1) page_directory_at_rf_sr)+ apply clarsimp diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index cb1fe7a009..2b2013a989 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -755,11 +755,13 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_move_c_guard_tcb_ctes)+ apply (ctac (no_vcg)) + apply (rename_tac bufferCap bufferCap') apply csymbr - apply (rule_tac b="isArchObjectCap rva \ isPageCap (capCap rva)" in ccorres_case_bools') + apply (rule_tac b="isArchObjectCap bufferCap \ isPageCap (capCap bufferCap)" + in ccorres_case_bools') apply simp apply (rule ccorres_symb_exec_r) - apply (rule_tac b="capVPSize (capCap rva) \ ARMSmallPage" in ccorres_case_bools') + apply (rule_tac b="capVPSize (capCap bufferCap) \ ARMSmallPage" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_rhs_assoc)+ apply csymbr @@ -767,7 +769,7 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap bufferCap" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg @@ -821,7 +823,7 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap bufferCap" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy index 986f148b55..99f8eb0707 100644 --- a/proof/crefine/ARM/Syscall_C.thy +++ b/proof/crefine/ARM/Syscall_C.thy @@ -1203,7 +1203,7 @@ lemma handleRecv_ccorres: apply (simp add: liftE_bind) apply (ctac) - apply (rule_tac P="\s. ksCurThread s = rv" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ksCurThread s = thread" in ccorres_cross_over_guard) apply (ctac add: receiveIPC_ccorres) apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 4b49c16ebc..d69234ed5b 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -399,7 +399,7 @@ lemma setPriority_ccorres: apply (frule (1) valid_objs'_maxDomain[where t=t]) apply (frule (1) valid_objs'_maxPriority[where t=t]) apply simp -done + done lemma setMCPriority_ccorres: "ccorres dc xfdc @@ -1139,10 +1139,10 @@ lemma invokeTCB_CopyRegisters_ccorres: apply (simp add: word_bits_def frame_gp_registers_convs n_gpRegisters_def) apply simp apply (rule ccorres_pre_getCurThread) + apply (rename_tac thread) apply (ctac add: postModifyRegisters_ccorres[simplified]) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rvd = ksCurThread s" - in ccorres_when) + apply (rule_tac R="\s. thread = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp apply (ctac (no_vcg) add: rescheduleRequired_ccorres) @@ -1550,8 +1550,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: apply simp apply (rule ceqv_refl) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rv = ksCurThread s" - in ccorres_when) + apply (rule_tac R="\s. self = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp apply (ctac (no_vcg) add: rescheduleRequired_ccorres) @@ -2020,7 +2019,7 @@ shows apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size word_less_nat_alt split: if_split_asm dest!: word_unat.Rep_inverse') - apply simp + apply (simp add: pred_conj_def) apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp tcb_in_cur_domain'_lift) apply (simp add: n_frameRegisters_def n_msgRegisters_def @@ -2152,7 +2151,8 @@ lemma decodeReadRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2163,13 +2163,13 @@ lemma decodeReadRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2263,7 +2263,8 @@ lemma decodeWriteRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2274,13 +2275,13 @@ lemma decodeWriteRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2566,7 +2567,7 @@ lemma slotCapLongRunningDelete_ccorres: apply (simp add: case_Null_If del: Collect_const) apply (rule ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_if_lhs) @@ -2587,7 +2588,7 @@ lemma slotCapLongRunningDelete_ccorres: apply vcg apply (simp del: Collect_const) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_from_vcg_throws[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of return_def) @@ -3714,7 +3715,7 @@ lemma bindNotification_ccorres: (Call bindNotification_'proc)" apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr and tcb_at' tcb" and P'=UNIV + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr and tcb_at' tcb" and P'=UNIV in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) @@ -3734,7 +3735,7 @@ lemma bindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv") + apply (case_tac "ntfnObj ntfn") apply (auto simp: option_to_ctcb_ptr_def obj_at'_def objBits_simps projectKOs bindNTFN_alignment_junk)[4] apply (simp add: carch_state_relation_def typ_heap_simps') @@ -3812,7 +3813,7 @@ lemma decodeUnbindNotification_ccorres: apply (rule ccorres_Guard_Seq) apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getBoundNotification) - apply (rule_tac P="\s. rv \ Some 0" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ntfn \ Some 0" in ccorres_cross_over_guard) apply (simp add: bindE_bind_linearise) apply wpc apply (simp add: bindE_bind_linearise[symmetric] diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy index 296aff8a69..d1ac6f07f7 100644 --- a/proof/crefine/ARM/VSpace_C.thy +++ b/proof/crefine/ARM/VSpace_C.thy @@ -171,7 +171,7 @@ lemma loadHWASID_ccorres: apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_gets]) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) apply (rename_tac pd) - apply (rule_tac P="\s. pd_at_asid' pd asid s \ rv = armKSASIDMap (ksArchState s) + apply (rule_tac P="\s. pd_at_asid' pd asid s \ asidMap = armKSASIDMap (ksArchState s) \ pd \ ran (option_map snd o armKSASIDMap (ksArchState s) |` (- {asid})) \ option_map snd (armKSASIDMap (ksArchState s) asid) \ {None, Some pd} @@ -746,7 +746,7 @@ lemma lookupPTSlot_ccorres: apply csymbr apply csymbr apply (rule ccorres_abstract_cleanup) - apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE rv)" + apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE pde)" in ccorres_gen_asm2) apply (rule ccorres_cond2'[where R=\]) apply (clarsimp simp: Collect_const_mem) @@ -761,9 +761,10 @@ lemma lookupPTSlot_ccorres: apply (simp add: checkPTAt_def bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) apply (rule ccorres_stateAssert) - apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable rv)) - and ko_at' rv (lookup_pd_slot pd vptr) - and K (isPageTablePDE rv)" and P'=UNIV in ccorres_from_vcg_throws) + apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable pde)) + and ko_at' pde (lookup_pd_slot pd vptr) and K (isPageTablePDE pde)" + and P'=UNIV + in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def Collect_const_mem lookup_pd_slot_def word_sle_def) @@ -1168,15 +1169,15 @@ lemma findFreeHWASID_ccorres: apply (rule_tac xf=hw_asid_offset_' and i=0 and xf_update=hw_asid_offset_'_update and r'=dc and xf'=xfdc and Q=UNIV - and F="\n s. rv = armKSHWASIDTable (ksArchState s) - \ nextASID = armKSNextASID (ksArchState s) - \ valid_arch_state' s" + and F="\n s. hwASIDTable = armKSHWASIDTable (ksArchState s) + \ nextASID = armKSNextASID (ksArchState s) + \ valid_arch_state' s" in ccorres_sequenceE_while_gen') apply (rule ccorres_from_vcg_might_throw) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: rf_sr_armKSNextASID) apply (subst down_cast_same [symmetric], - simp add: is_down_def target_size_def source_size_def word_size)+ + simp add: is_down_def target_size_def source_size_def word_size)+ apply (simp add: ucast_ucast_mask ucast_ucast_add ucast_and_mask ucast_of_nat_small asidInvalid_def @@ -1214,7 +1215,7 @@ lemma findFreeHWASID_ccorres: apply ceqv apply (rule ccorres_assert) apply (rule_tac A="\s. nextASID = armKSNextASID (ksArchState s) - \ rv = armKSHWASIDTable (ksArchState s) + \ hwASIDTable = armKSHWASIDTable (ksArchState s) \ valid_arch_state' s \ valid_pde_mappings' s" in ccorres_guard_imp2[where A'=UNIV]) apply (simp add: split_def) @@ -1360,7 +1361,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armKSGlobalPD) apply csymbr - apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentPD_ccorres) apply (rule ccorres_split_throws) @@ -1380,7 +1381,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armKSGlobalPD) apply csymbr - apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentPD_ccorres) apply (rule ccorres_split_throws) @@ -1409,7 +1410,7 @@ lemma setVMRoot_ccorres: apply (simp add: whenE_def throwError_def checkPDNotInASIDMap_def checkPDASIDMapMembership_def) apply (rule ccorres_stateAssert) - apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState[unfolded o_def]) + apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armKSGlobalPD) apply csymbr @@ -1424,7 +1425,7 @@ lemma setVMRoot_ccorres: apply (simp add: checkPDNotInASIDMap_def checkPDASIDMapMembership_def) apply (rule ccorres_stateAssert) apply (rule ccorres_rhs_assoc)+ - apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState[unfolded o_def]) + apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState) apply (rule ccorres_h_t_valid_armKSGlobalPD) apply csymbr apply (rule ccorres_add_return2) @@ -1476,9 +1477,9 @@ lemma setVMRootForFlush_ccorres: del: Collect_const) apply (rule ccorres_if_lhs) apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) - = (capPDMappedASID (capCap rva) = None) + = (capPDMappedASID (capCap rv) = None) \ capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) - = capPDBasePtr (capCap rva)" in ccorres_gen_asm2) + = capPDBasePtr (capCap rv)" in ccorres_gen_asm2) apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+ apply (rule ccorres_split_throws) apply (rule ccorres_return_C, simp+) @@ -1685,7 +1686,7 @@ lemma setRegister_ccorres: apply (rule ccorres_pre_threadGet) apply (rule ccorres_Guard) apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) - apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = rv" + apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = uc" in threadSet_ccorres_lemma2) apply vcg apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def @@ -2233,9 +2234,7 @@ lemma unmapPage_ccorres: \ \ARMSection\ apply (rule ccorres_Cond_rhs) apply (rule ccorres_rhs_assoc)+ - \ \FIXME: The second csymbr rewrites the return relation of the goal. - If this was avoided then folding the dc_def could be removed\ - apply (csymbr, csymbr, fold dc_def) + apply (csymbr, csymbr) apply (simp add: gen_framesize_to_H_def liftE_liftM del: Collect_const) apply (simp split: if_split, rule conjI[rotated], rule impI, @@ -2267,12 +2266,9 @@ lemma unmapPage_ccorres: \ \ARMSuperSection\ apply (rule ccorres_Cond_rhs) apply (rule ccorres_rhs_assoc)+ - \ \FIXME: The third csymbr rewrites the return relation of the goal. - If this was avoided then folding the dc_def could be removed\ apply csymbr apply csymbr apply csymbr - apply (fold dc_def) apply (case_tac "pd = pde_Ptr (lookup_pd_slot pdPtr vptr)") prefer 2 apply (simp, rule ccorres_empty) @@ -2885,13 +2881,13 @@ lemma performASIDPoolInvocation_ccorres: apply (rule ccorres_rhs_assoc2) apply (rule_tac ccorres_split_nothrow [where r'=dc and xf'=xfdc]) apply (simp add: updateCap_def) - apply (rule_tac A="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPDCap rv \ asid \ mask asid_bits)" + apply (rule_tac A="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPDCap oldcap \ asid \ mask asid_bits)" and A'=UNIV in ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) - apply (rule_tac P="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPDCap rv \ asid \ mask asid_bits) - and cte_wp_at' ((=) rva) ctSlot" + apply (rule_tac P="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPDCap oldcap \ asid \ mask asid_bits) + and cte_wp_at' ((=) rv) ctSlot" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of) diff --git a/proof/crefine/ARM_HYP/Arch_C.thy b/proof/crefine/ARM_HYP/Arch_C.thy index 3a431a7ec9..f651380021 100644 --- a/proof/crefine/ARM_HYP/Arch_C.thy +++ b/proof/crefine/ARM_HYP/Arch_C.thy @@ -438,7 +438,9 @@ shows apply (rule ccorres_rhs_assoc2) apply (rule ccorres_abstract_cleanup) apply (rule ccorres_symb_exec_l) - apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm) + apply (rename_tac pcap) + apply (rule_tac P = "pcap = (capability.UntypedCap isdev frame pageBits idx)" + in ccorres_gen_asm) apply (simp add: hrs_htd_update del:fun_upd_apply) apply (rule ccorres_split_nothrow) @@ -1497,13 +1499,13 @@ lemma pdeCheckIfMapped_ccorres: (Call pdeCheckIfMapped_'proc)" apply (cinit lift: pde___ptr_to_struct_pde_C_') apply (rule ccorres_pre_getObject_pde) - apply (rule_tac P'="{s. \pde'. cslift s (pde_Ptr slot) = Some pde' \ cpde_relation rv pde'}" + apply (rule_tac P'="{s. \pde'. cslift s (pde_Ptr slot) = Some pde' \ cpde_relation pd pde'}" in ccorres_from_vcg_throws[where P="\s. True"]) apply simp_all apply clarsimp apply (rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps' return_def) - apply (case_tac rv, simp_all add: cpde_relation_invalid isInvalidPDE_def + apply (case_tac pd, simp_all add: cpde_relation_invalid isInvalidPDE_def split: if_split) done @@ -2379,9 +2381,9 @@ lemma setVMRootForFlush_ccorres2: del: Collect_const) apply (rule ccorres_if_lhs) apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) - = (capPDMappedASID (capCap rva) = None) + = (capPDMappedASID (capCap rv) = None) \ capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) - = capPDBasePtr (capCap rva)" in ccorres_gen_asm2) + = capPDBasePtr (capCap rv)" in ccorres_gen_asm2) apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+ apply (rule ccorres_split_throws) apply (rule ccorres_return_C, simp+) @@ -4745,7 +4747,7 @@ lemma decodeVCPUInjectIRQ_ccorres: liftE_liftM[symmetric] liftE_bindE_assoc) (* symbolically execute the gets on LHS *) - apply (rule_tac ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState[simplified comp_def], + apply (rule_tac ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState, rename_tac nregs) (* unfortunately directly looking at \gic_vcpu_num_list_regs means we need to abstract the IF condition*) diff --git a/proof/crefine/ARM_HYP/CSpace_C.thy b/proof/crefine/ARM_HYP/CSpace_C.thy index 8d7aeb87b7..071f24ae7d 100644 --- a/proof/crefine/ARM_HYP/CSpace_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_C.thy @@ -796,7 +796,7 @@ lemma update_freeIndex': show ?thesis apply (cinit lift: cap_ptr_' v32_') apply (rule ccorres_pre_getCTE) - apply (rule_tac P="\s. ctes_of s srcSlot = Some rv \ (\i. cteCap rv = UntypedCap d p sz i)" + apply (rule_tac P="\s. ctes_of s srcSlot = Some cte \ (\i. cteCap cte = UntypedCap d p sz i)" in ccorres_from_vcg[where P' = UNIV]) apply (rule allI) apply (rule conseqPre) @@ -2552,7 +2552,7 @@ lemma capSwapForDelete_ccorres: \ \--- instruction: when (slot1 \ slot2) \ / IF Ptr slot1 = Ptr slot2 THEN \\ apply (simp add:when_def) apply (rule ccorres_if_cond_throws2 [where Q = \ and Q' = \]) - apply (case_tac "slot1=slot2", simp+) + apply (case_tac "slot1=slot2"; simp) apply (rule ccorres_return_void_C) \ \***Main goal***\ diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy index 765e53e324..732f2318b7 100644 --- a/proof/crefine/ARM_HYP/Finalise_C.thy +++ b/proof/crefine/ARM_HYP/Finalise_C.thy @@ -277,10 +277,10 @@ lemma cancelAllIPC_ccorres: apply (cinit lift: epptr_') apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) apply (rule_tac xf'=ret__unsigned_' - and val="case rv of IdleEP \ scast EPState_Idle + and val="case ep of IdleEP \ scast EPState_Idle | RecvEP _ \ scast EPState_Recv | SendEP _ \ scast EPState_Send" - and R="ko_at' rv epptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ep epptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ep]) @@ -289,8 +289,8 @@ lemma cancelAllIPC_ccorres: apply (simp add: cendpoint_relation_def Let_def split: endpoint.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv epptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ep epptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (rename_tac list) apply (simp add: endpoint_state_defs @@ -404,10 +404,10 @@ lemma cancelAllSignals_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac xf'=ret__unsigned_' - and val="case ntfnObj rv of IdleNtfn \ scast NtfnState_Idle + and val="case ntfnObj ntfn of IdleNtfn \ scast NtfnState_Idle | ActiveNtfn _ \ scast NtfnState_Active | WaitingNtfn _ \ scast NtfnState_Waiting" - and R="ko_at' rv ntfnptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ntfn ntfnptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) @@ -416,8 +416,8 @@ lemma cancelAllSignals_ccorres: apply (simp add: cnotification_relation_def Let_def split: ntfn.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv ntfnptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ntfn ntfnptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (simp add: notification_state_defs ccorres_cond_iffs) apply (rule ccorres_return_Skip) @@ -432,8 +432,8 @@ lemma cancelAllSignals_ccorres: apply csymbr apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule_tac P="ko_at' rv ntfnptr and invs'" - in ccorres_from_vcg[where P'=UNIV]) + apply (rule_tac P="ko_at' ntfn ntfnptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) @@ -677,8 +677,8 @@ lemma doUnbindNotification_ccorres: (Call doUnbindNotification_'proc)" apply (cinit' lift: ntfnPtr_' tcbptr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV - in ccorres_split_nothrow_novcg) + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_to_ptr_def option_to_0_def) @@ -697,7 +697,7 @@ lemma doUnbindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) + apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4]) subgoal by (simp add: carch_state_relation_def typ_heap_simps') subgoal by (simp add: cmachine_state_relation_def) subgoal by (simp add: h_t_valid_clift_Some_iff) @@ -812,13 +812,13 @@ lemma unbindMaybeNotification_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) - apply (rule_tac P="ntfnBoundTCB rv \ None \ - option_to_ctcb_ptr (ntfnBoundTCB rv) \ NULL" - in ccorres_gen_asm) + apply (rule_tac P="ntfnBoundTCB ntfn \ None \ + option_to_ctcb_ptr (ntfnBoundTCB ntfn) \ NULL" + in ccorres_gen_asm) apply (rule_tac xf'=boundTCB_' - and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" - and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)" + and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1[OF cmap_relation_ntfn]) diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy index 49d9acff6c..7b2e2fb0cd 100644 --- a/proof/crefine/ARM_HYP/Invoke_C.thy +++ b/proof/crefine/ARM_HYP/Invoke_C.thy @@ -65,7 +65,7 @@ lemma setDomain_ccorres: apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply (simp add: when_def) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. curThread = ksCurThread s" in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) @@ -76,14 +76,16 @@ lemma setDomain_ccorres: apply simp apply wp apply (rule_tac Q="\_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s)" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s)" + in hoare_strengthen_post) apply (wp threadSet_all_invs_but_sch_extra) apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric] sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" + in hoare_strengthen_post) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) @@ -638,7 +640,7 @@ 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] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add:if_P del: Collect_const) @@ -1107,7 +1109,7 @@ lemma decodeCNodeInvocation_ccorres: apply (simp add: throwError_def return_def exception_defs syscall_error_rel_def syscall_error_to_H_cases) apply clarsimp - apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const) apply csymbr apply (simp add: interpret_excaps_test_null excaps_map_def diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index accb989080..0b14957378 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -3416,9 +3416,10 @@ proof - apply (rule ccorres_symb_exec_r) apply csymbr apply (rename_tac "lngth") - apply (simp add: mi_from_H_def mapME_def del: Collect_const cong: bind_apply_cong) + apply (unfold mapME_def)[1] + apply (simp add: mi_from_H_def del: Collect_const) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="length rv = unat word2" in ccorres_gen_asm) + apply (rule_tac P="length xs = unat word2" in ccorres_gen_asm) apply csymbr apply (rule ccorres_rhs_assoc2) apply (rule ccorres_add_returnOk2, @@ -3428,7 +3429,7 @@ proof - and Q="UNIV" and F="\n s. valid_pspace' s \ tcb_at' thread s \ (case buffer of Some x \ valid_ipc_buffer_ptr' x | _ \ \) s \ - (\m < length rv. user_word_at (rv ! m) + (\m < length xs. user_word_at (xs ! m) (x2 + (of_nat m + (msgMaxLength + 2)) * 4) s)" in ccorres_sequenceE_while') apply (simp add: split_def) @@ -3438,7 +3439,7 @@ proof - apply (rule_tac xf'=cptr_' in ccorres_abstract, ceqv) apply (ctac add: capFaultOnFailure_ccorres [OF lookupSlotForThread_ccorres']) - apply (rule_tac P="is_aligned rva 4" in ccorres_gen_asm) + apply (rule_tac P="is_aligned rv 4" in ccorres_gen_asm) apply (simp add: ccorres_cond_iffs liftE_bindE) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_getSlotCap]) apply (rule_tac P'="UNIV \ {s. excaps_map ys @@ -3459,7 +3460,7 @@ proof - apply (clarsimp simp: ccorres_cond_iffs) apply (rule_tac P= \ and P'="{x. errstate x= lu_ret___struct_lookupSlot_raw_ret_C \ - rv' = (rv ! length ys)}" + rv' = (xs ! length ys)}" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def) @@ -3500,8 +3501,7 @@ proof - apply ceqv apply (simp del: Collect_const) apply (rule_tac P'="{s. snd rv'=?curr s}" - and P="\s. length rva = length rv - \ (\x \ set rva. snd x \ 0)" + and P="\s. length rv = length xs \ (\x \ set rv. snd x \ 0)" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def @@ -3809,7 +3809,7 @@ lemma Arch_getSanitiseRegisterInfo_ccorres: apply (cinit' lift: thread_' simp: getSanitiseRegisterInfo_def2) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_pre_archThreadGet) - apply (rule_tac P="\s. rv \ Some 0" in ccorres_cross_over_guard) + apply (rule_tac P="\s. v \ Some 0" in ccorres_cross_over_guard) apply (rule ccorres_return_C, simp+) apply (clarsimp simp: typ_heap_simps ctcb_relation_def carch_tcb_relation_def) apply (rule conjI) @@ -3850,7 +3850,7 @@ apply (ctac(no_vcg) add: Arch_getSanitiseRegisterInfo_ccorres) apply (rule ccorres_rhs_assoc2) apply (simp add: MessageID_Exception_def) apply ccorres_rewrite - apply (subst bind_return_unit) + apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_zipWithM_x_while) apply clarsimp diff --git a/proof/crefine/ARM_HYP/Recycle_C.thy b/proof/crefine/ARM_HYP/Recycle_C.thy index 94ae29054e..995f2129e6 100644 --- a/proof/crefine/ARM_HYP/Recycle_C.thy +++ b/proof/crefine/ARM_HYP/Recycle_C.thy @@ -922,8 +922,8 @@ lemma cancelBadgedSends_ccorres: cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong del: Collect_const) apply (rule ccorres_pre_getEndpoint) - apply (rule_tac R="ko_at' rv ptr" and xf'="ret__unsigned_'" - and val="case rv of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle + apply (rule_tac R="ko_at' ep ptr" and xf'="ret__unsigned_'" + and val="case ep of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle | SendEP q \ scast EPState_Send" in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg @@ -943,12 +943,12 @@ lemma cancelBadgedSends_ccorres: del: Collect_const cong: call_ignore_cong) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr) - apply (drule_tac s = rv in sym, simp only:) - apply (rule_tac P="ko_at' rv ptr and invs'" in ccorres_cross_over_guard) + apply (drule_tac s = ep in sym, simp only:) + apply (rule_tac P="ko_at' ep ptr and invs'" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]) - apply (rule_tac P="ko_at' rv ptr" + apply (rule_tac P="ko_at' ep ptr" in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp @@ -1058,7 +1058,7 @@ lemma cancelBadgedSends_ccorres: subgoal by (simp add: rf_sr_def) apply simp apply ceqv - apply (rule_tac P="ret__unsigned=blockingIPCBadge rva" in ccorres_gen_asm2) + apply (rule_tac P="ret__unsigned=blockingIPCBadge rv" in ccorres_gen_asm2) apply (rule ccorres_if_bind, rule ccorres_if_lhs) apply (simp add: bind_assoc) apply (rule ccorres_rhs_assoc)+ diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index 300d865db5..47ff210395 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -784,11 +784,13 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_move_c_guard_tcb_ctes)+ apply (ctac (no_vcg)) + apply (rename_tac bufferCap bufferCap') apply csymbr - apply (rule_tac b="isArchObjectCap rva \ isPageCap (capCap rva)" in ccorres_case_bools') + apply (rule_tac b="isArchObjectCap bufferCap \ isPageCap (capCap bufferCap)" + in ccorres_case_bools') apply simp apply (rule ccorres_symb_exec_r) - apply (rule_tac b="capVPSize (capCap rva) \ ARMSmallPage" in ccorres_case_bools') + apply (rule_tac b="capVPSize (capCap bufferCap) \ ARMSmallPage" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_rhs_assoc)+ apply csymbr @@ -796,7 +798,7 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap bufferCap" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg @@ -850,7 +852,7 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap bufferCap" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy index 704623ad1b..8096d9e357 100644 --- a/proof/crefine/ARM_HYP/Syscall_C.thy +++ b/proof/crefine/ARM_HYP/Syscall_C.thy @@ -1315,7 +1315,7 @@ lemma handleRecv_ccorres: apply (simp add: liftE_bind) apply (ctac) - apply (rule_tac P="\s. ksCurThread s = rv" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ksCurThread s = thread" in ccorres_cross_over_guard) apply (ctac add: receiveIPC_ccorres) apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index a1eb8c980d..b2e8f2066e 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -437,7 +437,7 @@ lemma setPriority_ccorres: apply (frule (1) valid_objs'_maxDomain[where t=t]) apply (frule (1) valid_objs'_maxPriority[where t=t]) apply simp -done + done lemma setMCPriority_ccorres: "ccorres dc xfdc @@ -1200,10 +1200,10 @@ lemma invokeTCB_CopyRegisters_ccorres: apply (simp add: word_bits_def frame_gp_registers_convs n_gpRegisters_def) apply simp apply (rule ccorres_pre_getCurThread) + apply (rename_tac thread) apply (ctac add: postModifyRegisters_ccorres[simplified]) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rvd = ksCurThread s" - in ccorres_when) + apply (rule_tac R="\s. thread = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp apply (ctac (no_vcg) add: rescheduleRequired_ccorres) @@ -1624,8 +1624,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: apply simp apply (rule ceqv_refl) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rv = ksCurThread s" - in ccorres_when) + apply (rule_tac R="\s. self = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp apply (ctac (no_vcg) add: rescheduleRequired_ccorres) @@ -2100,7 +2099,7 @@ shows apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size word_less_nat_alt split: if_split_asm dest!: word_unat.Rep_inverse') - apply simp + apply (simp add: pred_conj_def) apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp tcb_in_cur_domain'_lift) apply (simp add: n_frameRegisters_def n_msgRegisters_def @@ -2223,7 +2222,8 @@ lemma decodeReadRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2234,13 +2234,13 @@ lemma decodeReadRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2334,7 +2334,8 @@ lemma decodeWriteRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2345,13 +2346,13 @@ lemma decodeWriteRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2660,7 +2661,7 @@ lemma slotCapLongRunningDelete_ccorres: apply (simp add: case_Null_If del: Collect_const) apply (rule ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_if_lhs) @@ -2681,7 +2682,7 @@ lemma slotCapLongRunningDelete_ccorres: apply vcg apply (simp del: Collect_const) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_from_vcg_throws[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of return_def) @@ -3801,7 +3802,7 @@ lemma bindNotification_ccorres: (Call bindNotification_'proc)" apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr and tcb_at' tcb" and P'=UNIV + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr and tcb_at' tcb" and P'=UNIV in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) @@ -3821,7 +3822,7 @@ lemma bindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv") + apply (case_tac "ntfnObj ntfn") apply (auto simp: option_to_ctcb_ptr_def obj_at'_def objBits_simps projectKOs bindNTFN_alignment_junk)[4] apply (simp add: carch_state_relation_def typ_heap_simps') @@ -3899,7 +3900,7 @@ lemma decodeUnbindNotification_ccorres: apply (rule ccorres_Guard_Seq) apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getBoundNotification) - apply (rule_tac P="\s. rv \ Some 0" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ntfn \ Some 0" in ccorres_cross_over_guard) apply (simp add: bindE_bind_linearise) apply wpc apply (simp add: bindE_bind_linearise[symmetric] diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy index a0126fb016..293d0f7b2c 100644 --- a/proof/crefine/ARM_HYP/VSpace_C.thy +++ b/proof/crefine/ARM_HYP/VSpace_C.thy @@ -262,7 +262,7 @@ lemma loadHWASID_ccorres: apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_gets]) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) apply (rename_tac pd) - apply (rule_tac P="\s. pd_at_asid' pd asid s \ rv = armKSASIDMap (ksArchState s) + apply (rule_tac P="\s. pd_at_asid' pd asid s \ asidMap = armKSASIDMap (ksArchState s) \ pd \ ran (option_map snd o armKSASIDMap (ksArchState s) |` (- {asid})) \ option_map snd (armKSASIDMap (ksArchState s) asid) \ {None, Some pd} @@ -827,7 +827,7 @@ lemma lookupPTSlot_ccorres: apply csymbr apply csymbr apply (rule ccorres_abstract_cleanup) - apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE rv)" + apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE pde)" in ccorres_gen_asm2) apply (rule ccorres_cond2'[where R=\]) apply (clarsimp simp: Collect_const_mem) @@ -842,9 +842,10 @@ lemma lookupPTSlot_ccorres: apply (simp add: checkPTAt_def bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) apply (rule ccorres_stateAssert) - apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable rv)) - and ko_at' rv (lookup_pd_slot pd vptr) - and K (isPageTablePDE rv)" and P'=UNIV in ccorres_from_vcg_throws) + apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable pde)) + and ko_at' pde (lookup_pd_slot pd vptr) and K (isPageTablePDE pde)" + and P'=UNIV + in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def Collect_const_mem lookup_pd_slot_def word_sle_def) @@ -1248,15 +1249,15 @@ lemma findFreeHWASID_ccorres: apply (rule_tac xf=hw_asid_offset_' and i=0 and xf_update=hw_asid_offset_'_update and r'=dc and xf'=xfdc and Q=UNIV - and F="\n s. rv = armKSHWASIDTable (ksArchState s) - \ nextASID = armKSNextASID (ksArchState s) - \ valid_arch_state' s" + and F="\n s. hwASIDTable = armKSHWASIDTable (ksArchState s) + \ nextASID = armKSNextASID (ksArchState s) + \ valid_arch_state' s" in ccorres_sequenceE_while_gen') apply (rule ccorres_from_vcg_might_throw) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: rf_sr_armKSNextASID) apply (subst down_cast_same [symmetric], - simp add: is_down_def target_size_def source_size_def word_size)+ + simp add: is_down_def target_size_def source_size_def word_size)+ apply (simp add: ucast_ucast_mask ucast_ucast_add ucast_and_mask ucast_of_nat_small asidInvalid_def @@ -1294,7 +1295,7 @@ lemma findFreeHWASID_ccorres: apply ceqv apply (rule ccorres_assert) apply (rule_tac A="\s. nextASID = armKSNextASID (ksArchState s) - \ rv = armKSHWASIDTable (ksArchState s) + \ hwASIDTable = armKSHWASIDTable (ksArchState s) \ valid_arch_state' s \ valid_pde_mappings' s" in ccorres_guard_imp2[where A'=UNIV]) apply (simp add: split_def) @@ -2291,7 +2292,7 @@ lemma vcpu_save_ccorres: apply (rule ccorres_move_c_guard_vcpu) apply clarsimp apply (ctac (no_vcg) add: vgicUpdate_APR_ccorres) - apply (ctac (no_vcg) add: ccorres_gets_armKSGICVCPUNumListRegs[simplified comp_def]) + apply (ctac (no_vcg) add: ccorres_gets_armKSGICVCPUNumListRegs) apply (rename_tac lr_num lr_num') apply (rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow_novcg) @@ -2465,7 +2466,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armUSGlobalPD) apply csymbr - apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentPD_ccorres) apply (rule ccorres_split_throws) @@ -2485,7 +2486,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armUSGlobalPD) apply csymbr - apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentPD_ccorres) apply (rule ccorres_split_throws) @@ -2513,7 +2514,7 @@ lemma setVMRoot_ccorres: apply (simp add: whenE_def throwError_def checkPDNotInASIDMap_def checkPDASIDMapMembership_def) apply (rule ccorres_stateAssert) - apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def]) + apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_armUSGlobalPD) apply csymbr @@ -2531,7 +2532,7 @@ lemma setVMRoot_ccorres: apply (simp add: checkPDNotInASIDMap_def checkPDASIDMapMembership_def) apply (rule ccorres_stateAssert) apply (rule ccorres_rhs_assoc)+ - apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def]) + apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState) apply (rule ccorres_h_t_valid_armUSGlobalPD) apply csymbr apply (rule ccorres_add_return2) @@ -2583,9 +2584,9 @@ lemma setVMRootForFlush_ccorres: del: Collect_const) apply (rule ccorres_if_lhs) apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) - = (capPDMappedASID (capCap rva) = None) + = (capPDMappedASID (capCap rv) = None) \ capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) - = capPDBasePtr (capCap rva)" in ccorres_gen_asm2) + = capPDBasePtr (capCap rv)" in ccorres_gen_asm2) apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+ apply (rule ccorres_split_throws) apply (rule ccorres_return_C, simp+) @@ -2804,7 +2805,7 @@ lemma setRegister_ccorres: apply (rule ccorres_pre_threadGet) apply (rule ccorres_Guard) apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) - apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = rv" + apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = uc" in threadSet_ccorres_lemma2) apply vcg apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def @@ -3406,9 +3407,7 @@ lemma unmapPage_ccorres: \ \ARMSection\ apply (rule ccorres_Cond_rhs) apply (rule ccorres_rhs_assoc)+ - \ \FIXME: The second csymbr rewrites the return relation of the goal. - If this was avoided then folding the dc_def could be removed\ - apply (csymbr, csymbr, fold dc_def) + apply (csymbr, csymbr) apply (simp add: gen_framesize_to_H_def liftE_liftM del: Collect_const) apply (simp split: if_split, rule conjI[rotated], rule impI, @@ -3442,12 +3441,9 @@ lemma unmapPage_ccorres: \ \ARMSuperSection\ apply (rule ccorres_Cond_rhs) apply (rule ccorres_rhs_assoc)+ - \ \FIXME: The third csymbr rewrites the return relation of the goal. - If this was avoided then folding the dc_def could be removed\ apply csymbr apply csymbr apply csymbr - apply (fold dc_def) apply (case_tac "pd = pde_Ptr (lookup_pd_slot pdPtr vptr)") prefer 2 apply (simp, rule ccorres_empty) @@ -4052,13 +4048,13 @@ lemma performASIDPoolInvocation_ccorres: apply (rule ccorres_rhs_assoc2) apply (rule_tac ccorres_split_nothrow [where r'=dc and xf'=xfdc]) apply (simp add: updateCap_def) - apply (rule_tac A="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPDCap rv \ asid \ mask asid_bits)" + apply (rule_tac A="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPDCap oldcap \ asid \ mask asid_bits)" and A'=UNIV in ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) - apply (rule_tac P="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPDCap rv \ asid \ mask asid_bits) - and cte_wp_at' ((=) rva) ctSlot" + apply (rule_tac P="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPDCap oldcap \ asid \ mask asid_bits) + and cte_wp_at' ((=) rv) ctSlot" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of) diff --git a/proof/crefine/RISCV64/Arch_C.thy b/proof/crefine/RISCV64/Arch_C.thy index 9e7eb57cfe..fbcb34b1dd 100644 --- a/proof/crefine/RISCV64/Arch_C.thy +++ b/proof/crefine/RISCV64/Arch_C.thy @@ -446,7 +446,7 @@ shows apply (rule ccorres_rhs_assoc2) apply (rule ccorres_abstract_cleanup) apply (rule ccorres_symb_exec_l) - apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm) + apply (rule_tac P = "rv = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm) apply (simp add: hrs_htd_update del:fun_upd_apply) apply (rule ccorres_split_nothrow) diff --git a/proof/crefine/RISCV64/CSpace_C.thy b/proof/crefine/RISCV64/CSpace_C.thy index 97e6b2dc44..66e1663641 100644 --- a/proof/crefine/RISCV64/CSpace_C.thy +++ b/proof/crefine/RISCV64/CSpace_C.thy @@ -746,7 +746,7 @@ lemma update_freeIndex': show ?thesis apply (cinit lift: cap_ptr_' v64_') apply (rule ccorres_pre_getCTE) - apply (rule_tac P="\s. ctes_of s srcSlot = Some rv \ (\i. cteCap rv = UntypedCap d p sz i)" + apply (rule_tac P="\s. ctes_of s srcSlot = Some cte \ (\i. cteCap cte = UntypedCap d p sz i)" in ccorres_from_vcg[where P' = UNIV]) apply (rule allI) apply (rule conseqPre) @@ -2388,7 +2388,7 @@ lemma capSwapForDelete_ccorres: \ \--- instruction: when (slot1 \ slot2) \ / IF Ptr slot1 = Ptr slot2 THEN \\ apply (simp add:when_def) apply (rule ccorres_if_cond_throws2 [where Q = \ and Q' = \]) - apply (case_tac "slot1=slot2", simp+) + apply (case_tac "slot1=slot2"; simp) apply (rule ccorres_return_void_C) \ \***Main goal***\ diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 59088b49db..06ed79d48b 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -296,10 +296,10 @@ lemma cancelAllIPC_ccorres: apply (cinit lift: epptr_') apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) apply (rule_tac xf'=ret__unsigned_longlong_' - and val="case rv of IdleEP \ scast EPState_Idle + and val="case ep of IdleEP \ scast EPState_Idle | RecvEP _ \ scast EPState_Recv | SendEP _ \ scast EPState_Send" - and R="ko_at' rv epptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ep epptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ep]) @@ -308,8 +308,8 @@ lemma cancelAllIPC_ccorres: apply (simp add: cendpoint_relation_def Let_def split: endpoint.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv epptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ep epptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (rename_tac list) apply (simp add: endpoint_state_defs @@ -425,10 +425,10 @@ lemma cancelAllSignals_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac xf'=ret__unsigned_longlong_' - and val="case ntfnObj rv of IdleNtfn \ scast NtfnState_Idle + and val="case ntfnObj ntfn of IdleNtfn \ scast NtfnState_Idle | ActiveNtfn _ \ scast NtfnState_Active | WaitingNtfn _ \ scast NtfnState_Waiting" - and R="ko_at' rv ntfnptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ntfn ntfnptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) @@ -437,8 +437,8 @@ lemma cancelAllSignals_ccorres: apply (simp add: cnotification_relation_def Let_def split: ntfn.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv ntfnptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ntfn ntfnptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (simp add: notification_state_defs ccorres_cond_iffs) apply (rule ccorres_return_Skip) @@ -453,8 +453,8 @@ lemma cancelAllSignals_ccorres: apply csymbr apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule_tac P="ko_at' rv ntfnptr and invs'" - in ccorres_from_vcg[where P'=UNIV]) + apply (rule_tac P="ko_at' ntfn ntfnptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) @@ -698,8 +698,8 @@ lemma doUnbindNotification_ccorres: (Call doUnbindNotification_'proc)" apply (cinit' lift: ntfnPtr_' tcbptr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV - in ccorres_split_nothrow_novcg) + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_to_ptr_def option_to_0_def) @@ -718,7 +718,7 @@ lemma doUnbindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) + apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4]) subgoal by (simp add: carch_state_relation_def) subgoal by (simp add: cmachine_state_relation_def) subgoal by (simp add: h_t_valid_clift_Some_iff) @@ -832,13 +832,13 @@ lemma unbindMaybeNotification_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) - apply (rule_tac P="ntfnBoundTCB rv \ None \ - option_to_ctcb_ptr (ntfnBoundTCB rv) \ NULL" - in ccorres_gen_asm) + apply (rule_tac P="ntfnBoundTCB ntfn \ None \ + option_to_ctcb_ptr (ntfnBoundTCB ntfn) \ NULL" + in ccorres_gen_asm) apply (rule_tac xf'=boundTCB_' - and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" - and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)" + and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1[OF cmap_relation_ntfn]) diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy index 3b21c89e8d..64886ca41d 100644 --- a/proof/crefine/RISCV64/Invoke_C.thy +++ b/proof/crefine/RISCV64/Invoke_C.thy @@ -66,7 +66,7 @@ lemma setDomain_ccorres: apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply (simp add: when_def) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. curThread = ksCurThread s" in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) @@ -77,14 +77,16 @@ lemma setDomain_ccorres: apply simp apply wp apply (rule_tac Q="\_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s)" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s)" + in hoare_strengthen_post) apply (wp threadSet_all_invs_but_sch_extra) apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric] sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" + in hoare_strengthen_post) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) @@ -629,7 +631,7 @@ 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] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add:if_P del: Collect_const) @@ -1099,7 +1101,7 @@ lemma decodeCNodeInvocation_ccorres: apply (simp add: throwError_def return_def exception_defs syscall_error_rel_def syscall_error_to_H_cases) apply clarsimp - apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const) apply csymbr apply (simp add: interpret_excaps_test_null excaps_map_def diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 7cf046eb71..e420debed1 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -3171,9 +3171,10 @@ proof - apply csymbr apply csymbr apply (rename_tac "lngth") - apply (simp add: mi_from_H_def mapME_def del: Collect_const cong: bind_apply_cong) + apply (unfold mapME_def)[1] + apply (simp add: mi_from_H_def del: Collect_const) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="length rv = unat word2" in ccorres_gen_asm) + apply (rule_tac P="length xs = unat word2" in ccorres_gen_asm) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_add_returnOk2, rule ccorres_splitE_novcg) @@ -3182,7 +3183,7 @@ proof - and Q="UNIV" and F="\n s. valid_pspace' s \ tcb_at' thread s \ (case buffer of Some x \ valid_ipc_buffer_ptr' x | _ \ \) s \ - (\m < length rv. user_word_at (rv ! m) + (\m < length xs. user_word_at (xs ! m) (x2 + (of_nat m + (msgMaxLength + 2)) * 8) s)" in ccorres_sequenceE_while') apply (simp add: split_def) @@ -3192,7 +3193,7 @@ proof - apply (rule_tac xf'=cptr_' in ccorres_abstract, ceqv) apply (ctac add: capFaultOnFailure_ccorres [OF lookupSlotForThread_ccorres']) - apply (rule_tac P="is_aligned rva 5" in ccorres_gen_asm) + apply (rule_tac P="is_aligned rv 5" in ccorres_gen_asm) apply (simp add: ccorres_cond_iffs liftE_bindE) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_getSlotCap]) apply (rule_tac P'="UNIV \ {s. excaps_map ys @@ -3213,7 +3214,7 @@ proof - apply (clarsimp simp: ccorres_cond_iffs) apply (rule_tac P= \ and P'="{x. errstate x= lu_ret___struct_lookupSlot_raw_ret_C \ - rv' = (rv ! length ys)}" + rv' = (xs ! length ys)}" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def) @@ -3254,9 +3255,8 @@ proof - apply ceqv apply (simp del: Collect_const) apply (rule_tac P'="{s. snd rv'=?curr s}" - and P="\s. length rva = length rv - \ (\x \ set rva. snd x \ 0)" - in ccorres_from_vcg_throws) + and P="\s. length rv = length xs \ (\x \ set rv. snd x \ 0)" + in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def seL4_MsgExtraCapBits_def) @@ -3591,7 +3591,7 @@ proof - apply (rule ccorres_rhs_assoc2) apply (simp add: MessageID_Exception_def) apply ccorres_rewrite - apply (subst bind_return_unit) + apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_zipWithM_x_while) apply clarsimp diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy index a8f4f743fe..e4d91a565d 100644 --- a/proof/crefine/RISCV64/Recycle_C.thy +++ b/proof/crefine/RISCV64/Recycle_C.thy @@ -807,8 +807,8 @@ lemma cancelBadgedSends_ccorres: cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong del: Collect_const) apply (rule ccorres_pre_getEndpoint) - apply (rule_tac R="ko_at' rv ptr" and xf'="ret__unsigned_longlong_'" - and val="case rv of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle + apply (rule_tac R="ko_at' ep ptr" and xf'="ret__unsigned_longlong_'" + and val="case ep of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle | SendEP q \ scast EPState_Send" in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg @@ -828,12 +828,12 @@ lemma cancelBadgedSends_ccorres: del: Collect_const cong: call_ignore_cong) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr) - apply (drule_tac s = rv in sym, simp only:) - apply (rule_tac P="ko_at' rv ptr and invs'" in ccorres_cross_over_guard) + apply (drule_tac s = ep in sym, simp only:) + apply (rule_tac P="ko_at' ep ptr and invs'" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]) - apply (rule_tac P="ko_at' rv ptr" + apply (rule_tac P="ko_at' ep ptr" in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp @@ -944,7 +944,7 @@ lemma cancelBadgedSends_ccorres: subgoal by (simp add: rf_sr_def) apply simp apply ceqv - apply (rule_tac P="ret__unsigned_longlong=blockingIPCBadge rva" in ccorres_gen_asm2) + apply (rule_tac P="ret__unsigned_longlong=blockingIPCBadge rv" in ccorres_gen_asm2) apply (rule ccorres_if_bind, rule ccorres_if_lhs) apply (simp add: bind_assoc) apply (rule ccorres_rhs_assoc)+ diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index fc0af18a7d..b1b7124999 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -777,12 +777,12 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_move_array_assertion_tcb_ctes) apply (ctac (no_vcg)) apply csymbr - apply (rule_tac b="isArchObjectCap rva \ isFrameCap (capCap rva)" in ccorres_case_bools') + apply (rule_tac b="isArchObjectCap rv \ isFrameCap (capCap rv)" in ccorres_case_bools') apply simp apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap rv" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy index 37ade0c571..a3c20082d6 100644 --- a/proof/crefine/RISCV64/Syscall_C.thy +++ b/proof/crefine/RISCV64/Syscall_C.thy @@ -1255,7 +1255,7 @@ lemma handleRecv_ccorres: apply (simp add: liftE_bind) apply (ctac) - apply (rule_tac P="\s. ksCurThread s = rv" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ksCurThread s = thread" in ccorres_cross_over_guard) apply (ctac add: receiveIPC_ccorres) apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index 1277d69227..e10874cbd5 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -444,7 +444,7 @@ lemma setPriority_ccorres: apply (frule (1) valid_objs'_maxDomain[where t=t]) apply (frule (1) valid_objs'_maxPriority[where t=t]) apply simp -done + done lemma setMCPriority_ccorres: "ccorres dc xfdc @@ -1228,7 +1228,7 @@ lemma invokeTCB_CopyRegisters_ccorres: apply (rule ccorres_pre_getCurThread) apply (ctac add: postModifyRegisters_ccorres) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rvd = ksCurThread s" + apply (rule_tac R="\s. rvc = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp @@ -1514,7 +1514,7 @@ lemma asUser_getMRs_rel: apply (erule getMRs_rel_context, simp) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs) apply simp -done + done lemma asUser_sysargs_rel: @@ -1653,7 +1653,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: apply simp apply (rule ceqv_refl) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. self = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp @@ -2130,7 +2130,7 @@ shows apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size word_less_nat_alt split: if_split_asm dest!: word_unat.Rep_inverse') - apply simp + apply (simp add: pred_conj_def) apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp tcb_in_cur_domain'_lift) apply (simp add: n_frameRegisters_def n_msgRegisters_def @@ -2253,7 +2253,8 @@ lemma decodeReadRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2264,13 +2265,13 @@ lemma decodeReadRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2365,7 +2366,8 @@ lemma decodeWriteRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2376,13 +2378,13 @@ lemma decodeWriteRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2626,7 +2628,7 @@ lemma slotCapLongRunningDelete_ccorres: apply (simp add: case_Null_If del: Collect_const) apply (rule ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_if_lhs) @@ -2647,7 +2649,7 @@ lemma slotCapLongRunningDelete_ccorres: apply vcg apply (simp del: Collect_const) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_from_vcg_throws[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of return_def) @@ -3806,7 +3808,7 @@ lemma bindNotification_ccorres: (Call bindNotification_'proc)" apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr and tcb_at' tcb" and P'=UNIV + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr and tcb_at' tcb" and P'=UNIV in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) @@ -3826,7 +3828,7 @@ lemma bindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv") + apply (case_tac "ntfnObj ntfn") apply ((clarsimp simp: option_to_ctcb_ptr_canonical[OF invs_pspace_canonical'] simp flip: canonical_bit_def)+)[3] apply (auto simp: option_to_ctcb_ptr_def objBits_simps' @@ -3906,7 +3908,7 @@ lemma decodeUnbindNotification_ccorres: apply (rule ccorres_Guard_Seq) apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getBoundNotification) - apply (rule_tac P="\s. rv \ Some 0" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ntfn \ Some 0" in ccorres_cross_over_guard) apply (simp add: bindE_bind_linearise) apply wpc apply (simp add: bindE_bind_linearise[symmetric] diff --git a/proof/crefine/RISCV64/VSpace_C.thy b/proof/crefine/RISCV64/VSpace_C.thy index ccd15fc251..ea2c563dd0 100644 --- a/proof/crefine/RISCV64/VSpace_C.thy +++ b/proof/crefine/RISCV64/VSpace_C.thy @@ -895,7 +895,7 @@ lemma setVMRoot_ccorres: apply (subst will_throw_and_catch) apply (simp split: capability.split arch_capability.split option.split) apply (fastforce simp: isCap_simps) - apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState[unfolded o_def]) + apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_h_t_valid_riscvKSGlobalPT) apply csymbr @@ -928,7 +928,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_riscvKSGlobalPT) apply csymbr - apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -940,7 +940,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_riscvKSGlobalPT) apply csymbr - apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_riscvKSGlobalPT_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -1007,7 +1007,7 @@ lemma setRegister_ccorres: apply (rule ccorres_pre_threadGet) apply (rule ccorres_Guard) apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) - apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = rv" + apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = uc" in threadSet_ccorres_lemma2) apply vcg apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def diff --git a/proof/crefine/X64/Arch_C.thy b/proof/crefine/X64/Arch_C.thy index 791d0e8668..26f4689aad 100644 --- a/proof/crefine/X64/Arch_C.thy +++ b/proof/crefine/X64/Arch_C.thy @@ -748,7 +748,9 @@ shows apply (rule ccorres_rhs_assoc2) apply (rule ccorres_abstract_cleanup) apply (rule ccorres_symb_exec_l) - apply (rule_tac P = "rva = (capability.UntypedCap isdev frame pageBits idx)" in ccorres_gen_asm) + apply (rename_tac pcap) + apply (rule_tac P = "pcap = (capability.UntypedCap isdev frame pageBits idx)" + in ccorres_gen_asm) apply (simp add: hrs_htd_update del:fun_upd_apply) apply (rule ccorres_split_nothrow) diff --git a/proof/crefine/X64/CSpace_C.thy b/proof/crefine/X64/CSpace_C.thy index 68e07eb580..191859d975 100644 --- a/proof/crefine/X64/CSpace_C.thy +++ b/proof/crefine/X64/CSpace_C.thy @@ -770,7 +770,7 @@ lemma update_freeIndex': show ?thesis apply (cinit lift: cap_ptr_' v64_') apply (rule ccorres_pre_getCTE) - apply (rule_tac P="\s. ctes_of s srcSlot = Some rv \ (\i. cteCap rv = UntypedCap d p sz i)" + apply (rule_tac P="\s. ctes_of s srcSlot = Some cte \ (\i. cteCap cte = UntypedCap d p sz i)" in ccorres_from_vcg[where P' = UNIV]) apply (rule allI) apply (rule conseqPre) @@ -2642,7 +2642,7 @@ lemma capSwapForDelete_ccorres: \ \--- instruction: when (slot1 \ slot2) \ / IF Ptr slot1 = Ptr slot2 THEN \\ apply (simp add:when_def) apply (rule ccorres_if_cond_throws2 [where Q = \ and Q' = \]) - apply (case_tac "slot1=slot2", simp+) + apply (case_tac "slot1=slot2"; simp) apply (rule ccorres_return_void_C) \ \***Main goal***\ diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy index ba0c0ec6c2..76c5bf9e67 100644 --- a/proof/crefine/X64/Finalise_C.thy +++ b/proof/crefine/X64/Finalise_C.thy @@ -278,10 +278,10 @@ lemma cancelAllIPC_ccorres: apply (cinit lift: epptr_') apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) apply (rule_tac xf'=ret__unsigned_longlong_' - and val="case rv of IdleEP \ scast EPState_Idle + and val="case ep of IdleEP \ scast EPState_Idle | RecvEP _ \ scast EPState_Recv | SendEP _ \ scast EPState_Send" - and R="ko_at' rv epptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ep epptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ep]) @@ -290,8 +290,8 @@ lemma cancelAllIPC_ccorres: apply (simp add: cendpoint_relation_def Let_def split: endpoint.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv epptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ep epptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (rename_tac list) apply (simp add: endpoint_state_defs @@ -409,10 +409,10 @@ lemma cancelAllSignals_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule_tac xf'=ret__unsigned_longlong_' - and val="case ntfnObj rv of IdleNtfn \ scast NtfnState_Idle + and val="case ntfnObj ntfn of IdleNtfn \ scast NtfnState_Idle | ActiveNtfn _ \ scast NtfnState_Active | WaitingNtfn _ \ scast NtfnState_Waiting" - and R="ko_at' rv ntfnptr" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and R="ko_at' ntfn ntfnptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) @@ -421,8 +421,8 @@ lemma cancelAllSignals_ccorres: apply (simp add: cnotification_relation_def Let_def split: ntfn.split_asm) apply ceqv - apply (rule_tac A="invs' and ko_at' rv ntfnptr" - in ccorres_guard_imp2[where A'=UNIV]) + apply (rule_tac A="invs' and ko_at' ntfn ntfnptr" + in ccorres_guard_imp2[where A'=UNIV]) apply wpc apply (simp add: notification_state_defs ccorres_cond_iffs) apply (rule ccorres_return_Skip) @@ -437,8 +437,8 @@ lemma cancelAllSignals_ccorres: apply csymbr apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) - apply (rule_tac P="ko_at' rv ntfnptr and invs'" - in ccorres_from_vcg[where P'=UNIV]) + apply (rule_tac P="ko_at' ntfn ntfnptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) @@ -683,8 +683,8 @@ lemma doUnbindNotification_ccorres: (Call doUnbindNotification_'proc)" apply (cinit' lift: ntfnPtr_' tcbptr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV - in ccorres_split_nothrow_novcg) + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: option_to_ptr_def option_to_0_def) @@ -703,7 +703,7 @@ lemma doUnbindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) + apply (case_tac "ntfnObj ntfn", ((simp add: option_to_ctcb_ptr_def)+)[4]) subgoal by (simp add: carch_state_relation_def global_ioport_bitmap_heap_update_tag_disj_simps fpu_null_state_heap_update_tag_disj_simps) @@ -822,13 +822,13 @@ lemma unbindMaybeNotification_ccorres: apply (cinit lift: ntfnPtr_') apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) apply (rule ccorres_rhs_assoc2) - apply (rule_tac P="ntfnBoundTCB rv \ None \ - option_to_ctcb_ptr (ntfnBoundTCB rv) \ NULL" - in ccorres_gen_asm) + apply (rule_tac P="ntfnBoundTCB ntfn \ None \ + option_to_ctcb_ptr (ntfnBoundTCB ntfn) \ NULL" + in ccorres_gen_asm) apply (rule_tac xf'=boundTCB_' - and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" - and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + and val="option_to_ctcb_ptr (ntfnBoundTCB ntfn)" + and R="ko_at' ntfn ntfnptr and valid_bound_tcb' (ntfnBoundTCB ntfn)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg apply clarsimp apply (erule cmap_relationE1[OF cmap_relation_ntfn]) diff --git a/proof/crefine/X64/Interrupt_C.thy b/proof/crefine/X64/Interrupt_C.thy index 8a746e5de6..f84f8f8825 100644 --- a/proof/crefine/X64/Interrupt_C.thy +++ b/proof/crefine/X64/Interrupt_C.thy @@ -828,7 +828,7 @@ from assms show ?thesis where g="\_. injection_handler P Q >>=E R" for P Q R]) apply (clarsimp simp: injection_handler_returnOk) apply (simp only: bindE_K_bind) - apply (ctac add: ioapic_decode_map_pin_to_vector_ccorres[simplified o_def]) + apply (ctac add: ioapic_decode_map_pin_to_vector_ccorres) apply ccorres_rewrite apply (simp add: ccorres_invocationCatch_Inr performInvocation_def returnOk_bind liftE_bindE bindE_assoc diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy index b4c97f0312..2800a857e9 100644 --- a/proof/crefine/X64/Invoke_C.thy +++ b/proof/crefine/X64/Invoke_C.thy @@ -65,7 +65,7 @@ lemma setDomain_ccorres: apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply (simp add: when_def) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. curThread = ksCurThread s" in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) @@ -76,14 +76,16 @@ lemma setDomain_ccorres: apply simp apply wp apply (rule_tac Q="\_. all_invs_but_sch_extra and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s)" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s)" + in hoare_strengthen_post) apply (wp threadSet_all_invs_but_sch_extra) apply (clarsimp simp: valid_pspace_valid_objs' st_tcb_at_def[symmetric] sch_act_simple_def st_tcb_at'_def weak_sch_act_wf_def split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple - and (\s. rv = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" in hoare_strengthen_post) + and (\s. curThread = ksCurThread s \ (\p. t \ set (ksReadyQueues s p)))" + in hoare_strengthen_post) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_not_queued tcbSchedDequeue_not_in_queue hoare_vcg_imp_lift hoare_vcg_all_lift) apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) @@ -627,7 +629,7 @@ 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] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const cong: call_ignore_cong) apply (rule ccorres_Cond_rhs_Seq) apply (simp add:if_P del: Collect_const) @@ -1097,7 +1099,7 @@ lemma decodeCNodeInvocation_ccorres: apply (simp add: throwError_def return_def exception_defs syscall_error_rel_def syscall_error_to_H_cases) apply clarsimp - apply (simp add: invocationCatch_use_injection_handler[symmetric, unfolded o_def] + apply (simp add: invocationCatch_use_injection_handler[symmetric] del: Collect_const) apply csymbr apply (simp add: interpret_excaps_test_null excaps_map_def diff --git a/proof/crefine/X64/Ipc_C.thy b/proof/crefine/X64/Ipc_C.thy index dfc729f49d..45eecea7bb 100644 --- a/proof/crefine/X64/Ipc_C.thy +++ b/proof/crefine/X64/Ipc_C.thy @@ -3182,9 +3182,10 @@ proof - apply csymbr apply csymbr apply (rename_tac "lngth") - apply (simp add: mi_from_H_def mapME_def del: Collect_const cong: bind_apply_cong) + apply (unfold mapME_def)[1] + apply (simp add: mi_from_H_def del: Collect_const) apply (rule ccorres_symb_exec_l) - apply (rule_tac P="length rv = unat word2" in ccorres_gen_asm) + apply (rule_tac P="length xs = unat word2" in ccorres_gen_asm) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_add_returnOk2, rule ccorres_splitE_novcg) @@ -3193,7 +3194,7 @@ proof - and Q="UNIV" and F="\n s. valid_pspace' s \ tcb_at' thread s \ (case buffer of Some x \ valid_ipc_buffer_ptr' x | _ \ \) s \ - (\m < length rv. user_word_at (rv ! m) + (\m < length xs. user_word_at (xs ! m) (x2 + (of_nat m + (msgMaxLength + 2)) * 8) s)" in ccorres_sequenceE_while') apply (simp add: split_def) @@ -3203,7 +3204,7 @@ proof - apply (rule_tac xf'=cptr_' in ccorres_abstract, ceqv) apply (ctac add: capFaultOnFailure_ccorres [OF lookupSlotForThread_ccorres']) - apply (rule_tac P="is_aligned rva 5" in ccorres_gen_asm) + apply (rule_tac P="is_aligned rv 5" in ccorres_gen_asm) apply (simp add: ccorres_cond_iffs liftE_bindE) apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_getSlotCap]) apply (rule_tac P'="UNIV \ {s. excaps_map ys @@ -3224,7 +3225,7 @@ proof - apply (clarsimp simp: ccorres_cond_iffs) apply (rule_tac P= \ and P'="{x. errstate x= lu_ret___struct_lookupSlot_raw_ret_C \ - rv' = (rv ! length ys)}" + rv' = (xs ! length ys)}" in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def) @@ -3265,9 +3266,8 @@ proof - apply ceqv apply (simp del: Collect_const) apply (rule_tac P'="{s. snd rv'=?curr s}" - and P="\s. length rva = length rv - \ (\x \ set rva. snd x \ 0)" - in ccorres_from_vcg_throws) + and P="\s. length rv = length xs \ (\x \ set rv. snd x \ 0)" + in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def seL4_MsgExtraCapBits_def) @@ -3603,7 +3603,7 @@ proof - apply (rule ccorres_rhs_assoc2) apply (simp add: MessageID_Exception_def) apply ccorres_rewrite - apply (subst bind_return_unit) + apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_zipWithM_x_while) apply clarsimp diff --git a/proof/crefine/X64/Recycle_C.thy b/proof/crefine/X64/Recycle_C.thy index 54832cdb61..e904218590 100644 --- a/proof/crefine/X64/Recycle_C.thy +++ b/proof/crefine/X64/Recycle_C.thy @@ -903,8 +903,8 @@ lemma cancelBadgedSends_ccorres: cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong del: Collect_const) apply (rule ccorres_pre_getEndpoint) - apply (rule_tac R="ko_at' rv ptr" and xf'="ret__unsigned_longlong_'" - and val="case rv of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle + apply (rule_tac R="ko_at' ep ptr" and xf'="ret__unsigned_longlong_'" + and val="case ep of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle | SendEP q \ scast EPState_Send" in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) apply vcg @@ -924,12 +924,12 @@ lemma cancelBadgedSends_ccorres: del: Collect_const cong: call_ignore_cong) apply (rule ccorres_rhs_assoc)+ apply (csymbr, csymbr) - apply (drule_tac s = rv in sym, simp only:) - apply (rule_tac P="ko_at' rv ptr and invs'" in ccorres_cross_over_guard) + apply (drule_tac s = ep in sym, simp only:) + apply (rule_tac P="ko_at' ep ptr and invs'" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc, OF _ ceqv_refl]) - apply (rule_tac P="ko_at' rv ptr" + apply (rule_tac P="ko_at' ep ptr" in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp @@ -1043,7 +1043,7 @@ lemma cancelBadgedSends_ccorres: subgoal by (simp add: rf_sr_def) apply simp apply ceqv - apply (rule_tac P="ret__unsigned_longlong=blockingIPCBadge rva" in ccorres_gen_asm2) + apply (rule_tac P="ret__unsigned_longlong=blockingIPCBadge rv" in ccorres_gen_asm2) apply (rule ccorres_if_bind, rule ccorres_if_lhs) apply (simp add: bind_assoc) apply (rule ccorres_rhs_assoc)+ diff --git a/proof/crefine/X64/SyscallArgs_C.thy b/proof/crefine/X64/SyscallArgs_C.thy index ae323381a3..a01433a8bb 100644 --- a/proof/crefine/X64/SyscallArgs_C.thy +++ b/proof/crefine/X64/SyscallArgs_C.thy @@ -783,12 +783,12 @@ lemma lookupIPCBuffer_ccorres[corres]: apply (rule ccorres_move_array_assertion_tcb_ctes) apply (ctac (no_vcg)) apply csymbr - apply (rule_tac b="isArchObjectCap rva \ isPageCap (capCap rva)" in ccorres_case_bools') + apply (rule_tac b="isArchObjectCap rv \ isPageCap (capCap rv)" in ccorres_case_bools') apply simp apply (rule ccorres_cond_false_seq) apply (simp(no_asm)) apply csymbr - apply (rule_tac b="isDeviceCap rva" in ccorres_case_bools') + apply (rule_tac b="isDeviceCap rv" in ccorres_case_bools') apply (rule ccorres_cond_true_seq) apply (rule ccorres_from_vcg_split_throws[where P=\ and P'=UNIV]) apply vcg diff --git a/proof/crefine/X64/Syscall_C.thy b/proof/crefine/X64/Syscall_C.thy index 149b316f93..f3d3004b31 100644 --- a/proof/crefine/X64/Syscall_C.thy +++ b/proof/crefine/X64/Syscall_C.thy @@ -1253,7 +1253,7 @@ lemma handleRecv_ccorres: apply (simp add: liftE_bind) apply (ctac) - apply (rule_tac P="\s. ksCurThread s = rv" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ksCurThread s = thread" in ccorres_cross_over_guard) apply (ctac add: receiveIPC_ccorres) apply (wp deleteCallerCap_ksQ_ct' hoare_vcg_all_lift) diff --git a/proof/crefine/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy index 5e5888acb6..1e13a4f9bd 100644 --- a/proof/crefine/X64/Tcb_C.thy +++ b/proof/crefine/X64/Tcb_C.thy @@ -437,7 +437,7 @@ lemma setPriority_ccorres: apply (frule (1) valid_objs'_maxDomain[where t=t]) apply (frule (1) valid_objs'_maxPriority[where t=t]) apply simp -done + done lemma setMCPriority_ccorres: "ccorres dc xfdc @@ -1223,7 +1223,7 @@ lemma invokeTCB_CopyRegisters_ccorres: apply (rule ccorres_pre_getCurThread) apply (ctac add: postModifyRegisters_ccorres) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rvd = ksCurThread s" + apply (rule_tac R="\s. rvc = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp @@ -1504,7 +1504,7 @@ lemma asUser_getMRs_rel: apply (erule getMRs_rel_context, simp) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs) apply simp -done + done lemma asUser_sysargs_rel: @@ -1643,7 +1643,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: apply simp apply (rule ceqv_refl) apply (rule ccorres_split_nothrow_novcg_dc) - apply (rule_tac R="\s. rv = ksCurThread s" + apply (rule_tac R="\s. self = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp @@ -2120,7 +2120,7 @@ shows apply (clarsimp simp: min_def iffD2 [OF mask_eq_iff_w2p] word_size word_less_nat_alt split: if_split_asm dest!: word_unat.Rep_inverse') - apply simp + apply (simp add: pred_conj_def) apply (wp mapM_x_wp' sch_act_wf_lift valid_queues_lift static_imp_wp tcb_in_cur_domain'_lift) apply (simp add: n_frameRegisters_def n_msgRegisters_def @@ -2243,7 +2243,8 @@ lemma decodeReadRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2254,13 +2255,13 @@ lemma decodeReadRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2355,7 +2356,8 @@ lemma decodeWriteRegisters_ccorres: apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_cond_seq) - apply (rule_tac R="\s. rv = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = rv" in ccorres_cond_both) + apply (rule_tac R="\s. self = ksCurThread s \ isThreadCap cp" and P="\s. capTCBPtr cp = self" + in ccorres_cond_both) apply clarsimp apply (frule rf_sr_ksCurThread) apply clarsimp @@ -2366,13 +2368,13 @@ lemma decodeWriteRegisters_ccorres: apply (drule_tac t="ksCurThread s" in sym) apply simp apply simp - apply (rule_tac P="capTCBPtr cp = rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp = self" in ccorres_gen_asm) apply simp apply (simp add: throwError_bind invocationCatch_def cong: StateSpace.state.fold_congs globals.fold_congs) apply (rule syscall_error_throwError_ccorres_n) apply (simp add: syscall_error_to_H_cases) - apply (rule_tac P="capTCBPtr cp \ rv" in ccorres_gen_asm) + apply (rule_tac P="capTCBPtr cp \ self" in ccorres_gen_asm) apply (simp add: returnOk_bind) apply (simp add: ccorres_invocationCatch_Inr del: Collect_const) apply (ctac add: setThreadState_ccorres) @@ -2615,7 +2617,7 @@ lemma slotCapLongRunningDelete_ccorres: apply (simp add: case_Null_If del: Collect_const) apply (rule ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_cross_over_guard) apply (rule ccorres_symb_exec_r) apply (rule ccorres_if_lhs) @@ -2636,7 +2638,7 @@ lemma slotCapLongRunningDelete_ccorres: apply vcg apply (simp del: Collect_const) apply (rule ccorres_move_c_guard_cte) - apply (rule_tac P="cte_wp_at' ((=) rv) slot" + apply (rule_tac P="cte_wp_at' ((=) cte) slot" in ccorres_from_vcg_throws[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of return_def) @@ -3795,7 +3797,7 @@ lemma bindNotification_ccorres: (Call bindNotification_'proc)" apply (cinit lift: tcb_' ntfnPtr_' simp: bindNotification_def) apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) - apply (rule_tac P="invs' and ko_at' rv ntfnptr and tcb_at' tcb" and P'=UNIV + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr and tcb_at' tcb" and P'=UNIV in ccorres_split_nothrow_novcg) apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) apply (rule allI, rule conseqPre, vcg) @@ -3815,7 +3817,7 @@ lemma bindNotification_ccorres: apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (clarsimp simp: cnotification_relation_def Let_def mask_def [where n=2] NtfnState_Waiting_def) - apply (case_tac "ntfnObj rv") + apply (case_tac "ntfnObj ntfn") apply ((clarsimp simp: option_to_ctcb_ptr_canonical[OF invs_pspace_canonical'])+)[3] apply (auto simp: option_to_ctcb_ptr_def objBits_simps' bindNTFN_alignment_junk)[1] @@ -3895,7 +3897,7 @@ lemma decodeUnbindNotification_ccorres: apply (rule ccorres_Guard_Seq) apply (simp add: liftE_bindE bind_assoc) apply (rule ccorres_pre_getBoundNotification) - apply (rule_tac P="\s. rv \ Some 0" in ccorres_cross_over_guard) + apply (rule_tac P="\s. ntfn \ Some 0" in ccorres_cross_over_guard) apply (simp add: bindE_bind_linearise) apply wpc apply (simp add: bindE_bind_linearise[symmetric] diff --git a/proof/crefine/X64/VSpace_C.thy b/proof/crefine/X64/VSpace_C.thy index d2f81095f8..f2419d10db 100644 --- a/proof/crefine/X64/VSpace_C.thy +++ b/proof/crefine/X64/VSpace_C.thy @@ -654,7 +654,7 @@ lemma lookupPDPTSlot_ccorres': apply csymbr apply csymbr apply (rule ccorres_abstract_cleanup) - apply (rule_tac P="(ret__unsigned_longlong = 0) = (rv = X64_H.InvalidPML4E)" + apply (rule_tac P="(ret__unsigned_longlong = 0) = (pml4e = X64_H.InvalidPML4E)" in ccorres_gen_asm2) apply (wpc; ccorres_rewrite) apply (rule_tac P=\ and P' =UNIV in ccorres_from_vcg_throws) @@ -666,9 +666,9 @@ lemma lookupPDPTSlot_ccorres': apply (thin_tac "_ = PDPointerTablePML4E _ _ _ _ _ _") apply (simp add: bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) apply (rule ccorres_stateAssert) - apply (rule_tac P="pd_pointer_table_at' (ptrFromPAddr (pml4eTable rv)) - and ko_at' rv (lookup_pml4_slot pm vptr) - and K (isPDPointerTablePML4E rv)" + apply (rule_tac P="pd_pointer_table_at' (ptrFromPAddr (pml4eTable pml4e)) + and ko_at' pml4e (lookup_pml4_slot pm vptr) + and K (isPDPointerTablePML4E pml4e)" and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) @@ -1195,7 +1195,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_x64KSSKIMPML4) apply csymbr - apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -1212,7 +1212,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_x64KSSKIMPML4) apply csymbr - apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -1236,7 +1236,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_x64KSSKIMPML4) apply csymbr - apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -1258,7 +1258,7 @@ lemma setVMRoot_ccorres: apply (rule ccorres_rhs_assoc) apply (rule ccorres_h_t_valid_x64KSSKIMPML4) apply csymbr - apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) + apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState) apply (rule ccorres_add_return2) apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) apply (rule ccorres_return_void_C) @@ -1333,7 +1333,7 @@ lemma setRegister_ccorres: apply (rule ccorres_pre_threadGet) apply (rule ccorres_Guard) apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) - apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = rv" + apply (rule_tac P="\tcb. (atcbContextGet o tcbArch) tcb = uc" in threadSet_ccorres_lemma2) apply vcg apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def @@ -2337,13 +2337,13 @@ lemma performASIDPoolInvocation_ccorres: apply (rule ccorres_rhs_assoc2) apply (rule_tac ccorres_split_nothrow [where r'=dc and xf'=xfdc]) apply (simp add: updateCap_def) - apply (rule_tac A="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPML4Cap' rv \ asid \ mask asid_bits \ asid \ ucast asidInvalid)" + apply (rule_tac A="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPML4Cap' oldcap \ asid \ mask asid_bits \ asid \ ucast asidInvalid)" and A'=UNIV in ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) - apply (rule_tac P="cte_wp_at' ((=) rv o cteCap) ctSlot - and K (isPML4Cap' rv \ asid \ mask asid_bits \ asid \ ucast asidInvalid) - and cte_wp_at' ((=) rva) ctSlot" + apply (rule_tac P="cte_wp_at' ((=) oldcap o cteCap) ctSlot + and K (isPML4Cap' oldcap \ asid \ mask asid_bits \ asid \ ucast asidInvalid) + and cte_wp_at' ((=) rv) ctSlot" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of) diff --git a/proof/crefine/lib/Ctac.thy b/proof/crefine/lib/Ctac.thy index 0d8d1e97fe..676f3f5230 100644 --- a/proof/crefine/lib/Ctac.thy +++ b/proof/crefine/lib/Ctac.thy @@ -2031,6 +2031,7 @@ fun tac ctxt = ORELSE (resolve_tac ctxt [@{thm xpresI}] THEN' simp_tac (ctxt |> Splitter.del_split @{thm "if_split"})) 1 )) THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms com.case}) 1 + THEN no_name_eta_tac ctxt \ end diff --git a/proof/crefine/lib/ctac-method.ML b/proof/crefine/lib/ctac-method.ML index bf539617c2..eca4ad1ab4 100644 --- a/proof/crefine/lib/ctac-method.ML +++ b/proof/crefine/lib/ctac-method.ML @@ -1107,7 +1107,9 @@ fun shorten_names mp = mp -- Shorten_Names.shorten_names_preserve_new >> MethodExtras.then_all_new val corres_ctac_tactic = let - fun tac upds ctxt = Method.SIMPLE_METHOD' (corres_ctac (apply upds default_ctac_opts) ctxt); + fun tac upds ctxt + = Method.SIMPLE_METHOD' (corres_ctac (apply upds default_ctac_opts) ctxt + THEN_ALL_NEW (fn _ => no_name_eta_tac ctxt)); val option_args = Args.parens (P.list (Scan.first ctac_options)) val opt_option_args = Scan.lift (Scan.optional option_args []) @@ -1133,7 +1135,9 @@ val corres_abstract_args = corres_pre_abstract_args corres_pre_lift_tac_clift; val corres_abstract_init_args = corres_pre_abstract_args corres_pre_lift_tac_cinit; val corres_symb_rhs = let - fun tac upds ctxt = Method.SIMPLE_METHOD' (corres_symb_rhs_tac (apply upds default_csymbr_opts) ctxt); + fun tac upds ctxt + = Method.SIMPLE_METHOD' (corres_symb_rhs_tac (apply upds default_csymbr_opts) ctxt + THEN_ALL_NEW (fn _ => no_name_eta_tac ctxt)); val option_args = Args.parens (P.list (Scan.first csymbr_options)) val opt_option_args = Scan.lift (Scan.optional option_args []) @@ -1143,7 +1147,8 @@ in end; val corres_ceqv = let - fun tac upds ctxt = Method.SIMPLE_METHOD' (corres_solve_ceqv (#trace (apply upds default_ceqv_opts)) 0 ctxt); + fun tac upds ctxt + = Method.SIMPLE_METHOD' (corres_solve_ceqv (#trace (apply upds default_ceqv_opts)) 0 ctxt); val option_args = Args.parens (P.list (Scan.first ceqv_options)) val opt_option_args = Scan.lift (Scan.optional option_args []) @@ -1156,7 +1161,8 @@ end; * We should be able to get the xfs from the goal ... *) fun corres_boilerplate unfold_haskell_p = let fun tac (upds, xfs : string list) ctxt - = Method.SIMPLE_METHOD' (corres_boilerplate_tac (apply upds default_cinit_opts) unfold_haskell_p xfs ctxt) + = Method.SIMPLE_METHOD' (corres_boilerplate_tac (apply upds default_cinit_opts) unfold_haskell_p xfs ctxt + THEN_ALL_NEW (fn _ => no_name_eta_tac ctxt)) val var_lift_args = Args.$$$ liftoptN |-- Args.colon |-- Scan.repeat (Scan.unless (Scan.first boilerplate_modifiers) Args.name)