theory Retype_C

lemma insertNewCap_caps_no_overlap'':
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_no_overlap'' ptr us
        and K  (cptr \<noteq> (0::word32)) and K (untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {})\<rbrace>
 insertNewCap srcSlot cptr x
          \<lbrace>\<lambda>rv s. caps_no_overlap'' ptr us s\<rbrace>" apply (clarsimp simp:insertNewCap_def caps_no_overlap''_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 (frule_tac c=  "(cteCap xa)" and q = xb in caps_no_overlapD''[rotated]) apply (clarsimp simp:cte_wp_at_ctes_of) apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_no_overlap'' ptr us and K (cptr \<noteq> 0) and K (untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {})\<rbrace> insertNewCap srcSlot cptr x \<lbrace>\<lambda>rv. caps_no_overlap'' ptr us\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_no_overlap'' ptr us and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {})\<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). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap cte)\<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). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap cte)\<rbrace>
 2. \<And>s. (cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_no_overlap'' ptr us and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {})) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>_. True) cptr and valid_pspace' and caps_no_overlap'' ptr us and (\<lambda>y. cptr \<noteq> 0) and (\<lambda>y. untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {})) 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))). untypedRange (cteCap x) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap x)) \<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 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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; 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; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; (if xb = cptr then Some (CTE x (MDB ((mdbNext \<circ> cteMDBNode) ctea) srcSlot True True)) else ctes_of s xb) = Some xa\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; xb \<noteq> cptr; ctes_of s xb = Some xa\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; xb \<noteq> cptr; ctes_of s xb = Some xa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cap. cteCap cap = cteCap xa) xb s
 2. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; xb \<noteq> cptr; ctes_of s xb = Some xa; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap xa)\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; xb \<noteq> cptr; ctes_of s xb = Some xa; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap xa)\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea xa xaa xb. \<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_no_overlap'' ptr us s; untypedRange x \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} = {}; ctes_of s srcSlot = Some ctea; cteCap cte = capability.NullCap; mdbNext (cteMDBNode cte) = nullPointer; mdbPrev (cteMDBNode cte) = nullPointer; untypedRange (cteCap xa) \<inter> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<noteq> {}; xaa \<in> {ptr..(ptr && ~~ mask us) + 2 ^ us - 1}; xb \<noteq> cptr; ctes_of s xb = Some xa; {ptr..(ptr && ~~ mask us) + 2 ^ us - 1} \<subseteq> untypedRange (cteCap xa)\<rbrakk> \<Longrightarrow> xaa \<in> untypedRange (cteCap xa) proof (prove)
goal:
No subgoals!