theory Ipc_R

lemma transferCapsToSlots_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned'
         and K(distinct slots \<and> length slots \<le> 1)
         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 transferCaps_srcs caps\<rbrace>
     transferCapsToSlots ep buffer n caps slots mi
  \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp apply (clarsimp simp:cte_wp_at_ctes_of | intro ballI conjI)+ apply (drule(1) bspec,clarsimp) apply (case_tac cte,clarsimp) apply (frule(1) CSpace_I.ctes_of_valid_cap') apply (fastforce simp:valid_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned' and K (distinct slots \<and> length slots \<le> 1) 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. 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_irq_handlers'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap src dest s. valid_irq_handlers' 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> (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> (False \<longrightarrow> pspace_aligned' s \<and> pspace_distinct' s) \<Longrightarrow> valid_irq_handlers' s \<and> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)
 2. \<And>b n. \<lbrace>valid_irq_handlers'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_irq_handlers'\<rbrace>
 3. \<And>s. (valid_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned' and K (distinct slots \<and> length slots \<le> 1) 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. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)) s \<Longrightarrow> valid_irq_handlers' 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> (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>src dest s irq cte. \<lbrakk>valid_irq_handlers' s; valid_objs' s; valid_cap' (capability.IRQHandlerCap irq) s; real_cte_at' dest s; valid_mdb' s; ctes_of s src = Some cte; untyped_derived_eq (capability.IRQHandlerCap irq) (capability.IRQHandlerCap irq); \<not> isZombie (capability.IRQHandlerCap irq); \<not> isIRQControlCap (capability.IRQHandlerCap irq); \<not> isReplyCap (capability.IRQHandlerCap irq); cteCap cte = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> irq_issued' irq s
 2. \<And>b n. \<lbrace>valid_irq_handlers'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_irq_handlers'\<rbrace>
 3. \<And>s. (valid_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned' and K (distinct slots \<and> length slots \<le> 1) 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. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)) s \<Longrightarrow> valid_irq_handlers' 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> (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_irq_handlers'\<rbrace> setExtraBadge buffer b n \<lbrace>\<lambda>_. valid_irq_handlers'\<rbrace>
 2. \<And>s. (valid_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned' and K (distinct slots \<and> length slots \<le> 1) 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. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)) s \<Longrightarrow> valid_irq_handlers' 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> (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_irq_handlers' and valid_objs' and valid_mdb' and pspace_distinct' and pspace_aligned' and K (distinct slots \<and> length slots \<le> 1) 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. cte_wp_at' (\<lambda>cte. fst x \<noteq> capability.NullCap \<longrightarrow> cteCap cte = fst x) (snd x) s)) s \<Longrightarrow> valid_irq_handlers' 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> (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_irq_handlers' s; valid_objs' s; valid_mdb' s; pspace_distinct' s; pspace_aligned' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); \<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_irq_handlers' s; valid_objs' s; valid_mdb' s; pspace_distinct' s; pspace_aligned' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); 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; valid_irq_handlers' s; valid_objs' s; valid_mdb' s; pspace_distinct' s; pspace_aligned' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); 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; valid_irq_handlers' s; valid_objs' s; valid_mdb' s; pspace_distinct' s; pspace_aligned' s; distinct slots; length slots \<le> Suc 0; \<forall>x\<in>set slots. real_cte_at' x s \<and> (\<exists>cte. ctes_of s x = Some cte \<and> cteCap cte = capability.NullCap); 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!