theory ArchFinalise_AI

lemma arch_finalise_pt_pd_empty:
  "\<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (cap.ArchObjectCap acap) and
    K ((is_pt_cap (cap.ArchObjectCap acap) \<or> is_pd_cap (cap.ArchObjectCap acap)) \<and> aobj_ref acap = Some ptr)\<rbrace>
  arch_finalise_cap acap final
  \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace>" apply (rule hoare_gen_asm) apply clarsimp apply (erule disjE) apply (clarsimp simp: is_cap_simps arch_finalise_cap_def) apply (rule hoare_pre) apply (wp unmap_page_table_empty | wpc)+ apply clarsimp apply (clarsimp simp: is_cap_simps arch_finalise_cap_def) apply (rule hoare_pre) apply (wp unmap_page_table_empty delete_asid_empty_table_pd | wpc)+ apply (clarsimp simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap) and K ((is_pt_cap (ArchObjectCap acap) \<or> is_pd_cap (ArchObjectCap acap)) \<and> aobj_ref acap = Some ptr)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_pt_cap (ArchObjectCap acap) \<or> is_pd_cap (ArchObjectCap acap)) \<and> aobj_ref acap = Some ptr \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_pt_cap (ArchObjectCap acap) \<or> is_pd_cap (ArchObjectCap acap); aobj_ref acap = Some ptr\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>aobj_ref acap = Some ptr; is_pt_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace>
 2. \<lbrakk>aobj_ref acap = Some ptr; is_pd_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asid. acap = PageTableCap ptr asid \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageTableCap ptr asid))\<rbrace> case asid of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace>
 2. \<lbrakk>aobj_ref acap = Some ptr; is_pd_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>asid. acap = PageTableCap ptr asid \<Longrightarrow> \<lbrace>?Q13 asid\<rbrace> case asid of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace>
 2. \<And>asid s. \<lbrakk>acap = PageTableCap ptr asid; ((\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageTableCap ptr asid))) s\<rbrakk> \<Longrightarrow> ?Q13 asid s
 3. \<lbrakk>aobj_ref acap = Some ptr; is_pd_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asid s. \<lbrakk>acap = PageTableCap ptr asid; ((\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageTableCap ptr asid))) s\<rbrakk> \<Longrightarrow> (asid = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) \<and> (\<forall>x. asid = Some x \<longrightarrow> (\<forall>xa xb. x = (xa, xb) \<longrightarrow> (final = True \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) \<and> (final = False \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s)))
 2. \<lbrakk>aobj_ref acap = Some ptr; is_pd_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>aobj_ref acap = Some ptr; is_pd_cap (ArchObjectCap acap)\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap acap)\<rbrace> arch_finalise_cap acap final \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asid. acap = PageDirectoryCap ptr asid \<Longrightarrow> \<lbrace>(\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageDirectoryCap ptr asid))\<rbrace> case asid of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asid. acap = PageDirectoryCap ptr asid \<Longrightarrow> \<lbrace>?Q60 asid\<rbrace> case asid of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s\<rbrace>
 2. \<And>asid s. \<lbrakk>acap = PageDirectoryCap ptr asid; ((\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageDirectoryCap ptr asid))) s\<rbrakk> \<Longrightarrow> ?Q60 asid s proof (prove)
goal (1 subgoal):
 1. \<And>asid s. \<lbrakk>acap = PageDirectoryCap ptr asid; ((\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) and valid_cap (ArchObjectCap (PageDirectoryCap ptr asid))) s\<rbrakk> \<Longrightarrow> (asid = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) \<and> (\<forall>x. asid = Some x \<longrightarrow> (final = True \<longrightarrow> typ_at (AArch APageDirectory) ptr s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s) \<and> (final = False \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) ptr s)) proof (prove)
goal:
No subgoals!