theory Tcb_DR

lemma option_update_thread_corres:
  "dcorres (dc \<oplus> dc) \<top> (not_idle_thread obj_id and valid_etcbs)
       (case map_option of_bl fault_ep' of None \<Rightarrow> returnOk ()
        | Some x \<Rightarrow> liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x)))
       (liftE (option_update_thread obj_id (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) fault_ep'))" apply (simp add:option_update_thread_def not_idle_thread_def) apply (case_tac fault_ep') apply (simp add:liftE_def bindE_def returnOk_def) apply clarsimp apply (simp add:update_thread_def thread_set_def get_thread_def bind_assoc) apply (rule dcorres_gets_the) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:opt_object_tcb transform_tcb_def) apply (rule dcorres_set_object_tcb) apply (clarsimp simp:transform_tcb_def infer_tcb_pending_op_def ) apply (simp add: get_etcb_def cong:transform_full_intent_caps_cong_weak) apply simp apply (clarsimp simp: get_tcb_def split:option.splits) apply (clarsimp simp: get_etcb_def split:option.splits) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:opt_object_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (not_idle_thread obj_id and valid_etcbs) (case map_option of_bl fault_ep' of None \<Rightarrow> returnOk () | Some x \<Rightarrow> liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x))) (liftE (option_update_thread obj_id (tcb_fault_handler_update \<circ> (\<lambda>x y. x)) fault_ep')) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (case fault_ep' of None \<Rightarrow> returnOk () | Some x \<Rightarrow> ((\<lambda>x. liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x))) \<circ> of_bl) x) (liftE (case fault_ep' of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (tcb_fault_handler_update (\<lambda>y. v)) obj_id)) proof (prove)
goal (2 subgoals):
 1. fault_ep' = None \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (case fault_ep' of None \<Rightarrow> returnOk () | Some x \<Rightarrow> ((\<lambda>x. liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x))) \<circ> of_bl) x) (liftE (case fault_ep' of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (tcb_fault_handler_update (\<lambda>y. v)) obj_id))
 2. \<And>a. fault_ep' = Some a \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (case fault_ep' of None \<Rightarrow> returnOk () | Some x \<Rightarrow> ((\<lambda>x. liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x))) \<circ> of_bl) x) (liftE (case fault_ep' of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (tcb_fault_handler_update (\<lambda>y. v)) obj_id)) proof (prove)
goal (1 subgoal):
 1. \<And>a. fault_ep' = Some a \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (case fault_ep' of None \<Rightarrow> returnOk () | Some x \<Rightarrow> ((\<lambda>x. liftE $ update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x))) \<circ> of_bl) x) (liftE (case fault_ep' of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (tcb_fault_handler_update (\<lambda>y. v)) obj_id)) proof (prove)
goal (1 subgoal):
 1. \<And>a. fault_ep' = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. of_bl a))) (thread_set (tcb_fault_handler_update (\<lambda>y. a)) obj_id) proof (prove)
goal (1 subgoal):
 1. \<And>a. fault_ep' = Some a \<Longrightarrow> dcorres dc (\<lambda>_. True) ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) (do t <- KHeap_D.get_object obj_id;
case t of Tcb tcb \<Rightarrow> KHeap_D.set_object obj_id (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := of_bl a\<rparr>)) | _ \<Rightarrow> fail
od) (do tcb <- gets_the (get_tcb obj_id);
KHeap_A.set_object obj_id (TCB (tcb\<lparr>tcb_fault_handler := a\<rparr>))
od) proof (prove)
goal (2 subgoals):
 1. \<And>a s s' obj obj'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' = Some obj'; cdl_objects s obj_id = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object obj_id (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := of_bl a\<rparr>)) | _ \<Rightarrow> fail) (KHeap_A.set_object obj_id (TCB (obj'\<lparr>tcb_fault_handler := a\<rparr>)))
 2. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>a s' obj obj'. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; cdl_objects (transform s') obj_id = Some obj; obj_id \<noteq> idle_thread s'; valid_etcbs s'; \<exists>etcb. get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case obj of Tcb tcb \<Rightarrow> KHeap_D.set_object obj_id (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := of_bl a\<rparr>)) | _ \<Rightarrow> fail) (KHeap_A.set_object obj_id (TCB (obj'\<lparr>tcb_fault_handler := a\<rparr>)))
 2. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_object obj_id (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op obj_id (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl a, cdl_tcb_intent = transform_full_intent (machine_state s') obj_id obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (KHeap_A.set_object obj_id (TCB (obj'\<lparr>tcb_fault_handler := a\<rparr>)))
 2. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb'. transform_tcb (machine_state s') obj_id (obj'\<lparr>tcb_fault_handler := a\<rparr>) etcb' = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable obj'), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable obj'), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply obj'), tcb_caller_slot \<mapsto> transform_cap (tcb_caller obj'), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe obj'), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op obj_id (tcb_state obj'), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification obj')], cdl_tcb_fault_endpoint = of_bl a, cdl_tcb_intent = transform_full_intent (machine_state s') obj_id obj', cdl_tcb_has_fault = \<exists>y. tcb_fault obj' = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr> \<and> ekheap s' obj_id = Some etcb'
 2. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> obj_id \<noteq> idle_thread s'
 3. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' obj_id \<noteq> None
 4. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' obj_id \<noteq> None
 5. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> transform_full_intent (machine_state s') obj_id (obj'\<lparr>tcb_fault_handler := a\<rparr>) = transform_full_intent (machine_state s') obj_id obj' \<and> (\<exists>etcb'. tcb_domain etcb' = tcb_domain etcb \<and> ekheap s' obj_id = Some etcb')
 2. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> obj_id \<noteq> idle_thread s'
 3. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' obj_id \<noteq> None
 4. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' obj_id \<noteq> None
 5. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> obj_id \<noteq> idle_thread s'
 2. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' obj_id \<noteq> None
 3. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' obj_id \<noteq> None
 4. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' obj_id \<noteq> None
 2. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' obj_id \<noteq> None
 3. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>a s' obj' etcb. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some obj'; obj_id \<noteq> idle_thread s'; valid_etcbs s'; get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' obj_id \<noteq> None
 2. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>a s s'. \<lbrakk>fault_ep' = Some a; s = transform s'; True; ((\<lambda>s. obj_id \<noteq> idle_thread s) and valid_etcbs) s'; get_tcb obj_id s' \<noteq> None\<rbrakk> \<Longrightarrow> cdl_objects s obj_id \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>a s' y. \<lbrakk>fault_ep' = Some a; get_tcb obj_id s' = Some y; obj_id \<noteq> idle_thread s'; valid_etcbs s'; \<exists>etcb. get_etcb obj_id s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. cdl_objects (transform s') obj_id = Some y proof (prove)
goal:
No subgoals!