theory ArchCSpace_AI

lemma cte_at_length_limit:
  "\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits" apply (simp add: cte_at_cases) apply (erule disjE) apply clarsimp apply (erule(1) valid_objsE) apply (clarsimp simp: valid_obj_def well_formed_cnode_n_def valid_cs_def valid_cs_size_def
                         length_set_helper) apply (drule arg_cong[where f="\<lambda>S. snd p \<in> S"]) apply (simp add: domI) apply (clarsimp simp add: tcb_cap_cases_length word_bits_conv cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; valid_objs s\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases; valid_objs s\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; \<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits
 2. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<And>sz fun y. \<lbrakk>valid_objs s; kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some y\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits
 2. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<And>sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some y; valid_obj (fst p) (CNode sz fun) s\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits
 2. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<And>sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); dom fun = {x. length x = sz}; fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; sz < word_bits - cte_level_bits\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits
 2. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (2 subgoals):
 1. \<And>sz fun y. \<lbrakk>kheap s (fst p) = Some (CNode sz fun); fun (snd p) = Some y; \<forall>cap\<in>ran fun. s \<turnstile> cap; sz < word_bits - cte_level_bits; (snd p \<in> dom fun) = (snd p \<in> {x. length x = sz})\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits
 2. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; (\<exists>tcb. kheap s (fst p) = Some (TCB tcb)) \<and> snd p \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits proof (prove)
goal:
No subgoals!