theory TCB_DP

lemma insert_cap_sibling_current_thread_inv:
"\<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace>
  insert_cap_sibling cap src dest
 \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>" apply (clarsimp simp: insert_cap_sibling_def) apply (wp | wpc)+ apply (clarsimp) apply (intro hoare_conjI hoare_impI) apply (rule hoare_drop_imp) apply (wp) apply (rule hoare_drop_imp) apply (wp)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> insert_cap_sibling cap src dest \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_thread s)\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
y <- set_cap dest cap;
gets (opt_parent src) >>= case_option (return ()) (set_parent dest)
od \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>src_cap old_cap y ya. \<lbrace>?B4 src_cap old_cap y ya\<rbrace> set_cap dest cap \<lbrace>\<lambda>yb s. (opt_parent src s = None \<longrightarrow> P (cdl_current_thread s)) \<and> (\<forall>x. opt_parent src s = Some x \<longrightarrow> P (cdl_current_thread s))\<rbrace>
 2. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B4 src_cap old_cap y\<rbrace>
 3. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap old_cap. \<lbrace>?B4 src_cap old_cap () ()\<rbrace> set_cap dest cap \<lbrace>\<lambda>yb s. (opt_parent src s = None \<longrightarrow> P (cdl_current_thread s)) \<and> ((\<exists>a b. opt_parent src s = Some (a, b)) \<longrightarrow> P (cdl_current_thread s))\<rbrace>
 2. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B4 src_cap old_cap y\<rbrace>
 3. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>src_cap old_cap. \<lbrace>?B4 src_cap old_cap () ()\<rbrace> set_cap dest cap \<lbrace>\<lambda>r s. opt_parent src s = None \<longrightarrow> P (cdl_current_thread s)\<rbrace>
 2. \<And>src_cap old_cap. \<lbrace>?B4 src_cap old_cap () ()\<rbrace> set_cap dest cap \<lbrace>\<lambda>r s. (\<exists>a b. opt_parent src s = Some (a, b)) \<longrightarrow> P (cdl_current_thread s)\<rbrace>
 3. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B4 src_cap old_cap y\<rbrace>
 4. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 5. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 7. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>src_cap old_cap. \<lbrace>?B4 src_cap old_cap () ()\<rbrace> set_cap dest cap \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>
 2. \<And>src_cap old_cap. \<lbrace>?B4 src_cap old_cap () ()\<rbrace> set_cap dest cap \<lbrace>\<lambda>r s. (\<exists>a b. opt_parent src s = Some (a, b)) \<longrightarrow> P (cdl_current_thread s)\<rbrace>
 3. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B4 src_cap old_cap y\<rbrace>
 4. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 5. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 7. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap old_cap. \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> set_cap dest cap \<lbrace>\<lambda>r s. (\<exists>a b. opt_parent src s = Some (a, b)) \<longrightarrow> P (cdl_current_thread s)\<rbrace>
 2. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>a b. P (cdl_current_thread b)\<rbrace>
 3. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap old_cap. \<lbrace>\<lambda>a. P (cdl_current_thread a)\<rbrace> set_cap dest cap \<lbrace>\<lambda>rv s. P (cdl_current_thread s)\<rbrace>
 2. \<And>src_cap old_cap y. \<lbrace>?B3 src_cap old_cap y\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>a b. P (cdl_current_thread b)\<rbrace>
 3. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cdl_current_thread s) \<Longrightarrow> opt_cap src s \<noteq> None \<longrightarrow> opt_cap dest s \<noteq> None \<longrightarrow> the (opt_cap dest s) = NullCap \<longrightarrow> P (cdl_current_thread s) proof (prove)
goal:
No subgoals!