theory PageTableDuplicates

lemma tc_valid_duplicates':
  "\<lbrace>invs' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 (valid_option_prio d) and
    K (valid_option_prio mcp) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 ((simp only: simp_thms cases_simp cong: conj_cong
          | (wp cteDelete_deletes cteDelete_invs' cteDelete_sch_act_simple
              threadSet_ipcbuffer_trivial
              (* setPriority has no effect on vs_duplicates *)
              case_option_wp[where m'="return ()", OF setPriority_valid_duplicates' return_inv,simplified]
              checkCap_inv[where P="tcb_at' t" for t]
              checkCap_inv[where P="valid_cap' c" for c]
              checkCap_inv[where P="\<lambda>s. P (ksReadyQueues s)" for P]
              checkCap_inv[where P="\<lambda>s. vs_valid_duplicates' (ksPSpace s)"]
              checkCap_inv[where P=sch_act_simple] cteDelete_valid_duplicates' hoare_vcg_const_imp_lift_R
              typ_at_lifts[OF setPriority_typ_at'] assertDerived_wp threadSet_cte_wp_at'
              hoare_vcg_all_lift_R hoare_vcg_all_lift hoare_weak_lift_imp)[1]
          | wpc
          | simp add: inQ_def
          | wp hoare_vcg_conj_liftE1 cteDelete_invs' cteDelete_deletes hoare_vcg_const_imp_lift)+) 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 (valid_option_prio d) and K (valid_option_prio mcp) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 (valid_option_prio d) and K (valid_option_prio mcp) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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> vs_valid_duplicates' (ksPSpace 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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> vs_valid_duplicates' (ksPSpace x) \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<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 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 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> vs_valid_duplicates' (ksPSpace x) \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<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 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 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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> vs_valid_duplicates' (ksPSpace 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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> vs_valid_duplicates' (ksPSpace 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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> vs_valid_duplicates' (ksPSpace x) \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<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 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 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> vs_valid_duplicates' (ksPSpace x) \<and> tcb_at' a x \<and> ex_nonz_cap_to' a x \<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 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 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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> vs_valid_duplicates' (ksPSpace 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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<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 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and tcb_at' a and ex_nonz_cap_to' a 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 d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) and (\<lambda>y. case mcp of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority) 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 s. vs_valid_duplicates' (ksPSpace s)\<rbrace> 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 \<and> sch_act_simple s \<and> vs_valid_duplicates' (ksPSpace s) \<and> tcb_at' a s \<and> ex_nonz_cap_to' a s \<and> (case e' of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_cap' (fst x2)) s \<and> (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)) s \<and> (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) s \<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> (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> (e' = None \<longrightarrow> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> (\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> 2 ^ cteSizeBits \<in> dom tcb_cte_cases \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> (\<forall>aa. (\<exists>b. e' = Some (aa, b)) \<longrightarrow> (f' = None \<longrightarrow> (\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' aa s \<and> capBadge aa = None \<and> a \<in> (+) a ` dom tcb_cte_cases \<and> \<not> isReplyCap aa \<and> \<not> isIRQControlCap aa) \<and> (\<forall>ab. (\<exists>b. f' = Some (ab, b)) \<longrightarrow> valid_cap' aa s \<and> capBadge aa = None \<and> a \<in> (+) a ` dom tcb_cte_cases \<and> \<not> isReplyCap aa \<and> \<not> isIRQControlCap aa \<and> ((\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' ab s \<and> capBadge ab = None \<and> 2 ^ cteSizeBits \<in> dom tcb_cte_cases \<and> \<not> isReplyCap ab \<and> \<not> isIRQControlCap ab))) 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; vs_valid_duplicates' (ksPSpace s); tcb_at' a s; ex_nonz_cap_to' a s; (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 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 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> (e' = None \<longrightarrow> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> (\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> (\<forall>a. (\<exists>b. e' = Some (a, b)) \<longrightarrow> (f' = None \<longrightarrow> (\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a) \<and> (\<forall>aa. (\<exists>b. f' = Some (aa, b)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a \<and> ((\<exists>a b. g = Some (a, b)) \<longrightarrow> valid_cap' aa s \<and> capBadge aa = None \<and> \<not> isReplyCap aa \<and> \<not> isIRQControlCap aa)))