theory CSpaceInv_AI

lemma set_untyped_cap_as_full_tcb_cap_valid:
  "\<lbrace>tcb_cap_valid cap dest\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. tcb_cap_valid cap dest s\<rbrace>" apply (clarsimp simp: set_untyped_cap_as_full_def valid_def tcb_cap_valid_def) apply (intro conjI impI allI ballI) apply (case_tac "tcb_at (fst dest) s") apply clarsimp apply (intro conjI impI allI) apply (drule use_valid[OF _ set_cap_pred_tcb],simp+) apply (clarsimp simp: valid_ipc_buffer_cap_def is_cap_simps) apply (fastforce simp: tcb_at_def obj_at_def is_tcb) apply (clarsimp simp: tcb_at_typ) apply (drule use_valid[OF _ set_cap_typ_at]) apply (assumption) apply simp apply (clarsimp simp: return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap dest\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. tcb_cap_valid cap dest\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> (\<forall>s. (tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<longrightarrow> (\<forall>x\<in>fst (set_cap (max_free_index_update src_cap) src s). case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))))) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> (\<forall>s. (tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))) \<longrightarrow> (\<forall>x\<in>fst (return () s). case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))))) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 3. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap (max_free_index_update src_cap) src s); tcb_at (fst dest) s; is_untyped_cap src_cap; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s; snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) b\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) b \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) b \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 3. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (4 subgoals):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap (max_free_index_update src_cap) src s); tcb_at (fst dest) s; is_untyped_cap src_cap; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s; snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) b\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) b
 2. \<And>s b tcb. \<lbrakk>((), b) \<in> fst (set_cap (max_free_index_update src_cap) src s); tcb_at (fst dest) s; is_untyped_cap src_cap; st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s; snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)); is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) b; snd dest = tcb_cnode_index 4; ko_at (TCB tcb) (fst dest) b\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)
 3. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 4. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s b tcb. \<lbrakk>((), b) \<in> fst (set_cap (max_free_index_update src_cap) src s); tcb_at (fst dest) s; is_untyped_cap src_cap; st_tcb_at (\<lambda>st. is_nondevice_page_cap cap \<or> NullCap = cap) (fst dest) s; \<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb); is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) b; snd dest = tcb_cnode_index 4; ko_at (TCB tcb) (fst dest) b\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)
 2. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 3. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s b tcb dev deva ra bitsa f fa. \<lbrakk>((), b) \<in> fst (set_cap (free_index_update (\<lambda>_. max_free_index bitsa) (UntypedCap dev ra bitsa f)) src s); tcb_at (fst dest) s; st_tcb_at (\<lambda>st. is_nondevice_page_cap (UntypedCap deva ra bitsa fa)) (fst dest) s; \<forall>tcb. \<not> ko_at (TCB tcb) (fst dest) s; tcb_at (fst dest) b; snd dest = tcb_cnode_index 4; ko_at (TCB tcb) (fst dest) b; src_cap = UntypedCap dev ra bitsa f; cap = UntypedCap deva ra bitsa fa\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 3. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> tcb_at (fst dest) s\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (set_cap (max_free_index_update src_cap) src s); \<not> typ_at ATCB (fst dest) s; is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; typ_at ATCB (fst dest) b\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) b \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) b \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<lbrakk>\<not> typ_at ATCB (fst dest) s; is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; typ_at ATCB (fst dest) b\<rbrakk> \<Longrightarrow> ?P62 s b (typ_at (?T62 s b) (?p62 s b) s)
 2. \<And>s b. \<lbrakk>\<not> typ_at ATCB (fst dest) s; is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; typ_at ATCB (fst dest) b; ?P62 s b (typ_at (?T62 s b) (?p62 s b) b)\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) b \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) b \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 3. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>\<not> typ_at ATCB (fst dest) s; is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; typ_at ATCB (fst dest) b; \<not> typ_at ATCB (fst dest) b\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) b \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) b \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))
 2. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; tcb_at (fst dest) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))); x \<in> fst (return () s)\<rbrakk> \<Longrightarrow> case x of (r, s') \<Rightarrow> tcb_at (fst dest) s' \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd dest) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst dest) st cap) (fst dest) s' \<and> (snd dest = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst dest) s' \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal:
No subgoals!