theory Ipc_R

lemma transferCapsToSlots_valid_objs[wp]:
  "\<lbrace>valid_objs' and valid_mdb' and (\<lambda>s. \<forall>x \<in> set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s)
       and (\<lambda>s. \<forall>x \<in> set caps. s \<turnstile>' fst x) and K(distinct slots)\<rbrace>
       transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (rule hoare_pre) apply (rule transferCapsToSlots_presM[where vo=True and emx=False and drv=False and pad=False]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_mdb' and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. valid_cap' (fst x) s) and K (distinct slots)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>s. (valid_objs' and valid_mdb' and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. valid_cap' (fst x) s) and K (distinct slots)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>cap src dest. \<lbrace>\<lambda>s. valid_objs' s \<and> (False \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) dest s) \<and> (True \<longrightarrow> valid_objs' s \<and> valid_cap' cap s \<and> real_cte_at' dest s) \<and> (False \<longrightarrow> cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src s \<and> valid_mdb' s) \<and> (False \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>b n. \<lbrace>valid_objs'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_objs'\<rbrace>
 3. \<And>s. (valid_objs' and valid_mdb' and (\<lambda>s. \<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) and (\<lambda>s. \<forall>x\<in>set caps. valid_cap' (fst x) s) and K (distinct slots)) s \<Longrightarrow> valid_objs' s \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> distinct slots) \<and> (True \<longrightarrow> valid_objs' s \<and> (\<forall>x\<in>set slots. real_cte_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s) \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s) \<and> distinct slots) \<and> (False \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (False \<longrightarrow> True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_mdb' s \<and> length slots \<le> 1 \<and> (\<forall>x\<in>set caps. valid_cap' (fst x) s \<and> (slots \<noteq> [] \<longrightarrow> cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s))) proof (prove)
goal:
No subgoals!