theory Syscall_R

lemma dec_dom_inv_wf[wp]:
  "\<lbrace>invs' and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile>' fst x)\<rbrace>
  decodeDomainInvocation label args excaps
  \<lbrace>\<lambda>x s. tcb_at' (fst x) s \<and> snd x \<le> maxDomain\<rbrace>, -" apply (simp add:decodeDomainInvocation_def) apply (wp whenE_throwError_wp | wpc |simp)+ apply clarsimp apply (drule_tac x = "hd excaps" in bspec) apply (rule hd_in_set) apply (simp add:null_def) apply (simp add:valid_cap'_def) apply (simp add:not_le) apply (simp del: Word.of_nat_unat flip: ucast_nat_def) apply (rule word_of_nat_le) apply (simp add: le_maxDomain_eq_less_numDomains) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s)\<rbrace> decodeDomainInvocation label args excaps \<lbrace>\<lambda>x s. tcb_at' (fst x) s \<and> snd x \<le> maxDomain\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. \<forall>x\<in>set excaps. valid_cap' (fst x) s)\<rbrace> doE y <- whenE (gen_invocation_type label \<noteq> DomainSetSet) (throwError Fault_H.syscall_error.IllegalOperation);
domain <- case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | x # xa \<Rightarrow> doE whenE (numDomains \<le> fromIntegral x) $ throw (Fault_H.syscall_error.InvalidArgument 0);
returnOk $ fromIntegral x
odE;
y <- whenE (null excaps) (throwError Fault_H.syscall_error.TruncatedMessage);
case fst (hd excaps) of capability.ThreadCap ptr \<Rightarrow> returnOk $ (ptr, domain) | _ \<Rightarrow> throw (Fault_H.syscall_error.InvalidArgument 1)
odE \<lbrace>\<lambda>x s. tcb_at' (fst x) s \<and> snd x \<le> maxDomain\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> (\<forall>x\<in>set excaps. valid_cap' (fst x) s) \<Longrightarrow> gen_invocation_type label = DomainSetSet \<longrightarrow> (\<forall>x. \<not> numDomains \<le> unat x \<longrightarrow> (\<exists>xa. args = x # xa) \<longrightarrow> \<not> null excaps \<longrightarrow> (\<forall>xa. fst (hd excaps) = capability.ThreadCap xa \<longrightarrow> tcb_at' xa s \<and> UCAST(32 \<rightarrow> 8) x \<le> maxDomain)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; \<forall>x\<in>set excaps. valid_cap' (fst x) s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb\<rbrakk> \<Longrightarrow> tcb_at' xb s \<and> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb\<rbrakk> \<Longrightarrow> hd excaps \<in> set excaps
 2. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; valid_cap' (fst (hd excaps)) s\<rbrakk> \<Longrightarrow> tcb_at' xb s \<and> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb\<rbrakk> \<Longrightarrow> excaps \<noteq> []
 2. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; valid_cap' (fst (hd excaps)) s\<rbrakk> \<Longrightarrow> tcb_at' xb s \<and> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; valid_cap' (fst (hd excaps)) s\<rbrakk> \<Longrightarrow> tcb_at' xb s \<and> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; \<not> numDomains \<le> unat x; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; capAligned (capability.ThreadCap xb) \<and> tcb_at' xb s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; unat x < numDomains; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; capAligned (capability.ThreadCap xb) \<and> tcb_at' xb s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; unat x < numDomains; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; capAligned (capability.ThreadCap xb) \<and> tcb_at' xb s\<rbrakk> \<Longrightarrow> word_of_nat (unat x) \<le> maxDomain proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>invs' s; gen_invocation_type label = DomainSetSet; unat x < numDomains; args = x # xa; \<not> null excaps; fst (hd excaps) = capability.ThreadCap xb; capAligned (capability.ThreadCap xb) \<and> tcb_at' xb s\<rbrakk> \<Longrightarrow> unat x \<le> unat maxDomain proof (prove)
goal:
No subgoals!