diff --git a/proof/refine/AARCH64/ArchAcc_R.thy b/proof/refine/AARCH64/ArchAcc_R.thy index 45eb08c8b..c05e899be 100644 --- a/proof/refine/AARCH64/ArchAcc_R.thy +++ b/proof/refine/AARCH64/ArchAcc_R.thy @@ -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]: + "\\s. P (state_hyp_refs_of' s)\ + storePTE ptr val + \\rv s. P (state_hyp_refs_of' s)\" + 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 "\s. P (cte_wp_at' P' p s)" crunch inv[wp]: getIRQSlot "P" diff --git a/proof/refine/AARCH64/CSpace_R.thy b/proof/refine/AARCH64/CSpace_R.thy index 518dacc3c..d45be0d1b 100644 --- a/proof/refine/AARCH64/CSpace_R.thy +++ b/proof/refine/AARCH64/CSpace_R.thy @@ -2514,6 +2514,18 @@ qed crunch state_refs_of'[wp]: cteInsert "\s. P (state_refs_of' s)" (wp: crunch_wps) +lemma setCTE_state_hyp_refs_of'[wp]: + "\\s. P (state_hyp_refs_of' s)\ setCTE p cte \\rv s. P (state_hyp_refs_of' s)\" + 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 "\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 "\s. P (state_hyp_refs_of' s)" + (wp: crunch_wps) + lemma setCTE_cteCaps_of[wp]: "\\s. P ((cteCaps_of s)(p \ cteCap cte))\ setCTE p cte diff --git a/proof/refine/AARCH64/Invariants_H.thy b/proof/refine/AARCH64/Invariants_H.thy index 09dd35b65..4251fd53a 100644 --- a/proof/refine/AARCH64/Invariants_H.thy +++ b/proof/refine/AARCH64/Invariants_H.thy @@ -1060,7 +1060,7 @@ abbreviation definition valid_state' :: "kernel_state \ bool" where "valid_state' \ \s. valid_pspace' s \ sch_act_wf (ksSchedulerAction s) s - \ valid_queues s \ sym_refs (state_refs_of' s) + \ valid_queues s \ sym_refs (state_refs_of' s) \ sym_refs (state_hyp_refs_of' s) \ if_live_then_nonz_cap' s \ if_unsafe_then_cap' s \ valid_idle' s \ valid_global_refs' s \ valid_arch_state' s @@ -1148,7 +1148,7 @@ abbreviation(input) abbreviation(input) "all_invs_but_ct_not_inQ' \ \s. valid_pspace' s \ sch_act_wf (ksSchedulerAction s) s - \ valid_queues s \ sym_refs (state_refs_of' s) + \ valid_queues s \ sym_refs (state_refs_of' s) \ sym_refs (state_hyp_refs_of' s) \ if_live_then_nonz_cap' s \ if_unsafe_then_cap' s \ valid_idle' s \ valid_global_refs' s \ valid_arch_state' s \ valid_irq_node' (irq_node' s) s \ valid_irq_handlers' s @@ -1159,7 +1159,7 @@ abbreviation(input) \ valid_dom_schedule' s \ 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 \ state_refs_of' and ct_not_inQ) = invs'" + "(all_invs_but_sym_refs_ct_not_inQ' and sym_refs \ state_refs_of' and sym_refs \ 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' \ \s. valid_pspace' s \ sch_act_wf (ksSchedulerAction s) s - \ valid_queues s \ sym_refs (state_refs_of' s) + \ valid_queues s \ sym_refs (state_refs_of' s) \ sym_refs (state_hyp_refs_of' s) \ if_live_then_nonz_cap' s \ if_unsafe_then_cap' s \ valid_idle' s \ valid_global_refs' s \ valid_arch_state' s \ valid_irq_node' (irq_node' s) s \ valid_irq_handlers' s @@ -1797,6 +1797,10 @@ lemma state_refs_of'_pspaceI: "P (state_refs_of' s) \ ksPSpace s = ksPSpace s' \ 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) \ ksPSpace s = ksPSpace s' \ 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 \ ksPSpace s = ksPSpace s' \ 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 \ sym_refs (state_refs_of' s)" by (simp add: invs'_def valid_state'_def) +lemma invs_sym_hyp' [elim!]: + "invs' s \ sym_refs (state_hyp_refs_of' s)" + by (simp add: invs'_def valid_state'_def) + lemma invs_sch_act_wf' [elim!]: "invs' s \ sch_act_wf (ksSchedulerAction s) s" by (simp add: invs'_def valid_state'_def) diff --git a/proof/refine/AARCH64/KHeap_R.thy b/proof/refine/AARCH64/KHeap_R.thy index 5cbb5cc30..7ed320a99 100644 --- a/proof/refine/AARCH64/KHeap_R.thy +++ b/proof/refine/AARCH64/KHeap_R.thy @@ -2224,9 +2224,8 @@ lemma doMachineOp_invs_bits[wp]: doMachineOp m \\rv s. sch_act_wf (ksSchedulerAction s) s\" "\Invariants_H.valid_queues\ doMachineOp m \\rv. Invariants_H.valid_queues\" "\valid_queues'\ doMachineOp m \\rv. valid_queues'\" - "\\s. P (state_refs_of' s)\ - doMachineOp m - \\rv s. P (state_refs_of' s)\" + "\\s. P (state_refs_of' s)\ doMachineOp m \\rv s. P (state_refs_of' s)\" + "\\s. P (state_hyp_refs_of' s)\ doMachineOp m \\rv s. P (state_hyp_refs_of' s)\" "\if_live_then_nonz_cap'\ doMachineOp m \\rv. if_live_then_nonz_cap'\" "\cur_tcb'\ doMachineOp m \\rv. cur_tcb'\" "\if_unsafe_then_cap'\ doMachineOp m \\rv. if_unsafe_then_cap'\" diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy index 954b8542f..009b300ad 100644 --- a/proof/refine/AARCH64/TcbAcc_R.thy +++ b/proof/refine/AARCH64/TcbAcc_R.thy @@ -777,7 +777,7 @@ lemma threadSet_state_hyp_refs_of': shows "\\s. P (state_hyp_refs_of' s)\ threadSet F t \\rv s. P (state_hyp_refs_of' s)\" 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]: + "\\s. P (state_hyp_refs_of' s)\ + asUser t m + \\rv s. P (state_hyp_refs_of' s)\" + 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]: "\if_live_then_nonz_cap'\ asUser t m \\rv. if_live_then_nonz_cap'\" 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 "\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]: + "\\s. P ((state_hyp_refs_of' s))\ + setThreadState st t + \\rv s. P (state_hyp_refs_of' s)\" + apply (simp add: setThreadState_def fun_upd_def + | wp threadSet_state_hyp_refs_of')+ + done + lemma setBoundNotification_state_refs_of'[wp]: "\\s. P ((state_refs_of' s) (t := tcb_bound_refs' ntfn \ {r \ state_refs_of' s t. snd r \ TCBBound}))\ @@ -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]: + "\\s. P (state_hyp_refs_of' s)\ + setBoundNotification ntfn t + \\rv s. P (state_hyp_refs_of' s)\" + by (simp add: setBoundNotification_def fun_upd_def + | wp threadSet_state_hyp_refs_of')+ + lemma sts_cur_tcb'[wp]: "\cur_tcb'\ setThreadState st t \\rv. cur_tcb'\" by (wp cur_tcb_lift) diff --git a/proof/refine/AARCH64/VSpace_R.thy b/proof/refine/AARCH64/VSpace_R.thy index 5ab1cc237..7e4dc254d 100644 --- a/proof/refine/AARCH64/VSpace_R.thy +++ b/proof/refine/AARCH64/VSpace_R.thy @@ -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 \invs_no_cicd'\" + unfolding setGlobalUserVSpace_def + by wpsimp + lemma setVMRoot_invs_no_cicd': "\invs_no_cicd'\ setVMRoot p \\rv. invs_no_cicd'\" 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]: + "\\s. P (state_hyp_refs_of' s)\ setObject p (ap::asidpool) \\rv s. P (state_hyp_refs_of' s)\" + 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]: "\if_live_then_nonz_cap'\ setObject p (ap::asidpool) \\rv. if_live_then_nonz_cap'\" apply (rule hoare_pre)