theory CNode_DR

lemma dcorres_insert_cap_combine:
  "cdl_cap = transform_cap cap \<Longrightarrow> dcorres dc \<top>
   (\<lambda>s. cte_wp_at ((=) cap.NullCap) dest s \<and> cte_at src s \<and>
        not_idle_thread (fst dest) s \<and> not_idle_thread (fst src) s \<and>
         valid_mdb s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned cap
   )
   (insert_cap_sibling cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest)
    \<sqinter> insert_cap_child cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest))
   (cap_insert cap src dest)" apply (rule dcorres_expand_pfx) apply clarsimp apply (case_tac "cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src)
    cap (cap_insert_dest_original cap cap')) src s'") apply (rule corres_alternate1) apply (rule corres_guard_imp[OF insert_cap_sibling_corres]) apply clarsimp+ apply (rule corres_alternate2) apply (rule corres_guard_imp[OF insert_cap_child_corres]) apply clarsimp+ apply (fastforce simp:cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_cap = transform_cap cap \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s. cte_wp_at ((=) cap.NullCap) dest s \<and> cte_wp_at (\<lambda>_. True) src s \<and> not_idle_thread (fst dest) s \<and> not_idle_thread (fst src) s \<and> valid_mdb s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_objs s \<and> cap_aligned cap) (insert_cap_sibling cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cdl_cap = transform_cap cap; s = transform s'; True; cte_wp_at ((=) cap.NullCap) dest s' \<and> cte_wp_at (\<lambda>_. True) src s' \<and> not_idle_thread (fst dest) s' \<and> not_idle_thread (fst src) s' \<and> valid_mdb s' \<and> valid_idle s' \<and> valid_etcbs s' \<and> valid_objs s' \<and> cap_aligned cap\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (insert_cap_sibling cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child cdl_cap (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest)
 2. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest)
 2. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (3 subgoals):
 1. \<And>s' s. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' s. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'; s' = s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> cte_wp_at ((=) cap.NullCap) dest s \<and> cte_wp_at (\<lambda>_. True) src s \<and> not_idle_thread (fst dest) s \<and> not_idle_thread (fst src) s \<and> valid_etcbs s \<and> valid_mdb s \<and> valid_idle s \<and> valid_objs s \<and> cap_aligned cap
 3. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_sibling (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest) \<sqinter> insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (insert_cap_child (transform_cap cap) (transform_cslot_ptr src) (transform_cslot_ptr dest)) (cap_insert cap src dest) proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' s. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s'; cte_wp_at (\<lambda>_. True) src s'; not_idle_thread (fst dest) s'; not_idle_thread (fst src) s'; valid_mdb s'; valid_idle s'; valid_etcbs s'; valid_objs s'; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s' src) cap (cap_insert_dest_original cap cap')) src s'; s' = s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s \<and> not_idle_thread (fst dest) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst src) s \<and> valid_objs s \<and> cap_aligned cap proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl_cap = transform_cap cap; cte_wp_at ((=) cap.NullCap) dest s; cte_wp_at (\<lambda>_. True) src s; not_idle_thread (fst dest) s; not_idle_thread (fst src) s; valid_mdb s; valid_idle s; valid_etcbs s; valid_objs s; cap_aligned cap; \<not> cte_wp_at (\<lambda>cap'. \<not> should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s src) cap (cap_insert_dest_original cap cap')) src s proof (prove)
goal:
No subgoals!