theory Finalise_DR

lemma page_table_mapped_stable[wp]:
  "\<lbrace>(=) s\<rbrace> page_table_mapped a b w \<lbrace>\<lambda>r. (=) s\<rbrace>" apply (simp add:page_table_mapped_def) apply (wp|wpc)+ apply (simp add:get_pde_def) apply wp apply (simp add:find_pd_for_asid_def) apply (wp|wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> page_table_mapped a b w \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<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\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>pd. \<lbrace>?B3 pd\<rbrace> get_pde (lookup_pd_slot pd b) \<lbrace>\<lambda>x sa. (x = InvalidPDE \<longrightarrow> s = sa) \<and> (\<forall>xa xb xc. x = PageTablePDE xa xb xc \<longrightarrow> s = sa) \<and> (\<forall>xa xb xc xd. x = SectionPDE xa xb xc xd \<longrightarrow> s = sa) \<and> (\<forall>xa xb xc. x = SuperSectionPDE xa xb xc \<longrightarrow> s = sa)\<rbrace>
 2. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>sa. s = sa \<Longrightarrow> ?Q sa proof (prove)
goal (3 subgoals):
 1. \<And>pd. \<lbrace>?B3 pd\<rbrace> do pda <- get_pd (lookup_pd_slot pd b && ~~ mask pd_bits);
return (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)))
od \<lbrace>\<lambda>x sa. (x = InvalidPDE \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc. x = PageTablePDE xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc xd. x = SectionPDE xa xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc. x = SuperSectionPDE xa xb xc) \<longrightarrow> s = sa)\<rbrace>
 2. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>sa. s = sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pd sa. \<forall>pda. ako_at (arch_kernel_obj.PageDirectory pda) (lookup_pd_slot pd b && ~~ mask pd_bits) sa \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> s = sa)\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>sa. s = sa \<Longrightarrow> ?Q sa proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE y <- assertE (0 < a);
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>\<lambda>pd sa. \<forall>pda. ako_at (arch_kernel_obj.PageDirectory pda) (lookup_pd_slot pd b && ~~ mask pd_bits) sa \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = SectionPDE x xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd b && mask pd_bits >> 2)) = SuperSectionPDE x xa xb) \<longrightarrow> s = sa)\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>sa. s = sa \<Longrightarrow> ?Q sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. s = sa \<Longrightarrow> 0 < a \<longrightarrow> ((arm_asid_table \<circ> arch_state) sa (asid_high_bits_of a) = None \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) sa (asid_high_bits_of a) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x sa \<longrightarrow> True) \<and> (\<forall>pool. ako_at (ASIDPool pool) x sa \<longrightarrow> (pool (UCAST(32 \<rightarrow> 10) a) = None \<longrightarrow> s = sa \<and> True) \<and> (\<forall>x. pool (UCAST(32 \<rightarrow> 10) a) = Some x \<longrightarrow> (\<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot x b && ~~ mask pd_bits) sa \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)) = PageTablePDE xa xb xc) \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc xd. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)) = SectionPDE xa xb xc xd) \<longrightarrow> s = sa) \<and> ((\<exists>xa xb xc. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot x b && mask pd_bits >> 2)) = SuperSectionPDE xa xb xc) \<longrightarrow> s = sa))))) proof (prove)
goal:
No subgoals!