theory FinalCaps

lemma set_mrs_silc_inv[wp]:
  "set_mrs a b c \<lbrace>silc_inv aag st\<rbrace>" unfolding set_mrs_def apply (rule silc_inv_pres) apply (wp crunch_wps set_object_wp | wpc | simp add: crunch_simps split del: if_split)+ apply clarsimp apply (fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def) apply (wp crunch_wps set_object_wp | wpc | simp add: crunch_simps split del: if_split)+ apply (case_tac "a = fst slot") apply (clarsimp split: kernel_object.splits cong: conj_cong) apply (erule notE) apply (erule cte_wp_atE) apply (fastforce simp: obj_at_def) apply (drule get_tcb_SomeD) apply (rule cte_wp_at_tcbI) apply simp apply assumption apply (fastforce simp: tcb_cap_cases_def split: if_splits) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P. \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and K (pasObjectAbs aag ptr = SilcLabel)\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P s. silc_inv aag st s \<and> P (kheap s ptr) \<and> pasObjectAbs aag ptr = SilcLabel \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> P (if ptr = a then Some (TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>)) else kheap s ptr) \<and> ((\<exists>x. b = Some x) \<longrightarrow> P (if ptr = a then Some (TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>)) else kheap s ptr))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s y. \<lbrakk>silc_inv aag st s; P (kheap s a); pasObjectAbs aag a = SilcLabel; get_tcb a s = Some y\<rbrakk> \<Longrightarrow> P (Some (TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch y)\<rparr>))) \<and> ((\<exists>x. b = Some x) \<longrightarrow> P (Some (TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch y)\<rparr>))))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb a;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length c) msg_registers) then c ! the_index msg_registers reg else context reg);
set_object a (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) c);
case b of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length c)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length c) msg_max_length
od
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<not> cte_wp_at P slot s \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a = fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>))
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y. \<lbrakk>\<not> cte_wp_at P (a, b) s; get_tcb a s = Some y; cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y. \<lbrakk>get_tcb a s = Some y; cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>P b s y sz fun cte. \<lbrakk>get_tcb a s = Some y; kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (a, b)) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>get_tcb a s = Some y; kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>get_tcb a s = Some y; kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> kheap s (fst (a, b)) = Some (TCB (?tcb250 P b s y tcb getF setF restr))
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (a, b)) = Some (?getF250 P b s y tcb getF setF restr, ?setF250 P b s y tcb getF setF restr)
 3. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF250 P b s y tcb getF setF restr (?tcb250 P b s y tcb getF setF restr))
 4. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (a, b)) = Some (?getF250 P b s y tcb getF setF restr, ?setF250 P b s y tcb getF setF restr)
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF250 P b s y tcb getF setF restr y)
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>d. if d \<in> set (take (length c) msg_registers) then c ! the_index msg_registers d else arch_tcb_get_registers (tcb_arch (the (get_tcb (fst (a, b)) s))) d) (tcb_arch y)\<rparr>))\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb); kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> P (getF y)
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>) \<and> ((\<exists>x. b = Some x) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>b. if b \<in> set (take (length c) msg_registers) then c ! the_index msg_registers b else arch_tcb_get_registers (tcb_arch (the (get_tcb a s))) b) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!