theory DomainSepInv

lemma set_cap_neg_cte_wp_at:
  "\<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace>
   set_cap capa slota
   \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>" apply (case_tac "slot = slota") apply simp apply (simp add: set_cap_def set_object_def) apply (rule hoare_pre) apply (wp get_object_wp | wpc)+ apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) apply (rule hoare_pre) apply (rule set_cap_neg_cte_wp_at_other, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot = slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>
 2. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot = slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slota s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slota s\<rbrace>
 2. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot = slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slota s \<and> \<not> P capa\<rbrace> case slota of (oref, cref) \<Rightarrow> do obj <- get_object oref;
obj' <- 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> capa) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := capa\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := capa\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := capa\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := capa\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := capa\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object oref;
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(oref \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slota s\<rbrace>
 2. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. slot = slota \<Longrightarrow> \<lbrace>?Q1\<rbrace> case slota of (oref, cref) \<Rightarrow> do obj <- get_object oref;
obj' <- 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> capa) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := capa\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := capa\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := capa\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := capa\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := capa\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object oref;
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(oref \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slota s\<rbrace>
 2. \<And>s. \<lbrakk>slot = slota; \<not> cte_wp_at P slota s \<and> \<not> P capa\<rbrakk> \<Longrightarrow> ?Q1 s
 3. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slot = slota; \<not> cte_wp_at P slota s \<and> \<not> P capa\<rbrakk> \<Longrightarrow> \<forall>x xa. slota = (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> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (CNode xb $ xc(xa \<mapsto> capa)) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> CNode xb $ xc(xa \<mapsto> capa))\<rparr>))) \<and> (\<not> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc) \<longrightarrow> True)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (TCB $ xb\<lparr>tcb_ctable := capa\<rparr>) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB $ xb\<lparr>tcb_ctable := capa\<rparr>)\<rparr>))) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index 1 \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (TCB $ xb\<lparr>tcb_vtable := capa\<rparr>) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB $ xb\<lparr>tcb_vtable := capa\<rparr>)\<rparr>))) \<and> (xa \<noteq> tcb_cnode_index 1 \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (TCB $ xb\<lparr>tcb_reply := capa\<rparr>) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB $ xb\<lparr>tcb_reply := capa\<rparr>)\<rparr>))) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (TCB $ xb\<lparr>tcb_caller := capa\<rparr>) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB $ xb\<lparr>tcb_caller := capa\<rparr>)\<rparr>))) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> (xa = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko x s \<longrightarrow> a_type ko = a_type (TCB $ xb\<lparr>tcb_ipcframe := capa\<rparr>) \<longrightarrow> \<not> cte_wp_at P slota (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB $ xb\<lparr>tcb_ipcframe := capa\<rparr>)\<rparr>))) \<and> (xa \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True))
 2. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slota \<Longrightarrow> \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. slot \<noteq> slota \<Longrightarrow> \<lbrace>?Q193\<rbrace> set_cap capa slota \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace>
 2. \<And>s. \<lbrakk>slot \<noteq> slota; \<not> cte_wp_at P slot s \<and> \<not> P capa\<rbrakk> \<Longrightarrow> ?Q193 s proof (prove)
goal:
No subgoals!