theory VSpace_C

lemma setVMRootForFlush_ccorres:
  "ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_'
       (invs' and (\<lambda>s. asid \<le> mask asid_bits))
       (UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}) []
       (setVMRootForFlush pd asid) (Call setVMRootForFlush_'proc)" apply (cinit lift: pd_' asid_') apply (rule ccorres_pre_getCurThread) apply (simp add: getThreadVSpaceRoot_def locateSlot_conv
               del: Collect_const) apply (rule ccorres_Guard_Seq)+ apply (ctac add: getSlotCap_h_val_ccorres) apply csymbr apply csymbr apply (simp add: cap_get_tag_isCap_ArchObject2
                 del: Collect_const) apply (rule ccorres_if_lhs) apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0)
                             = (capPDMappedASID (capCap rv) = None)
                         \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)
                             = capPDBasePtr (capCap rv)" in ccorres_gen_asm2) apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+ apply (rule ccorres_split_throws) apply (rule ccorres_return_C, simp+) apply vcg apply (rule ccorres_rhs_assoc2,
            rule ccorres_rhs_assoc2,
            rule ccorres_symb_exec_r) apply simp apply (ctac (no_vcg)add: armv_contextSwitch_ccorres) apply (ctac add: ccorres_return_C) apply wp apply simp apply vcg apply (rule conseqPre, vcg) apply (simp add: Collect_const_mem) apply clarsimp apply simp apply (wp hoare_drop_imps) apply vcg apply (clarsimp simp: Collect_const_mem word_sle_def
                        ccap_rights_relation_def cap_rights_to_H_def
                        mask_def[where n="Suc 0"]
                        allRights_def size_of_def cte_level_bits_def
                        tcbVTableSlot_def Kernel_C.tcbVTable_def invs'_invs_no_cicd) apply (clarsimp simp: rf_sr_ksCurThread ptr_add_assertion_positive) apply (subst rf_sr_tcb_ctes_array_assertion[THEN array_assertion_shrink_right],
    assumption, simp add: tcb_at_invs', simp add: tcb_cnode_index_defs)+ apply (clarsimp simp: rf_sr_ksCurThread ptr_val_tcb_ptr_mask' [OF tcb_at_invs']) apply (frule cte_at_tcb_at_16'[OF tcb_at_invs'], clarsimp simp: cte_wp_at_ctes_of) apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) apply (clarsimp simp: typ_heap_simps') apply (case_tac "isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv)") apply (clarsimp simp: isCap_simps(2) cap_get_tag_isCap_ArchObject[symmetric]) apply (clarsimp simp: cap_page_directory_cap_lift cap_to_H_def
                  elim!: ccap_relationE) apply (simp add: to_bool_def split: if_split) by (auto simp: cap_get_tag_isCap_ArchObject2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) (UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] (setVMRootForFlush pd asid) (Call setVMRootForFlush_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>asida pda. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q964 asida pda) (?Q'964 asida pda) [SKIP] (do tcb <- getCurThread;
threadRootSlot <- getThreadVSpaceRoot tcb;
threadRoot <- getSlotCap threadRootSlot;
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>threadRoot);;
(\<acute>ret__int :== (if \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if pde_Ptr \<acute>ret__unsigned = pda then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pda,asida);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))))))))
 2. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q964 asida pda s \<and> s' \<in> ?Q'964 asida pda proof (prove)
goal (2 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?P970 asida pda tcb) (?P'970 asida pda tcb) [SKIP] (do threadRootSlot <- getThreadVSpaceRoot tcb;
threadRoot <- getSlotCap threadRootSlot;
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>threadRoot);;
(\<acute>ret__int :== (if \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if pde_Ptr \<acute>ret__unsigned = pda then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pda,asida);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))))))))
 2. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P970 asida pda rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'970 asida pda rv} proof (prove)
goal (2 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?P970 asid (pde_Ptr pd) tcb) (?P'970 asid (pde_Ptr pd) tcb) [SKIP] (do threadRoot <- getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot);
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>threadRoot);;
(\<acute>ret__int :== (if \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))))))))
 2. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P970 asida pda rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'970 asida pda rv} proof (prove)
goal (2 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?P970 asid (pde_Ptr pd) tcb) (?C'988 asid (pde_Ptr pd) tcb) [SKIP] (do threadRoot <- getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot);
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od) (\<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C'']));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>threadRoot);;
(\<acute>ret__int :== (if \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(\<acute>threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))))))))
 2. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P970 asida pda rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?C'988 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q996 asida pda tcb rv) (?Q'996 asida pda tcb rv threadRoot) [SKIP] (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od) (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(threadRoot);;
(\<acute>ret__int :== (if \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))))
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q996 asida pda tcb\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> ?Q'996 asida pda tcb rv (threadRoot_' s)}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q996 asida pda tcb rv) (?G'1265 asida pda tcb rv threadRoot ret__unsigned) [SKIP] (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od) (\<acute>ret__int :== (if ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))))))
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q996 asida pda tcb\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'1265 asida pda tcb rv (threadRoot_' s) v}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q996 asida pda tcb rv) (?G'1382 asida pda tcb rv threadRoot ret__unsigned) [SKIP] (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od) (IF (if ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q996 asida pda tcb\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> ?G'1382 asida pda tcb rv (threadRoot_' s) v}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q996 asid (pde_Ptr pd) tcb rv) (?G'1382 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q996 asida pda tcb\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> ?G'1382 asida pda tcb rv (threadRoot_' s) v}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q1485 asid (pde_Ptr pd) tcb rv) (?S1488 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (let cur_pd = pd in return False) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> ?Q1485 asida pda tcb a b) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> ?S1488 asida pda tcb rv (threadRoot_' s) v) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd; (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = capPDBasePtr (capCap rv)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q1485 asid (pde_Ptr pd) tcb rv) (?G'1495 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (let cur_pd = pd in return False) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> ?Q1485 asida pda tcb a b) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> ?G'1495 asida pda tcb rv (threadRoot_' s) v \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigneda ret__unsignedb ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigneda = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd; (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd; ret__unsignedb = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot); ret__unsigned = pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q1485 asid (pde_Ptr pd) tcb rv) (?G'1877 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) pd) [SKIP] (return False) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false);;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> ?Q1485 asida pda tcb a b) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if va \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>vb v'. vb = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := vb\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if vb = pd then 1 else 0\<rparr> \<in> ?G'1877 asida pda tcb rv (threadRoot_' s) v va vb}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigneda ret__unsignedb ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigneda = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd; (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd; ret__unsignedb = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot); ret__unsigned = pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q1485 asid (pde_Ptr pd) tcb rv) (?P'1977 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) pd) [SKIP] (return False) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false))
 2. \<And>asida pda tcb rv threadRoot ret__unsigneda ret__unsignedb ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigneda = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd; (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd; ret__unsignedb = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot); ret__unsigned = pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1976 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) pd) return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false) {},UNIV
 3. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> ?Q1485 asida pda tcb a b) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 5. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if va \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>vb v'. vb = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := vb\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if vb = pd then 1 else 0\<rparr> \<in> ?P'1977 asida pda tcb rv (threadRoot_' s) v va vb \<inter> ?R'1976 asida pda tcb rv (threadRoot_' s) v va vb}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 6. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigneda ret__unsignedb ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigneda = cap_get_tag threadRoot; isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd; (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd; ret__unsignedb = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot); ret__unsigned = pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1976 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) pd) return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false) {},UNIV
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if va \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>vb v'. vb = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := vb\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if vb = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> ?R'1976 asida pda tcb rv (threadRoot_' s) v va vb}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI;;
(CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true)))))
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?Q'2000 asida pda tcb rv threadRoot ret__unsigned) [SKIP] (do armv_contextSwitch pd asid;
return True
od) (CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI (?Q'2000 asida pda tcb rv threadRoot ret__unsigned)
 3. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); ?R1484 asid (pde_Ptr pd) tcb rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 5. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 6. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?R1484 asid (pde_Ptr pd) tcb rv) (?Q'2000 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) [SKIP] (do a <- armv_contextSwitch pd asid;
return True
od) (CALL armv_contextSwitch_'proc(pde_Ptr pd,asid);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI (?Q'2000 asida pda tcb rv threadRoot ret__unsigned)
 3. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); ?R1484 asid (pde_Ptr pd) tcb rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> ?R1484 asida pda tcb a b)\<rbrace>
 5. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 6. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned rva xfdc. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' (?Q2011 asida pda tcb rv threadRoot ret__unsigned rva) (?Q'2025 tcb rv threadRoot rva xfdc) [SKIP] (return True) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd\<rbrakk> \<Longrightarrow> \<lbrace>?R2019 asid (pde_Ptr pd) tcb rv\<rbrace> armv_contextSwitch pd asid \<lbrace>?Q2011 asida pda tcb rv threadRoot ret__unsigned\<rbrace>
 3. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI ({s. asid_'_update (\<lambda>_. asida) (cap_pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>cap_pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'2024 asida pda tcb rv threadRoot ret__unsigned t rva})
 4. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R2019 asid (pde_Ptr pd) tcb rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 5. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R2019 asida pda tcb a) b)\<rbrace>
 6. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 7. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>}
flex-flex pairs:
\<lambda>tcb rv threadRoot t rva. ?Q'2025 tcb rv threadRoot rva (xfdc t) \<equiv>\<^sup>? \<lambda>tcb rv threadRoot. ?Q'2024 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) proof (prove)
goal (6 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd\<rbrakk> \<Longrightarrow> \<lbrace>?R2019 asid (pde_Ptr pd) tcb rv\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI ({s. asid_'_update (\<lambda>_. asida) (cap_pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>cap_pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) true = from_bool True\<rbrace>})
 3. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and ?R2019 asid (pde_Ptr pd) tcb rv) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and ?R2019 asida pda tcb a) b)\<rbrace>
 5. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 6. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI ({s. asid_'_update (\<lambda>_. asida) (cap_pd_'_update (\<lambda>_. pda) s) \<in> UNIV \<inter> \<lbrace>\<acute>cap_pd = pda\<rbrace> \<inter> \<lbrace>\<acute>asid = asida\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) true = from_bool True\<rbrace>})
 2. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot)) Cond (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) (\<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)) SKIP;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI UNIV
 2. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?T1486 asid (pde_Ptr pd) tcb rv threadRoot (cap_get_tag threadRoot) \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 4. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> ?T1486 asida pda tcb rv (threadRoot_' s) v)}}}}
 5. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. (s \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0))) \<and> (s \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' s \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' s \<noteq> 0 \<longrightarrow> (ret__int_' s \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' s \<noteq> 0 \<longrightarrow> True)))} \<inter> {s'. (s, s') \<in> rf_sr}) IF isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDIsMapped_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned \<noteq> 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_page_directory_cap_get_capPDBasePtr_'proc(threadRoot);;
\<acute>ret__int :== (if \<acute>ret__unsigned = pd then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) false)
FI {s'. (s, s') \<in> rf_sr}
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda tcb rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd); (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask local.asid_bits) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> {s. (s \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0))) \<and> (s \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' s \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' s \<noteq> 0 \<longrightarrow> (ret__int_' s \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' s \<noteq> 0 \<longrightarrow> True)))} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> ((if capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0 \<and> ((if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0 \<longrightarrow> (s, sa\<lparr>ret__unsigned_' := capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot), ret__int_' := 0\<rparr>) \<in> rf_sr))) \<and> ((if capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> (s, sa\<lparr>ret__unsigned_' := capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot), ret__int_' := 0\<rparr>) \<in> rf_sr))) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv)) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0 \<and> ((if capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) = pd then 1 else 0) = 0 \<longrightarrow> (s, sa\<lparr>ret__unsigned_' := capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot), ret__int_' := 0\<rparr>) \<in> rf_sr))) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (s, sa) \<in> rf_sr)))}
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>asida pda rv threadRoot ret__unsigned s. \<lbrakk>asida = asid; pda = pde_Ptr pd; ccap_relation rv threadRoot; ret__unsigned = cap_get_tag threadRoot; isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd; all_invs_but_ct_idle_or_in_cur_domain' s \<and> asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> \<lbrace>(isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> \<acute>ret__int \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd))\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd \<and> (capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd \<longrightarrow> (s, sa) \<in> rf_sr))) \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0 \<longrightarrow> (s, sa) \<in> rf_sr))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> cap_get_tag threadRoot = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot)) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd \<and> (capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) \<noteq> pd \<longrightarrow> (s, sa) \<in> rf_sr))) \<and> (ret__int_' sa = 0 \<longrightarrow> (s, sa) \<in> rf_sr))}
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 3. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 4. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd \<longrightarrow> True) \<and> (\<not> (isArchObjectCap a \<and> isPageDirectoryCap (capCap a) \<and> (\<exists>y. capPDMappedASID (capCap a) = Some y) \<and> capPDBasePtr (capCap a) = pd) \<longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asida \<le> mask local.asid_bits) and (\<lambda>a. True)) b)\<rbrace>
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 3. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<lbrace>?R1004 asid (pde_Ptr pd) tcb\<rbrace> getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>a b. (isPageDirectoryCap (capCap a) \<longrightarrow> isArchObjectCap a \<longrightarrow> capPDMappedASID (capCap a) = None \<or> capPDBasePtr (capCap a) \<noteq> pd) \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' b \<and> asid \<le> mask local.asid_bits\<rbrace>
 2. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 3. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and ?R1004 asida pda rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>asida pda tcb. \<lbrakk>asida = asid; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'998 asid (pde_Ptr pd) tcb) \<acute>threadRoot :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])) {s. \<forall>rv. ccap_relation rv (threadRoot_' s) \<longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa\<lparr>ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> {sa. (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. sa\<lparr>ret__int_' := if v \<noteq> 0 then 1 else 0\<rparr> \<in> {sa. \<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. s\<lparr>ret__int_' := if v = pd then 1 else 0\<rparr> \<in> \<lbrace>SCAST(32 signed \<rightarrow> 32) false = from_bool False\<rbrace> \<inter> \<lbrace>True\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap}}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. threadRoot_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap} \<inter> \<lbrace>(capPDIsMapped_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>threadRoot) = capPDBasePtr (capCap rv)\<rbrace>) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> sa \<in> {sa. (sa \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0))) \<and> (sa \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (threadRoot_' s)) = pd then 1 else 0) = 0)) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> (ret__int_' sa \<noteq> 0 \<longrightarrow> False) \<and> (\<not> ret__int_' sa \<noteq> 0 \<longrightarrow> True)))})}}}}
 2. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> ?R'998 asida pda rv \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>asida pda s s'. \<lbrakk>asida = asid; pda = pde_Ptr pd; (s, s') \<in> rf_sr; (invs' and (\<lambda>s. asid \<le> mask local.asid_bits)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. all_invs_but_ct_idle_or_in_cur_domain' a \<and> asida \<le> mask local.asid_bits)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> \<lbrace>cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10) = cte_Ptr (rv + 2 ^ cte_level_bits * tcbVTableSlot)\<rbrace> \<inter> {s. \<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (\<forall>v. v = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> (\<forall>v v'. v = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<longrightarrow> (\<forall>v v'. v = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) false = from_bool False \<and> True) \<and> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) \<and> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) = capPDBasePtr (capCap rv)) \<and> (\<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd) \<longrightarrow> (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])), ret__unsigned_' := v, ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<in> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<longrightarrow> (if capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) = pd then 1 else 0) = 0))) \<and> (s\<lparr>threadRoot_' := h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])), ret__unsigned_' := v, ret__int_' := if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0\<rparr> \<notin> (if isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) then UNIV else {}) \<longrightarrow> ((if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 \<longrightarrow> v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (\<forall>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) \<longrightarrow> (if capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)\<rightarrow>[''cap_C''])))) = pd then 1 else 0) = 0)) \<and> (\<not> (if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 \<longrightarrow> ((if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 \<longrightarrow> False) \<and> (\<not> (if v = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap then 1 else 0) \<noteq> 0 \<longrightarrow> True)))))} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace> \<inter> {s. s \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (ksCurThread_' (globals s)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbVTable * 0x10)} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbVTable) False (hrs_htd \<acute>t_hrs)\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00 = rv \<and> (\<forall>rva. ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rva \<and> isPageDirectoryCap (capCap rva) \<and> (\<exists>y. capPDMappedASID (capCap rva) = Some y) \<and> capPDBasePtr (capCap rva) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rva) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rva) \<longrightarrow> isArchObjectCap rva \<longrightarrow> capPDMappedASID (capCap rva) = None \<or> capPDBasePtr (capCap rva) \<noteq> pd) \<longrightarrow> (isArchObjectCap rva \<and> isPageDirectoryCap (capCap rva) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rva \<longrightarrow> \<not> isPageDirectoryCap (capCap rva)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ptr_add_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00)) 1 False (hrs_htd (t_hrs_' (globals s'))) \<and> s' \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00) + 0x10) \<and> ptr_add_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr rv) && 0xFFFFFE00)) 1 False (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00 = ksCurThread s \<and> (\<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> array_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00)) (Suc 0) (hrs_htd (t_hrs_' (globals s'))) \<and> s' \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10) \<and> array_assertion (cte_Ptr (ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00)) (Suc 0) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00 = ksCurThread s \<and> (\<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> True \<and> s' \<Turnstile>\<^sub>c cte_Ptr ((ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00) + 0x10) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> (\<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> s' \<Turnstile>\<^sub>c cte_Ptr (ksCurThread s + 0x10) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte\<rbrakk> \<Longrightarrow> (\<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> s' \<Turnstile>\<^sub>c cte_Ptr (ksCurThread s + 0x10) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte y'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'\<rbrakk> \<Longrightarrow> (\<forall>rv. ccap_relation rv (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> 0 \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C'']))))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (cap_Ptr &(cte_Ptr (ksCurThread s + 0x10)\<rightarrow>[''cap_C''])))) \<noteq> pd))) \<and> s' \<Turnstile>\<^sub>c cte_Ptr (ksCurThread s + 0x10) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y')\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y'); isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv)\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))
 2. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y'); \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv))\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte y' v0. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation (capability.ArchObjectCap v0) (cte_C.cap_C y'); cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap\<rbrakk> \<Longrightarrow> ((\<exists>y. capPDMappedASID v0 = Some y) \<and> capPDBasePtr v0 = pd \<longrightarrow> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID v0 = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> (capPDMappedASID v0 = None \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd) \<and> (capPDBasePtr v0 \<noteq> pd \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)
 2. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y'); \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv))\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)) proof (prove)
goal (2 subgoals):
 1. \<And>s s' cte y'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; cap_lift (cte_C.cap_C y') = Some (Cap_page_directory_cap (cap_page_directory_cap_lift (cte_C.cap_C y')))\<rbrakk> \<Longrightarrow> ((\<exists>y. (if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) else None) = Some y) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd \<longrightarrow> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = ((if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) else None) = None)) \<and> ((if to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) then Some (capPDMappedASID_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) else None) = None \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)
 2. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y'); \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv))\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte y' rv. \<lbrakk>(s, s') \<in> rf_sr; invs' s; asid \<le> mask local.asid_bits; ctes_of s (ksCurThread s + 0x10) = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr (ksCurThread s + 0x10)) = Some y'; ccap_relation rv (cte_C.cap_C y'); \<not> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv))\<rbrakk> \<Longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<and> (\<exists>y. capPDMappedASID (capCap rv) = Some y) \<and> capPDBasePtr (capCap rv) = pd \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> (capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = 0) = (capPDMappedASID (capCap rv) = None) \<and> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) = pd) \<and> ((isPageDirectoryCap (capCap rv) \<longrightarrow> isArchObjectCap rv \<longrightarrow> capPDMappedASID (capCap rv) = None \<or> capPDBasePtr (capCap rv) \<noteq> pd) \<longrightarrow> (isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDIsMapped_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> 0 \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<and> ((\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))) \<and> ((isArchObjectCap rv \<longrightarrow> \<not> isPageDirectoryCap (capCap rv)) \<longrightarrow> cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (\<exists>t. ret__unsigned_' t = capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y'))) \<longrightarrow> capPDBasePtr_CL (cap_page_directory_cap_lift (cte_C.cap_C y')) \<noteq> pd))