aarch64 aspec+ainvs: provide+use symbolic ppn_len definition

We initially wanted to move ucast_ucast_ppn to Kernel_Config_Lemmas.
This doesn't work, because ppn is only defined in Arch_Structs_A, but
it turns out that ppn_len is exactly the term `ipa_size - pageBits`
that the lemma needs, so instead of moving the lemma up, we make its
proof generic by providing the symbolic form of `ppn_len` instead.

This still unfolds Kernel_Config.config_ARM_PA_SIZE_BITS_40, but it
does so only trivially and directly where ppn_len is defined.

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

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -1540,16 +1540,10 @@ lemma neg_mask_user_region:
   apply simp
   done
 
-(* FIXME AARCH64: move to Kernel_Config_Lemmas *)
-(* ptr is expected to be a kernel-virtual pointer/obj_ref *)
-lemma ucast_ucast_ppn:
-  "(ucast (ucast ptr::ppn)::machine_word) = ptr && mask (ipa_size - pageBits)" for ptr::machine_word
-  by (simp add: ucast_ucast_mask bit_simps Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
-
 lemma ptrFromPAddr_addr_from_ppn:
   "\<lbrakk> is_aligned pt_ptr pageBits; pptr_base \<le> pt_ptr; pt_ptr < pptrTop \<rbrakk> \<Longrightarrow>
    ptrFromPAddr (paddr_from_ppn (ppn_from_pptr pt_ptr)) = pt_ptr"
-  apply (simp add: paddr_from_ppn_def ppn_from_pptr_def ucast_ucast_ppn)
+  apply (simp add: paddr_from_ppn_def ppn_from_pptr_def ucast_ucast_ppn ppn_len_def')
   apply (frule is_aligned_addrFromPPtr)
   apply (simp add: nat_minus_add_max aligned_shiftr_mask_shiftl addrFromPPtr_mask_ipa
                    mask_len_id[where 'a=machine_word_len, simplified])

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -2395,6 +2395,10 @@ lemma pt_slot_offset_pt_range:
   for level::vm_level
   by (clarsimp simp: ptes_of_Some)
 
+lemma ucast_ucast_ppn:
+  "ucast (ucast ptr::ppn) = ptr && mask ppn_len" for ptr::obj_ref
+  by (simp add: ucast_ucast_mask ppn_len_def)
+
 lemma pte_base_addr_PageTablePTE[simp]:
   "pte_base_addr (PageTablePTE ppn) = paddr_from_ppn ppn"
   by (simp add: pte_base_addr_def)

spec/abstract/AARCH64/Arch_Structs_A.thy

@@ -88,6 +88,11 @@ text \<open>
 value_type ppn_len = "ipa_size - pageBits"
 type_synonym ppn = "ppn_len word"
 
+text \<open>This lemma encodes @{typ ppn_len} value above as a term, so we can use it generically:\<close>
+lemma ppn_len_def':
+  "ppn_len = ipa_size - pageBits"
+  by (simp add: ppn_len_def pageBits_def ipa_size_def Kernel_Config.config_ARM_PA_SIZE_BITS_40_def)
+
 datatype pte =
     InvalidPTE
   | PagePTE