From 375d6a5815d96e3fa1f71478c02105d6b78ccab5 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Mon, 9 Dec 2024 18:53:10 +1100 Subject: [PATCH] aarch64 refine: minimal fixups for arch-split tcb_cte_cases machinery Signed-off-by: Rafal Kolanski --- proof/refine/AARCH64/CNodeInv_R.thy | 1 + proof/refine/AARCH64/CSpace1_R.thy | 1 + proof/refine/AARCH64/CSpace_R.thy | 1 + proof/refine/AARCH64/Ipc_R.thy | 2 ++ proof/refine/AARCH64/KHeap_R.thy | 4 +++- proof/refine/AARCH64/TcbAcc_R.thy | 1 + proof/refine/AARCH64/Tcb_R.thy | 2 ++ proof/refine/AARCH64/orphanage/Orphanage.thy | 1 + 8 files changed, 12 insertions(+), 1 deletion(-) diff --git a/proof/refine/AARCH64/CNodeInv_R.thy b/proof/refine/AARCH64/CNodeInv_R.thy index f4379784f7..aead729009 100644 --- a/proof/refine/AARCH64/CNodeInv_R.thy +++ b/proof/refine/AARCH64/CNodeInv_R.thy @@ -5729,6 +5729,7 @@ lemma cte_wp_at_disj_eq': lemma valid_Zombie_cte_at': "\ s \' Zombie p zt m; n < zombieCTEs zt \ \ cte_at' (p + (of_nat n * 2^cteSizeBits)) s" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (clarsimp simp: valid_cap'_def split: zombie_type.split_asm) apply (clarsimp simp: obj_at'_def objBits_simps) apply (subgoal_tac "tcb_cte_cases (of_nat n * 2^cteSizeBits) \ None") diff --git a/proof/refine/AARCH64/CSpace1_R.thy b/proof/refine/AARCH64/CSpace1_R.thy index 8cff61483d..322e8b604c 100644 --- a/proof/refine/AARCH64/CSpace1_R.thy +++ b/proof/refine/AARCH64/CSpace1_R.thy @@ -212,6 +212,7 @@ lemma tcb_cases_related: "tcb_cap_cases ref = Some (getF, setF, restr) \ \getF' setF'. (\x. tcb_cte_cases (cte_map (x, ref) - x) = Some (getF', setF')) \ (\tcb tcb'. tcb_relation tcb tcb' \ cap_relation (getF tcb) (cteCap (getF' tcb')))" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) by (simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1 cte_map_def' tcb_relation_def split: if_split_asm) diff --git a/proof/refine/AARCH64/CSpace_R.thy b/proof/refine/AARCH64/CSpace_R.thy index acabae6d98..6778d2349e 100644 --- a/proof/refine/AARCH64/CSpace_R.thy +++ b/proof/refine/AARCH64/CSpace_R.thy @@ -4204,6 +4204,7 @@ lemma setupReplyMaster_invs'[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t\ setupReplyMaster t \\rv. invs'\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre) apply (wp setupReplyMaster_valid_pspace' sch_act_wf_lift tcb_in_cur_domain'_lift ct_idle_or_in_cur_domain'_lift diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index 89fe5e8fbe..6647567639 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -1649,6 +1649,7 @@ lemma doFaultTransfer_invs[wp]: lemma lookupIPCBuffer_valid_ipc_buffer [wp]: "\valid_objs'\ VSpace_H.lookupIPCBuffer b s \case_option \ valid_ipc_buffer_ptr'\" unfolding lookupIPCBuffer_def AARCH64_H.lookupIPCBuffer_def + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: Let_def getSlotCap_def getThreadBufferSlot_def locateSlot_conv threadGet_def comp_def) apply (wp getCTE_wp getObject_tcb_wp | wpc)+ @@ -3534,6 +3535,7 @@ lemma setupCallerCap_ifunsafe[wp]: \\rv. if_unsafe_then_cap'\" unfolding setupCallerCap_def getThreadCallerSlot_def getThreadReplySlot_def locateSlot_conv + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (wp getSlotCap_cte_wp_at | simp add: unique_master_reply_cap' | strengthen eq_imp_strg | wp (once) hoare_drop_imp[where f="getCTE rs" for rs])+ diff --git a/proof/refine/AARCH64/KHeap_R.thy b/proof/refine/AARCH64/KHeap_R.thy index cfc92c72d6..7671db1cb2 100644 --- a/proof/refine/AARCH64/KHeap_R.thy +++ b/proof/refine/AARCH64/KHeap_R.thy @@ -245,6 +245,7 @@ lemma updateObject_cte_is_tcb_or_cte: \ ko' = KOTCB (setF (\x. cte) tcb) \ is_aligned q tcbBlockSizeBits \ ps_clear q tcbBlockSizeBits s) \ (\cte'. ko = KOCTE cte' \ ko' = KOCTE cte \ s' = s \ p = q \ is_aligned p cte_level_bits \ ps_clear p cte_level_bits s)" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (clarsimp simp: updateObject_cte typeError_def alignError_def tcbVTableSlot_def tcbCTableSlot_def to_bl_1 rev_take objBits_simps' in_monad map_bits_to_bl cte_level_bits_def in_magnitude_check @@ -1199,6 +1200,7 @@ lemma typ_at'_valid_obj'_lift: assumes P: "\P T p. \\s. P (typ_at' T p s)\ f \\rv s. P (typ_at' T p s)\" notes [wp] = hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_const_Ball_lift typ_at_lifts [OF P] shows "\\s. valid_obj' obj s\ f \\rv s. valid_obj' obj s\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (cases obj; simp add: valid_obj'_def hoare_TrueI) apply (rename_tac endpoint) apply (case_tac endpoint; simp add: valid_ep'_def, wp) @@ -1210,7 +1212,7 @@ lemma typ_at'_valid_obj'_lift: apply (case_tac "tcbState tcb"; simp add: valid_tcb'_def valid_tcb_state'_def split_def opt_tcb_at'_def valid_bound_ntfn'_def; - wpsimp wp: hoare_case_option_wp hoare_case_option_wp2; + wpsimp wp: hoare_case_option_wp hoare_case_option_wp2 valid_arch_tcb_lift' P; (clarsimp split: option.splits)?) apply (wpsimp simp: valid_cte'_def) apply wp diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy index daf0e03a93..4328937651 100644 --- a/proof/refine/AARCH64/TcbAcc_R.thy +++ b/proof/refine/AARCH64/TcbAcc_R.thy @@ -4437,6 +4437,7 @@ qed lemma cte_at_tcb_at_32': "tcb_at' t s \ cte_at' (t + 32) s" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (simp add: cte_at'_obj_at') apply (rule disjI2, rule bexI[where x=32]) apply simp diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy index d303b7c184..9e7b2892ad 100644 --- a/proof/refine/AARCH64/Tcb_R.thy +++ b/proof/refine/AARCH64/Tcb_R.thy @@ -1014,6 +1014,7 @@ lemma threadcontrol_corres_helper4: (checkCapAt (capability.ThreadCap a) (cte_map slot) (assertDerived (cte_map (ab, ba)) ac (cteInsert ac (cte_map (ab, ba)) (cte_map (a, tcb_cnode_index 4))))) \\_ s. sym_heap_sched_pointers s \ valid_sched_pointers s \ valid_tcbs' s\" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (wpsimp wp: | strengthen invs_sym_heap_sched_pointers invs_valid_sched_pointers invs_valid_objs' valid_objs'_valid_tcbs')+ @@ -1303,6 +1304,7 @@ proof - od odE od) g')" (is "corres _ ?T2_pre ?T2_pre' _ _") using z u + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply - apply (rule corres_guard_imp[where P=P and P'=P' and Q="P and cte_at (a, tcb_cnode_index 4)" diff --git a/proof/refine/AARCH64/orphanage/Orphanage.thy b/proof/refine/AARCH64/orphanage/Orphanage.thy index 8e6994926e..00bdec740a 100644 --- a/proof/refine/AARCH64/orphanage/Orphanage.thy +++ b/proof/refine/AARCH64/orphanage/Orphanage.thy @@ -1669,6 +1669,7 @@ lemma tc_no_orphans: K (valid_option_prio d \ valid_option_prio mcp) \ invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \ \rv s. no_orphans s \" + supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *) apply (rule hoare_gen_asm) apply (rule hoare_gen_asm) apply (rule hoare_gen_asm)