theory Syscall_DR

lemma decode_invocation_ep_related_branch:
  "\<lbrakk>ep_related_cap (transform_cap cap);\<not> is_master_reply_cap cap\<rbrakk>
  \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
    (Decode_D.decode_invocation (transform_cap cap) (transform_cslot_ptr ref) caps intent)
    (Decode_A.decode_invocation label args index ref cap caps')" apply (clarsimp simp:ep_related_cap_def transform_cap_def split:cdl_cap.split_asm cap.split_asm arch_cap.split_asm) apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def | rule conjI)+ apply (rule corres_guard_imp[OF dcorres_returnOk],simp add:cdl_invocation_relation_def translate_invocation_def) apply simp+ apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def split:if_split_asm | rule conjI)+ apply (rule corres_guard_imp[OF dcorres_returnOk]) apply (simp add:cdl_invocation_relation_def translate_invocation_def)+ apply (clarsimp simp:Decode_D.decode_invocation_def Decode_A.decode_invocation_def is_master_reply_cap_def | rule conjI)+ 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>ep_related_cap (transform_cap cap); \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (transform_cap cap) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref cap caps') proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>\<not> is_master_reply_cap (cap.EndpointCap x31 x32 x33); cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.EndpointCap x31 x32 x33) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.EndpointCap x31 x32 x33) caps')
 2. \<And>x31 x32 x33 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.EndpointCap x31 x32 x33) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 3. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.NotificationCap x41 x42 x43) caps')
 4. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 5. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>\<not> is_master_reply_cap (cap.EndpointCap x31 x32 x33); cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cdl_invocation.InvokeEndpoint (SyncMessage x32 (AllowGrant \<in> x33) (AllowGrantReply \<in> x33) x31))) (returnOk (invocation.InvokeEndpoint x31 x32 (AllowGrant \<in> x33) (AllowGrantReply \<in> x33)))
 2. \<And>x31 x32 x33 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.EndpointCap x31 x32 x33) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 3. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.NotificationCap x41 x42 x43) caps')
 4. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 5. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>\<not> is_master_reply_cap (cap.EndpointCap x31 x32 x33); cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33; True\<rbrakk> \<Longrightarrow> True
 2. \<And>x31 x32 x33 s. \<lbrakk>\<not> is_master_reply_cap (cap.EndpointCap x31 x32 x33); cap = cap.EndpointCap x31 x32 x33; AllowWrite \<in> x33; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x31 x32 x33 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.EndpointCap x31 x32 x33) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 4. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.NotificationCap x41 x42 x43) caps')
 5. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 6. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.EndpointCap x31 x32 x33) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 2. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.NotificationCap x41 x42 x43) caps')
 3. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 4. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43; AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cdl_invocation.InvokeNotification (Signal x42 x41))) (returnOk (invocation.InvokeNotification x41 x42))
 2. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 3. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43; AllowWrite \<in> x43\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeNotification (Signal x42 x41)) (invocation.InvokeNotification x41 x42)
 2. \<And>x41 x42 x43 s. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43; AllowWrite \<in> x43; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x41 x42 x43 s. \<lbrakk>\<not> is_master_reply_cap (cap.NotificationCap x41 x42 x43); cap = cap.NotificationCap x41 x42 x43; AllowWrite \<in> x43; True\<rbrakk> \<Longrightarrow> True
 4. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 5. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 x43 x51 x52 x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51 x52 x53); cap = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = cdl_cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.NotificationCap x41 x42 x43) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51 x52 x53) caps')
 2. \<And>x51 x52 x51a x52a x53. \<lbrakk>\<not> is_master_reply_cap (cap.ReplyCap x51a x52a x53); cap = cap.ReplyCap x51a x52a x53; (if x52a then MasterReplyCap x51a else cdl_cap.ReplyCap x51a x53) = cdl_cap.ReplyCap x51 x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation (cdl_cap.ReplyCap x51 x52) (transform_cslot_ptr ref) caps intent) (Decode_A.decode_invocation label args index ref (cap.ReplyCap x51a x52a x53) caps') proof (prove)
goal (1 subgoal):
 1. \<And>x51 x52 x52a. \<lbrakk>\<not> x52a; cap = cap.ReplyCap x51 False x52\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cdl_invocation.InvokeReply (ReplyMessage x51 (transform_cslot_ptr ref) (AllowGrant \<in> x52)))) (returnOk (invocation.InvokeReply x51 ref (AllowGrant \<in> x52))) proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x52a. \<lbrakk>\<not> x52a; cap = cap.ReplyCap x51 False x52\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeReply (ReplyMessage x51 (transform_cslot_ptr ref) (AllowGrant \<in> x52))) (invocation.InvokeReply x51 ref (AllowGrant \<in> x52))
 2. \<And>x51 x52 x52a s. \<lbrakk>\<not> x52a; cap = cap.ReplyCap x51 False x52; True\<rbrakk> \<Longrightarrow> True
 3. \<And>x51 x52 x52a s. \<lbrakk>\<not> x52a; cap = cap.ReplyCap x51 False x52; True\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!