theory Retype_C

lemma createObject_ct_active'[wp]:
  "\<lbrace>\<lambda>s. ct_active' 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>r s. ct_active' s \<rbrace>" apply (simp add:ct_in_state'_def createObject_def3) apply (rule hoare_pre) apply wp apply wps apply (wp createNewCaps_pred_tcb_at') apply (intro conjI) apply (auto simp:range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_active' 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>r. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' active' (ksCurThread s) 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>r s. st_tcb_at' active' (ksCurThread s) s\<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 s. st_tcb_at' active' (ksCurThread s) s\<rbrace>
 2. \<And>s. st_tcb_at' active' (ksCurThread s) 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 a. st_tcb_at' active' (ksCurThread a) a\<rbrace>
 2. \<And>s. st_tcb_at' active' (ksCurThread s) 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. \<And>prev_s. \<lbrace>?P8 prev_s\<rbrace> createNewCaps ty ptr (Suc 0) us dev \<lbrace>\<lambda>rv. st_tcb_at' active' (ksCurThread prev_s)\<rbrace>
 2. \<And>s. st_tcb_at' active' (ksCurThread s) 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> ?P8 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at' active' (ksCurThread s) 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> st_tcb_at' active' (ksCurThread s) s \<and> range_cover ptr (?sz15 s) (APIType_capBits ty us) (Suc 0) \<and> 0 < Suc 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz15 s) s \<and> (\<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. active' (itcbState (tcb_to_itcb' (tcbDomain_update (\<lambda>_. d) tcb))) = active' (itcbState (tcb_to_itcb' tcb)))) proof (prove)
goal (7 subgoals):
 1. \<And>s. st_tcb_at' active' (ksCurThread s) 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> st_tcb_at' active' (ksCurThread s) s
 2. \<And>s. st_tcb_at' active' (ksCurThread s) 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> range_cover ptr (?sz15 s) (APIType_capBits ty us) (Suc 0)
 3. \<And>s. st_tcb_at' active' (ksCurThread s) 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> 0 < Suc 0
 4. \<And>s. st_tcb_at' active' (ksCurThread s) 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> pspace_aligned' s
 5. \<And>s. st_tcb_at' active' (ksCurThread s) 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> pspace_distinct' s
 6. \<And>s. st_tcb_at' active' (ksCurThread s) 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> pspace_no_overlap' ptr (?sz15 s) s
 7. \<And>s. st_tcb_at' active' (ksCurThread s) 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> \<forall>tcb. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<forall>d. active' (itcbState (tcb_to_itcb' (tcbDomain_update (\<lambda>_. d) tcb))) = active' (itcbState (tcb_to_itcb' tcb))) proof (prove)
goal:
No subgoals!