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

Signed-off-by: Gerwin Klein <[email protected]>

proof/crefine/AARCH64/CSpace_C.thy

@@ -2533,7 +2533,7 @@ lemma cap_get_capSizeBits_spec:
                         cap_lift_domain_cap cap_get_tag_scast
                         objBits_defs wordRadix_def
                         c_valid_cap_def cl_valid_cap_def pageBits_def asidPoolBits_def
-                        Kernel_Config.config_ARM_PA_SIZE_BITS_40_def (* FIXME AARCH64: #define in C, so no other option for now *)
+                        Kernel_Config.config_ARM_PA_SIZE_BITS_40_def (* #define in C, so no other option for now *)
                  cong: option.case_cong
                  dest!: sym [where t = "ucast (cap_get_tag cap)" for cap])
   apply (clarsimp split: option.splits cap_CL.splits dest!: cap_lift_Some_CapD)

proof/crefine/AARCH64/Finalise_C.thy

@@ -1570,7 +1570,7 @@ next
   have level: "level < maxPTLevel" by simp
   then
   have [simp]: "word_of_nat maxPTLevel - (1 + of_nat level) < maxPT" (is "?i < maxPT")
-    by (cases "config_ARM_PA_SIZE_BITS_40";
+    by (cases config_ARM_PA_SIZE_BITS_40;
         simp add: maxPTLevel_def maxPT_def unat_arith_simps unat_of_nat)
 
   from level

proof/crefine/AARCH64/Invoke_C.thy

@@ -1463,9 +1463,9 @@ lemma getObjectSize_spec:
                          bit_simps objBits_simps' framesize_to_H_def pageBitsForSize_def
                         object_type_to_H_def Kernel_C_defs APIType_capBits_def)
   apply (simp add:nAPIObjects_def)
-  (* FIXME AARCH64 abstraction violation, looks to be not true when config_ARM_PA_SIZE_BITS_40 *)
-  apply (simp add:enum_object_type enum_apiobject_type frameSizeConstants_defs
-                  Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
+  (* True for both cases of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *)
+  apply (simp add: enum_object_type enum_apiobject_type frameSizeConstants_defs
+                   Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
                split: if_split)
   apply unat_arith
   done

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)
@@ -4378,7 +4380,7 @@ lemma getObjectSize_symb:
                         APIType_capBits_def objBits_simps' bit_simps
                    split: if_split)
    apply unat_arith
-  (* FIXME AARCH64 abstraction violation *)
+  (* True in either config with corresponding max vm level change *)
   apply (simp add: Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
   done
 
@@ -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 (solves \<open>simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split\<close>)
      apply (simp add: bit_simps)
     apply (drule_tac p="vs_Ptr regionBase" and
                      d="hrs_htd (t_hrs_' (globals s'))" and
@@ -7162,7 +7164,7 @@ lemma ccorres_typ_region_bytes_dummy:
                    cnodes_retype_have_size_mono[where T=S]
                    tcb_ctes_typ_region_bytes[OF _ _ invs_pspace_aligned']
                    pte_typ_region_bytes o_def)
-  (* FIXME AARCH64 abstraction violation, need to know config_ARM_PA_SIZE_BITS_40 is False *)
+  (* True for either version of config_ARM_PA_SIZE_BITS_40 with corresponding max vm level change *)
   apply (simp add: cmap_array_typ_region_bytes_triv invs_pspace_aligned' bit_simps
                    objBitsT_simps word_bits_def zero_ranges_are_zero_typ_region_bytes
                    Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
@@ -8660,7 +8662,6 @@ shows  "ccorres dc xfdc
        subgoal premises prems using prems
          by (clarsimp simp: objBits_simps' unat_eq_def word_unat.Rep_inverse'
                             word_less_nat_alt)+
-    (* FIXME AARCH64 abstraction violation: for some of these we need to know config_ARM_PA_SIZE_BITS_40_def *)
     by (clarsimp simp: bit_simps pageBitsForSize_def framesize_to_H_def frameSizeConstants_defs
                        Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)+
 

proof/crefine/AARCH64/SR_lemmas_C.thy

@@ -2200,7 +2200,7 @@ lemma vspace_at_rf_sr:
    apply (simp add: align_of_def typ_info_array array_tag_def align_td_array_tag)
    apply clarsimp
    apply (drule aligned_intvl_0, simp)
-   apply (clarsimp simp: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def intvl_self)
+   apply (solves \<open>clarsimp simp: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def intvl_self\<close>)
   apply simp
   done
 

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 (solves \<open>cases config_ARM_PA_SIZE_BITS_40; clarsimp?; word_eqI_solve\<close>)
     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 config_ARM_PA_SIZE_BITS_40_def here, because the level_enum only produces a
+        contradiction in one of the branches when PA_40 is set. *)
+     apply (solves \<open>auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def\<close>)[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 (solves \<open>cases config_ARM_PA_SIZE_BITS_40; clarsimp?; word_eqI_solve\<close>)
     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 config_ARM_PA_SIZE_BITS_40_def here, because the level_enum only produces a
+        contradiction in one of the branches when PA_40 is set. *)
+     apply (solves \<open>auto simp: level_defs Kernel_Config.config_ARM_PA_SIZE_BITS_40_def split: if_split_asm\<close>)[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