theory Syscall_DR

lemma decode_domain_cap_label_not_match:
  "\<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'\<rbrakk>
    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>" apply (case_tac "invocation_type label' = GenInvocationLabel DomainSetSet") apply (clarsimp simp: Decode_A.decode_domain_invocation_def transform_intent_def gen_invocation_type_eq)+ apply (clarsimp simp: transform_intent_domain_def split: option.splits list.splits) apply wp apply (simp add: Decode_A.decode_domain_invocation_def gen_invocation_type_eq) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args' \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; invocation_type label' = GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; invocation_type label' \<noteq> GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> map_option DomainIntent (transform_intent_domain args'); gen_invocation_type label' = DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE domain <- case args' of [] \<Rightarrow> throwError TruncatedMessage | x # xs \<Rightarrow> doE whenE (numDomains \<le> unat x) $ throwError $ InvalidArgument 0;
returnOk (UCAST(32 \<rightarrow> 8) x)
odE;
y <- whenE (excaps' = []) (throwError TruncatedMessage);
case fst (hd excaps') of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; invocation_type label' \<noteq> GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gen_invocation_type label' = DomainSetSet; args' = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>
 2. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; invocation_type label' \<noteq> GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; invocation_type label' \<noteq> GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'; gen_invocation_type label' \<noteq> DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal:
No subgoals!