theory CSpace_R

lemma setupReplyMaster_valid_mdb:
  "slot = t + 2 ^ objBits (undefined :: cte) * tcbReplySlot \<Longrightarrow>
   \<lbrace>valid_mdb' and valid_pspace' and tcb_at' t\<rbrace>
   setupReplyMaster t
   \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" apply (clarsimp simp: setupReplyMaster_def locateSlot_conv
                        nullMDBNode_def) apply (fold initMDBNode_def) apply (wp setCTE_valid_mdb getCTE_wp') apply clarsimp apply (intro conjI) apply (case_tac cte) apply (fastforce simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def
                            no_mdb_def
                      elim: valid_nullcapsE) apply (frule obj_at_aligned') apply (simp add: valid_cap'_def capAligned_def
                       objBits_simps' word_bits_def)+ apply (clarsimp simp: valid_pspace'_def) apply (clarsimp simp: caps_no_overlap'_def capRange_def) apply (clarsimp simp: fresh_virt_cap_class_def
                 elim!: ranE) apply (clarsimp simp add: noReplyCapsFor_def cte_wp_at_ctes_of) apply (case_tac x) apply (rename_tac capability mdbnode) apply (case_tac capability; simp) apply (rename_tac arch_capability) apply (case_tac arch_capability; simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot = t + 2 ^ objBits undefined * tcbReplySlot \<Longrightarrow> \<lbrace>valid_mdb' and valid_pspace' and tcb_at' t\<rbrace> setupReplyMaster t \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot = t + 2 ^ objBits undefined * tcbReplySlot \<Longrightarrow> \<lbrace>valid_mdb' and valid_pspace' and tcb_at' t\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) (MDB nullPointer nullPointer True True))
od)
od \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot = t + 2 ^ objBits undefined * tcbReplySlot \<Longrightarrow> \<lbrace>valid_mdb' and valid_pspace' and tcb_at' t\<rbrace> do oldCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
when (cteCap oldCTE = capability.NullCap) (do y <- stateAssert (noReplyCapsFor t) [];
setCTE (t + 2 ^ cte_level_bits * tcbReplySlot) (CTE (capability.ReplyCap t True True) initMDBNode)
od)
od \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; (valid_mdb' and valid_pspace' and tcb_at' t) s\<rbrakk> \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s \<longrightarrow> (if cteCap cte = capability.NullCap then \<lambda>s. noReplyCapsFor t s \<longrightarrow> valid_mdb' s \<and> cte_wp_at' no_mdb (t + 2 ^ cte_level_bits * tcbReplySlot) s \<and> valid_cap' (capability.ReplyCap t True True) s \<and> valid_objs' s \<and> capability.ReplyCap t True True \<noteq> capability.NullCap \<and> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True)) \<and> fresh_virt_cap_class (capClass (capability.ReplyCap t True True)) (ctes_of s) \<and> (capability.ReplyCap t True True = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)) else valid_mdb') s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> cte_wp_at' no_mdb (t + 2 ^ cte_level_bits * tcbReplySlot) s \<and> valid_cap' (capability.ReplyCap t True True) s \<and> valid_objs' s \<and> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True)) \<and> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (5 subgoals):
 1. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> cte_wp_at' no_mdb (t + 2 ^ cte_level_bits * tcbReplySlot) s
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap t True True) s
 3. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 5. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (5 subgoals):
 1. \<And>s cte x1 x2. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> cte_wp_at' no_mdb (t + 2 ^ cte_level_bits * tcbReplySlot) s
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap t True True) s
 3. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 5. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (4 subgoals):
 1. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap t True True) s
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 4. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (5 subgoals):
 1. \<And>s cte v v'. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s; is_aligned t (objBits (?obj50 s cte))\<rbrakk> \<Longrightarrow> valid_cap' (capability.ReplyCap t True True) s
 3. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 5. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (3 subgoals):
 1. \<And>s cte. \<lbrakk>slot = t + 0x10 * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 3. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> caps_no_overlap' (ctes_of s) (capRange (capability.ReplyCap t True True))
 2. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s\<rbrakk> \<Longrightarrow> fresh_virt_cap_class (ReplyClass t) (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; cte_wp_at' ((=) cte) (t + 2 ^ cte_level_bits * tcbReplySlot) s; noReplyCapsFor t s; ReplyClass t = capClass (cteCap x); ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap t m r; ReplyClass t = capClass (cteCap x); ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa x1 x2. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap t m r; ReplyClass t = capClass (cteCap x); ctes_of s xa = Some x; x = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa capability mdbnode. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap t m r; ReplyClass t = capClass (cteCap x); ctes_of s xa = Some x; x = CTE capability mdbnode\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s cte x xa capability mdbnode x8. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap t m r; ReplyClass t = acapClass x8; ctes_of s xa = Some (CTE (capability.ArchObjectCap x8) mdbnode); x = CTE (capability.ArchObjectCap x8) mdbnode; capability = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> False
 2. \<And>s cte x xa capability mdbnode x91 x92 x93. \<lbrakk>slot = x91 + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' x91 s; cteCap cte = capability.NullCap; ctes_of s (x91 + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap x91 m r; t = x91; ctes_of s xa = Some (CTE (capability.ReplyCap x91 x92 x93) mdbnode); x = CTE (capability.ReplyCap x91 x92 x93) mdbnode; capability = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s cte x xa capability mdbnode arch_capability. \<lbrakk>slot = t + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' t s; cteCap cte = capability.NullCap; ctes_of s (t + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap t m r; ReplyClass t = acapClass arch_capability; ctes_of s xa = Some (CTE (capability.ArchObjectCap arch_capability) mdbnode); x = CTE (capability.ArchObjectCap arch_capability) mdbnode; capability = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> False
 2. \<And>s cte x xa capability mdbnode x91 x92 x93. \<lbrakk>slot = x91 + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' x91 s; cteCap cte = capability.NullCap; ctes_of s (x91 + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap x91 m r; t = x91; ctes_of s xa = Some (CTE (capability.ReplyCap x91 x92 x93) mdbnode); x = CTE (capability.ReplyCap x91 x92 x93) mdbnode; capability = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa capability mdbnode x91 x92 x93. \<lbrakk>slot = x91 + 2 ^ objBits undefined * tcbReplySlot; valid_mdb' s; valid_pspace' s; tcb_at' x91 s; cteCap cte = capability.NullCap; ctes_of s (x91 + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; \<forall>sl m r cte. ctes_of s sl = Some cte \<longrightarrow> cteCap cte \<noteq> capability.ReplyCap x91 m r; t = x91; ctes_of s xa = Some (CTE (capability.ReplyCap x91 x92 x93) mdbnode); x = CTE (capability.ReplyCap x91 x92 x93) mdbnode; capability = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!