theory VSpace_R

lemma armv_contextSwitch_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" apply (simp add: armv_contextSwitch_def armv_contextSwitch_HWASID_def setCurrentPD_to_abs) apply (wp dmo_invs_no_cicd' no_irq_setHardwareASID no_irq_set_current_pd no_irq) apply (rule hoare_post_imp[rotated], rule getHWASID_invs_no_cicd') apply clarsimp apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (clarsimp simp: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do hwasid <- getHWASID asid;
doMachineOp (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> getHWASID asid \<lbrace>\<lambda>hwasid s. (\<forall>m. \<forall>(r, m')\<in>fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) \<and> all_invs_but_ct_idle_or_in_cur_domain' s\<rbrace>
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> (\<forall>m. \<forall>(r, m')\<in>fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p) \<and> all_invs_but_ct_idle_or_in_cur_domain' s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal (2 subgoals):
 1. \<And>rv s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; ((), b) \<in> fst ((do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od) m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal (4 subgoals):
 1. \<And>rv s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P23 rv s m b p\<rbrace> do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID rv
od \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>rv s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P23 rv s m b p m
 3. \<And>rv s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s
 4. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s proof (prove)
goal:
No subgoals!