theory VSpace_R

lemma pteCheckIfMapped_corres:
  "corres (=) (pte_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (pte_check_if_mapped slot) (pteCheckIfMapped slot)" apply (simp add: pte_check_if_mapped_def pteCheckIfMapped_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_master_pte_corres', simplified]) apply (rule corres_return[where P="pte_at slot" and
                          P'="pspace_aligned' and pspace_distinct'", THEN iffD2]) apply (clarsimp simp: pte_relation'_def split: ) apply (case_tac pt, simp_all)[1] apply wp+ apply (simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (pte_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (pte_check_if_mapped slot) (pteCheckIfMapped slot) proof (prove)
goal (1 subgoal):
 1. corres (=) (pte_at slot) ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') (do pt <- get_master_pte slot;
return (pt \<noteq> ARM_A.InvalidPTE)
od) (do pt <- getObject slot;
return (pt \<noteq> ARM_H.InvalidPTE)
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do pt <- get_master_pte slot;
return (pt \<noteq> ARM_A.InvalidPTE)
od) (do pt <- getObject slot;
return (pt \<noteq> ARM_H.InvalidPTE)
od)
 2. \<And>s. pte_at slot s \<Longrightarrow> ?Q s
 3. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>pt pta. pte_relation' pt pta \<Longrightarrow> corres (=) (?R4 pt) (?R'4 pta) (return (pt \<noteq> ARM_A.InvalidPTE)) (return (pta \<noteq> ARM_H.InvalidPTE))
 2. \<lbrace>?Q4\<rbrace> get_master_pte slot \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>?R'4\<rbrace>
 4. \<And>s. pte_at slot s \<Longrightarrow> (pte_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>pt pta. pte_relation' pt pta \<Longrightarrow> (\<exists>s s'. pte_at slot s \<and> (pspace_aligned' and pspace_distinct') s' \<and> (s, s') \<in> state_relation) \<longrightarrow> (pt \<noteq> ARM_A.InvalidPTE) = (pta \<noteq> ARM_H.InvalidPTE)
 2. \<lbrace>?Q4\<rbrace> get_master_pte slot \<lbrace>\<lambda>pt. pte_at slot\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pta. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. pte_at slot s \<Longrightarrow> (pte_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>pt pta s s'. \<lbrakk>ARM_A.rec_pte (\<lambda>x. x = ARM_H.InvalidPTE) (\<lambda>ptr atts rghts x. x = ARM_H.LargePagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts)) (\<lambda>ptr atts rghts x. x = ARM_H.SmallPagePTE ptr (PageCacheable \<in> atts) (Global \<in> atts) (XNever \<in> atts) (vmrights_map rghts)) pt pta; pte_at slot s; pspace_aligned' s'; pspace_distinct' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pt = ARM_A.InvalidPTE) = (pta = ARM_H.InvalidPTE)
 2. \<lbrace>?Q4\<rbrace> get_master_pte slot \<lbrace>\<lambda>pt. pte_at slot\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pta. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. pte_at slot s \<Longrightarrow> (pte_at slot and ?Q4) s
 5. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_master_pte slot \<lbrace>\<lambda>pt. pte_at slot\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getObject slot \<lbrace>\<lambda>pta. pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. pte_at slot s \<Longrightarrow> (pte_at slot and ?Q4) s
 4. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. pte_at slot s \<Longrightarrow> (pte_at slot and pte_at slot) s
 2. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (pspace_aligned' and pspace_distinct')) s proof (prove)
goal:
No subgoals!