theory KHeap_DP

lemma insert_cap_sibling_wp:
  "\<lbrace><dest \<mapsto>c - \<and>* R> and K (\<not> is_untyped_cap cap)\<rbrace>
    insert_cap_sibling cap src dest
   \<lbrace>\<lambda>_. <dest \<mapsto>c cap \<and>* R>\<rbrace>" apply (clarsimp simp: insert_cap_sibling_def) apply (wp) apply (clarsimp split: option.splits) apply (safe) apply (wp set_parent_wp set_cap_wp not_untyped_cap_set_full | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)\<rbrace> insert_cap_sibling cap src dest \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest \<mapsto>c - \<and>* R) and (\<lambda>y. cap_type cap \<noteq> Some UntypedType)\<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>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>src_cap old_cap y ya yb x. \<lbrace>?B6 src_cap old_cap y ya yb x\<rbrace> case x of None \<Rightarrow> return () | Some x \<Rightarrow> set_parent dest x \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>src_cap old_cap y ya yb. \<lbrace>?B5 src_cap old_cap y ya yb\<rbrace> gets (opt_parent src) \<lbrace>?B6 src_cap old_cap y ya yb\<rbrace>
 3. \<And>src_cap old_cap y ya. \<lbrace>?B4 src_cap old_cap y ya\<rbrace> set_cap dest cap \<lbrace>?B5 src_cap old_cap y ya\<rbrace>
 4. \<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>
 5. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 6. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 7. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 8. \<And>s. (cdl.lift (dest \<mapsto>c - \<and>* R) and (\<lambda>y. cap_type cap \<noteq> Some UntypedType)) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>src_cap old_cap x. (x = None \<longrightarrow> \<lbrace>?B6 src_cap old_cap () () () None\<rbrace> return () \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace>) \<and> (\<forall>a b. x = Some (a, b) \<longrightarrow> \<lbrace>?B6 src_cap old_cap () () () (Some (a, b))\<rbrace> set_parent dest (a, b) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace>)
 2. \<And>src_cap old_cap y ya yb. \<lbrace>?B5 src_cap old_cap y ya yb\<rbrace> gets (opt_parent src) \<lbrace>?B6 src_cap old_cap y ya yb\<rbrace>
 3. \<And>src_cap old_cap y ya. \<lbrace>?B4 src_cap old_cap y ya\<rbrace> set_cap dest cap \<lbrace>?B5 src_cap old_cap y ya\<rbrace>
 4. \<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>
 5. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 6. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 7. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 8. \<And>s. (cdl.lift (dest \<mapsto>c - \<and>* R) and (\<lambda>y. cap_type cap \<noteq> Some UntypedType)) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>src_cap old_cap x. \<lbrace>?B6 src_cap old_cap () () () None\<rbrace> return () \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>src_cap old_cap x a b. \<lbrace>?B6 src_cap old_cap () () () (Some (a, b))\<rbrace> set_parent dest (a, b) \<lbrace>\<lambda>_. cdl.lift (dest \<mapsto>c cap \<and>* R)\<rbrace>
 3. \<And>src_cap old_cap y ya yb. \<lbrace>?B5 src_cap old_cap y ya yb\<rbrace> gets (opt_parent src) \<lbrace>?B6 src_cap old_cap y ya yb\<rbrace>
 4. \<And>src_cap old_cap y ya. \<lbrace>?B4 src_cap old_cap y ya\<rbrace> set_cap dest cap \<lbrace>?B5 src_cap old_cap y ya\<rbrace>
 5. \<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>
 6. \<And>src_cap old_cap. \<lbrace>?B2 src_cap old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B3 src_cap old_cap\<rbrace>
 7. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 8. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 9. \<And>s. \<lbrakk>cdl.lift (dest \<mapsto>c - \<and>* R) s; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!