arm+arm-hyp: remove duplicated ASpec asid bit definitions

MiscMachine_A already contains asid_high_bits, asid_low_bits and
asid_bits. Other architectures don't duplicate them in Arch_Structs_A,
so ARM and ARM_HYP shouldn't either.

For ARM, this also means fixing up DRefine+DPolicy+CamkesCdlRefine to
refer to the MiscMachine_A definitions when needed (CapDL duplicates
them again in Types_D, but as they don't import machine theories, those
can't be removed).

Signed-off-by: Rafal Kolanski <[email protected]>

camkes/cdl-refine/Eval_CAMKES_CDL.thy

@@ -169,42 +169,43 @@ 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)
    apply clarsimp
   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
 
 

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

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"

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)+

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)

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)

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)

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)

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")

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>
 

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>