theory Untyped_AI

lemma set_free_index_valid_pspace_simple:
  "\<lbrace>\<lambda>s. valid_mdb s \<and> valid_pspace s \<and> pspace_no_overlap_range_cover ptr sz s
   \<and> descendants_range_in {ptr .. ptr+2^sz - 1} cref s
   \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s
   \<and> idx \<le> 2^ sz\<rbrace>
  set_cap (UntypedCap dev ptr sz idx) 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_cap) apply (clarsimp simp: valid_cap_def cap_aligned_def ) apply (intro conjI) apply (simp add: valid_untyped_def) apply (intro impI allI) apply (elim allE allE impE) apply simp+ apply (drule(1) pspace_no_overlap_obj_range) apply (simp add: field_simps) 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 (drule(2) tcb_cap_slot_regular) apply (clarsimp simp: tcb_cap_cases_def is_cap_simps split: if_splits) apply (fastforce simp: is_nondevice_page_cap_simps) apply (clarsimp split: thread_state.splits simp: is_reply_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb s \<and> valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) cref \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb s \<and> 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> pspace_no_overlap (up_aligned_area ptr sz) s \<and> descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2 ^ sz\<rbrace> set_cap (UntypedCap dev ptr sz idx) 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_mdb s \<and> 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> pspace_no_overlap (up_aligned_area ptr sz) s \<and> descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr) cref s \<and> idx \<le> 2 ^ sz \<Longrightarrow> (valid_objs and valid_cap (UntypedCap dev ptr sz idx) and tcb_cap_valid (UntypedCap dev ptr sz idx) cref) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (cte_wp_at (\<lambda>cap'. zobj_refs cap' = zobj_refs (UntypedCap dev ptr sz idx)) 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 (UntypedCap dev ptr sz idx) \<inter> obj_refs cap'' \<noteq> {} \<longrightarrow> \<not> is_zombie (UntypedCap dev ptr sz idx) \<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 deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap (up_aligned_area ptr sz) s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f)\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev ptr sz idx \<and> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap (up_aligned_area ptr sz) s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); s \<turnstile> UntypedCap deva ptr sz f\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev ptr sz idx \<and> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev ptr sz idx) s \<and> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap dev ptr sz idx) s
 2. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if f < 2 ^ sz then {ptr + word_of_nat f..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> idx < 2 ^ sz \<longrightarrow> (\<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {})
 2. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if f < 2 ^ sz then {ptr + word_of_nat f..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {}
 2. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (4 subgoals):
 1. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> kheap s (?p62 s dev f p obj) = Some (?obj63 s dev f p obj)
 2. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range (?p62 s dev f p obj) (?obj63 s dev f p obj) \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}
 3. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range (?p62 s dev f p obj) (?obj63 s dev f p obj) \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if f < 2 ^ sz then {ptr + word_of_nat f..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range (?p62 s dev f p obj) (?obj63 s dev f p obj) = {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {}
 4. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if f < 2 ^ sz then {ptr + word_of_nat f..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {}
 2. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (2 subgoals):
 1. \<And>s dev f p obj. \<lbrakk>valid_mdb s; 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); descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; caps_of_state s cref = Some (UntypedCap dev ptr sz f); is_aligned ptr sz; sz < word_bits; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; idx < 2 ^ sz; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if f < 2 ^ sz then {ptr + word_of_nat f..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; obj_range p obj \<inter> {ptr..ptr + (2 ^ sz - 1)} = {}\<rbrakk> \<Longrightarrow> {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} \<inter> obj_range p obj = {}
 2. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s deva f. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev ptr sz idx) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s deva f tcb. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; caps_of_state s cref = Some (UntypedCap deva ptr sz f); is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<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 ptr sz idx))) \<and> snd cref \<noteq> tcb_cnode_index 4 proof (prove)
goal (1 subgoal):
 1. \<And>s deva f tcb. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<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 deva ptr sz 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 ptr sz idx))) \<and> snd cref \<noteq> tcb_cnode_index 4 proof (prove)
goal (2 subgoals):
 1. \<And>s dev f tcb. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; kheap s (fst cref) = Some (TCB tcb); snd cref = tcb_cnode_index 4; is_nondevice_page_cap (UntypedCap dev ptr sz f)\<rbrakk> \<Longrightarrow> False
 2. \<And>s deva f tcb. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; kheap s (fst cref) = Some (TCB tcb); snd cref = tcb_cnode_index 3; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (UntypedCap deva ptr sz f)\<rbrakk> \<Longrightarrow> (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (UntypedCap dev ptr sz idx) proof (prove)
goal (1 subgoal):
 1. \<And>s deva f tcb. \<lbrakk>valid_mdb s; 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); pspace_no_overlap {ptr..ptr + (2 ^ sz - 1)} s; descendants_range_in {ptr..ptr + 2 ^ sz - 1} cref s; idx \<le> 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap deva ptr sz f) s; untyped_min_bits \<le> sz; f \<le> 2 ^ sz; ptr \<noteq> 0; kheap s (fst cref) = Some (TCB tcb); snd cref = tcb_cnode_index 3; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (UntypedCap deva ptr sz f)\<rbrakk> \<Longrightarrow> (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (UntypedCap dev ptr sz idx) proof (prove)
goal:
No subgoals!