theory Finalise_C

lemma pageTableMapped_pd:
  "\<lbrace>\<top>\<rbrace> pageTableMapped asid vaddr ptPtr
   \<lbrace>\<lambda>rv s. case rv of Some x \<Rightarrow> page_directory_at' x s | _ \<Rightarrow> True\<rbrace>" apply (simp add: pageTableMapped_def) apply (rule hoare_pre) apply (wp getPDE_wp hoare_vcg_all_lift_R | wpc)+ apply (rule hoare_post_imp_R, rule findPDForASID_page_directory_at'_simple) apply (clarsimp split: if_split) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> pageTableMapped asid vaddr ptPtr \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr ptPtr then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE <catch> (\<lambda>_. return None) \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr ptPtr then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE <catch> (\<lambda>_. return None) \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrace>?P62 ko\<rbrace> findPDForASID asid \<lbrace>\<lambda>rv s. ko_at' ko (lookup_pd_slot rv vaddr) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb. ko = ARM_H.PageTablePDE x xa xb \<longrightarrow> (case if x = addrFromPPtr ptPtr then Just rv else Nothing of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s))\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s) \<and> (\<forall>x. ?P62 x s) proof (prove)
goal (2 subgoals):
 1. \<And>ko rv s. page_directory_at' rv s \<Longrightarrow> ko_at' ko (lookup_pd_slot rv vaddr) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb. ko = ARM_H.PageTablePDE x xa xb \<longrightarrow> (case if x = addrFromPPtr ptPtr then Just rv else Nothing of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s)) \<and> (\<forall>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s))
 2. \<And>s. True \<Longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s) \<and> (\<forall>x. True) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (case None of None \<Rightarrow> True | Some x \<Rightarrow> page_directory_at' x s) \<and> (\<forall>x. True) proof (prove)
goal:
No subgoals!