aarch64 refine: add state_hyp_refs_of' to valid_state'
Somehow we missed this on the first pass. Adjusted existing proofs. Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski
Gerwin Klein
parent
a79e06f419
commit
904056868d
|
|
@ -260,6 +260,13 @@ lemma storePTE_state_refs_of[wp]:
|
|||
clarsimp simp: updateObject_default_def in_monad)
|
||||
done
|
||||
|
||||
lemma storePTE_state_hyp_refs_of[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace>
|
||||
storePTE ptr val
|
||||
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
by (wpsimp wp: hoare_drop_imps setObject_state_hyp_refs_of_eq
|
||||
simp: storePTE_def updateObject_default_def in_monad)
|
||||
|
||||
crunch cte_wp_at'[wp]: setIRQState "\<lambda>s. P (cte_wp_at' P' p s)"
|
||||
crunch inv[wp]: getIRQSlot "P"
|
||||
|
||||
|
|
|
|||
|
|
@ -2514,6 +2514,18 @@ qed
|
|||
crunch state_refs_of'[wp]: cteInsert "\<lambda>s. P (state_refs_of' s)"
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma setCTE_state_hyp_refs_of'[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
unfolding setCTE_def
|
||||
apply (rule setObject_state_hyp_refs_of_eq)
|
||||
apply (clarsimp simp: updateObject_cte in_monad typeError_def
|
||||
in_magnitude_check objBits_simps
|
||||
split: kernel_object.split_asm if_split_asm)
|
||||
done
|
||||
|
||||
crunch state_hyp_refs_of'[wp]: cteInsert "\<lambda>s. P (state_hyp_refs_of' s)"
|
||||
(wp: crunch_wps)
|
||||
|
||||
crunch aligned'[wp]: cteInsert pspace_aligned'
|
||||
(wp: crunch_wps)
|
||||
|
||||
|
|
@ -2968,6 +2980,9 @@ crunch irq_states' [wp]: cteInsert valid_irq_states'
|
|||
crunch pred_tcb_at'[wp]: cteInsert "pred_tcb_at' proj P t"
|
||||
(wp: crunch_wps)
|
||||
|
||||
crunch state_hyp_refs_of'[wp]: setupReplyMaster "\<lambda>s. P (state_hyp_refs_of' s)"
|
||||
(wp: crunch_wps)
|
||||
|
||||
lemma setCTE_cteCaps_of[wp]:
|
||||
"\<lbrace>\<lambda>s. P ((cteCaps_of s)(p \<mapsto> cteCap cte))\<rbrace>
|
||||
setCTE p cte
|
||||
|
|
|
|||
|
|
@ -1060,7 +1060,7 @@ abbreviation
|
|||
|
||||
definition valid_state' :: "kernel_state \<Rightarrow> bool" where
|
||||
"valid_state' \<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s)
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> sym_refs (state_hyp_refs_of' s)
|
||||
\<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s
|
||||
\<and> valid_idle' s
|
||||
\<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
|
|
@ -1148,7 +1148,7 @@ abbreviation(input)
|
|||
abbreviation(input)
|
||||
"all_invs_but_ct_not_inQ'
|
||||
\<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s)
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> sym_refs (state_hyp_refs_of' s)
|
||||
\<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s
|
||||
\<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
\<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s
|
||||
|
|
@ -1159,7 +1159,7 @@ abbreviation(input)
|
|||
\<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s"
|
||||
|
||||
lemma all_invs_but_sym_refs_not_ct_inQ_check':
|
||||
"(all_invs_but_sym_refs_ct_not_inQ' and sym_refs \<circ> state_refs_of' and ct_not_inQ) = invs'"
|
||||
"(all_invs_but_sym_refs_ct_not_inQ' and sym_refs \<circ> state_refs_of' and sym_refs \<circ> state_hyp_refs_of' and ct_not_inQ) = invs'"
|
||||
by (simp add: pred_conj_def conj_commute conj_left_commute invs'_def valid_state'_def)
|
||||
|
||||
lemma all_invs_but_not_ct_inQ_check':
|
||||
|
|
@ -1169,7 +1169,7 @@ lemma all_invs_but_not_ct_inQ_check':
|
|||
definition
|
||||
"all_invs_but_ct_idle_or_in_cur_domain'
|
||||
\<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s)
|
||||
\<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> sym_refs (state_hyp_refs_of' s)
|
||||
\<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s
|
||||
\<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s
|
||||
\<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s
|
||||
|
|
@ -1797,6 +1797,10 @@ lemma state_refs_of'_pspaceI:
|
|||
"P (state_refs_of' s) \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> P (state_refs_of' s')"
|
||||
unfolding state_refs_of'_def ps_clear_def by (simp cong: option.case_cong)
|
||||
|
||||
lemma state_hyp_refs_of'_pspaceI:
|
||||
"P (state_hyp_refs_of' s) \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> P (state_hyp_refs_of' s')"
|
||||
unfolding state_hyp_refs_of'_def ps_clear_def by (simp cong: option.case_cong)
|
||||
|
||||
lemma valid_pspace':
|
||||
"valid_pspace' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_pspace' s'"
|
||||
by (auto simp add: valid_pspace'_def valid_objs'_def pspace_aligned'_def pspace_canonical'_def
|
||||
|
|
@ -2608,6 +2612,10 @@ lemma state_refs_of'_eq[iff]:
|
|||
"state_refs_of' (f s) = state_refs_of' s"
|
||||
by (rule state_refs_of'_pspaceI [OF _ pspace], rule refl)
|
||||
|
||||
lemma state_hyp_refs_of'_eq[iff]:
|
||||
"state_hyp_refs_of' (f s) = state_hyp_refs_of' s"
|
||||
by (rule state_hyp_refs_of'_pspaceI [OF _ pspace], rule refl)
|
||||
|
||||
lemma valid_space_update [iff]:
|
||||
"valid_pspace' (f s) = valid_pspace' s"
|
||||
by (fastforce simp: valid_pspace' pspace)
|
||||
|
|
@ -3229,6 +3237,10 @@ lemma invs_sym' [elim!]:
|
|||
"invs' s \<Longrightarrow> sym_refs (state_refs_of' s)"
|
||||
by (simp add: invs'_def valid_state'_def)
|
||||
|
||||
lemma invs_sym_hyp' [elim!]:
|
||||
"invs' s \<Longrightarrow> sym_refs (state_hyp_refs_of' s)"
|
||||
by (simp add: invs'_def valid_state'_def)
|
||||
|
||||
lemma invs_sch_act_wf' [elim!]:
|
||||
"invs' s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s"
|
||||
by (simp add: invs'_def valid_state'_def)
|
||||
|
|
|
|||
|
|
@ -2224,9 +2224,8 @@ lemma doMachineOp_invs_bits[wp]:
|
|||
doMachineOp m \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
|
||||
"\<lbrace>Invariants_H.valid_queues\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
|
||||
"\<lbrace>valid_queues'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
|
||||
"\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
|
||||
doMachineOp m
|
||||
\<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
|
||||
"\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
"\<lbrace>if_live_then_nonz_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
|
||||
"\<lbrace>cur_tcb'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
|
||||
"\<lbrace>if_unsafe_then_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>"
|
||||
|
|
|
|||
|
|
@ -777,7 +777,7 @@ lemma threadSet_state_hyp_refs_of':
|
|||
shows "\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
apply (simp add: threadSet_def)
|
||||
apply (wpsimp wp: setObject_state_hyp_refs_of' getObject_tcb_wp
|
||||
simp: objBits_simps' obj_at'_def state_hyp_refs_of'_def)
|
||||
simp: objBits_simps' obj_at'_def state_hyp_refs_of'_def)
|
||||
apply (clarsimp simp:objBits_simps' y state_hyp_refs_of'_def
|
||||
elim!: rsubst[where P=P] intro!: ext)+
|
||||
done
|
||||
|
|
@ -1294,6 +1294,7 @@ proof -
|
|||
threadSet_sch_actT_P[where P=False, simplified]
|
||||
threadSet_valid_queues
|
||||
threadSet_state_refs_of'T[where f'=id]
|
||||
threadSet_state_hyp_refs_of'
|
||||
threadSet_iflive'T
|
||||
threadSet_ifunsafe'T
|
||||
threadSet_idle'T
|
||||
|
|
@ -1520,6 +1521,14 @@ lemma asUser_st_refs_of'[wp]:
|
|||
apply (wp threadSet_state_refs_of' hoare_drop_imps | simp)+
|
||||
done
|
||||
|
||||
lemma asUser_st_hyp_refs_of'[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace>
|
||||
asUser t m
|
||||
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
apply (simp add: asUser_def split_def)
|
||||
apply (wp threadSet_state_hyp_refs_of' hoare_drop_imps | simp add: atcbContextSet_def atcbVCPUPtr_atcbContext_update)+
|
||||
done
|
||||
|
||||
lemma asUser_iflive'[wp]:
|
||||
"\<lbrace>if_live_then_nonz_cap'\<rbrace> asUser t m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
|
||||
apply (simp add: asUser_def split_def)
|
||||
|
|
@ -3883,6 +3892,17 @@ lemma setThreadState_state_refs_of'[wp]:
|
|||
by (simp add: setThreadState_def fun_upd_def
|
||||
| wp threadSet_state_refs_of')+
|
||||
|
||||
crunch hyp_refs_of'[wp]: rescheduleRequired "\<lambda>s. P (state_hyp_refs_of' s)"
|
||||
(simp: unless_def crunch_simps wp: threadSet_state_hyp_refs_of' ignore: threadSet)
|
||||
|
||||
lemma setThreadState_state_hyp_refs_of'[wp]:
|
||||
"\<lbrace>\<lambda>s. P ((state_hyp_refs_of' s))\<rbrace>
|
||||
setThreadState st t
|
||||
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
apply (simp add: setThreadState_def fun_upd_def
|
||||
| wp threadSet_state_hyp_refs_of')+
|
||||
done
|
||||
|
||||
lemma setBoundNotification_state_refs_of'[wp]:
|
||||
"\<lbrace>\<lambda>s. P ((state_refs_of' s) (t := tcb_bound_refs' ntfn
|
||||
\<union> {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound}))\<rbrace>
|
||||
|
|
@ -3891,6 +3911,13 @@ lemma setBoundNotification_state_refs_of'[wp]:
|
|||
by (simp add: setBoundNotification_def Un_commute fun_upd_def
|
||||
| wp threadSet_state_refs_of' )+
|
||||
|
||||
lemma setBoundNotification_state_hyp_refs_of'[wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace>
|
||||
setBoundNotification ntfn t
|
||||
\<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
by (simp add: setBoundNotification_def fun_upd_def
|
||||
| wp threadSet_state_hyp_refs_of')+
|
||||
|
||||
lemma sts_cur_tcb'[wp]:
|
||||
"\<lbrace>cur_tcb'\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
|
||||
by (wp cur_tcb_lift)
|
||||
|
|
|
|||
|
|
@ -2454,10 +2454,15 @@ lemma setVMRoot_invs'[wp]:
|
|||
by (wpsimp wp: whenE_wp findVSpaceForASID_vs_at_wp hoare_drop_imps hoare_vcg_ex_lift
|
||||
hoare_vcg_all_lift) *)
|
||||
|
||||
lemma setGlobalUserVSpace_invs_no_cicd'[wp]:
|
||||
"setGlobalUserVSpace \<lbrace>invs_no_cicd'\<rbrace>"
|
||||
unfolding setGlobalUserVSpace_def
|
||||
by wpsimp
|
||||
|
||||
lemma setVMRoot_invs_no_cicd':
|
||||
"\<lbrace>invs_no_cicd'\<rbrace> setVMRoot p \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>"
|
||||
unfolding setVMRoot_def getThreadVSpaceRoot_def
|
||||
sorry (* FIXME AARCH64 stuck on setGlobalUserVSpace
|
||||
sorry (* FIXME AARCH64 stuck on armContextSwitch
|
||||
by (wpsimp wp: whenE_wp findVSpaceForASID_vs_at_wp hoare_drop_imps hoare_vcg_ex_lift
|
||||
hoare_vcg_all_lift) *)
|
||||
|
||||
|
|
@ -2749,6 +2754,16 @@ lemma setASIDPool_state_refs' [wp]:
|
|||
apply (simp split: option.split)
|
||||
done
|
||||
|
||||
lemma setASIDPool_state_hyp_refs' [wp]:
|
||||
"\<lbrace>\<lambda>s. P (state_hyp_refs_of' s)\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv s. P (state_hyp_refs_of' s)\<rbrace>"
|
||||
apply (clarsimp simp: setObject_def valid_def in_monad split_def
|
||||
updateObject_default_def objBits_simps
|
||||
in_magnitude_check state_hyp_refs_of'_def ps_clear_upd
|
||||
elim!: rsubst[where P=P] del: ext intro!: ext
|
||||
split del: if_split cong: option.case_cong if_cong)
|
||||
apply (simp split: option.split)
|
||||
done
|
||||
|
||||
lemma setASIDPool_iflive [wp]:
|
||||
"\<lbrace>if_live_then_nonz_cap'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
|
||||
apply (rule hoare_pre)
|
||||
|
|
|
|||
Loading…
Reference in New Issue