theory ArchUntyped_AI

lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]:
  "\<lbrace>valid_arch_caps
      and valid_cap (default_cap tp oref sz dev)
      and (\<lambda>(s::'state_ext::state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
                (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
              \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
      and cte_wp_at ((=) cap.NullCap) cref
      and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
     create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" apply (simp add: create_cap_def set_cdt_def) apply (wp set_cap_valid_arch_caps) apply (simp add: trans_state_update[symmetric] del: trans_state_update) apply (wp hoare_vcg_disj_lift hoare_vcg_conj_lift hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+ apply (clarsimp simp del: split_paired_All split_paired_Ex
                            imp_disjL
                      simp: cte_wp_at_caps_of_state) apply (rule conjI) apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                         cte_wp_at_caps_of_state) apply (case_tac "\<exists>x. x \<in> obj_refs cap") apply (clarsimp dest!: obj_ref_elemD) apply (case_tac cref, fastforce) apply (simp add: obj_ref_none_no_asid) apply (rule conjI) apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def
                     obj_at_def nonempty_table_def a_type_simps)[1] apply (clarsimp simp del: imp_disjL) apply (case_tac "\<exists>x. x \<in> obj_refs cap") apply (clarsimp dest!: obj_ref_elemD) apply fastforce apply (auto simp: is_cap_simps)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at ((=) NullCap) cref and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at ((=) NullCap) cref and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od;
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>dest_p cdt y s f. (valid_arch_caps (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (default_cap tp oref sz dev) = Some vref \<and> obj_refs (default_cap tp oref sz dev) = obj_refs cap' \<or> \<not> is_final_cap' cap' (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<and> \<not> reachable_pg_cap cap' (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>))) \<and> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>))))) r (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>))) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> (\<forall>oldcap. caps_of_state (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) cref = Some oldcap \<longrightarrow> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap oldcap \<or> is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (default_cap tp oref sz dev)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap' \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap') \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap' = None)) ptr' (trans_state f s\<lparr>is_original_cap := (is_original_cap (trans_state f s))(cref := True)\<rparr>) \<longrightarrow> ptr' = cref))) = (valid_arch_caps (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (default_cap tp oref sz dev) = Some vref \<and> obj_refs (default_cap tp oref sz dev) = obj_refs cap' \<or> \<not> is_final_cap' cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> \<not> reachable_pg_cap cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))))) r (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> (\<forall>oldcap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) cref = Some oldcap \<longrightarrow> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap oldcap \<or> is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (default_cap tp oref sz dev)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap' \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap') \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap' = None)) ptr' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> ptr' = cref)))
 2. \<And>dest_p cdt. \<lbrace>?B8 dest_p cdt\<rbrace> do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od \<lbrace>\<lambda>y s. valid_arch_caps (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (default_cap tp oref sz dev) = Some vref \<and> obj_refs (default_cap tp oref sz dev) = obj_refs cap' \<or> \<not> is_final_cap' cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> \<not> reachable_pg_cap cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))))) r (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> (\<forall>oldcap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) cref = Some oldcap \<longrightarrow> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap oldcap \<or> is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (default_cap tp oref sz dev)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap' \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap') \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap' = None)) ptr' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> ptr' = cref))\<rbrace>
 3. \<And>dest_p. \<lbrace>?B7 dest_p\<rbrace> gets cdt \<lbrace>?B8 dest_p\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets (\<lambda>s. cdt s cref) \<lbrace>?B7\<rbrace>
 5. \<And>s. (valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at ((=) NullCap) cref and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (4 subgoals):
 1. \<And>dest_p cdt. \<lbrace>?B8 dest_p cdt\<rbrace> do s <- get;
put (s\<lparr>cdt := cdt(cref \<mapsto> p)\<rparr>)
od \<lbrace>\<lambda>y s. valid_arch_caps (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') cref (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> vs_cap_ref cap' = Some vref \<longrightarrow> vs_cap_ref (default_cap tp oref sz dev) = Some vref \<and> obj_refs (default_cap tp oref sz dev) = obj_refs cap' \<or> \<not> is_final_cap' cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> \<not> reachable_pg_cap cap' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs cap'. (vref, oref) \<notin> vs_lookup_pages (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))))) r (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>))) \<and> (is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<longrightarrow> (\<forall>oldcap. caps_of_state (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) cref = Some oldcap \<longrightarrow> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap oldcap \<or> is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap oldcap \<longrightarrow> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<longrightarrow> obj_refs oldcap \<noteq> obj_refs (default_cap tp oref sz dev)) \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap' \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap') \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap' = None)) ptr' (s\<lparr>is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<longrightarrow> ptr' = cref))\<rbrace>
 2. \<And>dest_p. \<lbrace>?B7 dest_p\<rbrace> gets cdt \<lbrace>?B8 dest_p\<rbrace>
 3. \<lbrace>?Q6\<rbrace> gets (\<lambda>s. cdt s cref) \<lbrace>?B7\<rbrace>
 4. \<And>s. (valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\<lambda>s. \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at ((=) NullCap) cref and (\<lambda>y. tp \<noteq> ArchObject ASIDPoolObj)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_caps s \<and> s \<turnstile> default_cap tp oref sz dev \<and> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) (a, b) s) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> cte_wp_at ((=) NullCap) cref s \<and> tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> (\<forall>x xa. vs_cap_ref xa = Some x \<longrightarrow> cte_wp_at ((=) xa) cref s \<longrightarrow> vs_cap_ref (default_cap tp oref sz dev) = Some x \<and> obj_refs (default_cap tp oref sz dev) = obj_refs xa \<or> \<not> is_final_cap' xa (s\<lparr>cdt := \<lambda>a. if a = cref then Some p else cdt s a, is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> \<not> reachable_pg_cap xa (s\<lparr>cdt := \<lambda>a. if a = cref then Some p else cdt s a, is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<or> (\<forall>oref\<in>obj_refs xa. (x, oref) \<notin> vs_lookup_pages s)) \<and> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>cdt := \<lambda>a. if a = cref then Some p else cdt s a, is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>oldcap. caps_of_state s cref = Some oldcap \<and> (is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap oldcap \<and> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<and> obj_refs oldcap = obj_refs (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap oldcap \<and> (cap_asid (default_cap tp oref sz dev) = None \<longrightarrow> cap_asid oldcap = None) \<and> obj_refs oldcap = obj_refs (default_cap tp oref sz dev))) \<or> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap' \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap') \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap' = None)) (a, b) s \<longrightarrow> (a, b) = cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>cdt := \<lambda>a. if a = cref then Some p else cdt s a, is_original_cap := (is_original_cap s)(cref := True)\<rparr>) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (default_cap tp oref sz dev) {cref} (s\<lparr>cdt := \<lambda>a. if a = cref then Some p else cdt s a, is_original_cap := (is_original_cap s)(cref := True)\<rparr>)
 2. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = obj_refs (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 2. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = obj_refs (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; \<exists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 2. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = obj_refs (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 3. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap x. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = {x}; caps_of_state s (a, b) = Some cap; obj_refs (default_cap tp oref sz dev) = {x}; \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> x \<notin> obj_refs cap; \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) x s\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 2. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = obj_refs (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 3. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; (a, b) \<noteq> cref; obj_refs cap = obj_refs (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref (default_cap tp oref sz dev)
 2. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) \<and> (\<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> \<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<exists>y. cap_asid (default_cap tp oref sz dev) = Some y) \<or> (\<forall>r\<in>obj_refs (default_cap tp oref sz dev). obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)
 2. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> \<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj\<rbrakk> \<Longrightarrow> \<not> is_pt_cap (default_cap tp oref sz dev) \<and> \<not> is_pd_cap (default_cap tp oref sz dev) \<or> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> obj_refs cap = obj_refs (default_cap tp oref sz dev) \<and> (is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap) \<and> (cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None)) \<longrightarrow> (a, b) = cref) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = obj_refs (default_cap tp oref sz dev); is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None\<rbrakk> \<Longrightarrow> (a, b) = cref proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = obj_refs (default_cap tp oref sz dev); is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None; \<exists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (a, b) = cref
 2. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = obj_refs (default_cap tp oref sz dev); is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (a, b) = cref proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap x. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = {x}; is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None; obj_refs (default_cap tp oref sz dev) = {x}; \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> x \<notin> obj_refs cap; \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) x s\<rbrakk> \<Longrightarrow> (a, b) = cref
 2. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = obj_refs (default_cap tp oref sz dev); is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (a, b) = cref proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>valid_arch_caps s; s \<turnstile> default_cap tp oref sz dev; \<forall>r\<in>obj_refs (default_cap tp oref sz dev). (\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> r \<notin> obj_refs cap) \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s; caps_of_state s cref = Some NullCap; tp \<noteq> ArchObject ASIDPoolObj; is_pt_cap (default_cap tp oref sz dev) \<or> is_pd_cap (default_cap tp oref sz dev); caps_of_state s (a, b) = Some cap; obj_refs cap = obj_refs (default_cap tp oref sz dev); is_pd_cap (default_cap tp oref sz dev) \<and> is_pd_cap cap \<or> is_pt_cap (default_cap tp oref sz dev) \<and> is_pt_cap cap; cap_asid (default_cap tp oref sz dev) = None \<or> cap_asid cap = None; \<nexists>x. x \<in> obj_refs cap\<rbrakk> \<Longrightarrow> (a, b) = cref proof (prove)
goal:
No subgoals!