theory Untyped_AI

lemma unsafe_protected:
  "\<lbrakk> cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s;
     descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx);
     \<And>cap. P cap \<Longrightarrow> cap \<noteq> cap.NullCap \<rbrakk>
     \<Longrightarrow> fst p \<notin> S" apply (rule ex_cte_cap_protects) apply (erule if_unsafe_then_capD) apply (clarsimp simp: invs_def valid_state_def) apply simp apply assumption+ apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> fst p \<notin> S proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to ?P p ?s
 2. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap ?dev ?ptr ?bits ?idx)) ?p' ?s
 3. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> descendants_range_in S ?p' ?s
 4. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> untyped_children_in_mdb ?s
 5. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> S \<subseteq> untyped_range (UntypedCap ?dev ?ptr ?bits ?idx)
 6. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_global_refs ?s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 2. \<And>cap. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap; P cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 3. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap ?dev ?ptr ?bits ?idx)) ?p' s
 4. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> descendants_range_in S ?p' s
 5. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 6. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> S \<subseteq> untyped_range (UntypedCap ?dev ?ptr ?bits ?idx)
 7. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_global_refs s proof (prove)
goal (6 subgoals):
 1. \<And>cap. \<lbrakk>cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap; P cap\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 2. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap ?dev ?ptr ?bits ?idx)) ?p' s
 3. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> descendants_range_in S ?p' s
 4. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 5. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> S \<subseteq> untyped_range (UntypedCap ?dev ?ptr ?bits ?idx)
 6. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_global_refs s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap ?dev ?ptr ?bits ?idx)) ?p' s
 2. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> descendants_range_in S ?p' s
 3. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 4. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> S \<subseteq> untyped_range (UntypedCap ?dev ?ptr ?bits ?idx)
 5. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_global_refs s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> untyped_children_in_mdb s
 2. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> S \<subseteq> untyped_range (UntypedCap dev ptr bits idx)
 3. \<lbrakk>cte_wp_at P p s; cte_wp_at ((=) (UntypedCap dev ptr bits idx)) p' s; descendants_range_in S p' s; invs s; S \<subseteq> untyped_range (UntypedCap dev ptr bits idx); \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> valid_global_refs s proof (prove)
goal:
No subgoals!