theory Detype_R

lemma createNewObjects_corres_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"
  and       c: "corres r P P' f (insertNewCaps ty parent dslots ptr us d)"
  and     imp: "\<And>s. P' s \<Longrightarrow> (cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent s
  \<and> (\<forall>slot \<in> set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s)
  \<and> pspace_no_overlap' ptr sz s
  \<and> caps_no_overlap'' ptr sz s
  \<and> caps_overlap_reserved'
   {ptr..ptr + of_nat (length dslots) * 2^ (Types_H.getObjectSize ty us) - 1} s
  \<and> valid_pspace' s \<and> valid_arch_state' s \<and> ksCurDomain s \<le> maxDomain)"
shows "corres r P P' f (createNewObjects ty parent dslots ptr us d)" using check cover not_0 apply (clarsimp simp:corres_underlying_def) apply (frule imp) apply (frule range_cover.range_cover_le_n_less(1)[where 'a=32, folded word_bits_def, OF _ le_refl]) apply clarsimp apply (simp add:createNewObjects_def2) using c apply (clarsimp simp:corres_underlying_def) apply (drule(1) bspec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P P' f (createNewObjects ty parent dslots ptr us d) 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. corres r P P' f (createNewObjects ty parent dslots ptr us d) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; (a, b) \<in> state_relation; P a; P' b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (createNewObjects ty parent dslots ptr us d b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra ()) \<and> \<not> snd (createNewObjects ty parent dslots ptr us d b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; (a, b) \<in> state_relation; P a; P' b; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent b \<and> (\<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot b) \<and> pspace_no_overlap' ptr sz b \<and> caps_no_overlap'' ptr sz b \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} b \<and> valid_pspace' b \<and> valid_arch_state' b \<and> ksCurDomain b \<le> maxDomain\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (createNewObjects ty parent dslots ptr us d b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra ()) \<and> \<not> snd (createNewObjects ty parent dslots ptr us d b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; (a, b) \<in> state_relation; P a; P' b; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent b \<and> (\<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot b) \<and> pspace_no_overlap' ptr sz b \<and> caps_no_overlap'' ptr sz b \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} b \<and> valid_pspace' b \<and> valid_arch_state' b \<and> ksCurDomain b \<le> maxDomain; length dslots < 2 ^ word_bits\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (createNewObjects ty parent dslots ptr us d b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra ()) \<and> \<not> snd (createNewObjects ty parent dslots ptr us d b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; (a, b) \<in> state_relation; P a; P' b; length dslots < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent b; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot b; pspace_no_overlap' ptr sz b; caps_no_overlap'' ptr sz b; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} b; valid_pspace' b; valid_arch_state' b; ksCurDomain b \<le> maxDomain\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (createNewObjects ty parent dslots ptr us d b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra ()) \<and> \<not> snd (createNewObjects ty parent dslots ptr us d b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>distinct dslots; range_cover ptr sz (getObjectSize ty us) (length dslots); ptr \<noteq> 0; dslots \<noteq> []; (a, b) \<in> state_relation; P a; P' b; length dslots < 2 ^ word_bits; cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c)) parent b; \<forall>slot\<in>set dslots. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot b; pspace_no_overlap' ptr sz b; caps_no_overlap'' ptr sz b; caps_overlap_reserved' {ptr..ptr + word_of_nat (length dslots) * 2 ^ getObjectSize ty us - 1} b; valid_pspace' b; valid_arch_state' b; ksCurDomain b \<le> maxDomain\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (insertNewCaps ty parent dslots ptr us d b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> state_relation \<and> r ra ()) \<and> \<not> snd (insertNewCaps ty parent dslots ptr us d b) proof (prove)
using this:
corres r P P' f (insertNewCaps ty parent dslots ptr us d)

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