theory Retype_DP

lemma invoke_untyped_no_pending[wp]:
  "\<lbrace>no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))\<rbrace>
  invoke_untyped (Retype ref a b c d e)
  \<lbrace>\<lambda>rv. no_pending\<rbrace>" apply (simp add: invoke_untyped_def create_cap_def) apply (wpsimp wp: mapM_x_wp' set_cap_no_pending_asm_in_pre get_cap_wp
              simp: update_available_range_def) apply (wp (once) hoare_drop_imps) apply (wpsimp split_del: if_split)+ apply (rule_tac Q' = "\<lambda>r s. no_pending s \<and> ((\<exists>y. opt_cap ref s = Some y) \<longrightarrow>
                        \<not> is_pending_cap (the (opt_cap ref s)))" in hoare_post_imp_R) apply (wp reset_untyped_cap_no_pending) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))\<rbrace> invoke_untyped (Retype ref a b c d e) \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))\<rbrace> doE y <- unlessE d (reset_untyped_cap ref);
liftE (do untyped_cap <- get_cap ref;
new_obj_refs <- generate_object_ids e a (available_range untyped_cap);
y <- update_available_range (available_range untyped_cap) (map pick new_obj_refs) ref untyped_cap;
y <- retype_region b a new_obj_refs;
mapM_x (\<lambda>(dest_slot, obj_refs). do old_cap <- get_cap dest_slot;
y <- assert (old_cap = NullCap);
y <- set_cap dest_slot (default_cap a obj_refs b (untyped_is_device untyped_cap));
set_parent dest_slot ref
od) (zip c new_obj_refs)
od)
odE \<lbrace>\<lambda>rv. no_pending\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>untyped_cap. \<lbrace>?B5 () untyped_cap\<rbrace> generate_object_ids e a (available_range untyped_cap) \<lbrace>\<lambda>a b. (\<exists>x. x \<subseteq> available_range untyped_cap - pick ` set a) \<longrightarrow> no_pending b \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap untyped_cap)\<rbrace>
 2. \<And>y. \<lbrace>?B3 y\<rbrace> get_cap ref \<lbrace>?B5 y\<rbrace>
 3. \<lbrace>?Q1\<rbrace> unlessE d (reset_untyped_cap ref) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 4. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>untyped_cap. \<lbrace>?B5 () untyped_cap\<rbrace> generate_object_ids e a (available_range untyped_cap) \<lbrace>\<lambda>rv s. no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap untyped_cap)\<rbrace>
 2. \<And>y. \<lbrace>?B3 y\<rbrace> get_cap ref \<lbrace>?B5 y\<rbrace>
 3. \<lbrace>?Q1\<rbrace> unlessE d (reset_untyped_cap ref) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. no_pending\<rbrace>
 4. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<not> d \<Longrightarrow> \<lbrace>?P'52\<rbrace> reset_untyped_cap ref \<lbrace>\<lambda>y s. (\<exists>y. opt_cap ref s = Some y) \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))\<rbrace>, -
 2. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> (if d then \<lambda>s. opt_cap ref s \<noteq> None \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s))) else (\<lambda>s. no_pending s \<and> ?P'52 s)) s proof (prove)
goal (3 subgoals):
 1. \<not> d \<Longrightarrow> \<lbrace>?P'52\<rbrace> reset_untyped_cap ref \<lbrace>\<lambda>r s. no_pending s \<and> ((\<exists>y. opt_cap ref s = Some y) \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))\<rbrace>, -
 2. \<And>rv s. \<lbrakk>\<not> d; no_pending s \<and> ((\<exists>y. opt_cap ref s = Some y) \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap ref s = Some y) \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))
 3. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> (if d then \<lambda>s. opt_cap ref s \<noteq> None \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s))) else (\<lambda>s. no_pending s \<and> ?P'52 s)) s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>\<not> d; no_pending s \<and> ((\<exists>y. opt_cap ref s = Some y) \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))\<rbrakk> \<Longrightarrow> (\<exists>y. opt_cap ref s = Some y) \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s)))
 2. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> (if d then \<lambda>s. opt_cap ref s \<noteq> None \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s))) else (\<lambda>s. no_pending s \<and> no_pending s \<and> \<not> is_pending_cap (the (opt_cap ref s)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (no_pending and (\<lambda>s. \<not> is_pending_cap (the (opt_cap ref s)))) s \<Longrightarrow> (if d then \<lambda>s. opt_cap ref s \<noteq> None \<longrightarrow> no_pending s \<and> (snd ref = tcb_pending_op_slot \<longrightarrow> \<not> is_pending_cap (the (opt_cap ref s))) else (\<lambda>s. no_pending s \<and> no_pending s \<and> \<not> is_pending_cap (the (opt_cap ref s)))) s proof (prove)
goal:
No subgoals!