theory PageTableDuplicates

lemma unmapPageTable_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
   unmapPageTable aa ba word
   \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:unmapPageTable_def pageTableMapped_def) apply (wpsimp wp: storePDE_no_duplicates' getPDE_wp) apply (rule hoare_post_imp_R[where Q' = "\<lambda>r s. vs_valid_duplicates' (ksPSpace s)"]) apply wp apply (clarsimp simp: ko_wp_at'_def obj_at'_real_def projectKO_opt_pde) apply (clarsimp simp: vs_entry_align_def
                   split: arch_kernel_object.splits pde.split kernel_object.splits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> unmapPageTable aa ba word \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do maybePD <- doE pd <- findPDForASID aa;
liftE (getObject (lookup_pd_slot pd ba)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr word then Some pd else None)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE <catch> (\<lambda>_. return None);
case maybePD of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- storePDE (lookup_pd_slot pd ba) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot pd ba) (addrFromPPtr (lookup_pd_slot pd ba)));
flushTable pd aa ba
od
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'151\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd s. \<forall>ko. ko_at' ko (lookup_pd_slot pd ba) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> (\<forall>x. (x = addrFromPPtr word \<longrightarrow> (\<exists>x xa. ko = ARM_H.PageTablePDE (addrFromPPtr word) x xa) \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot pd ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> (x \<noteq> addrFromPPtr word \<longrightarrow> (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))) \<and> ((\<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf) \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> ((\<exists>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))\<rbrace>, -
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (None = None \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ?P'92 s) \<and> (\<forall>x. None = Some x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot x ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> ?P'151 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'151\<rbrace> findPDForASID aa \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, -
 2. \<And>rv s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot rv ba) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> (\<forall>x. (x = addrFromPPtr word \<longrightarrow> (\<exists>x xa. ko = ARM_H.PageTablePDE (addrFromPPtr word) x xa) \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot rv ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> (x \<noteq> addrFromPPtr word \<longrightarrow> (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))) \<and> ((\<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf) \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> ((\<exists>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))
 3. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (None = None \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ?P'92 s) \<and> (\<forall>x. None = Some x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot x ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> ?P'151 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot rv ba) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> (\<forall>x. (x = addrFromPPtr word \<longrightarrow> (\<exists>x xa. ko = ARM_H.PageTablePDE (addrFromPPtr word) x xa) \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot rv ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> (x \<noteq> addrFromPPtr word \<longrightarrow> (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))) \<and> ((\<exists>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf) \<longrightarrow> vs_valid_duplicates' (ksPSpace s)) \<and> ((\<exists>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe) \<longrightarrow> vs_valid_duplicates' (ksPSpace s))
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (None = None \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ?P'92 s) \<and> (\<forall>x. None = Some x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot x ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> vs_valid_duplicates' (ksPSpace s) proof (prove)
goal (2 subgoals):
 1. \<And>rv s koa x xa. \<lbrakk>vs_valid_duplicates' (ksPSpace s); ksPSpace s (lookup_pd_slot rv ba) = Some koa; is_aligned (lookup_pd_slot rv ba) (objBitsKO koa); (case koa of KOArch (KOPDE xa) \<Rightarrow> Some xa | KOArch _ \<Rightarrow> None | _ \<Rightarrow> None) = Some (ARM_H.PageTablePDE (addrFromPPtr word) x xa); ps_clear (lookup_pd_slot rv ba) (objBitsKO koa) s\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0 \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (None = None \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ?P'92 s) \<and> (\<forall>x. None = Some x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot x ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> vs_valid_duplicates' (ksPSpace s) proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> (None = None \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ?P'92 s) \<and> (\<forall>x. None = Some x \<longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) (lookup_pd_slot x ba) s \<and> vs_entry_align (KOArch (KOPDE ARM_H.InvalidPDE)) = 0) \<and> vs_valid_duplicates' (ksPSpace s) proof (prove)
goal:
No subgoals!