theory VSpace_C

lemma lookupPTSlot_ccorres:
  "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf
       (page_directory_at' pd)
       (UNIV \<inter> \<lbrace>\<acute>pd = Ptr pd \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr  \<rbrace>)
       []
       (lookupPTSlot pd vptr)
       (Call lookupPTSlot_'proc)" apply (cinit lift: pd_' vptr_') apply (simp add: liftE_bindE pde_case_isPageTablePDE) apply (rule ccorres_pre_getObject_pde) apply csymbr apply csymbr apply (rule ccorres_abstract_cleanup) apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE pde)"
               in ccorres_gen_asm2) apply (rule ccorres_cond2'[where R=\<top>]) apply (clarsimp simp: Collect_const_mem) apply simp apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: throwError_def  return_def syscall_error_rel_def) apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) apply (simp add: lookup_fault_missing_capability_lift) apply (simp add: mask_def) apply (rule ccorres_rhs_assoc)+ apply (simp add: checkPTAt_def bind_liftE_distrib liftE_bindE
                    returnOk_liftE[symmetric]) apply (rule ccorres_stateAssert) apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable pde))
                      and ko_at' pde (lookup_pd_slot pd vptr) and K (isPageTablePDE pde)"
               and P'=UNIV
            in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: returnOk_def return_def Collect_const_mem
                         lookup_pd_slot_def word_sle_def) apply (frule(1) page_table_at_rf_sr, clarsimp) apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt) apply (clarsimp simp: typ_heap_simps cpde_relation_def Let_def isPageTablePDE_def
                         pde_pde_coarse_lift_def pde_pde_coarse_lift
                  split: pde.split_asm split_of_bool_asm) apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift; simp) apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp) apply (simp add: word_shift_by_2 lookup_pt_slot_no_fail_def) apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift; simp) apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp) apply (simp add: word_shift_by_2 lookup_pt_slot_no_fail_def) apply (clarsimp simp: Collect_const_mem h_t_valid_clift) apply (frule(1) page_directory_at_rf_sr, clarsimp) apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) apply (simp add: pageBits_def) apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def
                        pde_pde_coarse_lift Let_def isPageTablePDE_def
                 split: ARM_H.pde.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (page_directory_at' pd) (UNIV \<inter> \<lbrace>\<acute>pd = pde_Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr\<rbrace>) [] (lookupPTSlot pd vptr) (Call lookupPTSlot_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda. \<lbrakk>vptra = vptr; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Q1228 vptra pda) (?Q'1228 vptra pda) [SKIP] (doE pde <- liftE (getObject (lookup_pd_slot pd vptr));
case pde of ARM_H.PageTablePDE x xa xb \<Rightarrow> doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 20
odE) (\<acute>pdSlot :== CALL lookupPDSlot_'proc(pda,vptra);;
(\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(\<acute>pdSlot);;
IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(SCAST(32 signed \<rightarrow> 32) (8 + 0xC));;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(\<acute>pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptra >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1228 vptra pda s \<and> s' \<in> ?Q'1228 vptra pda proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda. \<lbrakk>vptra = vptr; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Q1228 vptr (pde_Ptr pd)) (?Q'1228 vptr (pde_Ptr pd)) [SKIP] (do pde <- getObject (lookup_pd_slot pd vptr);
if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20
od) (\<acute>pdSlot :== CALL lookupPDSlot_'proc(pde_Ptr pd,vptr);;
(\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(\<acute>pdSlot);;
IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(\<acute>pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q1228 vptra pda s \<and> s' \<in> ?Q'1228 vptra pda proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde. \<lbrakk>vptra = vptr; pda = pde_Ptr pd\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (\<lambda>a. ?P1238 vptr (pde_Ptr pd) a pde) (?P'1239 vptr (pde_Ptr pd) pde) [SKIP] (if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20) (\<acute>pdSlot :== CALL lookupPDSlot_'proc(pde_Ptr pd,vptr);;
(\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(\<acute>pdSlot);;
IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(\<acute>pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ?P1238 vptra pda s pde) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> ?P'1239 vptra pda pde} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr)\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?P1246 vptr (pde_Ptr pd) pde) (?G'1255 vptr (pde_Ptr pd) pde pdSlot) [SKIP] (if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20) (\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pdSlot);;
IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ?P1246 vptra pda pde s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> ?G'1255 vptra pda pde v}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr)\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?P1246 vptr (pde_Ptr pd) pde) (?G'1589 vptr (pde_Ptr pd) pde pdSlot ret__unsigned \<inter> {s. ret__unsigned = pde_get_tag (the (cslift s pdSlot))}) [SKIP] (if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20) (IF ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ?P1246 vptra pda pde s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> ?G'1589 vptra pda pde v va}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr)\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?P1246 vptr (pde_Ptr pd) pde) (?G'1841 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20) (IF ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ?P1246 vptra pda pde s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> ?G'1841 vptra pda pde v va}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?P1246 vptr (pde_Ptr pd) pde) (?G'1845 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (if isPageTablePDE pde then doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE else throw $ Fault_H.lookup_failure.MissingCapability 20) (IF ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse THEN
  \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
ELSE
  lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'
FI)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ?P1246 vptra pda pde s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> ?G'1845 vptra pda pde v va \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (4 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (\<not> isPageTablePDE pde) = (s' \<in> \<lbrace>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace>)
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pt1860 vptr (pde_Ptr pd) pde) (?Rt1856 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (throw $ Fault_H.lookup_failure.MissingCapability 20) (\<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 4. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> ?Pt1860 vptra pda pde s) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rt1856 vptra pda pde v va) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pt1860 vptr (pde_Ptr pd) pde) (?Rt1856 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (throw $ Fault_H.lookup_failure.MissingCapability 20) (\<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> ?Pt1860 vptra pda pde s) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rt1856 vptra pda pde v va) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pt1860 vptr (pde_Ptr pd) pde) (?Rt1856 vptr (pde_Ptr pd) pde (pde_Ptr (lookup_pd_slot pd vptr)) ret__unsigned) [SKIP] (throwError (Fault_H.lookup_failure.MissingCapability 20)) (\<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> ?Pt1860 vptra pda pde s) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rt1856 vptra pda pde v va) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>current_lookup_fault :== CALL lookup_fault_missing_capability_new_'proc(0x14);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. NULL) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_' {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.lookup_failure.MissingCapability 20) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) rv (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_' s)}
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned \<sigma>. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. lookup_fault_missing_capability_lift (ret__struct_lookup_fault_C_' t) = \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = 0x14 && mask 6\<rparr> \<and> lookup_fault_get_tag (ret__struct_lookup_fault_C_' t) = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (throwError (Fault_H.lookup_failure.MissingCapability 20) \<sigma>). (\<sigma>', globals_update (current_lookup_fault_'_update (\<lambda>_. ret__struct_lookup_fault_C_' t)) s\<lparr>ret___struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) (ptSlot_C_update (\<lambda>_. NULL) (ret___struct_lookupPTSlot_ret_C_' s)), ret__struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) (ptSlot_C_update (\<lambda>_. NULL) (ret___struct_lookupPTSlot_ret_C_' s)), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) rv (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_' (globals_update (current_lookup_fault_'_update (\<lambda>_. ret__struct_lookup_fault_C_' t)) s\<lparr>ret___struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) (ptSlot_C_update (\<lambda>_. NULL) (ret___struct_lookupPTSlot_ret_C_' s)), ret__struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_LOOKUP_FAULT) (ptSlot_C_update (\<lambda>_. NULL) (ret___struct_lookupPTSlot_ret_C_' s)), global_exn_var_' := Return\<rparr>)))}
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>pde ret__unsigned \<sigma> x t. \<lbrakk>(ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde; (\<sigma>, x) \<in> rf_sr; lookup_fault_missing_capability_lift (ret__struct_lookup_fault_C_' t) = \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = 0x14 && mask 6\<rparr>; lookup_fault_get_tag (ret__struct_lookup_fault_C_' t) = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability\<rbrakk> \<Longrightarrow> EXCEPTION_LOOKUP_FAULT \<noteq> EXCEPTION_NONE \<and> (\<exists>lf. lookup_fault_lift (ret__struct_lookup_fault_C_' t) = Some (Lookup_fault_missing_capability lf) \<and> unat (lookup_fault_missing_capability_CL.bitsLeft_CL lf) = 20)
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>pde ret__unsigned \<sigma> x t. \<lbrakk>(ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde; (\<sigma>, x) \<in> rf_sr; lookup_fault_missing_capability_lift (ret__struct_lookup_fault_C_' t) = \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = 0x14 && mask 6\<rparr>; lookup_fault_get_tag (ret__struct_lookup_fault_C_' t) = SCAST(32 signed \<rightarrow> 32) lookup_fault_missing_capability\<rbrakk> \<Longrightarrow> \<exists>lf. lookup_fault_lift (ret__struct_lookup_fault_C_' t) = Some (Lookup_fault_missing_capability lf) \<and> unat (lookup_fault_missing_capability_CL.bitsLeft_CL lf) = 20
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>pde ret__unsigned \<sigma> x t. \<lbrakk>(ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde; (\<sigma>, x) \<in> rf_sr; lookup_fault_missing_capability_lift (ret__struct_lookup_fault_C_' t) = \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = 0x14 && mask 6\<rparr>; lookup_fault_lift (ret__struct_lookup_fault_C_' t) = Some (Lookup_fault_missing_capability \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = 0x14 && mask 6\<rparr>)\<rbrakk> \<Longrightarrow> unat (0x14 && mask 6) = 20
 2. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
lvar_nondet_init ptSlot_' ptSlot_'_update;;
lvar_nondet_init ptIndex_' ptIndex_'_update;;
\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_')
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde pdSlot ret__unsigned) [SKIP] (doE pt <- returnOk (ptrFromPAddr $ pdeTable pde);
withoutFailure $ lookupPTSlotFromPT pt vptr
odE) (lvar_nondet_init pt_' pt_'_update;;
(lvar_nondet_init ptSlot_' ptSlot_'_update;;
(lvar_nondet_init ptIndex_' ptIndex_'_update;;
(\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pdSlot);;
(\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
(\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
(\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
(Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
(\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
(\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'))))))))))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?Pf1858 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde (pde_Ptr (lookup_pd_slot pd vptr)) ret__unsigned) [SKIP] (do y <- stateAssert (page_table_at' (ptrFromPAddr (pdeTable pde))) [];
returnOk (lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr)
od) (lvar_nondet_init pt_' pt_'_update;;
(lvar_nondet_init ptSlot_' ptSlot_'_update;;
(lvar_nondet_init ptIndex_' ptIndex_'_update;;
(\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pde_Ptr (lookup_pd_slot pd vptr));;
(\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
(\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
(\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
(Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
(\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
(\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'))))))))))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> ?Pf1858 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_') (?P1948 vptr (pde_Ptr pd) pde) (?Rf1854 vptr (pde_Ptr pd) pde (pde_Ptr (lookup_pd_slot pd vptr)) ret__unsigned) [SKIP] (returnOk (lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr)) (lvar_nondet_init pt_' pt_'_update;;
(lvar_nondet_init ptSlot_' ptSlot_'_update;;
(lvar_nondet_init ptIndex_' ptIndex_'_update;;
(\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pde_Ptr (lookup_pd_slot pd vptr));;
(\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
(\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
(\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
(Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
(\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
(\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'))))))))))
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> ?P1948 vptra pda pde s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> ?Rf1854 vptra pda pde v va)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptr) and K (isPageTablePDE pde)) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} lvar_nondet_init pt_' pt_'_update;;
(lvar_nondet_init ptSlot_' ptSlot_'_update;;
(lvar_nondet_init ptIndex_' ptIndex_'_update;;
(\<acute>ret__unsigned :== CALL pde_pde_coarse_ptr_get_address_'proc(pde_Ptr (lookup_pd_slot pd vptr));;
(\<acute>ret__ptr_to_void :== CALL ptrFromPAddr_'proc(\<acute>ret__unsigned);;
(\<acute>pt :== PTR_COERCE(unit \<rightarrow> pte_C) \<acute>ret__ptr_to_void;;
(\<acute>ptIndex :== (vptr >> 12) && 0xFF;;
(Guard MemorySafety \<lbrace>\<acute>ptIndex = 0 \<or> array_assertion \<acute>pt (unat \<acute>ptIndex) (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>ptSlot :== \<acute>pt +\<^sub>p uint \<acute>ptIndex);;
(\<acute>ret___struct_lookupPTSlot_ret_C :== ptSlot_C_update (\<lambda>_. \<acute>ptSlot) \<acute>ret___struct_lookupPTSlot_ret_C;;
(\<acute>ret___struct_lookupPTSlot_ret_C :== lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) \<acute>ret___struct_lookupPTSlot_ret_C;;
return_C ret__struct_lookupPTSlot_ret_C_'_update ret___struct_lookupPTSlot_ret_C_'))))))))) {},{s. \<exists>(rv, \<sigma>')\<in>fst (returnOk (lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) rv (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_' s)}
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>vptra pda pde pdSlot ret__unsigned \<sigma>. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; pdSlot = pde_Ptr (lookup_pd_slot pd vptr); (ret__unsigned = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrakk> \<Longrightarrow> {s. (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptr) and K (isPageTablePDE pde)) \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>v va vb. s \<Turnstile>\<^sub>c pde_Ptr (lookup_pd_slot pd vptr) \<and> pde_get_tag (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<and> (\<forall>t. ret__unsigned_' t = pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))) \<longrightarrow> (\<forall>t. ret__ptr_to_void_' t = PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))))) \<longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))))))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals s)))) \<and> (\<exists>(rv, \<sigma>')\<in>fst (returnOk (lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))), ret__ptr_to_void_' := PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))))), pt_' := PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))), ptIndex_' := (vptr >> 12) && 0xFF, ptSlot_' := PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF), ret___struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ptSlot_C_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF)) (ret___struct_lookupPTSlot_ret_C_' s)), ret__struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ptSlot_C_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF)) (ret___struct_lookupPTSlot_ret_C_' s)), global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) rv (liftxf errstate lookupPTSlot_ret_C.status_C ptSlot_C ret__struct_lookupPTSlot_ret_C_' (s\<lparr>ret__unsigned_' := pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))), ret__ptr_to_void_' := PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr))))))), pt_' := PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))), ptIndex_' := (vptr >> 12) && 0xFF, ptSlot_' := PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF), ret___struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ptSlot_C_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF)) (ret___struct_lookupPTSlot_ret_C_' s)), ret__struct_lookupPTSlot_ret_C_' := lookupPTSlot_ret_C.status_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) (ptSlot_C_update (\<lambda>_. PTR_COERCE(unit \<rightarrow> pte_C) (PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift s (pde_Ptr (lookup_pd_slot pd vptr)))))))) +\<^sub>p uint ((vptr >> 12) && 0xFF)) (ret___struct_lookupPTSlot_ret_C_' s)), global_exn_var_' := Return\<rparr>)))))}
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>pde \<sigma> x. \<lbrakk>page_table_at' (ptrFromPAddr (pdeTable pde)) \<sigma>; ko_at' pde (pd + (vptr >> 20 << 2)) \<sigma>; (\<sigma>, x) \<in> rf_sr; isPageTablePDE pde\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c pde_Ptr (pd + (vptr >> 20 << 2)) \<and> pde_get_tag (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<and> ((\<exists>t. ret__unsigned_' t = pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) \<longrightarrow> (\<exists>t. ret__ptr_to_void_' t = PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) \<longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>pde \<sigma> x y. \<lbrakk>page_table_at' (ptrFromPAddr (pdeTable pde)) \<sigma>; ko_at' pde (pd + (vptr >> 20 << 2)) \<sigma>; (\<sigma>, x) \<in> rf_sr; isPageTablePDE pde; cslift x (pt_Ptr (ptrFromPAddr (pdeTable pde))) = Some y\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c pde_Ptr (pd + (vptr >> 20 << 2)) \<and> pde_get_tag (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<and> ((\<exists>t. ret__unsigned_' t = pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) \<longrightarrow> (\<exists>t. ret__ptr_to_void_' t = PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) \<longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>pde \<sigma> x y y'. \<lbrakk>page_table_at' (ptrFromPAddr (pdeTable pde)) \<sigma>; ko_at' pde (pd + (vptr >> 20 << 2)) \<sigma>; isPageTablePDE pde; cslift x (pt_Ptr (ptrFromPAddr (pdeTable pde))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some pde; cpde_relation pde y'; cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c pde_Ptr (pd + (vptr >> 20 << 2)) \<and> pde_get_tag (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))) = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse \<and> ((\<exists>t. ret__unsigned_' t = pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) \<longrightarrow> (\<exists>t. ret__ptr_to_void_' t = PTR(unit) (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) \<longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (pde_pde_coarse_CL.address_CL (pde_pde_coarse_lift (the (cslift x (pde_Ptr (pd + (vptr >> 20 << 2))))))) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (pdeTable pde)) vptr)
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) True x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) True x23); x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 1, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (ret__unsigned_' t))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 2. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (ret__unsigned_' t))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) True x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) True x23); x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 1, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> unat ((vptr >> 12) && 0xFF) \<le> 256
 2. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) True x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) True x23); x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 1, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 3. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (ret__unsigned_' t))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 4. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) True x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) True x23); x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 1, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 2. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (ret__unsigned_' t))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion (pte_Ptr (ptrFromPAddr (ret__unsigned_' t))) (unat ((vptr >> 12) && 0xFF)) (hrs_htd (t_hrs_' (globals x)))) \<and> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> unat ((vptr >> 12) && 0xFF) \<le> 256
 2. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 3. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x y y' x22 x23 t ta. \<lbrakk>cslift x (pde_Ptr (pd + (vptr >> 20 << 2))) = Some y'; page_table_at' (ptrFromPAddr (ret__unsigned_' t)) \<sigma>; ko_at' (ARM_H.PageTablePDE (ret__unsigned_' t) False x23) (pd + (vptr >> 20 << 2)) \<sigma>; cslift x (pt_Ptr (ptrFromPAddr (ret__unsigned_' t))) = Some y; map_to_pdes (ksPSpace \<sigma>) (pd + (vptr >> 20 << 2)) = Some (ARM_H.PageTablePDE (ret__unsigned_' t) False x23); \<not> x22; pde_lift y' = Some (Pde_pde_coarse \<lparr>pde_pde_coarse_CL.address_CL = ret__unsigned_' t, P_CL = 0, Domain_CL = x23\<rparr>); ret__ptr_to_void_' ta = PTR(unit) (ptrFromPAddr (ret__unsigned_' t))\<rbrakk> \<Longrightarrow> ptrFromPAddr (ret__unsigned_' t) + ((vptr >> 12) && 0xFF) * 4 = lookup_pt_slot_no_fail (ptrFromPAddr (ret__unsigned_' t)) vptr
 2. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (1 subgoal):
 1. \<And>vptra pda s s'. \<lbrakk>vptra = vptr; pda = pde_Ptr pd; (s, s') \<in> rf_sr; page_directory_at' pd s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde (lookup_pd_slot pd vptra) s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<not> isPageTablePDE pde \<longrightarrow> True) and (\<lambda>s. isPageTablePDE pde \<longrightarrow> page_table_at' (ptrFromPAddr (pdeTable pde)) s \<longrightarrow> (page_table_at' (ptrFromPAddr (pdeTable pde)) and ko_at' pde (lookup_pd_slot pd vptra) and K (isPageTablePDE pde)) s)) s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr (lookup_pd_slot pd vptra)) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<forall>v v'. v = pde_Ptr (lookupPDSlot (ptr_val (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) (vptr_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))) \<longrightarrow> pdSlot_'_update (\<lambda>_. v) s \<in> {s. s \<in> {s. \<forall>va v'. va = pde_get_tag (the (cslift (pde_ptr_'_update (\<lambda>_. v) s) (pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. s \<in> {s. va = pde_get_tag (the (cslift s v))} \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV) \<and> (s \<notin> \<lbrace>va \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_coarse\<rbrace> \<longrightarrow> s \<in> UNIV)} \<inter> \<lbrace>(va = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde\<rbrace>}}} \<inter> {s. pde_ptr_'_update (\<lambda>_. v) s \<Turnstile>\<^sub>c pde_ptr_' (pde_ptr_'_update (\<lambda>_. v) s)}}} \<inter> {s. array_assertion (pd_' (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s))) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals (vptr_'_update (\<lambda>_. vptra) (pd_'_update (\<lambda>_. pda) s)))))}} proof (prove)
goal (1 subgoal):
 1. \<And>s s' pde pde'. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' pd s; cslift s' (pde_Ptr (lookup_pd_slot pd vptr)) = Some pde'; cpde_relation pde pde'\<rbrakk> \<Longrightarrow> (pde_get_tag pde' = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde \<and> array_assertion (pde_Ptr pd) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' pde pde' y. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' pd s; cslift s' (pde_Ptr (lookup_pd_slot pd vptr)) = Some pde'; cpde_relation pde pde'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> (pde_get_tag pde' = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde \<and> array_assertion (pde_Ptr pd) (2 ^ pageBits) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>s s' pde pde' y. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' pd s; cslift s' (pde_Ptr (lookup_pd_slot pd vptr)) = Some pde'; cpde_relation pde pde'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> 2 ^ pageBits \<le> 4096
 2. \<And>s s' pde pde' y. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' pd s; cslift s' (pde_Ptr (lookup_pd_slot pd vptr)) = Some pde'; cpde_relation pde pde'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> (pde_get_tag pde' = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s s' pde pde' y. \<lbrakk>(s, s') \<in> rf_sr; page_directory_at' pd s; cslift s' (pde_Ptr (lookup_pd_slot pd vptr)) = Some pde'; cpde_relation pde pde'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> (pde_get_tag pde' = SCAST(32 signed \<rightarrow> 32) pde_pde_coarse) = isPageTablePDE pde \<and> True proof (prove)
goal:
No subgoals!