theory Untyped_AI

lemma cnode_cap_bits_range:
  "\<lbrakk> cte_wp_at P p s; invs s \<rbrakk> \<Longrightarrow>
     (\<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow>
                 (\<lambda>n. n > 0 \<and> n < (word_bits - cte_level_bits) \<and> is_aligned (obj_ref_of c) (n + cte_level_bits)) (bits_of c)))" apply (frule invs_valid_objs) apply (drule(1) cte_wp_at_valid_objs_valid_cap) apply clarsimp apply (rule exI, erule conjI) apply (clarsimp simp: is_cap_simps valid_cap_def bits_of_def) apply (erule (1) obj_at_valid_objsE) apply (case_tac ko, simp_all add: is_cap_table_def)[1] apply (clarsimp simp: valid_obj_def valid_cs_def well_formed_cnode_n_def
                        valid_cs_size_def length_set_helper
                        word_bits_def) apply (drule invs_psp_aligned) apply (unfold pspace_aligned_def) apply (frule domI, drule (1) bspec) apply (clarsimp simp: ex_with_length add.commute split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; invs s\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow> 0 < bits_of c \<and> bits_of c < word_bits - cte_level_bits \<and> is_aligned (obj_ref_of c) (bits_of c + cte_level_bits)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; invs s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow> 0 < bits_of c \<and> bits_of c < word_bits - cte_level_bits \<and> is_aligned (obj_ref_of c) (bits_of c + cte_level_bits)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; valid_objs s; \<exists>cap. P cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow> 0 < bits_of c \<and> bits_of c < word_bits - cte_level_bits \<and> is_aligned (obj_ref_of c) (bits_of c + cte_level_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; valid_objs s; P cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow> 0 < bits_of c \<and> bits_of c < word_bits - cte_level_bits \<and> is_aligned (obj_ref_of c) (bits_of c + cte_level_bits)) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; valid_objs s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> is_cnode_cap cap \<longrightarrow> 0 < bits_of cap \<and> bits_of cap < word_bits - cte_level_bits \<and> is_aligned (obj_ref_of cap) (bits_of cap + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g. \<lbrakk>invs s; valid_objs s; cap_aligned (CNodeCap r bits g); cap_table_at bits r s; 0 < bits; length g \<le> word_bits\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits \<and> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g ko. \<lbrakk>invs s; valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> word_bits; kheap s r = Some ko; is_cap_table bits ko; valid_obj r ko s\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits \<and> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g ko x12. \<lbrakk>invs s; valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> word_bits; kheap s r = Some (CNode bits x12); well_formed_cnode_n bits x12; valid_obj r (CNode bits x12) s; ko = CNode bits x12\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits \<and> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g x12. \<lbrakk>invs s; valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> 32; kheap s r = Some (CNode bits x12); dom x12 = {x. length x = bits}; \<forall>cap\<in>ran x12. s \<turnstile> cap; bits < 32 - cte_level_bits\<rbrakk> \<Longrightarrow> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g x12. \<lbrakk>valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> 32; kheap s r = Some (CNode bits x12); dom x12 = {x. length x = bits}; \<forall>cap\<in>ran x12. s \<turnstile> cap; bits < 32 - cte_level_bits; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g x12. \<lbrakk>valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> 32; kheap s r = Some (CNode bits x12); dom x12 = {x. length x = bits}; \<forall>cap\<in>ran x12. s \<turnstile> cap; bits < 32 - cte_level_bits; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x)))\<rbrakk> \<Longrightarrow> is_aligned r (bits + cte_level_bits) proof (prove)
goal (1 subgoal):
 1. \<And>r bits g x12. \<lbrakk>valid_objs s; cap_aligned (CNodeCap r bits g); 0 < bits; length g \<le> 32; kheap s r = Some (CNode bits x12); dom x12 = {x. length x = bits}; \<forall>cap\<in>ran x12. s \<turnstile> cap; bits < 32 - cte_level_bits; r \<in> dom (kheap s); is_aligned r (obj_bits (the (kheap s r)))\<rbrakk> \<Longrightarrow> is_aligned r (bits + cte_level_bits) proof (prove)
goal:
No subgoals!