theory Ipc_DR

lemma ipc_buffer_wp_at_cap_insert[wp]:
  "\<lbrace>ipc_buffer_wp_at buf t :: det_state \<Rightarrow> bool \<rbrace> cap_insert cap' (slot_ptr, slot_idx) a \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>" apply (simp add:cap_insert_def set_untyped_cap_as_full_def) apply (wp|simp split del:if_split)+ apply (rule_tac Q = "\<lambda>r. ipc_buffer_wp_at buf t" in hoare_strengthen_post) apply wp apply (clarsimp simp:ipc_buffer_wp_at_def) apply (wp get_cap_inv hoare_drop_imp)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> cap_insert cap' (slot_ptr, slot_idx) a \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> do src_cap <- CSpaceAcc_A.get_cap (slot_ptr, slot_idx);
old_cap <- CSpaceAcc_A.get_cap a;
y <- assert (old_cap = cap.NullCap);
y <- if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap' \<and> obj_ref_of src_cap = obj_ref_of cap' \<and> cap_bits_untyped src_cap = cap_bits_untyped cap' then CSpaceAcc_A.set_cap (max_free_index_update src_cap) (slot_ptr, slot_idx) else return ();
y <- CSpaceAcc_A.set_cap cap' a;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s (slot_ptr, slot_idx));
dest_p <- gets (\<lambda>s. cdt s a);
y <- update_cdt (\<lambda>cdt. cdt(a := if should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap) then Some (slot_ptr, slot_idx) else cdt (slot_ptr, slot_idx)));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap)) (slot_ptr, slot_idx) a src_p dest_p;
set_original a (is_cap_revocable cap' src_cap)
od \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>src_cap x is_original src_p dest_p. \<lbrace>?B9 src_cap x () () () is_original src_p dest_p ()\<rbrace> cap_insert_ext (should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap)) (slot_ptr, slot_idx) a src_p dest_p \<lbrace>\<lambda>yd s. ipc_buffer_wp_at buf t (s\<lparr>is_original_cap := (is_original_cap s)(a := is_cap_revocable cap' src_cap)\<rparr>)\<rbrace>
 2. \<And>src_cap x y ya yb is_original src_p dest_p. \<lbrace>?B8 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(a := if should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap) then Some (slot_ptr, slot_idx) else cdt (slot_ptr, slot_idx))) \<lbrace>?B9 src_cap x y ya yb is_original src_p dest_p\<rbrace>
 3. \<And>src_cap x y ya yb is_original src_p. \<lbrace>?B7 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B8 src_cap x y ya yb is_original src_p\<rbrace>
 4. \<And>src_cap x y ya yb is_original. \<lbrace>?B6 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s (slot_ptr, slot_idx)) \<lbrace>?B7 src_cap x y ya yb is_original\<rbrace>
 5. \<And>src_cap x y ya yb. \<lbrace>?B5 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B6 src_cap x y ya yb\<rbrace>
 6. \<And>src_cap x y ya. \<lbrace>?B4 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>?B5 src_cap x y ya\<rbrace>
 7. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap' \<and> obj_ref_of src_cap = obj_ref_of cap' \<and> cap_bits_untyped src_cap = cap_bits_untyped cap' then CSpaceAcc_A.set_cap (max_free_index_update src_cap) (slot_ptr, slot_idx) else return () \<lbrace>?B4 src_cap x y\<rbrace>
 8. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 9. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> CSpaceAcc_A.get_cap a \<lbrace>?B2 src_cap\<rbrace>
 10. \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap (slot_ptr, slot_idx) \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>src_cap x is_original src_p dest_p. \<lbrace>?B9 src_cap x () () () is_original src_p dest_p ()\<rbrace> cap_insert_ext (should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap)) (slot_ptr, slot_idx) a src_p dest_p \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>src_cap x is_original src_p dest_p rv s. ipc_buffer_wp_at buf t s \<Longrightarrow> ipc_buffer_wp_at buf t (s\<lparr>is_original_cap := (is_original_cap s)(a := is_cap_revocable cap' src_cap)\<rparr>)
 3. \<And>src_cap x y ya yb is_original src_p dest_p. \<lbrace>?B8 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(a := if should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap) then Some (slot_ptr, slot_idx) else cdt (slot_ptr, slot_idx))) \<lbrace>?B9 src_cap x y ya yb is_original src_p dest_p\<rbrace>
 4. \<And>src_cap x y ya yb is_original src_p. \<lbrace>?B7 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B8 src_cap x y ya yb is_original src_p\<rbrace>
 5. \<And>src_cap x y ya yb is_original. \<lbrace>?B6 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s (slot_ptr, slot_idx)) \<lbrace>?B7 src_cap x y ya yb is_original\<rbrace>
 6. \<And>src_cap x y ya yb. \<lbrace>?B5 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B6 src_cap x y ya yb\<rbrace>
 7. \<And>src_cap x y ya. \<lbrace>?B4 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>?B5 src_cap x y ya\<rbrace>
 8. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap' \<and> obj_ref_of src_cap = obj_ref_of cap' \<and> cap_bits_untyped src_cap = cap_bits_untyped cap' then CSpaceAcc_A.set_cap (max_free_index_update src_cap) (slot_ptr, slot_idx) else return () \<lbrace>?B4 src_cap x y\<rbrace>
 9. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 10. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> CSpaceAcc_A.get_cap a \<lbrace>?B2 src_cap\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_cap x is_original src_p dest_p rv s. ipc_buffer_wp_at buf t s \<Longrightarrow> ipc_buffer_wp_at buf t (s\<lparr>is_original_cap := (is_original_cap s)(a := is_cap_revocable cap' src_cap)\<rparr>)
 2. \<And>src_cap x y ya yb is_original src_p dest_p. \<lbrace>?B8 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(a := if should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap) then Some (slot_ptr, slot_idx) else cdt (slot_ptr, slot_idx))) \<lbrace>\<lambda>a. ipc_buffer_wp_at buf t\<rbrace>
 3. \<And>src_cap x y ya yb is_original src_p. \<lbrace>?B7 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B8 src_cap x y ya yb is_original src_p\<rbrace>
 4. \<And>src_cap x y ya yb is_original. \<lbrace>?B6 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s (slot_ptr, slot_idx)) \<lbrace>?B7 src_cap x y ya yb is_original\<rbrace>
 5. \<And>src_cap x y ya yb. \<lbrace>?B5 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B6 src_cap x y ya yb\<rbrace>
 6. \<And>src_cap x y ya. \<lbrace>?B4 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>?B5 src_cap x y ya\<rbrace>
 7. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap' \<and> obj_ref_of src_cap = obj_ref_of cap' \<and> cap_bits_untyped src_cap = cap_bits_untyped cap' then CSpaceAcc_A.set_cap (max_free_index_update src_cap) (slot_ptr, slot_idx) else return () \<lbrace>?B4 src_cap x y\<rbrace>
 8. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 9. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> CSpaceAcc_A.get_cap a \<lbrace>?B2 src_cap\<rbrace>
 10. \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap (slot_ptr, slot_idx) \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>src_cap x y ya yb is_original src_p dest_p. \<lbrace>?B8 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(a := if should_be_parent_of src_cap (is_original (slot_ptr, slot_idx)) cap' (is_cap_revocable cap' src_cap) then Some (slot_ptr, slot_idx) else cdt (slot_ptr, slot_idx))) \<lbrace>\<lambda>a. ipc_buffer_wp_at buf t\<rbrace>
 2. \<And>src_cap x y ya yb is_original src_p. \<lbrace>?B7 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s a) \<lbrace>?B8 src_cap x y ya yb is_original src_p\<rbrace>
 3. \<And>src_cap x y ya yb is_original. \<lbrace>?B6 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s (slot_ptr, slot_idx)) \<lbrace>?B7 src_cap x y ya yb is_original\<rbrace>
 4. \<And>src_cap x y ya yb. \<lbrace>?B5 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B6 src_cap x y ya yb\<rbrace>
 5. \<And>src_cap x y ya. \<lbrace>?B4 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>?B5 src_cap x y ya\<rbrace>
 6. \<And>src_cap x y. \<lbrace>?B3 src_cap x y\<rbrace> if Structures_A.is_untyped_cap src_cap \<and> Structures_A.is_untyped_cap cap' \<and> obj_ref_of src_cap = obj_ref_of cap' \<and> cap_bits_untyped src_cap = cap_bits_untyped cap' then CSpaceAcc_A.set_cap (max_free_index_update src_cap) (slot_ptr, slot_idx) else return () \<lbrace>?B4 src_cap x y\<rbrace>
 7. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B3 src_cap x\<rbrace>
 8. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> CSpaceAcc_A.get_cap a \<lbrace>?B2 src_cap\<rbrace>
 9. \<lbrace>?Q\<rbrace> CSpaceAcc_A.get_cap (slot_ptr, slot_idx) \<lbrace>?B1\<rbrace>
 10. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ipc_buffer_wp_at buf t s \<Longrightarrow> ipc_buffer_wp_at buf t s \<and> ipc_buffer_wp_at buf t s proof (prove)
goal:
No subgoals!