theory CSpaceInvPre_AI

lemma set_cap_obj_at_impossible:
  "\<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>" apply (simp add: set_cap_def split_def set_object_def) apply (wp get_object_wp | wpc)+ apply (clarsimp simp: obj_at_def) apply (subgoal_tac "\<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs)") apply (subgoal_tac "\<forall>tcb. \<not> P' (TCB tcb)") apply (clarsimp simp: fun_upd_def[symmetric] wf_cs_insert dom_def) apply auto[1] apply (auto simp:caps_of_def cap_of_def ran_tcb_cnode_map wf_cs_ran_nonempty) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<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>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {}) \<Longrightarrow> \<forall>ko. ko_at ko (fst ptr) s \<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 $ xa(snd ptr \<mapsto> cap)) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> CNode x $ xa(snd ptr \<mapsto> cap))\<rparr>)))) \<and> (\<not> (snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<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 = a_type (TCB $ x\<lparr>tcb_ctable := cap\<rparr>) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_ctable := cap\<rparr>)\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index 1 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_vtable := cap\<rparr>) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_vtable := cap\<rparr>)\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst ptr) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_reply := cap\<rparr>) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_reply := cap\<rparr>)\<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 = a_type (TCB $ x\<lparr>tcb_caller := cap\<rparr>) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_caller := cap\<rparr>)\<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 = a_type (TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>) \<longrightarrow> P (obj_at P' p (s\<lparr>kheap := (kheap s)(fst ptr \<mapsto> TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>)\<rparr>)))) \<and> (snd ptr \<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) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> (p = fst ptr \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (CNode x xa) = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (P' (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a))))) \<and> (p = fst ptr \<longrightarrow> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ctable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> P (P' (TCB (x\<lparr>tcb_vtable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_reply := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_caller := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>))))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs)\<rbrakk> \<Longrightarrow> (p = fst ptr \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (CNode x xa) = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (P' (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a))))) \<and> (p = fst ptr \<longrightarrow> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ctable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> P (P' (TCB (x\<lparr>tcb_vtable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_reply := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_caller := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)))))))))
 2. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs) proof (prove)
goal (3 subgoals):
 1. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs); \<forall>tcb. \<not> P' (TCB tcb)\<rbrakk> \<Longrightarrow> (p = fst ptr \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> snd ptr \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (CNode x xa) = a_type (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a)) \<longrightarrow> P (P' (CNode x (\<lambda>a. if a = snd ptr then Some cap else xa a))))) \<and> (p = fst ptr \<longrightarrow> (\<forall>x. ko = TCB x \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ctable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> P (P' (TCB (x\<lparr>tcb_vtable := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_reply := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_caller := cap\<rparr>)))) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> P (P' (TCB (x\<lparr>tcb_ipcframe := cap\<rparr>)))))))))
 2. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs)\<rbrakk> \<Longrightarrow> \<forall>tcb. \<not> P' (TCB tcb)
 3. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs) proof (prove)
goal (3 subgoals):
 1. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs); \<forall>tcb. \<not> P' (TCB tcb)\<rbrakk> \<Longrightarrow> (p = fst ptr \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (\<exists>y. xa (snd ptr) = Some y) \<and> well_formed_cnode_n x xa \<longrightarrow> a_type (CNode x xa) = a_type (CNode x (xa(snd ptr \<mapsto> cap))) \<longrightarrow> P False)) \<and> (p = fst ptr \<longrightarrow> (\<exists>x. ko = TCB x) \<longrightarrow> (snd ptr = tcb_cnode_index 0 \<longrightarrow> P False) \<and> (snd ptr \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd ptr = tcb_cnode_index (Suc 0) \<longrightarrow> P False) \<and> (snd ptr \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd ptr = tcb_cnode_index 2 \<longrightarrow> P False) \<and> (snd ptr \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd ptr = tcb_cnode_index 3 \<longrightarrow> P False) \<and> (snd ptr \<noteq> tcb_cnode_index 3 \<longrightarrow> snd ptr = tcb_cnode_index 4 \<longrightarrow> P False)))))
 2. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs)\<rbrakk> \<Longrightarrow> \<forall>tcb. \<not> P' (TCB tcb)
 3. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko; \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs)\<rbrakk> \<Longrightarrow> \<forall>tcb. \<not> P' (TCB tcb)
 2. \<And>s ko. \<lbrakk>P (\<exists>ko. kheap s p = Some ko \<and> P' ko); \<forall>ko. P' ko \<longrightarrow> caps_of ko = {}; kheap s (fst ptr) = Some ko\<rbrakk> \<Longrightarrow> \<forall>sz cs. well_formed_cnode_n sz cs \<longrightarrow> \<not> P' (CNode sz cs) proof (prove)
goal:
No subgoals!