theory Ipc_DR

lemma dcorres_dummy_set_pending_cap_Restart:
  "dcorres dc \<top> (st_tcb_at ((=) Structures_A.thread_state.Restart) thread and not_idle_thread thread and valid_etcbs)
  (KHeap_D.set_cap (thread, tcb_pending_op_slot) RestartCap) (return ())" apply (simp add:KHeap_D.set_cap_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:st_tcb_at_def obj_at_def dest!:get_tcb_rev) apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (frule opt_object_tcb, simp) apply (simp add:not_idle_thread_def) apply (clarsimp simp:assert_opt_def update_slots_def
    transform_tcb_def has_slots_def object_slots_def) apply (simp add:KHeap_D.set_object_def simpler_modify_def) apply (clarsimp simp:corres_underlying_def return_def) apply (simp add:transform_def) apply (rule ext,clarsimp) apply (fastforce dest!: get_tcb_SomeD
    simp add: not_idle_thread_def
    transform_objects_def transform_tcb_def
    infer_tcb_pending_op_def runnable_def tcb_slots
    split : Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (st_tcb_at ((=) Restart) thread and not_idle_thread thread and valid_etcbs) (KHeap_D.set_cap (thread, tcb_pending_op_slot) RestartCap) (return ()) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (st_tcb_at ((=) Restart) thread and not_idle_thread thread and valid_etcbs) (do x <- get;
obj <- assert_opt (cdl_objects x thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (st_tcb_at ((=) Restart) thread and not_idle_thread thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (2 subgoals):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 2. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; cdl_objects (transform s') thread = Some (transform_tcb (machine_state s') thread tcb etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; cdl_objects (transform s') thread = Some (transform_tcb (machine_state s') thread tcb etcb)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do obj <- assert_opt (cdl_objects (transform s') thread);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj of Tcb t \<Rightarrow> if tcb_pending_op_slot = tcb_ipcbuffer_slot \<and> object_slots obj tcb_pending_op_slot \<noteq> Some RestartCap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(tcb_pending_op_slot \<mapsto> RestartCap)) obj)) >>= KHeap_D.set_object thread
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; cdl_objects (transform s') thread = Some (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> RestartCap, 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 = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_object thread (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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb), tcb_pending_op_slot \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; cdl_objects (transform s') thread = Some (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> RestartCap, 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 = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (\<lambda>a. ({((), dupdate_cdl_object thread (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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb), tcb_pending_op_slot \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) a)}, False)) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; cdl_objects (transform s') thread = Some (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> RestartCap, 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 = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> transform s' = dupdate_cdl_object thread (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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb), tcb_pending_op_slot \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform s') proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; transform_objects s' thread = Some (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> RestartCap, 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 = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> transform_objects s' = (transform_objects s')(thread \<mapsto> 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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb), tcb_pending_op_slot \<mapsto> RestartCap], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>not_idle_thread thread s'; valid_etcbs s'; Restart = tcb_state tcb; get_tcb thread s' = Some tcb; get_etcb thread s' = Some etcb; transform_objects s' thread = Some (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> RestartCap, 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 = transform_full_intent (machine_state s') thread tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> [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> RestartCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)] = [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_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb), tcb_pending_op_slot \<mapsto> RestartCap] proof (prove)
goal:
No subgoals!