theory ArchAcc_R

lemma ensureSafeMapping_corres [corres]:
  "mapping_map m m' \<Longrightarrow>
  corres (ser \<oplus> dc) (valid_mapping_entries m)
                    (pspace_aligned' and pspace_distinct'
                    and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
                    (ensure_safe_mapping m) (ensureSafeMapping m')" unfolding mapping_map_def ensureSafeMapping_def apply (cases m; cases m'; simp;
         match premises in "(_ \<otimes> (=)) p p'" for p p' \<Rightarrow> \<open>cases "fst p"; cases "fst p'"\<close>; clarsimp) by (corresKsimp corresK: mapME_x_corresK_inv
                           wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp;
            auto simp add: valid_mapping_entries_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapping_map m m' \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries m) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (ensure_safe_mapping m) (ensureSafeMapping m') proof (prove)
goal (1 subgoal):
 1. (pte_relation' \<otimes> (=) \<oplus> pde_relation' \<otimes> (=)) m m' \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries m) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (ensure_safe_mapping m) (case m' of Inl (ARM_H.InvalidPTE, x) \<Rightarrow> returnOk () | Inl (ARM_H.LargePagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.SmallPagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inl (ARM_H.SmallPagePTE xa xaa xb xc xd, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pte <- withoutFailure $ getObject slot;
case pte of ARM_H.LargePagePTE word bool1 bool2 bool3 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.InvalidPDE, x) \<Rightarrow> returnOk () | Inr (ARM_H.PageTablePDE xa xaa xb, x) \<Rightarrow> haskell_fail [] | Inr (ARM_H.SectionPDE xa xaa xb xc xd xe xf, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.PageTablePDE word1 bool word2 \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | ARM_H.SuperSectionPDE word bool1 bool2 bool3 bool4 vmrights \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst | _ \<Rightarrow> returnOk ()
odE) | Inr (ARM_H.SuperSectionPDE xa xaa xb xc xd xe, x) \<Rightarrow> forME_x x (\<lambda>slot. doE pde <- withoutFailure $ getObject slot;
case pde of ARM_H.InvalidPDE \<Rightarrow> returnOk () | ARM_H.SuperSectionPDE x xa xb xc xd xe \<Rightarrow> returnOk () | _ \<Rightarrow> throw Fault_H.syscall_error.DeleteFirst
odE)) proof (prove)
goal (7 subgoals):
 1. \<And>b. \<lbrakk>m = Inl (ARM_A.InvalidPTE, b); m' = Inl (ARM_H.InvalidPTE, b)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inl (ARM_A.InvalidPTE, b))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (returnOk ()) (returnOk ())
 2. \<And>ba x21 x22 x23. \<lbrakk>m = Inl (ARM_A.LargePagePTE x21 x22 x23, ba); m' = Inl (ARM_H.LargePagePTE x21 (PageCacheable \<in> x22) (Global \<in> x22) (XNever \<in> x22) (vmrights_map x23), ba)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inl (ARM_A.LargePagePTE x21 x22 x23, ba))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (mapME_x (\<lambda>slot. liftE (get_master_pte slot) >>=E ARM_A.case_pte (returnOk ()) (\<lambda>x xa xb. returnOk ()) (\<lambda>word set1 set2. throwError ExceptionTypes_A.syscall_error.DeleteFirst)) ba) (mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>x xa xb xc xd. returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) ba)
 3. \<And>ba x31 x32 x33. \<lbrakk>m = Inl (ARM_A.SmallPagePTE x31 x32 x33, ba); m' = Inl (ARM_H.SmallPagePTE x31 (PageCacheable \<in> x32) (Global \<in> x32) (XNever \<in> x32) (vmrights_map x33), ba)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inl (ARM_A.SmallPagePTE x31 x32 x33, ba))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (mapME_x (\<lambda>slot. liftE (get_master_pte slot) >>=E ARM_A.case_pte (returnOk ()) (\<lambda>word set1 set2. throwError ExceptionTypes_A.syscall_error.DeleteFirst) (\<lambda>x xa xb. returnOk ())) ba) (mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pte (returnOk ()) (\<lambda>word bool1 bool2 bool3 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd. returnOk ())) ba)
 4. \<And>b. \<lbrakk>m = Inr (ARM_A.InvalidPDE, b); m' = Inr (ARM_H.InvalidPDE, b)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inr (ARM_A.InvalidPDE, b))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (returnOk ()) (returnOk ())
 5. \<And>ba x21 x22 x23. \<lbrakk>m = Inr (ARM_A.PageTablePDE x21 x22 x23, ba); m' = Inr (ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23, ba)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inr (ARM_A.PageTablePDE x21 x22 x23, ba))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) fail fail
 6. \<And>ba x31 x32 x33 x34. \<lbrakk>m = Inr (ARM_A.SectionPDE x31 x32 x33 x34, ba); m' = Inr (ARM_H.SectionPDE x31 (ParityEnabled \<in> x32) x33 (PageCacheable \<in> x32) (Global \<in> x32) (XNever \<in> x32) (vmrights_map x34), ba)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inr (ARM_A.SectionPDE x31 x32 x33 x34, ba))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E ARM_A.case_pde (returnOk ()) (\<lambda>word1 set word2. throwError ExceptionTypes_A.syscall_error.DeleteFirst) (\<lambda>x xa xb xc. returnOk ()) (\<lambda>word set1 set2. throwError ExceptionTypes_A.syscall_error.DeleteFirst)) ba) (mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe xf. returnOk ()) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst)) ba)
 7. \<And>ba x41 x42 x43. \<lbrakk>m = Inr (ARM_A.SuperSectionPDE x41 x42 x43, ba); m' = Inr (ARM_H.SuperSectionPDE x41 (ParityEnabled \<in> x42) (PageCacheable \<in> x42) (Global \<in> x42) (XNever \<in> x42) (vmrights_map x43), ba)\<rbrakk> \<Longrightarrow> corres (ser \<oplus> dc) (valid_mapping_entries (Inr (ARM_A.SuperSectionPDE x41 x42 x43, ba))) (pspace_aligned' and pspace_distinct' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E ARM_A.case_pde (returnOk ()) (\<lambda>word1 set word2. throwError ExceptionTypes_A.syscall_error.DeleteFirst) (\<lambda>word1 set1 word2 set2. throwError ExceptionTypes_A.syscall_error.DeleteFirst) (\<lambda>x xa xb. returnOk ())) ba) (mapME_x (\<lambda>slot. liftE (getObject slot) >>=E ARM_H.case_pde (returnOk ()) (\<lambda>word1 bool word2. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. throwError Fault_H.syscall_error.DeleteFirst) (\<lambda>x xa xb xc xd xe. returnOk ())) ba)