From 29eb636d31e1c45360c519058e8d8214786611ce Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 26 Nov 2014 15:14:39 +1100 Subject: [PATCH] re-establish InfoFlow; generalising ptable_xn UserOp_IF had its own way of extracting the XN bit from page tables. This is now unified with the existing functions in ADT_AI, which also means that the proof for XN bit equality is basically the same as for pt_rights and pt_lift. --- proof/access-control/ADT_AC.thy | 18 +- proof/infoflow/ADT_IF.thy | 43 +-- proof/infoflow/ADT_IF_Refine.thy | 11 +- proof/infoflow/ADT_IF_Refine_C.thy | 25 +- proof/infoflow/Example_Valid_State.thy | 8 - proof/infoflow/Example_Valid_StateH.thy | 11 +- proof/infoflow/Noninterference.thy | 3 - proof/infoflow/UserOp_IF.thy | 276 +++++++----------- proof/invariant-abstract/ADT_AI.thy | 66 ++--- proof/invariant-abstract/AInvs.thy | 9 +- proof/invariant-abstract/Deterministic_AI.thy | 30 +- 11 files changed, 212 insertions(+), 288 deletions(-) diff --git a/proof/access-control/ADT_AC.thy b/proof/access-control/ADT_AC.thy index a6042a236..e10ee6c83 100644 --- a/proof/access-control/ADT_AC.thy +++ b/proof/access-control/ADT_AC.thy @@ -60,12 +60,12 @@ lemma pd_of_thread_page_directory_at: lemma ptr_offset_in_ptr_range: "\ invs s; get_page_info (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = - Some (a, aa, b); x \ kernel_mappings; + Some (base, sz, attr, r); x \ kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \ arm_global_pd (arch_state s) \ - \ ptrFromPAddr a + (x && mask aa) \ ptr_range (ptrFromPAddr a) aa" + \ ptrFromPAddr base + (x && mask sz) \ ptr_range (ptrFromPAddr base) sz" apply (simp add: ptr_range_def mask_def) apply (rule conjI) - apply (rule_tac b="2 ^ aa - 1" in word_plus_mono_right2) + apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2) apply (frule some_get_page_info_umapsD) apply (clarsimp simp: get_pd_of_thread_reachable invs_arch_objs invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ @@ -160,14 +160,14 @@ lemma pt_in_pd_page_table_at: done lemma get_page_info_state_objs_to_policy: - "\ invs s; auth \ vspace_cap_rights_to_auth b; + "\ invs s; auth \ vspace_cap_rights_to_auth r; get_page_info (\obj. get_arch_obj (kheap s obj)) - (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, b); + (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) tcb \ arm_global_pd (arch_state s); get_pd_entry (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); x \ kernel_mappings \ - \ (ptrFromPAddr word1, auth, ptrFromPAddr (a + (x && mask aa))) \ state_objs_to_policy s" + \ (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \ state_objs_to_policy s" apply (simp add: state_objs_to_policy_def) apply (rule sbta_vref) apply (clarsimp simp: state_vrefs_def split: option.splits) @@ -176,10 +176,10 @@ lemma get_page_info_state_objs_to_policy: apply (clarsimp simp: typ_at_eq_kheap_obj) apply (clarsimp simp: vs_refs_no_global_pts_def) - apply (rule_tac x="(ucast ((x >> 12) && mask 8), ptrFromPAddr a, aa, - vspace_cap_rights_to_auth b)" in bexI) + apply (rule_tac x="(ucast ((x >> 12) && mask 8), ptrFromPAddr base, sz, + vspace_cap_rights_to_auth r)" in bexI) apply clarsimp - apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI) + apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI) apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def) apply (simp add: ptr_offset_in_ptr_range) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 3f825ba0b..e9b639de3 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -1827,12 +1827,12 @@ lemma not_in_global_refs_vs_lookup: small page, since the invariants tell us that the arm_globals_frame is only a small page *) lemma get_page_info_arm_globals_frame: - "\get_page_info (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) p = Some (b, a, r); + "\get_page_info (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) t) p = Some (base, sz, attr, r); get_pd_of_thread (kheap s) (arch_state s) t \ arm_global_pd (arch_state s); valid_arch_state s; valid_arch_objs s; valid_global_pd_mappings s; equal_kernel_mappings s; valid_vs_lookup s; valid_global_objs s; valid_global_refs s; - b = addrFromPPtr (arm_globals_frame (arch_state s))\ \ r = {}" + base = addrFromPPtr (arm_globals_frame (arch_state s))\ \ r = {}" apply(case_tac "p \ kernel_mappings") apply(blast dest: some_get_page_info_kmapsD) apply(clarsimp simp: get_pd_of_thread_def split: option.splits kernel_object.splits cap.splits arch_cap.splits if_splits) @@ -1898,36 +1898,37 @@ lemma ptrFromPAddr_add_helper: done lemma get_page_info_is_arm_globals_frame: - notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff - Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex + notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff + Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex shows - "\x \ range_of_arm_globals_frame sa; invs sa; - get_page_info (\obj. get_arch_obj (kheap sa obj)) - (get_pd_of_thread (kheap sa) (arch_state sa) t) xa = - Some (a, aa, b); - a + (xa && mask aa) = addrFromPPtr x; - get_pd_of_thread (kheap sa) (arch_state sa) t \ arm_global_pd (arch_state sa); - xa \ kernel_mappings\ \ - ptrFromPAddr a = (arm_globals_frame (arch_state sa))" + "\x \ range_of_arm_globals_frame s; invs s; + get_page_info (\obj. get_arch_obj (kheap s obj)) + (get_pd_of_thread (kheap s) (arch_state s) t) x' = + Some (base, psz, attr, r); + base + (x' && mask psz) = addrFromPPtr x; + get_pd_of_thread (kheap s) (arch_state s) t \ arm_global_pd (arch_state s); + x' \ kernel_mappings\ \ + ptrFromPAddr base = (arm_globals_frame (arch_state s))" apply(frule some_get_page_info_umapsD) (* following two lines clagged from ADT_AC.ptr_offset_in_ptr_range *) apply (clarsimp simp: get_pd_of_thread_reachable invs_arch_objs invs_psp_aligned invs_valid_asid_table invs_valid_objs)+ - apply(subgoal_tac "typ_at (AArch (AIntData ARMSmallPage)) (arm_globals_frame (arch_state sa)) sa") + apply(rename_tac sz) + apply(subgoal_tac "typ_at (AArch (AIntData ARMSmallPage)) (arm_globals_frame (arch_state s)) s") apply(clarsimp simp: obj_at_def) prefer 2 apply(fastforce dest: invs_arch_state simp: valid_arch_state_def) apply(frule invs_distinct) apply(clarsimp simp: pspace_distinct_def) - apply(drule_tac x="ptrFromPAddr a" in spec, drule_tac x="arm_globals_frame (arch_state sa)" in spec) + apply(drule_tac x="ptrFromPAddr base" in spec, drule_tac x="arm_globals_frame (arch_state s)" in spec) apply simp - apply(case_tac "ptrFromPAddr a = arm_globals_frame (arch_state sa)") + apply(case_tac "ptrFromPAddr base = arm_globals_frame (arch_state s)") apply assumption apply(frule ptr_offset_in_ptr_range) apply (simp+) apply(simp add: ptr_range_def) - apply(subgoal_tac "ptrFromPAddr a + (xa && mask (pageBitsForSize sz)) \ {arm_globals_frame - (arch_state sa)..arm_globals_frame (arch_state sa) + 0xFFF}") + apply(subgoal_tac "ptrFromPAddr base + (x' && mask (pageBitsForSize sz)) \ {arm_globals_frame + (arch_state s)..arm_globals_frame (arch_state s) + 0xFFF}") apply(simp only: p_assoc_help) apply blast apply(drule_tac y="addrFromPPtr x" and f=ptrFromPAddr in arg_cong) @@ -1957,8 +1958,10 @@ lemma empty_rights_in_arm_globals_frame: apply(erule invs_equal_kernel_mappings) apply blast apply(rule get_page_info_arm_globals_frame) - apply (simp add: invs_arch_state invs_arch_objs invs_valid_global_pd_mappings invs_equal_kernel_mappings invs_valid_vs_lookup invs_valid_global_objs invs_valid_global_refs)+ - apply(drule get_page_info_is_arm_globals_frame, simp+) + apply (simp add: invs_arch_state invs_arch_objs invs_valid_global_pd_mappings + invs_equal_kernel_mappings invs_valid_vs_lookup invs_valid_global_objs + invs_valid_global_refs)+ + apply(drule get_page_info_is_arm_globals_frame, simp+)[1] apply(fastforce dest: arg_cong[where f=addrFromPPtr]) done @@ -3755,4 +3758,4 @@ where "uop_sane f \ \t pl pr pxn tcu. (f t pl pr pxn tcu) \ {} \ (\tc um es. (Some Interrupt, tc, um, es) \ (f t pl pr pxn tcu))" -end (* a comment *) +end diff --git a/proof/infoflow/ADT_IF_Refine.thy b/proof/infoflow/ADT_IF_Refine.thy index 6be02117c..b0f0c8bf4 100644 --- a/proof/infoflow/ADT_IF_Refine.thy +++ b/proof/infoflow/ADT_IF_Refine.thy @@ -116,12 +116,15 @@ definition "ptable_lift_s' s \ ptable_lift (ksCurThread s) (absKState s)" definition - "ptable_xn_s' s \ ptable_xn (ksCurThread s) (absKState s)" + "ptable_attrs_s' s \ ptable_attrs (ksCurThread s) (absKState s)" + +definition + "ptable_xn_s' s \ \addr. XNever \ ptable_attrs_s' s addr" definition doUserOp_if :: "user_transition_if \ user_context \ (kernel_state, (event option \ user_context)) nondet_monad" where "doUserOp_if uop tc \ do pr \ gets ptable_rights_s'; - pxn \ gets ptable_xn_s'; + pxn \ gets (\s x. pr x \ {} \ ptable_xn_s' s x); pl \ gets (\s. ptable_lift_s' s |` {x. pr x \ {}}); t \ getCurThread; um \ @@ -199,7 +202,7 @@ lemma do_user_op_if_corres: apply (clarsimp elim!: state_relationE) apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split) prefer 2 - apply (clarsimp simp: ptable_xn_s_def ptable_xn_s'_def) + apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def) apply (subst absKState_correct, fastforce, assumption+) apply (clarsimp elim!: state_relationE) apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split) @@ -374,7 +377,7 @@ lemma do_user_op_if_corres': apply (rule_tac r'="op=" and P=einvs and P'=invs' in corres_split) prefer 2 apply (clarsimp simp: absArchState_correct curthread_relation ptable_xn_s'_def - ptable_xn_s_def) + ptable_xn_s_def ptable_attrs_s_def ptable_attrs_s'_def) apply (subst absKState_correct, fastforce, assumption+) apply simp apply (clarsimp elim!: state_relationE) diff --git a/proof/infoflow/ADT_IF_Refine_C.thy b/proof/infoflow/ADT_IF_Refine_C.thy index d566ebad4..988c86c74 100644 --- a/proof/infoflow/ADT_IF_Refine_C.thy +++ b/proof/infoflow/ADT_IF_Refine_C.thy @@ -314,17 +314,22 @@ lemma kernelEntry_corres_C: end +context state_rel +begin -definition (in state_rel) +definition "ptable_rights_s'' s \ ptable_rights (cur_thread (cstate_to_A s)) (cstate_to_A s)" -definition (in state_rel) +definition "ptable_lift_s'' s \ ptable_lift (cur_thread (cstate_to_A s)) (cstate_to_A s)" -definition (in state_rel) - "ptable_xn_s'' s \ ptable_xn (cur_thread (cstate_to_A s)) (cstate_to_A s)" +definition + "ptable_attrs_s'' s \ ptable_attrs (cur_thread (cstate_to_A s)) (cstate_to_A s)" -definition (in state_rel) +definition + "ptable_xn_s'' s \ \addr. XNever \ ptable_attrs_s'' s addr" + +definition doMachineOp_C :: "(machine_state, 'a) nondet_monad \ (cstate, 'a) nondet_monad" where "doMachineOp_C mop \ @@ -335,13 +340,13 @@ where return r od" -definition (in state_rel) doUserOp_C_if +definition doUserOp_C_if :: "user_transition_if \ user_context \ (cstate, (event option \ user_context)) nondet_monad" where "doUserOp_C_if uop tc \ do pr \ gets ptable_rights_s''; - pxn \ gets ptable_xn_s''; + pxn \ gets (\s x. pr x \ {} \ ptable_xn_s'' s x); pl \ gets (\s. restrict_map (ptable_lift_s'' s) {x. pr x \ {}}); t \ gets (\s. cur_thread (cstate_to_A s)); um \ gets (\s. restrict_map (user_mem_C (globals s) \ ptrFromPAddr) @@ -358,11 +363,12 @@ definition (in state_rel) doUserOp_C_if od" -definition (in state_rel) +definition do_user_op_C_if where "do_user_op_C_if uop \ {(s,e,(tc,s'))| s e tc s'. ((e,tc),s') \ fst (split (doUserOp_C_if uop) s)}" +end context kernel_m begin @@ -451,7 +457,8 @@ lemma do_user_op_if_C_corres: invs_def valid_state_def valid_pspace_def state_relation_def) apply (rule_tac r'="op=" and P'=\ and P="invs' and ex_abs (einvs)" in corres_split) prefer 2 - apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def cstate_to_A_def rf_sr_def) + apply (clarsimp simp: ptable_xn_s'_def ptable_xn_s''_def ptable_attrs_s_def + ptable_attrs_s'_def ptable_attrs_s''_def cstate_to_A_def rf_sr_def) apply (subst cstate_to_H_correct, simp add: invs'_def,force+)+ apply (simp only: ex_abs_def) apply (elim exE conjE) diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy index 3754cb87c..aab2ceff4 100644 --- a/proof/infoflow/Example_Valid_State.thy +++ b/proof/infoflow/Example_Valid_State.thy @@ -1721,14 +1721,6 @@ lemma valid_sched_s0[simp]: apply (clarsimp simp: valid_idle_etcb_def etcb_at'_def ekh0_obj_def s0_ptr_defs idle_thread_ptr_def) done -lemma executable_arch_objs_s0[simp]: - "executable_arch_objs s0_internal" - by (clarsimp simp: executable_arch_objs_def executable_arch_obj_def - executable_pte_def executable_pde_def s0_internal_def - obj_at_def kh0_def kh0_obj_def s0_ptr_defs High_pt'_def Low_pt'_def - High_pd'_def Low_pd'_def - split: arch_kernel_obj.splits pte.splits pde.splits split_if_asm) - lemma einvs_s0: "einvs s0_internal" apply (simp add: valid_state_def invs_def) diff --git a/proof/infoflow/Example_Valid_StateH.thy b/proof/infoflow/Example_Valid_StateH.thy index bc41e788d..c12a7b9a4 100644 --- a/proof/infoflow/Example_Valid_StateH.thy +++ b/proof/infoflow/Example_Valid_StateH.thy @@ -129,7 +129,7 @@ definition Low_pt'H :: "word8 \ Hardware_H.pte " where "Low_pt'H \ (\_. Hardware_H.InvalidPTE) - (0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \ {}) (Global \ {}) (vmrights_map vm_read_write))" + (0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \ {}) (Global \ {}) (XNever \ {}) (vmrights_map vm_read_write))" definition Low_ptH :: "word32 \ word32 \ Structures_H.kernel_object option" @@ -141,7 +141,9 @@ where definition [simp]: - "global_pdH \ (\_. Hardware_H.InvalidPDE)( ucast (kernel_base >> 20) := Hardware_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \ {}) 0 (PageCacheable \ {}) (Global \ {}) (vmrights_map {}))" + "global_pdH \ (\_. Hardware_H.InvalidPDE)( ucast (kernel_base >> 20) := + Hardware_H.SectionPDE (addrFromPPtr kernel_base) (ParityEnabled \ {}) 0 + (PageCacheable \ {}) (Global \ {}) (XNever \ {}) (vmrights_map {}))" definition @@ -152,7 +154,7 @@ where (0 := Hardware_H.PageTablePDE (Platform.addrFromPPtr Low_pt_ptr) (ParityEnabled \ {}) - undefined )" + undefined)" (* used addrFromPPtr because proof gives me ptrFromAddr.. TODO: check if it's right *) @@ -174,7 +176,8 @@ definition where "High_pt'H \ (\_. Hardware_H.InvalidPTE) - (0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \ {}) (Global \ {}) (vmrights_map vm_read_only))" + (0 := Hardware_H.SmallPagePTE shared_page_ptr (PageCacheable \ {}) (Global \ {}) (XNever \ {}) + (vmrights_map vm_read_only))" definition diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 2d04bae12..d65845780 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -20,9 +20,6 @@ begin datatype 'a partition = Partition 'a | PSched - - - fun scheduler_modes where "scheduler_modes KernelPreempted = True" | "scheduler_modes (KernelEntry Interrupt) = True" | diff --git a/proof/infoflow/UserOp_IF.thy b/proof/infoflow/UserOp_IF.thy index 000409393..9dbf0cc02 100644 --- a/proof/infoflow/UserOp_IF.thy +++ b/proof/infoflow/UserOp_IF.thy @@ -26,31 +26,20 @@ definition ptable_lift_s where definition ptable_rights_s where "ptable_rights_s s \ ptable_rights (cur_thread s) s" -definition get_pt_xn :: "(obj_ref \ arch_kernel_obj) \ obj_ref \ word32 \ bool" where - "get_pt_xn ahp pt_ref vptr \ - case get_pt_entry ahp pt_ref vptr of - Some (ARM_Structs_A.SmallPagePTE base atts _) \ Some (XNever \ atts) - | Some (ARM_Structs_A.LargePagePTE base atts _) \ Some (XNever \ atts) - | _ \ None" - -definition get_page_xn :: "(obj_ref \ arch_kernel_obj) \ obj_ref \ word32 \ bool" where - "get_page_xn ahp pd_ref vptr \ - case get_pd_entry ahp pd_ref vptr of - Some (ARM_Structs_A.PageTablePDE p _ _) \ - get_pt_xn ahp (Platform.ptrFromPAddr p) vptr - | Some (ARM_Structs_A.SectionPDE base atts _ _) \ Some (XNever \ atts) - | Some (ARM_Structs_A.SuperSectionPDE base atts _) \ Some (XNever \ atts) - | _ \ None" - +(* FIXME: move to ADT_AI.thy *) definition - ptable_xn :: "obj_ref \ 'z state \ word32 \ bool" where - "ptable_xn tcb s \ \addr. - case_option False (\x. x) - (get_page_xn (\obj. get_arch_obj (kheap s obj)) + ptable_attrs :: "obj_ref \ 'z state \ word32 \ vm_attributes" where + "ptable_attrs tcb s \ \addr. + case_option {} (fst o snd o snd) + (get_page_info (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) addr)" +definition + ptable_attrs_s :: "'z state \ word32 \ vm_attributes" where + "ptable_attrs_s s \ ptable_attrs (cur_thread s) s" + definition ptable_xn_s where - "ptable_xn_s s \ ptable_xn (cur_thread s) s" + "ptable_xn_s s \ \addr. XNever \ ptable_attrs_s s addr" definition getExMonitor :: "exclusive_monitors machine_monad" where "getExMonitor \ gets exclusive_state" @@ -64,8 +53,8 @@ definition do_user_op_if where (* Get the page rights of each address (ReadOnly, ReadWrite, None, etc). *) pr \ gets ptable_rights_s; - (* Fetch the 'execute never' bits of the current thread's page directory. *) - pxn \ gets ptable_xn_s; + (* Fetch the 'execute never' bits of the current thread's page mappings. *) + pxn \ gets (\s x. pr x \ {} \ ptable_xn_s s x); (* Get the mapping from virtual to physical addresses. *) pl \ gets (\s. restrict_map (ptable_lift_s s) {x. pr x \ {}}); @@ -229,51 +218,98 @@ lemma requiv_ptable_rights_eq: apply (rule ext) apply (case_tac "x \ kernel_mappings") apply (clarsimp simp: ptable_rights_def split: option.splits) - apply (intro conjI) + apply (rule conjI) apply clarsimp apply (frule some_get_page_info_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings - vspace_cap_rights_to_auth_def)+ + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def)+)[4] apply clarsimp apply (frule some_get_page_info_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings - vspace_cap_rights_to_auth_def)+ + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def)+)[4] apply clarsimp apply (frule_tac r=ba in some_get_page_info_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings - vspace_cap_rights_to_auth_def)+ + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def)+)[4] apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)") apply (frule requiv_pd_of_thread_global_pd) - apply fastforce+ + apply (fastforce+)[4] apply (clarsimp simp: ptable_rights_def split: option.splits) - apply (intro conjI) + apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp - apply (intro conjI) + apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')") apply (drule reads_equiv_sym) apply (frule requiv_pd_of_thread_global_pd) - apply (fastforce simp: reads_equiv_def)+ + apply ((fastforce simp: reads_equiv_def)+)[5] apply (simp add: ptable_rights_def) apply (frule requiv_get_pd_of_thread_eq) - apply fastforce+ + apply (fastforce+)[6] apply (frule pd_of_thread_same_agent, simp+) apply (subst requiv_get_page_info_eq, simp+) done + +lemma requiv_ptable_attrs_eq: + "\ reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; + is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \ {} \ + \ ptable_attrs_s s x = ptable_attrs_s s' x" + apply (simp add: ptable_attrs_s_def ptable_rights_s_def) + apply (case_tac "x \ kernel_mappings") + apply (clarsimp simp: ptable_attrs_def split: option.splits) + apply (rule conjI) + apply clarsimp + apply (frule some_get_page_info_kmapsD) + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] + apply clarsimp + apply (frule some_get_page_info_kmapsD) + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] + + apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) + = arm_global_pd (arch_state s)") + apply (frule requiv_pd_of_thread_global_pd) + apply (fastforce+)[4] + apply (clarsimp simp: ptable_attrs_def split: option.splits) + apply (rule conjI) + apply clarsimp + apply (frule get_page_info_gpd_kmaps[rotated, rotated]) + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] + apply clarsimp + apply (rule conjI) + apply (frule get_page_info_gpd_kmaps[rotated, rotated]) + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] + apply clarsimp + apply (frule get_page_info_gpd_kmaps[rotated, rotated]) + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] + + apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') + = arm_global_pd (arch_state s')") + apply (drule reads_equiv_sym) + apply (frule requiv_pd_of_thread_global_pd) + apply ((fastforce simp: reads_equiv_def)+)[5] + + apply (simp add: ptable_attrs_def) + apply (frule requiv_get_pd_of_thread_eq, simp+)[1] + apply (frule pd_of_thread_same_agent, simp+)[1] + apply (subst requiv_get_page_info_eq, simp+)[1] + done + lemma requiv_ptable_lift_eq: "\ reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights_s s x \ {} \ @@ -281,166 +317,50 @@ lemma requiv_ptable_lift_eq: apply (simp add: ptable_lift_s_def ptable_rights_s_def) apply (case_tac "x \ kernel_mappings") apply (clarsimp simp: ptable_lift_def split: option.splits) - apply (intro conjI) + apply (rule conjI) apply clarsimp apply (frule some_get_page_info_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings - vspace_cap_rights_to_auth_def ptable_rights_def)+ + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] apply clarsimp apply (frule some_get_page_info_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings - vspace_cap_rights_to_auth_def ptable_rights_def)+ + apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings + vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)") apply (frule requiv_pd_of_thread_global_pd) - apply fastforce+ + apply (fastforce+)[4] apply (clarsimp simp: ptable_lift_def split: option.splits) - apply (intro conjI) + apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp - apply (intro conjI) + apply (rule conjI) apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ + apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')") apply (drule reads_equiv_sym) apply (frule requiv_pd_of_thread_global_pd) - apply (fastforce simp: reads_equiv_def)+ + apply ((fastforce simp: reads_equiv_def)+)[5] apply (simp add: ptable_lift_def) - apply (frule requiv_get_pd_of_thread_eq, simp+) - apply (frule pd_of_thread_same_agent, simp+) - apply (subst requiv_get_page_info_eq, simp+) - done - -lemma requiv_get_pt_xn_eq: - "\ reads_equiv aag s s'; pas_refined aag s; is_subject aag pt \ - \ get_pt_xn (\obj. get_arch_obj (kheap s obj)) pt x - = get_pt_xn (\obj. get_arch_obj (kheap s' obj)) pt x" - apply (simp add: get_pt_xn_def) - apply (subst requiv_get_pt_entry_eq, simp+) - done - -lemma requiv_get_page_xn_eq: - "\ reads_equiv aag s s'; pas_refined aag s; is_subject aag pd; - x \ kernel_mappings \ - \ get_page_xn (\obj. get_arch_obj (kheap s obj)) pd x - = get_page_xn (\obj. get_arch_obj (kheap s' obj)) pd x" - apply (simp add: get_page_xn_def) - apply (subst requiv_get_pd_entry_eq[symmetric], simp+) - apply (clarsimp split: option.splits pde.splits) - apply (frule pt_in_pd_same_agent, fastforce+) - apply (rule requiv_get_pt_xn_eq, simp+) - done - -lemma some_get_page_xn_kmapsD: - "\get_page_xn (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some xn; - p \ kernel_mappings; valid_global_pd_mappings s; equal_kernel_mappings s\ - \ \ xn" - apply (clarsimp simp: get_page_xn_def get_pd_entry_def get_arch_obj_def - kernel_mappings_slots_eq - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) - apply (erule valid_global_pd_mappingsE) - apply (clarsimp simp: equal_kernel_mappings_def obj_at_def) - apply (drule_tac x=pd_ref in spec, - drule_tac x="arm_global_pd (arch_state s)" in spec, simp) - apply (drule bspec, assumption) - apply (clarsimp simp: valid_pd_kernel_mappings_def pde_mapping_bits_def) - apply (drule_tac x="ucast (p >> 20)" in spec) - apply (clarsimp simp: get_page_xn_def get_pd_entry_def get_arch_obj_def - get_pt_xn_def get_pt_entry_def - kernel_mappings_slots_eq - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits - ARM_Structs_A.pde.splits ARM_Structs_A.pte.splits) - apply (simp add: valid_pde_kernel_mappings_def obj_at_def - valid_pt_kernel_mappings_def) - apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec) - apply (clarsimp simp: valid_pte_kernel_mappings_def) - apply (simp add: valid_pde_kernel_mappings_def obj_at_def - valid_pt_kernel_mappings_def) - apply (drule_tac x="ucast ((p >> 12) && mask 8)" in spec) - apply (clarsimp simp: valid_pte_kernel_mappings_def) - apply (simp add: valid_pde_kernel_mappings_def) - apply (simp add: valid_pde_kernel_mappings_def) - done - -lemma get_pt_xn_some_get_pt_info: - "get_pt_xn ahp pd_ref vptr = Some xn \ - \base sz rights. get_pt_info ahp pd_ref vptr = Some (base, sz, rights)" - by (simp add: get_pt_xn_def get_pt_info_def split: option.splits pte.splits) - -lemma get_page_xn_some_get_page_info: - "get_page_xn ahp pd_ref vptr = Some xn \ - \base sz rights. get_page_info ahp pd_ref vptr = Some (base, sz, rights)" - apply (simp add: get_page_xn_def get_page_info_def split: option.splits pde.splits) - apply (drule get_pt_xn_some_get_pt_info) - apply simp + apply (frule requiv_get_pd_of_thread_eq, simp+)[1] + apply (frule pd_of_thread_same_agent, simp+)[1] + apply (subst requiv_get_page_info_eq, simp+)[1] done lemma requiv_ptable_xn_eq: "\ reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; - is_subject aag (cur_thread s); invs s; invs s' \ - \ ptable_xn_s s = ptable_xn_s s'" - apply (simp add: ptable_xn_s_def) - apply (rule ext) - apply (case_tac "x \ kernel_mappings") - apply (clarsimp simp: ptable_xn_def split: option.splits) - apply (intro conjI) - apply clarsimp - apply (frule some_get_page_xn_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+ - apply clarsimp - apply (frule some_get_page_xn_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+ - apply clarsimp - apply (frule_tac xn=True in some_get_page_xn_kmapsD) - apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings)+ - - apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) - = arm_global_pd (arch_state s)") - apply (frule requiv_pd_of_thread_global_pd) - apply fastforce+ - apply (clarsimp simp: ptable_xn_def split: option.splits) - apply (intro conjI) - apply clarsimp - apply (drule get_page_xn_some_get_page_info) - apply clarsimp - apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ - apply clarsimp - apply (intro conjI) - apply clarsimp - apply (drule get_page_xn_some_get_page_info) - apply clarsimp - apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ - apply clarsimp - apply (drule get_page_xn_some_get_page_info) - apply clarsimp - apply (frule get_page_info_gpd_kmaps[rotated, rotated]) - apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ - - apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') - = arm_global_pd (arch_state s')") - apply (drule reads_equiv_sym) - apply (frule requiv_pd_of_thread_global_pd) - apply (fastforce simp: reads_equiv_def)+ - - apply (simp add: ptable_xn_def) - apply (frule requiv_get_pd_of_thread_eq) - apply fastforce+ - apply (frule pd_of_thread_same_agent, simp+) - apply (subst requiv_get_page_xn_eq, simp+) - done + is_subject aag (cur_thread s); invs s; invs s'; ptable_rights_s s x \ {} \ + \ ptable_xn_s s x = ptable_xn_s s' x" + by (simp add: ptable_xn_s_def requiv_ptable_attrs_eq) lemma requiv_user_mem_eq: "\ reads_equiv aag s s'; globals_equiv s s'; invs s; @@ -502,7 +422,7 @@ definition context_matches_state where "context_matches_state pl pr pxn um es s \ pl = ptable_lift_s s |` {x. pr x \ {}} \ pr = ptable_rights_s s \ - pxn = ptable_xn_s s \ + pxn = (\x. pr x \ {} \ ptable_xn_s s x) \ um = (user_mem s \ ptrFromPAddr) |` {y. \x. pl x = Some y \ AllowRead \ pr x} \ es = exclusive_state (machine_state s)" @@ -569,16 +489,20 @@ lemma do_user_op_reads_respects_g: apply clarsimp apply (wp add: select_wp select_ev dmo_getExMonitor_reads_respects_g del: gets_ev | rule_tac P="pas_refined aag and invs" in gets_ev''' | simp)+ - apply (simp add: reads_equiv_g_def, intro context_conjI allI impI, safe) - apply (simp add: requiv_ptable_rights_eq) + apply (simp add: reads_equiv_g_def) + apply (intro context_conjI allI impI, safe) + apply (clarsimp simp: requiv_ptable_rights_eq) + apply (rule ext) + apply (case_tac "ptable_rights_s s x = {}", simp) apply (simp add: requiv_ptable_xn_eq) apply (subst expand_restrict_map_eq) apply (clarsimp simp: requiv_ptable_lift_eq) - apply (simp add: requiv_cur_thread_eq) + apply (clarsimp simp: requiv_cur_thread_eq) apply (subst expand_restrict_map_eq) apply (clarsimp simp: restrict_map_def requiv_user_mem_eq requiv_user_mem_eq[symmetric, OF reads_equiv_sym globals_equiv_sym]) apply (simp add: context_matches_state_def comp_def) + apply (clarsimp) apply (erule_tac x=st in allE)+ apply (simp add: context_matches_state_def reads_equiv_sym globals_equiv_sym affects_equiv_sym comp_def) apply (simp add: globals_equiv_def) diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index 3317c03f6..b6abd5b1a 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -179,24 +179,6 @@ text {* (e.g. because the VTable entry is not set or a reference has been invalid), the function returns the global kernel mapping. - @{text get_page_info} takes the architecture-specific part of the kernel heap, - a reference to the page directory, and a virtual memory address. - It returns a triple containing - (a) the physical address, where the associated page table starts, - (b) the page table's size in bits, and - (c) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}). - - NOTE: it should not be necessary to use these functions directly. - For the user's convenience, - the functions @{text ptable_lift} and @{text ptable_rights} are - defined below using @{text get_page_info} and @{text get_pd_of_thread}. -*} -consts - get_pd_of_thread :: "kheap \ arch_state \ obj_ref \ obj_ref" - get_page_info :: "(obj_ref \ arch_kernel_obj) \ obj_ref \ - word32 \ (word32 \ nat \ vm_rights)" - -text {* Looking up the page directory for a thread reference involves the following steps: @@ -207,7 +189,9 @@ text {* Note that the mapping data might become stale. Hence, we have to follow the mapping data through the ASID table. *} -defs +definition + get_pd_of_thread :: "kheap \ arch_state \ obj_ref \ obj_ref" +where get_pd_of_thread_def: "get_pd_of_thread khp astate tcb_ref \ case khp tcb_ref of Some (TCB tcb) \ @@ -225,6 +209,7 @@ defs | _ \ arm_global_pd astate) | _ \ arm_global_pd astate" + lemma VSRef_AASIDPool_in_vs_refs: "(VSRef (asid && mask asid_low_bits) (Some AASIDPool), r) \ vs_refs ko = (\apool. ko = ArchObj (arch_kernel_obj.ASIDPool apool) \ @@ -488,17 +473,30 @@ done definition "get_pt_info ahp pt_ref vptr \ case get_pt_entry ahp pt_ref vptr of - Some (ARM_Structs_A.SmallPagePTE base _ rights) \ Some (base, 12, rights) - | Some (ARM_Structs_A.LargePagePTE base _ rights) \ Some (base, 16, rights) + Some (ARM_Structs_A.SmallPagePTE base attrs rights) \ Some (base, 12, attrs, rights) + | Some (ARM_Structs_A.LargePagePTE base attrs rights) \ Some (base, 16, attrs, rights) | _ \ None" -defs + +text {* + @{text get_page_info} takes the architecture-specific part of the kernel heap, + a reference to the page directory, and a virtual memory address. + It returns a tuple containing + (a) the physical address, where the associated page table starts, + (b) the page table's size in bits, and + (c) the page attributes (cachable, XNever, etc) + (d) the access rights (a subset of @{term "{AllowRead, AllowWrite}"}). +*} +definition + get_page_info :: "(obj_ref \ arch_kernel_obj) \ obj_ref \ + word32 \ (word32 \ nat \ vm_attributes \ vm_rights)" +where get_page_info_def: "get_page_info ahp pd_ref vptr \ case get_pd_entry ahp pd_ref vptr of Some (ARM_Structs_A.PageTablePDE p _ _) \ get_pt_info ahp (Platform.ptrFromPAddr p) vptr - | Some (ARM_Structs_A.SectionPDE base _ _ rights) \ Some (base, 20, rights) - | Some (ARM_Structs_A.SuperSectionPDE base _ rights) \ Some (base,24,rights) + | Some (ARM_Structs_A.SectionPDE base attrs _ rights) \ Some (base, 20, attrs, rights) + | Some (ARM_Structs_A.SuperSectionPDE base attrs rights) \ Some (base,24, attrs, rights) | _ \ None" @@ -586,15 +584,15 @@ by (clarsimp simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def split: sum.splits split_if_asm kernel_object.splits arch_kernel_obj.splits ARM_Structs_A.pde.splits) -lemma +lemma get_page_info_pte: "is_aligned pd_ref pd_bits \ lookup_pt_slot pd_ref vptr s = ({(Inr x,s)},False) \ is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits \ get_pte x s = ({(pte,s)},False) \ get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = (case pte of - ARM_Structs_A.SmallPagePTE base _ rights \ Some (base, 12, rights) - | ARM_Structs_A.LargePagePTE base _ rights \ Some (base, 16, rights) + ARM_Structs_A.SmallPagePTE base attrs rights \ Some (base, 12, attrs, rights) + | ARM_Structs_A.LargePagePTE base attrs rights \ Some (base, 16, attrs, rights) | _ \ None)" apply (clarsimp simp add: get_page_info_def get_pd_entry_def split: option.splits) @@ -616,12 +614,12 @@ apply (drule_tac x=x2 in get_pt_entry_Some_eq_get_pte[where s=s and vptr=vptr]) apply (simp add: pt_bits_def pageBits_def mask_def) done -lemma +lemma get_page_info_section: "is_aligned pd_ref pd_bits \ get_pde (lookup_pd_slot pd_ref vptr) s = - ({(ARM_Structs_A.SectionPDE base XX YY rights,s)},False) \ + ({(ARM_Structs_A.SectionPDE base attrs X rights, s)},False) \ get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = - Some (base, 20, rights)" + Some (base, 20, attrs, rights)" apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits) apply (intro conjI impI allI) apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr]) @@ -630,12 +628,12 @@ apply (drule_tac x=x2 in get_pd_entry_Some_eq_get_pde[where s=s and vptr=vptr]) apply clarsimp done -lemma +lemma get_page_info_super_section: "is_aligned pd_ref pd_bits \ get_pde (lookup_pd_slot pd_ref vptr) s = - ({(ARM_Structs_A.SuperSectionPDE base XX rights,s)},False) \ + ({(ARM_Structs_A.SuperSectionPDE base attrs rights,s)},False) \ get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = - Some (base, 24, rights)" + Some (base, 24, attrs, rights)" apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits) apply (intro conjI impI allI) apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr]) @@ -658,7 +656,7 @@ definition definition ptable_rights :: "obj_ref \ 'z state \ word32 \ vm_rights" where "ptable_rights tcb s \ \addr. - case_option {} (snd o snd) + case_option {} (snd o snd o snd) (get_page_info (\obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) addr)" diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 521989a7f..43067c198 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -98,11 +98,8 @@ lemma valid_global_pd_mappingsE: (* NOTE: we could probably add "is_aligned b (pageBitsForSize sz)" if we assumed "valid_global_objs s", additionally. *) -(* NOTE: we might be able to show "p && ~~ mask a = Platform.ptrFromPAddr b" - with the help of valid_pde_kernel_mappings and WordLib.and_not_mask - (though that is not trivial) *) lemma some_get_page_info_kmapsD: - "\get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, r); + "\get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); p \ kernel_mappings; valid_global_pd_mappings s; equal_kernel_mappings s\ \ (\sz. pageBitsForSize sz = a) \ r = {}" apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def @@ -141,7 +138,7 @@ lemma some_get_page_info_kmapsD: lemma get_page_info_gpd_kmaps: "\valid_global_objs s; valid_arch_state s; get_page_info (\obj. get_arch_obj (kheap s obj)) - (arm_global_pd (arch_state s)) p = Some (b, a, r)\ + (arm_global_pd (arch_state s)) p = Some (b, a, attr, r)\ \ p \ kernel_mappings" apply (clarsimp simp: valid_global_objs_def valid_arch_state_def) apply (thin_tac "Ball ?x ?y") @@ -171,7 +168,7 @@ lemma is_aligned_ptrFromPAddrD: done lemma some_get_page_info_umapsD: - "\get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, r); + "\get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); (\\ pd_ref) s; p \ kernel_mappings; valid_arch_objs s; pspace_aligned s; valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\ \ (\sz. pageBitsForSize sz = a \ is_aligned b a \ diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index 7ade16e8a..ce0124113 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -1000,7 +1000,7 @@ lemma valid_list_post: \ valid_list_2 (t'(p := list_insert_after (t' p) src dest)) n" apply (insert valid_list dest neq) apply (simp add: valid_list_2_def t'_def n_def) - apply (fastforce simp: distinct_list_insert_after list_remove_distinct list_remove_removed set_list_insert_after list_remove_removed) + apply (fastforce simp: distinct_list_insert_after list_remove_distinct set_list_insert_after list_remove_removed) done end @@ -1118,7 +1118,7 @@ lemma next_not_child: apply(drule(1) next_not_child_NoneD) apply(rule next_not_child_NoneI) apply(simp add: next_sib' descendants_child no_mloop_descendants desc) - apply(simp add: dest_no_parent descendants_of_def) + apply(simp add: descendants_of_def) apply(simp add: next_sib') apply(simp add: finite_depth_insert_child) apply(simp add: next_slot_def split: split_if_asm) @@ -1134,13 +1134,13 @@ lemma next_not_child: apply(intro allI impI conjI) apply(drule_tac a=src and b=q' and c=src in descendants_trans, simp) apply(simp) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro conjI impI notI allI) apply(simp add: desc) - apply(simp add: dest_no_parent descendants_of_def) + apply(simp add: descendants_of_def) apply(simp) apply(simp add: finite_depth_insert_child) apply(case_tac "next_not_child p t m") @@ -1294,7 +1294,7 @@ lemma next_not_child_no_parent: else next_not_child p t m)" apply(simp) apply(intro conjI impI) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(simp add: no_mloop_def descendants_of_def) apply(subgoal_tac "next_not_child src t m = None") prefer 2 @@ -1312,7 +1312,7 @@ lemma next_not_child_no_parent: apply(simp) apply(drule(1) next_not_child_NoneD, rule next_not_child_NoneI) apply(simp add: descendants next_sib_no_parent) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def ) apply(simp add: next_sib_no_parent) apply(simp add: finite_depth) apply(simp) @@ -1326,7 +1326,7 @@ lemma next_not_child_no_parent: apply(simp) apply(intro allI conjI impI notI) apply(simp add: desc) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(simp add: finite_depth) apply(rule next_not_child_NoneI) apply(intro allI impI) @@ -1360,7 +1360,7 @@ lemma next_not_child: else next_not_child p t m)" apply(simp) apply(intro conjI impI) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(simp add: no_mloop_def descendants_of_def) apply(erule conjE) apply(rule next_not_childI) @@ -1379,7 +1379,7 @@ lemma next_not_child: apply(simp) apply(drule(1) next_not_child_NoneD, rule next_not_child_NoneI) apply(simp add: descendants next_sib) - apply(simp add: descendants_of_def dest_no_parent no_mloop_def) + apply(simp add: descendants_of_def no_mloop_def) apply(simp add: next_sib) apply(simp add: finite_depth) apply(simp) @@ -1388,13 +1388,13 @@ lemma next_not_child: apply(simp add: next_sib descendants) apply(rule disjI2) apply(simp add: next_sib descendants no_mloop_descendants) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(elim exE conjE) apply(rule_tac x=q in exI) apply(simp) apply(intro conjI impI notI) apply(simp add: desc) - apply(simp add: descendants_of_def dest_no_parent) + apply(simp add: descendants_of_def) apply(simp add: finite_depth) apply(rule next_not_childI) apply(rule disjI1) @@ -1442,7 +1442,7 @@ lemma next_slot_no_parent: apply(subgoal_tac "next_not_child dest t m = None") prefer 2 apply((rule next_not_child_NoneI | intro allI impI - | simp add: descendants_of_def dest_no_parent next_sib_def finite_depth dest)+)[1] + | simp add: descendants_of_def next_sib_def finite_depth dest)+)[1] apply(subgoal_tac "next_not_child src t m = None") prefer 2 apply((rule next_not_child_NoneI | intro allI impI | @@ -1632,7 +1632,7 @@ lemma cte_at_next_slot: apply(subgoal_tac "next_not_child_dom (p, cdt_list s, cdt s)") prefer 2 apply(simp add: next_not_child_termination valid_mdb_def valid_list_2_def) - apply(simp add: next_not_child.psimps split: split_if_asm) + apply(simp split: split_if_asm) apply(case_tac "cdt s p") apply(simp) apply(rule descendants_of_cte_at) @@ -2403,7 +2403,7 @@ lemma (in mdb_empty_abs') valid_list_post: apply(rule distinct_list_replace_list) apply(simp)+ apply(rule ccontr) - apply(fastforce dest: int_not_emptyD simp: no_mdb_loop) + apply(fastforce dest: int_not_emptyD) apply(simp) done @@ -2547,7 +2547,7 @@ lemma (in mdb_empty_abs') next_sib: apply(drule after_in_list_in_list) apply(simp add: valid_list_2_def) apply(simp) - apply(intro conjI impI notI, simp add: no_mdb_loop) + apply(intro conjI impI notI, simp) apply(subst list_replace_after_fst_list) apply(frule after_in_list_in_list) apply(simp add: valid_list_2_def)