diff --git a/proof/refine/ARM_HYP/CSpace_R.thy b/proof/refine/ARM_HYP/CSpace_R.thy index bc4fff0ae..53195a701 100644 --- a/proof/refine/ARM_HYP/CSpace_R.thy +++ b/proof/refine/ARM_HYP/CSpace_R.thy @@ -2797,7 +2797,10 @@ lemma setCTE_idle [wp]: "\valid_idle'\ setCTE p cte \\rv. valid_idle'\" apply (simp add: valid_idle'_def) apply (rule hoare_lift_Pf [where f="ksIdleThread"]) - apply (wp setCTE_pred_tcb_at')+ + apply (intro hoare_vcg_conj_lift; (solves \wpsimp\)?) + apply (clarsimp simp: setCTE_def) + apply (rule setObject_cte_obj_at_tcb'[where P="idle_tcb'", simplified]) + apply wpsimp done crunch it[wp]: getCTE "\s. P (ksIdleThread s)" @@ -2816,7 +2819,7 @@ lemma updateMDB_idle'[wp]: apply (clarsimp simp add: updateMDB_def) apply (rule hoare_pre) apply (wp | simp add: valid_idle'_def)+ - done + by fastforce lemma updateCap_idle': "\valid_idle'\ updateCap p c \\rv. valid_idle'\" diff --git a/proof/refine/ARM_HYP/Finalise_R.thy b/proof/refine/ARM_HYP/Finalise_R.thy index f20506383..283f93f03 100644 --- a/proof/refine/ARM_HYP/Finalise_R.thy +++ b/proof/refine/ARM_HYP/Finalise_R.thy @@ -2544,8 +2544,7 @@ lemma archThreadSet_valid_idle'[wp]: "archThreadSet f t \valid_idle'\" unfolding archThreadSet_def apply (wpsimp wp: setObject_tcb_idle' getObject_tcb_wp) - apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def) - apply normalise_obj_at' + apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) done lemma archThreadSet_ko_wp_at_no_vcpu[wp]: diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index 18c45b564..dbe28edca 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -1182,10 +1182,10 @@ lemma vgicMaintenance_invs'[wp]: apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq) apply (rule conjI) apply (fastforce elim!: st_tcb_ex_cap'' simp: valid_state'_def valid_pspace'_def) - apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) - apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq pred_tcb_at'_def) + apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def obj_at'_def idle_tcb'_def) apply wps apply (wpsimp simp: if_apply_def2 wp: hoare_vcg_const_imp_lift hoare_drop_imps +hoare_vcg_ex_lift hoare_vcg_conj_lift | wps)+ apply (clarsimp cong: conj_cong imp_cong split: if_split) apply (strengthen st_tcb_ex_cap''[where P=active']) @@ -1195,8 +1195,7 @@ lemma vgicMaintenance_invs'[wp]: apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq) apply (rule conjI) apply (fastforce elim!: st_tcb_ex_cap'' simp: valid_state'_def valid_pspace'_def) - apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) - apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq pred_tcb_at'_def) + apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def obj_at'_def idle_tcb'_def) apply clarsimp done @@ -1218,8 +1217,7 @@ lemma vppiEvent_invs'[wp]: apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq) apply (rule conjI) apply (fastforce elim!: st_tcb_ex_cap'' simp: valid_state'_def valid_pspace'_def) - apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) - apply (clarsimp simp: st_tcb_at'_def obj_at'_def runnable'_eq pred_tcb_at'_def) + apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def obj_at'_def idle_tcb'_def) apply wps apply (wpsimp simp: if_apply_def2 vcpuUpdate_def wp: hoare_vcg_const_imp_lift hoare_drop_imps diff --git a/proof/refine/ARM_HYP/Invariants_H.thy b/proof/refine/ARM_HYP/Invariants_H.thy index d431aaaad..1d8d080ec 100644 --- a/proof/refine/ARM_HYP/Invariants_H.thy +++ b/proof/refine/ARM_HYP/Invariants_H.thy @@ -1110,12 +1110,27 @@ where abbreviation "sch_act_not t \ \s. ksSchedulerAction s \ SwitchToThread t" -abbreviation "idle_tcb_at' \ pred_tcb_at' (\t. (itcbState t, itcbBoundNotification t))" +definition + idle_tcb'_2 :: "Structures_H.thread_state \ machine_word option + \ bool" +where + "idle_tcb'_2 \ \(st, ntfn_opt). (idle' st \ ntfn_opt = None)" + +abbreviation + "idle_tcb' tcb \ idle_tcb'_2 (tcbState tcb, tcbBoundNotification tcb)" + +lemmas idle_tcb'_def = idle_tcb'_2_def definition valid_idle' :: "kernel_state \ bool" where - "valid_idle' \ \s. idle_tcb_at' (\p. idle' (fst p) \ snd p = None) (ksIdleThread s) s" + "valid_idle' \ + \s. obj_at' idle_tcb' (ksIdleThread s) s + \ idle_thread_ptr = ksIdleThread s" + +lemma valid_idle'_tcb_at': + "valid_idle' s \ obj_at' idle_tcb' (ksIdleThread s) s" + by (clarsimp simp: valid_idle'_def) definition valid_irq_node' :: "word32 \ kernel_state \ bool" @@ -1949,7 +1964,7 @@ lemma valid_pspaceE' [elim]: lemma idle'_no_refs: "valid_idle' s \ state_refs_of' s (ksIdleThread s) = {}" by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def - projectKO_eq project_inject state_refs_of'_def) + projectKO_eq project_inject state_refs_of'_def idle_tcb'_def) lemma idle'_not_queued': "\valid_idle' s; sym_refs (state_refs_of' s); @@ -2088,7 +2103,7 @@ lemma valid_idle'_pspace_itI[elim]: "\ valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s' \ \ valid_idle' s'" apply (clarsimp simp: valid_idle'_def ex_nonz_cap_to'_def) - apply (erule pred_tcb_at'_pspaceI, assumption) + apply (erule obj_at'_pspaceI, assumption) done lemma obj_at'_weaken: @@ -3430,10 +3445,6 @@ lemma not_pred_tcb_at'_strengthen: "pred_tcb_at' f (Not \ P) p s \ \ pred_tcb_at' f P p s" by (clarsimp simp: pred_tcb_at'_def obj_at'_def) -lemma idle_tcb_at'_split: - "idle_tcb_at' (\p. P (fst p) \ Q (snd p)) t s \ st_tcb_at' P t s \ bound_tcb_at' Q t s" - by (clarsimp simp: pred_tcb_at'_def dest!: obj_at'_conj_distrib) - lemma valid_queues_no_bitmap_def': "valid_queues_no_bitmap = (\s. \d p. (\t\set (ksReadyQueues s (d, p)). diff --git a/proof/refine/ARM_HYP/IpcCancel_R.thy b/proof/refine/ARM_HYP/IpcCancel_R.thy index 3857c306b..ecdb0c5dd 100644 --- a/proof/refine/ARM_HYP/IpcCancel_R.thy +++ b/proof/refine/ARM_HYP/IpcCancel_R.thy @@ -867,7 +867,7 @@ proof - | wpc)+ apply (clarsimp simp: pred_tcb_at' fun_upd_def[symmetric] conj_comms split del: if_split cong: if_cong) - apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) + apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: projectKOs valid_obj'_def) apply (rule conjI) @@ -2723,7 +2723,7 @@ lemma cancelBadgedSends_filterM_helper': apply (intro conjI) apply (clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE dest!: st_tcb_ex_cap'') apply (fastforce dest!: st_tcb_ex_cap'') - apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def) + apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply (erule delta_sym_refs) apply (fastforce elim!: obj_atE' simp: state_refs_of'_def projectKOs tcb_bound_refs'_def diff --git a/proof/refine/ARM_HYP/Ipc_R.thy b/proof/refine/ARM_HYP/Ipc_R.thy index 483c8583e..34fe3d80c 100644 --- a/proof/refine/ARM_HYP/Ipc_R.thy +++ b/proof/refine/ARM_HYP/Ipc_R.thy @@ -3116,7 +3116,7 @@ lemma sai_invs'[wp]: apply (clarsimp simp: valid_obj'_def valid_ntfn'_def split: list.splits) apply (clarsimp simp: invs'_def valid_state'_def) - apply (clarsimp simp: st_tcb_at_refs_of_rev' valid_idle'_def pred_tcb_at'_def + apply (clarsimp simp: st_tcb_at_refs_of_rev' valid_idle'_def pred_tcb_at'_def idle_tcb'_def dest!: sym_refs_ko_atD' sym_refs_st_tcb_atD' sym_refs_obj_atD' split: list.splits) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) @@ -3723,7 +3723,7 @@ crunch cap_to'[wp]: doIPCTransfer "ex_nonz_cap_to' p" lemma st_tcb_idle': "\valid_idle' s; st_tcb_at' P t s\ \ (t = ksIdleThread s) \ P IdleThreadState" - by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def) + by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) crunch idle'[wp]: getThreadCallerSlot "valid_idle'" crunch idle'[wp]: getThreadReplySlot "valid_idle'" diff --git a/proof/refine/ARM_HYP/KHeap_R.thy b/proof/refine/ARM_HYP/KHeap_R.thy index 502028d0f..819953b56 100644 --- a/proof/refine/ARM_HYP/KHeap_R.thy +++ b/proof/refine/ARM_HYP/KHeap_R.thy @@ -1250,6 +1250,13 @@ lemma setObject_it[wp]: apply (wp x | simp)+ done +\\ + `idle_tcb_ps val` asserts that `val` is a pspace_storable value + which corresponds to an idle TCB. +\ +definition idle_tcb_ps :: "('a :: pspace_storable) \ bool" where + "idle_tcb_ps val \ (\tcb. projectKO_opt (injectKO val) = Some tcb \ idle_tcb' tcb)" + lemma setObject_idle': fixes v :: "'a :: pspace_storable" assumes R: "\ko s x y n. (updateObject v ko ptr y n s) @@ -1260,12 +1267,9 @@ lemma setObject_idle': \\s. P (ksIdleThread s)\ updateObject v p q n ko \\rv s. P (ksIdleThread s)\" shows "\\s. valid_idle' s \ - (ptr = ksIdleThread s \ - (\obj (val :: 'a). projectKO_opt (injectKO val) = Some obj - \ idle' (tcbState obj) \ tcbBoundNotification obj = None) - \ (\obj. projectKO_opt (injectKO v) = Some obj \ - idle' (tcbState obj) \ tcbBoundNotification obj = None)) \ - P s\ + (ptr = ksIdleThread s + \ (\val :: 'a. idle_tcb_ps val) + \ idle_tcb_ps v)\ setObject ptr v \\rv s. valid_idle' s\" apply (simp add: valid_idle'_def pred_tcb_at'_def o_def) @@ -1274,8 +1278,7 @@ lemma setObject_idle': apply (simp add: pred_tcb_at'_def obj_at'_real_def) apply (rule setObject_ko_wp_at [OF R n m]) apply (wp z) - apply (clarsimp simp add: pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def) - apply (drule_tac x=obj in spec, simp) + apply (clarsimp simp add: pred_tcb_at'_def obj_at'_real_def ko_wp_at'_def idle_tcb_ps_def) apply (clarsimp simp add: project_inject) apply (drule_tac x=obja in spec, simp) done @@ -1884,9 +1887,9 @@ lemma setEndpoint_idle'[wp]: setEndpoint p v \\_. valid_idle'\" unfolding setEndpoint_def - apply (wp setObject_idle'[where P="\"]) + apply (wp setObject_idle') apply (simp add: objBits_simps' updateObject_default_inv)+ - apply (clarsimp simp: projectKOs) + apply (clarsimp simp: projectKOs idle_tcb_ps_def) done crunch it[wp]: setEndpoint "\s. P (ksIdleThread s)" @@ -2035,9 +2038,9 @@ lemma setNotification_ifunsafe'[wp]: lemma setNotification_idle'[wp]: "\\s. valid_idle' s\ setNotification p v \\rv. valid_idle'\" unfolding setNotification_def - apply (wp setObject_idle'[where P="\"]) + apply (wp setObject_idle') apply (simp add: objBits_simps' updateObject_default_inv)+ - apply (clarsimp simp: projectKOs) + apply (clarsimp simp: projectKOs idle_tcb_ps_def) done crunch it[wp]: setNotification "\s. P (ksIdleThread s)" diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index ea6008a45..d7ce021c4 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -4160,6 +4160,7 @@ lemma createObjects_idle': apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (clarsimp simp add: valid_idle'_def pred_tcb_at'_def) + apply (rule hoare_vcg_conj_lift) apply (rule hoare_as_subst [OF createObjects'_it]) apply (wp createObjects_orig_obj_at' createObjects_orig_cte_wp_at2' diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 44f18d938..478e52377 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -967,7 +967,7 @@ lemma idle'_not_tcbQueued': shows "obj_at' (Not \ tcbQueued) (ksIdleThread s) s" proof - from idle have stidle: "st_tcb_at' (Not \ runnable') (ksIdleThread s) s" - by (clarsimp simp add: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) + by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def) with vq vq' show ?thesis by (rule valid_queues_not_runnable_not_queued) @@ -985,15 +985,17 @@ proof - show ?thesis apply (simp add: setCurThread_def) apply wp - apply (clarsimp simp add: ct_not_inQ_ct idle'_activatable' idle'_not_tcbQueued'[simplified o_def] + apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def) + apply (frule (2) idle'_not_tcbQueued'[simplified o_def]) + apply (clarsimp simp add: ct_not_inQ_ct idle'_activatable' invs'_def cur_tcb'_def valid_state'_def valid_idle'_def sch_act_wf ct_in_state'_def state_refs_of'_def ps_clear_def valid_irq_node'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def valid_queues'_def - all_invs_but_ct_idle_or_in_cur_domain'_def pred_tcb_at'_def + pred_tcb_at'_def cong: option.case_cong) - apply (clarsimp simp: obj_at'_def projectKOs) + apply (clarsimp simp: obj_at'_def projectKOs idle_tcb'_def) done qed @@ -2164,7 +2166,7 @@ lemma switchToIdleThread_activatable_2[wp]: ARM_HYP_H.switchToIdleThread_def) apply (wp setCurThread_ct_in_state) apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def - pred_tcb_at'_def obj_at'_def) + pred_tcb_at'_def obj_at'_def idle_tcb'_def) done lemma switchToThread_tcb_in_cur_domain': diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 0c2d1da88..0ab7604b8 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -834,18 +834,17 @@ lemma doReply_invs[wp]: in hoare_strengthen_post [rotated]) apply (clarsimp) apply (rule conjI) - apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def) + apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) apply (rule conjI) apply clarsimp - apply clarsimp - apply (drule idle_tcb_at'_split, clarsimp, drule (1) st_tcb_at'_eqD, simp) + apply (clarsimp simp: obj_at'_def idle_tcb'_def pred_tcb_at'_def) apply clarsimp apply (rule conjI) - apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def) + apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) apply (erule pred_tcb'_weakenE, clarsimp) apply (rule conjI) - apply (clarsimp simp add: invs'_def valid_state'_def valid_idle'_def pred_tcb_at'_def - obj_at'_def) + apply (clarsimp simp : invs'_def valid_state'_def valid_idle'_def pred_tcb_at'_def + obj_at'_def idle_tcb'_def) apply (rule conjI) apply clarsimp apply (frule invs'_not_runnable_not_queued) @@ -1159,7 +1158,7 @@ lemma get_mrs_length_rv[wp]: lemma st_tcb_at_idle_thread': "\ st_tcb_at' P (ksIdleThread s) s; valid_idle' s \ \ P IdleThreadState" - by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def) + by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) crunch tcb_at'[wp]: replyFromKernel "tcb_at' t" @@ -1354,7 +1353,7 @@ lemma hinv_invs'[wp]: apply (subgoal_tac "thread \ ksIdleThread s", simp_all)[1] apply (fastforce elim!: pred_tcb'_weakenE st_tcb_ex_cap'') apply (clarsimp simp: valid_idle'_def valid_state'_def - invs'_def pred_tcb_at'_def obj_at'_def) + invs'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply wp+ apply (wp sts_invs_minor' setThreadState_st_tcb setThreadState_rct ct_in_state_thread_state_lift' sts_st_tcb_at'_cases @@ -2147,7 +2146,7 @@ proof assume "ksCurThread s = ksIdleThread s" with vi have "ct_in_state' idle' s" unfolding ct_in_state'_def valid_idle'_def - by (clarsimp simp: pred_tcb_at'_def obj_at'_def) + by (clarsimp simp: pred_tcb_at'_def obj_at'_def idle_tcb'_def) with cts show False unfolding ct_in_state'_def diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy index c254b46dd..58b4a90e6 100644 --- a/proof/refine/ARM_HYP/TcbAcc_R.thy +++ b/proof/refine/ARM_HYP/TcbAcc_R.thy @@ -541,10 +541,10 @@ lemma setObject_tcb_idle': (t = ksIdleThread s \ idle' (tcbState v) \ tcbBoundNotification v = None)\ setObject t (v :: tcb) \\rv. valid_idle'\" apply (rule hoare_pre) - apply (rule_tac P="\" in setObject_idle') + apply (rule setObject_idle') apply (simp add: objBits_simps')+ apply (simp add: updateObject_default_inv) - apply (simp add: projectKOs) + apply (simp add: projectKOs idle_tcb_ps_def idle_tcb'_def) done lemma setObject_tcb_irq_node'[wp]: @@ -826,14 +826,13 @@ lemma threadSet_idle'T: shows "\\s. valid_idle' s \ (t = ksIdleThread s \ - (\tcb. ko_at' tcb t s \ idle' (tcbState tcb) \ idle' (tcbState (F tcb))) - \ (\tcb. ko_at' tcb t s \ tcbBoundNotification tcb = None \ tcbBoundNotification (F tcb) = None))\ + (\tcb. ko_at' tcb t s \ idle_tcb' tcb \ idle_tcb' (F tcb)))\ threadSet F t \\rv. valid_idle'\" apply (simp add: threadSet_def) apply (wp setObject_tcb_idle' getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs) - apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) + apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs idle_tcb'_def) done lemmas threadSet_idle' = @@ -3730,7 +3729,7 @@ lemma sts_valid_idle'[wp]: setThreadState ts t \\rv. valid_idle'\" apply (simp add: setThreadState_def) - apply (wp threadSet_idle', simp+)+ + apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def) done lemma sbn_valid_idle'[wp]: @@ -3739,7 +3738,7 @@ lemma sbn_valid_idle'[wp]: setBoundNotification ntfn t \\rv. valid_idle'\" apply (simp add: setBoundNotification_def) - apply (wp threadSet_idle', simp+)+ + apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def) done lemma gts_sp': diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 4453bd79d..fdcace89f 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -120,7 +120,7 @@ lemma activate_invs': in hoare_post_imp, clarsimp) apply (wp sch_act_simple_lift)+ apply (clarsimp simp: valid_idle'_def invs'_def valid_state'_def - pred_tcb_at'_def obj_at'_def + pred_tcb_at'_def obj_at'_def idle_tcb'_def elim!: pred_tcb'_weakenE) apply (wp gts_st_tcb')+ apply (clarsimp simp: tcb_at_invs' ct_in_state'_def diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index 11afd0ac6..b1f4d5b0e 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -4513,8 +4513,15 @@ lemma storePDE_ifunsafe [wp]: lemma storePDE_idle [wp]: "\valid_idle'\ storePDE p pde \\rv. valid_idle'\" - unfolding valid_idle'_def - by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp) + apply (simp add: valid_idle'_def) + apply (rule hoare_lift_Pf [where f="ksIdleThread"]) + apply (intro hoare_vcg_conj_lift; (solves \wpsimp\)?) + apply (clarsimp simp: storePDE_def) + apply (wpsimp wp: obj_at_setObject2[where P="idle_tcb'", simplified] hoare_drop_imp) + apply (clarsimp dest!: updateObject_default_result) + apply simp + apply wpsimp + done lemma storePDE_arch'[wp]: "\\s. P (ksArchState s)\ storePDE param_a param_b \\_ s. P (ksArchState s)\" @@ -4715,8 +4722,15 @@ lemma storePTE_ifunsafe [wp]: lemma storePTE_idle [wp]: "\valid_idle'\ storePTE p pte \\rv. valid_idle'\" - unfolding valid_idle'_def - by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp) + apply (simp add: valid_idle'_def) + apply (rule hoare_lift_Pf [where f="ksIdleThread"]) + apply (intro hoare_vcg_conj_lift; (solves \wpsimp\)?) + apply (clarsimp simp: storePTE_def) + apply (wpsimp wp: obj_at_setObject2[where P="idle_tcb'", simplified] hoare_drop_imp) + apply (clarsimp dest!: updateObject_default_result) + apply simp + apply wpsimp + done lemma storePTE_arch'[wp]: "\\s. P (ksArchState s)\ storePTE param_a param_b \\_ s. P (ksArchState s)\" @@ -4919,8 +4933,13 @@ lemma setASIDPool_it' [wp]: lemma setASIDPool_idle [wp]: "\valid_idle'\ setObject p (ap::asidpool) \\rv. valid_idle'\" - unfolding valid_idle'_def - by (rule hoare_lift_Pf [where f="ksIdleThread"]; wp) + apply (simp add: valid_idle'_def) + apply (rule hoare_lift_Pf [where f="ksIdleThread"]) + apply (intro hoare_vcg_conj_lift; (solves \wpsimp\)?) + apply (rule obj_at_setObject2[where P="idle_tcb'", simplified]) + apply (clarsimp dest!: updateObject_default_result) + apply wpsimp + done lemma setASIDPool_irq_states' [wp]: "\valid_irq_states'\ setObject p (ap::asidpool) \\_. valid_irq_states'\"