theory Finalise_DR

lemma pd_pt_relation_page_table_mapped_wp:
  "\<lbrace>page_table_at w\<rbrace> page_table_mapped a b w
      \<lbrace>\<lambda>r s. (case r of Some pd \<Rightarrow> pd_pt_relation
    (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s | _ \<Rightarrow> True)\<rbrace>" apply (simp add:page_table_mapped_def) apply wp apply wpc apply (clarsimp simp:validE_def valid_def return_def returnOk_def) apply wp+ apply simp apply (simp add:get_pde_def) apply wp apply (simp add:validE_def) apply (rule hoare_strengthen_post[where Q="\<lambda>rv. page_table_at w"]) apply wp apply (clarsimp simp:pd_pt_relation_def obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at (AArch APageTable) w\<rbrace> page_table_mapped a b w \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at (AArch APageTable) w\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None) \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>pd x. \<lbrace>?B4 pd x\<rbrace> case x of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pd else None) | _ \<Rightarrow> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 2. \<And>pd. \<lbrace>?B3 pd\<rbrace> liftE (get_pde (lookup_pd_slot pd b)) \<lbrace>?B4 pd\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 4. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>pd x. x = InvalidPDE \<Longrightarrow> \<lbrace>?R26 pd x\<rbrace> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 2. \<And>pd x x21 x22 x23. x = PageTablePDE x21 x22 x23 \<Longrightarrow> \<lbrace>?R27 pd x x21 x22 x23\<rbrace> returnOk (if addrFromPPtr w = x21 then Some pd else None) \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<And>pd x x31 x32 x33 x34. x = SectionPDE x31 x32 x33 x34 \<Longrightarrow> \<lbrace>?R28 pd x x31 x32 x33 x34\<rbrace> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 4. \<And>pd x x41 x42 x43. x = SuperSectionPDE x41 x42 x43 \<Longrightarrow> \<lbrace>?R29 pd x x41 x42 x43\<rbrace> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 5. \<And>pd. \<lbrace>?B3 pd\<rbrace> liftE (get_pde (lookup_pd_slot pd b)) \<lbrace>\<lambda>x s. (x = InvalidPDE \<longrightarrow> ?R26 pd x s) \<and> (\<forall>xa xb xc. x = PageTablePDE xa xb xc \<longrightarrow> ?R27 pd x xa xb xc s) \<and> (\<forall>xa xb xc xd. x = SectionPDE xa xb xc xd \<longrightarrow> ?R28 pd x xa xb xc xd s) \<and> (\<forall>xa xb xc. x = SuperSectionPDE xa xb xc \<longrightarrow> ?R29 pd x xa xb xc s)\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 6. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 7. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>pd x x21 x22 x23. x = PageTablePDE x21 x22 x23 \<Longrightarrow> \<lbrace>?R27 pd x x21 x22 x23\<rbrace> returnOk (if addrFromPPtr w = x21 then Some pd else None) \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 2. \<And>pd x x31 x32 x33 x34. x = SectionPDE x31 x32 x33 x34 \<Longrightarrow> \<lbrace>?R28 pd x x31 x32 x33 x34\<rbrace> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<And>pd x x41 x42 x43. x = SuperSectionPDE x41 x42 x43 \<Longrightarrow> \<lbrace>?R29 pd x x41 x42 x43\<rbrace> returnOk None \<lbrace>\<lambda>r s. case r of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 4. \<And>pd. \<lbrace>?B3 pd\<rbrace> liftE (get_pde (lookup_pd_slot pd b)) \<lbrace>\<lambda>x s. (x = InvalidPDE \<longrightarrow> ?R26 pd x s) \<and> (\<forall>xa xb xc. x = PageTablePDE xa xb xc \<longrightarrow> ?R27 pd x xa xb xc s) \<and> (\<forall>xa xb xc xd. x = SectionPDE xa xb xc xd \<longrightarrow> ?R28 pd x xa xb xc xd s) \<and> (\<forall>xa xb xc. x = SuperSectionPDE xa xb xc \<longrightarrow> ?R29 pd x xa xb xc s)\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 5. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 6. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B3 x\<rbrace> get_pde (lookup_pd_slot x b) \<lbrace>\<lambda>r s. (r = InvalidPDE \<longrightarrow> True) \<and> (\<forall>xa xb xc. r = PageTablePDE xa xb xc \<longrightarrow> (case if addrFromPPtr w = xa then Some x else None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s)) \<and> (\<forall>x xa xb xc. r = SectionPDE x xa xb xc \<longrightarrow> (case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s)) \<and> (\<forall>x xa xb. r = SuperSectionPDE x xa xb \<longrightarrow> (case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s))\<rbrace>
 2. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B3 x\<rbrace> get_pde (lookup_pd_slot x b) \<lbrace>\<lambda>r s. (\<exists>x xa. r = PageTablePDE (addrFromPPtr w) x xa) \<longrightarrow> pd_pt_relation (lookup_pd_slot x b && ~~ mask pd_bits) w (lookup_pd_slot x b) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B3 x\<rbrace> do pd <- get_pd (lookup_pd_slot x b && ~~ mask pd_bits);
return (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)))
od \<lbrace>\<lambda>r s. (\<exists>x xa. r = PageTablePDE (addrFromPPtr w) x xa) \<longrightarrow> pd_pt_relation (lookup_pd_slot x b && ~~ mask pd_bits) w (lookup_pd_slot x b) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 3. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>x s. \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot x b && ~~ mask pd_bits) s \<longrightarrow> (\<exists>xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)) = PageTablePDE (addrFromPPtr w) xa xb) \<longrightarrow> pd_pt_relation (lookup_pd_slot x b && ~~ mask pd_bits) w (lookup_pd_slot x b) s\<rbrace>, \<lbrace>\<lambda>x a. case None of None \<Rightarrow> True | Some pd \<Rightarrow> pd_pt_relation (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) a\<rbrace>
 2. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> (\<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot r b && ~~ mask pd_bits) s \<longrightarrow> (\<exists>x xa. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot r b && mask pd_bits >> 2)) = PageTablePDE (addrFromPPtr w) x xa) \<longrightarrow> pd_pt_relation (lookup_pd_slot r b && ~~ mask pd_bits) w (lookup_pd_slot r b) s)\<rbrace>
 2. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>rv. typ_at (AArch APageTable) w\<rbrace>
 2. \<And>rv s. typ_at (AArch APageTable) w s \<Longrightarrow> \<forall>r. rv = Inr r \<longrightarrow> (\<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot r b && ~~ mask pd_bits) s \<longrightarrow> (\<exists>x xa. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot r b && mask pd_bits >> 2)) = PageTablePDE (addrFromPPtr w) x xa) \<longrightarrow> pd_pt_relation (lookup_pd_slot r b && ~~ mask pd_bits) w (lookup_pd_slot r b) s)
 3. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. typ_at (AArch APageTable) w s \<Longrightarrow> \<forall>r. rv = Inr r \<longrightarrow> (\<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot r b && ~~ mask pd_bits) s \<longrightarrow> (\<exists>x xa. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot r b && mask pd_bits >> 2)) = PageTablePDE (addrFromPPtr w) x xa) \<longrightarrow> pd_pt_relation (lookup_pd_slot r b && ~~ mask pd_bits) w (lookup_pd_slot r b) s)
 2. \<And>s. typ_at (AArch APageTable) w s \<Longrightarrow> typ_at (AArch APageTable) w s proof (prove)
goal:
No subgoals!