theory Tcb_DR

lemma dcorres_corrupt_tcb_intent_ipcbuffer_upd:
  "dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
    (corrupt_tcb_intent  y)
    (thread_set (tcb_ipc_buffer_update (\<lambda>_. a)) y)" apply (clarsimp simp:corrupt_tcb_intent_def thread_set_def get_thread_def bind_assoc) apply (rule dcorres_expand_pfx) apply (clarsimp simp:update_thread_def tcb_at_def) apply (rule select_pick_corres[where S = UNIV,simplified]) apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (rule dcorres_gets_the) apply (clarsimp simp:opt_object_tcb not_idle_thread_def) apply (simp add:transform_tcb_def) apply (rule corres_guard_imp) apply (rule_tac s' = s'a in dcorres_set_object_tcb) apply (clarsimp simp:transform_tcb_def) apply (simp add: get_etcb_def) apply (clarsimp dest!: get_tcb_SomeD get_etcb_SomeD split:option.splits)+ apply (clarsimp simp: opt_object_tcb not_idle_thread_def dest!:get_tcb_rev get_etcb_rev) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (thread_set (tcb_ipc_buffer_update (\<lambda>_. a)) y) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do new_intent <- select UNIV;
KHeap_D.get_object y >>= case_cdl_object fail fail (\<lambda>tcb. KHeap_D.set_object y (Tcb (dupdate_tcb_intent new_intent tcb))) (\<lambda>cdl_cnode_ext. fail) (\<lambda>cdl_asid_pool_ext. fail) (\<lambda>cdl_page_table_ext. fail) (\<lambda>cdl_page_directory_ext. fail) (\<lambda>cdl_frame_ext. fail) fail (\<lambda>cdl_irq_node_ext. fail)
od) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.get_object y >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object y (Tcb (dupdate_tcb_intent (?x7 s' tcb) tcba))) (\<lambda>cdl_cnode_ext. fail) (\<lambda>cdl_asid_pool_ext. fail) (\<lambda>cdl_page_table_ext. fail) (\<lambda>cdl_page_directory_ext. fail) (\<lambda>cdl_frame_ext. fail) fail (\<lambda>cdl_irq_node_ext. fail)) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.get_object y >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object y (Tcb (dupdate_tcb_intent (?x7 s' tcb) tcba))) (\<lambda>cdl_cnode_ext. fail) (\<lambda>cdl_asid_pool_ext. fail) (\<lambda>cdl_page_table_ext. fail) (\<lambda>cdl_page_directory_ext. fail) (\<lambda>cdl_frame_ext. fail) fail (\<lambda>cdl_irq_node_ext. fail)) (do tcb <- gets_the (get_tcb y);
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>))
od) proof (prove)
goal (2 subgoals):
 1. \<And>s' tcb s s'a obj obj'. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a = Some obj'; cdl_objects s y = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s'a) (case obj of Tcb tcba \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent (?x7 s' tcb) tcba)) | _ \<Rightarrow> fail) (KHeap_A.set_object y (TCB (obj'\<lparr>tcb_ipc_buffer := a\<rparr>)))
 2. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (case transform_tcb (machine_state s'a) y tcb etcb of Tcb tcba \<Rightarrow> KHeap_D.set_object y (Tcb (dupdate_tcb_intent (?x7 s'a tcb) tcba)) | _ \<Rightarrow> fail) (KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>)))
 2. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (KHeap_D.set_object y (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = ?x7 s'a tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>)))
 2. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q21 tcb s'a etcb) (?Q'21 tcb s'a etcb) (KHeap_D.set_object y (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = ?x7 s'a tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object y (TCB (tcb\<lparr>tcb_ipc_buffer := a\<rparr>)))
 2. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; transform s'a = s\<rbrakk> \<Longrightarrow> ?Q21 tcb s'a etcb s
 3. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; s'a = s\<rbrakk> \<Longrightarrow> ?Q'21 tcb s'a etcb s
 4. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb'. transform_tcb (machine_state s'a) y (tcb\<lparr>tcb_ipc_buffer := a\<rparr>) etcb' = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op y (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = ?x7 s'a tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr> \<and> ekheap s'a y = Some etcb'
 2. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s'a
 3. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> kheap s'a y \<noteq> None
 4. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> ekheap s'a y \<noteq> None
 5. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; transform s'a = s\<rbrakk> \<Longrightarrow> transform s'a = s
 6. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; s'a = s\<rbrakk> \<Longrightarrow> s'a = s
 7. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> transform_full_intent (machine_state s'a) y (tcb\<lparr>tcb_ipc_buffer := a\<rparr>) = ?x7 s'a tcb \<and> (\<exists>etcb'. tcb_domain etcb' = tcb_domain etcb \<and> ekheap s'a y = Some etcb')
 2. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s'a
 3. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> kheap s'a y \<noteq> None
 4. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> ekheap s'a y \<noteq> None
 5. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; transform s'a = s\<rbrakk> \<Longrightarrow> transform s'a = s
 6. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; s'a = s\<rbrakk> \<Longrightarrow> s'a = s
 7. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s'a
 2. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> kheap s'a y \<noteq> None
 3. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> ekheap s'a y \<noteq> None
 4. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; transform s'a = s\<rbrakk> \<Longrightarrow> transform s'a = s
 5. \<And>tcb s'a etcb s. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb; s'a = s\<rbrakk> \<Longrightarrow> s'a = s
 6. \<And>s' tcb s s'a. \<lbrakk>get_tcb y s' = Some tcb; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; \<exists>etcb. get_etcb y s' = Some etcb; s = transform s'a; transform s' = s; s' = s'a; get_tcb y s'a \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s y \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>tcb s'a etcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; kheap s'a y = Some (TCB tcb); ekheap s'a y = Some etcb\<rbrakk> \<Longrightarrow> \<exists>ya. cdl_objects (transform s'a) y = Some ya proof (prove)
goal:
No subgoals!