theory CSpace_C

lemma ensureNoChildren_ccorres:
  "ccorres (syscall_error_rel \<currency> dc) (liftxf errstate id undefined ret__unsigned_long_')
   (\<lambda>s. valid_objs' s \<and> valid_mdb' s) (UNIV \<inter> \<lbrace>slot = ptr_val (\<acute>slot)\<rbrace>) []
   (ensureNoChildren slot) (Call ensureNoChildren_'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. valid_objs' s \<and> valid_mdb' s \<and> 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 (clarsimp simp: whenE_def throwError_def return_def nullPointer_def liftE_bindE) apply (clarsimp simp: returnOk_def return_def) \<comment> \<open>solve the case where mdbNext is zero\<close>

   \<comment> \<open>main goal\<close> apply (simp add: ccte_relation_def) apply (frule_tac cte="cte_to_H y" in valid_mdb_ctes_of_next, simp+) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule_tac cte=cte in rf_sr_ctes_of_clift, assumption, clarsimp) apply (rule conjI) apply (frule_tac cte="(cte_to_H ya)" in ctes_of_valid', assumption, simp) apply (rule valid_capAligned, assumption) apply (rule conjI) apply (frule_tac cte="(cte_to_H y)" in ctes_of_valid', assumption, simp) apply blast apply clarsimp apply (rule conjI)
   \<comment> \<open>isMDBParentOf is not zero\<close> apply clarsimp apply (case_tac "isMDBParentOf (cte_to_H y) (cte_to_H ya)", simp_all)[1] apply (simp add: bind_def) apply (simp add: split_paired_Bex) apply (clarsimp simp: in_getCTE_cte_wp_at') apply (simp add: cte_wp_at_ctes_of) apply (simp add: syscall_error_rel_def EXCEPTION_NONE_def EXCEPTION_SYSCALL_ERROR_def) apply (simp add: syscall_error_to_H_cases(9))
   \<comment> \<open>isMDBParentOf is zero\<close> apply clarsimp apply (case_tac "isMDBParentOf (cte_to_H y) (cte_to_H ya)", simp_all)[1] apply (simp add: bind_def) apply (simp add: split_paired_Bex) apply (clarsimp simp: in_getCTE_cte_wp_at') apply (simp add: cte_wp_at_ctes_of) apply (simp add: returnOk_def return_def)

  \<comment> \<open>last goal\<close> 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>s. valid_objs' s \<and> valid_mdb' s) (UNIV \<inter> \<lbrace>slot = ptr_val \<acute>slot\<rbrace>) [] (ensureNoChildren slot) (Call ensureNoChildren_'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_') (?Q226 slota) (?Q'226 slota) [SKIP] (doE cte <- liftE (getCTE slot);
whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE)
odE) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
\<acute>ret__unsigned_long :== CALL isMDBParentOf_'proc(slota,\<acute>next);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI
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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q226 slota s \<and> s' \<in> ?Q'226 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_') (?Q226 slota) (?Q'226 slota) [SKIP] (do cte <- getCTE slot;
whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
\<acute>ret__unsigned_long :== CALL isMDBParentOf_'proc(slota,\<acute>next);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI
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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q226 slota s \<and> s' \<in> ?Q'226 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_') (?P234 slota cte) (?P'234 slota cte) [SKIP] (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE)) (Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
\<acute>ret__unsigned_long :== CALL isMDBParentOf_'proc(slota,\<acute>next);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI
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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ?P234 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'234 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_') (?A236 slota cte) (?C'236 slota cte) [SKIP] (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE)) (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])));;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
\<acute>ret__unsigned_long :== CALL isMDBParentOf_'proc(slota,\<acute>next);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI
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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> (?A236 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'236 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. (valid_objs' \<sigma> \<and> valid_mdb' \<sigma> \<and> ctes_of \<sigma> (ptr_val slota) = Some cte) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])));;
(IF \<acute>ret__unsigned \<noteq> 0 THEN
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slota} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr \<acute>ret__unsigned;;
\<acute>ret__unsigned_long :== CALL isMDBParentOf_'proc(slota,\<acute>next);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) {},{s. \<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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. (valid_objs' \<sigma> \<and> valid_mdb' \<sigma> \<and> 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 = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> s \<Turnstile>\<^sub>c slota \<and> (\<forall>t. ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) \<longrightarrow> (\<exists>ctea cte_a. cslift s slota = Some cte_a \<and> ccte_relation ctea cte_a \<and> (\<exists>cteb cte_b. cslift s (cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> (\<forall>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb) \<longrightarrow> (from_bool (isMDBParentOf ctea cteb) \<noteq> 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) (current_syscall_error_' (globals s)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) (s\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_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_RevokeFirst) (current_syscall_error_' (globals s)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) (s\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))), next_' := cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))), 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_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))), next_' := cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))), ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))))))))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals s))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := 0, 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_' := 0, 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some cte; (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))\<rbrakk> \<Longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> x \<Turnstile>\<^sub>c slota \<and> (\<exists>ctea cte_a. cslift x slota = Some cte_a \<and> ccte_relation ctea cte_a \<and> (\<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb)) \<longrightarrow> (isMDBParentOf ctea cteb \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) (x\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))), next_' := cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))), ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))))))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext (cteMDBNode cte) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext (cteMDBNode cte)));
whenE (isMDBParentOf cte next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_' := 0, 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) \<noteq> 0 \<longrightarrow> x \<Turnstile>\<^sub>c slota \<and> (\<exists>ctea. ccte_relation ctea cte' \<and> (\<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb)) \<longrightarrow> (isMDBParentOf ctea cteb \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext_CL (cteMDBNode_CL y) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext_CL (cteMDBNode_CL y)));
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))))) (x\<lparr>ret__unsigned_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext_CL (cteMDBNode_CL y) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext_CL (cteMDBNode_CL y)));
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_' := mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))), next_' := cte_Ptr (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C'']))))), ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))))))) \<and> (mdbNext_CL (mdb_node_lift (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_Ptr &(slota\<rightarrow>[''cteMDBNode_C''])))) = 0 \<longrightarrow> (\<exists>xa\<in>fst (whenE (mdbNext_CL (cteMDBNode_CL y) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext_CL (cteMDBNode_CL y)));
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_' := 0, 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (mdbNext_CL (cteMDBNode_CL y) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ccte_relation ctea cte' \<and> (\<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb)) \<longrightarrow> (isMDBParentOf ctea cteb \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext_CL (cteMDBNode_CL y) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext_CL (cteMDBNode_CL y)));
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<sigma>). (\<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (whenE (mdbNext_CL (cteMDBNode_CL y) \<noteq> nullPointer) (doE next <- liftE (getCTE (mdbNext_CL (cteMDBNode_CL y)));
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<sigma>). (\<sigma>', x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) rv (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))))))) \<and> (mdbNext_CL (cteMDBNode_CL y) = 0 \<longrightarrow> (\<exists>xa\<in>fst (whenE False (doE next <- liftE (getCTE 0);
whenE (isMDBParentOf (cte_to_H y) next) (throwError Fault_H.syscall_error.RevokeFirst)
odE) \<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_' := 0, 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> (mdbNext_CL (cteMDBNode_CL y) \<noteq> 0 \<longrightarrow> (\<exists>ctea. ccte_relation ctea cte' \<and> (\<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb)) \<longrightarrow> (isMDBParentOf ctea cteb \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>)))))))) \<and> (mdbNext_CL (cteMDBNode_CL y) = 0 \<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_' := 0, 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; mdbNext_CL (cteMDBNode_CL y) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>ctea. ccte_relation ctea cte' \<and> (\<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> ccte_relation cteb cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cteCap ctea)) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf ctea cteb)) \<longrightarrow> (isMDBParentOf ctea cteb \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf ctea cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; mdbNext_CL (cteMDBNode_CL y) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> Some cteb = map_option cte_to_H (cte_lift cte_b) \<and> c_valid_cte cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) cteb)) \<longrightarrow> (isMDBParentOf (cte_to_H y) cteb \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; mdbNext_CL (cteMDBNode_CL y) \<noteq> 0; cte_wp_at' (\<lambda>_. True) (mdbNext_CL (cteMDBNode_CL y)) \<sigma>\<rbrakk> \<Longrightarrow> \<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> Some cteb = map_option cte_to_H (cte_lift cte_b) \<and> c_valid_cte cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) cteb)) \<longrightarrow> (isMDBParentOf (cte_to_H y) cteb \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some cte\<rbrakk> \<Longrightarrow> \<exists>cteb cte_b. cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte_b \<and> Some cteb = map_option cte_to_H (cte_lift cte_b) \<and> c_valid_cte cte_b \<and> capAligned (cteCap cteb) \<and> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) cteb)) \<longrightarrow> (isMDBParentOf (cte_to_H y) cteb \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) cteb) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> capAligned (cap_to_H (cap_CL ya)) \<and> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> capAligned (cap_to_H (cap_CL ya))
 2. \<And>slota \<sigma> x t cte' y cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; valid_cap' (cap_to_H (cap_CL ya)) \<sigma>\<rbrakk> \<Longrightarrow> capAligned (cap_to_H (cap_CL ya))
 2. \<And>slota \<sigma> x t cte' y cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> Ex (valid_cap' (cap_to_H (cap_CL y))) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> Ex (valid_cap' (cap_to_H (cap_CL y)))
 2. \<And>slota \<sigma> x t cte' y cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; valid_cap' (cap_to_H (cap_CL y)) \<sigma>\<rbrakk> \<Longrightarrow> Ex (valid_cap' (cap_to_H (cap_CL y)))
 2. \<And>slota \<sigma> x t cte' y cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a\<rbrakk> \<Longrightarrow> (\<exists>t. ret__unsigned_long_' t = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))) \<longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> (isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> isMDBParentOf (cte_to_H y) (cte_to_H ya) \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya\<in>fst (getCTE (mdbNext_CL (cteMDBNode_CL y)) \<sigma>). \<exists>xa\<in>fst (case ya of (next, x) \<Rightarrow> (if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) x). 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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya yb. (ya, yb) \<in> fst (getCTE (mdbNext_CL (cteMDBNode_CL y)) \<sigma>) \<and> (\<exists>xa yc. (xa, yc) \<in> fst ((if isMDBParentOf (cte_to_H y) ya then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) yb) \<and> (yc, x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) xa (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya. cte_wp_at' ((=) ya) (mdbNext_CL (cteMDBNode_CL y)) \<sigma> \<and> (\<exists>xa yb. (xa, yb) \<in> fst ((if isMDBParentOf (cte_to_H y) ya then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) \<sigma>) \<and> (yb, x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) xa (liftxf errstate id undefined ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> EXCEPTION_SYSCALL_ERROR \<noteq> EXCEPTION_NONE \<and> syscall_error_rel Fault_H.syscall_error.RevokeFirst (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_RevokeFirst) (current_syscall_error_' (globals x)))) (next_'_update (\<lambda>_. cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y)\<rparr>))))
 2. \<And>slota \<sigma> x t cte' y cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = SCAST(32 signed \<rightarrow> 32) true; isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> syscall_error_to_H (type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_RevokeFirst) (current_syscall_error_' (globals x))) (lookup_fault_lift (current_lookup_fault_' (globals x))) = Some Fault_H.syscall_error.RevokeFirst
 2. \<And>slota \<sigma> x t cte' y cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya))\<rbrakk> \<Longrightarrow> from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0 \<longrightarrow> (\<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; from_bool (isMDBParentOf (cte_to_H y) (cte_to_H ya)) = 0\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; \<not> isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do next <- getCTE (mdbNext_CL (cteMDBNode_CL y));
if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()
od) \<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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; \<not> isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya\<in>fst (getCTE (mdbNext_CL (cteMDBNode_CL y)) \<sigma>). \<exists>xa\<in>fst (case ya of (next, x) \<Rightarrow> (if isMDBParentOf (cte_to_H y) next then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) x). 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_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; \<not> isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya yb. (ya, yb) \<in> fst (getCTE (mdbNext_CL (cteMDBNode_CL y)) \<sigma>) \<and> (\<exists>xa yc. (xa, yc) \<in> fst ((if isMDBParentOf (cte_to_H y) ya then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) yb) \<and> (yc, x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) xa (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; \<not> isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>ya. cte_wp_at' ((=) ya) (mdbNext_CL (cteMDBNode_CL y)) \<sigma> \<and> (\<exists>xa yb. (xa, yb) \<in> fst ((if isMDBParentOf (cte_to_H y) ya then \<lambda>s. ({(Inl Fault_H.syscall_error.RevokeFirst, s)}, False) else returnOk ()) \<sigma>) \<and> (yb, x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) xa (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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 cte'a ya ta. \<lbrakk>slot = ptr_val slota; valid_objs' \<sigma>; valid_mdb' \<sigma>; ctes_of \<sigma> (ptr_val slota) = Some (cte_to_H y); (\<sigma>, x) \<in> rf_sr; ret__unsigned_' t = mdbNext_CL (cteMDBNode_CL y); cslift x slota = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ctes_of \<sigma> (mdbNext_CL (cteMDBNode_CL y)) = Some (cte_to_H ya); cslift x (cte_Ptr (mdbNext_CL (cteMDBNode_CL y))) = Some cte'a; cte_lift cte'a = Some ya; c_valid_cte cte'a; ret__unsigned_long_' ta = 0; \<not> isMDBParentOf (cte_to_H y) (cte_to_H ya)\<rbrakk> \<Longrightarrow> \<exists>xa ya. (xa, ya) \<in> fst (returnOk () \<sigma>) \<and> (ya, x) \<in> rf_sr \<and> (syscall_error_rel \<currency> dc) xa (liftxf errstate id undefined ret__unsigned_long_' (x\<lparr>ret__unsigned_' := mdbNext_CL (cteMDBNode_CL y), next_' := cte_Ptr (mdbNext_CL (cteMDBNode_CL y)), 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' s \<and> valid_mdb' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>cte. ctes_of s slot = Some cte \<longrightarrow> ((\<lambda>s. valid_objs' s \<and> valid_mdb' s \<and> 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; valid_objs' s; valid_mdb' s; ctes_of s (ptr_val slota) = Some cte\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (ptr_val slota) s proof (prove)
goal:
No subgoals!