From 8f7b838b72c03588567e1b8a4d65f89d28f52288 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Wed, 25 Mar 2020 11:27:26 +1100 Subject: [PATCH] riscv crefine: update to Move_C/ArchMove_C includes Signed-off-by: Rafal Kolanski --- proof/crefine/RISCV64/ArchMove_C.thy | 48 +++++++ proof/crefine/RISCV64/CLevityCatch.thy | 4 +- proof/crefine/RISCV64/DetWP.thy | 2 +- proof/crefine/RISCV64/Include_C.thy | 13 -- proof/crefine/RISCV64/Move_C.thy | 178 ------------------------- 5 files changed, 51 insertions(+), 194 deletions(-) create mode 100644 proof/crefine/RISCV64/ArchMove_C.thy delete mode 100644 proof/crefine/RISCV64/Include_C.thy delete mode 100644 proof/crefine/RISCV64/Move_C.thy diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy new file mode 100644 index 000000000..44dbc7ab1 --- /dev/null +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -0,0 +1,48 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +(* Arch specific lemmas that should be moved into theory files before CRefine *) + +theory ArchMove_C +imports "../Move_C" +begin + +lemma word_shift_by_3: + "x * 8 = (x::'a::len word) << 3" + by (simp add: shiftl_t2n) + +lemma unat_mask_3_less_8: + "unat (p && mask 3 :: word64) < 8" + apply (rule unat_less_helper) + apply (rule order_le_less_trans, rule word_and_le1) + apply (simp add: mask_def) + done + +definition + user_word_at :: "machine_word \ machine_word \ kernel_state \ bool" +where + "user_word_at x p \ \s. is_aligned p 3 + \ pointerInUserData p s + \ x = word_rcat (map (underlying_memory (ksMachineState s)) + [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])" +definition + device_word_at :: "machine_word \ machine_word \ kernel_state \ bool" +where + "device_word_at x p \ \s. is_aligned p 3 + \ pointerInDeviceData p s + \ x = word_rcat (map (underlying_memory (ksMachineState s)) + [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])" + +(* FIXME: move to GenericLib *) +lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def] + +context begin interpretation Arch . + +(* FIXME RISCV: some 64-bit lemmas from X64's ArchMove_C will be needed here *) + +end + +end diff --git a/proof/crefine/RISCV64/CLevityCatch.thy b/proof/crefine/RISCV64/CLevityCatch.thy index 52f97c026..31badd5e7 100644 --- a/proof/crefine/RISCV64/CLevityCatch.thy +++ b/proof/crefine/RISCV64/CLevityCatch.thy @@ -6,8 +6,8 @@ theory CLevityCatch imports - Include_C - Move_C + "../Include_C" + ArchMove_C "CLib.LemmaBucket_C" "Lib.LemmaBucket" begin diff --git a/proof/crefine/RISCV64/DetWP.thy b/proof/crefine/RISCV64/DetWP.thy index 6943b4c12..3d2c12c49 100644 --- a/proof/crefine/RISCV64/DetWP.thy +++ b/proof/crefine/RISCV64/DetWP.thy @@ -6,7 +6,7 @@ *) theory DetWP -imports "Lib.DetWPLib" Include_C +imports "Lib.DetWPLib" "../Include_C" begin context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/proof/crefine/RISCV64/Include_C.thy b/proof/crefine/RISCV64/Include_C.thy deleted file mode 100644 index 2828d33fb..000000000 --- a/proof/crefine/RISCV64/Include_C.thy +++ /dev/null @@ -1,13 +0,0 @@ -(* - * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230) - * - * SPDX-License-Identifier: GPL-2.0-only - *) - -theory Include_C -imports - "CSpec.KernelInc_C" - "Refine.Refine" -begin - -end diff --git a/proof/crefine/RISCV64/Move_C.thy b/proof/crefine/RISCV64/Move_C.thy deleted file mode 100644 index cf5cac14a..000000000 --- a/proof/crefine/RISCV64/Move_C.thy +++ /dev/null @@ -1,178 +0,0 @@ -(* - * Copyright 2014, General Dynamics C4 Systems - * - * SPDX-License-Identifier: GPL-2.0-only -*) - -(* things that should be moved into first refinement *) - -theory Move_C -imports "Refine.Refine" -begin - -lemma finaliseCap_Reply: - "\Q (NullCap,NullCap) and K (isReplyCap cap)\ finaliseCapTrue_standin cap fin \Q\" - apply (rule NonDetMonadVCG.hoare_gen_asm) - apply (clarsimp simp: finaliseCapTrue_standin_def isCap_simps) - apply wp - done - -lemma cteDeleteOne_Reply: - "\st_tcb_at' P t and cte_wp_at' (isReplyCap o cteCap) slot\ cteDeleteOne slot \\_. st_tcb_at' P t\" - apply (simp add: cteDeleteOne_def unless_def split_def) - apply (wp finaliseCap_Reply isFinalCapability_inv getCTE_wp') - apply (clarsimp simp: cte_wp_at_ctes_of) - done - -lemma cancelSignal_st_tcb': - "\\s. t\t' \ st_tcb_at' P t' s\ cancelSignal t ntfn \\_. st_tcb_at' P t'\" - apply (simp add: cancelSignal_def Let_def) - apply (rule hoare_pre) - apply (wp sts_pred_tcb_neq' getNotification_wp|wpc)+ - apply clarsimp - done - -lemma cancelIPC_st_tcb_at': - "\\s. t\t' \ st_tcb_at' P t' s\ cancelIPC t \\_. st_tcb_at' P t'\" - apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv) - apply (wp sts_pred_tcb_neq' getEndpoint_wp cteDeleteOne_Reply getCTE_wp'|wpc)+ - apply (rule hoare_strengthen_post [where Q="\_. st_tcb_at' P t'"]) - apply (wp threadSet_st_tcb_at2) - apply simp - apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def) - apply (wp cancelSignal_st_tcb' sts_pred_tcb_neq' getEndpoint_wp gts_wp'|wpc)+ - apply clarsimp - done - -lemma suspend_st_tcb_at': - "\\s. (t\t' \ st_tcb_at' P t' s) \ (t=t' \ P Inactive)\ - suspend t - \\_. st_tcb_at' P t'\" - apply (simp add: suspend_def unless_def) - unfolding updateRestartPC_def - apply (cases "t=t'") - apply (simp|wp cancelIPC_st_tcb_at' sts_st_tcb')+ - done - -lemma to_bool_if: - "(if w \ 0 then 1 else 0) = (if to_bool w then 1 else 0)" - by (auto simp: to_bool_def) - -(* FIXME MOVE *) -lemma typ_at'_no_0_objD: - "typ_at' P p s \ no_0_obj' s \ p \ 0" - by (cases "p = 0" ; clarsimp) - -(* FIXME ARMHYP MOVE *) -lemma ko_at'_not_NULL: - "\ ko_at' ko p s ; no_0_obj' s\ - \ p \ 0" - by (fastforce simp: word_gt_0 typ_at'_no_0_objD) - -context begin interpretation Arch . (*FIXME: arch_split*) - -crunches setVMRoot - for ksQ'[wp]: "\s. P (ksReadyQueues s)" - -(* FIXME move *) -lemma setVMRoot_valid_queues': - "\ valid_queues' \ setVMRoot a \ \_. valid_queues' \" - by (rule valid_queues_lift'; wp) - -(* FIXME: change the original to be predicated! *) -crunch pred_tcb_at'2[wp]: doMachineOp "\s. P (pred_tcb_at' a b p s)" - (simp: crunch_simps) - -end - -(* FIXME move *) -lemma shiftr_and_eq_shiftl: - fixes w x y :: "'a::len word" - assumes r: "(w >> n) && x = y" - shows "w && (x << n) = (y << n)" - using assms - proof - - { fix i - assume i: "i < LENGTH('a)" - hence "test_bit (w && (x << n)) i \ test_bit (y << n) i" - using word_eqD[where x="i-n", OF r] - by (cases "n \ i") (auto simp: nth_shiftl nth_shiftr) - } - thus ?thesis using word_eq_iff by blast - qed - -(* FIXME: move *) -lemma cond_throw_whenE: - "(if P then f else throwError e) = (whenE (\ P) (throwError e) >>=E (\_. f))" - by (auto split: if_splits - simp: throwError_def bindE_def - whenE_def bind_def returnOk_def return_def) - -lemma ksPSpace_update_eq_ExD: - "s = t\ ksPSpace := ksPSpace s\ - \ \ps. s = t \ ksPSpace := ps \" - by (erule exI) - -lemma threadGet_wp'': - "\\s. \v. obj_at' (\tcb. f tcb = v) thread s \ P v s\ threadGet f thread \P\" - apply (rule hoare_pre) - apply (rule threadGet_wp) - apply (clarsimp simp: obj_at'_def) - done - -lemma tcbSchedEnqueue_queued_queues_inv: - "\\s. obj_at' tcbQueued t s \ P (ksReadyQueues s) \ tcbSchedEnqueue t \\_ s. P (ksReadyQueues s)\" - unfolding tcbSchedEnqueue_def unless_def - apply (wpsimp simp: if_apply_def2 wp: threadGet_wp) - apply normalise_obj_at' - done - -lemma addToBitmap_sets_L1Bitmap_same_dom: - "\\s. p \ maxPriority \ d' = d \ addToBitmap d' p - \\rv s. ksReadyQueuesL1Bitmap s d \ 0 \" - unfolding addToBitmap_def bitmap_fun_defs - apply wpsimp - apply (clarsimp simp: maxPriority_def numPriorities_def word_or_zero le_def - prioToL1Index_max[simplified wordRadix_def, simplified]) - done - -crunch ksReadyQueuesL1Bitmap[wp]: setQueue "\s. P (ksReadyQueuesL1Bitmap s)" - -lemma tcb_in_cur_domain'_def': - "tcb_in_cur_domain' t = (\s. obj_at' (\tcb. tcbDomain tcb = ksCurDomain s) t s)" - unfolding tcb_in_cur_domain'_def - by (auto simp: obj_at'_def) - -lemma sts_running_ksReadyQueuesL1Bitmap[wp]: - "\\s. P (ksReadyQueuesL1Bitmap s)\ - setThreadState Structures_H.thread_state.Running t - \\_ s. P (ksReadyQueuesL1Bitmap s)\" - unfolding setThreadState_def - apply wp - apply (rule hoare_pre_cont) - apply (wpsimp simp: if_apply_def2 - wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ - done - -lemma sts_running_ksReadyQueuesL2Bitmap[wp]: - "\\s. P (ksReadyQueuesL2Bitmap s)\ - setThreadState Structures_H.thread_state.Running t - \\_ s. P (ksReadyQueuesL2Bitmap s)\" - unfolding setThreadState_def - apply wp - apply (rule hoare_pre_cont) - apply (wpsimp simp: if_apply_def2 - wp: hoare_drop_imps hoare_vcg_disj_lift threadSet_tcbState_st_tcb_at')+ - done - -lemma asUser_obj_at_not_queued[wp]: - "\obj_at' (\tcb. \ tcbQueued tcb) p\ asUser t m \\rv. obj_at' (\tcb. \ tcbQueued tcb) p\" - apply (simp add: asUser_def split_def) - apply (wp hoare_drop_imps | simp)+ - done - -lemma ko_at'_obj_at'_field: - "ko_at' ko (t s) s \ obj_at' (\ko'. f ko' = f ko) (t s) s" - by (erule obj_at'_weakenE, simp) - -end