theory KHeap_DR

lemma final_cap_set_map:
  "\<lbrakk>valid_idle s'; valid_irq_node s';valid_objs s';if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk>
    \<Longrightarrow> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap'
                                    \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')}
    = transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}" apply (rule set_eqI) apply (rule iffI) apply (clarsimp simp: image_def) apply (drule cap_counts_inv[rotated]) apply simp+ apply clarsimp apply (rule_tac x=aa in exI) apply (rule_tac x=ba in exI) apply simp+ apply (erule cte_wp_at_weakenE_customised) 
   (*defer till the otherway around comes up*)
    defer apply (clarsimp simp:image_def opt_cap_wp_at_def') apply (drule iffD1[OF cte_wp_at_caps_of_state]) apply clarsimp apply (frule caps_of_state_transform_opt_cap, simp) apply clarsimp apply (frule valid_idle_has_null_cap) 
        (*It is true since idle thread should not get any cap installed *)
         apply simp+ apply (thin_tac "opt_cap x y = Q" for x y Q) by (auto simp: transform_cap_def cap_has_object_def cap_counts_def cdl_cap_irq_def
            split: cap.splits arch_cap.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk> \<Longrightarrow> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} = transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk> \<Longrightarrow> (x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')}) = (x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')}\<rbrakk> \<Longrightarrow> x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') (a, b) (transform s')\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s' \<and> (a, b) = transform_cslot_ptr (aa, ba)
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk> \<Longrightarrow> valid_objs s'
 2. \<And>a b. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'\<rbrakk> \<Longrightarrow> valid_etcbs s'
 3. \<And>a b capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; cap_object (transform_cap cap) = cap_object capa \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq capa \<and> cap_counts capa\<rbrakk> \<Longrightarrow> cap_counts capa
 4. \<And>a b. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; \<exists>slot'. (a, b) = transform_cslot_ptr slot' \<and> cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) slot' s'\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s' \<and> (a, b) = transform_cslot_ptr (aa, ba)
 5. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; \<exists>aa ba. (a, b) = transform_cslot_ptr (aa, ba) \<and> cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) (aa, ba) s'\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s' \<and> (a, b) = transform_cslot_ptr (aa, ba)
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) (aa, ba) s'\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (a, b) s' \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b)
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) (aa, ba) s'\<rbrakk> \<Longrightarrow> \<exists>b. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, b) s' \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (aa, b)
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) (aa, ba) s'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s' \<and> transform_cslot_ptr (aa, ba) = transform_cslot_ptr (aa, ba)
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cte_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object (transform_cap cap') \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap cap') \<and> cap_counts (transform_cap cap')) (aa, ba) s'\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s'
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}
 2. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; x \<in> transform_cslot_ptr ` {cref. cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) cref s'}\<rbrakk> \<Longrightarrow> x \<in> {cref. opt_cap_wp_at (\<lambda>cap'. cap_object (transform_cap cap) = cap_object cap' \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq cap' \<and> cap_counts cap') cref (transform s')}
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; cte_wp_at (\<lambda>cap'. cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) (aa, ba) s'; (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); \<exists>capa. caps_of_state s' (aa, ba) = Some capa \<and> (cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {})\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> fst (aa, ba) \<noteq> idle_thread s'
 2. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; opt_cap (transform_cslot_ptr (aa, ba)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 3. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (3 subgoals):
 1. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; opt_cap (transform_cslot_ptr (aa, ba)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 3. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (7 subgoals):
 1. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_global_refs s'
 2. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_idle s'
 3. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_irq_node s'
 4. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s' (idle_thread s', ?v41 a b ba capa) = Some (?cap41 a b ba capa)
 5. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; ?cap41 a b ba capa = cap.NullCap\<rbrakk> \<Longrightarrow> False
 6. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; opt_cap (transform_cslot_ptr (aa, ba)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 7. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (7 subgoals):
 1. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_global_refs s'
 2. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_idle s'
 3. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> valid_irq_node s'
 4. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s' (idle_thread s', ?v41 a b ba capa) = Some (?cap41 a b ba capa)
 5. \<And>a b ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (idle_thread s', ba); caps_of_state s' (idle_thread s', ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; ?cap41 a b ba capa = cap.NullCap\<rbrakk> \<Longrightarrow> False
 6. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; opt_cap (transform_cslot_ptr (aa, ba)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> case opt_cap (transform_cslot_ptr (aa, ba)) (transform s') of None \<Rightarrow> False | Some a \<Rightarrow> cap_object (transform_cap cap) = cap_object a \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq a \<and> cap_counts a
 7. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; opt_cap (transform_cslot_ptr (aa, ba)) (transform s') = Some (transform_cap capa)\<rbrakk> \<Longrightarrow> cap_object (transform_cap cap) = cap_object (transform_cap capa) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap capa) \<and> cap_counts (transform_cap capa)
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {} proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba capa. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s' (aa, ba) = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}\<rbrakk> \<Longrightarrow> cap_object (transform_cap cap) = cap_object (transform_cap capa) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap capa) \<and> cap_counts (transform_cap capa)
 2. \<And>a b aa ba c. \<lbrakk>valid_idle s'; valid_irq_node s'; valid_objs s'; if_unsafe_then_cap s'; valid_global_refs s'; cap_counts (transform_cap cap); valid_etcbs s'; (a, b) = transform_cslot_ptr (aa, ba); cap_object (transform_cap cap) = cap_object (transform_cap c) \<and> cdl_cap_irq (transform_cap cap) = cdl_cap_irq (transform_cap c) \<and> cap_counts (transform_cap c); cte_wp_at ((=) c) (aa, ba) s'\<rbrakk> \<Longrightarrow> cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}