theory CSpace_AI

lemma set_cap_cns_of_heap[wp]:
 "\<lbrace>\<lambda>s. P (cns_of_heap (kheap s))\<rbrace> set_cap cap sl
  \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace>" apply (simp add: set_cap_def split_def set_object_def) apply (rule hoare_seq_ext [OF _ get_object_sp]) apply (case_tac obj) apply (auto simp: valid_def in_monad obj_at_def get_object_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cns_of_heap (kheap s))\<rbrace> set_cap cap sl \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cns_of_heap (kheap s))\<rbrace> do obj <- get_object (fst sl);
obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>obj x11 x12. obj = CNode x11 x12 \<Longrightarrow> \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace>
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace>
 3. \<And>obj x3. obj = Endpoint x3 \<Longrightarrow> \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace>
 4. \<And>obj x4. obj = Notification x4 \<Longrightarrow> \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace>
 5. \<And>obj x5. obj = ArchObj x5 \<Longrightarrow> \<lbrace>(\<lambda>s. P (cns_of_heap (kheap s))) and ko_at obj (fst sl)\<rbrace> do obj' <- case obj of CNode sz cn \<Rightarrow> if snd sl \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd sl \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd sl = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd sl = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd sl = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd sl = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd sl = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst sl);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst sl \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>_ s. P (cns_of_heap (kheap s))\<rbrace> proof (prove)
goal:
No subgoals!