theory Syscall_DR

lemma decode_invocation_corres':
  "\<lbrakk>(\<lambda>(cap, slot, extra) (slot', cap', extra', buffer).
     cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' \<and> extra = transform_cap_list extra')
     rv rv'; get_tcb (cur_thread s) s = Some ctcb; ct_running s;invs s\<rbrakk>
  \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top>
    ((=) s and (\<lambda>(slot,cap,excaps,buffer) s. \<not> is_master_reply_cap (cap) \<and> valid_cap cap s \<and> valid_etcbs s
    \<and> evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some buffer
    \<and> (\<forall>e\<in> set excaps. s \<turnstile> fst e) \<and> cte_wp_at (Not \<circ> is_master_reply_cap) slot s \<and> cte_wp_at ((=) cap) slot s
    \<and> (\<forall>e\<in> set excaps. cte_wp_at ((=) (fst e)) (snd e) s)) rv')
     ((\<lambda>(cap, cap_ref, extra_caps).
          case_option (if ep_related_cap cap then Decode_D.decode_invocation cap cap_ref extra_caps undefined else Monads_D.throw)
          (Decode_D.decode_invocation cap cap_ref extra_caps)
          (cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb)))
     rv)
     ((\<lambda>(slot, cap, extracaps, buffer).
          do args \<leftarrow> get_mrs (cur_thread s) buffer (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register));
          Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) args
          (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) slot cap extracaps
         od)
     rv')" apply (rule dcorres_expand_pfx) apply (clarsimp split del:if_split) apply (rule_tac Q' ="\<lambda>r ns. ns = s
     \<and> r =  get_tcb_mrs (machine_state s) ctcb"
     in corres_symb_exec_r) apply (clarsimp split:option.split | rule conjI)+ apply (rule corres_guard_imp[OF decode_invocation_ep_related_branch]) apply clarsimp+ defer apply clarsimp apply (rule dcorres_expand_pfx) apply (rule corres_guard_imp[OF decode_invocation_corres]) apply (clarsimp simp:transform_full_intent_def Let_def get_tcb_message_info_def)+ apply (wp get_tcb_mrs_wp | clarsimp)+ apply (rule dcorres_expand_pfx) apply (rule dcorres_free_throw[OF decode_invocation_error_branch]) apply (clarsimp simp:transform_full_intent_def Let_def get_tcb_message_info_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case rv of (cap, slot, extra) \<Rightarrow> \<lambda>(slot', cap', extra', buffer). cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' \<and> extra = transform_cap_list extra') rv'; get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) ((=) s and (case rv' of (slot, cap, excaps, buffer) \<Rightarrow> \<lambda>s. \<not> is_master_reply_cap cap \<and> s \<turnstile> cap \<and> valid_etcbs s \<and> evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some buffer \<and> (\<forall>e\<in>set excaps. s \<turnstile> fst e) \<and> cte_wp_at (Not \<circ> is_master_reply_cap) slot s \<and> cte_wp_at ((=) cap) slot s \<and> (\<forall>e\<in>set excaps. cte_wp_at ((=) (fst e)) (snd e) s))) (case rv of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) of None \<Rightarrow> if ep_related_cap cap then Decode_D.decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> Decode_D.decode_invocation cap cap_ref extra_caps x) (case rv' of (slot, cap, extracaps, buffer) \<Rightarrow> do args <- get_mrs (cur_thread s) buffer (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register));
Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) args (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) slot cap extracaps
od) proof (prove)
goal (1 subgoal):
 1. \<And>sa s'. \<lbrakk>(case rv of (cap, slot, extra) \<Rightarrow> \<lambda>(slot', cap', extra', buffer). cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' \<and> extra = transform_cap_list extra') rv'; get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; sa = transform s'; True; ((=) s and (case rv' of (slot, cap, excaps, buffer) \<Rightarrow> \<lambda>s. \<not> is_master_reply_cap cap \<and> s \<turnstile> cap \<and> valid_etcbs s \<and> evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some buffer \<and> (\<forall>e\<in>set excaps. s \<turnstile> fst e) \<and> cte_wp_at (Not \<circ> is_master_reply_cap) slot s \<and> cte_wp_at ((=) cap) slot s \<and> (\<forall>e\<in>set excaps. cte_wp_at ((=) (fst e)) (snd e) s))) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) sa) ((=) s') (case rv of (cap, cap_ref, extra_caps) \<Rightarrow> case cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) of None \<Rightarrow> if ep_related_cap cap then Decode_D.decode_invocation cap cap_ref extra_caps undefined else throw | Some x \<Rightarrow> Decode_D.decode_invocation cap cap_ref extra_caps x) (case rv' of (slot, cap, extracaps, buffer) \<Rightarrow> do args <- get_mrs (cur_thread s) buffer (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register));
Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) args (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) slot cap extracaps
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) ((=) s) (case cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) of None \<Rightarrow> if ep_related_cap (transform_cap ab) then Decode_D.decode_invocation (transform_cap ab) (a, b) (transform_cap_list ac) undefined else throw | Some x \<Rightarrow> Decode_D.decode_invocation (transform_cap ab) (a, b) (transform_cap_list ac) x) (do args <- get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register));
Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) args (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac
od) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (case cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) of None \<Rightarrow> if ep_related_cap (transform_cap ab) then Decode_D.decode_invocation (transform_cap ab) (a, b) (transform_cap_list ac) undefined else throw | Some x \<Rightarrow> Decode_D.decode_invocation (transform_cap ab) (a, b) (transform_cap_list ac) x) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 3. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) undefined) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None\<rbrakk> \<Longrightarrow> \<not> ep_related_cap (transform_cap ab) \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 3. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<forall>x2. cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2 \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 4. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 5. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) proof (prove)
goal (9 subgoals):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> ep_related_cap (transform_cap ab)
 2. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap ab
 3. \<And>a b aa bb ab ac bc rva sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; ep_related_cap (transform_cap ab); transform s = sa\<rbrakk> \<Longrightarrow> True
 4. \<And>a b aa bb ab ac bc rva sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; ep_related_cap (transform_cap ab); sa = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> True
 5. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None\<rbrakk> \<Longrightarrow> \<not> ep_related_cap (transform_cap ab) \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 6. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<forall>x2. cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2 \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 7. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 8. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<forall>x2. cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2 \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 3. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 4. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<forall>x2. cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2 \<longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 3. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))
 5. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab ac bc rva x2. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 3. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))
 5. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (5 subgoals):
 1. \<And>a b aa bb ab ac bc rva x2 sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) sa) ((=) s') (Decode_D.decode_invocation (transform_cap ab) (transform_cslot_ptr (aa, bb)) (transform_cap_list ac) x2) (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac)
 2. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 3. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))
 5. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (10 subgoals):
 1. \<And>a b aa bb ab ac bc rva x2 sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> Some x2 = transform_intent (invocation_type (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))) rva
 2. \<And>a b aa bb ab ac bc rva x2 sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (aa, bb)
 3. \<And>a b aa bb ab ac bc rva x2 sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> transform_cap ab = transform_cap ab
 4. \<And>a b aa bb ab ac bc rva x2 sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> transform_cap_list ac = transform_cap_list ac
 5. \<And>a b aa bb ab ac bc rva x2 sa s' saa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb; sa = saa\<rbrakk> \<Longrightarrow> True
 6. \<And>a b aa bb ab ac bc rva x2 sa s' saa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = Some x2; sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb; s' = saa\<rbrakk> \<Longrightarrow> (invs and valid_cap ab and (\<lambda>s. \<forall>e\<in>set ac. s \<turnstile> fst e) and (cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) and cte_wp_at ((=) ab) (aa, bb)) and (\<lambda>s. \<forall>x\<in>set ac. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) saa
 7. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 8. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))
 10. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (4 subgoals):
 1. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r ns. ns = s \<and> r = get_tcb_mrs (machine_state s) ctcb\<rbrace>
 2. \<And>a b aa bb ab ac bc sa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>a b aa bb ab ac bc. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_mrs (cur_thread s) bc (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))
 4. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ac bc rva. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s)) (\<lambda>ns. ns = s \<and> rva = get_tcb_mrs (machine_state s) ctcb) throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa bb ab ac bc rva sa s'. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab); sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) sa) ((=) s') throw (Decode_A.decode_invocation (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register))) rva (to_bl (arch_tcb_context_get (tcb_arch ctcb) cap_register)) (aa, bb) ab ac) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa bb ab ac bc rva sa s' saa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab); sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> transform_intent (invocation_type (mi_label (data_to_message_info (arch_tcb_context_get (tcb_arch ctcb) msg_info_register)))) rva = None
 2. \<And>a b aa bb ab ac bc rva sa s' saa. \<lbrakk>get_tcb (cur_thread s) s = Some ctcb; ct_running s; invs s; rv = (transform_cap ab, transform_cslot_ptr (aa, bb), transform_cap_list ac); rv' = ((aa, bb), ab, ac, bc); \<not> is_master_reply_cap ab; (a, b) = transform_cslot_ptr (aa, bb); s \<turnstile> ab; valid_etcbs s; evalMonad (lookup_ipc_buffer False (cur_thread s)) s = Some bc; \<forall>e\<in>set ac. s \<turnstile> fst e; cte_wp_at (Not \<circ> is_master_reply_cap) (aa, bb) s; cte_wp_at ((=) ab) (aa, bb) s; \<forall>e\<in>set ac. cte_wp_at ((=) (fst e)) (snd e) s; cdl_intent_op (transform_full_intent (machine_state s) (cur_thread s) ctcb) = None; \<not> ep_related_cap (transform_cap ab); sa = transform s'; transform s = sa; s' = s \<and> rva = get_tcb_mrs (machine_state s) ctcb\<rbrakk> \<Longrightarrow> \<not> ep_related_cap (transform_cap ab) proof (prove)
goal:
No subgoals!