theory Retype_C

lemma createObject_caps_overlap_reserved_ret':
  "\<lbrace>\<lambda>s.  caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and>
         pspace_aligned' s \<and>
         pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and>
         is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits
    \<rbrace>createObject ty ptr us dev \<lbrace>\<lambda>rv. caps_overlap_reserved' (untypedRange rv)\<rbrace>" apply (simp add:createObject_def3) apply (rule hoare_pre) apply wp apply (rule_tac Q = "\<lambda>r s. r \<noteq> [] \<and> Q r s" for Q in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF createNewCaps_ret_len]) apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]]) apply assumption apply (rename_tac rv s) apply (case_tac rv,simp) apply clarsimp apply (erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) apply (clarsimp simp add:word_bits_conv range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv. caps_overlap_reserved' (untypedRange rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv. caps_overlap_reserved' (untypedRange rv)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>rv. caps_overlap_reserved' (untypedRange rv)\<rbrace>
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>m. caps_overlap_reserved' (untypedRange (hd m))\<rbrace>
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q1\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>r s. r \<noteq> [] \<and> ?Q13 r s\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 3. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv s. rv \<noteq> []\<rbrace>
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 4. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> ?P14 s \<and> ?P'14 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. Suc 0 = length rv \<Longrightarrow> rv \<noteq> []
 2. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 3. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 4. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'14\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>?Q13\<rbrace>
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 3. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> ?P'14 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s \<Longrightarrow> ?Q13 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 3. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s) \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s) \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>rv s a list. \<lbrakk>rv \<noteq> [] \<and> (\<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s); rv = a # list\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (untypedRange (hd rv)) s
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s a list. \<lbrakk>caps_overlap_reserved' (capRange a) s; \<forall>y\<in>set list. caps_overlap_reserved' (capRange y) s\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (untypedRange a) s
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<And>s a list. \<forall>y\<in>set list. caps_overlap_reserved' (capRange y) s \<Longrightarrow> untypedRange a \<subseteq> capRange a
 2. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<Longrightarrow> K (Suc 0 < 2 ^ word_bits \<and> Suc 0 \<noteq> 0) s \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> 0 < Suc 0 \<and> range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) proof (prove)
goal:
No subgoals!