theory CSpaceInv_AI

lemma set_cap_idle[wp]:
  "\<lbrace>\<lambda>s. valid_idle s\<rbrace>
   set_cap cap p
  \<lbrace>\<lambda>rv. valid_idle\<rbrace>" apply (simp add: valid_idle_def set_cap_def set_object_def split_def) apply (wp get_object_wp|wpc)+ apply (auto simp: pred_tcb_at_def obj_at_def is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> do obj <- get_object (fst p);
obj' <- case obj of CNode sz cn \<Rightarrow> if snd p \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd p = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd p = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd p = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd p = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd p = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail;
kobj <- get_object (fst p);
y <- assert (a_type kobj = a_type obj');
s <- get;
put (s\<lparr>kheap := (kheap s)(fst p \<mapsto> obj')\<rparr>)
od \<lbrace>\<lambda>rv s. idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr \<Longrightarrow> \<forall>ko. ko_at ko (fst p) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (CNode x $ xa(snd p \<mapsto> cap)) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> CNode x $ xa(snd p \<mapsto> cap))\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> CNode x $ xa(snd p \<mapsto> cap))\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> CNode x $ xa(snd p \<mapsto> cap))\<rparr>) = idle_thread_ptr)) \<and> (\<not> (snd p \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_ctable := cap\<rparr>) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ctable := cap\<rparr>)\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ctable := cap\<rparr>)\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ctable := cap\<rparr>)\<rparr>) = idle_thread_ptr)) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index 1 \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_vtable := cap\<rparr>) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_vtable := cap\<rparr>)\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_vtable := cap\<rparr>)\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_vtable := cap\<rparr>)\<rparr>) = idle_thread_ptr)) \<and> (snd p \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_reply := cap\<rparr>) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_reply := cap\<rparr>)\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_reply := cap\<rparr>)\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_reply := cap\<rparr>)\<rparr>) = idle_thread_ptr)) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_caller := cap\<rparr>) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_caller := cap\<rparr>)\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_caller := cap\<rparr>)\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_caller := cap\<rparr>)\<rparr>) = idle_thread_ptr)) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>ko. ko_at ko (fst p) s \<longrightarrow> a_type ko = a_type (TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>) \<longrightarrow> idle_tcb_at (\<lambda>p. idle (fst p) \<and> fst (snd p) = None \<and> valid_arch_idle (snd (snd p))) (idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>)\<rparr>)) (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>)\<rparr>) \<and> idle_thread (s\<lparr>kheap := (kheap s)(fst p \<mapsto> TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>)\<rparr>) = idle_thread_ptr)) \<and> (snd p \<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:
No subgoals!