theory ArchVSpace_AI

lemma svr_invs [wp]:
  "\<lbrace>invs\<rbrace> set_vm_root t' \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: set_vm_root_def) apply (rule hoare_pre) apply (wp whenE_wp find_pd_for_asid_inv hoare_vcg_all_lift | wpc | simp add: split_def)+ apply (rule_tac Q'="\<lambda>_ s. invs s \<and> x2 \<le> mask asid_bits" in hoare_post_imp_R) prefer 2 apply simp apply (rule valid_validE_R) apply (wp find_pd_for_asid_inv | simp add: split_def)+ apply (rule_tac Q="\<lambda>c s. invs s \<and> s \<turnstile> c" in hoare_strengthen_post) apply wp apply (clarsimp simp: valid_cap_def mask_def) apply(simp add: invs_valid_objs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> set_vm_root t' \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do thread_root <- get_cap (t', tcb_cnode_index (Suc 0));
(case thread_root of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od)
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do thread_root <- get_cap (t', tcb_cnode_index (Suc 0));
(case thread_root of ArchObjectCap (PageDirectoryCap pd None) \<Rightarrow> throwError InvalidRoot | ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError InvalidRoot;
liftE $ arm_context_switch pd asid
odE | ArchObjectCap _ \<Rightarrow> throwError InvalidRoot | _ \<Rightarrow> throwError InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (set_current_pd (addrFromKPPtr global_pd))
od)
od \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>x x12 x51 x52 x2. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'251 (ArchObjectCap (PageDirectoryCap x51 (Some x2))) (PageDirectoryCap x51 (Some x2)) x51 (Some x2) x2\<rbrace> find_pd_for_asid x2 \<lbrace>\<lambda>pd' s. (if x51 \<noteq> pd' then \<lambda>s. invs s \<and> True else (\<lambda>_. True)) s \<and> (if x51 \<noteq> pd' then \<lambda>s. True \<and> True else (\<lambda>s. True \<and> (invs and K (x2 \<le> mask local.asid_bits)) s)) s\<rbrace>, -
 2. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> invs s \<and> True) \<and> (x = DomainCap \<longrightarrow> invs s \<and> True) \<and> (x = IRQControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> invs s \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> invs s \<and> True) \<and> (\<forall>xb xc. xa = PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> invs s \<and> True) \<and> (\<forall>xd. xc = Some xd \<longrightarrow> invs s \<and> ?P'251 x xa xb xc xd s)))\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>x x12 x51 x52 x2. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'251 (ArchObjectCap (PageDirectoryCap x51 (Some x2))) (PageDirectoryCap x51 (Some x2)) x51 (Some x2) x2\<rbrace> find_pd_for_asid x2 \<lbrace>\<lambda>_ s. invs s \<and> x2 \<le> mask local.asid_bits\<rbrace>, -
 2. \<And>x x12 x51 x52 x2 rv s. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2; invs s \<and> x2 \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> (if x51 \<noteq> rv then \<lambda>s. invs s \<and> True else (\<lambda>_. True)) s \<and> (if x51 \<noteq> rv then \<lambda>s. True \<and> True else (\<lambda>s. True \<and> (invs and K (x2 \<le> mask local.asid_bits)) s)) s
 3. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> invs s \<and> True) \<and> (x = DomainCap \<longrightarrow> invs s \<and> True) \<and> (x = IRQControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> invs s \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> invs s \<and> True) \<and> (\<forall>xb xc. xa = PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> invs s \<and> True) \<and> (\<forall>xd. xc = Some xd \<longrightarrow> invs s \<and> ?P'251 x xa xb xc xd s)))\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>x x12 x51 x52 x2 rv s. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2; invs s \<and> x2 \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> (if x51 \<noteq> rv then \<lambda>s. invs s \<and> True else (\<lambda>_. True)) s \<and> (if x51 \<noteq> rv then \<lambda>s. True \<and> True else (\<lambda>s. True \<and> (invs and K (x2 \<le> mask local.asid_bits)) s)) s
 2. \<And>x x12 x51 x52 x2. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'251 (ArchObjectCap (PageDirectoryCap x51 (Some x2))) (PageDirectoryCap x51 (Some x2)) x51 (Some x2) x2\<rbrace> find_pd_for_asid x2 \<lbrace>\<lambda>_ s. invs s \<and> x2 \<le> mask local.asid_bits\<rbrace>, -
 3. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> invs s \<and> True) \<and> (x = DomainCap \<longrightarrow> invs s \<and> True) \<and> (x = IRQControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> invs s \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> invs s \<and> True) \<and> (\<forall>xb xc. xa = PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> invs s \<and> True) \<and> (\<forall>xd. xc = Some xd \<longrightarrow> invs s \<and> ?P'251 x xa xb xc xd s)))\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>x x12 x51 x52 x2. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'251 (ArchObjectCap (PageDirectoryCap x51 (Some x2))) (PageDirectoryCap x51 (Some x2)) x51 (Some x2) x2\<rbrace> find_pd_for_asid x2 \<lbrace>\<lambda>_ s. invs s \<and> x2 \<le> mask local.asid_bits\<rbrace>, -
 2. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> invs s \<and> True) \<and> (x = DomainCap \<longrightarrow> invs s \<and> True) \<and> (x = IRQControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> invs s \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> invs s \<and> True) \<and> (\<forall>xb xc. xa = PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> invs s \<and> True) \<and> (\<forall>xd. xc = Some xd \<longrightarrow> invs s \<and> ?P'251 x xa xb xc xd s)))\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>x x12 x51 x52 x2. \<lbrakk>x = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'251 (ArchObjectCap (PageDirectoryCap x51 (Some x2))) (PageDirectoryCap x51 (Some x2)) x51 (Some x2) x2\<rbrace> find_pd_for_asid x2 \<lbrace>\<lambda>_ a. invs a \<and> x2 \<le> mask local.asid_bits\<rbrace>
 2. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc xd. x = UntypedCap xa xb xc xd \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = ReplyCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = CNodeCap xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> invs s \<and> True) \<and> (x = DomainCap \<longrightarrow> invs s \<and> True) \<and> (x = IRQControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> invs s \<and> True) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> invs s \<and> True) \<and> (xa = ASIDControlCap \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> invs s \<and> True) \<and> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> invs s \<and> True) \<and> (\<forall>xb xc. xa = PageDirectoryCap xb xc \<longrightarrow> (xc = None \<longrightarrow> invs s \<and> True) \<and> (\<forall>xd. xc = Some xd \<longrightarrow> invs s \<and> ?P'251 x xa xb xc xd s)))\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc xd. x = UntypedCap xa xb xc xd) \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc. x = EndpointCap xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc. x = NotificationCap xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc. x = ReplyCap xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc. x = CNodeCap xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>xa. x = ThreadCap xa) \<longrightarrow> invs s) \<and> (x = DomainCap \<longrightarrow> invs s) \<and> (x = IRQControlCap \<longrightarrow> invs s) \<and> ((\<exists>xa. x = IRQHandlerCap xa) \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc. x = Zombie xa xb xc) \<longrightarrow> invs s) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> ((\<exists>x xb. xa = ASIDPoolCap x xb) \<longrightarrow> invs s) \<and> (xa = ASIDControlCap \<longrightarrow> invs s) \<and> ((\<exists>x xb xc xd xe. xa = PageCap x xb xc xd xe) \<longrightarrow> invs s) \<and> ((\<exists>x xb. xa = PageTableCap x xb) \<longrightarrow> invs s) \<and> (\<forall>x xb. xa = PageDirectoryCap x xb \<longrightarrow> (xb = None \<longrightarrow> invs s) \<and> (\<forall>x. xb = Some x \<longrightarrow> invs s \<and> x \<le> mask local.asid_bits)))\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> get_cap (t', tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>c s. invs s \<and> s \<turnstile> c\<rbrace>
 2. \<And>rv s. invs s \<and> s \<turnstile> rv \<Longrightarrow> (rv = NullCap \<longrightarrow> invs s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> invs s) \<and> (rv = DomainCap \<longrightarrow> invs s) \<and> (rv = IRQControlCap \<longrightarrow> invs s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> invs s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ((\<exists>xa xb. x = ASIDPoolCap xa xb) \<longrightarrow> invs s) \<and> (x = ASIDControlCap \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc xd xe. x = PageCap xa xb xc xd xe) \<longrightarrow> invs s) \<and> ((\<exists>xa xb. x = PageTableCap xa xb) \<longrightarrow> invs s) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> invs s) \<and> (\<forall>x. xb = Some x \<longrightarrow> invs s \<and> x \<le> mask local.asid_bits)))
 3. \<And>s. invs s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. invs s \<and> s \<turnstile> rv \<Longrightarrow> (rv = NullCap \<longrightarrow> invs s) \<and> ((\<exists>x xa xb xc. rv = UntypedCap x xa xb xc) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = EndpointCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = NotificationCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = ReplyCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = CNodeCap x xa xb) \<longrightarrow> invs s) \<and> ((\<exists>x. rv = ThreadCap x) \<longrightarrow> invs s) \<and> (rv = DomainCap \<longrightarrow> invs s) \<and> (rv = IRQControlCap \<longrightarrow> invs s) \<and> ((\<exists>x. rv = IRQHandlerCap x) \<longrightarrow> invs s) \<and> ((\<exists>x xa xb. rv = Zombie x xa xb) \<longrightarrow> invs s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ((\<exists>xa xb. x = ASIDPoolCap xa xb) \<longrightarrow> invs s) \<and> (x = ASIDControlCap \<longrightarrow> invs s) \<and> ((\<exists>xa xb xc xd xe. x = PageCap xa xb xc xd xe) \<longrightarrow> invs s) \<and> ((\<exists>xa xb. x = PageTableCap xa xb) \<longrightarrow> invs s) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> invs s) \<and> (\<forall>x. xb = Some x \<longrightarrow> invs s \<and> x \<le> mask local.asid_bits)))
 2. \<And>s. invs s \<Longrightarrow> invs s \<and> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> invs s \<and> valid_objs s proof (prove)
goal:
No subgoals!