theory Syscall_DR

lemma transform_intent_domain_cap_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk>
     \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>" including no_pre supply gen_invocation_type_eq[symmetric, simp] apply (clarsimp simp: Decode_A.decode_invocation_def) apply wp apply (case_tac excaps, simp_all) apply (clarsimp simp: decode_domain_invocation_def) apply (case_tac args, simp_all) apply (wp whenE_inv whenE_inv[THEN valid_validE] | simp)+ apply (clarsimp simp: decode_domain_invocation_def) apply (case_tac args, simp_all) apply ((wp whenE_inv whenE_inv[THEN valid_validE] | simp)+)[1] apply (case_tac "invocation_type label \<noteq> GenInvocationLabel DomainSetSet", simp_all) apply wp apply (clarsimp simp: transform_intent_def transform_intent_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap.DomainCap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME (\<lambda>(x, y). invocation.InvokeDomain x y) (Decode_A.decode_domain_invocation label args excaps) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args excaps \<lbrace>(\<lambda>r _. False) \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args [] \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a list. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args (a # list) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
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;
throwError TruncatedMessage
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a list. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args (a # list) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>transform_intent (invocation_type label) [] = None; cap = cap.DomainCap; excaps = []; args = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
throwError TruncatedMessage
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a list. \<lbrakk>transform_intent (invocation_type label) (a # list) = None; cap = cap.DomainCap; excaps = []; args = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
domain <- doE y <- whenE (numDomains \<le> unat a) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) a)
odE;
throwError TruncatedMessage
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>a list. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args (a # list) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = a # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args (a # list) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list. \<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.DomainCap; excaps = (a, aa, b) # list\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
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;
case a of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b list. \<lbrakk>transform_intent (invocation_type label) [] = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = []\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
throwError TruncatedMessage
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a aa b list ab lista. \<lbrakk>transform_intent (invocation_type label) (ab # lista) = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = ab # lista\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
domain <- doE y <- whenE (numDomains \<le> unat ab) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) ab)
odE;
case a of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list ab lista. \<lbrakk>transform_intent (invocation_type label) (ab # lista) = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = ab # lista\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE y <- whenE (invocation_type label \<noteq> GenInvocationLabel DomainSetSet) (throwError IllegalOperation);
domain <- doE y <- whenE (numDomains \<le> unat ab) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) ab)
odE;
case a of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa b list ab lista. \<lbrakk>transform_intent (invocation_type label) (ab # lista) = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = ab # lista; invocation_type label \<noteq> GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> throwError IllegalOperation \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>a aa b list ab lista. \<lbrakk>transform_intent (GenInvocationLabel DomainSetSet) (ab # lista) = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = ab # lista; invocation_type label = GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE domain <- doE y <- whenE (numDomains \<le> unat ab) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) ab)
odE;
case a of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a aa b list ab lista. \<lbrakk>transform_intent (GenInvocationLabel DomainSetSet) (ab # lista) = None; cap = cap.DomainCap; excaps = (a, aa, b) # list; args = ab # lista; invocation_type label = GenInvocationLabel DomainSetSet\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE domain <- doE y <- whenE (numDomains \<le> unat ab) (throwError (InvalidArgument 0));
returnOk (UCAST(32 \<rightarrow> 8) ab)
odE;
case a of ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throwError $ InvalidArgument 1
odE \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal:
No subgoals!