theory ArchCSpace_AI

lemma cap_insert_simple_arch_caps_no_ap:
  "\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s)
             and no_cap_to_obj_with_diff_ref cap {dest} and K (is_simple_cap cap \<and> \<not>is_ap_cap cap)\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: cap_insert_def) apply (wp set_cap_valid_arch_caps set_untyped_cap_as_full_valid_arch_caps get_cap_wp
    | simp split del: if_split)+ apply (wp hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_imp_lift hoare_vcg_ball_lift hoare_vcg_disj_lift
    set_untyped_cap_as_full_cte_wp_at_neg set_untyped_cap_as_full_is_final_cap'_neg
    set_untyped_cap_as_full_empty_table_at hoare_vcg_ex_lift
    set_untyped_cap_as_full_caps_of_state_diff[where dest=dest]
    | wps)+ apply (wp get_cap_wp)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (intro conjI impI allI) by (auto simp:is_simple_cap_def[simplified is_simple_cap_arch_def] is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and K (is_simple_cap cap \<and> \<not> is_ap_cap cap)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap)\<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 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 <- do_extended_op (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>rv. valid_arch_caps\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>src_cap x. \<lbrace>?P'32 src_cap x ()\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. (\<forall>vref cap'. cte_wp_at ((=) cap') dest s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref cap {dest} s \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (is_pt_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = dest)) \<and> (is_pd_cap cap \<longrightarrow> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap)) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap \<and> (is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = dest))\<rbrace>
 2. \<And>src_cap x. \<lbrace>?B2 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (valid_arch_caps and cte_wp_at ((=) src_cap) src) s \<and> ?P'32 src_cap x y s\<rbrace>
 3. \<And>src_cap. \<lbrace>?B1 src_cap\<rbrace> get_cap dest \<lbrace>?B2 src_cap\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>?B1\<rbrace>
 5. \<And>s. (valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>src_cap. \<lbrace>?P'300 src_cap\<rbrace> get_cap dest \<lbrace>\<lambda>rv s. rv \<noteq> NullCap\<rbrace>
 2. \<And>src_cap. \<lbrace>?Q'300 src_cap\<rbrace> get_cap dest \<lbrace>\<lambda>rv. valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace>
 3. \<And>src_cap. \<lbrace>?P'299 src_cap\<rbrace> get_cap dest \<lbrace>\<lambda>rv s. (\<forall>x xa. ((rv = NullCap \<longrightarrow> dest \<noteq> src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at ((=) xa) dest s) \<or> (rv = NullCap \<longrightarrow> dest = src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. xa = masked_as_full a cap) src s)) \<and> (rv = NullCap \<longrightarrow> cte_wp_at ((=) src_cap) src s) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> vs_cap_ref xa \<noteq> Some x) \<or> ((rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> vs_cap_ref cap = Some x)) \<and> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> obj_refs cap = obj_refs xa) \<or> ((rv = NullCap \<longrightarrow> \<not> is_final_cap' xa s) \<and> (rv = NullCap \<longrightarrow> cte_wp_at ((=) src_cap) src s)) \<and> (rv = NullCap \<longrightarrow> \<not> reachable_pg_cap xa s) \<or> (\<forall>xa\<in>obj_refs xa. rv = NullCap \<longrightarrow> (x, xa) \<notin> vs_lookup_pages s)) \<and> ((rv = NullCap \<longrightarrow> no_cap_to_obj_with_diff_ref cap {dest} s) \<and> (rv = NullCap \<longrightarrow> cte_wp_at ((=) src_cap) src s)) \<and> ((rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> cap_asid cap \<noteq> None) \<or> (\<forall>x\<in>obj_refs cap. rv = NullCap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> ((rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> cap_asid cap \<noteq> None) \<or> (\<forall>x\<in>obj_refs cap. rv = NullCap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> ((rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap))) \<or> (\<forall>x xa. ((rv = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs a = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap a \<or> is_pt_cap a) \<and> (cap_asid cap = None \<or> cap_asid a = None)) (x, xa) s) \<or> (rv = NullCap \<longrightarrow> (x, xa) = src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs (masked_as_full a cap) = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap (masked_as_full a cap) \<or> is_pt_cap (masked_as_full a cap)) \<and> (cap_asid cap = None \<or> cap_asid (masked_as_full a cap) = None)) src s)) \<and> (rv = NullCap \<longrightarrow> cte_wp_at ((=) src_cap) src s) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> (x, xa) = dest))) \<and> ((rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> \<not> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap))) \<or> (\<forall>x xa. ((rv = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs a = obj_refs cap \<and> (is_pd_cap a \<or> is_pt_cap cap \<and> is_pt_cap a) \<and> (cap_asid cap = None \<or> cap_asid a = None)) (x, xa) s) \<or> (rv = NullCap \<longrightarrow> (x, xa) = src) \<and> (rv = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs (masked_as_full a cap) = obj_refs cap \<and> (is_pd_cap (masked_as_full a cap) \<or> is_pt_cap cap \<and> is_pt_cap (masked_as_full a cap)) \<and> (cap_asid cap = None \<or> cap_asid (masked_as_full a cap) = None)) src s)) \<and> (rv = NullCap \<longrightarrow> cte_wp_at ((=) src_cap) src s) \<or> (rv = NullCap \<longrightarrow> src \<noteq> dest) \<and> (rv = NullCap \<longrightarrow> (x, xa) = dest)))\<rbrace>
 4. \<lbrace>?Q\<rbrace> get_cap src \<lbrace>\<lambda>src_cap s. (?P'300 src_cap s \<or> ?Q'300 src_cap s) \<and> ?P'299 src_cap s\<rbrace>
 5. \<And>s. (valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and no_cap_to_obj_with_diff_ref cap {dest} and (\<lambda>y. is_simple_cap cap \<and> \<not> is_ap_cap cap)) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> ((\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> cap \<noteq> NullCap) \<or> (\<forall>cap. cte_wp_at ((=) cap) dest s \<longrightarrow> (valid_arch_caps and cte_wp_at ((=) capa) src) s)) \<and> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> (\<forall>x xa. ((capb = NullCap \<longrightarrow> dest \<noteq> src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at ((=) xa) dest s) \<or> (capb = NullCap \<longrightarrow> dest = src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. xa = masked_as_full a cap) src s)) \<and> (capb = NullCap \<longrightarrow> cte_wp_at ((=) capa) src s) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> vs_cap_ref xa \<noteq> Some x) \<or> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> vs_cap_ref cap = Some x)) \<and> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> obj_refs cap = obj_refs xa) \<or> ((capb = NullCap \<longrightarrow> \<not> is_final_cap' xa s) \<and> (capb = NullCap \<longrightarrow> cte_wp_at ((=) capa) src s)) \<and> (capb = NullCap \<longrightarrow> \<not> reachable_pg_cap xa s) \<or> (\<forall>xa\<in>obj_refs xa. capb = NullCap \<longrightarrow> (x, xa) \<notin> vs_lookup_pages s)) \<and> ((capb = NullCap \<longrightarrow> no_cap_to_obj_with_diff_ref cap {dest} s) \<and> (capb = NullCap \<longrightarrow> cte_wp_at ((=) capa) src s)) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> cap_asid cap \<noteq> None) \<or> (\<forall>x\<in>obj_refs cap. capb = NullCap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> cap_asid cap \<noteq> None) \<or> (\<forall>x\<in>obj_refs cap. capb = NullCap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap cap \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap))) \<or> (\<forall>x xa. ((capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs a = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap a \<or> is_pt_cap a) \<and> (cap_asid cap = None \<or> cap_asid a = None)) (x, xa) s) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs (masked_as_full a cap) = obj_refs cap \<and> (is_pd_cap cap \<and> is_pd_cap (masked_as_full a cap) \<or> is_pt_cap (masked_as_full a cap)) \<and> (cap_asid cap = None \<or> cap_asid (masked_as_full a cap) = None)) src s)) \<and> (capb = NullCap \<longrightarrow> cte_wp_at ((=) capa) src s) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest))) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> (\<forall>oldcap. caps_of_state s dest = Some oldcap \<longrightarrow> (is_pt_cap cap \<and> is_pt_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) \<and> (is_pd_cap oldcap \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap))) \<or> (\<forall>x xa. ((capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs a = obj_refs cap \<and> (is_pd_cap a \<or> is_pt_cap cap \<and> is_pt_cap a) \<and> (cap_asid cap = None \<or> cap_asid a = None)) (x, xa) s) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> \<not> cte_wp_at (\<lambda>a. obj_refs (masked_as_full a cap) = obj_refs cap \<and> (is_pd_cap (masked_as_full a cap) \<or> is_pt_cap cap \<and> is_pt_cap (masked_as_full a cap)) \<and> (cap_asid cap = None \<or> cap_asid (masked_as_full a cap) = None)) src s)) \<and> (capb = NullCap \<longrightarrow> cte_wp_at ((=) capa) src s) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest)))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa capb. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb\<rbrakk> \<Longrightarrow> (capb = NullCap \<longrightarrow> (\<forall>x xa. dest \<noteq> src \<and> xa \<noteq> NullCap \<or> dest = src \<and> xa \<noteq> masked_as_full capa cap \<or> src \<noteq> dest \<and> vs_cap_ref xa \<noteq> Some x \<or> src \<noteq> dest \<and> vs_cap_ref cap = Some x \<and> src \<noteq> dest \<and> obj_refs cap = obj_refs xa \<or> \<not> is_final_cap' xa s \<and> \<not> reachable_pg_cap xa s \<or> (\<forall>xa\<in>obj_refs xa. (x, xa) \<notin> vs_lookup_pages s))) \<and> (capb = NullCap \<longrightarrow> src \<noteq> dest \<and> \<not> is_pt_cap cap \<or> src \<noteq> dest \<and> (\<exists>y. cap_asid cap = Some y) \<or> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> (capb = NullCap \<longrightarrow> src \<noteq> dest \<and> \<not> is_pd_cap cap \<or> src \<noteq> dest \<and> (\<exists>y. cap_asid cap = Some y) \<or> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> capb \<noteq> NullCap \<or> (\<forall>x xa. (capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (x, xa) = Some capa \<longrightarrow> (is_pd_cap cap \<longrightarrow> \<not> is_pd_cap capa) \<and> \<not> is_pt_cap capa \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y))) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> obj_refs capa = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> \<not> is_pd_cap capa) \<and> \<not> is_pt_cap capa \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y)) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest))) \<and> ((capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> capb \<noteq> NullCap \<or> (\<forall>x xa. (capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (x, xa) = Some capa \<longrightarrow> \<not> is_pd_cap capa \<and> (is_pt_cap cap \<longrightarrow> \<not> is_pt_cap capa) \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y))) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> obj_refs capa = obj_refs cap \<longrightarrow> \<not> is_pd_cap capa \<and> (is_pt_cap cap \<longrightarrow> \<not> is_pt_cap capa) \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y)) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest))) proof (prove)
goal (5 subgoals):
 1. \<And>s capa capb x xa. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb; capb = NullCap\<rbrakk> \<Longrightarrow> dest \<noteq> src \<and> xa \<noteq> NullCap \<or> dest = src \<and> xa \<noteq> masked_as_full capa cap \<or> src \<noteq> dest \<and> vs_cap_ref xa \<noteq> Some x \<or> src \<noteq> dest \<and> vs_cap_ref cap = Some x \<and> src \<noteq> dest \<and> obj_refs cap = obj_refs xa \<or> \<not> is_final_cap' xa s \<and> \<not> reachable_pg_cap xa s \<or> (\<forall>xa\<in>obj_refs xa. (x, xa) \<notin> vs_lookup_pages s)
 2. \<And>s capa capb. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb; capb = NullCap\<rbrakk> \<Longrightarrow> src \<noteq> dest \<and> \<not> is_pt_cap cap \<or> src \<noteq> dest \<and> (\<exists>y. cap_asid cap = Some y) \<or> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)
 3. \<And>s capa capb. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb; capb = NullCap\<rbrakk> \<Longrightarrow> src \<noteq> dest \<and> \<not> is_pd_cap cap \<or> src \<noteq> dest \<and> (\<exists>y. cap_asid cap = Some y) \<or> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)
 4. \<And>s capa capb. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb\<rbrakk> \<Longrightarrow> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pt_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> capb \<noteq> NullCap \<or> (\<forall>x xa. (capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (x, xa) = Some capa \<longrightarrow> (is_pd_cap cap \<longrightarrow> \<not> is_pd_cap capa) \<and> \<not> is_pt_cap capa \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y))) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> obj_refs capa = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> \<not> is_pd_cap capa) \<and> \<not> is_pt_cap capa \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y)) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest))
 5. \<And>s capa capb. \<lbrakk>valid_arch_caps s; no_cap_to_obj_with_diff_ref cap {dest} s; safe_parent_for (cdt s) src cap capa; is_simple_cap cap; \<not> is_ap_cap cap; caps_of_state s src = Some capa; caps_of_state s dest = Some capb\<rbrakk> \<Longrightarrow> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> \<not> is_pd_cap cap) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> capb \<noteq> NullCap \<or> (\<forall>x xa. (capb = NullCap \<longrightarrow> (x, xa) \<noteq> src) \<and> (capb = NullCap \<longrightarrow> (\<forall>capa. obj_refs capa = obj_refs cap \<longrightarrow> caps_of_state s (x, xa) = Some capa \<longrightarrow> \<not> is_pd_cap capa \<and> (is_pt_cap cap \<longrightarrow> \<not> is_pt_cap capa) \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y))) \<or> (capb = NullCap \<longrightarrow> (x, xa) = src) \<and> (capb = NullCap \<longrightarrow> obj_refs capa = obj_refs cap \<longrightarrow> \<not> is_pd_cap capa \<and> (is_pt_cap cap \<longrightarrow> \<not> is_pt_cap capa) \<or> (\<exists>y. cap_asid cap = Some y) \<and> (\<exists>y. cap_asid capa = Some y)) \<or> (capb = NullCap \<longrightarrow> src \<noteq> dest) \<and> (capb = NullCap \<longrightarrow> (x, xa) = dest))