theory Invariants_AI

lemma valid_objs_caps_contained:
  "\<lbrakk> valid_objs s; pspace_aligned s \<rbrakk> \<Longrightarrow> caps_contained s" unfolding caps_contained_def apply (intro allI impI) apply (drule (1) cte_wp_at_valid_objs_valid_cap) apply (drule (1) cte_wp_at_valid_objs_valid_cap) apply clarsimp apply (case_tac c, simp_all) apply (erule disjE) apply (clarsimp simp: valid_cap_def is_cap_simps) apply (clarsimp simp: valid_untyped_T) apply (simp add: cap_table_at_typ) apply (erule allE, erule allE, erule (1) impE) apply (drule (2) typ_at_range) apply (clarsimp simp: typ_range_def obj_bits_type_def) apply fastforce apply (clarsimp simp: valid_cap_def is_cap_simps) apply (clarsimp simp: valid_untyped_T) apply (simp add: tcb_at_typ) apply (erule allE, erule allE, erule (1) impE) apply (drule (2) typ_at_range) apply (clarsimp simp: typ_range_def obj_bits_type_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> caps_contained s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>c p c' p'. cte_wp_at ((=) c) p s \<longrightarrow> cte_wp_at ((=) c') p' s \<longrightarrow> obj_ref_of c' \<in> untyped_range c \<longrightarrow> is_cnode_cap c' \<or> is_thread_cap c' \<longrightarrow> obj_ref_of c' + obj_size c' - 1 \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>c p c' p'. \<lbrakk>valid_objs s; pspace_aligned s; cte_wp_at ((=) c) p s; cte_wp_at ((=) c') p' s; obj_ref_of c' \<in> untyped_range c; is_cnode_cap c' \<or> is_thread_cap c'\<rbrakk> \<Longrightarrow> obj_ref_of c' + obj_size c' - 1 \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>c p c' p'. \<lbrakk>valid_objs s; pspace_aligned s; cte_wp_at ((=) c') p' s; obj_ref_of c' \<in> untyped_range c; is_cnode_cap c' \<or> is_thread_cap c'; \<exists>cap. c = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> obj_ref_of c' + obj_size c' - 1 \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>c p c' p'. \<lbrakk>valid_objs s; pspace_aligned s; obj_ref_of c' \<in> untyped_range c; is_cnode_cap c' \<or> is_thread_cap c'; \<exists>cap. c = cap \<and> s \<turnstile> cap; \<exists>cap. c' = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> obj_ref_of c' + obj_size c' - 1 \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>valid_objs s; pspace_aligned s; obj_ref_of c' \<in> untyped_range c; is_cnode_cap c' \<or> is_thread_cap c'; s \<turnstile> c; s \<turnstile> c'\<rbrakk> \<Longrightarrow> obj_ref_of c' + obj_size c' - 1 \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; is_cnode_cap c' \<or> is_thread_cap c'; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_cnode_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; cap_table_at bits r s; 0 < bits; length g \<le> word_bits\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1 \<and> r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); \<forall>T p. typ_at T p s \<longrightarrow> typ_range p T \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range p T \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range p T \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; cap_table_at bits r s; 0 < bits; length g \<le> word_bits\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1 \<and> r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); \<forall>T p. typ_at T p s \<longrightarrow> typ_range p T \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range p T \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range p T \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; typ_at (ACapTable bits) r s; 0 < bits; length g \<le> word_bits\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1 \<and> r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; typ_at (ACapTable bits) r s; 0 < bits; length g \<le> word_bits; typ_range r (ACapTable bits) \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range r (ACapTable bits) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range r (ACapTable bits) \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1 \<and> r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; 0 < bits; length g \<le> word_bits; typ_range r (ACapTable bits) \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range r (ACapTable bits) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range r (ACapTable bits) \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; typ_range r (ACapTable bits) \<noteq> {}\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1 \<and> r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24 r bits g. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (CNodeCap r bits g); untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; 0 < bits; length g \<le> word_bits; r \<le> r + 2 ^ (cte_level_bits + bits) - 1; r + 2 ^ (cte_level_bits + bits) - 1 \<le> x22 + 2 ^ x23 - 1; {r..r + 2 ^ (cte_level_bits + bits) - 1} \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}\<rbrakk> \<Longrightarrow> x22 \<le> r + 2 ^ (cte_level_bits + bits) - 1
 2. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>c c' x21 x22 x23 x24. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> obj_ref_of c' \<and> obj_ref_of c' \<le> x22 + 2 ^ x23 - 1; s \<turnstile> UntypedCap x21 x22 x23 x24; s \<turnstile> c'; c = UntypedCap x21 x22 x23 x24; is_thread_cap c'\<rbrakk> \<Longrightarrow> x22 \<le> obj_ref_of c' + obj_size c' - 1 \<and> obj_ref_of c' + obj_size c' - 1 \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); tcb_at r s; valid_untyped (UntypedCap x21 x22 x23 x24) s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r \<and> 0x1FF + r \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); tcb_at r s; \<forall>T p. typ_at T p s \<longrightarrow> typ_range p T \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range p T \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range p T \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r \<and> 0x1FF + r \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); typ_at ATCB r s; \<forall>T p. typ_at T p s \<longrightarrow> typ_range p T \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range p T \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range p T \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r \<and> 0x1FF + r \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); typ_at ATCB r s; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; typ_range r ATCB \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range r ATCB \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range r ATCB \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r \<and> 0x1FF + r \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; typ_range r ATCB \<inter> {x22..x22 + 2 ^ x23 - 1} = {} \<or> typ_range r ATCB \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> typ_range r ATCB \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}; typ_range r ATCB \<noteq> {}\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r \<and> 0x1FF + r \<le> x22 + 2 ^ x23 - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23 x24 r. \<lbrakk>valid_objs s; pspace_aligned s; x22 \<le> r; r \<le> x22 + 2 ^ x23 - 1; cap_aligned (UntypedCap x21 x22 x23 x24); cap_aligned (ThreadCap r); untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; r \<le> 0x1FF + r; 0x1FF + r \<le> x22 + 2 ^ x23 - 1; {r..0x1FF + r} \<inter> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) = {}\<rbrakk> \<Longrightarrow> x22 \<le> 0x1FF + r proof (prove)
goal:
No subgoals!