theory CSpace_C

lemma ensureEmptySlot_ccorres:
  "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_')
   \<top>  (UNIV \<inter> \<lbrace>slot = ptr_val (\<acute>slot)\<rbrace>) []
   (ensureEmptySlot slot) (Call ensureEmptySlot_'proc)" apply (cinit lift: slot_') apply (rule ccorres_liftE_Seq) apply (rule ccorres_getCTE) apply (rule ccorres_move_c_guard_cte) apply (rule_tac P= "\<lambda> s. ctes_of s (ptr_val slota) = Some cte"
               and P' =UNIV in ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (frule (1) rf_sr_ctes_of_clift, clarsimp) apply (simp add: typ_heap_simps) apply (rule conjI) apply (clarsimp simp: unlessE_def throwError_def return_def) apply (subgoal_tac "cap_to_H (cap_CL y) \<noteq> capability.NullCap") apply simp apply (simp add: syscall_error_rel_def EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) apply (rule syscall_error_to_H_cases(8)) apply simp apply (subst cap_get_tag_NullCap [symmetric]) prefer 2 apply assumption apply (simp add: ccap_relation_def c_valid_cte_def) apply (clarsimp simp: unlessE_def throwError_def return_def) apply (subgoal_tac "cap_to_H (cap_CL y) = capability.NullCap") apply simp apply (simp add: returnOk_def return_def) apply (subst cap_get_tag_NullCap [symmetric]) prefer 2 apply assumption apply (simp add: ccap_relation_def c_valid_cte_def) apply clarsimp apply (simp add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') (\<lambda>_. True) (UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>) [] (ensureEmptySlot slot) (Call ensureEmptySlot_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>slota. slot = ptr_val slota \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') (?Q116 slota) (?Q'116 slota) [SKIP] (doE cte <- liftE (getCTE slot);
unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)
odE) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))));;
(IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 slota s \<and> s' \<in> ?Q'116 slota proof (prove)
goal (2 subgoals):
 1. \<And>slota. slot = ptr_val slota \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') (?Q116 slota) (?Q'116 slota) [SKIP] (do cte <- getCTE slot;
unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))));;
(IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q116 slota s \<and> s' \<in> ?Q'116 slota proof (prove)
goal (2 subgoals):
 1. \<And>slota cte. slot = ptr_val slota \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') (?P124 slota cte) (?P'124 slota cte) [SKIP] (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))));;
(IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ?P124 slota cte s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?P'124 slota (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>slota cte. slot = ptr_val slota \<Longrightarrow> ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_') (?A126 slota cte) (?C'126 slota cte) [SKIP] (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst)) (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])));;
(IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (?A126 slota cte and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> ?C'126 slota (cte_to_H cte') \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota cte. slot = ptr_val slota \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. ctes_of \<sigma> (ptr_val slota) = Some cte \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL cap_get_capType_'proc(h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(slota\<rightarrow>[''cap_C''])));;
(IF \<acute>ret__unsigned \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) {},{s. \<exists>(rv, \<sigma>')\<in>fst (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' s)}
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota cte \<sigma>. slot = ptr_val slota \<Longrightarrow> {s. ctes_of \<sigma> (ptr_val slota) = Some cte \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<forall>t. ret__unsigned_' t = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) \<longrightarrow> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals s)))) (s\<lparr>ret__unsigned_' := cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals s)))) (s\<lparr>ret__unsigned_' := cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals s))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (s\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))}
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota cte \<sigma> x t. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some cte; (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rbrakk> \<Longrightarrow> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cteCap cte = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C''])))\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (cap_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (cap_Ptr &(slota\<rightarrow>[''cap_C'']))) = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (cte_C.cap_C cte')\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (cte_C.cap_C cte')\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((if cap_to_H (cap_CL y) = capability.NullCap then returnOk () else (\<lambda>s. ({(Inl Fault_H.syscall_error.DeleteFirst, s)}, False))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (cte_C.cap_C cte')\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((if cap_to_H (cap_CL y) = capability.NullCap then returnOk () else (\<lambda>s. ({(Inl Fault_H.syscall_error.DeleteFirst, s)}, False))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (cte_C.cap_C cte')\<rparr>)\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) \<noteq> capability.NullCap
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> EXCEPTION_SYSCALL_ERROR \<noteq> EXCEPTION_NONE \<and> syscall_error_rel Fault_H.syscall_error.DeleteFirst (SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) (errstate (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x)))) (x\<lparr>ret__unsigned_' := cap_get_tag (cte_C.cap_C cte')\<rparr>)))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) \<noteq> capability.NullCap
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> syscall_error_to_H (type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x))) (lookup_fault_lift (current_lookup_fault_' (globals x))) = Some Fault_H.syscall_error.DeleteFirst
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) \<noteq> capability.NullCap
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> type_C (type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst) (current_syscall_error_' (globals x))) = SCAST(32 signed \<rightarrow> 32) seL4_DeleteFirst
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) \<noteq> capability.NullCap
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) \<noteq> capability.NullCap
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (?cap'191 slota \<sigma> x t cte' y)
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_get_tag (?cap'191 slota \<sigma> x t cte' y) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_get_tag (?cap'191 slota \<sigma> x t cte' y) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (?cap'191 slota \<sigma> x t cte' y)
 3. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 4. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') \<noteq> SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (cte_C.cap_C cte')
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = cap_get_tag (cte_C.cap_C cte'); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap \<longrightarrow> (\<exists>xa\<in>fst (unlessE (cap_to_H (cap_CL y) = capability.NullCap) (throwError Fault_H.syscall_error.DeleteFirst) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((if cap_to_H (cap_CL y) = capability.NullCap then returnOk () else (\<lambda>s. ({(Inl Fault_H.syscall_error.DeleteFirst, s)}, False))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((if cap_to_H (cap_CL y) = capability.NullCap then returnOk () else (\<lambda>s. ({(Inl Fault_H.syscall_error.DeleteFirst, s)}, False))) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) = capability.NullCap
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cap_to_H (cap_CL y) = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (returnOk () \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := SCAST(32 signed \<rightarrow> 32) cap_null_cap, ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) = capability.NullCap
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_to_H (cap_CL y) = capability.NullCap
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (?cap'198 slota \<sigma> x t cte' y)
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_get_tag (?cap'198 slota \<sigma> x t cte' y) = SCAST(32 signed \<rightarrow> 32) cap_null_cap
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> cap_get_tag (?cap'198 slota \<sigma> x t cte' y) = SCAST(32 signed \<rightarrow> 32) cap_null_cap
 2. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (?cap'198 slota \<sigma> x t cte' y)
 3. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>slota \<sigma> x t cte' y. \<lbrakk>slot = ptr_val slota; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = SCAST(32 signed \<rightarrow> 32) cap_null_cap; cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; cap_get_tag (cte_C.cap_C cte') = SCAST(32 signed \<rightarrow> 32) cap_null_cap\<rbrakk> \<Longrightarrow> ccap_relation (cap_to_H (cap_CL y)) (cte_C.cap_C cte')
 2. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>slota s s'. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. ctes_of s (ptr_val slota) = Some cte) and cte_wp_at' (\<lambda>_. True) (ptr_val slota)) s) \<and> s' \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr slot) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>slota s s' cte. \<lbrakk>slot = ptr_val slota; (s, s') \<in> rf_sr; ctes_of s (ptr_val slota) = Some cte\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (ptr_val slota) s proof (prove)
goal:
No subgoals!