theory Invariants_AI

lemma valid_CNodeCapE:
  assumes p: "s \<turnstile> CNodeCap ptr cbits guard" "valid_objs s" "pspace_aligned s"
  assumes R: "\<And>cs. \<lbrakk> 0 < cbits; kheap s ptr = Some (CNode cbits cs);
               \<forall>cap\<in>ran cs. s \<turnstile> cap; dom cs = {x. length x = cbits};
               is_aligned ptr (cte_level_bits + cbits); cbits < word_bits - cte_level_bits
              \<rbrakk> \<Longrightarrow> P"
  shows "P" using p apply (clarsimp simp: pspace_aligned_def valid_cap_def) apply (erule (1) obj_at_valid_objsE) apply (drule bspec, blast) apply (clarsimp simp add: is_cap_table) apply (clarsimp simp: valid_obj_def valid_cs_def well_formed_cnode_n_def) apply (erule valid_cs_sizeE) apply (clarsimp simp: cap_aligned_def) apply (erule (5) R) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
s \<turnstile> CNodeCap ptr cbits guard
valid_objs s
pspace_aligned s

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); cap_aligned (CNodeCap ptr cbits guard); cap_table_at cbits ptr s; 0 < cbits; length guard \<le> word_bits\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); cap_aligned (CNodeCap ptr cbits guard); 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some ko; is_cap_table cbits ko; valid_obj ptr ko s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; cap_aligned (CNodeCap ptr cbits guard); 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some ko; is_cap_table cbits ko; valid_obj ptr ko s; is_aligned ptr (obj_bits (the (kheap s ptr)))\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>valid_objs s; cap_aligned (CNodeCap ptr cbits guard); 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some (CNode cbits cs); valid_obj ptr (CNode cbits cs) s; is_aligned ptr (cte_level_bits + cbits); well_formed_cnode_n cbits cs\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>valid_objs s; cap_aligned (CNodeCap ptr cbits guard); 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some (CNode cbits cs); is_aligned ptr (cte_level_bits + cbits); dom cs = {x. length x = cbits}; \<forall>cap\<in>ran cs. s \<turnstile> cap; valid_cs_size cbits cs\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>valid_objs s; cap_aligned (CNodeCap ptr cbits guard); 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some (CNode cbits cs); is_aligned ptr (cte_level_bits + cbits); dom cs = {x. length x = cbits}; \<forall>cap\<in>ran cs. s \<turnstile> cap; cbits < word_bits - cte_level_bits; dom cs = {x. length x = cbits}; obj_bits (CNode cbits cs) = cte_level_bits + cbits\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>valid_objs s; cte_level_bits + cbits < word_bits; 0 < cbits; length guard \<le> word_bits; kheap s ptr = Some (CNode cbits cs); is_aligned ptr (cte_level_bits + cbits); \<forall>cap\<in>ran cs. s \<turnstile> cap; cbits < word_bits - cte_level_bits; dom cs = {x. length x = cbits}\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!