aarch64 ainvs+refine+crefine: make proofs generic in PA_SIZE_BITS_40

This needed only very minor tweaks, and interestingly only involved more
unfolding of Kernel_Config.config_ARM_PA_SIZE_BITS_40_def. Most of the
unfoldings involved goals where concrete vmlevel numbers now overflow
earlier (3 = 0 for config_ARM_PA_SIZE_BITS_40, instead of 4 = 0).

proof/crefine/AARCH64/Retype_C.thy

@@ -2142,7 +2142,7 @@ proof (intro impI allI)
     and cover: "range_cover ptr sz (ptBits pt_t) 1"
     and al: "is_aligned ptr (ptBits pt_t)"
     and ptr0: "ptr \<noteq> 0"
-    and sz: "(ptBits pt_t) \<le> sz"
+    and sz: "ptBits pt_t \<le> sz"
     and szb: "sz < word_bits"
     and pal: "pspace_aligned' \<sigma>"
     and pdst: "pspace_distinct' \<sigma>"
@@ -2215,7 +2215,9 @@ proof (intro impI allI)
     using al[simplified bit_simps]
     apply -
     apply (rule is_aligned_c_guard[where n="ptBits pt_t" and m=3])
-    apply (simp_all add:  align_td_array align_of_def bit_simps ptr0 split: if_split)
+    apply (simp_all add:  align_td_array align_of_def bit_simps ptr0 pt_t_def
+                          Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
+                    split: if_splits)
     done
 
   have guard'[unfolded array_len_def]: "\<forall>n < array_len. c_guard (pte_Ptr ptr +\<^sub>p int n)"
@@ -2266,7 +2268,7 @@ proof (intro impI allI)
                           pt_bits_def table_size_def power_add pte_bits_def word_size_bits_def
                           hrs_htd_update ht_rl foldr_upd_app_if [folded data_map_insert_def] rl
                           cvariable_array_ptr_retyps[OF szo]
-                          zero_ranges_ptr_retyps[where p="pt_Ptr ptr", simplified szo])
+                          zero_ranges_ptr_retyps[where p="vs_Ptr ptr", simplified szo])
     apply (subst h_t_valid_ptr_retyps_gen_disjoint, assumption)
      apply (simp add:szo cte_C_size cte_level_bits_def)
      apply (erule disjoint_subset)
@@ -5923,7 +5925,7 @@ subgoal
      apply (rule is_aligned_c_guard[where m=pte_bits], simp, simp)
        apply (simp add: align_of_array)
        apply (simp add: align_of_def bit_simps)
-      apply (simp add: bit_simps split: if_split)
+      apply (simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split)
      apply (simp add: bit_simps)
     apply (drule_tac p="vs_Ptr regionBase" and
                      d="hrs_htd (t_hrs_' (globals s'))" and

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -840,7 +840,7 @@ proof -
   have m1: "(-1::vm_level) = (if config_ARM_PA_SIZE_BITS_40 then 3 else 4)"
     by (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
   show ?thesis unfolding asid_pool_level_def
-   by (simp add: m1)
+    by (simp add: m1 Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
 qed
 
 lemma asid_pool_level_not_0[simp]:
@@ -864,7 +864,8 @@ next
   note maxBound_minus_one_bit[simp del]
   assume "x \<le> max_pt_level"
   thus "x \<noteq> asid_pool_level"
-    unfolding level_defs by (auto simp: maxBound_size_bit split: if_splits)
+    unfolding level_defs
+    by (auto simp: maxBound_size_bit Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_splits)
 qed
 
 lemma asid_pool_level_eq:
@@ -891,7 +892,9 @@ lemma vm_level_less_max_pt_level:
 
 lemma vm_level_less_le_1:
   "\<lbrakk> (level' :: vm_level) < level \<rbrakk> \<Longrightarrow> level' \<le> level' + 1"
-  by (fastforce dest: max_pt_level_enum vm_level_less_max_pt_level split: if_split_asm)
+  by (fastforce dest: max_pt_level_enum vm_level_less_max_pt_level
+                simp: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
+                split: if_split_asm)
 
 lemma asid_pool_level_leq_conv[iff]:
   "(asid_pool_level \<le> level) = (level = asid_pool_level)"
@@ -905,7 +908,7 @@ lemma max_pt_level_not_asid_pool_level[simp]:
   "max_pt_level \<noteq> asid_pool_level"
   "asid_pool_level \<noteq> max_pt_level"
   by (simp add: asid_pool_level_def)
-     (simp add: level_defs)
+     (simp add: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
 
 lemma asid_pool_level_minus:
   "asid_pool_level = -1"

proof/refine/AARCH64/ArchAcc_R.thy

@@ -603,6 +603,8 @@ lemma user_region_or:
   "\<lbrakk> vref \<in> user_region; vref' \<in> user_region \<rbrakk> \<Longrightarrow> vref || vref' \<in> user_region"
   by (simp add: user_region_def canonical_user_def le_mask_high_bits word_size)
 
+lemmas bit_pred = bit0.pred bit1.pred
+
 lemma lookupPTSlotFromLevel_corres:
   "\<lbrakk> level' = size level; pt' = pt; level \<le> max_pt_level \<rbrakk> \<Longrightarrow>
    corres (\<lambda>(level, p) (bits, p'). bits = pt_bits_left level \<and> p' = p)
@@ -619,7 +621,7 @@ next
   from `0 < level`
   obtain nlevel where nlevel: "level = nlevel + 1" by (auto intro: that[of "level-1"])
   with `0 < level`
-  have nlevel1: "nlevel < nlevel + 1" using bit1.pred by fastforce
+  have nlevel1: "nlevel < nlevel + 1" using bit_pred by fastforce
   with nlevel
   have level: "size level = Suc (size nlevel)" by simp
 
@@ -672,7 +674,7 @@ next
      apply (simp add: plus_one_eq_asid_pool vref_for_level_def pt_bits_left_def)
      apply (rule conjI, simp add: max_pt_level_def)
      apply (clarsimp simp: level_defs bit_simps maxPTLevel_def)
-     apply word_eqI_solve
+     apply (cases "config_ARM_PA_SIZE_BITS_40"; clarsimp?; word_eqI_solve)
     apply (clarsimp simp: vref_for_level_def pt_bits_left_def)
     apply (rule conjI; clarsimp)
      apply (subgoal_tac "nlevel = max_pt_level - 1")
@@ -684,11 +686,13 @@ next
     apply (simp add: pt_bits_def)
     apply (prop_tac "level_type (nlevel + 1) = NormalPT_T")
      apply (drule max_pt_level_enum)
-     apply (auto simp: level_defs split: if_split_asm)[1]
+     (* Unfolding here, because the level_enum only produces a contradiction in one of the branches
+        when PA_40 is set. *)
+     apply (auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)[1]
     apply (simp add: bit_simps)
     apply word_eqI
     apply (drule max_pt_level_enum)
-    by (auto split: if_split_asm)
+    by (cases config_ARM_PA_SIZE_BITS_40, auto simp: max_pt_level_def2)
 
   from `0 < level` `level' = size level` `pt' = pt` level `level \<le> max_pt_level` level_m1
   show ?case
@@ -828,7 +832,7 @@ next
      apply (simp add: plus_one_eq_asid_pool vref_for_level_def pt_bits_left_def)
      apply (rule conjI, simp add: max_pt_level_def)
      apply (clarsimp simp: level_defs bit_simps maxPTLevel_def)
-     apply word_eqI_solve
+     apply (cases "config_ARM_PA_SIZE_BITS_40"; clarsimp?; word_eqI_solve)
     apply (clarsimp simp: vref_for_level_def pt_bits_left_def)
     apply (rule conjI; clarsimp)
      apply (subgoal_tac "nlevel = max_pt_level - 1")
@@ -840,11 +844,13 @@ next
     apply (simp add: pt_bits_def)
     apply (prop_tac "level_type (nlevel + 1) = NormalPT_T")
      apply (drule max_pt_level_enum)
-     apply (auto simp: level_defs split: if_split_asm)[1]
+     (* Unfolding here, because the level_enum only produces a contradiction in one of the branches
+        when PA_40 is set. *)
+     apply (auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split_asm)[1]
     apply (simp add: bit_simps)
     apply word_eqI
     apply (drule max_pt_level_enum)
-    by (auto split: if_split_asm)
+    by (cases config_ARM_PA_SIZE_BITS_40, auto simp: max_pt_level_def2)
 
   note vm_level.size_minus_one[simp]
   from minus.prems