theory CNode_AC

lemma set_cap_tcb_states_of_state[wp]:
  "set_cap cap ptr \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace>" apply (simp add: set_cap_def split_def set_object_def) apply (wpsimp wp: get_object_wp) apply (fastforce simp: obj_at_def get_tcb_def tcb_states_of_state_def rsubst[where P=P, OF _ ext]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> do obj <- get_object (fst ptr);
obj' <- case obj of CNode sz cn \<Rightarrow> if snd ptr \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd ptr \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd ptr = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd ptr = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd ptr = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd ptr = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd ptr = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst ptr);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (tcb_states_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (tcb_states_of_state s); ko_at ko (fst ptr) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) else kheap s a\<rparr>)))) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ctable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_vtable := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_reply := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_caller := cap\<rparr>)) else kheap s a\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (tcb_states_of_state (s\<lparr>kheap := \<lambda>a. if a = fst ptr then Some (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)) else kheap s a\<rparr>)))))))) proof (prove)
goal:
No subgoals!