theory ArchFinalise_AI

lemma flush_table_empty:
  "\<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
    flush_table ac aa b word
   \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>" apply (clarsimp simp: flush_table_def set_vm_root_def) apply (wp do_machine_op_obj_at arm_context_switch_empty whenE_wp
    | wpc
    | simp
    | wps)+ apply (rename_tac pd x y) apply (rule_tac Q="\<lambda>pd' s.
              (if pd \<noteq> pd'
               then (\<lambda>s. obj_at
                         (empty_table (set (arm_global_pts (arch_state s)))) word
                         s)
               else (\<lambda>_. True))
               s \<and>
              (if pd \<noteq> pd' then \<lambda>s. True
               else (\<lambda>s. obj_at
                         (empty_table (set (arm_global_pts (arch_state s)))) word
                         s))
               s"
    and Q'="\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s"
    in hoare_post_imp_R) prefer 2 apply simp apply (wp find_pd_for_asid_inv mapM_wp
    | simp
    | wpc
    | rule_tac
        Q="\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s"
        in hoare_strengthen_post)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> flush_table ac aa b word \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> do y <- assert (b && mask 20 = 0);
root_switched <- set_vm_root_for_flush ac aa;
maybe_hw_asid <- load_hw_asid aa;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (do tcb <- gets cur_thread;
thread_root <- get_cap (tcb, 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)
od)
od \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>root_switched maybe_hw_asid tcb thread_root x12 x51 x52 x2. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap x51 (Some x2)); x12 = PageDirectoryCap x51 (Some x2); x52 = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'257 () True maybe_hw_asid () tcb (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. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s else (\<lambda>_. True)) s \<and> (if x51 \<noteq> pd' then \<lambda>s. True else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)) s\<rbrace>, -
 2. \<And>y root_switched maybe_hw_asid ya tcb. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B11 y root_switched maybe_hw_asid ya tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>thread_root s. (thread_root = NullCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb xc. thread_root = UntypedCap x xa xb xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = EndpointCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = NotificationCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = ReplyCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = CNodeCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ThreadCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = DomainCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = IRQControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = IRQHandlerCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = Zombie x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (x = ASIDControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> ?P'257 y root_switched maybe_hw_asid ya tcb thread_root x xa xb xc s)))\<rbrace>
 3. \<And>y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B11 y root_switched maybe_hw_asid ya\<rbrace>
 4. \<And>y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q8 y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid)) \<lbrace>\<lambda>ya. if root_switched then ?Q10 y root_switched maybe_hw_asid ya else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 5. \<And>y root_switched. \<lbrace>?B6 y root_switched\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q8 y root_switched maybe_hw_asid else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<And>y. \<lbrace>?B5 y\<rbrace> set_vm_root_for_flush ac aa \<lbrace>?B6 y\<rbrace>
 7. \<lbrace>?Q4\<rbrace> assert (b && mask 20 = 0) \<lbrace>?B5\<rbrace>
 8. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'257 () True maybe_hw_asid () tcb (ArchObjectCap (PageDirectoryCap pd (Some y))) (PageDirectoryCap pd (Some y)) pd (Some y) y\<rbrace> find_pd_for_asid y \<lbrace>\<lambda>pd' s. (if pd \<noteq> pd' then \<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s else (\<lambda>_. True)) s \<and> (if pd \<noteq> pd' then \<lambda>s. True else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)) s\<rbrace>, -
 2. \<And>y root_switched maybe_hw_asid ya tcb. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B11 y root_switched maybe_hw_asid ya tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>thread_root s. (thread_root = NullCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb xc. thread_root = UntypedCap x xa xb xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = EndpointCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = NotificationCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = ReplyCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = CNodeCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ThreadCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = DomainCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = IRQControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = IRQHandlerCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = Zombie x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (x = ASIDControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> ?P'257 y root_switched maybe_hw_asid ya tcb thread_root x xa xb xc s)))\<rbrace>
 3. \<And>y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B11 y root_switched maybe_hw_asid ya\<rbrace>
 4. \<And>y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q8 y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid)) \<lbrace>\<lambda>ya. if root_switched then ?Q10 y root_switched maybe_hw_asid ya else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 5. \<And>y root_switched. \<lbrace>?B6 y root_switched\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q8 y root_switched maybe_hw_asid else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<And>y. \<lbrace>?B5 y\<rbrace> set_vm_root_for_flush ac aa \<lbrace>?B6 y\<rbrace>
 7. \<lbrace>?Q4\<rbrace> assert (b && mask 20 = 0) \<lbrace>?B5\<rbrace>
 8. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'257 () True maybe_hw_asid () tcb (ArchObjectCap (PageDirectoryCap pd (Some y))) (PageDirectoryCap pd (Some y)) pd (Some y) y\<rbrace> find_pd_for_asid y \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>, -
 2. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y rv s. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y; obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrakk> \<Longrightarrow> (if pd \<noteq> rv then \<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s else (\<lambda>_. True)) s \<and> (if pd \<noteq> rv then \<lambda>s. True else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)) s
 3. \<And>y root_switched maybe_hw_asid ya tcb. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B11 y root_switched maybe_hw_asid ya tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>thread_root s. (thread_root = NullCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb xc. thread_root = UntypedCap x xa xb xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = EndpointCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = NotificationCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = ReplyCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = CNodeCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ThreadCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = DomainCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = IRQControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = IRQHandlerCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = Zombie x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (x = ASIDControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> ?P'257 y root_switched maybe_hw_asid ya tcb thread_root x xa xb xc s)))\<rbrace>
 4. \<And>y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B11 y root_switched maybe_hw_asid ya\<rbrace>
 5. \<And>y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q8 y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid)) \<lbrace>\<lambda>ya. if root_switched then ?Q10 y root_switched maybe_hw_asid ya else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<And>y root_switched. \<lbrace>?B6 y root_switched\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q8 y root_switched maybe_hw_asid else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 7. \<And>y. \<lbrace>?B5 y\<rbrace> set_vm_root_for_flush ac aa \<lbrace>?B6 y\<rbrace>
 8. \<lbrace>?Q4\<rbrace> assert (b && mask 20 = 0) \<lbrace>?B5\<rbrace>
 9. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y rv s. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y; obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrakk> \<Longrightarrow> (if pd \<noteq> rv then \<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s else (\<lambda>_. True)) s \<and> (if pd \<noteq> rv then \<lambda>s. True else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)) s
 2. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'257 () True maybe_hw_asid () tcb (ArchObjectCap (PageDirectoryCap pd (Some y))) (PageDirectoryCap pd (Some y)) pd (Some y) y\<rbrace> find_pd_for_asid y \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>, -
 3. \<And>y root_switched maybe_hw_asid ya tcb. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B11 y root_switched maybe_hw_asid ya tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>thread_root s. (thread_root = NullCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb xc. thread_root = UntypedCap x xa xb xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = EndpointCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = NotificationCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = ReplyCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = CNodeCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ThreadCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = DomainCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = IRQControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = IRQHandlerCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = Zombie x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (x = ASIDControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> ?P'257 y root_switched maybe_hw_asid ya tcb thread_root x xa xb xc s)))\<rbrace>
 4. \<And>y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B11 y root_switched maybe_hw_asid ya\<rbrace>
 5. \<And>y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q8 y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid)) \<lbrace>\<lambda>ya. if root_switched then ?Q10 y root_switched maybe_hw_asid ya else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<And>y root_switched. \<lbrace>?B6 y root_switched\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q8 y root_switched maybe_hw_asid else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 7. \<And>y. \<lbrace>?B5 y\<rbrace> set_vm_root_for_flush ac aa \<lbrace>?B6 y\<rbrace>
 8. \<lbrace>?Q4\<rbrace> assert (b && mask 20 = 0) \<lbrace>?B5\<rbrace>
 9. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>root_switched maybe_hw_asid tcb thread_root x12 pd x y. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched; thread_root = ArchObjectCap (PageDirectoryCap pd (Some y)); x12 = PageDirectoryCap pd (Some y); x = Some y\<rbrakk> \<Longrightarrow> \<lbrace>?P'257 () True maybe_hw_asid () tcb (ArchObjectCap (PageDirectoryCap pd (Some y))) (PageDirectoryCap pd (Some y)) pd (Some y) y\<rbrace> find_pd_for_asid y \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>, -
 2. \<And>y root_switched maybe_hw_asid ya tcb. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B11 y root_switched maybe_hw_asid ya tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>thread_root s. (thread_root = NullCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb xc. thread_root = UntypedCap x xa xb xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = EndpointCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = NotificationCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = ReplyCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = CNodeCap x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ThreadCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = DomainCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (thread_root = IRQControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = IRQHandlerCap x \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x xa xb. thread_root = Zombie x xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>x. thread_root = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (x = ASIDControlCap \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageTableCap xa xb \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xa xb. x = PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> True) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> ?P'257 y root_switched maybe_hw_asid ya tcb thread_root x xa xb xc s)))\<rbrace>
 3. \<And>y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B11 y root_switched maybe_hw_asid ya\<rbrace>
 4. \<And>y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q8 y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid)) \<lbrace>\<lambda>ya. if root_switched then ?Q10 y root_switched maybe_hw_asid ya else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 5. \<And>y root_switched. \<lbrace>?B6 y root_switched\<rbrace> load_hw_asid aa \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q8 y root_switched maybe_hw_asid else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<And>y. \<lbrace>?B5 y\<rbrace> set_vm_root_for_flush ac aa \<lbrace>?B6 y\<rbrace>
 7. \<lbrace>?Q4\<rbrace> assert (b && mask 20 = 0) \<lbrace>?B5\<rbrace>
 8. \<And>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!