theory ArchArch_AI

lemma cap_insert_simple_arch_caps_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 (\<lambda>s. asid_table s (asid_high_bits_of asid) = None)
     and ko_at (ArchObj (ASIDPool Map.empty)) ap
     and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s
                       \<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>" apply (simp add: cap_insert_def update_cdt_def set_cdt_def valid_arch_caps_def
    set_untyped_cap_as_full_def bind_assoc) apply (strengthen valid_vs_lookup_at_upd_strg) apply (wp get_cap_wp set_cap_valid_vs_lookup set_cap_arch_obj
            set_cap_valid_table_caps hoare_vcg_all_lift
          | simp split del: if_split)+ apply (rule_tac P = "cte_wp_at ((=) src_cap) src" in set_cap_orth) apply (wp hoare_vcg_imp_lift hoare_vcg_ball_lift set_free_index_final_cap
                 hoare_vcg_disj_lift set_cap_reachable_pg_cap set_cap.vs_lookup_pages
              | clarsimp)+ apply (wp set_cap_arch_obj set_cap_valid_table_caps hoare_vcg_ball_lift
                get_cap_wp hoare_weak_lift_imp)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) apply (rule conjI) apply (clarsimp simp: vs_cap_ref_def) apply (rule_tac x="fst dest" in exI) apply (rule_tac x="snd dest" in exI) apply simp apply (rule conjI) apply (simp add: unique_table_caps_def is_cap_simps) apply (subst unique_table_refs_def) apply (intro allI impI) apply (simp split: if_split_asm) apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) apply (erule (3) unique_table_refsD) done

(* 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 (\<lambda>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and K (cap = ArchObjectCap (ASIDPoolCap ap asid))\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
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);
x <- gets cdt;
xa <- get;
y <- put (xa\<lparr>cdt := x(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else x src)\<rparr>);
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 s. valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
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);
x <- gets cdt;
xa <- get;
y <- put (xa\<lparr>cdt := x(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else x src)\<rparr>);
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>r s. (valid_vs_lookup s \<and> ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None])) \<and> valid_table_caps s \<and> unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>src_cap x vref cap'. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P86 src_cap x () vref cap'\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. 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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)\<rbrace>
 2. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'84 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. unique_table_refs (caps_of_state s) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap))\<rbrace>
 3. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R80 src_cap x y\<rbrace> return () \<lbrace>\<lambda>rv s. valid_vs_lookup s \<and> ((\<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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap))\<rbrace>
 4. \<And>src_cap x. \<lbrace>?B9 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') src s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (max_free_index_update src_cap) = Some vref \<and> obj_refs (max_free_index_update src_cap) = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (\<forall>xa xb. ?P86 src_cap x y xa xb s) \<and> ?P'84 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R80 src_cap x y s)\<rbrace>
 5. \<And>src_cap. \<lbrace>?B8 src_cap\<rbrace> get_cap dest \<lbrace>?B9 src_cap\<rbrace>
 6. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B8\<rbrace>
 7. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))) s \<Longrightarrow> ?Q6 s proof (prove)
goal (7 subgoals):
 1. \<And>src_cap x vref cap'. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at ((=) src_cap) src s \<and> (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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s))\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. 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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)\<rbrace>
 2. \<And>src_cap x y. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>?P'84 src_cap x y\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. unique_table_refs (caps_of_state s) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap))\<rbrace>
 3. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R80 src_cap x y\<rbrace> return () \<lbrace>\<lambda>rv s. valid_vs_lookup s \<and> ((\<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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap))\<rbrace>
 4. \<And>src_cap x. \<lbrace>?B9 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') src s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (max_free_index_update src_cap) = Some vref \<and> obj_refs (max_free_index_update src_cap) = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (\<forall>x xa. cte_wp_at ((=) src_cap) src s \<and> src \<noteq> dest \<and> (cte_wp_at ((=) xa) dest s \<longrightarrow> vs_cap_ref xa = Some x \<longrightarrow> vs_cap_ref cap = Some x \<and> obj_refs cap = obj_refs xa \<or> \<not> is_final_cap' xa s \<and> \<not> reachable_pg_cap xa s \<or> (\<forall>oref. oref \<in> obj_refs xa \<longrightarrow> (x, oref) \<notin> vs_lookup_pages s))) \<and> ?P'84 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R80 src_cap x y s)\<rbrace>
 5. \<And>src_cap. \<lbrace>?B8 src_cap\<rbrace> get_cap dest \<lbrace>?B9 src_cap\<rbrace>
 6. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B8\<rbrace>
 7. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>src_cap x. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>?P'103 src_cap x ()\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. ako_at (ASIDPool (\<lambda>x. None)) ap s \<and> cte_wp_at (\<lambda>_. True) dest s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b. ((a, b) = dest \<longrightarrow> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]))) \<and> valid_table_caps 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> unique_table_caps (\<lambda>a. if a = dest then Some cap else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some cap else caps_of_state s a)\<rbrace>
 2. \<And>src_cap x y. \<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<Longrightarrow> \<lbrace>?R80 src_cap x y\<rbrace> return () \<lbrace>\<lambda>rv s. valid_vs_lookup s \<and> ((\<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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap))\<rbrace>
 3. \<And>src_cap x. \<lbrace>?B9 src_cap x\<rbrace> assert (x = NullCap) \<lbrace>\<lambda>y s. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') src s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (max_free_index_update src_cap) = Some vref \<and> obj_refs (max_free_index_update src_cap) = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (\<forall>x xa. cte_wp_at ((=) src_cap) src s \<and> src \<noteq> dest \<and> (cte_wp_at ((=) xa) dest s \<longrightarrow> vs_cap_ref xa = Some x \<longrightarrow> vs_cap_ref cap = Some x \<and> obj_refs cap = obj_refs xa \<or> \<not> is_final_cap' xa s \<and> \<not> reachable_pg_cap xa s \<or> (\<forall>oref. oref \<in> obj_refs xa \<longrightarrow> (x, oref) \<notin> vs_lookup_pages s))) \<and> unique_table_refs ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) \<and> ?P'103 src_cap x y s) \<and> (\<not> (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap) \<longrightarrow> ?R80 src_cap x y s)\<rbrace>
 4. \<And>src_cap. \<lbrace>?B8 src_cap\<rbrace> get_cap dest \<lbrace>?B9 src_cap\<rbrace>
 5. \<lbrace>?Q6\<rbrace> get_cap src \<lbrace>?B8\<rbrace>
 6. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vs_lookup and valid_table_caps and (\<lambda>s. unique_table_caps (caps_of_state s) \<and> unique_table_refs (caps_of_state s)) 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>s. asid_table s (asid_high_bits_of asid) = None) and ako_at (ASIDPool (\<lambda>x. None)) ap and (\<lambda>y. cap = ArchObjectCap (ASIDPoolCap ap asid))) s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> (\<forall>capb. cte_wp_at ((=) capb) dest s \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> capb = NullCap \<longrightarrow> (valid_vs_lookup s \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') src s \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (max_free_index_update capa) = Some vref \<and> obj_refs (max_free_index_update capa) = obj_refs cap' \<or> \<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (\<forall>x xa. cte_wp_at ((=) capa) src s \<and> src \<noteq> dest \<and> (cte_wp_at ((=) xa) dest s \<longrightarrow> vs_cap_ref xa = Some x \<longrightarrow> vs_cap_ref cap = Some x \<and> obj_refs cap = obj_refs xa \<or> \<not> is_final_cap' xa s \<and> \<not> reachable_pg_cap xa s \<or> (\<forall>oref. oref \<in> obj_refs xa \<longrightarrow> (x, oref) \<notin> vs_lookup_pages s))) \<and> unique_table_refs ((caps_of_state s)(src \<mapsto> max_free_index_update capa)) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) src) s \<and> cte_wp_at (\<lambda>_. True) dest s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b. ((a, b) = dest \<longrightarrow> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. ((caps_of_state s)(src \<mapsto> max_free_index_update capa)) (a, b) = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]))) \<and> (valid_table_caps s \<and> (is_pt_cap (max_free_index_update capa) \<or> is_pd_cap (max_free_index_update capa) \<longrightarrow> cap_asid (max_free_index_update capa) = None \<longrightarrow> (\<forall>r\<in>obj_refs (max_free_index_update capa). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> (\<forall>x\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) x s)) \<and> unique_table_caps (\<lambda>a. if a = dest then Some cap else ((caps_of_state s)(src \<mapsto> max_free_index_update capa)) a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some cap else ((caps_of_state s)(src \<mapsto> max_free_index_update capa)) a)) \<and> (\<not> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap) \<longrightarrow> capb = NullCap \<longrightarrow> valid_vs_lookup s \<and> ((\<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. oref \<in> obj_refs cap' \<longrightarrow> (vref, oref) \<notin> vs_lookup_pages s)) \<and> unique_table_refs (caps_of_state s)) \<and> (ako_at (ASIDPool (\<lambda>x. None)) ap and cte_wp_at (\<lambda>_. True) dest) s \<and> asid_table s (asid_high_bits_of asid) = None \<and> (\<exists>a b capa. ((caps_of_state s)(dest \<mapsto> cap)) (a, b) = Some capa \<and> ap \<in> obj_refs capa \<and> vs_cap_ref capa = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> (valid_table_caps s \<and> (is_pt_cap cap \<or> 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> unique_table_caps ((caps_of_state s)(dest \<mapsto> cap)) \<and> unique_table_refs ((caps_of_state s)(dest \<mapsto> cap)))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> (\<exists>a b. ((a, b) = dest \<longrightarrow> vs_cap_ref (ArchObjectCap (ASIDPoolCap ap asid)) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]))) \<and> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> \<exists>a b. ((a, b) = dest \<longrightarrow> vs_cap_ref (ArchObjectCap (ASIDPoolCap ap asid)) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<and> ((a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]))
 2. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> \<exists>a b. (a, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> ap \<in> obj_refs cap \<and> (case cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap ASIDControlCap \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights _ None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights _ (Some (asid, vptr))) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None])
 2. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> \<exists>b. (fst dest, b) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (fst dest, b) = Some cap \<and> ap \<in> obj_refs cap \<and> (case cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap ASIDControlCap \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights _ None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights _ (Some (asid, vptr))) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None])
 2. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> (fst dest, snd dest) \<noteq> dest \<longrightarrow> (\<exists>cap. caps_of_state s (fst dest, snd dest) = Some cap \<and> ap \<in> obj_refs cap \<and> (case cap of ArchObjectCap (ASIDPoolCap obj_ref asid) \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap ASIDControlCap \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights ARMSuperSection (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageCap dev obj_ref rights _ None) \<Rightarrow> None | ArchObjectCap (PageCap dev obj_ref rights _ (Some (asid, vptr))) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageTableCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageTableCap obj_ref (Some (asid, vptr))) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | ArchObjectCap (PageDirectoryCap obj_ref None) \<Rightarrow> None | ArchObjectCap (PageDirectoryCap obj_ref (Some asid)) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | _ \<Rightarrow> None) = Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None])
 2. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) \<and> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_caps (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a)
 2. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>a. if a = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (if p = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s p) = Some cap \<longrightarrow> (if p' = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>s capa p p' capaa cap'. \<lbrakk>valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; (if p = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s p) = Some capaa; (if p' = dest then Some (ArchObjectCap (ASIDPoolCap ap asid)) else caps_of_state s p') = Some cap'; obj_refs cap' = obj_refs capaa\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa proof (prove)
goal (3 subgoals):
 1. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref capaa {dest} s; safe_parent_for (cdt s) src capaa capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = capaa; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p = dest; ArchObjectCap (ASIDPoolCap ap asid) = capaa; p' \<noteq> dest; caps_of_state s p' = Some cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa
 2. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref cap' {dest} s; safe_parent_for (cdt s) src cap' capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = cap'; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p \<noteq> dest; caps_of_state s p = Some capaa; p' = dest; ArchObjectCap (ASIDPoolCap ap asid) = cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa
 3. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p \<noteq> dest; caps_of_state s p = Some capaa; p' \<noteq> dest; caps_of_state s p' = Some cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa proof (prove)
goal (2 subgoals):
 1. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref cap' {dest} s; safe_parent_for (cdt s) src cap' capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = cap'; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p \<noteq> dest; caps_of_state s p = Some capaa; p' = dest; ArchObjectCap (ASIDPoolCap ap asid) = cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa
 2. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p \<noteq> dest; caps_of_state s p = Some capaa; p' \<noteq> dest; caps_of_state s p' = Some cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa proof (prove)
goal (1 subgoal):
 1. \<And>s capa p p' capaa cap'. \<lbrakk>obj_refs cap' = obj_refs capaa; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref (ArchObjectCap (ASIDPoolCap ap asid)) {dest} s; safe_parent_for (cdt s) src (ArchObjectCap (ASIDPoolCap ap asid)) capa; asid_table s (asid_high_bits_of asid) = None; ako_at (ASIDPool (\<lambda>x. None)) ap s; cap = ArchObjectCap (ASIDPoolCap ap asid); caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; p \<noteq> dest; caps_of_state s p = Some capaa; p' \<noteq> dest; caps_of_state s p' = Some cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capaa proof (prove)
goal:
No subgoals!