theory FinalCaps

lemma set_cap_cte_wp_at_triv:
  "\<lbrace>\<top>\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at ((=) cap) slot\<rbrace>" unfolding set_cap_def apply (wpsimp wp: set_object_wp get_object_wp) apply (intro impI conjI allI) apply (rule cte_wp_at_cteI) apply fastforce apply clarsimp apply (drule set_cap_well_formed_cnode_helper[where slot=slot], simp+) apply (fastforce intro: cte_wp_at_tcbI simp: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. cte_wp_at ((=) cap) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case slot of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>_. cte_wp_at ((=) cap) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa ko. \<lbrakk>slot = (x, xa); ko_at ko x s\<rbrakk> \<Longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> cte_wp_at ((=) cap) (x, xa) (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index (Suc 0) \<longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> xa = tcb_cnode_index 4 \<longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>)))))) proof (prove)
goal (6 subgoals):
 1. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, xa) (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>)
 2. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa \<noteq> tcb_cnode_index 3; xa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal (9 subgoals):
 1. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> kheap (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>) (fst (x, xa)) = Some (CNode (?sz107 s x xa ko xb xc) (?fun107 s x xa ko xb xc))
 2. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> well_formed_cnode_n (?sz107 s x xa ko xb xc) (?fun107 s x xa ko xb xc)
 3. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> ?fun107 s x xa ko xb xc (snd (x, xa)) = Some (?cte107 s x xa ko xb xc)
 4. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> cap = ?cte107 s x xa ko xb xc
 5. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 7. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 8. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 9. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa \<noteq> tcb_cnode_index 3; xa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal (8 subgoals):
 1. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> well_formed_cnode_n xb (\<lambda>a. if a = xa then Some cap else xc a)
 2. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> (if snd (x, xa) = xa then Some cap else xc (snd (x, xa))) = Some (?cte107 s x xa ko xb xc)
 3. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> cap = ?cte107 s x xa ko xb xc
 4. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 7. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 8. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa \<noteq> tcb_cnode_index 3; xa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal (8 subgoals):
 1. \<And>s x xa xb xc y. \<lbrakk>slot = (x, xa); ko_at (CNode xb xc) x s; well_formed_cnode_n xb xc; xc xa = Some y\<rbrakk> \<Longrightarrow> well_formed_cnode_n xb (\<lambda>a. if a = xa then Some cap else xc a)
 2. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> (if snd (x, xa) = xa then Some cap else xc (snd (x, xa))) = Some (?cte107 s x xa ko xb xc)
 3. \<And>s x xa ko xb xc. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> cap = ?cte107 s x xa ko xb xc
 4. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 7. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 8. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa \<noteq> tcb_cnode_index 3; xa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>s x xa ko xb. \<lbrakk>slot = (x, tcb_cnode_index 0); ko_at (TCB xb) x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 0) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 2. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index (Suc 0)) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa = tcb_cnode_index 2\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 2) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 3) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>slot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa \<noteq> tcb_cnode_index (Suc 0); xa \<noteq> tcb_cnode_index 2; xa \<noteq> tcb_cnode_index 3; xa = tcb_cnode_index 4\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (x, tcb_cnode_index 4) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!