theory Untyped_R

lemma deleteObjects_ct_active':
  "\<lbrace>invs' and sch_act_simple and ct_active'
      and cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr sz idx) cref
      and (\<lambda>s. descendants_range' (UntypedCap d ptr sz idx) cref (ctes_of s))
      and K (sz < word_bits \<and> is_aligned ptr sz)\<rbrace>
     deleteObjects ptr sz
   \<lbrace>\<lambda>_. ct_active'\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_pre) apply wps apply (wp deleteObjects_st_tcb_at') apply (auto simp: ct_in_state'_def elim: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_active' and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) cref and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr sz idx) cref (ctes_of s)) and K (sz < word_bits \<and> is_aligned ptr sz)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>_. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) cref and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr sz idx) cref (ctes_of s)) and (\<lambda>y. sz < word_bits \<and> is_aligned ptr sz)\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>_ s. st_tcb_at' active' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>_ s. st_tcb_at' active' (ksCurThread s) s\<rbrace>
 2. \<And>s. (invs' and sch_act_simple and (\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) cref and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr sz idx) cref (ctes_of s)) and (\<lambda>y. sz < word_bits \<and> is_aligned ptr sz)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> deleteObjects ptr sz \<lbrace>\<lambda>rv. st_tcb_at' active' (ksCurThread prev_s)\<rbrace>
 2. \<And>s. (invs' and sch_act_simple and (\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) cref and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr sz idx) cref (ctes_of s)) and (\<lambda>y. sz < word_bits \<and> is_aligned ptr sz)) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and (\<lambda>s. st_tcb_at' active' (ksCurThread s) s) and cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr sz idx) cref and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr sz idx) cref (ctes_of s)) and (\<lambda>y. sz < word_bits \<and> is_aligned ptr sz)) s \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d10 s) ptr sz (?idx10 s)) (?p10 s) and invs' and ct_active' and sch_act_simple and (\<lambda>sa. descendants_range' (capability.UntypedCap (?d10 s) ptr sz (?idx10 s)) (?p10 s) (ctes_of sa)) and st_tcb_at' (active' and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) (ksCurThread s) and K (sz < word_bits \<and> is_aligned ptr sz)) s proof (prove)
goal:
No subgoals!