theory Untyped_AI

lemma ex_cte_cap_protects:
  "\<lbrakk> ex_cte_cap_wp_to P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s;
     descendants_range_in S p' s; untyped_children_in_mdb s; S\<subseteq> untyped_range (UntypedCap dev ptr bits idx);
     valid_global_refs s \<rbrakk>
      \<Longrightarrow> fst p \<notin> S" apply (drule ex_cte_cap_to_obj_ref_disj, erule disjE) apply clarsimp apply (erule(1) untyped_children_in_mdbEE[where P="\<lambda>c. fst p \<in> obj_refs c" for c]) apply simp apply assumption apply (rule notemptyI[where x="fst p"]) apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                              Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex) apply blast apply (clarsimp simp:cte_wp_at_caps_of_state) apply (drule(2) descendants_range_inD) apply (clarsimp simp:cap_range_def) apply blast apply clarsimp apply (drule_tac irq=irq in valid_globals_irq_node, assumption) apply (clarsimp simp del:atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_cte_cap_wp_to P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr'. cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) ptr' s\<rbrakk> \<Longrightarrow> fst p \<notin> S
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev ptr bits idx)
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. fst p \<in> obj_refs c) (?ptr'10 a b) s
 3. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (?ptr'10 a b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}
 4. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (?ptr'10 a b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; ?ptr'10 a b \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. fst p \<in> obj_refs c) (?ptr'10 a b) s
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (?ptr'10 a b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}
 3. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (?ptr'10 a b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; ?ptr'10 a b \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (3 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (3 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> fst p \<in> obj_refs cap' \<inter> untyped_range (UntypedCap dev ptr bits idx)
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (3 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; fst p \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> fst p \<in> {ptr..ptr + 2 ^ bits - 1}
 2. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at (\<lambda>cap. fst p \<in> obj_refs cap) (a, b) s; fst p \<in> S; cte_wp_at ((=) cap') (a, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev ptr bits idx) \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>caps_of_state s p' = Some (UntypedCap dev ptr bits idx); descendants_range_in S p' s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; fst p \<in> obj_refs cap'; fst p \<in> S; caps_of_state s (a, b) = Some cap'; cap_range cap' \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>caps_of_state s p' = Some (UntypedCap dev ptr bits idx); S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; fst p \<in> obj_refs cap'; fst p \<in> S; caps_of_state s (a, b) = Some cap'; cap_range cap' \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s); cap_range cap' \<inter> S = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (2 subgoals):
 1. \<And>a b cap'. \<lbrakk>caps_of_state s p' = Some (UntypedCap dev ptr bits idx); S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; fst p \<in> obj_refs cap'; fst p \<in> S; caps_of_state s (a, b) = Some cap'; (untyped_range cap' \<union> obj_refs cap') \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}; (a, b) \<in> descendants_of p' (cdt s); (untyped_range cap' \<union> obj_refs cap') \<inter> S = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); valid_global_refs s; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> p = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (1 subgoal):
 1. \<And>a b irq. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; valid_global_refs s; cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; p = (interrupt_irq_node s irq, []); interrupt_irq_node s irq \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b irq. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; p = (interrupt_irq_node s irq, []); interrupt_irq_node s irq \<in> S; interrupt_irq_node s irq \<notin> cap_range (UntypedCap dev ptr bits idx)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b irq. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; untyped_children_in_mdb s; S \<subseteq> {ptr..ptr + 2 ^ bits - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s; p = (interrupt_irq_node s irq, []); interrupt_irq_node s irq \<in> S; interrupt_irq_node s irq \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!