theory Retype_R

lemma createObjects_orig_cte_wp_at2':
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)
      \<and> n \<noteq> 0
      \<and> range_cover ptr sz (objBitsKO val + gbits) n
      \<and> pspace_aligned' s \<and> pspace_distinct' s
      \<and> \<not> (case_option False P' (projectKO_opt val))
      \<and> (\<forall>(getF, setF) \<in> ran tcb_cte_cases.
              \<not> (case_option False (P' \<circ> getF) (projectKO_opt val)))
      \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (cte_wp_at' P' p s)\<rbrace>" apply (simp add: cte_wp_at'_obj_at') apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def) including no_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz]
             | simp add: o_def cong: option.case_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cte_wp_at' P' p s) \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> P' x) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> (P' \<circ> getF) x)) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (cte_wp_at' P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s)) \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (getF x2))) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (obj_at' P' p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (obj_at' P' p s) \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (getF x2))) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (obj_at' P' p s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s) \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (getF x2))) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s) \<and> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (getF x2))) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P' \<circ> fst (the (tcb_cte_cases n))) (p - n) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (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> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbIPCBufferFrame x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbCaller x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbReply x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbVTable x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbCTable x2)) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (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>P. \<lbrace>\<lambda>s. P (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> 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' x2) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbIPCBufferFrame x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbCaller x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbReply x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbVTable x2)) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> P' (tcbCTable x2)) \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>r s. P (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:
No subgoals!