theory CSpace_AI

lemma cap_insert_mdb_cte_at:
  "\<lbrace>(\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s))
    and valid_cap cap and
    (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and
    K (src \<noteq> dest) \<rbrace>
    cap_insert cap src dest
   \<lbrace>\<lambda>_ s.  mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" unfolding cap_insert_def apply (wp | simp cong: update_original_mdb_cte_at split del: if_split)+ apply (wp update_cdt_mdb_cte_at set_cap_mdb_cte_at[simplified swp_def] | simp split del: if_split)+ apply wps apply (wp valid_case_option_post_wp hoare_vcg_if_lift hoare_impI mdb_cte_at_set_untyped_cap_as_full[simplified swp_def]
    set_cap_cte_wp_at get_cap_wp)+ apply (clarsimp simp:free_index_update_def split:cap.splits) apply (wp)+ apply (clarsimp simp:conj_comms split del:if_split cong:prod.case_cong_weak) apply (wps) apply (wp valid_case_option_post_wp get_cap_wp hoare_vcg_if_lift
    hoare_impI set_untyped_cap_as_full_cte_wp_at )+ apply (unfold swp_def) apply (intro conjI | clarify)+ apply (clarsimp simp:free_index_update_def split:cap.splits) apply (drule mdb_cte_at_cte_wp_at[simplified swp_def]) apply simp apply (simp add:cte_wp_at_caps_of_state) apply (clarsimp split del: if_split split:option.splits
                  simp: cte_wp_at_caps_of_state not_sym[OF is_derived_not_Null] neq_commute)+ apply (drule imp_rev) apply (clarsimp split:if_splits cap.splits
                   simp:free_index_update_def is_cap_simps masked_as_full_def) apply (subst (asm) mdb_cte_at_def,elim allE impE,simp,clarsimp simp:cte_wp_at_caps_of_state)+ apply (clarsimp split: if_splits cap.splits
                  simp: free_index_update_def is_cap_simps masked_as_full_def) apply (subst (asm) mdb_cte_at_def,elim allE impE,simp,clarsimp simp:cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_ s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)\<rbrace> do src_cap <- get_cap src;
dest_original <- return $ is_cap_revocable cap src_cap;
old_cap <- get_cap dest;
assert (old_cap = NullCap);
set_untyped_cap_as_full src_cap cap src;
set_cap cap dest;
is_original <- gets is_original_cap;
src_parent <- return $ should_be_parent_of src_cap (is_original src) cap dest_original;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src));
do_extended_op (cap_insert_ext src_parent src dest src_p dest_p);
set_original dest dest_original
od \<lbrace>\<lambda>_ s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>src_cap dest_original old_cap is_original src_parent src_p dest_p. \<lbrace>?B13 src_cap dest_original old_cap () () () is_original src_parent src_p dest_p\<rbrace> update_cdt (\<lambda>cdt. cdt(dest := if src_parent then Some src else cdt src)) \<lbrace>\<lambda>xc s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)\<rbrace>
 2. \<And>src_cap dest_original old_cap x xa xb is_original src_parent src_p. \<lbrace>?B12 src_cap dest_original old_cap x xa xb is_original src_parent src_p\<rbrace> gets (\<lambda>s. cdt s dest) \<lbrace>?B13 src_cap dest_original old_cap x xa xb is_original src_parent src_p\<rbrace>
 3. \<And>src_cap dest_original old_cap x xa xb is_original src_parent. \<lbrace>?B11 src_cap dest_original old_cap x xa xb is_original src_parent\<rbrace> gets (\<lambda>s. cdt s src) \<lbrace>?B12 src_cap dest_original old_cap x xa xb is_original src_parent\<rbrace>
 4. \<And>src_cap dest_original old_cap x xa xb is_original. \<lbrace>?B10 src_cap dest_original old_cap x xa xb is_original\<rbrace> return $ should_be_parent_of src_cap (is_original src) cap dest_original \<lbrace>?B11 src_cap dest_original old_cap x xa xb is_original\<rbrace>
 5. \<And>src_cap dest_original old_cap x xa xb. \<lbrace>?B8 src_cap dest_original old_cap x xa xb\<rbrace> gets is_original_cap \<lbrace>?B10 src_cap dest_original old_cap x xa xb\<rbrace>
 6. \<And>src_cap dest_original old_cap x xa. \<lbrace>?B6 src_cap dest_original old_cap x xa\<rbrace> set_cap cap dest \<lbrace>?B8 src_cap dest_original old_cap x xa\<rbrace>
 7. \<And>src_cap dest_original old_cap x. \<lbrace>?B4 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>?B6 src_cap dest_original old_cap x\<rbrace>
 8. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B4 src_cap dest_original old_cap\<rbrace>
 9. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 10. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
A total of 12 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>src_cap dest_original old_cap. \<lbrace>?P'40 src_cap dest_original old_cap () ()\<rbrace> set_cap cap dest \<lbrace>\<lambda>rv s. case if should_be_parent_of src_cap (is_original_cap s src) cap dest_original then Some src else cdt s src of None \<Rightarrow> True | Some p \<Rightarrow> cte_wp_at ((\<noteq>) NullCap) p s \<and> cte_wp_at ((\<noteq>) NullCap) dest s\<rbrace>
 2. \<And>src_cap dest_original old_cap x. \<lbrace>?B4 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>a b. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y b) (cdt b) \<and> (dest \<in> dom (cdt b) \<union> ran (cdt b) \<longrightarrow> NullCap \<noteq> cap)) \<and> ?P'40 src_cap dest_original old_cap x a b\<rbrace>
 3. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B4 src_cap dest_original old_cap\<rbrace>
 4. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 5. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 7. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>src_cap dest_original old_cap prev_s. \<lbrace>?P44 src_cap dest_original old_cap prev_s\<rbrace> set_cap cap dest \<lbrace>\<lambda>rv s'. case if should_be_parent_of src_cap (is_original_cap prev_s src) cap dest_original then Some src else cdt prev_s src of None \<Rightarrow> True | Some p \<Rightarrow> cte_wp_at ((\<noteq>) NullCap) p s' \<and> cte_wp_at ((\<noteq>) NullCap) dest s'\<rbrace>
 2. \<And>src_cap dest_original old_cap x. \<lbrace>?B4 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>a b. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y b) (cdt b) \<and> (dest \<in> dom (cdt b) \<union> ran (cdt b) \<longrightarrow> NullCap \<noteq> cap)) \<and> ?P'40 src_cap dest_original old_cap x a b\<rbrace>
 3. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>?B4 src_cap dest_original old_cap\<rbrace>
 4. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 5. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 7. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s
flex-flex pairs:
\<lambda>src_cap dest_original old_cap s. ?P44 src_cap dest_original old_cap s s \<equiv>\<^sup>? \<lambda>src_cap dest_original old_cap. ?P'40 src_cap dest_original old_cap () () proof (prove)
goal (7 subgoals):
 1. \<And>src_cap dest_original old_cap x a cap. (NullCap \<noteq> free_index_update (\<lambda>_. a) cap) = (NullCap \<noteq> cap)
 2. \<And>src_cap dest_original old_cap x. \<lbrace>?P'68 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> (case if should_be_parent_of src_cap (is_original_cap s src) cap dest_original then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>s. if x = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) x s) and cte_wp_at (\<lambda>_. True) dest) s \<and> ((\<lambda>s. if dest = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) dest s) and cte_wp_at (\<lambda>_. True) dest) s)\<rbrace>
 3. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>\<lambda>x s. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s) \<and> ?P'68 src_cap dest_original old_cap x s\<rbrace>
 4. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 5. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 6. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 7. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap dest_original old_cap x. \<lbrace>?P'68 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> (case if should_be_parent_of src_cap (is_original_cap s src) cap dest_original then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>s. if x = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) x s) and cte_wp_at (\<lambda>_. True) dest) s \<and> ((\<lambda>s. if dest = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) dest s) and cte_wp_at (\<lambda>_. True) dest) s)\<rbrace>
 2. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>\<lambda>x s. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s) \<and> ?P'68 src_cap dest_original old_cap x s\<rbrace>
 3. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap dest_original old_cap x. \<lbrace>?P'76 src_cap dest_original old_cap x\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. case if should_be_parent_of src_cap (is_original_cap s src) cap dest_original then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>s. if x = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) x s) and cte_wp_at (\<lambda>_. True) dest) s \<and> ((\<lambda>s. if dest = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) dest s) and cte_wp_at (\<lambda>_. True) dest) s\<rbrace>
 2. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>\<lambda>x s. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> ?P'76 src_cap dest_original old_cap x s\<rbrace>
 3. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap dest_original old_cap. \<lbrace>?P'76 src_cap dest_original old_cap ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. case if should_be_parent_of src_cap (is_original_cap s src) cap dest_original then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> ((\<lambda>s. if x = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) x s) and cte_wp_at (\<lambda>_. True) dest) s \<and> ((\<lambda>s. if dest = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) dest s) and cte_wp_at (\<lambda>_. True) dest) s\<rbrace>
 2. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>\<lambda>x s. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> ?P'76 src_cap dest_original old_cap x s\<rbrace>
 3. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap dest_original old_cap prev_s. \<lbrace>?P83 src_cap dest_original old_cap prev_s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s'. case if should_be_parent_of src_cap (is_original_cap prev_s src) cap dest_original then Some src else cdt prev_s src of None \<Rightarrow> True | Some x \<Rightarrow> (if x = dest then NullCap \<noteq> cap else cte_wp_at ((\<noteq>) NullCap) x s') \<and> cte_wp_at (\<lambda>_. True) dest s' \<and> NullCap \<noteq> cap \<and> cte_wp_at (\<lambda>_. True) dest s'\<rbrace>
 2. \<And>src_cap dest_original old_cap. \<lbrace>?B3 src_cap dest_original old_cap\<rbrace> assert (old_cap = NullCap) \<lbrace>\<lambda>x s. (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> ?P'76 src_cap dest_original old_cap x s\<rbrace>
 3. \<And>src_cap dest_original. \<lbrace>?B2 src_cap dest_original\<rbrace> get_cap dest \<lbrace>?B3 src_cap dest_original\<rbrace>
 4. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> return $ is_cap_revocable cap src_cap \<lbrace>?B2 src_cap\<rbrace>
 5. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> ?Q s
flex-flex pairs:
\<lambda>src_cap dest_original old_cap s. ?P83 src_cap dest_original old_cap s s \<equiv>\<^sup>? \<lambda>src_cap dest_original old_cap. ?P'76 src_cap dest_original old_cap () proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<longrightarrow> (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) capa) src s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> (case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s)) and (\<lambda>s. no_mloop (cdt s)) and valid_cap cap and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> capb = NullCap \<longrightarrow> (mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s) \<and> cte_wp_at ((=) capa) src s) \<and> (dest \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> NullCap \<noteq> cap) \<and> (case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src NullCap) src s; s \<turnstile> NullCap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; dest \<in> dom (cdt s) \<union> ran (cdt s); cap = NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src cap) src s; s \<turnstile> cap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>src \<noteq> dest; cte_wp_at (is_derived (cdt s) src NullCap) src s; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; dest \<in> dom (cdt s) \<or> dest \<in> ran (cdt s); cap = NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src cap) src s; s \<turnstile> cap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>src \<noteq> dest; cte_wp_at (is_derived (cdt s) src NullCap) src s; no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; dest \<in> dom (cdt s) \<or> dest \<in> ran (cdt s); cap = NullCap\<rbrakk> \<Longrightarrow> ?src176 s capa \<in> dom (cdt s) \<or> ?src176 s capa \<in> ran (cdt s)
 2. \<And>s capa. \<lbrakk>src \<noteq> dest; cte_wp_at (is_derived (cdt s) src NullCap) src s; no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; dest \<in> dom (cdt s) \<or> dest \<in> ran (cdt s); cap = NullCap; cte_wp_at ((\<noteq>) NullCap) (?src176 s capa) s\<rbrakk> \<Longrightarrow> False
 3. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src cap) src s; s \<turnstile> cap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>src \<noteq> dest; cte_wp_at (is_derived (cdt s) src NullCap) src s; no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s; dest \<in> dom (cdt s) \<or> dest \<in> ran (cdt s); cap = NullCap; cte_wp_at ((\<noteq>) NullCap) dest s\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src cap) src s; s \<turnstile> cap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s proof (prove)
goal (1 subgoal):
 1. \<And>s capa capaa. \<lbrakk>K (src \<noteq> dest) s; cte_wp_at (is_derived (cdt s) src cap) src s; s \<turnstile> cap; mdb_cte_at (\<lambda>y. cte_wp_at ((\<noteq>) NullCap) y s) (cdt s); no_mloop (cdt s); cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> case if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src of None \<Rightarrow> True | Some x \<Rightarrow> (NullCap \<noteq> cap \<and> (x \<noteq> src \<and> cte_wp_at ((\<noteq>) NullCap) x s \<or> x = src \<and> cte_wp_at (\<lambda>a. NullCap \<noteq> masked_as_full a cap) src s) \<and> cte_wp_at ((=) capa) src s) \<and> ((dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s) \<and> NullCap \<noteq> cap \<and> (dest \<noteq> src \<and> cte_wp_at (\<lambda>a. True) dest s \<or> dest = src \<and> cte_wp_at (\<lambda>a. True) src s) \<and> cte_wp_at ((=) capa) src s proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src) = Some (a, b); src = (a, b) \<longrightarrow> NullCap = masked_as_full capa cap\<rbrakk> \<Longrightarrow> src \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src) = Some (a, b)\<rbrakk> \<Longrightarrow> NullCap \<noteq> masked_as_full capa cap
 2. \<And>s capa a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src) = Some (a, b); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> src \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap NullCap; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some NullCap; caps_of_state s dest = Some NullCap; cdt s src = Some (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src) = Some (a, b); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> src \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b. \<lbrakk>dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa) then Some src else cdt s src) = Some (a, b); src \<noteq> (a, b)\<rbrakk> \<Longrightarrow> src \<noteq> (a, b) \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b. \<lbrakk>src \<noteq> (a, b); dest \<noteq> src; is_derived (cdt s) src cap capa; s \<turnstile> cap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> cap \<noteq> NullCap) (cdt s); no_mloop (cdt s); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; \<not> should_be_parent_of capa (is_original_cap s src) cap (is_cap_revocable cap capa); cdt s src = Some (a, b)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap proof (prove)
goal:
No subgoals!