aarch64 aspec+ainvs: symbolic vs_index_len

Making vs_index_len a sybmolic value instead of a plain number means we
have to unfold config_ARM_PA_SIZE_BITS_40 less often (instead, we need
to consider both cases, which forces us to stay generic).

This also makes sure the type vs_index_len is always distinct from
pt_index_len (even if the sizes are the same), which was only
guaranteed in one of the two configurations before.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -549,7 +549,9 @@ lemmas valid_asid_table_def = valid_asid_table_2_def
 definition arch_obj_bits_type :: "aa_type \<Rightarrow> nat" where
   "arch_obj_bits_type T \<equiv> case T of
      AASIDPool      \<Rightarrow> arch_kobj_size (ASIDPool undefined)
-   | APageTable vsp \<Rightarrow> arch_kobj_size (PageTable ((if vsp then VSRootPT else NormalPT) undefined))
+   | APageTable vsp \<Rightarrow> arch_kobj_size (PageTable (if vsp
+                                                  then VSRootPT undefined
+                                                  else NormalPT undefined))
    | AUserData sz   \<Rightarrow> arch_kobj_size (DataPage False sz)
    | ADeviceData sz \<Rightarrow> arch_kobj_size (DataPage True sz)
    | AVCPU          \<Rightarrow> arch_kobj_size (VCPU undefined)"
@@ -726,10 +728,12 @@ context
   includes machine_bit_simps
 begin
 
-lemmas simple_bit_simps = table_size word_size_bits_def ptTranslationBits_def pageBits_def vcpuBits_def
-lemmas table_bits_simps = pt_bits_def[simplified] pte_bits_def[unfolded word_size_bits_def]
+lemmas simple_bit_simps =
+  table_size word_size_bits_def ptTranslationBits_def pageBits_def vcpuBits_def
+lemmas table_bits_simps =
+  pt_bits_def[simplified] pte_bits_def[unfolded word_size_bits_def] vs_index_bits_def
 
-named_theorems bit_simps
+named_theorems bit_simps (* FIXME AARCH64: shadows Word_Lib bit_simps *)
 
 lemmas [bit_simps] = table_bits_simps simple_bit_simps ipa_size_def valid_vs_slot_bits_def
 
@@ -1931,18 +1935,14 @@ lemma table_index_plus_ucast_pt[simp]:
 lemma table_index_plus_ucast_vs[simp]:
   "is_aligned pt_ptr (pt_bits True) \<Longrightarrow>
    table_index True (pt_ptr + (ucast (i::vs_index) << pte_bits)) = i"
-  by (rule table_index_plus_ucast;
-      simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
-  (* FIXME AARCH64: occasionally we need the config value to relate the (fixed per config) type to
-                    the (conditional) constant. *)
+  by (rule table_index_plus_ucast; simp add: bit_simps)
 
 lemma table_index_offset_pt_bits_left_vs:
   "\<lbrakk> is_aligned pt_ref (pt_bits True); lvl = max_pt_level \<rbrakk> \<Longrightarrow>
    (table_index True (pt_slot_offset lvl pt_ref vref)::vs_index) =
    ucast (vref >> pt_bits_left lvl)"
-  by (simp add: table_index_plus_ucast pt_slot_offset_def pt_index_def
-                Kernel_Config.config_ARM_PA_SIZE_BITS_40_def
-                ptTranslationBits_def ucast_ucast_mask[where 'a=vs_index_len, simplified, symmetric])
+  by (auto simp: table_index_plus_ucast pt_slot_offset_def pt_index_def vs_index_ptTranslationBits
+                 ucast_ucast_mask[where 'a=vs_index_len, simplified, symmetric])
 
 lemma table_index_offset_pt_bits_left_pt:
   "\<lbrakk> is_aligned pt_ref (pt_bits False); lvl \<noteq> max_pt_level \<rbrakk> \<Longrightarrow>
@@ -2537,7 +2537,7 @@ lemma table_index_pt_slot_offset_vs:
    vsroot_index (pt_slot_offset level p (vref_for_level_idx vref idx level)) = idx"
   for idx :: vs_index
   using table_index_pt_slot_offset[where level=max_pt_level and 'a=vs_index_len]
-  by (simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+  by (simp add: bit_simps)
 
 lemma vs_lookup_vref_for_level_eq1:
   "vref_for_level vref' (bot_level+1) = vref_for_level vref (bot_level+1) \<Longrightarrow>
@@ -2629,12 +2629,11 @@ lemma vs_lookup_table_pt_step:
      apply (subst vs_lookup_vref_for_level_eq1)
       prefer 2
       apply assumption
-     apply (simp add: bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+     apply (simp add: bit_simps)
     apply (fastforce simp: ptes_of_Some_distinct in_omonad is_aligned_pt_slot_offset_pte
                            table_index_pt_slot_offset_vs)
    apply (prop_tac "idx \<notin> invalid_mapping_slots", clarsimp simp: valid_pt_range_def)
-   apply (simp add: user_region_def vref_for_level_idx_canonical_user bit_simps
-                    Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+   apply (simp add: user_region_def vref_for_level_idx_canonical_user bit_simps)
   apply (rename_tac ptn idx)
   apply (rule_tac x="vref_for_level vref (level+1) ||
                      (ucast (idx::pt_index) << pt_bits_left level)" in exI)

spec/abstract/AARCH64/Arch_Structs_A.thy

@@ -76,22 +76,51 @@ datatype pte =
       (pte_base_addr : paddr)
 
 
-(* A dependent-ish type in Isabelle: *)
-value_type vs_index_len = "if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"
-type_synonym vs_index = "vs_index_len word"
+definition vs_index_bits :: nat where
+  "vs_index_bits \<equiv> if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat)"
 
-(* Use vs_index_len instead of vs_index_len_def in generic proofs *)
-lemma vs_index_len:
-  "vs_index_len = (if config_ARM_PA_SIZE_BITS_40 then 10 else (9::nat))"
-  by (simp add: vs_index_len_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+lemma vs_index_bits_ge0[simp, intro!]: "0 < vs_index_bits"
+  by (simp add: vs_index_bits_def)
+
+(* A dependent-ish type in Isabelle. We use typedef here instead of value_type so that we can
+   retain a symbolic value (vs_index_bits) for the size of the type instead of getting a plain
+   number such as 9 or 10. *)
+typedef vs_index_len = "{n :: nat. n < vs_index_bits}" by auto
+
+end
+
+instantiation AARCH64_A.vs_index_len :: len0
+begin
+  interpretation Arch .
+  definition len_of_vs_index_len: "len_of (x::vs_index_len itself) \<equiv> CARD(vs_index_len)"
+  instance ..
+end
+
+instantiation AARCH64_A.vs_index_len :: len
+begin
+  interpretation Arch .
+  instance
+  proof
+   show "0 < LENGTH(vs_index_len)"
+     by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
+  qed
+end
+
+context Arch begin global_naming AARCH64_A
+
+type_synonym vs_index = "vs_index_len word"
 
 type_synonym pt_index_len = 9
 type_synonym pt_index = "pt_index_len word"
 
 text \<open>Sanity check:\<close>
+lemma length_vs_index_len[simp]:
+  "LENGTH(vs_index_len) = vs_index_bits"
+  by (simp add: len_of_vs_index_len type_definition.card[OF type_definition_vs_index_len])
+
 lemma vs_index_ptTranslationBits:
   "ptTranslationBits True = LENGTH(vs_index_len)"
-  by (simp add: ptTranslationBits_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+  by (simp add: ptTranslationBits_def vs_index_bits_def)
 
 lemma pt_index_ptTranslationBits:
   "ptTranslationBits False = LENGTH(pt_index_len)"