theory Ipc_R

lemma transferCapsToSlots_mdb[wp]:
  "\<lbrace>\<lambda>s. valid_pspace' s \<and> distinct slots
          \<and> length slots \<le> 1
          \<and> (\<forall>x \<in> set slots. ex_cte_cap_to' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) x s)
          \<and> (\<forall>x \<in> set slots. real_cte_at' x s)
          \<and> transferCaps_srcs caps s\<rbrace>
    transferCapsToSlots ep buffer n caps slots mi
   \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply clarsimp apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp apply (clarsimp simp: valid_pspace'_def) apply (clarsimp simp:cte_wp_at_ctes_of) apply (drule(1) bspec,clarify) apply (case_tac cte) apply (clarsimp dest!:ctes_of_valid_cap' split:if_splits) apply (fastforce simp:valid_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap src dest s. valid_mdb' s \<and> (True \<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> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<Longrightarrow> (valid_mdb' and pspace_aligned' and pspace_distinct' and (\<lambda>s. src \<noteq> dest) and K (capAligned cap) and valid_objs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s
 2. \<And>b n. \<lbrace>valid_mdb'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_mdb'\<rbrace>
 3. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> valid_mdb' s \<and> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (True \<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 (3 subgoals):
 1. \<And>cap src dest s. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; valid_objs' s; valid_cap' cap s; real_cte_at' dest s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src s; valid_mdb' s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> src \<noteq> dest \<and> capAligned cap
 2. \<And>b n. \<lbrace>valid_mdb'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_mdb'\<rbrace>
 3. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> valid_mdb' s \<and> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (True \<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 (3 subgoals):
 1. \<And>cap src dest s. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s; ex_cte_cap_wp_to' (\<lambda>_. True) dest s; valid_objs' s; valid_cap' cap s; real_cte_at' dest s; cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s; cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src s; valid_mdb' s; pspace_aligned' s; pspace_distinct' s; capAligned cap\<rbrakk> \<Longrightarrow> src \<noteq> dest \<and> capAligned cap
 2. \<And>b n. \<lbrace>valid_mdb'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_mdb'\<rbrace>
 3. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> valid_mdb' s \<and> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (True \<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 (2 subgoals):
 1. \<And>b n. \<lbrace>valid_mdb'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_mdb'\<rbrace>
 2. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> valid_mdb' s \<and> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (True \<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 (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> distinct slots \<and> length slots \<le> 1 \<and> (\<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> (\<forall>x\<in>set slots. real_cte_at' x s) \<and> (\<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s) \<Longrightarrow> valid_mdb' s \<and> (True \<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> (True \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<and> (True \<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 (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> set caps; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; distinct slots; length slots \<le> Suc 0; \<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; \<forall>x\<in>set slots. real_cte_at' x s; \<forall>x\<in>set caps. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s\<rbrakk> \<Longrightarrow> valid_cap' a s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> set caps; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); \<forall>x\<in>set slots. real_cte_at' x s; \<forall>x\<in>set caps. \<exists>cte. ctes_of s (snd x) = Some cte \<and> (fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x)\<rbrakk> \<Longrightarrow> valid_cap' a s proof (prove)
goal (1 subgoal):
 1. \<And>s a b cte. \<lbrakk>(a, b) \<in> set caps; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); \<forall>x\<in>set slots. real_cte_at' x s; ctes_of s (snd (a, b)) = Some cte; fst (a, b) \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst (a, b)\<rbrakk> \<Longrightarrow> valid_cap' a s proof (prove)
goal (1 subgoal):
 1. \<And>s a b cte x1 x2. \<lbrakk>(a, b) \<in> set caps; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); \<forall>x\<in>set slots. real_cte_at' x s; ctes_of s (snd (a, b)) = Some cte; fst (a, b) \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst (a, b); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' a s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x1. \<lbrakk>(a, b) \<in> set caps; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. ex_cte_cap_wp_to' (\<lambda>_. True) x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); \<forall>x\<in>set slots. real_cte_at' x s; a \<noteq> capability.NullCap \<longrightarrow> x1 = a; valid_cap' x1 s\<rbrakk> \<Longrightarrow> valid_cap' a s proof (prove)
goal:
No subgoals!