theory Finalise_DR

lemma dcorres_flush_page:
  "dcorres dc \<top> \<top>  (return x) (flush_page aa a b word)" supply if_cong[cong] apply (rule corres_dummy_return_r) apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]]) apply wp apply (simp add:flush_page_def) apply wp apply (rule dcorres_to_wp[OF dcorres_set_vm_root]) apply wp apply clarsimp apply (wp do_machine_op_wp, clarsimp) apply (wp) apply (simp add:load_hw_asid_def) apply wp apply (clarsimp simp:set_vm_root_for_flush_def) apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+ apply (wpc) apply wp+ apply (rule hoare_conjI,rule hoare_drop_imp) apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+ apply (wpc|wp)+ apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (flush_page aa a b word) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (flush_page aa a b word) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (flush_page aa a b word >>= return) proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> flush_page aa a b word \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_page aa a b word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_page aa a b word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do y <- assert (word && mask pageBits = 0);
root_switched <- set_vm_root_for_flush a b;
maybe_hw_asid <- load_hw_asid b;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>cs y root_switched maybe_hw_asid ya x. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?B18 cs y root_switched maybe_hw_asid ya x\<rbrace> set_vm_root x \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. \<And>cs y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 cs y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>?B18 cs y root_switched maybe_hw_asid ya\<rbrace>
 3. \<And>cs y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q15 cs y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid))) \<lbrace>\<lambda>ya. if root_switched then ?Q17 cs y root_switched maybe_hw_asid ya else (\<lambda>s. transform s = cs)\<rbrace>
 4. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q15 cs y root_switched maybe_hw_asid else (\<lambda>s. transform s = cs)\<rbrace>
 5. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 6. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 7. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (6 subgoals):
 1. \<And>cs y root_switched maybe_hw_asid ya. \<lbrakk>\<exists>y. maybe_hw_asid = Some y; root_switched\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 cs y root_switched maybe_hw_asid ya\<rbrace> gets cur_thread \<lbrace>\<lambda>x s. True \<and> transform s = cs\<rbrace>
 2. \<And>cs y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q15 cs y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid))) \<lbrace>\<lambda>ya. if root_switched then ?Q17 cs y root_switched maybe_hw_asid ya else (\<lambda>s. transform s = cs)\<rbrace>
 3. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q15 cs y root_switched maybe_hw_asid else (\<lambda>s. transform s = cs)\<rbrace>
 4. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 5. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 6. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (5 subgoals):
 1. \<And>cs y root_switched maybe_hw_asid. \<exists>y. maybe_hw_asid = Some y \<Longrightarrow> \<lbrace>?Q15 cs y root_switched maybe_hw_asid\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid))) \<lbrace>\<lambda>ya. if root_switched then \<lambda>s. True \<and> transform s = cs else (\<lambda>s. transform s = cs)\<rbrace>
 2. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q15 cs y root_switched maybe_hw_asid else (\<lambda>s. transform s = cs)\<rbrace>
 3. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 4. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 5. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (5 subgoals):
 1. \<And>cs root_switched y. \<lbrace>?Q15 cs () root_switched (Some y)\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) y)) \<lbrace>\<lambda>ya s. transform s = cs\<rbrace>
 2. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then ?Q15 cs y root_switched maybe_hw_asid else (\<lambda>s. transform s = cs)\<rbrace>
 3. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 4. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 5. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (5 subgoals):
 1. \<And>y m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_VAASID (word || UCAST(8 \<rightarrow> 32) y) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then \<lambda>x5. transform x5 = cs else (\<lambda>s. transform s = cs)\<rbrace>
 3. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 4. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 5. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (4 subgoals):
 1. \<And>cs y root_switched. \<lbrace>?B13 cs y root_switched\<rbrace> load_hw_asid b \<lbrace>\<lambda>maybe_hw_asid. if \<exists>y. maybe_hw_asid = Some y then \<lambda>x5. transform x5 = cs else (\<lambda>s. transform s = cs)\<rbrace>
 2. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 3. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 4. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (4 subgoals):
 1. \<And>cs root_switched. \<lbrace>?B13 cs () root_switched\<rbrace> do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map b))
od \<lbrace>\<lambda>maybe_hw_asid x5. transform x5 = cs\<rbrace>
 2. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>?B13 cs y\<rbrace>
 3. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 4. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (3 subgoals):
 1. \<And>cs y. \<lbrace>?B12 cs y\<rbrace> set_vm_root_for_flush a b \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 2. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 3. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (3 subgoals):
 1. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> do tcb <- gets cur_thread;
thread_root <- CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> a) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do y <- arm_context_switch a b;
return True
od else return False
od \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 2. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 3. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (8 subgoals):
 1. \<And>cs tcb x xa xb. xa \<Longrightarrow> \<lbrace>?B73 cs tcb x True xb\<rbrace> case xb of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid b new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid \<lbrace>\<lambda>xb ps. transform ps = cs\<rbrace>
 2. \<And>cs tcb x xa. xa \<Longrightarrow> \<lbrace>?Q52 cs tcb x (ds_id True)\<rbrace> load_hw_asid b \<lbrace>?B73 cs tcb x xa\<rbrace>
 3. \<And>cs tcb x xa. \<not> xa \<Longrightarrow> \<lbrace>?R52 cs tcb x xa\<rbrace> return False \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 4. \<And>cs tcb x. \<lbrace>?B50 cs tcb x\<rbrace> case x of ArchObjectCap b \<Rightarrow> case b of arch_cap.PageDirectoryCap cur_pd b \<Rightarrow> case b of None \<Rightarrow> return True | Some x \<Rightarrow> return (cur_pd \<noteq> a) | _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>xa s. (xa \<longrightarrow> ?Q52 cs tcb x xa s) \<and> (\<not> xa \<longrightarrow> ?R52 cs tcb x xa s)\<rbrace>
 5. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B50 cs tcb\<rbrace>
 6. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 7. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 8. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (9 subgoals):
 1. \<And>cs tcb x xa xb. \<lbrakk>xa; xb = None\<rbrakk> \<Longrightarrow> \<lbrace>?R88 cs tcb x True xb\<rbrace> do new_hw_asid <- find_free_hw_asid;
store_hw_asid b new_hw_asid;
return new_hw_asid
od \<lbrace>\<lambda>xb ps. transform ps = cs\<rbrace>
 2. \<And>cs tcb x xa xb x2. \<lbrakk>xa; xb = Some x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. ?R87 cs tcb x True xb a x2\<rbrace> return x2 \<lbrace>\<lambda>xb ps. transform ps = cs\<rbrace>
 3. \<And>cs tcb x xa. xa \<Longrightarrow> \<lbrace>?Q52 cs tcb x (ds_id True)\<rbrace> load_hw_asid b \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R88 cs tcb x xa a b) \<and> (\<forall>xb. a = Some xb \<longrightarrow> ?R87 cs tcb x xa a b xb)\<rbrace>
 4. \<And>cs tcb x xa. \<not> xa \<Longrightarrow> \<lbrace>?R52 cs tcb x xa\<rbrace> return False \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 5. \<And>cs tcb x. \<lbrace>?B50 cs tcb x\<rbrace> case x of ArchObjectCap b \<Rightarrow> case b of arch_cap.PageDirectoryCap cur_pd b \<Rightarrow> case b of None \<Rightarrow> return True | Some x \<Rightarrow> return (cur_pd \<noteq> a) | _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>xa s. (xa \<longrightarrow> ?Q52 cs tcb x xa s) \<and> (\<not> xa \<longrightarrow> ?R52 cs tcb x xa s)\<rbrace>
 6. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B50 cs tcb\<rbrace>
 7. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 8. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 9. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (7 subgoals):
 1. \<And>cs tcb x xa. xa \<Longrightarrow> \<lbrace>?Q52 cs tcb x (ds_id True)\<rbrace> load_hw_asid b \<lbrace>\<lambda>a b. (a = None \<longrightarrow> transform b = cs) \<and> (\<forall>x. a = Some x \<longrightarrow> transform b = cs)\<rbrace>
 2. \<And>cs tcb x xa. \<not> xa \<Longrightarrow> \<lbrace>?R52 cs tcb x xa\<rbrace> return False \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 3. \<And>cs tcb x. \<lbrace>?B50 cs tcb x\<rbrace> case x of ArchObjectCap b \<Rightarrow> case b of arch_cap.PageDirectoryCap cur_pd b \<Rightarrow> case b of None \<Rightarrow> return True | Some x \<Rightarrow> return (cur_pd \<noteq> a) | _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>xa s. (xa \<longrightarrow> ?Q52 cs tcb x xa s) \<and> (\<not> xa \<longrightarrow> ?R52 cs tcb x xa s)\<rbrace>
 4. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B50 cs tcb\<rbrace>
 5. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 6. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 7. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (8 subgoals):
 1. \<And>cs tcb x xa. xa \<Longrightarrow> \<lbrace>?Q52 cs tcb x (ds_id True)\<rbrace> load_hw_asid b \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>cs tcb x xa. xa \<Longrightarrow> \<lbrace>?Q52 cs tcb x (ds_id True)\<rbrace> load_hw_asid b \<lbrace>\<lambda>r s. \<forall>x. r = Some x \<longrightarrow> transform s = cs\<rbrace>
 3. \<And>cs tcb x xa. \<not> xa \<Longrightarrow> \<lbrace>?R52 cs tcb x xa\<rbrace> return False \<lbrace>\<lambda>a b. transform b = cs\<rbrace>
 4. \<And>cs tcb x. \<lbrace>?B50 cs tcb x\<rbrace> case x of ArchObjectCap b \<Rightarrow> case b of arch_cap.PageDirectoryCap cur_pd b \<Rightarrow> case b of None \<Rightarrow> return True | Some x \<Rightarrow> return (cur_pd \<noteq> a) | _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>xa s. (xa \<longrightarrow> ?Q52 cs tcb x xa s) \<and> (\<not> xa \<longrightarrow> ?R52 cs tcb x xa s)\<rbrace>
 5. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B50 cs tcb\<rbrace>
 6. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 7. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 8. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (5 subgoals):
 1. \<And>cs tcb x. \<lbrace>?B50 cs tcb x\<rbrace> case x of ArchObjectCap b \<Rightarrow> case b of arch_cap.PageDirectoryCap cur_pd b \<Rightarrow> case b of None \<Rightarrow> return True | Some x \<Rightarrow> return (cur_pd \<noteq> a) | _ \<Rightarrow> return True | _ \<Rightarrow> return True \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>
 2. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?B50 cs tcb\<rbrace>
 3. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 4. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 5. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (4 subgoals):
 1. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>x s. (x = cap.NullCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc xd. x = cap.UntypedCap xa xb xc xd \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.EndpointCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.NotificationCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.ReplyCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = cap.CNodeCap xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = ThreadCap xa \<longrightarrow> transform s = cs) \<and> (x = cap.DomainCap \<longrightarrow> transform s = cs) \<and> (x = IRQControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = IRQHandlerCap xa \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc. x = Zombie xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = ASIDPoolCap x xb \<longrightarrow> transform s = cs) \<and> (xa = ASIDControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>x xb xc xd xe. xa = PageCap x xb xc xd xe \<longrightarrow> transform s = cs) \<and> (\<forall>x xb. xa = arch_cap.PageTableCap x xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xb. xa = arch_cap.PageDirectoryCap x xb \<longrightarrow> (xb = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. xb = Some x \<longrightarrow> transform s = cs)))\<rbrace>
 2. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 3. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 4. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal (5 subgoals):
 1. \<And>cs tcb. \<lbrace>?B49 cs tcb\<rbrace> CSpaceAcc_A.get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>cs tcb rv s. transform s = cs \<Longrightarrow> (rv = cap.NullCap \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> transform s = cs) \<and> (rv = cap.DomainCap \<longrightarrow> transform s = cs) \<and> (rv = IRQControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> transform s = cs) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = ASIDPoolCap xa xb \<longrightarrow> transform s = cs) \<and> (x = ASIDControlCap \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb xc xd xe. x = PageCap xa xb xc xd xe \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb. x = arch_cap.PageTableCap xa xb \<longrightarrow> transform s = cs) \<and> (\<forall>xa xb. x = arch_cap.PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> transform s = cs) \<and> (\<forall>x. xb = Some x \<longrightarrow> transform s = cs)))
 3. \<And>cs. \<lbrace>?B12 cs ()\<rbrace> gets cur_thread \<lbrace>?B49 cs\<rbrace>
 4. \<And>cs. \<lbrace>?Q11 cs\<rbrace> assert (word && mask pageBits = 0) \<lbrace>?B12 cs\<rbrace>
 5. \<And>cs s. transform s = cs \<Longrightarrow> ?Q11 cs s proof (prove)
goal:
No subgoals!