theory ArchFinalise_AI

lemma replaceable_reset_pt:
  "\<lbrakk>cap = PageTableCap p m \<and>
   cte_wp_at ((=) (ArchObjectCap cap)) slot s \<and>
   (\<forall>vs. vs_cap_ref (ArchObjectCap cap) = Some vs \<longrightarrow> \<not> (vs \<unrhd> p) s) \<and>
   is_final_cap' (ArchObjectCap cap) s \<and>
   obj_at (empty_table (set (second_level_tables (arch_state s)))) p s\<rbrakk> \<Longrightarrow>
   replaceable s slot (ArchObjectCap (PageTableCap p None))
                      (ArchObjectCap cap)" apply (elim conjE) apply (cases m, simp_all add: replaceable_def gen_obj_refs_def cap_range_def
                                is_cap_simps tcb_cap_valid_pagetable) apply (rule conjI) apply (frule is_final_cap_pt_asid_eq) defer apply clarsimp apply (drule cte_wp_at_obj_refs_singleton_page_table) apply (erule exE) apply (drule_tac x="asid" in is_final_cap_pt_asid_eq) apply (drule final_cap_pt_slot_eq) apply simp_all apply (rule_tac
    cap="(cap.ArchObjectCap cap)"
    in  no_cap_to_obj_with_diff_ref_finalI) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = PageTableCap p m \<and> cte_wp_at ((=) (ArchObjectCap cap)) slot s \<and> (\<forall>vs. vs_cap_ref (ArchObjectCap cap) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s) \<and> is_final_cap' (ArchObjectCap cap) s \<and> obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<Longrightarrow> replaceable s slot (ArchObjectCap (PageTableCap p None)) (ArchObjectCap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = PageTableCap p m; cte_wp_at ((=) (ArchObjectCap cap)) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap cap) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap cap) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s\<rbrakk> \<Longrightarrow> replaceable s slot (ArchObjectCap (PageTableCap p None)) (ArchObjectCap cap) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s \<and> ((\<exists>y. cap_asid (ArchObjectCap (PageTableCap p (Some a))) = Some y) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (a, b) s \<longrightarrow> (a, b) = slot)) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a\<rbrakk> \<Longrightarrow> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap p (Some a))) = Some y) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (a, b) s \<longrightarrow> (a, b) = slot) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a\<rbrakk> \<Longrightarrow> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap p (Some a))) = Some y) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (a, b) s \<longrightarrow> (a, b) = slot) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a\<rbrakk> \<Longrightarrow> (\<exists>y. cap_asid (ArchObjectCap (PageTableCap p (Some a))) = Some y) \<longrightarrow> (\<forall>a b. cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (a, b) s \<longrightarrow> (a, b) = slot)
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (2 subgoals):
 1. \<And>b y aa ba. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some (y, b)))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at (\<lambda>cap'. obj_refs cap' = {p} \<and> (\<exists>p asid. cap' = ArchObjectCap (PageTableCap p asid))) (aa, ba) s\<rbrakk> \<Longrightarrow> (aa, ba) = slot
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (2 subgoals):
 1. \<And>b y aa ba. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some (y, b)))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); \<exists>asid. cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s\<rbrakk> \<Longrightarrow> (aa, ba) = slot
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (2 subgoals):
 1. \<And>b y aa ba asid. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some (y, b)))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s\<rbrakk> \<Longrightarrow> (aa, ba) = slot
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (2 subgoals):
 1. \<And>b y aa ba asid. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s; is_final_cap' (ArchObjectCap (PageTableCap p asid)) s\<rbrakk> \<Longrightarrow> (aa, ba) = slot
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (4 subgoals):
 1. \<And>b y aa ba asid. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap (PageTableCap p (?asid'39 b y aa ba asid)))) (?slot39 b y aa ba asid) s
 2. \<And>b y aa ba asid. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap (PageTableCap p (?asid''39 b y aa ba asid)))) (?slot'39 b y aa ba asid) s
 3. \<And>b y aa ba asid. \<lbrakk>cap = PageTableCap p (Some (y, b)); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some (y, b))))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some (y, b)))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some (y, b); cte_wp_at ((=) (ArchObjectCap (PageTableCap p asid))) (aa, ba) s; ?slot'39 b y aa ba asid = ?slot39 b y aa ba asid\<rbrakk> \<Longrightarrow> (aa, ba) = slot
 4. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref (ArchObjectCap (PageTableCap p None)) {slot} s proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap cap)) slot s
 2. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> is_final_cap' (ArchObjectCap cap) s
 3. \<And>a. \<lbrakk>cap = PageTableCap p (Some a); cte_wp_at ((=) (ArchObjectCap (PageTableCap p (Some a)))) slot s; \<forall>vs. vs_cap_ref (ArchObjectCap (PageTableCap p (Some a))) = Some vs \<longrightarrow> (vs, p) \<notin> vs_lookup_pages s; is_final_cap' (ArchObjectCap (PageTableCap p (Some a))) s; obj_at (empty_table (set (second_level_tables (arch_state s)))) p s; m = Some a; is_final_cap' (ArchObjectCap (PageTableCap p (?x23 a))) s\<rbrakk> \<Longrightarrow> obj_refs (ArchObjectCap (PageTableCap p None)) = obj_refs (ArchObjectCap cap) proof (prove)
goal:
No subgoals!