x64 refine: proof update for ASIDMap removal

proof/refine/X64/ADT_H.thy

@@ -2054,10 +2054,10 @@ where
 
 definition
   "absArchState s' \<equiv>
-   case s' of X64KernelState asid_tbl am gpm gpdpts gpds gpts ccr3 kvspace \<Rightarrow>
+   case s' of X64KernelState asid_tbl gpm gpdpts gpds gpts ccr3 kvspace \<Rightarrow>
      \<lparr>x64_asid_table = asid_tbl \<circ> ucast, x64_global_pml4 = gpm,
       x64_kernel_vspace = kvspace, x64_global_pts = gpts,
-      x64_global_pdpts = gpdpts, x64_global_pds = gpds, x64_asid_map = am,
+      x64_global_pdpts = gpdpts, x64_global_pds = gpds,
       x64_current_cr3 = absCR3 ccr3\<rparr>"
 
 lemma cr3_expand_unexpand[simp]: "cr3 (cr3_base_address a) (cr3_pcid a) = a"

proof/refine/X64/ArchAcc_R.thy

@@ -1799,9 +1799,6 @@ find_consts "64 word \<Rightarrow> 'a state \<Rightarrow> bool" name:asid
 definition
   "vspace_at_asid_ex asid \<equiv> \<lambda>s. \<exists>pm. vspace_at_asid asid pm s"
 
-definition
-  "vspace_at_uniq_ex asid \<equiv> \<lambda>s. \<exists>pm. vspace_at_asid asid pm s \<and> vspace_at_uniq asid pm s"
-
 lemma find_vspace_for_asid_corres:
   assumes "asid' = asid"
   shows "corres (lfr \<oplus> op =)

proof/refine/X64/Detype_R.thy

@@ -108,8 +108,7 @@ defs deletionIsSafe_def:
         \<longrightarrow> 6 \<le> bits)"
 
 defs ksASIDMapSafe_def:
-  "ksASIDMapSafe \<equiv> \<lambda>s. \<forall>asid pm.
-     x64KSASIDMap (ksArchState s) asid = Some (pm) \<longrightarrow> page_map_l4_at' pm s"
+  "ksASIDMapSafe \<equiv> \<lambda>s. True"
 
 defs cNodePartialOverlap_def:
   "cNodePartialOverlap \<equiv> \<lambda>cns inRange. \<exists>p n. cns p = Some n
@@ -571,31 +570,8 @@ qed
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 lemma ksASIDMapSafeI:
-  "\<lbrakk> (s,s') \<in> state_relation; invs s; pspace_aligned' s' \<and> pspace_distinct' s' \<rbrakk>
-  \<Longrightarrow> ksASIDMapSafe s'"
-  apply (clarsimp simp: ksASIDMapSafe_def)
-  apply (subgoal_tac "valid_asid_map s")
-   prefer 2
-   apply fastforce
-  apply (clarsimp simp: valid_asid_map_def graph_of_def)
-  apply (subgoal_tac "x64_asid_map (arch_state s) asid = Some pm")
-   prefer 2
-   apply (clarsimp simp: state_relation_def arch_state_relation_def)
-  apply (erule allE)+
-  apply (erule (1) impE)
-  apply clarsimp
-  apply (drule find_vspace_for_asid_eq_helper)
-     apply fastforce
-    apply assumption
-   apply fastforce
-  apply clarsimp
-  apply (rule pspace_relation_pml4)
-      apply (fastforce simp: state_relation_def)
-     apply fastforce
-    apply assumption
-   apply assumption
-  apply simp
-  done
+  "ksASIDMapSafe s'"
+  by (clarsimp simp: ksASIDMapSafe_def)
 
 (* FIXME: generalizes lemma SubMonadLib.corres_submonad *)
 (* FIXME: generalizes lemma SubMonad_R.corres_machine_op *)
@@ -676,21 +652,7 @@ lemma detype_corres:
           simp_all add: detype_locale'_def
      detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
-  apply (simp add: bind_assoc[symmetric])
-  apply (rule corres_stateAssert_implied2)
-     defer
-     apply (erule ksASIDMapSafeI, assumption, assumption)
-    apply (rule hoare_pre)
-     apply (rule delete_objects_invs)
-    apply fastforce
-   apply (simp add: doMachineOp_def split_def)
-   apply wp
-   apply (clarsimp simp: valid_pspace'_def pspace_distinct'_def
-                         pspace_aligned'_def)
-   apply (rule conjI)
-    subgoal by fastforce
-   apply (clarsimp simp add: pspace_distinct'_def ps_clear_def
-                             dom_if_None Diff_Int_distrib)
+  apply (simp add: bind_assoc[symmetric] ksASIDMapSafe_def)
   apply (simp add: delete_objects_def)
   apply (rule_tac Q="\<lambda>_ s. valid_objs s \<and> valid_list s \<and>
            (\<exists>cref. cte_wp_at (op = (cap.UntypedCap d base magnitude idx)) cref s \<and>

proof/refine/X64/Finalise_R.thy

@@ -2343,17 +2343,6 @@ lemma invs_asid_update_strg':
   apply (auto simp add: ran_def split: if_split_asm)
   done
 
-lemma invalidateASID'_invs' [wp]:
-  "\<lbrace>invs'\<rbrace> invalidateASID' asid \<lbrace>\<lambda>r. invs'\<rbrace>"
-  apply (simp add: invalidateASID'_def bind_assoc)
-  apply (wp  | simp)+
-  apply (auto simp: invs'_def valid_state'_def valid_global_refs'_def valid_arch_state'_def
-                        valid_asid_map'_def valid_machine_state'_def global_refs'_def
-                        ct_idle_or_in_cur_domain'_def fun_upd_def[symmetric] tcb_in_cur_domain'_def
-                        dom_def inj_on_def)
-  done
-
-
 lemma invalidateASIDEntry_invs'[wp]:
   "\<lbrace>invs'\<rbrace> invalidateASIDEntry asid vs \<lbrace>\<lambda>r. invs'\<rbrace>"
   apply (simp add: invalidateASIDEntry_def hwASIDInvalidate_def)
@@ -2369,21 +2358,10 @@ lemma deleteASIDPool_invs[wp]:
               | simp)+
   done
 
-lemma valid_asid_pool'_ASIDMap_inv[simp]:
-  "valid_asid_pool' p s \<Longrightarrow> valid_asid_pool' p (s\<lparr>ksArchState := x64KSASIDMap_update (\<lambda>_ a.
-                   if a = asid then b
-                   else x64KSASIDMap
-  (ksArchState s) a)
-               (ksArchState s)\<rparr>)"
-  by (cases p; simp)
-
 lemma invalidateASIDEntry_valid_ap' [wp]:
   "\<lbrace>valid_asid_pool' p\<rbrace> invalidateASIDEntry asid vs \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace>"
-  apply (simp add: invalidateASIDEntry_def invalidateASID'_def hwASIDInvalidate_def
-                    bind_assoc)
-  apply (wp | simp)+
-  apply (rule_tac Q="\<lambda>rv. valid_asid_pool' p" in hoare_strengthen_post)
-    by (wpsimp)+
+  apply (simp add: invalidateASIDEntry_def)
+  by wp
 
 lemma deleteASID_invs'[wp]:
   "\<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace>"

proof/refine/X64/Invariants_H.thy

@@ -1078,12 +1078,6 @@ definition
 where
   "valid_global_pdpts' pdpts \<equiv> \<lambda>s. \<forall>p \<in> set pdpts. pd_pointer_table_at' p s"
 
-definition
-  valid_asid_map' :: "(asid \<rightharpoonup> machine_word) \<Rightarrow> bool"
-where
- "valid_asid_map' m \<equiv> inj_on m (dom m)
-                          \<and> dom m \<subseteq> ({0 .. mask asid_bits} - {0})"
-
 definition
   valid_arch_state' :: "kernel_state \<Rightarrow> bool"
 where
@@ -1092,8 +1086,7 @@ where
   page_map_l4_at' (x64KSGlobalPML4 (ksArchState s)) s \<and>
   valid_global_pds' (x64KSGlobalPDs (ksArchState s)) s \<and>
   valid_global_pdpts' (x64KSGlobalPDPTs (ksArchState s)) s \<and>
-  valid_global_pts' (x64KSGlobalPTs (ksArchState s)) s \<and>
-  valid_asid_map' (x64KSASIDMap (ksArchState s))"
+  valid_global_pts' (x64KSGlobalPTs (ksArchState s)) s"
 
 definition
   irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool"

proof/refine/X64/PageTableDuplicates.thy

@@ -192,11 +192,6 @@ crunch valid_arch_state'[wp]:
   (wp: crunch_wps  simp: crunch_simps unless_def
     ignore:getObject updateObject setObject)
 
-crunch ko_wp_at'[wp]:
- checkPML4NotInASIDMap "\<lambda>s. ko_wp_at' P p s"
-  (wp: crunch_wps simp: crunch_simps unless_def
-    ignore:getObject updateObject setObject)
-
 declare withoutPreemption_lift [wp del]
 
 crunch valid_cap'[wp]:

proof/refine/X64/StateRelation.thy

@@ -478,7 +478,6 @@ where
        \<and> x64_global_pdpts s = x64KSGlobalPDPTs s'
        \<and> x64_global_pds s = x64KSGlobalPDs s'
        \<and> x64_global_pts s = x64KSGlobalPTs s'
-       \<and> x64_asid_map s = x64KSASIDMap s'
        \<and> cr3_relation (x64_current_cr3 s) (x64KSCurrentCR3 s')
        \<and> x64_kernel_vspace s = x64KSKernelVSpace s'}"