x64: fix ARM build after merge

proof/invariant-abstract/ARM/ArchIpc_AI.thy

@@ -46,11 +46,11 @@ lemma update_cap_data_closedform:
          simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True
                         is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size
                         cap_ep_badge.simps badge_update_def o_def cap_rights_update_def
-                        simp_thms cap_rights.simps Let_def split_def badge_bits_def
+                        simp_thms cap_rights.simps Let_def split_def
                         the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
                         arch_update_cap_data_def
                   cong: if_cong)
-  apply (auto simp: word_bits_def cnode_padding_bits_def cnode_guard_size_bits_def)
+  apply (auto simp: word_bits_def)
   done
 
 lemma cap_asid_PageCap_None [simp]:

proof/invariant-abstract/Untyped_AI.thy

@@ -3149,11 +3149,11 @@ locale Untyped_AI_nonempty_table =
   assumes nonempty_table_caps_of:
   "\<And>S ko. nonempty_table S ko \<Longrightarrow> caps_of ko = {}"
   assumes init_arch_objects_nonempty_table:
-  "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
+  "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
          \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
     K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
         init_arch_objects tp ptr bits us refs
-   \<lbrace>\<lambda>rv. \<lambda>s :: 'state_ext state. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>"
+   \<lbrace>\<lambda>rv. \<lambda>s :: 'state_ext state. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
 
 crunch valid_global_objs[wp]: create_cap "valid_global_objs"
   (simp: crunch_simps)

spec/abstract/ARM/ArchCSpace_A.thy

@@ -23,11 +23,11 @@ context Arch begin global_naming ARM_A
 
 definition cnode_guard_size_bits :: "nat"
 where
-  "cnode_guard_size_bits \<equiv> 5"
+  cnode_guard_size_bits_def [simp]: "cnode_guard_size_bits \<equiv> 5"
 
 definition cnode_padding_bits :: "nat"
 where
-  "cnode_padding_bits \<equiv> 3"
+  cnode_padding_bits_def [simp]: "cnode_padding_bits \<equiv> 3"
 
 text {* On a user request to modify a cnode capability, extract new guard bits and guard. *}
 definition

spec/abstract/ARM/Arch_Structs_A.thy

@@ -264,8 +264,9 @@ where
 text {* For implementation reasons the badge word has differing amounts of bits *}
 definition
   badge_bits :: nat where
-  "badge_bits \<equiv> 28"
+  badge_bits_def [simp]: "badge_bits \<equiv> 28"
 end
+
 section "Arch-specific tcb"