armhyp refine: define valid_idle' directly, without using itcb
- this introduces idle_tcb' which is defined directly using tcb fields - backport from MCS ARM Refine Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
parent
d054484474
commit
4da06d81ad
|
@ -2797,7 +2797,10 @@ lemma setCTE_idle [wp]:
|
|||
"\<lbrace>valid_idle'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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 \<open>wpsimp\<close>)?)
|
||||
apply (clarsimp simp: setCTE_def)
|
||||
apply (rule setObject_cte_obj_at_tcb'[where P="idle_tcb'", simplified])
|
||||
apply wpsimp
|
||||
done
|
||||
|
||||
crunch it[wp]: getCTE "\<lambda>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':
|
||||
"\<lbrace>valid_idle'\<rbrace> updateCap p c \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
|
|
|
@ -2544,8 +2544,7 @@ lemma archThreadSet_valid_idle'[wp]:
|
|||
"archThreadSet f t \<lbrace>valid_idle'\<rbrace>"
|
||||
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]:
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -1110,12 +1110,27 @@ where
|
|||
abbreviation
|
||||
"sch_act_not t \<equiv> \<lambda>s. ksSchedulerAction s \<noteq> SwitchToThread t"
|
||||
|
||||
abbreviation "idle_tcb_at' \<equiv> pred_tcb_at' (\<lambda>t. (itcbState t, itcbBoundNotification t))"
|
||||
definition
|
||||
idle_tcb'_2 :: "Structures_H.thread_state \<times> machine_word option
|
||||
\<Rightarrow> bool"
|
||||
where
|
||||
"idle_tcb'_2 \<equiv> \<lambda>(st, ntfn_opt). (idle' st \<and> ntfn_opt = None)"
|
||||
|
||||
abbreviation
|
||||
"idle_tcb' tcb \<equiv> idle_tcb'_2 (tcbState tcb, tcbBoundNotification tcb)"
|
||||
|
||||
lemmas idle_tcb'_def = idle_tcb'_2_def
|
||||
|
||||
definition
|
||||
valid_idle' :: "kernel_state \<Rightarrow> bool"
|
||||
where
|
||||
"valid_idle' \<equiv> \<lambda>s. idle_tcb_at' (\<lambda>p. idle' (fst p) \<and> snd p = None) (ksIdleThread s) s"
|
||||
"valid_idle' \<equiv>
|
||||
\<lambda>s. obj_at' idle_tcb' (ksIdleThread s) s
|
||||
\<and> idle_thread_ptr = ksIdleThread s"
|
||||
|
||||
lemma valid_idle'_tcb_at':
|
||||
"valid_idle' s \<Longrightarrow> obj_at' idle_tcb' (ksIdleThread s) s"
|
||||
by (clarsimp simp: valid_idle'_def)
|
||||
|
||||
definition
|
||||
valid_irq_node' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool"
|
||||
|
@ -1949,7 +1964,7 @@ lemma valid_pspaceE' [elim]:
|
|||
lemma idle'_no_refs:
|
||||
"valid_idle' s \<Longrightarrow> 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':
|
||||
"\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s);
|
||||
|
@ -2088,7 +2103,7 @@ lemma valid_idle'_pspace_itI[elim]:
|
|||
"\<lbrakk> valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s' \<rbrakk>
|
||||
\<Longrightarrow> 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 \<circ> P) p s \<Longrightarrow> \<not> 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' (\<lambda>p. P (fst p) \<and> Q (snd p)) t s \<Longrightarrow> st_tcb_at' P t s \<and> 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 =
|
||||
(\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)).
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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':
|
||||
"\<lbrakk>valid_idle' s; st_tcb_at' P t s\<rbrakk> \<Longrightarrow>
|
||||
(t = ksIdleThread s) \<longrightarrow> 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'"
|
||||
|
|
|
@ -1250,6 +1250,13 @@ lemma setObject_it[wp]:
|
|||
apply (wp x | simp)+
|
||||
done
|
||||
|
||||
\<comment>\<open>
|
||||
`idle_tcb_ps val` asserts that `val` is a pspace_storable value
|
||||
which corresponds to an idle TCB.
|
||||
\<close>
|
||||
definition idle_tcb_ps :: "('a :: pspace_storable) \<Rightarrow> bool" where
|
||||
"idle_tcb_ps val \<equiv> (\<exists>tcb. projectKO_opt (injectKO val) = Some tcb \<and> idle_tcb' tcb)"
|
||||
|
||||
lemma setObject_idle':
|
||||
fixes v :: "'a :: pspace_storable"
|
||||
assumes R: "\<And>ko s x y n. (updateObject v ko ptr y n s)
|
||||
|
@ -1260,12 +1267,9 @@ lemma setObject_idle':
|
|||
\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko
|
||||
\<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>"
|
||||
shows "\<lbrace>\<lambda>s. valid_idle' s \<and>
|
||||
(ptr = ksIdleThread s \<longrightarrow>
|
||||
(\<exists>obj (val :: 'a). projectKO_opt (injectKO val) = Some obj
|
||||
\<and> idle' (tcbState obj) \<and> tcbBoundNotification obj = None)
|
||||
\<longrightarrow> (\<exists>obj. projectKO_opt (injectKO v) = Some obj \<and>
|
||||
idle' (tcbState obj) \<and> tcbBoundNotification obj = None)) \<and>
|
||||
P s\<rbrace>
|
||||
(ptr = ksIdleThread s
|
||||
\<longrightarrow> (\<exists>val :: 'a. idle_tcb_ps val)
|
||||
\<longrightarrow> idle_tcb_ps v)\<rbrace>
|
||||
setObject ptr v
|
||||
\<lbrace>\<lambda>rv s. valid_idle' s\<rbrace>"
|
||||
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
|
||||
\<lbrace>\<lambda>_. valid_idle'\<rbrace>"
|
||||
unfolding setEndpoint_def
|
||||
apply (wp setObject_idle'[where P="\<top>"])
|
||||
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 "\<lambda>s. P (ksIdleThread s)"
|
||||
|
@ -2035,9 +2038,9 @@ lemma setNotification_ifunsafe'[wp]:
|
|||
lemma setNotification_idle'[wp]:
|
||||
"\<lbrace>\<lambda>s. valid_idle' s\<rbrace> setNotification p v \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
unfolding setNotification_def
|
||||
apply (wp setObject_idle'[where P="\<top>"])
|
||||
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 "\<lambda>s. P (ksIdleThread s)"
|
||||
|
|
|
@ -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'
|
||||
|
|
|
@ -967,7 +967,7 @@ lemma idle'_not_tcbQueued':
|
|||
shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s"
|
||||
proof -
|
||||
from idle have stidle: "st_tcb_at' (Not \<circ> 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':
|
||||
|
|
|
@ -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':
|
||||
"\<lbrakk> st_tcb_at' P (ksIdleThread s) s; valid_idle' s \<rbrakk>
|
||||
\<Longrightarrow> 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 \<noteq> 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
|
||||
|
|
|
@ -541,10 +541,10 @@ lemma setObject_tcb_idle':
|
|||
(t = ksIdleThread s \<longrightarrow> idle' (tcbState v) \<and> tcbBoundNotification v = None)\<rbrace>
|
||||
setObject t (v :: tcb) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
apply (rule_tac P="\<top>" 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
|
||||
"\<lbrace>\<lambda>s. valid_idle' s
|
||||
\<and> (t = ksIdleThread s \<longrightarrow>
|
||||
(\<forall>tcb. ko_at' tcb t s \<and> idle' (tcbState tcb) \<longrightarrow> idle' (tcbState (F tcb)))
|
||||
\<and> (\<forall>tcb. ko_at' tcb t s \<and> tcbBoundNotification tcb = None \<longrightarrow> tcbBoundNotification (F tcb) = None))\<rbrace>
|
||||
(\<forall>tcb. ko_at' tcb t s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (F tcb)))\<rbrace>
|
||||
threadSet F t
|
||||
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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
|
||||
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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
|
||||
\<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
apply (simp add: setBoundNotification_def)
|
||||
apply (wp threadSet_idle', simp+)+
|
||||
apply (wpsimp wp: threadSet_idle' simp: idle_tcb'_def)
|
||||
done
|
||||
|
||||
lemma gts_sp':
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -4513,8 +4513,15 @@ lemma storePDE_ifunsafe [wp]:
|
|||
|
||||
lemma storePDE_idle [wp]:
|
||||
"\<lbrace>valid_idle'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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 \<open>wpsimp\<close>)?)
|
||||
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]:
|
||||
"\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> storePDE param_a param_b \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>"
|
||||
|
@ -4715,8 +4722,15 @@ lemma storePTE_ifunsafe [wp]:
|
|||
|
||||
lemma storePTE_idle [wp]:
|
||||
"\<lbrace>valid_idle'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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 \<open>wpsimp\<close>)?)
|
||||
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]:
|
||||
"\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> storePTE param_a param_b \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>"
|
||||
|
@ -4919,8 +4933,13 @@ lemma setASIDPool_it' [wp]:
|
|||
|
||||
lemma setASIDPool_idle [wp]:
|
||||
"\<lbrace>valid_idle'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>"
|
||||
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 \<open>wpsimp\<close>)?)
|
||||
apply (rule obj_at_setObject2[where P="idle_tcb'", simplified])
|
||||
apply (clarsimp dest!: updateObject_default_result)
|
||||
apply wpsimp
|
||||
done
|
||||
|
||||
lemma setASIDPool_irq_states' [wp]:
|
||||
"\<lbrace>valid_irq_states'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>"
|
||||
|
|
Loading…
Reference in New Issue