theory ArchCNodeInv_AI

lemma valid_cnode_capI:
  "\<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; n > 0; length g \<le> 32\<rbrakk>
   \<Longrightarrow> s \<turnstile> cap.CNodeCap w n g" apply (simp add: valid_cap_def cap_aligned_def) apply (rule conjI) apply (clarsimp simp add: pspace_aligned_def obj_at_def) apply (drule bspec, fastforce) apply (clarsimp simp: is_obj_defs wf_obj_bits) apply (clarsimp simp add: obj_at_def is_obj_defs valid_objs_def dom_def) apply (erule allE, erule impE, blast) apply (simp add: valid_obj_def valid_cs_def valid_cs_size_def) apply (simp add: word_bits_def cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> s \<turnstile> CNodeCap w n g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> is_aligned w (cte_level_bits + n) \<and> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> is_aligned w (cte_level_bits + n)
 2. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>valid_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); 0 < n; length g \<le> 32; kheap s w = Some ko; is_cap_table n ko\<rbrakk> \<Longrightarrow> is_aligned w (cte_level_bits + n)
 2. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>valid_objs s; 0 < n; length g \<le> 32; kheap s w = Some ko; is_cap_table n ko; is_aligned w (obj_bits (the (kheap s w)))\<rbrakk> \<Longrightarrow> is_aligned w (cte_level_bits + n)
 2. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; 0 < n; length g \<le> 32\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); pspace_aligned s; 0 < n; length g \<le> 32; kheap s w = Some (CNode n cs); well_formed_cnode_n n cs\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>pspace_aligned s; 0 < n; length g \<le> 32; kheap s w = Some (CNode n cs); well_formed_cnode_n n cs; \<exists>obj. kheap s w = Some obj \<and> valid_obj w obj s\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>pspace_aligned s; 0 < n; length g \<le> 32; kheap s w = Some (CNode n cs); well_formed_cnode_n n cs; (\<forall>cap\<in>ran cs. s \<turnstile> cap) \<and> n < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> cte_level_bits + n < word_bits \<and> length g \<le> word_bits proof (prove)
goal:
No subgoals!