theory ArchArch_IF

lemma set_cap_globals_equiv''[Arch_IF_assms]:
  "\<lbrace>globals_equiv s and valid_arch_state\<rbrace>
   set_cap cap p
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_cap_def apply (simp only: split_def) apply (wp set_object_globals_equiv hoare_vcg_all_lift get_object_wp | wpc | simp)+ apply (fastforce simp: valid_arch_state_def obj_at_def is_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> set_cap cap p \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<rbrace> case p of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(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> cap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state\<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>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. globals_equiv s sa \<and> valid_arch_state sa \<Longrightarrow> (\<forall>x xa. ko_at (CNode x xa) (fst p) sa \<longrightarrow> snd p \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) \<noteq> Some (TCB tcb)))) \<and> (\<forall>x. ko_at (TCB x) (fst p) sa \<longrightarrow> (snd p = tcb_cnode_index 0 \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch x)) \<and> tcb_at (idle_thread sa) sa)) \<and> (snd p \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd p = tcb_cnode_index (Suc 0) \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch x)) \<and> tcb_at (idle_thread sa) sa)) \<and> (snd p \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd p = tcb_cnode_index 2 \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch x)) \<and> tcb_at (idle_thread sa) sa)) \<and> (snd p \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd p = tcb_cnode_index 3 \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch x)) \<and> tcb_at (idle_thread sa) sa)) \<and> (snd p \<noteq> tcb_cnode_index 3 \<longrightarrow> snd p = tcb_cnode_index 4 \<longrightarrow> fst p \<noteq> arm_global_pd (arch_state sa) \<and> (fst p = idle_thread sa \<longrightarrow> (\<forall>tcb. kheap sa (idle_thread sa) = Some (TCB tcb) \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch x)) \<and> tcb_at (idle_thread sa) sa)))))) proof (prove)
goal:
No subgoals!