theory CNode_AC

lemma set_untyped_cap_as_full_is_transferable':
  "\<lbrace>\<lambda>s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3) \<and>
        Some src_cap = (caps_of_state s slot)\<rbrace>
   set_untyped_cap_as_full src_cap new_cap slot
   \<lbrace>\<lambda>_ s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3)\<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def) apply safe apply (wp,fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3) \<and> Some src_cap = caps_of_state s slot\<rbrace> set_untyped_cap_as_full src_cap new_cap slot \<lbrace>\<lambda>_ s. is_transferable (((caps_of_state s)(slot2 \<mapsto> new_cap)) slot3)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap new_cap \<and> obj_ref_of src_cap = obj_ref_of new_cap \<and> cap_bits_untyped src_cap = cap_bits_untyped new_cap \<longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> set_cap (max_free_index_update src_cap) slot \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of new_cap \<longrightarrow> is_untyped_cap new_cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped new_cap) \<longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> return () \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap new_cap; obj_ref_of src_cap = obj_ref_of new_cap; cap_bits_untyped src_cap = cap_bits_untyped new_cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> set_cap (max_free_index_update src_cap) slot \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>
 2. obj_ref_of src_cap \<noteq> obj_ref_of new_cap \<Longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> return () \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>
 3. \<not> is_untyped_cap new_cap \<Longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> return () \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>
 4. \<not> is_untyped_cap src_cap \<Longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> return () \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace>
 5. cap_bits_untyped src_cap \<noteq> cap_bits_untyped new_cap \<Longrightarrow> \<lbrace>\<lambda>s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap \<and> Some src_cap = caps_of_state s slot) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s \<and> Some src_cap = caps_of_state s slot)\<rbrace> return () \<lbrace>\<lambda>_ s. (slot3 = slot2 \<longrightarrow> is_transferable_cap new_cap) \<and> (slot3 \<noteq> slot2 \<longrightarrow> is_transferable_in slot3 s)\<rbrace> proof (prove)
goal:
No subgoals!