diff --git a/camkes/cdl-refine/Eval_CAMKES_CDL.thy b/camkes/cdl-refine/Eval_CAMKES_CDL.thy index 1a1347223d..83be8b8482 100644 --- a/camkes/cdl-refine/Eval_CAMKES_CDL.thy +++ b/camkes/cdl-refine/Eval_CAMKES_CDL.thy @@ -169,7 +169,7 @@ lemma Collect_asid_high__eval_helper: apply (subst arg_cong[where f="(<) _"]) prefer 2 apply (rule unat_lt2p) - apply (simp add: asid_high_bits_def) + apply (simp add: MiscMachine_A.asid_high_bits_def) apply (simp add: transform_asid_def asid_high_bits_of_def[abs_def]) apply (rule set_eqI) apply (rule iffI) @@ -177,34 +177,35 @@ lemma Collect_asid_high__eval_helper: apply (clarsimp simp: Collect_conj_eq image_iff) apply (rule_tac x="(of_nat asid_high << asid_low_bits) + 1" in bexI) apply (subst add.commute, subst shiftr_irrelevant) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) - apply (clarsimp simp: is_aligned_shift) - apply (subst shiftl_shiftr_id) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def) + apply (clarsimp simp: is_aligned_shift MiscMachine_A.asid_low_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def) + apply (subst shiftl_shiftr_id, simp) + apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less) apply (subst ucast_of_nat_small) - apply (clarsimp simp: asid_high_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_high_bits_def) apply simp apply clarsimp apply (rule conjI) apply (clarsimp simp: unat_ucast_eq_unat_and_mask) apply (subst add.commute, subst shiftr_irrelevant) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def) apply (clarsimp simp: is_aligned_shift) apply (subst shiftl_shiftr_id) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def + word_of_nat_less) apply (fold asid_high_bits_def) apply (subst less_mask_eq) - apply (clarsimp simp: asid_high_bits_def word_of_nat_less) + apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less) apply (rule unat_of_nat_eq) - apply (clarsimp simp: asid_high_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_high_bits_def) apply (rule less_is_non_zero_p1[where k="2^asid_high_bits << asid_low_bits"]) - apply (simp only: shiftl_t2n) + apply (simp add: shiftl_t2n) apply (subst mult.commute, subst mult.commute, rule word_mult_less_mono1) - apply (clarsimp simp: asid_high_bits_def word_of_nat_less) - apply (clarsimp simp: asid_low_bits_def) - apply (clarsimp simp: asid_low_bits_def asid_high_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def) + apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def) done diff --git a/proof/dpolicy/Dpolicy.thy b/proof/dpolicy/Dpolicy.thy index b00c5679ff..786af5eb04 100644 --- a/proof/dpolicy/Dpolicy.thy +++ b/proof/dpolicy/Dpolicy.thy @@ -217,26 +217,26 @@ 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 \<le> 2 ^ ARM_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid" + "asid \<le> 2 ^ MiscMachine_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid" apply (clarsimp simp:transform_asid_def transform_asid_rev_def - asid_high_bits_of_def ARM_A.asid_low_bits_def) + asid_high_bits_of_def asid_low_bits_def) apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits") - apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def) + apply (simp add: MiscMachine_A.asid_high_bits_def MiscMachine_A.asid_bits_def MiscMachine_A.asid_low_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:ARM_A.asid_high_bits_def) - apply (rule shiftr_less_t2n[where m=7, simplified]) - apply (simp add:ARM_A.asid_bits_def) + apply (simp add: asid_high_bits_def) + apply (rule shiftr_less_t2n[where m=MiscMachine_A.asid_high_bits, simplified]) + apply (simp add: MiscMachine_A.asid_bits_def MiscMachine_A.asid_high_bits_def) done abbreviation "valid_asid_mapping mapping \<equiv> (case mapping of None \<Rightarrow> True - | Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ ARM_A.asid_bits - 1)" + | Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ asid_bits - 1)" lemma transform_asid_rev_transform_mapping [simp]: "valid_asid_mapping mapping \<Longrightarrow> @@ -1073,7 +1073,7 @@ lemma state_vrefs_asid_pool_transform_rev: "\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow> - (pdptr, asid && mask ARM_A.asid_low_bits, AASIDPool, Control) + (pdptr, asid && mask MiscMachine_A.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s (cap_object poolcap)" apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s") prefer 2 diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index 9d9d453a8e..29ae0394f4 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -730,7 +730,7 @@ next apply (thin_tac "free_asid_select v \<notin> dom v") apply clarsimp apply (subgoal_tac "unat ((ucast (free_asid_select v) :: word32) << 10) mod 1024=0") - apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def]) + apply (simp add: asid_high_bits_of_shift[simplified asid_low_bits_def[simplified]]) apply (rule shiftl_mod[where n=10, simplified]) apply (cut_tac x="free_asid_select v" and 'a=32 in ucast_less) apply simp @@ -1638,8 +1638,8 @@ proof - "CSpaceAcc_A.descendants_of cref (cdt s') = {}" "caps_of_state s' cref = Some cap" "cap = cap.UntypedCap False frame pageBits idx" - "is_aligned (base::word32) ARM_A.asid_low_bits" - "base < 2 ^ ARM_A.asid_bits" + "is_aligned (base::word32) asid_low_bits" + "base < 2 ^ asid_bits" assume relation:"arch_invocation_relation (InvokeAsidControl asid_inv) (arch_invocation.InvokeASIDControl (asid_control_invocation.MakePool frame cnode_ref cref base))" assume asid_para: "asid_inv' = asid_control_invocation.MakePool frame cnode_ref cref base" diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index d0d0c18985..2e19318788 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -1159,7 +1159,7 @@ lemma set_asid_pool_empty': done lemma empty_pool: - "(\<lambda>x. if x \<le> 2 ^ ARM_A.asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty" + "(\<lambda>x. if x \<le> 2 ^ asid_low_bits - 1 then None else (ap :: 10 word \<rightharpoonup> word32) x) = Map.empty" apply (rule ext) apply (cut_tac ptr=x and 'a=10 in word_up_bound) apply (simp add:asid_low_bits_def) @@ -1180,8 +1180,8 @@ lemma get_set_asid_pool: lemma set_asid_pool_empty: "set_asid_pool a Map.empty \<equiv> mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None)))) - [0 :: word32 .e. 2 ^ ARM_A.asid_low_bits - 1]" - using set_asid_pool_empty' [of "2 ^ ARM_A.asid_low_bits - 1" a] + [0 :: word32 .e. 2 ^ asid_low_bits - 1]" + using set_asid_pool_empty' [of "2 ^ asid_low_bits - 1" a] apply - apply (rule eq_reflection) apply simp @@ -1243,7 +1243,7 @@ lemma dcorres_set_asid_pool_empty: "dcorres dc \<top> (valid_idle and asid_pool_at a and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) (mapM_x PageTableUnmap_D.empty_slot - (map (Pair a) [0 .e. 2 ^ ARM_A.asid_low_bits - 1])) + (map (Pair a) [0 .e. 2 ^ asid_low_bits - 1])) (set_asid_pool a Map.empty)" apply (unfold set_asid_pool_empty) apply (rule dcorres_list_all2_mapM_[where F="\<lambda>x y. snd x = snd (transform_asid y)"]) @@ -1269,7 +1269,7 @@ lemma dcorres_set_asid_pool_empty: apply (wp | clarsimp)+ apply simp apply (wp get_asid_pool_triv | clarsimp simp:typ_at_eq_kheap_obj obj_at_def swp_def)+ - apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ ARM_A.asid_low_bits])") + apply (subgoal_tac "(aa, snd (transform_asid y)) \<in> set (map (Pair a) [0..<2 ^ asid_low_bits])") apply clarsimp apply (clarsimp simp del:set_map simp: suffix_def) apply (wp | clarsimp simp:swp_def)+ diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy index 0681e51b52..ddf11f8f95 100644 --- a/proof/invariant-abstract/ARM/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -1074,7 +1074,7 @@ lemma find_pd_for_asid_ref_offset_voodoo: in hoare_strengthen_postE_R) apply (simp add: ucast_ucast_mask mask_asid_low_bits_ucast_ucast) - apply (fold asid_low_bits_def) + apply (fold asid_low_bits_def[simplified]) apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref) apply (simp add: ) apply (simp add: pd_shifting) diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index d50975e78c..765c51f107 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -4933,7 +4933,7 @@ lemma perform_asid_pool_invs [wp]: apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast) - apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask + apply (clarsimp simp: asid_low_bits_def[simplified, symmetric] ucast_ucast_mask word_neq_0_conv[symmetric]) apply (erule notE, rule asid_low_high_bits, simp_all)[1] apply (simp add: asid_high_bits_of_def) diff --git a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy index 399350faf0..8729252859 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy @@ -1416,7 +1416,7 @@ lemma find_pd_for_asid_ref_offset_voodoo: in hoare_strengthen_postE_R) apply (simp add: ucast_ucast_mask mask_asid_low_bits_ucast_ucast) - apply (fold asid_low_bits_def) + apply (fold asid_low_bits_def[simplified]) apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref) apply (simp add: vspace_bits_defs) apply (simp add: pd_shifting[simplified vspace_bits_defs, simplified] vspace_bits_defs) diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy index 8355c415c0..18cf5c470a 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy @@ -5998,7 +5998,7 @@ lemma perform_asid_pool_invs [wp]: apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast) - apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask + apply (clarsimp simp: asid_low_bits_def[simplified, symmetric] ucast_ucast_mask word_neq_0_conv[symmetric]) apply (erule notE, rule asid_low_high_bits, simp_all)[1] apply (simp add: asid_high_bits_of_def) diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index 2231ea2cae..3a05e92571 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -888,7 +888,7 @@ shows apply (drule dom_hd_assocsD) apply (simp add: select_ext_fa[simplified free_asid_select_def] free_asid_select_def o_def returnOk_liftE[symmetric] - split del: if_split) + split del: if_split) apply (thin_tac "fst a \<notin> b \<and> P" for a b P) apply (case_tac "isUntypedCap a \<and> capBlockSize a = objBits (makeObject::asidpool) \<and> \<not> capIsDevice a") diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index 95df6a4bc0..5c2a766816 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/spec/abstract/ARM/Arch_Structs_A.thy @@ -56,15 +56,6 @@ definition is_page_cap :: "arch_cap \<Rightarrow> bool" where "is_page_cap c \<equiv> \<exists>x0 x1 x2 x3 x4. c = PageCap x0 x1 x2 x3 x4" -definition - asid_high_bits :: nat where - "asid_high_bits \<equiv> 7" -definition - asid_low_bits :: nat where - "asid_low_bits \<equiv> 10 :: nat" -definition - asid_bits :: nat where - "asid_bits \<equiv> 17 :: nat" section \<open>Architecture-specific objects\<close> diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy index 2a1d925e31..ba98106cc1 100644 --- a/spec/abstract/ARM_HYP/Arch_Structs_A.thy +++ b/spec/abstract/ARM_HYP/Arch_Structs_A.thy @@ -57,15 +57,6 @@ definition is_page_cap :: "arch_cap \<Rightarrow> bool" where "is_page_cap c \<equiv> \<exists>x0 x1 x2 x3 x4. c = PageCap x0 x1 x2 x3 x4" -definition - asid_high_bits :: nat where - "asid_high_bits \<equiv> 7" -definition - asid_low_bits :: nat where - "asid_low_bits \<equiv> 10 :: nat" -definition - asid_bits :: nat where - "asid_bits \<equiv> 17 :: nat" section \<open>Architecture-specific objects\<close>