theory Retype_C

lemma createObject_capClass[wp]:
  "\<lbrace> \<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits
   \<rbrace> createObject ty ptr us dev
   \<lbrace>\<lambda>rv s. capClass rv = PhysicalClass\<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_range_helper]) apply assumption apply (rename_tac rv s) apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv ) apply (rule range_cover_full) apply (simp add:word_bits_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned ptr (APIType_capBits ty us) \<and> APIType_capBits ty us < word_bits\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>rv s. capClass rv = PhysicalClass\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 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 s. capClass rv = PhysicalClass\<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 s. capClass rv = PhysicalClass\<rbrace>
 2. \<And>s. 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 a. capClass (hd m) = PhysicalClass\<rbrace>
 2. \<And>s. 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> capClass (hd rv) = PhysicalClass
 3. \<And>s. 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> capClass (hd rv) = PhysicalClass
 4. \<And>s. 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> capClass (hd rv) = PhysicalClass
 4. \<And>s. 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> capClass (hd rv) = PhysicalClass
 3. \<And>s. 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. \<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us) \<Longrightarrow> ?Q13 rv s
 2. \<And>rv s. rv \<noteq> [] \<and> ?Q13 rv s \<Longrightarrow> capClass (hd rv) = PhysicalClass
 3. \<And>s. 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> range_cover ptr ?sz25 (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)) \<Longrightarrow> capClass (hd rv) = PhysicalClass
 2. \<And>s. 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> range_cover ptr ?sz25 (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 proof (prove)
goal (2 subgoals):
 1. \<And>rv s. rv \<noteq> [] \<and> (\<exists>capfn. rv = map capfn (map (\<lambda>p. More_Word_Operations.ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<Suc 0]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)) \<Longrightarrow> capClass (hd rv) = PhysicalClass
 2. \<And>s. 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> range_cover ptr ?sz25 (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 proof (prove)
goal (1 subgoal):
 1. \<And>s. 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> range_cover ptr ?sz25 (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < 32\<rbrakk> \<Longrightarrow> range_cover ptr ?sz25 (APIType_capBits ty us) (Suc 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < 32\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits ty us)
 2. \<lbrakk>is_aligned ptr (APIType_capBits ty us); APIType_capBits ty us < 32\<rbrakk> \<Longrightarrow> APIType_capBits ty us < word_bits proof (prove)
goal:
No subgoals!