theory Untyped_R

lemma zipWithM_x_insertNewCap_invs'':
  "\<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup \<in> set ls. s \<turnstile>' snd tup)
        \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and>
                            (\<forall>tup \<in> set ls. sameRegionAs (cteCap cte) (snd tup))) parent s
        \<and> (\<forall>tup \<in> set ls. \<not> isZombie (snd tup))
        \<and> (\<forall>tup \<in> set ls. ex_cte_cap_to' (fst tup) s)
        \<and> (\<forall>tup \<in> set ls. descendants_range' (snd tup) parent (ctes_of s))
        \<and> (\<forall>tup \<in> set ls. ksIdleThread s \<notin> capRange (snd tup))
        \<and> (\<forall>tup \<in> set ls. caps_overlap_reserved' (capRange (snd tup)) s)
        \<and> distinct_sets (map capRange (map snd ls))
        \<and> (\<forall>irq. IRQHandlerCap irq \<in> set (map snd ls) \<longrightarrow> irq_issued' irq s)
        \<and> distinct (map fst ls)\<rbrace>
    mapM (\<lambda>(x, y). insertNewCap parent x y) ls
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (induct ls) apply (simp add: mapM_def sequence_def) apply (wp, simp) apply (simp add: mapM_Cons) including no_pre apply wp apply (thin_tac "valid P f Q" for P f Q) apply clarsimp apply (rule hoare_pre) apply (wp insertNewCap_invs'
             hoare_vcg_const_Ball_lift
             insertNewCap_cte_wp_at' insertNewCap_ranges
             hoare_vcg_all_lift insertNewCap_pred_tcb_at')+ apply (clarsimp simp: cte_wp_at_ctes_of invs_mdb' invs_valid_objs' dest!:valid_capAligned) apply (drule caps_overlap_reserved'_subseteq[OF _ untypedRange_in_capRange]) apply (auto simp:comp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd ls)) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd ls) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>(x, y). insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set []. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set []. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set []. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set []. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set []. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set []. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set []. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd [])) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd []) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst [])\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) [] \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd ls)) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd ls) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set (a # ls). valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (a # ls). global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set (a # ls). \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set (a # ls). descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set (a # ls). ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd (a # ls))) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd (a # ls)) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst (a # ls))\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) (a # ls) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte)) parent s\<rbrace> return [] \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd ls)) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd ls) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set (a # ls). valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (a # ls). global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set (a # ls). \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set (a # ls). descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set (a # ls). ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd (a # ls))) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd (a # ls)) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst (a # ls))\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) (a # ls) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd ls)) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd ls) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set (a # ls). valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set (a # ls). global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set (a # ls). \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set (a # ls). descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set (a # ls). ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set (a # ls). caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map capRange (map snd (a # ls))) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> set (map snd (a # ls)) \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst (a # ls))\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) (a # ls) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> valid_cap' (snd a) s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd a) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie (snd a) \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (fst a) s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' (snd a) parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange (snd a) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange (snd a)) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange (snd a) \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = snd a \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> fst a \<notin> fst ` set ls \<and> distinct (map fst ls)\<rbrace> do y <- case a of (x, xa) \<Rightarrow> insertNewCap parent x xa;
ys <- mapM (\<lambda>(x, y). insertNewCap parent x y) ls;
return (() # ys)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> valid_cap' (snd a) s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd a) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie (snd a) \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (fst a) s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' (snd a) parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange (snd a) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange (snd a)) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange (snd a) \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = snd a \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> fst a \<notin> fst ` set ls \<and> distinct (map fst ls)\<rbrace> do y <- case a of (x, xa) \<Rightarrow> insertNewCap parent x xa;
ys <- mapM (\<lambda>(x, y). insertNewCap parent x y) ls;
return (() # ys)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> mapM (\<lambda>a. case a of (x, y) \<Rightarrow> insertNewCap parent x y) ls \<lbrace>\<lambda>rv. invs'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> valid_cap' (snd a) s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd a) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie (snd a) \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (fst a) s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' (snd a) parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange (snd a) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange (snd a)) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange (snd a) \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = snd a \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> fst a \<notin> fst ` set ls \<and> distinct (map fst ls)\<rbrace> case a of (x, xa) \<Rightarrow> insertNewCap parent x xa \<lbrace>\<lambda>x s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> valid_cap' (snd a) s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) (snd a) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie (snd a) \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) (fst a) s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' (snd a) parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange (snd a) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange (snd a)) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange (snd a) \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = snd a \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> fst a \<notin> fst ` set ls \<and> distinct (map fst ls)\<rbrace> case a of (x, xa) \<Rightarrow> insertNewCap parent x xa \<lbrace>\<lambda>x s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b ls. \<lbrace>\<lambda>s. invs' s \<and> ct_active' s \<and> valid_cap' b s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie b \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) a s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' b parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange b \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange b) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange b \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = b \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> a \<notin> fst ` set ls \<and> distinct (map fst ls)\<rbrace> insertNewCap parent a b \<lbrace>\<lambda>x s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b ls. \<lbrace>?Q18 a b ls\<rbrace> insertNewCap parent a b \<lbrace>\<lambda>x s. invs' s \<and> ct_active' s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s) \<and> distinct (map fst ls)\<rbrace>
 2. \<And>a b ls s. invs' s \<and> ct_active' s \<and> valid_cap' b s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie b \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) a s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' b parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange b \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange b) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange b \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = b \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> a \<notin> fst ` set ls \<and> distinct (map fst ls) \<Longrightarrow> ?Q18 a b ls s proof (prove)
goal (1 subgoal):
 1. \<And>a b ls s. invs' s \<and> ct_active' s \<and> valid_cap' b s \<and> (\<forall>tup\<in>set ls. valid_cap' (snd tup) s) \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent s \<and> \<not> isZombie b \<and> (\<forall>tup\<in>set ls. \<not> isZombie (snd tup)) \<and> ex_cte_cap_wp_to' (\<lambda>_. True) a s \<and> (\<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s) \<and> descendants_range' b parent (ctes_of s) \<and> (\<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s)) \<and> ksIdleThread s \<notin> capRange b \<and> (\<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup)) \<and> caps_overlap_reserved' (capRange b) s \<and> (\<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s) \<and> capRange b \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {} \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>irq. (capability.IRQHandlerCap irq = b \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s)) \<and> a \<notin> fst ` set ls \<and> distinct (map fst ls) \<Longrightarrow> (invs' and ct_active' and valid_cap' b and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b) parent and K (\<not> isZombie b) and (\<lambda>s. descendants_range' b parent (ctes_of s)) and caps_overlap_reserved' (untypedRange b) and ex_cte_cap_wp_to' (\<lambda>_. True) a and (\<lambda>s. ksIdleThread s \<notin> capRange b) and (\<lambda>s. \<forall>irq. b = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)) s \<and> ct_active' s \<and> (\<forall>x\<in>set ls. valid_cap' (snd x) s) \<and> (cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> (\<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup))) parent and K (\<not> (isUntypedCap capability.NullCap \<and> (\<forall>tup\<in>set ls. global.sameRegionAs capability.NullCap (snd tup))))) s \<and> (\<forall>x\<in>set ls. \<not> isZombie (snd x)) \<and> (\<forall>x\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst x) s) \<and> (\<forall>x\<in>set ls. descendants_range' (snd x) parent (ctes_of s) \<and> descendants_range' b parent (ctes_of s) \<and> capRange (snd x) \<inter> capRange b = {} \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b) parent s \<and> valid_mdb' s \<and> valid_objs' s) \<and> (\<forall>x\<in>set ls. ksIdleThread s \<notin> capRange (snd x)) \<and> (\<forall>x\<in>set ls. caps_overlap_reserved' (capRange (snd x)) s \<and> capRange (snd x) \<inter> capRange b = {} \<and> capAligned b \<and> cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> global.sameRegionAs (cteCap cte) b) parent s \<and> valid_mdb' s \<and> valid_objs' s) \<and> distinct_sets (map (capRange \<circ> snd) ls) \<and> (\<forall>x. capability.IRQHandlerCap x \<in> snd ` set ls \<longrightarrow> irq_issued' x s) \<and> distinct (map fst ls) proof (prove)
goal (1 subgoal):
 1. \<And>a b ls s cte. \<lbrakk>invs' s; ct_active' s; capAligned b; \<forall>tup\<in>set ls. valid_cap' (snd tup) s; \<not> isZombie b; ctes_of s parent = Some cte; \<forall>tup\<in>set ls. \<not> isZombie (snd tup); isUntypedCap (cteCap cte); ex_cte_cap_wp_to' (\<lambda>_. True) a s; global.sameRegionAs (cteCap cte) b; \<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup); \<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s; descendants_range' b parent (ctes_of s); \<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s); ksIdleThread s \<notin> capRange b; \<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup); caps_overlap_reserved' (capRange b) s; \<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s; capRange b \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ls); \<forall>irq. (capability.IRQHandlerCap irq = b \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s); a \<notin> fst ` set ls; distinct (map fst ls)\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (untypedRange b) s \<and> (\<forall>x\<in>set ls. capRange (snd x) \<inter> capRange b = {}) \<and> distinct_sets (map (\<lambda>a. capRange (snd a)) ls) proof (prove)
goal (1 subgoal):
 1. \<And>a b ls s cte. \<lbrakk>invs' s; ct_active' s; capAligned b; \<forall>tup\<in>set ls. valid_cap' (snd tup) s; \<not> isZombie b; ctes_of s parent = Some cte; \<forall>tup\<in>set ls. \<not> isZombie (snd tup); isUntypedCap (cteCap cte); ex_cte_cap_wp_to' (\<lambda>_. True) a s; global.sameRegionAs (cteCap cte) b; \<forall>tup\<in>set ls. global.sameRegionAs (cteCap cte) (snd tup); \<forall>tup\<in>set ls. ex_cte_cap_wp_to' (\<lambda>_. True) (fst tup) s; descendants_range' b parent (ctes_of s); \<forall>tup\<in>set ls. descendants_range' (snd tup) parent (ctes_of s); ksIdleThread s \<notin> capRange b; \<forall>tup\<in>set ls. ksIdleThread s \<notin> capRange (snd tup); \<forall>tup\<in>set ls. caps_overlap_reserved' (capRange (snd tup)) s; capRange b \<inter> (\<Union>x\<in>set ls. capRange (snd x)) = {}; distinct_sets (map (capRange \<circ> snd) ls); \<forall>irq. (capability.IRQHandlerCap irq = b \<longrightarrow> irq_issued' irq s) \<and> (capability.IRQHandlerCap irq \<in> snd ` set ls \<longrightarrow> irq_issued' irq s); a \<notin> fst ` set ls; distinct (map fst ls); caps_overlap_reserved' (untypedRange b) s\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (untypedRange b) s \<and> (\<forall>x\<in>set ls. capRange (snd x) \<inter> capRange b = {}) \<and> distinct_sets (map (\<lambda>a. capRange (snd a)) ls) proof (prove)
goal:
No subgoals!