theory Retype_R

lemma createObjects_ex_cte_cap_to [wp]:
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and>
        pspace_distinct' s \<and> ex_cte_cap_to' p s \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects ptr n val gbits \<lbrace>\<lambda>r. ex_cte_cap_to' p\<rbrace>" apply (simp add: ex_cte_cap_to'_def createObjects_def) apply (rule hoare_lift_Pf2 [where f="irq_node'"]) apply (wp hoare_vcg_ex_lift createObjects_orig_cte_wp_at'[where sz = sz]) apply simp apply wp 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> ex_cte_cap_wp_to' (\<lambda>_. True) p s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>r. ex_cte_cap_wp_to' (\<lambda>_. True) 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> (\<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>r s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) x) cref s) \<and> pspace_no_overlap' ptr sz s\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ a. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) x) cref a\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> (\<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) x) cref s) \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> \<exists>xa. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) x) xa s \<and> pspace_no_overlap' ptr sz s
 2. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace> proof (prove)
goal:
No subgoals!