theory Tcb_R

lemma tc_invs':
  "\<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and
    K (valid_option_prio d \<and> valid_option_prio mcp) and
    case_option \<top> (valid_cap' o fst) e' and
    K (case_option True (isCNodeCap o fst) e') and
    case_option \<top> (valid_cap' o fst) f' and
    K (case_option True (isValidVTableRoot o fst) f') and
    case_option \<top> (valid_cap') (case_option None (case_option None (Some o fst) o snd) g) and
    K (case_option True isArchObjectCap (case_option None (case_option None (Some o fst) o snd) g))
    and K (case_option True (swp is_aligned msg_align_bits o fst) g) \<rbrace>
      invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g)
   \<lbrace>\<lambda>rv. invs'\<rbrace>" (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") apply (rule hoare_gen_asm) apply (simp add: split_def invokeTCB_def getThreadCSpaceRoot getThreadVSpaceRoot
                   getThreadBufferSlot_def locateSlot_conv
             cong: option.case_cong) apply (simp only: eq_commute[where a="a"]) apply (rule hoare_walk_assmsE) apply (clarsimp simp: pred_conj_def option.splits [where P="\<lambda>x. x s" for s]) apply ((wp case_option_wp threadSet_invs_trivial hoare_weak_lift_imp
               hoare_vcg_all_lift threadSet_cap_to' | clarsimp simp: inQ_def)+)[2] apply (rule hoare_walk_assmsE) apply (clarsimp simp: pred_conj_def option.splits [where P="\<lambda>x. x s" for s]) apply ((wp case_option_wp threadSet_invs_trivial hoare_weak_lift_imp setMCPriority_invs'
               typ_at_lifts[OF setMCPriority_typ_at']
               hoare_vcg_all_lift threadSet_cap_to' | clarsimp simp: inQ_def)+)[2] apply (wp add: setP_invs' hoare_weak_lift_imp hoare_vcg_all_lift)+ apply (rule case_option_wp_None_return[OF setP_invs'[simplified pred_conj_assoc]]) apply clarsimp apply wpfix apply assumption apply (rule case_option_wp_None_returnOk) apply (wpsimp wp: hoare_weak_lift_imp hoare_vcg_all_lift
                        checkCap_inv[where P="tcb_at' t" for t] assertDerived_wp_weak
                        threadSet_invs_trivial2 threadSet_tcb'  hoare_vcg_all_lift threadSet_cte_wp_at')+ apply (wpsimp wp: hoare_weak_lift_imp_R cteDelete_deletes
                         hoare_vcg_all_lift_R hoare_vcg_conj_liftE1 hoare_vcg_const_imp_lift_R hoare_vcg_propE_R
                         cteDelete_invs' cteDelete_invs' cteDelete_typ_at'_lifts)+ apply (assumption | clarsimp cong: conj_cong imp_cong | (rule case_option_wp_None_returnOk)
            | wpsimp wp: hoare_weak_lift_imp hoare_vcg_all_lift checkCap_inv[where P="tcb_at' t" for t] assertDerived_wp_weak
                         hoare_vcg_imp_lift' hoare_vcg_all_lift checkCap_inv[where P="tcb_at' t" for t]
                         checkCap_inv[where P="valid_cap' c" for c] checkCap_inv[where P=sch_act_simple]
                         hoare_vcg_const_imp_lift_R assertDerived_wp_weak hoare_weak_lift_imp_R cteDelete_deletes
                         hoare_vcg_all_lift_R hoare_vcg_conj_liftE1 hoare_vcg_const_imp_lift_R hoare_vcg_propE_R
                         cteDelete_invs' cteDelete_typ_at'_lifts cteDelete_sch_act_simple)+ apply (clarsimp simp: tcb_cte_cases_def cte_level_bits_def objBits_defs tcbIPCBufferSlot_def) by (auto dest!: isCapDs isReplyCapD isValidVTableRootD simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and K (valid_option_prio d \<and> valid_option_prio mcp) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case e' of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case f' of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and (case case g of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_cap' x) and K (case case g of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> True | Some x \<Rightarrow> isArchObjectCap x) and K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x)\<rbrace> invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. case g of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and K (valid_option_prio d \<and> valid_option_prio mcp) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case e' of None \<Rightarrow> True | Some x \<Rightarrow> (isCNodeCap \<circ> fst) x) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> (valid_cap' \<circ> fst) x) and K (case f' of None \<Rightarrow> True | Some x \<Rightarrow> (isValidVTableRoot \<circ> fst) x) and (case case g of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_cap' x) and K (case case g of None \<Rightarrow> None | Some x \<Rightarrow> (case_option None (Some \<circ> fst) \<circ> snd) x of None \<Rightarrow> True | Some x \<Rightarrow> isArchObjectCap x)\<rbrace> invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2));
y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (a = thread) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a);
y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2));
y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a) \<lbrace>\<lambda>rv. invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace>
 2. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> invs' s
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2));
y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>\<lambda>x. invs' x \<and> sch_act_simple x \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<and> (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (\<forall>a. (\<exists>b. e' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (\<forall>x2. (case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) = Some x2 \<longrightarrow> valid_cap' x2 x) \<and> (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a) \<lbrace>\<lambda>rv x. invs' x \<and> sch_act_simple x \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<and> (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (\<forall>a. (\<exists>b. e' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (\<forall>x2. (case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) = Some x2 \<longrightarrow> valid_cap' x2 x) \<and> (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace>
 2. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> invs' s
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2));
y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2));
y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2)) \<lbrace>\<lambda>rv. invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace>
 2. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> invs' s
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>\<lambda>x. invs' x \<and> sch_act_simple x \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<and> (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (\<forall>a. (\<exists>b. e' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (\<forall>x2. (case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) = Some x2 \<longrightarrow> valid_cap' x2 x) \<and> (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2)) \<lbrace>\<lambda>rv x. invs' x \<and> sch_act_simple x \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<and> (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (\<forall>a. (\<exists>b. e' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) \<and> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> valid_cap' a x) \<and> (case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) \<and> (\<forall>x2. (case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) = Some x2 \<longrightarrow> valid_cap' x2 x) \<and> (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace>
 2. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> invs' s
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)\<rbrace> doE y <- case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE;
y <- case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE;
y <- liftE (case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2));
returnOk []
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B184 y ya yb\<rbrace> case d of None \<Rightarrow> return () | Some x2 \<Rightarrow> setPriority a (fst x2) \<lbrace>\<lambda>yc. invs'\<rbrace>
 2. \<And>y ya. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B183 y ya\<rbrace> case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>?B184 y ya\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B183 y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (5 subgoals):
 1. \<And>y ya yb x2 s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and ?P188 y ya yb x2) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' a and K (fst x2 \<le> maxPriority)) s
 2. \<And>y ya. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B183 y ya\<rbrace> case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>\<lambda>yb. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> ?P188 y ya yb (the d) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B183 y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (5 subgoals):
 1. \<And>aa b s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; invs' s; ?P188 () () () (aa, b) s\<rbrakk> \<Longrightarrow> tcb_at' a s \<and> aa \<le> maxPriority
 2. \<And>y ya. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B183 y ya\<rbrace> case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>\<lambda>yb. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> ?P188 y ya yb (the d) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B183 y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (5 subgoals):
 1. \<And>aa b s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; invs' s; ?P196 aa b () () () (aa, b) s\<rbrakk> \<Longrightarrow> tcb_at' a s \<and> aa \<le> maxPriority
 2. \<And>y ya. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B183 y ya\<rbrace> case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>\<lambda>yb. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> ?P196 (fst (the d)) (snd (the d)) y ya yb (the d) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B183 y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (4 subgoals):
 1. \<And>y ya. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B183 y ya\<rbrace> case g of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>\<lambda>yb. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B183 y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (5 subgoals):
 1. \<And>y ya p. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?P'197 y ya p\<rbrace> doE bufferSlot <- liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot));
y <- cteDelete bufferSlot True;
y <- liftE (threadSet (tcbIPCBuffer_update (\<lambda>_. fst p)) a);
y <- liftE (case snd p of None \<Rightarrow> return () | Some x2 \<Rightarrow> checkCapAt (fst x2) (snd x2) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd x2) (fst x2) (cteInsert (fst x2) (snd x2) bufferSlot))));
thread <- liftE getCurThread;
liftE (when (thread = a) rescheduleRequired)
odE \<lbrace>\<lambda>yb. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>y ya p s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority) and ?P197 y ya p) s\<rbrakk> \<Longrightarrow> ?P'197 y ya p s
 3. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>\<lambda>ya. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority) and (\<lambda>s. g \<noteq> None \<longrightarrow> ?P197 y ya (the g) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (6 subgoals):
 1. \<And>aa b bufferSlot. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B325 aa b () () (aa, b) bufferSlot\<rbrace> cteDelete bufferSlot True \<lbrace>\<lambda>yb s. (b = None \<longrightarrow> invs' s \<and> is_aligned aa msg_align_bits \<and> tcb_at' a s \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority)) \<and> (\<forall>ab. (\<exists>ba. b = Some (ab, ba)) \<longrightarrow> invs' s \<and> is_aligned aa msg_align_bits \<and> tcb_at' a s \<and> cte_wp_at' (\<lambda>a. cteCap a = capability.NullCap) bufferSlot s \<and> valid_cap' ab s \<and> capBadge ab = None \<and> bufferSlot \<in> (+) a ` dom tcb_cte_cases \<and> \<not> isReplyCap ab \<and> \<not> isIRQControlCap ab \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority))\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>y ya p. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?P'197 y ya p\<rbrace> liftE (return (a + 2 ^ cte_level_bits * tcbIPCBufferSlot)) \<lbrace>?B325 (fst p) (snd p) y ya p\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>y ya p s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority) and ?P197 y ya p) s\<rbrakk> \<Longrightarrow> ?P'197 y ya p s
 4. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>\<lambda>ya. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority) and (\<lambda>s. g \<noteq> None \<longrightarrow> ?P197 y ya (the g) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (4 subgoals):
 1. \<And>aa b s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; invs' s; (\<exists>a b. d = Some (a, b)) \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority; ?P471 aa b () () (aa, b) s\<rbrakk> \<Longrightarrow> (b = None \<longrightarrow> sch_act_simple s \<and> is_aligned aa msg_align_bits \<and> tcb_at' a s) \<and> sch_act_simple s \<and> (\<forall>x. (\<exists>ba. b = Some (x, ba)) \<longrightarrow> sch_act_simple s \<and> is_aligned aa msg_align_bits \<and> tcb_at' a s \<and> valid_cap' x s \<and> capBadge x = None \<and> 2 ^ cte_level_bits * tcbIPCBufferSlot \<in> dom tcb_cte_cases \<and> \<not> isReplyCap x \<and> \<not> isIRQControlCap x)
 2. \<And>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?B182 y\<rbrace> case f' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return (a + 2 ^ cteSizeBits));
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>\<lambda>ya. invs' and (\<lambda>s. d \<noteq> None \<longrightarrow> tcb_at' a s \<and> fst (the d) \<le> maxPriority) and (\<lambda>s. g \<noteq> None \<longrightarrow> ?P471 (fst (the g)) (snd (the g)) y ya (the g) s)\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits \<Longrightarrow> \<lbrace>?Q180\<rbrace> case e' of None \<Rightarrow> returnOk () | Some p \<Rightarrow> doE rootSlot <- liftE (return a);
y <- cteDelete rootSlot True;
liftE (checkCapAt (fst p) (snd p) (checkCapAt (capability.ThreadCap a) sl (assertDerived (snd p) (fst p) (cteInsert (fst p) (snd p) rootSlot))))
odE \<lbrace>?B182\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (invs' and sch_act_simple and tcb_at' a and ex_nonz_cap_to' a and (\<lambda>y. (case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) \<and> (case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority)) and (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2)) and (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) and (\<lambda>y. case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2)) and (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) and (\<lambda>y. case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2)) s\<rbrakk> \<Longrightarrow> ?Q180 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; invs' s; sch_act_simple s; tcb_at' a s; ex_nonz_cap_to' a s; case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2); (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2); (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) s; case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2\<rbrakk> \<Longrightarrow> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> fst (the d) \<le> maxPriority) \<and> ((\<exists>a b. g = Some (a, b)) \<longrightarrow> (snd (the g) = None \<longrightarrow> is_aligned (fst (the g)) msg_align_bits) \<and> (\<forall>x. (\<exists>b. snd (the g) = Some (x, b)) \<longrightarrow> is_aligned (fst (the g)) msg_align_bits \<and> valid_cap' x s \<and> capBadge x = None \<and> 2 ^ cte_level_bits * tcbIPCBufferSlot \<in> dom tcb_cte_cases \<and> \<not> isReplyCap x \<and> \<not> isIRQControlCap x)) \<and> ((\<exists>a b. f' = Some (a, b)) \<longrightarrow> valid_cap' (fst (the f')) s \<and> capBadge (fst (the f')) = None \<and> 2 ^ cteSizeBits \<in> dom tcb_cte_cases \<and> \<not> isReplyCap (fst (the f')) \<and> \<not> isIRQControlCap (fst (the f'))) \<and> ((\<exists>a b. e' = Some (a, b)) \<longrightarrow> valid_cap' (fst (the e')) s \<and> capBadge (fst (the e')) = None \<and> a \<in> (+) a ` dom tcb_cte_cases \<and> \<not> isReplyCap (fst (the e')) \<and> \<not> isIRQControlCap (fst (the e'))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; invs' s; sch_act_simple s; tcb_at' a s; ex_nonz_cap_to' a s; case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case e' of None \<Rightarrow> True | Some x2 \<Rightarrow> isCNodeCap (fst x2); (case f' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s; case f' of None \<Rightarrow> True | Some x2 \<Rightarrow> isValidVTableRoot (fst x2); (case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' x2) s; case case g of None \<Rightarrow> None | Some x2 \<Rightarrow> case snd x2 of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2) of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap x2\<rbrakk> \<Longrightarrow> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> fst (the d) \<le> maxPriority) \<and> ((\<exists>a b. g = Some (a, b)) \<longrightarrow> (snd (the g) = None \<longrightarrow> is_aligned (fst (the g)) msg_align_bits) \<and> (\<forall>x. (\<exists>b. snd (the g) = Some (x, b)) \<longrightarrow> is_aligned (fst (the g)) msg_align_bits \<and> valid_cap' x s \<and> capBadge x = None \<and> \<not> isReplyCap x \<and> \<not> isIRQControlCap x)) \<and> ((\<exists>a b. f' = Some (a, b)) \<longrightarrow> valid_cap' (fst (the f')) s \<and> capBadge (fst (the f')) = None \<and> \<not> isReplyCap (fst (the f')) \<and> \<not> isIRQControlCap (fst (the f'))) \<and> ((\<exists>a b. e' = Some (a, b)) \<longrightarrow> valid_cap' (fst (the e')) s \<and> capBadge (fst (the e')) = None \<and> \<not> isReplyCap (fst (the e')) \<and> \<not> isIRQControlCap (fst (the e')))