theory ArchVSpace_AI

lemma invalidate_asid_entry_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) apply (wp load_hw_asid_wp) apply (clarsimp simp: valid_asid_map_def simp del: fun_upd_apply None_upd_eq) apply (clarsimp simp: vspace_at_asid_def vs_lookup_arch_update) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(the maybe_hw_asid := None)\<rparr>\<rparr>)
od);
asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_asid_map s \<Longrightarrow> (if \<exists>y. map_option fst (arm_asid_map (arch_state s) asid) = Some y then \<lambda>sa. valid_asid_map (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>) else (\<lambda>s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {asid} \<times> UNIV. case x of (asida, hwasid, pd) \<Rightarrow> vspace_at_asid asida pd (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := (arm_hwasid_table (arch_state s))(the (map_option fst (arm_asid_map (arch_state s) asid)) := None), arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> asida \<noteq> 0)) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)) - {asid} \<times> UNIV. case x of (asida, hwasid, pd) \<Rightarrow> vspace_at_asid asida pd (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := (arm_asid_map (arch_state s))(asid := None)\<rparr>\<rparr>) \<and> asida \<noteq> 0)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<exists>y b. arm_asid_map (arch_state s) asid = Some (y, b)) \<longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits}) \<and> (arm_asid_map (arch_state s) asid = None \<longrightarrow> dom (arm_asid_map (arch_state s)) - {asid} \<subseteq> {0..mask local.asid_bits}) proof (prove)
goal:
No subgoals!