theory VSpace_R

lemma invalidateASID_valid_arch_state [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> invalidateASIDEntry x \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" apply (simp add: invalidateASID_def
                   invalidateASIDEntry_def invalidateHWASIDEntry_def) apply (wp | simp)+ apply (clarsimp simp: valid_arch_state'_def simp del: fun_upd_apply) apply (clarsimp simp: is_inv_None_upd fun_upd_def[symmetric] comp_upd_simp
                        inj_on_fun_upd_elsewhere valid_asid_map'_def) apply (auto elim!: subset_inj_on dest!: ran_del_subset)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> invalidateASIDEntry x \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> do maybeHWASID <- loadHWASID x;
y <- when (\<exists>y. maybeHWASID = Some y) (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(the maybeHWASID := None)) (ksArchState s)\<rparr>)
od);
y <- findPDForASIDAssert x;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(x := None)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_state' s \<Longrightarrow> ((\<exists>y b. armKSASIDMap (ksArchState s) x = Some (y, b)) \<longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_ a. if a = x then None else armKSASIDMap (ksArchState s) a) (armKSHWASIDTable_update (\<lambda>_ a. if a = the (map_option fst (armKSASIDMap (ksArchState s) x)) then None else armKSHWASIDTable (ksArchState s) a) (ksArchState s))\<rparr>)) \<and> (armKSASIDMap (ksArchState s) x = None \<longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. armKSASIDMap (ksArchState s)) (ksArchState s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); valid_asid_map' (armKSASIDMap (ksArchState s)); armKSASIDMap (ksArchState s) x = Some (y, b)\<rbrakk> \<Longrightarrow> is_inv (\<lambda>a. if a = y then None else armKSHWASIDTable (ksArchState s) a) (map_option fst \<circ> (\<lambda>a. if a = x then None else armKSASIDMap (ksArchState s) a)) \<and> valid_asid_map' (\<lambda>a. if a = x then None else armKSASIDMap (ksArchState s) a) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>valid_asid_table' (armKSASIDTable (ksArchState s)) s; page_directory_at' (armKSGlobalPD (ksArchState s)) s; valid_global_pts' (armKSGlobalPTs (ksArchState s)) s; is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)); armKSASIDMap (ksArchState s) x = Some (y, b); inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s))); dom (armKSASIDMap (ksArchState s)) \<subseteq> {0..mask local.asid_bits} - {0}\<rbrakk> \<Longrightarrow> inj_on (map_option snd \<circ> armKSASIDMap (ksArchState s)) (dom (armKSASIDMap (ksArchState s)) - {x}) \<and> dom (armKSASIDMap (ksArchState s)) - {x} \<subseteq> {0..mask local.asid_bits} - {0} proof (prove)
goal:
No subgoals!