theory CSpace_AI

lemma set_free_index_valid_pspace:
  "\<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and>
        (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and>idx \<le> 2^ cap_bits cap)\<rbrace>
   set_cap (free_index_update (\<lambda>_. idx) cap) cref
   \<lbrace>\<lambda>rv s'. valid_pspace s'\<rbrace>" apply (clarsimp simp: valid_pspace_def) apply (wp set_cap_valid_objs update_cap_iflive set_cap_zombies') apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps)+ apply (frule(1) caps_of_state_valid) apply (clarsimp simp:valid_cap_def cap_aligned_def free_index_update_def) apply (intro conjI) apply (clarsimp simp: valid_untyped_def) apply (elim impE allE) apply assumption+ apply (clarsimp simp: free_index_of_def) apply (erule disjoint_subset[rotated]) apply clarsimp apply (rule word_plus_mono_right) apply (rule of_nat_mono_maybe_le[THEN iffD1]) apply (subst word_bits_def[symmetric]) apply (erule less_le_trans[OF _  power_increasing]) apply simp apply simp apply (subst word_bits_def[symmetric]) apply (erule le_less_trans) apply (erule less_le_trans[OF _ power_increasing]) apply simp+ apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply (simp add: word_bits_def) apply (clarsimp simp add: pred_tcb_at_def tcb_cap_valid_def obj_at_def is_tcb valid_ipc_buffer_cap_def
                     split: option.split) apply (frule tcb_cap_slot_regular) apply simp+ apply (clarsimp simp: is_nondevice_page_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap\<rbrace> set_cap (free_index_update (\<lambda>_. idx) cap) cref \<lbrace>\<lambda>rv s'. valid_objs s' \<and> pspace_aligned s' \<and> pspace_distinct s' \<and> if_live_then_nonz_cap s' \<and> zombies_final s' \<and> sym_refs (state_refs_of s') \<and> sym_refs (state_hyp_refs_of s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> cte_wp_at ((=) cap) cref s \<and> free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2 ^ cap_bits cap \<Longrightarrow> (valid_objs and valid_cap (free_index_update (\<lambda>_. idx) cap) and tcb_cap_valid (free_index_update (\<lambda>_. idx) cap) cref) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs (free_index_update (\<lambda>_. idx) cap)) cref and if_live_then_nonz_cap) s \<and> (zombies_final s \<and> cte_wp_at (\<lambda>cap'. \<forall>p' cap''. cte_wp_at ((=) cap'') p' s \<and> cref \<noteq> p' \<and> obj_refs (free_index_update (\<lambda>_. idx) cap) \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie (free_index_update (\<lambda>_. idx) cap) \<and> \<not> is_zombie cap'') cref s) \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev r bits idx \<and> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; s \<turnstile> UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev r bits idx \<and> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev r bits idx) s \<and> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev r bits idx) s
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {r + word_of_nat idx..r + 2 ^ bits - 1} \<inter> obj_range p obj = {}
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> kheap s (?p52 s dev r bits f p obj) = Some (?obj53 s dev r bits f p obj)
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range (?p52 s dev r bits f p obj) (?obj53 s dev r bits f p obj) \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range (?p52 s dev r bits f p obj) (?obj53 s dev r bits f p obj) \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range (?p52 s dev r bits f p obj) (?obj53 s dev r bits f p obj) = {}\<rbrakk> \<Longrightarrow> {r + word_of_nat idx..r + 2 ^ bits - 1} \<inter> obj_range p obj = {}
 4. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1} \<and> (if f < 2 ^ bits then {r + word_of_nat f..r + 2 ^ bits - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> {r + word_of_nat idx..r + 2 ^ bits - 1} \<inter> obj_range p obj = {}
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; {r + word_of_nat f..r + 2 ^ bits - 1} \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> {r + word_of_nat idx..r + 2 ^ bits - 1} \<inter> obj_range p obj = {}
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> {r + word_of_nat idx..r + 2 ^ bits - 1} \<subseteq> {r + word_of_nat f..r + 2 ^ bits - 1}
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r + word_of_nat f \<le> r + word_of_nat idx
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word_of_nat f \<le> word_of_nat idx
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 3. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (5 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32)
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ LENGTH(32)
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 4. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 5. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (5 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ word_bits
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ LENGTH(32)
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 4. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 5. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (6 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> bits \<le> word_bits
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ LENGTH(32)
 4. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 5. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 6. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (5 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ LENGTH(32)
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 4. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 5. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ LENGTH(32)
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 4. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f < 2 ^ word_bits
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 4. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (4 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> idx < 2 ^ word_bits
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 4. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (5 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> bits \<le> word_bits
 2. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> f \<le> idx
 4. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 5. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> r + word_of_nat idx
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ bits
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev r bits f p obj. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); f \<le> idx; cap = UntypedCap dev r bits f; bits < word_bits; untyped_min_bits \<le> bits; r \<noteq> 0; idx < 2 ^ bits; kheap s p = Some obj; obj_range p obj \<inter> {r..r + 2 ^ bits - 1} \<noteq> {}; obj_range p obj \<subseteq> {r..r + 2 ^ bits - 1}; r + word_of_nat idx \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> idx < unat (2 ^ bits)
 2. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; kheap s (fst cref) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<exists>tcba. (tcb_cap_cases (snd cref) = None \<longrightarrow> tcb = tcba) \<and> (\<forall>a aa b. tcb_cap_cases (snd cref) = Some (a, aa, b) \<longrightarrow> tcb = tcba \<and> b (fst cref) (tcb_state tcba) (UntypedCap dev r bits f))) \<and> snd cref \<noteq> tcb_cnode_index 4 proof (prove)
goal (3 subgoals):
 1. \<And>s dev r bits f tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; kheap s (fst cref) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s dev r bits f tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; kheap s (fst cref) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> kheap s (fst cref) = Some (TCB (?tcb109 s dev r bits f tcb))
 3. \<And>s dev r bits f tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; kheap s (fst cref) = Some (TCB tcb); \<exists>fa upd check. tcb_cap_cases (snd cref) = Some (fa, upd, check) \<and> check (fst cref) (tcb_state (?tcb109 s dev r bits f tcb)) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (\<exists>tcba. (tcb_cap_cases (snd cref) = None \<longrightarrow> tcb = tcba) \<and> (\<forall>a aa b. tcb_cap_cases (snd cref) = Some (a, aa, b) \<longrightarrow> tcb = tcba \<and> b (fst cref) (tcb_state tcba) (UntypedCap dev r bits f))) \<and> snd cref \<noteq> tcb_cnode_index 4 proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); caps_of_state s cref = Some (UntypedCap dev r bits f); free_index_of (UntypedCap dev r bits f) \<le> idx; idx \<le> 2 ^ bits; cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; valid_untyped (UntypedCap dev r bits f) s; untyped_min_bits \<le> bits; f \<le> 2 ^ bits; r \<noteq> 0; kheap s (fst cref) = Some (TCB tcb); \<exists>fa upd check. tcb_cap_cases (snd cref) = Some (fa, upd, check) \<and> check (fst cref) (tcb_state tcb) (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> (\<exists>tcba. (tcb_cap_cases (snd cref) = None \<longrightarrow> tcb = tcba) \<and> (\<forall>a aa b. tcb_cap_cases (snd cref) = Some (a, aa, b) \<longrightarrow> tcb = tcba \<and> b (fst cref) (tcb_state tcba) (UntypedCap dev r bits f))) \<and> snd cref \<noteq> tcb_cnode_index 4 proof (prove)
goal:
No subgoals!