theory VSpaceEntries_AI

lemma set_cap_arch_obj_neg:
  "\<lbrace>\<lambda>s. \<not>ko_at (ArchObj ao) p s \<and> cte_wp_at (\<lambda>_. True) p' s\<rbrace> set_cap cap p' \<lbrace>\<lambda>_ s. \<not>ko_at (ArchObj ao) p s\<rbrace>" apply (simp add: set_cap_def split_def) apply (wp set_object_neg_ko get_object_wp| wpc)+ apply (auto simp: pred_neg_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> ako_at ao p s \<and> cte_wp_at (\<lambda>_. True) p' s\<rbrace> set_cap cap p' \<lbrace>\<lambda>_ s. \<not> ako_at ao p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> ako_at ao p s \<and> cte_wp_at (\<lambda>_. True) p' s\<rbrace> do obj <- get_object (fst p');
(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) >>= set_object (fst p')
od \<lbrace>\<lambda>_ s. \<not> ako_at ao p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> ako_at ao p s \<and> cte_wp_at (\<lambda>_. True) p' s \<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> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (CNode x $ xa(snd p' \<mapsto> cap)) \<noteq> ArchObj ao) s) \<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> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (TCB $ x\<lparr>tcb_ctable := cap\<rparr>) \<noteq> ArchObj ao) s) \<and> (snd p' \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p' = tcb_cnode_index 1 \<longrightarrow> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (TCB $ x\<lparr>tcb_vtable := cap\<rparr>) \<noteq> ArchObj ao) s) \<and> (snd p' \<noteq> tcb_cnode_index 1 \<longrightarrow> (snd p' = tcb_cnode_index 2 \<longrightarrow> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (TCB $ x\<lparr>tcb_reply := cap\<rparr>) \<noteq> ArchObj ao) s) \<and> (snd p' \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p' = tcb_cnode_index 3 \<longrightarrow> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (TCB $ x\<lparr>tcb_caller := cap\<rparr>) \<noteq> ArchObj ao) s) \<and> (snd p' \<noteq> tcb_cnode_index 3 \<longrightarrow> (snd p' = tcb_cnode_index 4 \<longrightarrow> (not ako_at ao p) s \<and> K (fst p' = p \<longrightarrow> (TCB $ x\<lparr>tcb_ipcframe := cap\<rparr>) \<noteq> ArchObj ao) s) \<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!