theory VSpace_R

lemma storeHWASID_invs_no_cicd':
  "\<lbrace>invs_no_cicd' and
   (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and>
        armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace>
  storeHWASID asid hw_asid
  \<lbrace>\<lambda>x. invs_no_cicd'\<rbrace>" apply (rule hoare_add_post) apply (rule storeHWASID_valid_arch') apply (fastforce simp: all_invs_but_ct_idle_or_in_cur_domain'_def) apply (simp add: storeHWASID_def) apply (wp findPDForASIDAssert_pd_at_wp) apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_arch_state'_def
             valid_global_refs'_def global_refs'_def valid_machine_state'_def
             ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>x. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace> storeHWASID asid hw_asid \<lbrace>?Q'\<rbrace>
 2. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s \<Longrightarrow> ?P' s
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>rv s. ?Q' rv s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s \<Longrightarrow> (valid_arch_state' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s
 2. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> storeHWASID asid hw_asid \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)\<rbrace> do pd <- findPDForASIDAssert asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(hw_asid \<mapsto> asid)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>rv s. valid_arch_state' s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. armKSASIDMap (ksArchState s) asid = None \<and> armKSHWASIDTable (ksArchState s) hw_asid = None)) s \<Longrightarrow> \<forall>pd. pd_at_asid' pd asid s \<and> pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) \<longrightarrow> valid_arch_state' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s), ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))(hw_asid \<mapsto> asid)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))\<rparr>) \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s), ksArchState := armKSHWASIDTable_update (\<lambda>_. ((armKSHWASIDTable \<circ> ksArchState) (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))(hw_asid \<mapsto> asid)) (ksArchState (s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. ((armKSASIDMap \<circ> ksArchState) s)(asid \<mapsto> (hw_asid, pd))) (ksArchState s)\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!