theory CNode_DR

lemma transform_default_tcb:
  "transform_tcb ms y Structures_A.default_tcb Deterministic_A.default_etcb = cdl_default_tcb" apply (clarsimp simp:Structures_A.default_tcb_def tcb_registers_caps_merge_def
    transform_tcb_def infer_tcb_pending_op_def new_context_def default_arch_tcb_def) apply (clarsimp simp:get_tcb_message_info_def arch_tcb_context_get_def
                       transform_full_intent_def get_tcb_mrs_def Let_def neq_CPSR ) apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length]) apply (simp add:transform_intent_invalid_invocation) apply (simp add:get_ipc_buffer_words_def cdl_default_tcb_def guess_error_def
                  data_to_message_info_def default_etcb_def default_domain_def tcb_slot_defs
                  infer_tcb_bound_notification_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_tcb ms y Structures_A.default_tcb default_etcb = cdl_default_tcb proof (prove)
goal (1 subgoal):
 1. Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> cdl_cap.NullCap, tcb_vspace_slot \<mapsto> cdl_cap.NullCap, tcb_replycap_slot \<mapsto> cdl_cap.NullCap, tcb_caller_slot \<mapsto> cdl_cap.NullCap, tcb_ipcbuffer_slot \<mapsto> cdl_cap.NullCap, tcb_pending_op_slot \<mapsto> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification None], cdl_tcb_fault_endpoint = 0, cdl_tcb_intent = transform_full_intent ms y \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr>, cdl_tcb_has_fault = False, cdl_tcb_domain = tcb_domain default_etcb\<rparr> = cdl_default_tcb proof (prove)
goal (1 subgoal):
 1. (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> cdl_cap.NullCap, tcb_vspace_slot \<mapsto> cdl_cap.NullCap, tcb_replycap_slot \<mapsto> cdl_cap.NullCap, tcb_caller_slot \<mapsto> cdl_cap.NullCap, tcb_ipcbuffer_slot \<mapsto> cdl_cap.NullCap, tcb_pending_op_slot \<mapsto> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification None], cdl_tcb_fault_endpoint = 0, cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (data_to_message_info 0))) (take (unat (mi_length (data_to_message_info 0))) (map ((\<lambda>r. 0)(CPSR := 0x150)) msg_registers) @ take (unat (mi_length (data_to_message_info 0)) - length msg_registers) (get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))), cdl_intent_error = guess_error (mi_label (data_to_message_info 0)), cdl_intent_cap = 0, cdl_intent_extras = get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info 0))], cdl_intent_recv_slot = case get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [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 = False, cdl_tcb_domain = tcb_domain default_etcb\<rparr> = cdl_default_tcb) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> cdl_cap.NullCap, tcb_vspace_slot \<mapsto> cdl_cap.NullCap, tcb_replycap_slot \<mapsto> cdl_cap.NullCap, tcb_caller_slot \<mapsto> cdl_cap.NullCap, tcb_ipcbuffer_slot \<mapsto> cdl_cap.NullCap, tcb_pending_op_slot \<mapsto> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification None], cdl_tcb_fault_endpoint = 0, cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (data_to_message_info 0))) (take (unat (mi_length (data_to_message_info 0))) (map ((\<lambda>r. 0)(CPSR := 0x150)) msg_registers)), cdl_intent_error = guess_error (mi_label (data_to_message_info 0)), cdl_intent_cap = 0, cdl_intent_extras = get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info 0))], cdl_intent_recv_slot = case get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [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 = False, cdl_tcb_domain = tcb_domain default_etcb\<rparr> = cdl_default_tcb) proof (prove)
goal (1 subgoal):
 1. Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> cdl_cap.NullCap, tcb_vspace_slot \<mapsto> cdl_cap.NullCap, tcb_replycap_slot \<mapsto> cdl_cap.NullCap, tcb_caller_slot \<mapsto> cdl_cap.NullCap, tcb_ipcbuffer_slot \<mapsto> cdl_cap.NullCap, tcb_pending_op_slot \<mapsto> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification None], cdl_tcb_fault_endpoint = 0, cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (data_to_message_info 0))) (take (unat (mi_length (data_to_message_info 0))) (map ((\<lambda>r. 0)(CPSR := 0x150)) msg_registers) @ take (unat (mi_length (data_to_message_info 0)) - length msg_registers) (get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))), cdl_intent_error = guess_error (mi_label (data_to_message_info 0)), cdl_intent_cap = 0, cdl_intent_extras = get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info 0))], cdl_intent_recv_slot = case get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [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 = False, cdl_tcb_domain = tcb_domain default_etcb\<rparr> = cdl_default_tcb proof (prove)
goal (1 subgoal):
 1. Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> cdl_cap.NullCap, tcb_vspace_slot \<mapsto> cdl_cap.NullCap, tcb_replycap_slot \<mapsto> cdl_cap.NullCap, tcb_caller_slot \<mapsto> cdl_cap.NullCap, tcb_ipcbuffer_slot \<mapsto> cdl_cap.NullCap, tcb_pending_op_slot \<mapsto> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification None], cdl_tcb_fault_endpoint = 0, cdl_tcb_intent = \<lparr>cdl_intent_op = None, cdl_intent_error = guess_error (mi_label (data_to_message_info 0)), cdl_intent_cap = 0, cdl_intent_extras = get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info 0))], cdl_intent_recv_slot = case get_ipc_buffer_words ms \<lparr>tcb_ctable = cap.NullCap, tcb_vtable = cap.NullCap, tcb_reply = cap.NullCap, tcb_caller = cap.NullCap, tcb_ipcframe = cap.NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = \<lparr>tcb_context = (\<lambda>r. 0)(CPSR := 0x150)\<rparr>\<rparr> [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 = False, cdl_tcb_domain = tcb_domain default_etcb\<rparr> = cdl_default_tcb proof (prove)
goal:
No subgoals!