kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_R

lemma decodeWriteReg_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
     decodeWriteRegisters args (ThreadCap t)
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeWriteRegisters_def whenE_def decodeTransfer_def
             cong: list.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeWriteRegisters args (capability.ThreadCap t) \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # n # values \<Rightarrow> doE y <- if genericLength values < n then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
self <- liftE getCurThread;
y <- if t = self then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (tcbinvocation.WriteRegisters t (flags !! 0) (genericTake n values) copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'6\<rbrace> case args of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | [flags] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | flags # n # values \<Rightarrow> doE y <- if genericLength values < n then throwError Fault_H.syscall_error.TruncatedMessage else returnOk ();
self <- liftE getCurThread;
y <- if t = self then throwError Fault_H.syscall_error.IllegalOperation else returnOk ();
returnOk (tcbinvocation.WriteRegisters t (flags !! 0) (genericTake n values) copy_register_sets.ARMNoExtraRegisters)
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> ?P'6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> (args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (xa = [] \<longrightarrow> True) \<and> (\<forall>xb xc. xa = xb # xc \<longrightarrow> True \<and> True \<and> True \<and> (genericLength xc < xb \<longrightarrow> True) \<and> (\<not> genericLength xc < xb \<longrightarrow> (t = ksCurThread s \<longrightarrow> True) \<and> (t \<noteq> ksCurThread s \<longrightarrow> tcb_inv_wf' (tcbinvocation.WriteRegisters t (x !! 0) (genericTake xb xc) copy_register_sets.ARMNoExtraRegisters) s)))) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma getMCP_sp:
  "\<lbrace>P\<rbrace> threadGet tcbMCP t \<lbrace>\<lambda>rv. mcpriority_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace>" apply (simp add: threadGet_def) apply wp apply (simp add: o_def pred_tcb_at'_def) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> threadGet tcbMCP t \<lbrace>\<lambda>rv. mcpriority_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftM tcbMCP (getObject t) \<lbrace>\<lambda>rv. mcpriority_tcb_at' (\<lambda>st. st = rv) t and P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>(\<lambda>rv s. mcpriority_tcb_at' (\<lambda>st. st = rv) t s \<and> P s) \<circ> tcbMCP\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getObject t \<lbrace>\<lambda>x s. obj_at' (\<lambda>ko. tcbMCP ko = tcbMCP x) t s \<and> P s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> obj_at' (\<lambda>ko. tcbMCP ko = tcbMCP ta) t s \<and> P s) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma checkPrio_wp:
  "\<lbrace> \<lambda>s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> ucast mcp) auth s \<longrightarrow> P s \<rbrace>
    checkPrio prio auth
   \<lbrace> \<lambda>rv. P \<rbrace>,-" apply (simp add: checkPrio_def) apply (wp Nondet_VCG.whenE_throwError_wp getMCP_wp) by (auto simp add: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> P s\<rbrace> checkPrio prio auth \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> P s\<rbrace> doE mcp <- liftE (threadGet tcbMCP auth);
whenE (UCAST(8 \<rightarrow> 32) mcp < prio) (throwError (Fault_H.syscall_error.RangeError (UCAST(8 \<rightarrow> 32) minPriority) (UCAST(8 \<rightarrow> 32) mcp)))
odE \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<longrightarrow> P s \<Longrightarrow> \<forall>mcp. mcpriority_tcb_at' ((=) mcp) auth s \<longrightarrow> \<not> UCAST(8 \<rightarrow> 32) mcp < prio \<longrightarrow> P s
theory Tcb_R

lemma checkPrio_lt_ct:
  "\<lbrace>\<top>\<rbrace> checkPrio prio auth \<lbrace>\<lambda>rv s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> ucast mcp) auth s\<rbrace>, -" by (wp checkPrio_wp) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> checkPrio prio auth \<lbrace>\<lambda>rv. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth\<rbrace>, -
theory Tcb_R

lemma checkPrio_lt_ct_weak:
  "\<lbrace>\<top>\<rbrace> checkPrio prio auth \<lbrace>\<lambda>rv s. mcpriority_tcb_at' (\<lambda>mcp. ucast prio \<le> mcp) auth s\<rbrace>, -" apply (rule hoare_post_imp_R) apply (rule checkPrio_lt_ct) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) by (rule le_ucast_ucast_le) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> checkPrio prio auth \<lbrace>\<lambda>rv. mcpriority_tcb_at' ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> checkPrio prio auth \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> mcpriority_tcb_at' ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. mcpriority_tcb_at' (\<lambda>mcp. prio \<le> UCAST(8 \<rightarrow> 32) mcp) auth s \<Longrightarrow> mcpriority_tcb_at' ((\<le>) (UCAST(32 \<rightarrow> 8) prio)) auth s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj. \<lbrakk>ksPSpace s auth = Some ko; is_aligned auth (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; prio \<le> UCAST(8 \<rightarrow> 32) (tcbMCP obj); ps_clear auth (objBitsKO ko) s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) prio \<le> tcbMCP obj
theory Tcb_R

lemma decodeSetPriority_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t \<rbrace>
    decodeSetPriority args (ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>,-" unfolding decodeSetPriority_def apply (rule hoare_pre) apply (wp checkPrio_lt_ct_weak | wpc | simp | wp (once) checkPrio_inv)+ apply (clarsimp simp: maxPriority_def numPriorities_def) using max_word_max [of \<open>UCAST(32 \<rightarrow> 8) x\<close> for x] apply (simp add: max_word_mask numeral_eq_Suc mask_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeSetPriority args (capability.ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case (args, extras) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newPrio # xb, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newPrio # xb, (authCap, xa) # xba) \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap tcbPtr \<Rightarrow> returnOk tcbPtr | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr (capability.ThreadCap t)) 0 Nothing Nothing (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case (args, extras) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newPrio # xb, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newPrio # xb, (authCap, xa) # xba) \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap tcbPtr \<Rightarrow> returnOk tcbPtr | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr (capability.ThreadCap t)) 0 Nothing Nothing (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<Longrightarrow> \<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (\<forall>a. (\<exists>b x. extras = (a, b) # x) \<longrightarrow> (\<exists>x. a = capability.ThreadCap x) \<longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> maxPriority) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa b xb xc. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xa; extras = (capability.ThreadCap xc, b) # xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
using this:
UCAST(32 \<rightarrow> 8) ?x2 \<le> - 1

goal (1 subgoal):
 1. \<And>s x xa b xb xc. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xa; extras = (capability.ThreadCap xc, b) # xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeSetPriority_inv[wp]:
  "\<lbrace>P\<rbrace> decodeSetPriority args cap extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decodeSetPriority_def Let_def split del: if_split) apply (rule hoare_pre) apply (wp checkPrio_inv | simp add: whenE_def split del: if_split
             | rule hoare_drop_imps
             | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decodeSetPriority args cap extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newPrio # x \<Rightarrow> case extras of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap) 0 Nothing Nothing (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newPrio # x \<Rightarrow> case extras of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap) 0 Nothing Nothing (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeSetMCPriority_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t \<rbrace>
    decodeSetMCPriority args (ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>,-" unfolding decodeSetMCPriority_def Let_def apply (rule hoare_pre) apply (wp checkPrio_lt_ct_weak | wpc | simp | wp (once) checkPrio_inv)+ apply (clarsimp simp: maxPriority_def numPriorities_def) using max_word_max [of \<open>UCAST(32 \<rightarrow> 8) x\<close> for x] apply (simp add: max_word_mask numeral_eq_Suc mask_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeSetMCPriority args (capability.ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case (args, extras) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # xb, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # xb, (authCap, xa) # xba) \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap tcbPtr \<Rightarrow> returnOk tcbPtr | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr (capability.ThreadCap t)) 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) Nothing Nothing Nothing Nothing
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case (args, extras) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # xb, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # xb, (authCap, xa) # xba) \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap tcbPtr \<Rightarrow> returnOk tcbPtr | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr (capability.ThreadCap t)) 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) Nothing Nothing Nothing Nothing
odE \<lbrace>tcb_inv_wf'\<rbrace>, -
 2. \<And>s. (invs' and tcb_at' t and ex_nonz_cap_to' t) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<Longrightarrow> \<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (\<forall>a. (\<exists>b x. extras = (a, b) # x) \<longrightarrow> (\<exists>x. a = capability.ThreadCap x) \<longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> maxPriority) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa b xb xc. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xa; extras = (capability.ThreadCap xc, b) # xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
using this:
UCAST(32 \<rightarrow> 8) ?x2 \<le> - 1

goal (1 subgoal):
 1. \<And>s x xa b xb xc. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xa; extras = (capability.ThreadCap xc, b) # xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeSetMCPriority_inv[wp]:
  "\<lbrace>P\<rbrace> decodeSetMCPriority args cap extras \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decodeSetMCPriority_def Let_def split del: if_split) apply (rule hoare_pre) apply (wp checkPrio_inv | simp add: whenE_def split del: if_split
             | rule hoare_drop_imps
             | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decodeSetMCPriority args cap extras \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # x \<Rightarrow> case extras of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap) 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) Nothing Nothing Nothing Nothing
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | newMCP # x \<Rightarrow> case extras of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (authCap, xa) # xb \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap x \<Rightarrow> returnOk x | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr cap) 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) Nothing Nothing Nothing Nothing
odE \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeSetSchedParams_wf[wp]:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t \<rbrace>
    decodeSetSchedParams args (ThreadCap t) extras
   \<lbrace>tcb_inv_wf'\<rbrace>,-" unfolding decodeSetSchedParams_def apply (wpsimp wp: checkPrio_lt_ct_weak | wp (once) checkPrio_inv)+ apply (clarsimp simp: maxPriority_def numPriorities_def) using max_word_max [of \<open>UCAST(32 \<rightarrow> 8) x\<close> for x] apply (simp add: max_word_mask numeral_eq_Suc mask_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeSetSchedParams args (capability.ThreadCap t) extras \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case (args, extras) of ([], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | ([newMCP], xa) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # newPrio # x, []) \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | (newMCP # newPrio # x, (authCap, xa) # xb) \<Rightarrow> doE authTCB <- case authCap of capability.ThreadCap tcbPtr \<Rightarrow> returnOk tcbPtr | _ \<Rightarrow> throw $ Fault_H.syscall_error.InvalidCapability 1;
checkPrio newMCP authTCB;
checkPrio newPrio authTCB;
returnOk $ tcbinvocation.ThreadControl (capTCBPtr (capability.ThreadCap t)) 0 Nothing (Just $ (fromIntegral newMCP, authTCB)) (Just $ (fromIntegral newPrio, authTCB)) Nothing Nothing Nothing
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xc b xd xe. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xb # xc; extras = (capability.ThreadCap xe, b) # xd\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) xb \<le> maxPriority \<and> UCAST(32 \<rightarrow> 8) x \<le> maxPriority proof (prove)
goal (1 subgoal):
 1. \<And>s x xb xc b xd xe. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xb # xc; extras = (capability.ThreadCap xe, b) # xd\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) xb \<le> 0xFF \<and> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
using this:
UCAST(32 \<rightarrow> 8) ?x2 \<le> - 1

goal (1 subgoal):
 1. \<And>s x xb xc b xd xe. \<lbrakk>invs' s; tcb_at' t s; ex_nonz_cap_to' t s; args = x # xb # xc; extras = (capability.ThreadCap xe, b) # xd\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) xb \<le> 0xFF \<and> UCAST(32 \<rightarrow> 8) x \<le> 0xFF proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma checkValidIPCBuffer_corres:
  "cap_relation cap cap' \<Longrightarrow>
   corres (ser \<oplus> dc) \<top> \<top>
     (check_valid_ipc_buffer vptr cap)
     (checkValidIPCBuffer vptr cap')" apply (simp add: check_valid_ipc_buffer_def
                   checkValidIPCBuffer_def
                   ARM_H.checkValidIPCBuffer_def
                   unlessE_def Let_def
            split: cap_relation_split_asm arch_cap.split_asm bool.splits) apply (simp add: capTransferDataSize_def msgMaxLength_def
                   msg_max_length_def msgMaxExtraCaps_def
                   cap_transfer_data_size_def word_size
                   msgLengthBits_def msgExtraCapBits_def msg_align_bits msgAlignBits_def
                   msg_max_extra_caps_def is_aligned_mask whenE_def split:vmpage_size.splits) apply (auto simp add: returnOk_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (check_valid_ipc_buffer vptr cap) (checkValidIPCBuffer vptr cap') proof (prove)
goal (1 subgoal):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); x12 = arch_cap.PageCap x31 x32 x33 x34 x35; cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)\<rbrakk> \<Longrightarrow> \<not> x31 \<longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (whenE (\<not> is_aligned vptr msg_align_bits) (throwError ExceptionTypes_A.syscall_error.AlignmentError)) (whenE (vptr && mask msgAlignBits \<noteq> 0) (throwError Fault_H.syscall_error.AlignmentError)) proof (prove)
goal (1 subgoal):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = cap.ArchObjectCap (arch_cap.PageCap x31 x32 x33 x34 x35); x12 = arch_cap.PageCap x31 x32 x33 x34 x35; cap' = capability.ArchObjectCap (arch_capability.PageCap x31 x32 (vmrights_map x33) x34 x35)\<rbrakk> \<Longrightarrow> vptr && mask 9 = 0 \<longrightarrow> \<not> x31 \<longrightarrow> corres (ser \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (returnOk ()) (returnOk ()) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma checkValidIPCBuffer_ArchObject_wp:
  "\<lbrace>\<lambda>s. isArchObjectCap cap \<and> is_aligned x msg_align_bits \<longrightarrow> P s\<rbrace>
     checkValidIPCBuffer x cap
   \<lbrace>\<lambda>rv s. P s\<rbrace>,-" apply (simp add: checkValidIPCBuffer_def
                   ARM_H.checkValidIPCBuffer_def
                   whenE_def unlessE_def
             cong: capability.case_cong
                   arch_capability.case_cong
            split del: if_split) apply (rule hoare_pre) apply (wp whenE_throwError_wp
    | wpc | clarsimp simp: isCap_simps is_aligned_mask msg_align_bits msgAlignBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isArchObjectCap cap \<and> is_aligned x msg_align_bits \<longrightarrow> P s\<rbrace> checkValidIPCBuffer x cap \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. isArchObjectCap cap \<and> is_aligned x msg_align_bits \<longrightarrow> P s\<rbrace> case cap of capability.ArchObjectCap (arch_capability.PageCap True xa xaa xb xc) \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | capability.ArchObjectCap (arch_capability.PageCap False xa xaa xb xc) \<Rightarrow> doE whenE (x && mask msgAlignBits \<noteq> 0) $ throw Fault_H.syscall_error.AlignmentError;
returnOk ()
odE | capability.ArchObjectCap _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'14\<rbrace> case cap of capability.ArchObjectCap (arch_capability.PageCap True xa xaa xb xc) \<Rightarrow> throw Fault_H.syscall_error.IllegalOperation | capability.ArchObjectCap (arch_capability.PageCap False xa xaa xb xc) \<Rightarrow> doE whenE (x && mask msgAlignBits \<noteq> 0) $ throw Fault_H.syscall_error.AlignmentError;
returnOk ()
odE | capability.ArchObjectCap _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | _ \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>, -
 2. \<And>s. isArchObjectCap cap \<and> is_aligned x msg_align_bits \<longrightarrow> P s \<Longrightarrow> ?P'14 s proof (prove)
goal:
No subgoals!