theory ArchFinalise_AI

lemma page_table_mapped_wp_weak:
  "\<lbrace>\<lambda>s. Q None s \<and> (\<forall>x. Q (Some x) s)\<rbrace>
     page_table_mapped asid vptr pt
   \<lbrace>Q\<rbrace>"
  (is "\<lbrace>?P\<rbrace> page_table_mapped asid vptr pt \<lbrace>Q\<rbrace>") apply (simp add: page_table_mapped_def) apply (rule hoare_pre) apply (wp get_pde_wp | wpc)+ apply (rule_tac Q'="\<lambda>_. ?P" in hoare_post_imp_R) apply wp apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q None s \<and> (\<forall>x. Q (Some x) s)\<rbrace> page_table_mapped asid vptr pt \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q None s \<and> (\<forall>x. Q (Some x) s)\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = 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>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = 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>Q\<rbrace>
 2. \<And>s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'54\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd s. \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> Q (if addrFromPPtr pt = x then Some pd else None) s) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> Q None s)\<rbrace>, -
 2. \<And>s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> Q None s \<and> ?P'54 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'54\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>_ s. Q None s \<and> (\<forall>x. Q (Some x) s)\<rbrace>, -
 2. \<And>rv s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot rv vptr && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> Q (if addrFromPPtr pt = x then Some rv else None) s) \<and> (\<forall>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> Q None s)
 3. \<And>s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> Q None s \<and> ?P'54 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot rv vptr && ~~ mask pd_bits) s \<longrightarrow> (pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> Q (if addrFromPPtr pt = x then Some rv else None) s) \<and> (\<forall>x xa xb xc. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> Q None s) \<and> (\<forall>x xa xb. pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> Q None s)
 2. \<And>s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> Q None s \<and> Q None s \<and> (\<forall>x. Q (Some x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. Q None s \<and> (\<forall>x. Q (Some x) s) \<Longrightarrow> Q None s \<and> Q None s \<and> (\<forall>x. Q (Some x) s) proof (prove)
goal:
No subgoals!