theory Retype_C

lemma createObject_invs':
  "\<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s
          \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and>
          caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and>
          (ty = APIObjectType apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and>
          is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and>
          {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and>
          0 < gsMaxObjectSize s
    \<rbrace> createObject ty ptr us dev\<lbrace>\<lambda>r s. invs' s \<rbrace>" apply (simp add:createObject_def3) apply (rule hoare_pre) apply (wp createNewCaps_invs'[where sz = "APIType_capBits ty us"]) apply (clarsimp simp:range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and> 0 < gsMaxObjectSize s\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and> 0 < gsMaxObjectSize s\<rbrace> do m <- createNewCaps ty ptr (Suc 0) us dev;
return (hd m)
od \<lbrace>\<lambda>r. invs'\<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>r. invs'\<rbrace>
 2. \<And>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and> caps_overlap_reserved' {ptr..ptr + 2 ^ APIType_capBits ty us - 1} s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits \<and> {ptr..ptr + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ((\<lambda>s. invs' s \<and> ct_active' s \<and> pspace_no_overlap' ptr (APIType_capBits ty us) s \<and> caps_no_overlap'' ptr (APIType_capBits ty us) s \<and> ptr \<noteq> 0 \<and> {ptr..(ptr && ~~ mask (APIType_capBits ty us)) + 2 ^ APIType_capBits ty us - 1} \<inter> kernel_data_refs = {} \<and> caps_overlap_reserved' {ptr..ptr + word_of_nat (Suc 0) * 2 ^ APIType_capBits ty us - 1} s \<and> (ty = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us) \<and> 0 < gsMaxObjectSize s) and K (range_cover ptr (APIType_capBits ty us) (APIType_capBits ty us) (Suc 0) \<and> Suc 0 \<noteq> 0)) s proof (prove)
goal:
No subgoals!