theory Retype_C

lemma insertNewCap_caps_overlap_reserved':
notes blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
      Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
shows "\<lbrace>cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_overlap_reserved' S
        and valid_cap' x and K  (cptr \<noteq> (0::word32)) and K (untypedRange x \<inter> S = {})\<rbrace>
       insertNewCap srcSlot cptr x
       \<lbrace>\<lambda>rv s. caps_overlap_reserved' S s\<rbrace>" apply (clarsimp simp:insertNewCap_def caps_overlap_reserved'_def) apply (rule hoare_pre) apply (wp getCTE_wp updateMDB_ctes_of_cap) apply (clarsimp simp:cte_wp_at_ctes_of valid_pspace'_def
    valid_mdb'_def valid_mdb_ctes_def no_0_def split:if_splits) apply (erule ranE) apply (clarsimp split:if_splits) apply (drule usableRange_subseteq[rotated]) apply (simp add:valid_cap'_def) apply blast apply (drule_tac p = xaa in caps_overlap_reserved'_D) apply simp apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_overlap_reserved' S and valid_cap' x and K (cptr \<noteq> 0) and K (untypedRange x \<inter> S = {})\<rbrace> insertNewCap srcSlot cptr x \<lbrace>\<lambda>rv. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_overlap_reserved' S and valid_cap' x and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> S = {})\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE cptr;
y <- assert (nullCapPointers oldCTE);
y <- setCTE cptr (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. cptr));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. cptr));
updateNewFreeIndex cptr
od \<lbrace>\<lambda>rv s. \<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE srcSlot);
oldCTE <- getCTE cptr;
y <- assert (nullCapPointers oldCTE);
y <- setCTE cptr (CTE x (MDB next srcSlot True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. cptr));
y <- updateMDB srcSlot (mdbNext_update (\<lambda>_. cptr));
updateNewFreeIndex cptr
od \<lbrace>\<lambda>rv s. \<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_overlap_reserved' S and valid_cap' x and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> S = {})) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_overlap_reserved' S and valid_cap' x and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> S = {})) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) srcSlot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) srcSlot s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) cptr s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) cptr s \<and> (nullCapPointers cte \<longrightarrow> ((\<forall>x\<in>ran ((ctes_of s)(cptr \<mapsto> CTE x (MDB next srcSlot True True))). isUntypedCap (cteCap x) \<longrightarrow> usableUntypedRange (cteCap x) \<inter> S = {}) \<and> no_0 ((ctes_of s)(cptr \<mapsto> CTE x (MDB next srcSlot True True)))) \<and> no_0 ((ctes_of s)(cptr \<mapsto> CTE x (MDB next srcSlot True True)))))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; xa \<in> ran (\<lambda>a. if a = cptr then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) ctea) srcSlot True True)) else ctes_of s a); cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); (if xaa = cptr then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) ctea) srcSlot True True)) else ctes_of s xaa) = Some xa\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap x\<rbrakk> \<Longrightarrow> usableUntypedRange x \<inter> S = {}
 2. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> capAligned x
 2. \<And>s cte ctea. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; usableUntypedRange x \<subseteq> untypedRange x\<rbrakk> \<Longrightarrow> usableUntypedRange x \<inter> S = {}
 3. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; usableUntypedRange x \<subseteq> untypedRange x\<rbrakk> \<Longrightarrow> usableUntypedRange x \<inter> S = {}
 2. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); caps_overlap_reserved' S s; valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> ctes_of s xaa = Some (?cte107 s cte ctea xa xaa)
 2. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (?cte107 s cte ctea xa xaa))
 3. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa; usableUntypedRange (cteCap (?cte107 s cte ctea xa xaa)) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap xa)
 2. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa; usableUntypedRange (cteCap xa) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa. \<lbrakk>ctes_of s cptr = Some cte; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_dlist (ctes_of s); ctes_of s 0 = None; mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); valid_cap' x s; untypedRange x \<inter> S = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; isUntypedCap (cteCap xa); xaa \<noteq> cptr; ctes_of s xaa = Some xa; usableUntypedRange (cteCap xa) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap xa) \<inter> S = {} proof (prove)
goal:
No subgoals!