theory Ipc_DR

lemma cap_insert_weak_cte_wp_at_not_null:
assumes "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
shows "\<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot :: det_state \<Rightarrow> bool\<rbrace> cap_insert cap' src dest
  \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace>" apply (case_tac "slot = dest") apply (clarsimp simp:cap_insert_def) apply wp apply (rule hoare_pre_cont) apply (rule hoare_pre_cont) apply (wp get_cap_wp)+ apply (clarsimp simp:cte_wp_at_caps_of_state) apply (wp cap_insert_weak_cte_wp_at2) apply (clarsimp simp:assms) apply (clarsimp simp:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot = dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace>
 2. slot \<noteq> dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot = dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) dest\<rbrace> do src_cap <- CSpaceAcc_A.get_cap src;
old_cap <- CSpaceAcc_A.get_cap dest;
y <- assert (old_cap = cap.NullCap);
y <- CSpace_A.set_untyped_cap_as_full src_cap cap' src;
y <- CSpaceAcc_A.set_cap cap' dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap' (is_cap_revocable cap' src_cap) then Some src else cdt src));
y <- cap_insert_ext (should_be_parent_of src_cap (is_original src) cap' (is_cap_revocable cap' src_cap)) src dest src_p dest_p;
set_original dest (is_cap_revocable cap' src_cap)
od \<lbrace>\<lambda>r. cte_wp_at P dest\<rbrace>
 2. slot \<noteq> dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>src_cap x y ya yb is_original src_p dest_p yc. slot = dest \<Longrightarrow> \<lbrace>?B13 src_cap x y ya yb is_original src_p dest_p yc\<rbrace> cap_insert_ext (should_be_parent_of src_cap (is_original src) cap' (is_cap_revocable cap' src_cap)) src dest src_p dest_p \<lbrace>\<lambda>yd s. cte_wp_at P dest (s\<lparr>is_original_cap := (is_original_cap s)(dest := is_cap_revocable cap' src_cap)\<rparr>)\<rbrace>
 2. \<And>src_cap x y ya yb is_original src_p dest_p. slot = dest \<Longrightarrow> \<lbrace>?B12 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap' (is_cap_revocable cap' src_cap) then Some src else cdt src)) \<lbrace>?B13 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. slot = dest \<Longrightarrow> \<lbrace>?B11 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s dest) \<lbrace>?B12 src_cap x y ya yb is_original src_p\<rbrace>
 4. \<And>src_cap x y ya yb is_original. slot = dest \<Longrightarrow> \<lbrace>?B10 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s src) \<lbrace>?B11 src_cap x y ya yb is_original\<rbrace>
 5. \<And>src_cap x y ya yb. slot = dest \<Longrightarrow> \<lbrace>?B9 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B10 src_cap x y ya yb\<rbrace>
 6. \<And>src_cap x y ya. slot = dest \<Longrightarrow> \<lbrace>?B8 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' dest \<lbrace>?B9 src_cap x y ya\<rbrace>
 7. \<And>src_cap x y. slot = dest \<Longrightarrow> \<lbrace>?B7 src_cap x y\<rbrace> CSpace_A.set_untyped_cap_as_full src_cap cap' src \<lbrace>?B8 src_cap x y\<rbrace>
 8. \<And>src_cap x. slot = dest \<Longrightarrow> \<lbrace>?B6 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B7 src_cap x\<rbrace>
 9. \<And>src_cap. slot = dest \<Longrightarrow> \<lbrace>?B5 src_cap\<rbrace> CSpaceAcc_A.get_cap dest \<lbrace>?B6 src_cap\<rbrace>
 10. slot = dest \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>?B5\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>src_cap x y ya yb is_original src_p dest_p. slot = dest \<Longrightarrow> \<lbrace>?B12 src_cap x y ya yb is_original src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap' (is_cap_revocable cap' src_cap) then Some src else cdt src)) \<lbrace>\<lambda>yc _. False\<rbrace>
 2. \<And>src_cap x y ya yb is_original src_p. slot = dest \<Longrightarrow> \<lbrace>?B11 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s dest) \<lbrace>?B12 src_cap x y ya yb is_original src_p\<rbrace>
 3. \<And>src_cap x y ya yb is_original. slot = dest \<Longrightarrow> \<lbrace>?B10 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s src) \<lbrace>?B11 src_cap x y ya yb is_original\<rbrace>
 4. \<And>src_cap x y ya yb. slot = dest \<Longrightarrow> \<lbrace>?B9 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B10 src_cap x y ya yb\<rbrace>
 5. \<And>src_cap x y ya. slot = dest \<Longrightarrow> \<lbrace>?B8 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' dest \<lbrace>?B9 src_cap x y ya\<rbrace>
 6. \<And>src_cap x y. slot = dest \<Longrightarrow> \<lbrace>?B7 src_cap x y\<rbrace> CSpace_A.set_untyped_cap_as_full src_cap cap' src \<lbrace>?B8 src_cap x y\<rbrace>
 7. \<And>src_cap x. slot = dest \<Longrightarrow> \<lbrace>?B6 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B7 src_cap x\<rbrace>
 8. \<And>src_cap. slot = dest \<Longrightarrow> \<lbrace>?B5 src_cap\<rbrace> CSpaceAcc_A.get_cap dest \<lbrace>?B6 src_cap\<rbrace>
 9. slot = dest \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>?B5\<rbrace>
 10. \<And>s. \<lbrakk>slot = dest; cte_wp_at (P and (\<noteq>) cap.NullCap) dest s\<rbrakk> \<Longrightarrow> ?Q4 s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>src_cap x y ya yb is_original src_p. slot = dest \<Longrightarrow> \<lbrace>?B11 src_cap x y ya yb is_original src_p\<rbrace> gets (\<lambda>s. cdt s dest) \<lbrace>\<lambda>dest_p _. False\<rbrace>
 2. \<And>src_cap x y ya yb is_original. slot = dest \<Longrightarrow> \<lbrace>?B10 src_cap x y ya yb is_original\<rbrace> gets (\<lambda>s. cdt s src) \<lbrace>?B11 src_cap x y ya yb is_original\<rbrace>
 3. \<And>src_cap x y ya yb. slot = dest \<Longrightarrow> \<lbrace>?B9 src_cap x y ya yb\<rbrace> gets is_original_cap \<lbrace>?B10 src_cap x y ya yb\<rbrace>
 4. \<And>src_cap x y ya. slot = dest \<Longrightarrow> \<lbrace>?B8 src_cap x y ya\<rbrace> CSpaceAcc_A.set_cap cap' dest \<lbrace>?B9 src_cap x y ya\<rbrace>
 5. \<And>src_cap x y. slot = dest \<Longrightarrow> \<lbrace>?B7 src_cap x y\<rbrace> CSpace_A.set_untyped_cap_as_full src_cap cap' src \<lbrace>?B8 src_cap x y\<rbrace>
 6. \<And>src_cap x. slot = dest \<Longrightarrow> \<lbrace>?B6 src_cap x\<rbrace> assert (x = cap.NullCap) \<lbrace>?B7 src_cap x\<rbrace>
 7. \<And>src_cap. slot = dest \<Longrightarrow> \<lbrace>?B5 src_cap\<rbrace> CSpaceAcc_A.get_cap dest \<lbrace>?B6 src_cap\<rbrace>
 8. slot = dest \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpaceAcc_A.get_cap src \<lbrace>?B5\<rbrace>
 9. \<And>s. \<lbrakk>slot = dest; cte_wp_at (P and (\<noteq>) cap.NullCap) dest s\<rbrakk> \<Longrightarrow> ?Q4 s
 10. slot \<noteq> dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slot = dest; cte_wp_at (P and (\<noteq>) cap.NullCap) dest s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) src s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap = cap.NullCap \<longrightarrow> False)
 2. slot \<noteq> dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot \<noteq> dest \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> cap_insert cap' src dest \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>slot \<noteq> dest; P c\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_untyped_cap c
 2. \<And>s. \<lbrakk>slot \<noteq> dest; cte_wp_at (P and (\<noteq>) cap.NullCap) slot s\<rbrakk> \<Longrightarrow> if slot = dest then P cap' else cte_wp_at P slot s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot \<noteq> dest; cte_wp_at (P and (\<noteq>) cap.NullCap) slot s\<rbrakk> \<Longrightarrow> if slot = dest then P cap' else cte_wp_at P slot s proof (prove)
goal:
No subgoals!