theory DomainSepInv

lemma set_cap_neg_cte_wp_at_other:
  "oslot \<noteq> slot \<Longrightarrow> set_cap cap oslot \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace>" unfolding set_cap_def apply (wp set_object_wp get_object_wp | wpc | simp add: split_def)+ apply (intro allI impI conjI) apply (rule notI) apply (erule cte_wp_atE) apply (fastforce split: if_splits dest: prod_eqI elim: notE intro: cte_wp_at_cteI simp: obj_at_def) apply (fastforce split: if_splits elim: notE intro: cte_wp_at_tcbI) apply (auto dest: set_cap_neg_cte_wp_at_other_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oslot \<noteq> slot \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_cap cap oslot \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. oslot \<noteq> slot \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> case oslot 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>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s\<rbrakk> \<Longrightarrow> \<forall>x xa. oslot = (x, xa) \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> \<not> cte_wp_at P slot (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> \<not> cte_wp_at P slot (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> \<not> cte_wp_at P slot (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> \<not> cte_wp_at P slot (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> \<not> cte_wp_at P slot (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> \<not> cte_wp_at P slot (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>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (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>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (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>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal (7 subgoals):
 1. \<And>s x xa ko xb xc sz fun cte. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc; kheap (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>) (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; P cte\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa ko xb xc tcb getF setF restr. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc; kheap (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> False
 3. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 7. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (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 tcb getF setF restr. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = CNode xb xc; xa \<in> dom xc \<and> well_formed_cnode_n xb xc; kheap (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb (\<lambda>a. if a = xa then Some cap else xc a))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 6. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (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>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa = tcb_cnode_index 0\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ctable := cap\<rparr>))\<rparr>)
 2. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (x, xa); ko_at ko x s; ko = TCB xb; xa \<noteq> tcb_cnode_index 0; xa = tcb_cnode_index (Suc 0)\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_vtable := cap\<rparr>))\<rparr>)
 3. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_reply := cap\<rparr>))\<rparr>)
 4. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_caller := cap\<rparr>))\<rparr>)
 5. \<And>s x xa ko xb. \<lbrakk>oslot \<noteq> slot; \<not> cte_wp_at P slot s; oslot = (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> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (xb\<lparr>tcb_ipcframe := cap\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!