theory Intent_DR

lemma valid_objs_set_cxt_mrs[wp]:
  "\<lbrace>ko_at (TCB tcb) thread and valid_objs\<rbrace>
     KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb))
   \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (wp set_object_valid_objs) apply (clarsimp simp:obj_at_def) apply (clarsimp simp:valid_objs_def) apply (drule_tac x=thread in bspec) apply (clarsimp simp:dom_def) apply (clarsimp simp:valid_obj_def valid_tcb_def) apply (drule_tac x="(a,aa,b)" in bspec) apply simp apply (clarsimp simp:tcb_cap_cases_def) apply (erule disjE|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (TCB tcb) thread and valid_objs\<rbrace> KHeap_A.set_object thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ko_at (TCB tcb) thread and valid_objs) s \<Longrightarrow> (valid_objs and valid_obj thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>kheap s thread = Some (TCB tcb); valid_objs s\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>kheap s thread = Some (TCB tcb); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. kheap s thread = Some (TCB tcb) \<Longrightarrow> thread \<in> dom (kheap s)
 2. \<And>s. \<lbrakk>kheap s thread = Some (TCB tcb); \<exists>obj. kheap s thread = Some obj \<and> valid_obj thread obj s\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>kheap s thread = Some (TCB tcb); \<exists>obj. kheap s thread = Some obj \<and> valid_obj thread obj s\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (tcb_arch_update (arch_tcb_context_set t) tcb)) s proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s thread = Some (TCB tcb); (a, aa, b) \<in> ran tcb_cap_cases; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state tcb) (getF tcb)); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> s \<turnstile> a (tcb_arch_update (arch_tcb_context_set t) tcb) \<and> b thread (tcb_state tcb) (a (tcb_arch_update (arch_tcb_context_set t) tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>s a aa b. \<lbrakk>kheap s thread = Some (TCB tcb); (a, aa, b) \<in> ran tcb_cap_cases; valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> ran tcb_cap_cases
 2. \<And>s a aa b. \<lbrakk>kheap s thread = Some (TCB tcb); (a, aa, b) \<in> ran tcb_cap_cases; valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; case (a, aa, b) of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state tcb) (getF tcb))\<rbrakk> \<Longrightarrow> s \<turnstile> a (tcb_arch_update (arch_tcb_context_set t) tcb) \<and> b thread (tcb_state tcb) (a (tcb_arch_update (arch_tcb_context_set t) tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s thread = Some (TCB tcb); (a, aa, b) \<in> ran tcb_cap_cases; valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; case (a, aa, b) of (getF, ab) \<Rightarrow> s \<turnstile> getF tcb \<and> (case ab of (setF, restr) \<Rightarrow> restr thread (tcb_state tcb) (getF tcb))\<rbrakk> \<Longrightarrow> s \<turnstile> a (tcb_arch_update (arch_tcb_context_set t) tcb) \<and> b thread (tcb_state tcb) (a (tcb_arch_update (arch_tcb_context_set t) tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa b. \<lbrakk>kheap s thread = Some (TCB tcb); a = tcb_ipcframe \<and> aa = tcb_ipcframe_update \<and> b = (\<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap) \<or> a = tcb_caller \<and> aa = tcb_caller_update \<and> b = (\<lambda>_. case_thread_state (is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (\<lambda>e data. (=) cap.NullCap) (\<lambda>word sender_payload_ext. is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (\<lambda>word. is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap)) \<or> a = tcb_reply \<and> aa = tcb_reply_update \<and> b = (\<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> Structures_A.cap_rights c \<or> halted st \<and> c = cap.NullCap) \<or> a = tcb_vtable \<and> aa = tcb_vtable_update \<and> b = (\<lambda>_ _. is_valid_vtable_root or (=) cap.NullCap) \<or> a = tcb_ctable \<and> aa = tcb_ctable_update \<and> b = (\<lambda>_ _ _. True); valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb); valid_tcb_state (tcb_state tcb) s; case tcb_fault tcb of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler tcb) = word_bits; valid_bound_ntfn (tcb_bound_notification tcb) s; valid_arch_tcb (tcb_arch tcb) s; s \<turnstile> a tcb; b thread (tcb_state tcb) (a tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> a (tcb_arch_update (arch_tcb_context_set t) tcb) \<and> b thread (tcb_state tcb) (a (tcb_arch_update (arch_tcb_context_set t) tcb)) proof (prove)
goal:
No subgoals!