theory Ipc_AI

lemma transfer_caps_loop_valid_mdb[wp]:
  "\<And>slots caps ep buffer n mi.
    \<lbrace>\<lambda>s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s
         \<and> (\<forall>slot \<in> set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap) slot s)
         \<and> transfer_caps_srcs caps s \<and> distinct slots\<rbrace>
      transfer_caps_loop ep buffer n caps slots mi
    \<lbrace>\<lambda>rv. valid_mdb :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (rule hoare_pre) apply (rule transfer_caps_loop_presM[where vo=True and em=True and ex=False]) apply wp apply (clarsimp simp: cte_wp_at_caps_of_state) apply (wp set_extra_badge_valid_mdb) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule(1) bspec)+ apply clarsimp apply (drule(1) caps_of_state_valid) apply (case_tac "a = cap.NullCap") apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slots caps ep buffer n mi. \<lbrace>\<lambda>s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>slots caps ep buffer n mi. \<lbrace>?Q slots caps ep buffer n mi\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_mdb\<rbrace>
 2. \<And>slots caps ep buffer n mi s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots \<Longrightarrow> ?Q slots caps ep buffer n mi s proof (prove)
goal (3 subgoals):
 1. \<And>slots caps ep buffer n mi cap src dest. \<lbrace>\<lambda>s. valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb 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) \<and> (True \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_mdb\<rbrace>
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_mdb\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_mdb\<rbrace>
 3. \<And>slots caps ep buffer n mi s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots \<Longrightarrow> valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (3 subgoals):
 1. \<And>slots caps ep buffer n mi cap src dest s. valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb 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) \<and> (True \<longrightarrow> cte_wp_at ((=) NullCap) dest s) \<and> (False \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) dest s) \<Longrightarrow> (valid_mdb and valid_cap cap and valid_objs and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s) and K (src \<noteq> dest)) s
 2. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_mdb\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_mdb\<rbrace>
 3. \<And>slots caps ep buffer n mi s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots \<Longrightarrow> valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (2 subgoals):
 1. \<And>slots caps ep buffer n mi b na. \<lbrace>valid_mdb\<rbrace> set_extra_badge buffer b na \<lbrace>\<lambda>_. valid_mdb\<rbrace>
 2. \<And>slots caps ep buffer n mi s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots \<Longrightarrow> valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps ep buffer n mi s. valid_mdb s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>slot\<in>set slots. real_cte_at slot s \<and> cte_wp_at (\<lambda>cap. cap = NullCap) slot s) \<and> (\<forall>x\<in>set caps. cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp = fst x) (snd x) s \<and> real_cte_at (snd x) s) \<and> distinct slots \<Longrightarrow> valid_mdb s \<and> (True \<longrightarrow> valid_objs s \<and> valid_mdb s \<and> distinct slots \<and> (\<forall>x\<in>set slots. cte_wp_at (\<lambda>cap. cap = NullCap) x s \<and> real_cte_at x s) \<and> (\<forall>x\<in>set caps. s \<turnstile> fst x \<and> cte_wp_at (\<lambda>cp. fst x \<noteq> NullCap \<longrightarrow> cp \<noteq> fst x \<longrightarrow> cp = masked_as_full (fst x) (fst x)) (snd x) s \<and> real_cte_at (snd x) s)) \<and> (False \<longrightarrow> (\<forall>x\<in>set slots. ex_cte_cap_wp_to is_cnode_cap x s)) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; \<forall>x\<in>set caps. (\<exists>cap. caps_of_state s (snd x) = Some cap \<and> (fst x \<noteq> NullCap \<longrightarrow> cap = fst x)) \<and> real_cte_at (snd x) s; distinct slots\<rbrakk> \<Longrightarrow> s \<turnstile> a \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; distinct slots; (\<exists>cap. caps_of_state s (snd (a, aa, b)) = Some cap \<and> (fst (a, aa, b) \<noteq> NullCap \<longrightarrow> cap = fst (a, aa, b))) \<and> real_cte_at (snd (a, aa, b)) s\<rbrakk> \<Longrightarrow> s \<turnstile> a \<and> (\<exists>cap. caps_of_state s (aa, b) = Some cap \<and> (a \<noteq> NullCap \<longrightarrow> cap \<noteq> a \<longrightarrow> cap = masked_as_full a a)) proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; distinct slots; cap_table_at (length b) aa s; caps_of_state s (aa, b) = Some cap; a \<noteq> NullCap \<longrightarrow> cap = a\<rbrakk> \<Longrightarrow> s \<turnstile> a proof (prove)
goal (1 subgoal):
 1. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; distinct slots; cap_table_at (length b) aa s; a \<noteq> NullCap \<longrightarrow> cap = a; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> a proof (prove)
goal (2 subgoals):
 1. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; distinct slots; cap_table_at (length b) aa s; a \<noteq> NullCap \<longrightarrow> cap = a; s \<turnstile> cap; a = NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> a
 2. \<And>slots caps s a aa b cap. \<lbrakk>(a, aa, b) \<in> set caps; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; \<forall>slot\<in>set slots. real_cte_at slot s \<and> caps_of_state s slot = Some NullCap; distinct slots; cap_table_at (length b) aa s; a \<noteq> NullCap \<longrightarrow> cap = a; s \<turnstile> cap; a \<noteq> NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> a proof (prove)
goal:
No subgoals!