theory Untyped_AI

lemma cap_to_protected:
  "\<lbrakk> ex_cte_cap_wp_to P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s;
     descendants_range (UntypedCap dev ptr bits idx) p' s; invs s \<rbrakk>
     \<Longrightarrow> ex_cte_cap_wp_to P p (detype {ptr .. ptr + 2 ^ bits - 1} s)" apply (clarsimp simp: ex_cte_cap_wp_to_def, simp add: detype_def descendants_range_def2) apply (intro exI conjI, assumption) apply (case_tac "a = fst p") apply (frule(1) ex_cte_cap_protects
     [rotated,where P=P]) apply clarsimp+ apply (simp add: ex_cte_cap_wp_to_def) apply fastforce+ apply (drule(2) unsafe_protected[rotated]) apply simp+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply auto 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 (UntypedCap dev ptr bits idx) p' s; invs s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P p (detype {ptr..ptr + 2 ^ bits - 1} s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>b. cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s) \<and> (ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ bits - 1} \<subseteq> untyped_range (UntypedCap dev ptr bits idx)
 3. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p\<rbrakk> \<Longrightarrow> valid_global_refs s
 4. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P (?p6 a b) s
 5. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p; fst (?p6 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1
 6. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (fst p, b) s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P (?p6 (fst p) b) s
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p; fst (?p6 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (fst p, b) s\<rbrakk> \<Longrightarrow> \<exists>a ba. cte_wp_at (\<lambda>c. P c \<and> ?p6 (fst p) b \<in> cte_refs c (interrupt_irq_node s)) (a, ba) s
 2. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a = fst p; fst (?p6 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1
 3. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> {ptr..ptr + 2 ^ bits - 1} \<subseteq> untyped_range (UntypedCap dev ptr bits idx)
 2. \<And>a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p; ?P31 a b cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 3. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> cte_wp_at (?P31 a b) (?p31 a b) s
 4. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p; fst (?p31 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap) (?p31 a b) s
 2. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p; fst (?p31 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; a \<noteq> fst p; caps_of_state s (a, b) = Some cap; P cap; p \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (?p31 a b) = Some cap \<and> cap \<noteq> NullCap
 2. \<And>a b. \<lbrakk>descendants_range_in {ptr..ptr + 2 ^ bits - 1} p' s; invs s; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; a \<noteq> fst p; fst (?p31 a b) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> ptr \<le> a \<longrightarrow> \<not> a \<le> ptr + 2 ^ bits - 1 proof (prove)
goal:
No subgoals!