theory VSpace_C

lemma performPageTableInvocationMap_ccorres:
  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (cte_at' ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits)))
       (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = Ptr ctSlot\<rbrace> \<inter> \<lbrace>cpde_relation pde \<acute>pde\<rbrace> \<inter> \<lbrace>\<acute>pdSlot = Ptr pdSlot\<rbrace>)
       []
       (liftE (performPageTableInvocation (PageTableMap cap ctSlot pde pdSlot)))
       (Call performPageTableInvocationMap_'proc)" apply (simp only: liftE_liftM ccorres_liftM_simp) apply (cinit lift: cap_' ctSlot_' pde_' pdSlot_') apply (ctac (no_vcg)) apply (rule ccorres_split_nothrow_novcg) apply simp apply (erule storePDE_Basic_ccorres) apply ceqv apply (rule ccorres_symb_exec_r) apply (rule ccorres_add_return2) apply (rule ccorres_split_nothrow_novcg) apply simp apply (rule ccorres_call) apply (rule cleanByVA_PoU_ccorres) apply (rule refl) apply (simp add: xfdc_def) apply simp apply ceqv apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply wp apply (simp add: guard_is_UNIV_def) apply vcg apply (rule conseqPre, vcg) apply clarsimp apply wp apply (simp add: guard_is_UNIV_def) apply wp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>cpde_relation pde \<acute>pde\<rbrace> \<inter> \<lbrace>\<acute>pdSlot = pde_Ptr pdSlot\<rbrace>) [] (liftE (performPageTableInvocation (ARM_H.PageTableMap cap ctSlot pde pdSlot))) (Call performPageTableInvocationMap_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>cpde_relation pde \<acute>pde\<rbrace> \<inter> \<lbrace>\<acute>pdSlot = pde_Ptr pdSlot\<rbrace>) [] (performPageTableInvocation (ARM_H.PageTableMap cap ctSlot pde pdSlot)) (Call performPageTableInvocationMap_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q485 pdSlota pdea ctSlota capa) (?Q'485 pdSlota pdea ctSlota capa) [SKIP] (do y <- updateCap ctSlot cap;
y <- storePDE pdSlot pde;
doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ctSlota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(ctSlota\<rightarrow>[''cap_C''])) capa)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update pdSlota pdea)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q485 pdSlota pdea ctSlota capa s \<and> s' \<in> ?Q'485 pdSlota pdea ctSlota capa proof (prove)
goal (4 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q494 pdSlota pdea ctSlota capa y) (?Q'494 pdSlota pdea ctSlota capa y xfdc) [SKIP] (do y <- storePDE pdSlot pde;
doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update pdSlota pdea)));;
(\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>?Q494 pdSlota pdea ctSlota capa\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'494 pdSlota pdea ctSlota capa rv (xfdc s)
 4. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> ccorres (?r'515 pdSlota pdea ctSlota capa y xfdc) (?xf'515 pdSlota pdea ctSlota capa y xfdc) (?P516 pdSlota pdea ctSlota capa y) (?Q'494 pdSlota pdea ctSlota capa y xfdc) [] (storePDE pdSlot pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pdSlota} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update pdSlota pdea))))
 2. \<And>pdSlota pdea ctSlota capa y xfdc rv' t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'515 pdSlota pdea ctSlota capa y xfdc) rv' t t' (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'515 pdSlota pdea ctSlota capa y xfdc rv')
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; ?r'515 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (?d'515 pdSlota pdea ctSlota capa y xfdc rv')
 4. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'515 pdSlota pdea ctSlota capa y xfdc) (?xf'515 pdSlota pdea ctSlota capa y xfdc) (?Q'515 pdSlota pdea ctSlota capa y xfdc)
 6. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. ?P516 pdSlota pdea ctSlota capa y and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'494 pdSlota pdea ctSlota capa rv (xfdc s)
 8. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres (?r'515 pdSlota pdea ctSlota capa y xfdc) (?xf'515 pdSlota pdea ctSlota capa y xfdc) (?P516 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa ()) (?Q'494 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa () xfdc) [] (storePDE pdSlot pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr pdSlot} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr pdSlot) pdea))))
 2. \<And>pdSlota pdea ctSlota capa y xfdc rv' t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'515 pdSlota pdea ctSlota capa y xfdc) rv' t t' (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'515 pdSlota pdea ctSlota capa y xfdc rv')
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; ?r'515 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (?d'515 pdSlota pdea ctSlota capa y xfdc rv')
 4. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'515 pdSlota pdea ctSlota capa y xfdc) (?xf'515 pdSlota pdea ctSlota capa y xfdc) (?Q'515 pdSlota pdea ctSlota capa y xfdc)
 6. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. ?P516 pdSlota pdea ctSlota capa y and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> ?Q'494 pdSlota pdea ctSlota capa rv (xfdc s)
 8. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdca rv' t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))) (?d'515 pdSlota pdea ctSlota capa y xfdca rv')
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (?d'515 pdSlota pdea ctSlota capa y xfdc rv')
 3. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 4. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 5. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota);;
(CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 4. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv')
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ?Q515 pdSlota pdea ctSlota capa y xfdc ya s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 4. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 6. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q515 pdSlota pdea ctSlota capa y xfdc ya) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv') [SKIP] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) >>= return) (CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv')
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ?Q515 pdSlota pdea ctSlota capa y xfdc ya s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 4. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>?Q515 pdSlota pdea ctSlota capa y xfdc\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 6. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ccorres (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?P545 pdSlota pdea ctSlota capa y xfdc ya) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv') [] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (CALL cleanByVA_PoU_'proc(ptr_val pdSlota,\<acute>ret__unsigned_long))
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ?r'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv')
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; (?P545 pdSlota pdea ctSlota capa y xfdc ya and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 8. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. ?P545 pdSlota pdea ctSlota capa y xfdc ya and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 10. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?P545 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa () xfdc ()) (?Q'538 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa () xfdc () rv') [] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (CALL cleanByVA_PoU_'proc(pdSlot,\<acute>ret__unsigned_long))
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ?r'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) (?Q'538 pdSlota pdea ctSlota capa y xfdc ya rv')
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; (?P545 pdSlota pdea ctSlota capa y xfdc ya and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 8. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. ?P545 pdSlota pdea ctSlota capa y xfdc ya and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 10. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ccorres (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf''562 pdSlota pdea ctSlota capa y xfdc ya rv') (?P545 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa () xfdc ()) (?C'565 (pde_Ptr pdSlot) pdea (cte_Ptr ctSlot) capa () xfdc () rv') [] (doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot))) (Call cleanByVA_PoU_'proc)
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s ta sa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals sa = globals sa
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' a s t. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv' (s\<lparr>globals := globals t\<rparr>) = ?xf''562 pdSlota pdea ctSlota capa y xfdc ya rv' t
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals (paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s)) = globals s
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ?r'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV (?r'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 9. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> ?C'565 pdSlota pdea ctSlota capa y xfdc ya rv'}
 10. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; (?P545 pdSlota pdea ctSlota capa y xfdc ya and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s ta sa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals sa = globals sa
 2. \<And>pdSlota pdea ctSlota capa y xfdca ya rv' a s t. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ?xf'544 pdSlota pdea ctSlota capa y xfdca ya rv' (s\<lparr>globals := globals t\<rparr>) = xfdc t
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals (paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s)) = globals s
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 8. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 9. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 10. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdca ya rv' a s t. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> ?xf'544 pdSlota pdea ctSlota capa y xfdca ya rv' (s\<lparr>globals := globals t\<rparr>) = xfdc t
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals (paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s)) = globals s
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (?xf'544 pdSlota pdea ctSlota capa y xfdc ya rv') (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 8. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 9. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 10. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> globals (paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s)) = globals s
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (\<lambda>a. 0) rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 7. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 8. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 10. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' rv'a t t'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> ceqv \<Gamma> (\<lambda>a. 0) rv'a t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (?d'544 pdSlota pdea ctSlota capa y xfdc ya rv' rv'a)
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 6. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 7. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 9. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 10. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> ccorres (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q544 pdSlota pdea ctSlota capa y xfdc ya rv' x) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a) [SKIP] (return x) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>?Q544 pdSlota pdea ctSlota capa y xfdc ya rv'\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (?Q'544 pdSlota pdea ctSlota capa y xfdc ya rv')
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 6. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 8. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 10. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc \<circ> Inr) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (\<lambda>x rv'a. UNIV)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 6. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 8. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 10. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' x rv'a \<sigma>. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; dc x rv'a\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (K (K (\<lambda>_. False)) \<currency> dc) (Inr rv) (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (\<lambda>x rv'a. UNIV)
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 5. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 6. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 8. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 10. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace> doMachineOp (cleanByVA_PoU pdSlot (addrFromPPtr pdSlot)) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (\<lambda>x rv'a. UNIV)
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 4. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 5. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and ?R546 pdSlota pdea ctSlota capa y xfdc ya\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 7. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 9. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> guard_is_UNIV dc (\<lambda>a. 0) (\<lambda>x rv'a. UNIV)
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 3. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 4. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 6. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 8. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv') \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s. paddr_'_update (\<lambda>_. ret__unsigned_long_' s) (vaddr_'_update (\<lambda>_. pdSlot) s) \<in> \<lbrace>\<acute>vaddr = pdSlot\<rbrace> \<inter> \<lbrace>\<acute>paddr = addrFromPPtr pdSlot\<rbrace>}
 2. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'515 pdSlota pdea ctSlota capa y xfdc ya rv' \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 3. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>
 4. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'515 pdSlota pdea ctSlota capa y xfdca)
 5. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 7. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(PTR_COERCE(pde_C \<rightarrow> unit) pdSlota) {s'. (s, s') \<in> rf_sr}
 2. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>ya rv'. \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace>)
 4. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc ya rv' s. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc; dc ya rv'; ((\<lambda>a. True) and (\<lambda>a. True)) s\<rbrakk> \<Longrightarrow> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. \<forall>t. ret__unsigned_long_' t = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> (s, sa\<lparr>ret__unsigned_long_' := addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota))\<rparr>) \<in> rf_sr}
 2. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>ya rv'. \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace>)
 4. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 6. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdc. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R517 pdSlota pdea ctSlota capa y\<rbrace> storePDE pdSlot pde \<lbrace>\<lambda>ya. (\<lambda>a. True) and (\<lambda>a. True)\<rbrace>
 2. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>ya rv'. \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace>)
 3. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and ?R517 pdSlota pdea ctSlota capa y\<rbrace>
 4. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 5. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pdSlota pdea ctSlota capa y xfdca. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc y xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>ya rv'. \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) \<longrightarrow> addrFromPPtr (ptr_val (PTR_COERCE(pde_C \<rightarrow> unit) pdSlota)) = addrFromPPtr pdSlot\<rbrace>)
 2. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and (\<lambda>a. True \<and> True)\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 4. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>pdSlota pdea ctSlota capa. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa\<rbrakk> \<Longrightarrow> \<lbrace>?R494 pdSlota pdea ctSlota capa\<rbrace> updateCap ctSlot cap \<lbrace>\<lambda>y. (\<lambda>a. valid_pde_mapping_offset' (pdSlot && mask pdBits)) and (\<lambda>a. True \<and> True)\<rbrace>
 2. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 3. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R494 pdSlota pdea ctSlota capa and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>pdSlota pdea ctSlota capa s rv. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; dc rv (xfdc s)\<rbrakk> \<Longrightarrow> s \<in> \<lbrace>pdSlot = pdSlot\<rbrace>
 2. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_pde_mapping_offset' (pdSlot && mask pdBits) \<and> True \<and> True) and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pdSlota pdea ctSlota capa s s'. \<lbrakk>pdSlota = pde_Ptr pdSlot; cpde_relation pde pdea; ctSlota = cte_Ptr ctSlot; ccap_relation cap capa; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>_. True) ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. valid_pde_mapping_offset' (pdSlot && mask pdBits) \<and> True \<and> True) and cte_wp_at' (\<lambda>_. True) (ptr_val ctSlota)) s \<and> s' \<in> \<lbrace>ccap_relation cap capa\<rbrace> \<inter> \<lbrace>ctSlota = cte_Ptr ctSlot\<rbrace> \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!