theory Orphanage

lemma tc_no_orphans:
  "\<lbrace> no_orphans and invs' and sch_act_simple 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 (case_option True isArchObjectCap (case_option None (case_option None (Some o fst) o snd) g)) and
    K (case_option True (swp is_aligned 2 o fst) g) and
    K (case_option True (swp is_aligned msg_align_bits o fst) g) and
    K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x) and
    K (valid_option_prio d \<and> valid_option_prio mcp) \<rbrace>
      invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g)
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_gen_asm) apply (rule hoare_gen_asm) apply (simp add: invokeTCB_def getThreadCSpaceRoot getThreadVSpaceRoot
                   getThreadBufferSlot_def split_def) 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_no_orphans threadSet_invs_trivial
               threadSet_cap_to' hoare_vcg_all_lift hoare_weak_lift_imp | clarsimp simp: inQ_def)+)[2] apply (rule hoare_walk_assmsE) apply (cases mcp; clarsimp simp: pred_conj_def option.splits[where P="\<lambda>x. x s" for s]) apply ((wp case_option_wp threadSet_no_orphans threadSet_invs_trivial setMCPriority_invs'
                typ_at_lifts[OF setMCPriority_typ_at']
                threadSet_cap_to' hoare_vcg_all_lift hoare_weak_lift_imp | clarsimp simp: inQ_def)+)[3] apply ((simp only: simp_thms cong: conj_cong
          | wp cteDelete_deletes cteDelete_invs' cteDelete_sch_act_simple
               case_option_wp[where m'="return ()", OF setPriority_no_orphans return_inv,simplified]
               checkCap_inv[where P="valid_cap' c" for c] checkCap_inv[where P=sch_act_simple]
               checkCap_inv[where P=no_orphans] checkCap_inv[where P="tcb_at' a"]
               threadSet_cte_wp_at' hoare_vcg_all_lift_R hoare_vcg_all_lift threadSet_no_orphans
               hoare_vcg_const_imp_lift_R hoare_weak_lift_imp hoare_drop_imp threadSet_ipcbuffer_invs
          | strengthen invs_valid_queues'
          | (simp add: locateSlotTCB_def locateSlotBasic_def objBits_def
                     objBitsKO_def tcbIPCBufferSlot_def tcb_cte_cases_def,
           wp hoare_return_sp)
          | wpc | clarsimp)+) apply (fastforce simp: objBits_defs isCap_simps dest!: isValidVTableRootD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans and invs' and sch_act_simple 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 (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 2 \<circ> fst) x) and K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x) and K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x) and K (valid_option_prio d \<and> valid_option_prio mcp)\<rbrace> invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_option_prio d \<and> valid_option_prio mcp \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 (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 2 \<circ> fst) x) and K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x) and K (case g of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x)\<rbrace> invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_option_prio d \<and> valid_option_prio mcp; case g of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 (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 2 \<circ> fst) 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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_option_prio d \<and> valid_option_prio mcp; case g of None \<Rightarrow> True | Some x \<Rightarrow> (case_option True (isArchObjectCap \<circ> fst) \<circ> snd) x; case g of None \<Rightarrow> True | Some x \<Rightarrow> (swp is_aligned msg_align_bits \<circ> fst) x\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 (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 2 \<circ> fst) x)\<rbrace> invokeTCB (tcbinvocation.ThreadControl a sl b' mcp d e' f' g) \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace> liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a) \<lbrace>\<lambda>rv. no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace>
 2. \<And>s. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)) s\<rbrakk> \<Longrightarrow> no_orphans s
 3. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; 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\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace> liftE (case b' of None \<Rightarrow> return () | Some ep \<Rightarrow> threadSet (tcbFaultHandler_update (\<lambda>_. ep)) a) \<lbrace>\<lambda>rv x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace>
 2. \<And>s. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)) s\<rbrakk> \<Longrightarrow> no_orphans s
 3. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace> liftE (case mcp of None \<Rightarrow> return () | Some x2 \<Rightarrow> setMCPriority a (fst x2)) \<lbrace>\<lambda>rv. no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace>
 2. \<And>s. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)) s\<rbrakk> \<Longrightarrow> no_orphans s
 3. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; mcp = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace> liftE (return ()) \<lbrace>\<lambda>rv x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace>
 2. \<And>aa b. \<lbrakk>case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; mcp = Some (aa, b); case d of None \<Rightarrow> True | Some x2 \<Rightarrow> fst x2 \<le> maxPriority; aa \<le> maxPriority\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace> liftE (setMCPriority a aa) \<lbrace>\<lambda>rv x. no_orphans x \<and> invs' x \<and> sch_act_simple 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 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) \<and> (case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<rbrace>
 3. \<And>s. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; (no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)) s\<rbrakk> \<Longrightarrow> no_orphans s
 4. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(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); case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits\<rbrakk> \<Longrightarrow> \<lbrace>no_orphans and invs' and sch_act_simple 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 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) and (\<lambda>y. case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2)\<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 (locateSlotTCB a 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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case g of None \<Rightarrow> True | Some x \<Rightarrow> case snd x of None \<Rightarrow> True | Some x2 \<Rightarrow> isArchObjectCap (fst x2); case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) msg_align_bits; 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; no_orphans s; invs' s; sch_act_simple 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 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; case g of None \<Rightarrow> True | Some x2 \<Rightarrow> is_aligned (fst x2) 2\<rbrakk> \<Longrightarrow> (e' = None \<longrightarrow> (f' = None \<longrightarrow> (\<forall>a b. g = Some (a, b) \<longrightarrow> (d = None \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)))) \<and> (\<forall>a. (\<exists>b. f' = Some (a, b)) \<longrightarrow> (g = None \<longrightarrow> (\<exists>a b. d = 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 b. g = Some (aa, 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> (d = None \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a))))) \<and> (\<forall>aa. (\<exists>b. e' = Some (aa, b)) \<longrightarrow> (f' = None \<longrightarrow> (g = None \<longrightarrow> (\<exists>a b. d = 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 b. g = 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> (d = None \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)))) \<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> (g = None \<longrightarrow> (\<exists>a b. d = 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) \<and> (\<forall>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 \<and> (d = None \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a)) \<and> ((\<exists>a b. d = Some (a, b)) \<longrightarrow> (\<forall>a. (\<exists>ba. b = Some (a, ba)) \<longrightarrow> valid_cap' a s \<and> capBadge a = None \<and> (2 ^ cteSizeBits * 4 = 0x40 \<or> 2 ^ cteSizeBits * 4 = 0x30 \<or> 2 ^ cteSizeBits * 4 = 0x20 \<or> 2 ^ cteSizeBits * 4 = 0x10 \<or> 2 ^ cteSizeBits * 4 = 0) \<and> \<not> isReplyCap a \<and> \<not> isIRQControlCap a))))) proof (prove)
goal:
No subgoals!