theory Ipc_AC

lemma transfer_caps_loop_pres_dest:
  assumes x: "\<And>cap src dest.
              \<lbrace>\<lambda>s. P s \<and> dest \<in> set slots \<and> src \<in> snd ` set caps \<and> valid_objs s \<and>
                   real_cte_at dest s \<and> s \<turnstile> cap \<and> tcb_cap_valid cap dest s \<and> real_cte_at src s \<and>
                   cte_wp_at (is_derived (cdt s) src cap) src s \<and> cap \<noteq> NullCap \<rbrace>
              cap_insert cap src dest
              \<lbrace>\<lambda>_. P\<rbrace>"
  assumes eb: "\<And>b n'. n' \<le> n + length caps \<Longrightarrow> \<lbrace>P\<rbrace> set_extra_badge buffer b n' \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>\<lambda>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x \<in> set slots. real_cte_at x s) \<and>
              (\<forall>x \<in> set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and>
                              cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x
                                              \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace>
              transfer_caps_loop ep buffer n caps slots mi
              \<lbrace>\<lambda>_. P\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_pres_dest_aux [OF x eb]) apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>b n'. n' \<le> ?N3 \<Longrightarrow> n' \<le> n + length caps
 2. n + length caps \<le> ?N3
 3. \<And>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) \<Longrightarrow> P s \<and> set slots \<subseteq> set slots \<and> set caps \<subseteq> set caps \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) proof (prove)
goal (2 subgoals):
 1. n + length caps \<le> n + length caps
 2. \<And>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) \<Longrightarrow> P s \<and> set slots \<subseteq> set slots \<and> set caps \<subseteq> set caps \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) \<Longrightarrow> P s \<and> set slots \<subseteq> set slots \<and> set caps \<subseteq> set caps \<and> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> real_cte_at (snd x) s \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<and> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s) proof (prove)
goal:
No subgoals!