theory ArchDecode_IF

lemma ensure_safe_mapping_reads_respects:
  "reads_respects aag l (K (authorised_slots aag entries)) (ensure_safe_mapping entries)" apply (rule gen_asm_ev) apply (case_tac entries) apply (rename_tac a, case_tac a) apply (rename_tac aa b, case_tac aa) apply (fastforce intro: returnOk_ev_pre) apply (rule equiv_valid_guard_imp) apply (wp mapME_x_ev' get_master_pte_reads_respects get_pte_reads_respects | wpc | simp)+ apply (clarsimp simp: authorised_slots_def) apply simp apply (rule equiv_valid_guard_imp) apply (wp mapME_x_ev' get_master_pte_reads_respects | wpc | simp)+ apply (fastforce simp: authorised_slots_def) apply (rename_tac b, case_tac b) apply (rename_tac a ba, case_tac a) apply (fastforce intro: returnOk_ev) apply simp apply (rule fail_ev) apply simp apply (rule equiv_valid_guard_imp) apply (wp mapME_x_ev' get_master_pde_reads_respects | wpc | simp)+ apply (fastforce simp: authorised_slots_def) apply simp apply (rule equiv_valid_guard_imp) apply (wp mapME_x_ev' get_master_pde_reads_respects | wpc | simp)+ apply (fastforce simp: authorised_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (K (authorised_slots aag entries)) (ensure_safe_mapping entries) proof (prove)
goal (1 subgoal):
 1. authorised_slots aag entries \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>authorised_slots aag entries; entries = Inl a\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b)\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = InvalidPTE\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>a aa b x21 x22 x23. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 4. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x21 x22 x23. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (4 subgoals):
 1. \<And>a aa b x21 x22 x23. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q15 a aa b x21 x22 x23) (ensure_safe_mapping entries)
 2. \<And>a aa b x21 x22 x23 s. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = LargePagePTE x21 x22 x23; True\<rbrakk> \<Longrightarrow> ?Q15 a aa b x21 x22 x23 s
 3. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 4. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x21 x22 x23. \<lbrakk>authorised_slots aag (Inl (LargePagePTE x21 x22 x23, b)); entries = Inl (LargePagePTE x21 x22 x23, b); a = (LargePagePTE x21 x22 x23, b); aa = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. is_subject aag (x && ~~ mask pt_bits)
 2. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag entries; entries = Inl a; a = (aa, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag (Inl (SmallPagePTE x31 x32 x33, b)); entries = Inl (SmallPagePTE x31 x32 x33, b); a = (SmallPagePTE x31 x32 x33, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (mapME_x (\<lambda>slot. liftE (get_master_pte slot) >>=E case_pte (returnOk ()) (\<lambda>word set1 set2. throwError DeleteFirst) (\<lambda>x xa xb. returnOk ())) b)
 2. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag (Inl (SmallPagePTE x31 x32 x33, b)); entries = Inl (SmallPagePTE x31 x32 x33, b); a = (SmallPagePTE x31 x32 x33, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q65 a aa b x31 x32 x33) (mapME_x (\<lambda>slot. liftE (get_master_pte slot) >>=E case_pte (returnOk ()) (\<lambda>word set1 set2. throwError DeleteFirst) (\<lambda>x xa xb. returnOk ())) b)
 2. \<And>a aa b x31 x32 x33 s. \<lbrakk>authorised_slots aag (Inl (SmallPagePTE x31 x32 x33, b)); entries = Inl (SmallPagePTE x31 x32 x33, b); a = (SmallPagePTE x31 x32 x33, b); aa = SmallPagePTE x31 x32 x33; True\<rbrakk> \<Longrightarrow> ?Q65 a aa b x31 x32 x33 s
 3. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b x31 x32 x33. \<lbrakk>authorised_slots aag (Inl (SmallPagePTE x31 x32 x33, b)); entries = Inl (SmallPagePTE x31 x32 x33, b); a = (SmallPagePTE x31 x32 x33, b); aa = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. is_subject aag (x && ~~ mask pt_bits)
 2. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>authorised_slots aag entries; entries = Inr b\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba)\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (4 subgoals):
 1. \<And>b a ba. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = InvalidPDE\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b a ba x21 x22 x23. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 4. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba x21 x22 x23. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba x21 x22 x23. \<lbrakk>authorised_slots aag (Inr (PageTablePDE x21 x22 x23, ba)); entries = Inr (PageTablePDE x21 x22 x23, ba); b = (PageTablePDE x21 x22 x23, ba); a = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) fail
 2. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 3. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries)
 2. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag (Inr (SectionPDE x31 x32 x33 x34, ba)); entries = Inr (SectionPDE x31 x32 x33 x34, ba); b = (SectionPDE x31 x32 x33 x34, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E case_pde (returnOk ()) (\<lambda>word1 set word2. throwError DeleteFirst) (\<lambda>x xa xb xc. returnOk ()) (\<lambda>word set1 set2. throwError DeleteFirst)) ba)
 2. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (3 subgoals):
 1. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag (Inr (SectionPDE x31 x32 x33 x34, ba)); entries = Inr (SectionPDE x31 x32 x33 x34, ba); b = (SectionPDE x31 x32 x33 x34, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q133 b a ba x31 x32 x33 x34) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E case_pde (returnOk ()) (\<lambda>word1 set word2. throwError DeleteFirst) (\<lambda>x xa xb xc. returnOk ()) (\<lambda>word set1 set2. throwError DeleteFirst)) ba)
 2. \<And>b a ba x31 x32 x33 x34 s. \<lbrakk>authorised_slots aag (Inr (SectionPDE x31 x32 x33 x34, ba)); entries = Inr (SectionPDE x31 x32 x33 x34, ba); b = (SectionPDE x31 x32 x33 x34, ba); a = SectionPDE x31 x32 x33 x34; True\<rbrakk> \<Longrightarrow> ?Q133 b a ba x31 x32 x33 x34 s
 3. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x31 x32 x33 x34. \<lbrakk>authorised_slots aag (Inr (SectionPDE x31 x32 x33 x34, ba)); entries = Inr (SectionPDE x31 x32 x33 x34, ba); b = (SectionPDE x31 x32 x33 x34, ba); a = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ba. is_subject aag (x && ~~ mask pd_bits)
 2. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag entries; entries = Inr b; b = (a, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (ensure_safe_mapping entries) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag (Inr (SuperSectionPDE x41 x42 x43, ba)); entries = Inr (SuperSectionPDE x41 x42 x43, ba); b = (SuperSectionPDE x41 x42 x43, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (\<lambda>_. True) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E case_pde (returnOk ()) (\<lambda>word1 set word2. throwError DeleteFirst) (\<lambda>word1 set1 word2 set2. throwError DeleteFirst) (\<lambda>x xa xb. returnOk ())) ba) proof (prove)
goal (2 subgoals):
 1. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag (Inr (SuperSectionPDE x41 x42 x43, ba)); entries = Inr (SuperSectionPDE x41 x42 x43, ba); b = (SuperSectionPDE x41 x42 x43, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> reads_respects aag l (?Q199 b a ba x41 x42 x43) (mapME_x (\<lambda>slot. liftE (get_master_pde slot) >>=E case_pde (returnOk ()) (\<lambda>word1 set word2. throwError DeleteFirst) (\<lambda>word1 set1 word2 set2. throwError DeleteFirst) (\<lambda>x xa xb. returnOk ())) ba)
 2. \<And>b a ba x41 x42 x43 s. \<lbrakk>authorised_slots aag (Inr (SuperSectionPDE x41 x42 x43, ba)); entries = Inr (SuperSectionPDE x41 x42 x43, ba); b = (SuperSectionPDE x41 x42 x43, ba); a = SuperSectionPDE x41 x42 x43; True\<rbrakk> \<Longrightarrow> ?Q199 b a ba x41 x42 x43 s proof (prove)
goal (1 subgoal):
 1. \<And>b a ba x41 x42 x43. \<lbrakk>authorised_slots aag (Inr (SuperSectionPDE x41 x42 x43, ba)); entries = Inr (SuperSectionPDE x41 x42 x43, ba); b = (SuperSectionPDE x41 x42 x43, ba); a = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ba. is_subject aag (x && ~~ mask pd_bits) proof (prove)
goal:
No subgoals!