theory Intent_DR

lemma set_message_info_corres:
  "dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y)
             (set_message_info y m)" apply (clarsimp simp:set_message_info_def) apply (clarsimp simp:as_user_def setRegister_def) apply (rule dcorres_absorb_gets_the) apply (clarsimp simp:get_tcb_def split:option.splits Structures_A.kernel_object.splits) apply (subst modify_def[unfolded bind_def]|clarsimp simp:get_def put_def)+ apply (frule_tac ptr=y and tcb=obj' in valid_etcbs_tcb_etcb, clarsimp, clarsimp) apply (clarsimp simp:select_f_def bind_def arch_tcb_update_aux3) apply (rule corres_guard_imp) apply (erule set_cxt_none_det_intent_corres) apply (clarsimp simp: valid_def get_tcb_def lift_simp not_idle_thread_def transform_tcb_def
                   split: option.splits Structures_A.kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (set_message_info y m) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (as_user y (setRegister msg_info_register (message_info_to_data m))) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do tcb <- gets_the (get_tcb y);
(a, uc') <- select_f (modify (\<lambda>uc. uc(msg_info_register := message_info_to_data m)) (arch_tcb_context_get (tcb_arch tcb)));
KHeap_A.set_object y (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(valid_idle and not_idle_thread y and valid_etcbs) s'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f (modify (\<lambda>uc. uc(msg_info_register := message_info_to_data m)) (arch_tcb_context_get (tcb_arch obj')));
KHeap_A.set_object y (TCB (obj'\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch obj')\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f (modify (\<lambda>uc. uc(msg_info_register := message_info_to_data m)) (arch_tcb_context_get (tcb_arch obj')));
KHeap_A.set_object y (TCB (obj'\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch obj')\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f ({((), (arch_tcb_context_get (tcb_arch obj'))(msg_info_register := message_info_to_data m))}, False);
KHeap_A.set_object y (TCB (obj'\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch obj')\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f ({((), (arch_tcb_context_get (tcb_arch obj'))(msg_info_register := message_info_to_data m))}, False);
KHeap_A.set_object y (TCB (obj'\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch obj')\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set ((arch_tcb_context_get (tcb_arch obj'))(msg_info_register := message_info_to_data m))) obj'))) proof (prove)
goal (3 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc (?Q50 s' obj' etcb) (?Q'50 s' obj' etcb) (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set ((arch_tcb_context_get (tcb_arch obj'))(msg_info_register := message_info_to_data m))) obj')))
 2. \<And>s' obj' etcb s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q50 s' obj' etcb s
 3. \<And>s' obj' etcb s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'50 s' obj' etcb s proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' y \<noteq> None
 2. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> valid_idle s'
 3. \<And>s' obj' etcb. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> not_idle_thread y s'
 4. \<And>s' obj' etcb s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> transform s' = s
 5. \<And>s' obj' etcb s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ekheap s' y = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s' = s proof (prove)
goal:
No subgoals!