From 86f495d4f3a71470b3a912d0e092644324752a46 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Sun, 1 May 2016 10:17:22 +1000 Subject: [PATCH] arch_split: DPolicy checking --- proof/access-control/Dpolicy.thy | 40 ++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 18 deletions(-) diff --git a/proof/access-control/Dpolicy.thy b/proof/access-control/Dpolicy.thy index 438b598f5..59e77a80b 100644 --- a/proof/access-control/Dpolicy.thy +++ b/proof/access-control/Dpolicy.thy @@ -15,6 +15,8 @@ imports "../drefine/Include_D" begin +context begin interpretation Arch . (*FIXME: arch_split*) + definition cdl_cap_auth_conferred :: "cdl_cap \ auth set" where @@ -196,27 +198,27 @@ lemmas cdl_state_objs_to_policy_cases = cdl_state_bits_to_policy.cases[OF cdl_state_objs_to_policy_mem[THEN iffD1]] lemma transform_asid_rev [simp]: - "asid \ 2 ^ Arch_Structs_A.asid_bits - 1 \ transform_asid_rev (transform_asid asid) = asid" + "asid \ 2 ^ ARM_A.asid_bits - 1 \ transform_asid_rev (transform_asid asid) = asid" apply (clarsimp simp:transform_asid_def transform_asid_rev_def - asid_high_bits_of_def Arch_Structs_A.asid_low_bits_def) + asid_high_bits_of_def ARM_A.asid_low_bits_def) apply (clarsimp simp:ucast_nat_def) apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits") - apply (simp add:Arch_Structs_A.asid_high_bits_def Arch_Structs_A.asid_bits_def) + apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def) apply (subst ucast_ucast_len) apply simp apply (subst shiftr_shiftl1) apply simp apply (subst ucast_ucast_mask) apply (simp add:mask_out_sub_mask) - apply (simp add:Arch_Structs_A.asid_high_bits_def) + apply (simp add:ARM_A.asid_high_bits_def) apply (rule shiftr_less_t2n[where m=8, simplified]) - apply (simp add:Arch_Structs_A.asid_bits_def) + apply (simp add:ARM_A.asid_bits_def) done abbreviation "valid_asid_mapping mapping \ (case mapping of None \ True - | Some (asid, ref) \ asid \ 2 ^ Arch_Structs_A.asid_bits - 1)" + | Some (asid, ref) \ asid \ 2 ^ ARM_A.asid_bits - 1)" lemma transform_asid_rev_transform_mapping [simp]: "valid_asid_mapping mapping \ @@ -347,10 +349,10 @@ lemma caps_of_state_transform_opt_cap_rev: split:option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:split_if_asm) apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pte_def - split:Arch_Structs_A.pte.splits) + split:ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:split_if_asm) apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pde_def - split:Arch_Structs_A.pde.splits) + split:ARM_A.pde.splits) done abbreviation @@ -485,9 +487,9 @@ lemma thread_state_cap_transform_tcb: apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def transform_asid_pool_entry_def split:split_if_asm option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def - split:split_if_asm Arch_Structs_A.pte.splits) + split:split_if_asm ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def - split:split_if_asm Arch_Structs_A.pde.splits) + split:split_if_asm ARM_A.pde.splits) done @@ -515,9 +517,9 @@ lemma thread_bound_ntfn_cap_transform_tcb: apply (case_tac arch_obj;clarsimp simp:transform_asid_pool_contents_def unat_map_def split:split_if_asm) apply (clarsimp simp:transform_asid_pool_entry_def is_bound_ntfn_cap_def split:option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def is_bound_ntfn_cap_def - split:split_if_asm Arch_Structs_A.pte.splits) + split:split_if_asm ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def is_bound_ntfn_cap_def - split:split_if_asm Arch_Structs_A.pde.splits) + split:split_if_asm ARM_A.pde.splits) done @@ -849,7 +851,7 @@ lemma state_objs_transform_rev: done lemma state_vrefs_asidpool_control: - "(pdptr, Invariants_AI.VSRef asid (Some Invariants_AI.AASIDPool), auth) \ + "(pdptr, VSRef asid (Some AASIDPool), auth) \ state_vrefs s poolptr \ auth = Control" apply (clarsimp simp:state_vrefs_def ) apply (cases "kheap s poolptr") @@ -860,7 +862,7 @@ lemma state_vrefs_asidpool_control: done lemma idle_thread_no_asid: - "\ invs s; Invariants_AI.caps_of_state s ptr = Some cap; + "\ invs s; caps_of_state s ptr = Some cap; asid \ cap_asid' cap \ \ fst ptr \ idle_thread s" apply (rule notI) apply (drule idle_thread_null_cap, simp+) @@ -961,16 +963,16 @@ lemma opt_cap_Some_asid_real: apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:split_if_asm) apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits) apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:split_if_asm) - apply (clarsimp simp:transform_pte_def split:Arch_Structs_A.pte.splits) + apply (clarsimp simp:transform_pte_def split:ARM_A.pte.splits) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:split_if_asm) - apply (clarsimp simp:transform_pde_def split:Arch_Structs_A.pde.splits) + apply (clarsimp simp:transform_pde_def split:ARM_A.pde.splits) done lemma state_vrefs_asid_pool_transform_rev: "\ einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \ is_null_cap poolcap; \ is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \ \ - (pdptr, VSRef (asid && mask Arch_Structs_A.asid_low_bits) (Some AASIDPool), Control) + (pdptr, VSRef (asid && mask ARM_A.asid_low_bits) (Some AASIDPool), Control) \ state_vrefs s (cap_object poolcap)" apply (subgoal_tac "cap_object poolcap \ idle_thread s") prefer 2 @@ -1036,7 +1038,7 @@ lemma state_asids_transform_rev: done lemma idle_thread_no_irqs: - "\ invs s; Invariants_AI.caps_of_state s ptr = Some cap; + "\ invs s; caps_of_state s ptr = Some cap; irq \ cap_irqs_controlled cap \ \ fst ptr \ idle_thread s" apply (rule notI) apply (drule idle_thread_null_cap, simp+) @@ -1186,3 +1188,5 @@ lemma pas_refined_transform: done end + +end