theory Syscall_DR

lemma decode_invocation_replycap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label') args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.ReplyCap a b c \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> (cte_wp_at (Not\<circ> is_master_reply_cap) invoked_cap_ref' and
                                               cte_wp_at ((=) invoked_cap') invoked_cap_ref')
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def ) apply (rule dcorres_expand_pfx) apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def
           split:rights.splits) apply (clarsimp simp:cte_wp_at_def is_master_reply_cap_def) apply (rule corres_guard_imp[OF dcorres_returnOk]) apply (simp add:cdl_invocation_relation_def translate_invocation_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a b c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (cte_wp_at (Not \<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at ((=) invoked_cap') invoked_cap_ref') (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (cte_wp_at (Not \<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at ((=) (cap.ReplyCap a False c)) invoked_cap_ref') (returnOk (cdl_invocation.InvokeReply (ReplyMessage a (transform_cslot_ptr invoked_cap_ref') (AllowGrant \<in> c)))) (returnOk (invocation.InvokeReply a invoked_cap_ref' (AllowGrant \<in> c))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; s = transform s'; True; (cte_wp_at (Not \<circ> is_master_reply_cap) invoked_cap_ref' and cte_wp_at ((=) (cap.ReplyCap a False c)) invoked_cap_ref') s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) s) ((=) s') (returnOk (cdl_invocation.InvokeReply (ReplyMessage a (transform_cslot_ptr invoked_cap_ref') (AllowGrant \<in> c)))) (returnOk (invocation.InvokeReply a invoked_cap_ref' (AllowGrant \<in> c))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; cte_wp_at (Not \<circ> is_master_reply_cap) invoked_cap_ref' s'; cte_wp_at ((=) (cap.ReplyCap a False c)) invoked_cap_ref' s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s')) ((=) s') (returnOk (cdl_invocation.InvokeReply (ReplyMessage a (transform_cslot_ptr invoked_cap_ref') (AllowGrant \<in> c)))) (returnOk (invocation.InvokeReply a invoked_cap_ref' (AllowGrant \<in> c))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; fst (CSpaceAcc_A.get_cap invoked_cap_ref' s') = {(cap.ReplyCap a False c, s')}\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) ((=) (transform s')) ((=) s') (returnOk (cdl_invocation.InvokeReply (ReplyMessage a (transform_cslot_ptr invoked_cap_ref') (AllowGrant \<in> c)))) (returnOk (invocation.InvokeReply a invoked_cap_ref' (AllowGrant \<in> c))) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; fst (CSpaceAcc_A.get_cap invoked_cap_ref' s') = {(cap.ReplyCap a False c, s')}\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeReply (ReplyMessage a (transform_cslot_ptr invoked_cap_ref') (AllowGrant \<in> c))) (invocation.InvokeReply a invoked_cap_ref' (AllowGrant \<in> c))
 2. \<And>s' s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; fst (CSpaceAcc_A.get_cap invoked_cap_ref' s') = {(cap.ReplyCap a False c, s')}; transform s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.ReplyCap a c; excaps = transform_cap_list excaps'; invoked_cap' = cap.ReplyCap a False c; \<not> b; fst (CSpaceAcc_A.get_cap invoked_cap_ref' s') = {(cap.ReplyCap a False c, s')}; s' = s\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!