theory Detype_R

lemma createNewObjects_wp_helper:
  assumes check: "distinct dslots"
  and   cover: "range_cover ptr sz (Types_H.getObjectSize ty us) (length dslots)"
  and   not_0: "ptr \<noteq> 0" "length dslots \<noteq> 0"
  shows "\<lbrace>P\<rbrace> insertNewCaps ty parent dslots ptr us d \<lbrace>Q\<rbrace>
  \<Longrightarrow> \<lbrace>P and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent
  and (\<lambda>s. \<forall>slot \<in> set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s)
  and pspace_no_overlap' ptr sz
  and caps_no_overlap'' ptr sz
  and valid_pspace'
  and valid_arch_state'
  and caps_overlap_reserved'
   {ptr..ptr + of_nat (length dslots) * 2^ (Types_H.getObjectSize ty us) - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))
  \<rbrace> (createNewObjects ty parent dslots ptr us d) \<lbrace>Q\<rbrace>" using assms apply (clarsimp simp:valid_def) apply (drule_tac x = s in spec) apply (frule range_cover.range_cover_le_n_less(1)[where 'a=32, folded word_bits_def, OF _ le_refl]) apply (simp add:createNewObjects_def2[symmetric]) apply (drule(1) bspec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> insertNewCaps ty parent dslots ptr us d \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and (\<lambda>s. \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))\<rbrace> createNewObjects ty parent dslots ptr us d \<lbrace>Q\<rbrace> proof (prove)
using this:
distinct dslots
range_cover ptr sz (getObjectSize ty us) (length dslots)
ptr \<noteq> 0
length dslots \<noteq> 0

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> insertNewCaps ty parent dslots ptr us d \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P and (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent and (\<lambda>s. \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s) and pspace_no_overlap' ptr sz and caps_no_overlap'' ptr sz and valid_pspace' and valid_arch_state' and caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} and (\<lambda>s. ksCurDomain s \<le> maxDomain))\<rbrace> createNewObjects ty parent dslots ptr us d \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (insertNewCaps ty parent dslots ptr us d s). case x of (x, xa) \<Rightarrow> Q x xa); distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; ((), b) \<in> fst (createNewObjects ty parent dslots ptr us d s); P s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; valid_pspace' s; valid_arch_state' s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; ksCurDomain s \<le> maxDomain\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; ((), b) \<in> fst (createNewObjects ty parent dslots ptr us d s); P s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; valid_pspace' s; valid_arch_state' s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; ksCurDomain s \<le> maxDomain; P s \<longrightarrow> (\<forall>x\<in>fst (insertNewCaps ty parent dslots ptr us d s). case x of (x, xa) \<Rightarrow> Q x xa)\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; ((), b) \<in> fst (createNewObjects ty parent dslots ptr us d s); P s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; valid_pspace' s; valid_arch_state' s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; ksCurDomain s \<le> maxDomain; P s \<longrightarrow> (\<forall>x\<in>fst (insertNewCaps ty parent dslots ptr us d s). case x of (x, xa) \<Rightarrow> Q x xa); length dslots < 2 ^ word_bits\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; ((), b) \<in> fst (createNewObjects ty parent dslots ptr us d s); P s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; valid_pspace' s; valid_arch_state' s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; ksCurDomain s \<le> maxDomain; \<forall>(x, y)\<in>fst (createNewObjects ty parent dslots ptr us d s). Q x y; length dslots < 2 ^ word_bits\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; ((), b) \<in> fst (createNewObjects ty parent dslots ptr us d s); P s; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s; pspace_no_overlap' ptr sz s; caps_no_overlap'' ptr sz s; valid_pspace' s; valid_arch_state' s; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} s; ksCurDomain s \<le> maxDomain; length dslots < 2 ^ word_bits; case ((), b) of (x, xa) \<Rightarrow> Q x xa\<rbrakk> \<Longrightarrow> Q () b proof (prove)
goal:
No subgoals!