theory Retype_R

lemma createObjects_orig_cte_wp_at':
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> cte_wp_at' P p s
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r s. cte_wp_at' P p s\<rbrace>" apply (simp add: cte_wp_at'_obj_at' tcb_cte_cases_def) apply (rule hoare_pre, wp hoare_vcg_disj_lift createObjects_orig_obj_at'[where sz = sz]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' P p s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (obj_at' P p s \<or> obj_at' (P \<circ> tcbIPCBufferFrame) (p - 0x40) s \<or> obj_at' (P \<circ> tcbCaller) (p - 0x30) s \<or> obj_at' (P \<circ> tcbReply) (p - 0x20) s \<or> obj_at' (P \<circ> tcbVTable) (p - 0x10) s \<or> obj_at' (P \<circ> tcbCTable) p s) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. obj_at' P p s \<or> obj_at' (P \<circ> tcbIPCBufferFrame) (p - 0x40) s \<or> obj_at' (P \<circ> tcbCaller) (p - 0x30) s \<or> obj_at' (P \<circ> tcbReply) (p - 0x20) s \<or> obj_at' (P \<circ> tcbVTable) (p - 0x10) s \<or> obj_at' (P \<circ> tcbCTable) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (obj_at' P p s \<or> obj_at' (P \<circ> tcbIPCBufferFrame) (p - 0x40) s \<or> obj_at' (P \<circ> tcbCaller) (p - 0x30) s \<or> obj_at' (P \<circ> tcbReply) (p - 0x20) s \<or> obj_at' (P \<circ> tcbVTable) (p - 0x10) s \<or> obj_at' (P \<circ> tcbCTable) p s) \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' P p s \<and> pspace_no_overlap' ptr sz s \<or> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (P \<circ> tcbIPCBufferFrame) (p - 0x40) s \<and> pspace_no_overlap' ptr sz s \<or> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (P \<circ> tcbCaller) (p - 0x30) s \<and> pspace_no_overlap' ptr sz s \<or> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (P \<circ> tcbReply) (p - 0x20) s \<and> pspace_no_overlap' ptr sz s \<or> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (P \<circ> tcbVTable) (p - 0x10) s \<and> pspace_no_overlap' ptr sz s \<or> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (P \<circ> tcbCTable) p s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal:
No subgoals!