theory Intent_DR

lemma dummy_corrupt_tcb_intent_corres:
  "dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs)
    (corrupt_tcb_intent y) (return a)" apply (simp add:corrupt_tcb_intent_def not_idle_thread_def) apply (rule dcorres_expand_pfx, clarsimp) apply (clarsimp simp:tcb_at_def) apply (drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (rule corres_guard_imp) apply (rule_tac P="(=)(transform s')" and Q="(=) s'" and
                    x="transform_full_intent (machine_state s') y tcb" in select_pick_corres) apply (clarsimp simp:update_thread_def gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def) apply (clarsimp simp:KHeap_D.set_object_def get_def put_def modify_def assert_def bind_def return_def) apply (subst corres_singleton) apply (clarsimp simp:dc_def) apply (clarsimp simp:transform_def) apply (rule ext) apply (clarsimp simp: restrict_map_Some_iff transform_objects_def
                   split: option.splits dest!:get_tcb_SomeD get_etcb_SomeD) apply (clarsimp simp: transform_tcb_def) apply (clarsimp simp:transform_def)+ 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) (return a) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and (\<lambda>s. y \<noteq> idle_thread s) and valid_etcbs) (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>tcb_at y s'; valid_idle s'; y \<noteq> idle_thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; valid_etcbs s'; get_tcb y s' = Some tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (return a) proof (prove)
goal (1 subgoal):
 1. \<And>s' tcb etcb. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (return a) proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb etcb. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q11 s' tcb etcb) (?Q'11 s' tcb etcb) (do new_intent <- select UNIV;
update_thread y (dupdate_tcb_intent new_intent)
od) (return a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q11 s' tcb etcb s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'11 s' tcb etcb s proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb etcb. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (update_thread y (dupdate_tcb_intent (transform_full_intent (machine_state s') y tcb))) (return a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb etcb. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- get;
assert_opt (cdl_objects x y) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object y (Tcb (dupdate_tcb_intent (transform_full_intent (machine_state s') y 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)
od) (return a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb etcb s'a. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (assert_opt (cdl_objects (transform s'a) y) >>= case_cdl_object fail fail (\<lambda>tcba. KHeap_D.set_object y (Tcb (dupdate_tcb_intent (transform_full_intent (machine_state s') y 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)) (return a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread 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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) (return a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread 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) (\<lambda>s. ({((), dupdate_cdl_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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) s)}, False)) (\<lambda>s. ({(a, s)}, False))
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> \<forall>s s'. transform s'a = s \<and> s'a = s' \<and> (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> (False \<longrightarrow> \<not> False) \<longrightarrow> (dupdate_cdl_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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> dc () a
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> transform s'a = dupdate_cdl_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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) (transform s'a)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> transform_objects s'a = (transform_objects s'a)(y \<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_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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a x. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; get_tcb y s'a = Some tcb; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> transform_objects s'a x = ((transform_objects s'a)(y \<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_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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>)) x
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (3 subgoals):
 1. \<And>tcb etcb s'a. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; ekheap s'a y = Some etcb; kheap s'a y = Some (TCB tcb)\<rbrakk> \<Longrightarrow> transform_tcb (machine_state s'a) y tcb 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 = transform_full_intent (machine_state s'a) y tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 3. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal (2 subgoals):
 1. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((=) (transform s') and (\<lambda>s. transform_full_intent (machine_state s') y tcb \<in> UNIV)) s
 2. \<And>s' tcb etcb s. \<lbrakk>valid_idle s'; y \<noteq> idle_thread s'; get_tcb y s' = Some tcb; get_etcb y s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal:
No subgoals!