theory KHeap_DR

lemma dmo_maskIRQ_dcorres:
  "dcorres dc \<top> \<top> (return ()) (do_machine_op (maskInterrupt b st))" supply option.case_cong[cong] apply (clarsimp simp: do_machine_op_def corres_underlying_def return_def select_f_def in_monad) apply (clarsimp simp: maskInterrupt_def in_monad) apply (clarsimp simp: transform_def transform_current_thread_def) apply (rule ext) apply (simp add: transform_objects_def option_map_def map_add_def
            split: option.split) apply (simp add: transform_object_def transform_tcb_def
                   transform_full_intent_def Let_def
            split: Structures_A.kernel_object.split) apply (clarsimp simp: transform_intent_def cong: get_tcb_mrs_cong get_ipc_buffer_words_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do_machine_op (maskInterrupt b st)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do_machine_op (maskInterrupt b st)) proof (prove)
goal (1 subgoal):
 1. \<And>ba bb. ((), bb) \<in> fst (maskInterrupt b st (machine_state ba)) \<Longrightarrow> transform (update_machine bb ba) = transform ba proof (prove)
goal (1 subgoal):
 1. \<And>ba. transform (update_machine (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) ba) = transform ba proof (prove)
goal (1 subgoal):
 1. \<And>ba. transform_objects (update_machine (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) ba) = transform_objects ba proof (prove)
goal (1 subgoal):
 1. \<And>ba x. transform_objects (update_machine (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) ba) x = transform_objects ba x proof (prove)
goal (1 subgoal):
 1. \<And>ba x. \<forall>x2. (kheap ba |` (- {idle_thread ba})) x = Some x2 \<longrightarrow> transform_object (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) x ((ekheap ba |` (- {idle_thread ba})) x) x2 = transform_object (machine_state ba) x ((ekheap ba |` (- {idle_thread ba})) x) x2 proof (prove)
goal (1 subgoal):
 1. \<And>ba x. \<forall>x2. (kheap ba |` (- {idle_thread ba})) x = Some (TCB x2) \<longrightarrow> (case (ekheap ba |` (- {idle_thread ba})) x of Some x2a \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable x2), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable x2), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply x2), tcb_caller_slot \<mapsto> transform_cap (tcb_caller x2), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe x2), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op x (tcb_state x2), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (get_tcb_message_info x2))) (get_tcb_mrs (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) x2), cdl_intent_error = guess_error (mi_label (get_tcb_message_info x2)), cdl_intent_cap = arch_tcb_context_get (tcb_arch x2) cap_register, cdl_intent_extras = get_ipc_buffer_words (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) x2 [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info x2))], cdl_intent_recv_slot = case get_ipc_buffer_words (machine_state ba\<lparr>irq_masks := (irq_masks (machine_state ba))(st := b)\<rparr>) x2 [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain x2a\<rparr>) = (case (ekheap ba |` (- {idle_thread ba})) x of Some etcb \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable x2), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable x2), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply x2), tcb_caller_slot \<mapsto> transform_cap (tcb_caller x2), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe x2), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op x (tcb_state x2), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (get_tcb_message_info x2))) (get_tcb_mrs (machine_state ba) x2), cdl_intent_error = guess_error (mi_label (get_tcb_message_info x2)), cdl_intent_cap = arch_tcb_context_get (tcb_arch x2) cap_register, cdl_intent_extras = get_ipc_buffer_words (machine_state ba) x2 [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info x2))], cdl_intent_recv_slot = case get_ipc_buffer_words (machine_state ba) x2 [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) proof (prove)
goal:
No subgoals!