theory Retype_DP

lemma reset_untyped_cap_not_pending_cap[wp]:
  "\<lbrace>\<lambda>s. \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
  reset_untyped_cap cref
  \<lbrace>\<lambda>rv s.  (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>" apply (simp add: reset_untyped_cap_def) apply (wp whenE_wp) apply (rule_tac P = " \<not> is_pending_cap cap" in hoare_gen_asmEx) apply (wp mapME_x_inv_wp set_cap_opt_cap)+ apply simp apply wp+ apply (clarsimp simp: detype_no_pending) apply (cases cref) apply (clarsimp simp: detype_def opt_cap_def slots_of_def object_slots_def
                 split: option.split_asm if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> is_pending_cap (the (opt_cap cref s))\<rbrace> reset_untyped_cap cref \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s)))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 5. \<And>s. \<not> is_pending_cap (the (opt_cap cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap y x. \<lbrakk>available_range cap \<noteq> cap_objects cap; \<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 (\<not> is_pending_cap cap)\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s)))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 5. \<And>s. \<not> is_pending_cap (the (opt_cap cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>cap y x xa s. \<lbrakk>available_range cap \<noteq> cap_objects cap; \<not> is_pending_cap cap; (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrakk> \<Longrightarrow> ((\<exists>capa. Some (set_available_range cap xa) = Some capa) \<longrightarrow> \<not> is_pending_cap (the (Some (set_available_range cap xa)))) \<and> ((\<exists>capa. Some (set_available_range cap xa) = Some capa) \<longrightarrow> \<not> is_pending_cap (the (Some (set_available_range cap xa)))) \<and> True
 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. (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))) and K (\<not> is_pending_cap cap)\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 4. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s)))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 5. \<And>s. \<not> is_pending_cap (the (opt_cap cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<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. (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))) and K (\<not> is_pending_cap cap)\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 2. \<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 s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 3. \<lbrace>?Q\<rbrace> liftE (get_cap cref) \<lbrace>\<lambda>cap. if available_range cap \<noteq> cap_objects cap then ?Q3 cap else (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s)))\<rbrace>, \<lbrace>\<lambda>rv s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))\<rbrace>
 4. \<And>s. \<not> is_pending_cap (the (opt_cap cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> is_pending_cap (the (opt_cap cref s)) \<Longrightarrow> opt_cap cref s \<noteq> None \<longrightarrow> (if available_range (the (opt_cap cref s)) \<noteq> cap_objects (the (opt_cap cref s)) then \<lambda>sa. \<forall>x\<in>{xs. (\<forall>S\<in>set xs. S \<subseteq> cap_objects (the (opt_cap cref s)) \<and> available_range (the (opt_cap cref s)) \<subset> S) \<and> xs \<noteq> [] \<and> last xs = cap_objects (the (opt_cap cref s))}. ((\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s))) and K (\<not> is_pending_cap (the (opt_cap cref s)))) (detype (cap_objects (the (opt_cap cref s))) sa) else (\<lambda>s. (\<exists>cap. opt_cap cref s = Some cap) \<longrightarrow> \<not> is_pending_cap (the (opt_cap cref s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s y x cap. \<lbrakk>\<not> is_pending_cap y; 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; opt_cap cref (detype (cap_objects y) s) = Some cap; is_pending_cap cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y x cap a b. \<lbrakk>\<not> is_pending_cap y; 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; opt_cap cref (detype (cap_objects y) s) = Some cap; is_pending_cap cap; cref = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!