theory Untyped_AI

lemma detype_valid_untyped:
  "\<lbrakk>invs s; detype S s \<turnstile> UntypedCap dev ptr sz idx1;
    {ptr .. ptr + 2 ^ sz - 1} \<subseteq> S; idx2 \<le> 2 ^ sz\<rbrakk>
   \<Longrightarrow> detype S s \<turnstile> UntypedCap dev ptr sz idx2" apply (clarsimp simp: detype_def valid_cap_def valid_untyped_def cap_aligned_def) apply (drule_tac x = p in spec) apply clarsimp apply (drule p_in_obj_range) apply (simp add: invs_psp_aligned invs_valid_objs)+ apply (drule(1) subset_trans[rotated]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; detype S s \<turnstile> UntypedCap dev ptr sz idx1; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; idx2 \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> detype S s \<turnstile> UntypedCap dev ptr sz idx2 proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; \<forall>p obj. (if p \<in> S then None else kheap s p) = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; \<forall>obj. (if p \<in> S then None else kheap s p) = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal (3 subgoals):
 1. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; p \<in> obj_range p obj\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>invs s; {ptr..ptr + 2 ^ sz - 1} \<subseteq> S; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; p \<in> obj_range p obj\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>invs s; is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; idx1 \<le> 2 ^ sz; ptr \<noteq> 0; idx2 < 2 ^ sz; p \<notin> S; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1}; (if idx1 < 2 ^ sz then {ptr + word_of_nat idx1..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; p \<in> obj_range p obj; obj_range p obj \<subseteq> S\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx2..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {} proof (prove)
goal:
No subgoals!