riscv aspec: abbreviations for asid_table & pt table base + index

(moved from riscv ainvs)

proof/invariant-abstract/RISCV64/ArchAcc_AI.thy

@@ -1412,14 +1412,6 @@ lemma set_pt_invs:
   apply (clarsimp simp: is_pt_cap_def cap_asid_def)
   done *)
 
-(* FIXME RISCV: move to ASpec/ArchVSpaceAcc *)
-locale_abbrev table_base :: "obj_ref \<Rightarrow> obj_ref" where
-  "table_base p \<equiv> p && ~~mask pt_bits"
-
-(* FIXME RISCV: move to ASpec/ArchVSpaceAcc *)
-locale_abbrev table_index :: "obj_ref \<Rightarrow> pt_index" where
-  "table_index p \<equiv> ucast (p && mask pt_bits >> pte_bits)"
-
 lemma store_pte_invs:
   "\<lbrace>invs and (\<lambda>s. (\<forall>level. \<exists>\<rhd>(level, table_base p) s \<longrightarrow> valid_pte level pte s)) and (* potential off-by-one in level *)
     K (wellformed_pte pte) and

proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy

@@ -120,10 +120,6 @@ end_qualify
 
 context Arch begin global_naming RISCV64
 
-(* FIXME RISCV: move to ASpec *)
-locale_abbrev
-  "asid_table \<equiv> \<lambda>s. riscv_asid_table (arch_state s)"
-
 (* compatibility with other architectures, input only *)
 abbreviation
   "vs_lookup s \<equiv> \<lambda>level asid vref. vs_lookup_table level asid vref s"

spec/abstract/RISCV64/ArchVSpaceAcc_A.thy

@@ -37,6 +37,9 @@ definition asid_low_bits_of :: "asid \<Rightarrow> asid_low_index"
 
 lemmas asid_bits_of_defs = asid_high_bits_of_def asid_low_bits_of_def
 
+locale_abbrev
+  "asid_table \<equiv> \<lambda>s. riscv_asid_table (arch_state s)"
+
 section "Kernel Heap Accessors"
 
 text \<open>Manipulate ASID pools, page directories and page tables in the kernel heap.\<close>
@@ -75,17 +78,23 @@ definition set_pt :: "obj_ref \<Rightarrow> (pt_index \<Rightarrow> pte) \<Right
      set_object ptr (ArchObj (PageTable pt))
    od"
 
+(* The base address of the table a page table entry at p is in (assuming alignment) *)
+locale_abbrev table_base :: "obj_ref \<Rightarrow> obj_ref" where
+  "table_base p \<equiv> p && ~~mask pt_bits"
+
+(* The index within the page table that a page table entry at p addresses *)
+locale_abbrev table_index :: "obj_ref \<Rightarrow> pt_index" where
+  "table_index p \<equiv> ucast (p && mask pt_bits >> pte_bits)"
+
 (* p is the address of the pte,
    which consists of base (for the pt) and offset (for the index inside the pt).
-   We avoid addresses between ptes. *)
+   We assert that we avoid addresses between ptes. *)
 definition pte_of :: "obj_ref \<Rightarrow> (obj_ref \<rightharpoonup> pt) \<rightharpoonup> pte"
   where
   "pte_of p \<equiv> do {
      oassert (is_aligned p pte_bits);
-     let base = p && ~~mask pt_bits;
+     pt \<leftarrow> oapply (table_base p);
-     let index = (p && mask pt_bits) >> pte_bits;
+     oreturn $ pt (table_index p)
-     pt \<leftarrow> oapply base;
-     oreturn $ pt (ucast index)
    }"
 
 locale_abbrev ptes_of :: "'z::state_ext state \<Rightarrow> obj_ref \<rightharpoonup> pte"
@@ -101,10 +110,10 @@ definition store_pte :: "obj_ref \<Rightarrow> pte \<Rightarrow> (unit,'z::state
   where
   "store_pte p pte \<equiv> do
      assert (is_aligned p pte_bits);
-     base \<leftarrow> return $ p && ~~mask pt_bits;
+     base \<leftarrow> return $ table_base p;
-     index \<leftarrow> return $ (p && mask pt_bits) >> pte_bits;
+     index \<leftarrow> return $ table_index p;
-     pt \<leftarrow> get_pt base;
+     pt \<leftarrow> get_pt (table_base p);
-     pt' \<leftarrow> return $ pt (ucast index := pte);
+     pt' \<leftarrow> return $ pt (index := pte);
      set_pt base pt'
    od"