theory KHeap_DR

lemma transform_full_intent_update_tcb_state[simp]:
  "transform_full_intent m ptr (update_tcb_state st a)
  = transform_full_intent m ptr a" apply (case_tac a) apply (simp add:transform_full_intent_def Let_def) apply (simp add:get_tcb_message_info_def
    get_tcb_mrs_def get_ipc_buffer_words_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_full_intent m ptr (update_tcb_state st a) = transform_full_intent m ptr a proof (prove)
goal (1 subgoal):
 1. \<And>tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. a = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr> \<Longrightarrow> transform_full_intent m ptr (update_tcb_state st a) = transform_full_intent m ptr a proof (prove)
goal (1 subgoal):
 1. \<And>tcb_ctable tcb_vtable tcb_reply tcb_caller tcb_ipcframe tcb_state tcb_fault_handler tcb_ipc_buffer tcb_fault tcb_bound_notification tcb_mcpriority tcb_arch. a = \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr> \<Longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>))) (get_tcb_mrs m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>) = transform_intent (invocation_type (mi_label (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>))) (get_tcb_mrs m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>) \<and> guess_error (mi_label (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>)) = guess_error (mi_label (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>)) \<and> get_ipc_buffer_words m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>))] = get_ipc_buffer_words m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr> [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<rparr>))] \<and> (case get_ipc_buffer_words m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = st, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<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) = (case get_ipc_buffer_words m \<lparr>tcb_ctable = tcb_ctable, tcb_vtable = tcb_vtable, tcb_reply = tcb_reply, tcb_caller = tcb_caller, tcb_ipcframe = tcb_ipcframe, tcb_state = tcb_state, tcb_fault_handler = tcb_fault_handler, tcb_ipc_buffer = tcb_ipc_buffer, tcb_fault = tcb_fault, tcb_bound_notification = tcb_bound_notification, tcb_mcpriority = tcb_mcpriority, tcb_arch = tcb_arch\<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) proof (prove)
goal:
No subgoals!