diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy new file mode 100644 index 000000000..1184e0597 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchArch_AI +imports "../Arch_AI" +begin + +context Arch begin + +named_theorems Arch_AI_asms + +definition "Arch_AI_dummy_const \ (1 :: nat)" + +lemma Arch_AI_trivial_result[Arch_AI_asms]: + "Arch_AI_dummy_const > 0" + by (simp add: Arch_AI_dummy_const_def) + +end + +interpretation Arch_AI?: Arch_AI + where Arch_AI_dummy_const = Arch.Arch_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Arch_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy b/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy new file mode 100644 index 000000000..2bfbb1c7e --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchCNodeInv_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchCNodeInv_AI +imports "../CNodeInv_AI" +begin + +context Arch begin + +named_theorems CNodeInv_AI_asms + +definition "CNodeInv_AI_dummy_const \ (1 :: nat)" + +lemma CNodeInv_AI_trivial_result[CNodeInv_AI_asms]: + "CNodeInv_AI_dummy_const > 0" + by (simp add: CNodeInv_AI_dummy_const_def) + +end + +interpretation CNodeInv_AI?: CNodeInv_AI + where CNodeInv_AI_dummy_const = Arch.CNodeInv_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact CNodeInv_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy new file mode 100644 index 000000000..d6b290506 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchDetype_AI +imports "../Detype_AI" +begin + +context Arch begin + +named_theorems Detype_AI_asms + +definition "Detype_AI_dummy_const \ (1 :: nat)" + +lemma Detype_AI_trivial_result[Detype_AI_asms]: + "Detype_AI_dummy_const > 0" + by (simp add: Detype_AI_dummy_const_def) + +end + +interpretation Detype_AI?: Detype_AI + where Detype_AI_dummy_const = Arch.Detype_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Detype_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy new file mode 100644 index 000000000..03fbc9e67 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchFinalise_AI +imports "../Finalise_AI" +begin + +context Arch begin + +named_theorems Finalise_AI_asms + +definition "Finalise_AI_dummy_const \ (1 :: nat)" + +lemma Finalise_AI_trivial_result[Finalise_AI_asms]: + "Finalise_AI_dummy_const > 0" + by (simp add: Finalise_AI_dummy_const_def) + +end + +interpretation Finalise_AI?: Finalise_AI + where Finalise_AI_dummy_const = Arch.Finalise_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Finalise_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy new file mode 100644 index 000000000..22dd03482 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchInterrupt_AI +imports "../Interrupt_AI" +begin + +context Arch begin + +named_theorems Interrupt_AI_asms + +definition "Interrupt_AI_dummy_const \ (1 :: nat)" + +lemma Interrupt_AI_trivial_result[Interrupt_AI_asms]: + "Interrupt_AI_dummy_const > 0" + by (simp add: Interrupt_AI_dummy_const_def) + +end + +interpretation Interrupt_AI?: Interrupt_AI + where Interrupt_AI_dummy_const = Arch.Interrupt_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Interrupt_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy new file mode 100644 index 000000000..fae986a1d --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchIpcCancel_AI.thy @@ -0,0 +1,33 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchIpcCancel_AI +imports "../IpcCancel_AI" +begin + +context Arch begin + +named_theorems IpcCancel_AI_asms + +definition "IpcCancel_AI_dummy_const \ (1 :: nat)" + +lemma IpcCancel_AI_trivial_result[IpcCancel_AI_asms]: + "IpcCancel_AI_dummy_const > 0" + by (simp add: IpcCancel_AI_dummy_const_def) + +end + +interpretation IpcCancel_AI: IpcCancel_AI + where IpcCancel_AI_dummy_const = Arch.IpcCancel_AI_dummy_const proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact IpcCancel_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy new file mode 100644 index 000000000..df6d83b0b --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchIpc_AI +imports "../Ipc_AI" +begin + +context Arch begin + +named_theorems Ipc_AI_asms + +definition "Ipc_AI_dummy_const \ (1 :: nat)" + +lemma Ipc_AI_trivial_result[Ipc_AI_asms]: + "Ipc_AI_dummy_const > 0" + by (simp add: Ipc_AI_dummy_const_def) + +end + +interpretation Ipc_AI?: Ipc_AI + where Ipc_AI_dummy_const = Arch.Ipc_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Ipc_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy new file mode 100644 index 000000000..b6423d61f --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -0,0 +1,78 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +(* + Arch-specific retype invariants +*) + +theory ArchRetype_AI +imports "../Retype_AI" +begin + + + +context Arch begin + +named_theorems Retype_AI_asms + +lemma clearMemoryVM_return[simp, Retype_AI_asms]: + "clearMemoryVM a b = return ()" + by (simp add: clearMemoryVM_def) + +end + + +interpretation Retype_AI?: Retype_AI + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Retype_AI_asms)?) + qed + +context Arch begin global_naming ARM + +lemma retype_region_plain_invs: + "\invs and caps_no_overlap ptr sz and pspace_no_overlap ptr sz + and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} + and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1} + and K (ty = Structures_A.CapTableObject \ 0 < us) + and K (range_cover ptr sz (obj_bits_api ty us) n) + and K (ty \ ArchObject PageDirectoryObj)\ + retype_region ptr n us ty \\rv. invs\" + apply (rule hoare_gen_asm) + apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs]) + apply (simp add: post_retype_invs_def) + done + +lemma storeWord_um_eq_0: + "\\m. underlying_memory m p = 0\ + storeWord x 0 + \\_ m. underlying_memory m p = 0\" + by (simp add: storeWord_def word_rsplit_0 | wp)+ + +lemma clearMemory_um_eq_0: + "\\m. underlying_memory m p = 0\ + clearMemory ptr bits + \\_ m. underlying_memory m p = 0\" + apply (clarsimp simp: clearMemory_def) + apply (wp mapM_x_wp_inv | simp)+ + apply (rule hoare_pre) + apply (wp hoare_drop_imps storeWord_um_eq_0) + apply (fastforce simp: ignore_failure_def split: split_if_asm) + done + +lemma cleanCacheRange_PoU_um_inv[wp]: + "\\m. P (underlying_memory m)\ + cleanCacheRange_PoU ptr w p + \\_ m. P (underlying_memory m)\" + by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def + split_def | wp)+ +end + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy new file mode 100644 index 000000000..0d46d47a0 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchSchedule_AI +imports "../Schedule_AI" +begin + +context Arch begin + +named_theorems Schedule_AI_asms + +definition "Schedule_AI_dummy_const \ (1 :: nat)" + +lemma Schedule_AI_trivial_result[Schedule_AI_asms]: + "Schedule_AI_dummy_const > 0" + by (simp add: Schedule_AI_dummy_const_def) + +end + +interpretation Schedule_AI: Schedule_AI + where Schedule_AI_dummy_const = Arch.Schedule_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Schedule_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy new file mode 100644 index 000000000..a257ca089 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchTcb_AI +imports "../Tcb_AI" +begin + +context Arch begin + +named_theorems Tcb_AI_asms + +definition "Tcb_AI_dummy_const \ (1 :: nat)" + +lemma Tcb_AI_trivial_result[Tcb_AI_asms]: + "Tcb_AI_dummy_const > 0" + by (simp add: Tcb_AI_dummy_const_def) + +end + +interpretation Tcb_AI?: Tcb_AI + where Tcb_AI_dummy_const = Arch.Tcb_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Tcb_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy new file mode 100644 index 000000000..549ee2c18 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -0,0 +1,34 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchUntyped_AI +imports "../Untyped_AI" +begin + +context Arch begin + +named_theorems Untyped_AI_asms + +definition "Untyped_AI_dummy_const \ (1 :: nat)" + +lemma Untyped_AI_trivial_result[Untyped_AI_asms]: + "Untyped_AI_dummy_const > 0" + by (simp add: Untyped_AI_dummy_const_def) + +end + +interpretation Untyped_AI?: Untyped_AI + where Untyped_AI_dummy_const = Arch.Untyped_AI_dummy_const + proof goal_cases + interpret Arch . + case 1 show ?case by (intro_locales; (unfold_locales, fact Untyped_AI_asms)?) + qed + +end \ No newline at end of file diff --git a/proof/invariant-abstract/Arch_AI.thy b/proof/invariant-abstract/Arch_AI.thy index 2222ac7dd..9f539aeb9 100644 --- a/proof/invariant-abstract/Arch_AI.thy +++ b/proof/invariant-abstract/Arch_AI.thy @@ -13,9 +13,17 @@ Top level architecture related proofs. *) theory Arch_AI -imports Untyped_AI Finalise_AI +imports "./$L4V_ARCH/ArchUntyped_AI" "./$L4V_ARCH/ArchFinalise_AI" begin +locale Arch_AI begin + +extend_locale + fixes Arch_AI_dummy_const :: nat + assumes Arch_AI_trivial_asm: "Arch_AI_dummy_const > 0" + +end + context Arch begin global_naming ARM (*FIXME: arch_split*) definition diff --git a/proof/invariant-abstract/BCorres2_AI.thy b/proof/invariant-abstract/BCorres2_AI.thy index 201711102..da1aa7444 100644 --- a/proof/invariant-abstract/BCorres2_AI.thy +++ b/proof/invariant-abstract/BCorres2_AI.thy @@ -12,7 +12,7 @@ theory BCorres2_AI imports EmptyFail_AI "../../lib/BCorres_UL" - CNodeInv_AI + "./$L4V_ARCH/ArchCNodeInv_AI" begin definition all_but_exst where diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index c611b72c8..e63dc9d43 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -14,9 +14,17 @@ recursive revoke and delete operations. *) theory CNodeInv_AI -imports Ipc_AI +imports "./$L4V_ARCH/ArchIpc_AI" begin +locale CNodeInv_AI begin + +extend_locale + fixes CNodeInv_AI_dummy_const :: nat + assumes CNodeInv_AI_trivial_asm: "CNodeInv_AI_dummy_const > 0" + +end + primrec valid_cnode_inv :: "cnode_invocation \ 'z::state_ext state \ bool" where diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 2c2df40ba..fa448fb77 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -9,9 +9,17 @@ *) theory Detype_AI -imports Retype_AI +imports "./$L4V_ARCH/ArchRetype_AI" begin +locale Detype_AI begin + +extend_locale + fixes Detype_AI_dummy_const :: nat + assumes Detype_AI_trivial_asm: "Detype_AI_dummy_const > 0" + +end + lemma obj_at_detype[simp]: "obj_at P p (detype S s) = (p \ S \ obj_at P p s)" by (clarsimp simp: obj_at_def detype_def) diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 520013769..f4188a55a 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -10,11 +10,19 @@ theory Finalise_AI imports - IpcCancel_AI + "./$L4V_ARCH/ArchIpcCancel_AI" InterruptAcc_AI - Retype_AI + "./$L4V_ARCH/ArchRetype_AI" begin +locale Finalise_AI begin + +extend_locale + fixes Finalise_AI_dummy_const :: nat + assumes Finalise_AI_trivial_asm: "Finalise_AI_dummy_const > 0" + +end + context begin interpretation Arch . requalify_consts diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 890804af5..17a4c0eb3 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -13,9 +13,17 @@ Refinement for interrupt controller operations *) theory Interrupt_AI -imports Ipc_AI +imports "./$L4V_ARCH/ArchIpc_AI" begin +locale Interrupt_AI begin + +extend_locale + fixes Interrupt_AI_dummy_const :: nat + assumes Interrupt_AI_trivial_asm: "Interrupt_AI_dummy_const > 0" + +end + context begin interpretation Arch . requalify_consts maxIRQ diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 2e43500d9..af9e8f802 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -9,9 +9,17 @@ *) theory IpcCancel_AI -imports Schedule_AI +imports "./$L4V_ARCH/ArchSchedule_AI" begin +locale IpcCancel_AI begin + +extend_locale + fixes IpcCancel_AI_dummy_const :: nat + assumes IpcCancel_AI_trivial_asm: "IpcCancel_AI_dummy_const > 0" + +end + lemma blocked_cancel_ipc_simple: "\tcb_at t\ blocked_cancel_ipc ts t \\rv. st_tcb_at simple t\" by (simp add: blocked_cancel_ipc_def | wp sts_st_tcb_at')+ diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index f3f0da6af..2354bc6e8 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -9,9 +9,17 @@ *) theory Ipc_AI -imports Finalise_AI +imports "./$L4V_ARCH/ArchFinalise_AI" begin +locale Ipc_AI begin + +extend_locale + fixes Ipc_AI_dummy_const :: nat + assumes Ipc_AI_trivial_asm: "Ipc_AI_dummy_const > 0" + +end + declare if_cong[cong del] lemmas lookup_slot_wrapper_defs[simp] = diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index 312de32b6..fafdc51ef 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -20,10 +20,14 @@ context begin interpretation Arch . requalify_facts global_refs_kheap +requalify_consts clearMemoryVM + end declare global_refs_kheap[simp] +locale Retype_AI begin + lemma upto_enum_inc_1: "a < 2^word_bits - 1 \ [(0::machine_word).e.1 + a] = [0.e.a] @ [(1+a)]" apply (simp add:upto_enum_word) @@ -83,17 +87,12 @@ proof - done qed -context Arch begin global_naming ARM (*FIXME: arch_split*) -lemma clearMemoryVM_return [simp]: + +extend_locale + assumes clearMemoryVM_return [simp]: "clearMemoryVM a b = return ()" - by (simp add: clearMemoryVM_def storeWordVM_def) - - -lemma clearMemoryVM_return_raw: - "clearMemoryVM = (\x y. return ())" - apply (rule ext)+ - by (simp add: clearMemoryVM_def storeWordVM_def) -end + +lemmas clearMemoryVM_return_raw = clearMemoryVM_return[abs_def] lemma unat_of_nat_minus_1: "\n < 2^len_of TYPE('a);n\ 0\ \ (unat (((of_nat n):: 'a :: len word) - 1)) = n - 1" @@ -468,12 +467,12 @@ lemma word_plus_mono_right_split: done lemmas word32_plus_mono_right_split = word_plus_mono_right_split[where 'a=32, folded word_bits_def] - +end (* range_cover locale: proves properties when a small range is inside in a large range *) -locale range_cover = +locale range_cover = Retype_AI + fixes ptr :: "'a :: len word" and sz sbit n assumes aligned: "is_aligned ptr sbit" @@ -641,6 +640,11 @@ lemma range_cover_base_le: end +context Retype_AI begin + +lemmas range_cover_def = + range_cover_def[simplified range_cover_axioms_def Retype_AI_axioms, simplified] + lemma range_cover_subset: fixes ptr :: "'a :: len word" assumes cover: "range_cover ptr sz sbit n" @@ -959,6 +963,8 @@ lemma shiftr_mask_cmp: apply (simp add:le_mask_iff shiftr_shiftr) done +end + context Arch begin global_naming ARM (*FIXME: arch_split*) definition "no_gs_types \ UNIV - {Structures_A.CapTableObject, @@ -1000,6 +1006,7 @@ lemma range_cover_not_zero: apply simp done +context Retype_AI begin lemma range_cover_not_zero_shift: "\n \ 0; range_cover (ptr :: 'a :: len word) sz bits n; gbits \ bits\ @@ -1206,6 +1213,7 @@ done crunch valid_pspace: do_machine_op "valid_pspace" +end context Arch begin global_naming ARM (*FIXME: arch_split*) declare store_pde_state_refs_of [wp] @@ -1863,6 +1871,8 @@ lemma init_arch_objects_invs_from_restricted: done end +context Retype_AI begin + lemma retype_region_aligned_for_init[wp]: "\\s. range_cover ptr sz (obj_bits_api new_type obj_sz) n\ retype_region ptr n obj_sz new_type @@ -2363,6 +2373,8 @@ lemma valid_arch_obj_default: apply (simp add: valid_arch_obj_default') done +end + context Arch begin global_naming ARM (*FIXME: arch_split*) lemma vs_lookup_trans_sub2: assumes ko: "\ko p. \ ko_at ko p s; vs_refs ko \ {} \ \ obj_at (\ko'. vs_refs ko \ vs_refs ko') p s'" @@ -2440,7 +2452,7 @@ lemma usable_range_emptyD: done -context begin interpretation Arch . (*FIXME: arch_split*) +context Retype_AI begin interpretation Arch . (*FIXME: arch_split*) lemma valid_untyped_helper: assumes valid_c : "s \ c" and cte_at : "cte_wp_at (op = c) q s" @@ -2518,7 +2530,7 @@ end -locale retype_region_proofs_gen = +locale retype_region_proofs_gen = Retype_AI + fixes s ty us ptr sz n ps s' assumes vp: "valid_pspace s" and vm: "valid_mdb s" @@ -3257,7 +3269,11 @@ lemma post_retype_invs: end end -context begin interpretation Arch . (*FIXME: arch_split*) +context Retype_AI begin interpretation Arch . (*FIXME: arch_split*) + +lemmas retype_region_proofs_gen_intro = + retype_region_proofs_gen.intro[simplified Retype_AI_axioms retype_region_proofs_gen_axioms_def] + lemma use_retype_region_proofs': assumes x: "\s. \ retype_region_proofs s ty us ptr sz n; P s \ \ Q (retype_addrs ptr ty n us) (s\kheap := @@ -3278,12 +3294,14 @@ lemma use_retype_region_proofs': foldr_upd_app_if fun_upd_def[symmetric]) apply safe apply (rule x) - apply (rule retype_region_proofs.intro[OF retype_region_proofs_gen.intro], simp_all)[1] - apply (simp add: range_cover_def obj_bits_api_def + apply (rule retype_region_proofs.intro[OF retype_region_proofs_gen_intro], simp_all)[1] + apply (clarsimp simp add: range_cover_def obj_bits_api_def slot_bits_def word_bits_def cte_level_bits_def)+ done end +context Retype_AI begin + lemmas use_retype_region_proofs = use_retype_region_proofs'[where Q="\_. Q" and P=Q, simplified] for Q @@ -3408,50 +3426,10 @@ lemma retype_region_post_retype_invs: done -context Arch begin global_naming ARM (*FIXME: arch_split*) -lemma retype_region_plain_invs: - "\invs and caps_no_overlap ptr sz and pspace_no_overlap ptr sz - and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} - and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1} - and K (ty = Structures_A.CapTableObject \ 0 < us) - and K (range_cover ptr sz (obj_bits_api ty us) n) - and K (ty \ ArchObject PageDirectoryObj)\ - retype_region ptr n us ty \\rv. invs\" - apply (rule hoare_gen_asm) - apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs]) - apply (simp add: post_retype_invs_def) - done -end - lemma subset_not_le_trans: "\\ A \ B; C \ B\ \ \ A \ C" by auto -context Arch begin global_naming ARM (*FIXME: arch_split*) -lemma storeWord_um_eq_0: - "\\m. underlying_memory m p = 0\ - storeWord x 0 - \\_ m. underlying_memory m p = 0\" - by (simp add: storeWord_def word_rsplit_0 | wp)+ -lemma clearMemory_um_eq_0: - "\\m. underlying_memory m p = 0\ - clearMemory ptr bits - \\_ m. underlying_memory m p = 0\" - apply (clarsimp simp: clearMemory_def) - apply (wp mapM_x_wp_inv | simp)+ - apply (rule hoare_pre) - apply (wp hoare_drop_imps storeWord_um_eq_0) - apply (fastforce simp: ignore_failure_def split: split_if_asm) - done - -lemma cleanCacheRange_PoU_um_inv[wp]: - "\\m. P (underlying_memory m)\ - cleanCacheRange_PoU ptr w p - \\_ m. P (underlying_memory m)\" - by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def - split_def | wp)+ -end - lemma cte_wp_at_trans_state[simp]: "cte_wp_at P ptr (kheap_update f (trans_state f' s)) = cte_wp_at P ptr (kheap_update f s)" apply (simp add: trans_state_update[symmetric] del: trans_state_update) @@ -3542,3 +3520,5 @@ lemma no_cap_to_obj_with_diff_ref_more_update[simp]: no_cap_to_obj_with_diff_ref cap sl s" by (simp add: no_cap_to_obj_with_diff_ref_def) end + +end diff --git a/proof/invariant-abstract/Schedule_AI.thy b/proof/invariant-abstract/Schedule_AI.thy index d778276ee..be04469d9 100644 --- a/proof/invariant-abstract/Schedule_AI.thy +++ b/proof/invariant-abstract/Schedule_AI.thy @@ -12,6 +12,14 @@ theory Schedule_AI imports VSpace_AI begin +locale Schedule_AI begin + +extend_locale + fixes Schedule_AI_dummy_const :: nat + assumes Schedule_AI_trivial_asm: "Schedule_AI_dummy_const > 0" + +end + context begin interpretation Arch . (* FIXME arch_split: some of these could be moved to generic theories so they don't need to be unqualified. *) diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 6c645346f..f47cea92f 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -15,9 +15,9 @@ Refinement for handleEvent and syscalls theory Syscall_AI imports BCorres2_AI - Tcb_AI - Arch_AI - Interrupt_AI + "./$L4V_ARCH/ArchTcb_AI" + "./$L4V_ARCH/ArchArch_AI" + "./$L4V_ARCH/ArchInterrupt_AI" begin lemma schedule_invs[wp]: "\invs\ (Schedule_A.schedule :: (unit,det_ext) s_monad) \\rv. invs\" diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 7c4d53217..5103eb219 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -9,8 +9,16 @@ *) theory Tcb_AI -imports CNodeInv_AI +imports "./$L4V_ARCH/ArchCNodeInv_AI" begin + +locale Tcb_AI begin + +extend_locale + fixes Tcb_AI_dummy_const :: nat + assumes Tcb_AI_trivial_asm: "Tcb_AI_dummy_const > 0" + +end lemma ct_in_state_weaken: "\ ct_in_state Q s; \st. Q st \ P st \ \ ct_in_state P s" diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index 6a4d82d00..d6589365f 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -11,8 +11,17 @@ (* Proofs about untyped invocations. *) theory Untyped_AI -imports Detype_AI +imports "./$L4V_ARCH/ArchDetype_AI" begin + +locale Untyped_AI begin + +extend_locale + fixes Untyped_AI_dummy_const :: nat + assumes Untyped_AI_trivial_asm: "Untyped_AI_dummy_const > 0" + +end + context begin interpretation Arch . requalify_consts