theory Ipc_R

lemma tcts_zero_ranges[wp]:
  "\<lbrace>\<lambda>s. untyped_ranges_zero' s \<and> valid_pspace' s \<and> distinct slots
          \<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> length slots \<le> 1
          \<and> transferCaps_srcs caps s\<rbrace>
    transferCapsToSlots ep buffer n caps slots mi
  \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (wp transferCapsToSlots_presM[where emx=True and vo=True
      and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) apply (simp add: o_def) apply (clarsimp simp: valid_pspace'_def ball_conj_distrib[symmetric]) apply (drule(1) bspec) apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, clarsimp) apply (frule(1) ctes_of_valid_cap') apply auto[1] done

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