theory Syscall_DR

lemma dcorres_set_intent_error:
  "dcorres dc \<top>
    (invs and valid_etcbs and (\<lambda>s.  \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er
    \<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) (mark_tcb_intent_error oid er) (return a)" apply (clarsimp simp:mark_tcb_intent_error_def bind_assoc
                       gets_the_def update_thread_def gets_def ) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: not_idle_thread_def) apply (frule ko_at_tcb_at) apply (frule(1) tcb_at_is_etcb_at) apply (clarsimp simp:tcb_at_def is_etcb_at_def, fold get_etcb_def) apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def KHeap_D.set_object_def
                       simpler_modify_def corres_underlying_def) apply (simp add:transform_def return_def) apply (rule ext) apply (clarsimp simp:transform_objects_def transform_tcb_def
                  dest!:get_tcb_SomeD get_etcb_SomeD) apply (simp add:transform_full_intent_def Let_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) (mark_tcb_intent_error oid er) (return a) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) (do x <- get;
assert_opt (cdl_objects x oid) >>= case_cdl_object fail fail (\<lambda>tcb. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcb\<lparr>cdl_intent_error := er\<rparr>) 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) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (invs and valid_etcbs and (\<lambda>s. \<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and> ko_at (TCB tcb) oid s) and not_idle_thread oid) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (assert_opt (cdl_objects (transform s') oid) >>= case_cdl_object fail fail (\<lambda>tcb. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcb\<lparr>cdl_intent_error := er\<rparr>) 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)) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (assert_opt (cdl_objects (transform s') oid) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>) 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)) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); tcb_at oid s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (assert_opt (cdl_objects (transform s') oid) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>) 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)) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); tcb_at oid s'; is_etcb_at oid s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (assert_opt (cdl_objects (transform s') oid) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>) 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)) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb tcba y. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); get_tcb oid s' = Some tcba; get_etcb oid s' = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (assert_opt (cdl_objects (transform s') oid) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object oid (Tcb (dupdate_tcb_intent (cdl_tcb_intent tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>) 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)) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb tcba y aa b. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); get_tcb oid s' = Some tcba; get_etcb oid s' = Some y; (aa, b) \<in> fst (return a s')\<rbrakk> \<Longrightarrow> transform b = dupdate_cdl_object oid (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcba), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcba), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcba), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcba), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcba), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op oid (tcb_state tcba), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcba)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcba), cdl_tcb_intent = transform_full_intent (machine_state s') oid tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault tcba = Some y, cdl_tcb_domain = tcb_domain y\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb tcba y aa. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); get_tcb oid s' = Some tcba; get_etcb oid s' = Some y; aa = a\<rbrakk> \<Longrightarrow> transform_objects s' = (transform_objects s')(oid \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcba), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcba), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcba), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcba), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcba), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op oid (tcb_state tcba), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcba)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcba), cdl_tcb_intent = transform_full_intent (machine_state s') oid tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault tcba = Some y, cdl_tcb_domain = tcb_domain y\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb tcba y aa x. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); get_tcb oid s' = Some tcba; get_etcb oid s' = Some y; aa = a\<rbrakk> \<Longrightarrow> transform_objects s' x = ((transform_objects s')(oid \<mapsto> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcba), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcba), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcba), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcba), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcba), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op oid (tcb_state tcba), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcba)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcba), cdl_tcb_intent = transform_full_intent (machine_state s') oid tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault tcba = Some y, cdl_tcb_domain = tcb_domain y\<rparr>)) x proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb tcba y. \<lbrakk>invs s'; valid_etcbs s'; oid \<noteq> idle_thread s'; ko_at (TCB tcb) oid s'; er = guess_error (mi_label (get_tcb_message_info tcb)); ekheap s' oid = Some y; kheap s' oid = Some (TCB tcba)\<rbrakk> \<Longrightarrow> transform_full_intent (machine_state s') oid tcba = transform_full_intent (machine_state s') oid tcba\<lparr>cdl_intent_error := guess_error (mi_label (get_tcb_message_info tcb))\<rparr> proof (prove)
goal:
No subgoals!