theory Intent_DR

lemma transform_full_intent_no_ipc_buffer:
    "\<not> (is_arch_page_cap (tcb_ipcframe tcb)) \<Longrightarrow> transform_full_intent ms ptr tcb = transform_full_intent ms' ptr tcb" unfolding transform_full_intent_def apply (clarsimp simp: evalMonad_def Let_def return_def get_tcb_mrs_def
     split:if_splits cap.splits arch_cap.splits) apply (simp add: get_ipc_frame_words_no_ipc_buffer) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_page_cap (tcb_ipcframe tcb) \<Longrightarrow> transform_full_intent ms ptr tcb = transform_full_intent ms' ptr tcb proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_page_cap (tcb_ipcframe tcb) \<Longrightarrow> (let mi = get_tcb_message_info tcb; offset = msg_max_length + msg_max_extra_caps + 2 in \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label mi)) (get_tcb_mrs ms tcb), cdl_intent_error = guess_error (mi_label mi), cdl_intent_cap = arch_tcb_context_get (tcb_arch tcb) cap_register, cdl_intent_extras = get_ipc_buffer_words ms tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)], cdl_intent_recv_slot = case get_ipc_buffer_words ms tcb [offset..<offset + 3] 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>) = (let mi = get_tcb_message_info tcb; offset = msg_max_length + msg_max_extra_caps + 2 in \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label mi)) (get_tcb_mrs ms' tcb), cdl_intent_error = guess_error (mi_label mi), cdl_intent_cap = arch_tcb_context_get (tcb_arch tcb) cap_register, cdl_intent_extras = get_ipc_buffer_words ms' tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)], cdl_intent_recv_slot = case get_ipc_buffer_words ms' tcb [offset..<offset + 3] 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>) proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_page_cap (tcb_ipcframe tcb) \<Longrightarrow> (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (get_ipc_buffer_words ms tcb ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (get_ipc_buffer_words ms' tcb ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))) \<and> get_ipc_buffer_words ms tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] = get_ipc_buffer_words ms' tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] \<and> (case get_ipc_buffer_words ms tcb [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 ms' tcb [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)) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (get_ipc_buffer_words ms tcb [])) = transform_intent (invocation_type (mi_label (get_tcb_message_info tcb))) (take (unat (mi_length (get_tcb_message_info tcb))) (map (arch_tcb_context_get (tcb_arch tcb)) msg_registers) @ take (unat (mi_length (get_tcb_message_info tcb)) - length msg_registers) (get_ipc_buffer_words ms' tcb [])) \<and> get_ipc_buffer_words ms tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] = get_ipc_buffer_words ms' tcb [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))] \<and> (case get_ipc_buffer_words ms tcb [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 ms' tcb [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!