theory CSpace_AI

lemma set_untyped_cap_as_full_valid_reply_masters:
  "\<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. valid_reply_masters s \<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def) apply (intro conjI impI) apply wp apply (clarsimp simp: cte_wp_at_caps_of_state free_index_update_def split:cap.splits) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrakk> \<Longrightarrow> (valid_reply_masters and cte_wp_at (\<lambda>_. True) src and (\<lambda>s. \<forall>x. (\<exists>rights. max_free_index_update src_cap = ReplyCap x True rights) \<longrightarrow> fst src = x \<and> snd src = tcb_cnode_index 2)) s
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; valid_reply_masters s \<and> cte_wp_at ((=) src_cap) src s\<rbrakk> \<Longrightarrow> valid_reply_masters s proof (prove)
goal:
No subgoals!