theory Retype_DP

lemma reset_untyped_cap_no_pending[wp]:
  "\<lbrace>no_pending \<rbrace> reset_untyped_cap cref \<lbrace>\<lambda>rv. no_pending\<rbrace>" apply (simp add: reset_untyped_cap_def) apply (wp whenE_wp) apply (rule_tac P = "snd cref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap" in hoare_gen_asmEx) apply (wp mapME_x_inv_wp | simp)+ apply (clarsimp simp: detype_no_pending) apply (cases cref, clarsimp simp: no_pending_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending\<rbrace> reset_untyped_cap cref \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending\<rbrace> doE cap <- liftE (get_cap cref);
whenE (available_range cap \<noteq> cap_objects cap) (doE y <- liftE (modify (detype (cap_objects cap)));
liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) >>=E mapME_x (\<lambda>r. doE y <- liftE (set_cap cref (set_available_range cap r));
returnOk () \<sqinter> throw
odE)
odE)
odE \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cap y x. available_range cap \<noteq> cap_objects cap \<Longrightarrow> \<lbrace>?B5 cap y x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap cref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>rv. no_pending\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 2. \<And>cap y. available_range cap \<noteq> cap_objects cap \<Longrightarrow> \<lbrace>?B4 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>?B5 cap y\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 3. \<And>cap. available_range cap \<noteq> cap_objects cap \<Longrightarrow> \<lbrace>?Q3 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B4 cap\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else no_pending\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 5. \<And>s. no_pending s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap y x. \<lbrakk>available_range cap \<noteq> cap_objects cap; snd cref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'6 cap y x\<rbrace> mapME_x (\<lambda>r. doE y <- liftE (set_cap cref (set_available_range cap r));
returnOk () \<sqinter> throw
odE) x \<lbrace>\<lambda>rv. no_pending\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 2. \<And>cap y. available_range cap \<noteq> cap_objects cap \<Longrightarrow> \<lbrace>?B4 cap y\<rbrace> liftE (select {xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects cap \<and> available_range cap \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects cap}) \<lbrace>\<lambda>x. ?P'6 cap y x and K (snd cref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap cap)\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 3. \<And>cap. available_range cap \<noteq> cap_objects cap \<Longrightarrow> \<lbrace>?Q3 cap\<rbrace> liftE (modify (detype (cap_objects cap))) \<lbrace>?B4 cap\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else no_pending\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 5. \<And>s. no_pending s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_pending s \<Longrightarrow> available_range (the (opt_cap cref s)) \<noteq> cap_objects (the (opt_cap cref s)) \<longrightarrow> (\<exists>y. opt_cap cref s = Some y) \<longrightarrow> (\<exists>x. (\<forall>S\<in>set x. S \<subseteq> cap_objects (the (opt_cap cref s)) \<and> available_range (the (opt_cap cref s)) \<subset> S) \<and> x \<noteq> [] \<and> last x = cap_objects (the (opt_cap cref s))) \<longrightarrow> no_pending (detype (cap_objects (the (opt_cap cref s))) s) \<and> (snd cref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))) proof (prove)
goal (1 subgoal):
 1. \<And>s y x. \<lbrakk>no_pending s; available_range y \<noteq> cap_objects y; opt_cap cref s = Some y; \<forall>S\<in>set x. S \<subseteq> cap_objects y \<and> available_range y \<subset> S; x \<noteq> []; last x = cap_objects y; snd cref = tcb_pending_op_slot; is_pending_cap y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!