theory Detype_R

lemma createObjects_setDomain_commute:
  "monad_commute
  (\<lambda>s. range_cover ptr'  (objBitsKO (KOTCB makeObject))
       (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and>
  pspace_aligned' s \<and> pspace_distinct' s \<and>
  pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and>
  tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)))
  (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0)
  (threadSet (tcbDomain_update (\<lambda>_. r)) ptr)" apply (rule monad_commute_guard_imp) apply (rule threadSet_commute) apply (wp createObjects_orig_obj_at'[where sz = "(objBitsKO (KOTCB makeObject))"]) apply clarsimp apply assumption apply (simp add:placeNewObject_def2[where val = "makeObject::tcb",simplified,symmetric]) apply (rule placeNewObject_modify_commute) apply (clarsimp simp: objBits_simps' typ_at'_def word_bits_def
    obj_at'_def ko_wp_at'_def projectKO_eq projectKO_opt_tcb) apply (clarsimp split:Structures_H.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject))) (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (threadSet (tcbDomain_update (\<lambda>_. r)) ptr) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (threadSet (tcbDomain_update (\<lambda>_. r)) ptr)
 2. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> ?P s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3 and tcb_at' ptr\<rbrace> createObjects' ptr' (Suc 0) (KOTCB makeObject) 0 \<lbrace>\<lambda>r. tcb_at' ptr\<rbrace>
 2. monad_commute ?P'3 (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)))))
 3. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and ?P3 and ?P'3) s proof (prove)
goal (3 subgoals):
 1. \<And>s. (?P3 and tcb_at' ptr) s \<Longrightarrow> Suc 0 \<noteq> 0 \<and> range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> tcb_at' ptr s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s
 2. monad_commute ?P'3 (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)))))
 3. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and ?P3 and ?P'3) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>?P3 s; tcb_at' ptr s\<rbrakk> \<Longrightarrow> range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject)) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s
 2. monad_commute ?P'3 (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)))))
 3. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and ?P3 and ?P'3) s proof (prove)
goal (2 subgoals):
 1. monad_commute ?P'3 (createObjects' ptr' (Suc 0) (KOTCB makeObject) 0) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)))))
 2. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and (\<lambda>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject)) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s) and ?P'3) s proof (prove)
goal (2 subgoals):
 1. monad_commute ?P'3 (placeNewObject ptr' makeObject 0) (modify (ksPSpace_update (\<lambda>ps. ps(ptr \<mapsto> case ps ptr of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)))))
 2. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and (\<lambda>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject)) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s) and ?P'3) s proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject) + 0) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s \<and> tcb_at' ptr s \<and> is_aligned ptr' (objBitsKO (KOTCB makeObject)) \<Longrightarrow> (tcb_at' ptr and (\<lambda>s. range_cover ptr' (objBitsKO (KOTCB makeObject)) (objBitsKO (KOTCB makeObject)) (Suc 0) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr' (objBitsKO (KOTCB makeObject)) s) and (K (is_aligned ptr' (objBitsKO (injectKOS makeObject) + 0) \<and> objBitsKO (injectKOS makeObject) + 0 < word_bits) and pspace_no_overlap' ptr' (objBitsKO (injectKOS makeObject) + 0) and pspace_aligned' and ko_wp_at' (\<lambda>a. objBitsKO (case Some a of Some (KOTCB tcb) \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb)) = objBitsKO a) ptr)) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj. \<lbrakk>range_cover ptr' 9 9 (Suc 0); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr' 9 s; is_aligned ptr' 9; ksPSpace s ptr = Some ko; is_aligned ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ps_clear ptr (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; (case ko of KOTCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some obj\<rbrakk> \<Longrightarrow> (case case ko of KOTCB tcb \<Rightarrow> KOTCB (tcbDomain_update (\<lambda>_. r) tcb) of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) = (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) proof (prove)
goal:
No subgoals!