theory CNodeInv_AI

lemma invoke_cnode_invs[wp]:
  fixes i shows
  "\<lbrace>invs and valid_cnode_inv i\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv. invs::'state_ext state \<Rightarrow> bool\<rbrace>" unfolding invoke_cnode_def apply (cases i) apply simp apply wp apply (simp add: ex_cte_cap_to_cnode_always_appropriate_strg
                         real_cte_tcb_valid) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state dest!: cap_irqs_is_derived) apply (rule conjI) apply (elim conjE) apply (drule real_cte_is_derived_not_replyD) apply (simp add:invs_valid_objs invs_valid_reply_masters)+ apply (clarsimp simp:is_cap_simps) apply (elim conjE) apply (drule real_cte_not_reply_masterD) apply (simp add:invs_valid_objs invs_valid_reply_masters)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def) apply simp apply wp apply (fastforce simp: real_cte_tcb_valid cte_wp_at_caps_of_state
                             ex_cte_cap_to_cnode_always_appropriate_strg
                       dest: real_cte_weak_derived_not_reply_masterD) apply simp apply (wp cap_revoke_invs) apply simp apply simp apply wp apply (clarsimp simp: emptyable_def obj_at_def is_tcb is_cap_table) apply simp apply (rule conjI) apply (rule impI) apply wp apply (fastforce simp: real_cte_tcb_valid
                           ex_cte_cap_to_cnode_always_appropriate_strg
                     dest: real_cte_weak_derived_not_reply_masterD) apply (rule impI) apply (rule hoare_pre) apply wp apply (simp add: cte_wp_at_caps_of_state) apply (wp cap_move_caps_of_state cap_move_ex_cap_cte) apply (simp add: pred_conj_def) apply (elim conjE exE) apply (simp add: real_cte_tcb_valid ex_cte_cap_to_cnode_always_appropriate_strg
                     cap_irqs_appropriateness [OF weak_derived_cap_irqs]) apply (intro conjI,
          (fastforce simp: cte_wp_at_caps_of_state
                    dest: real_cte_weak_derived_not_reply_masterD)+)[1] apply (wpsimp wp: hoare_drop_imps get_cap_wp)+ apply (rule conjI) apply (clarsimp elim!: cte_wp_valid_cap) apply (clarsimp simp: real_cte_tcb_valid cte_wp_at_caps_of_state
                         is_cap_simps ex_cte_cap_to_cnode_always_appropriate_strg) apply (wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cnode_inv i\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. i = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. i = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>invs and (valid_cap x11 and real_cte_at x12 and real_cte_at x13 and (\<lambda>s. cte_wp_at (is_derived (cdt s) x12 x11) x12 s) and cte_wp_at (\<lambda>c. c = NullCap) x13 and ex_cte_cap_wp_to is_cnode_cap x13 and (\<lambda>y. x12 \<noteq> x13) and (\<lambda>s. \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11))\<rbrace> liftE (cap_insert x11 x12 x13) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; (invs and (valid_cap x11 and real_cte_at x12 and real_cte_at x13 and (\<lambda>s. cte_wp_at (is_derived (cdt s) x12 x11) x12 s) and cte_wp_at (\<lambda>c. c = NullCap) x13 and ex_cte_cap_wp_to is_cnode_cap x13 and (\<lambda>y. x12 \<noteq> x13) and (\<lambda>s. \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11))) s\<rbrakk> \<Longrightarrow> (invs and cte_wp_at (\<lambda>c. c = NullCap) x13 and valid_cap x11 and tcb_cap_valid x11 x13 and ex_cte_cap_wp_to (appropriate_cte_cap x11) x13 and (\<lambda>s. \<forall>r\<in>obj_refs x11. \<forall>p'. x13 \<noteq> p' \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') p' s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) p' s \<and> \<not> is_zombie x11) and (\<lambda>s. cte_wp_at (is_derived (cdt s) x12 x11) x12 s) and (\<lambda>s. cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs x11 - cap_irqs cap'. irq_issued irq s) x12 s) and (\<lambda>s. \<forall>t R. x11 = ReplyCap t False R \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) and K (\<not> is_master_reply_cap x11)) s
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs x11 - cap_irqs cap'. irq_issued irq s) x12 s \<and> (\<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap x11
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs x11 - cap_irqs cap'. irq_issued irq s) x12 s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap x11
 3. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> (\<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s) \<and> \<not> is_master_reply_cap x11
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 3. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 3. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> real_cte_at x12 s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> valid_reply_masters s
 3. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11; \<not> is_reply_cap x11\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 5. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 6. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 9. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 10. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
A total of 11 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11; \<not> is_reply_cap x11\<rbrakk> \<Longrightarrow> \<forall>t. (\<exists>R. x11 = ReplyCap t False R) \<longrightarrow> st_tcb_at awaiting_reply t s \<and> \<not> has_reply_cap t s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 3. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s \<and> s \<turnstile> x11 \<and> real_cte_at x12 s \<and> real_cte_at x13 s \<and> cte_wp_at (is_derived (cdt s) x12 x11) x12 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x13 s \<and> x12 \<noteq> x13 \<and> (\<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11)\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x12 s; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> valid_reply_masters s
 2. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11; cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) x12 s\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 4. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 9. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; invs s; s \<turnstile> x11; real_cte_at x13 s; cte_wp_at (is_derived (cdt s) x12 x11) x12 s; cte_wp_at (\<lambda>c. c = NullCap) x13 s; ex_cte_cap_wp_to is_cnode_cap x13 s; x12 \<noteq> x13; \<forall>r\<in>obj_refs x11. \<forall>a b. x13 \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap'. r \<in> obj_refs cap') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie x11; cte_wp_at (\<lambda>cap. \<not> is_master_reply_cap cap) x12 s\<rbrakk> \<Longrightarrow> \<not> is_master_reply_cap x11
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>invs and (valid_cap x21 and cte_wp_at ((=) NullCap) x23 and cte_wp_at ((\<noteq>) NullCap) x22 and cte_wp_at (weak_derived x21) x22 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x21) x22 and ex_cte_cap_wp_to is_cnode_cap x23 and real_cte_at x22 and real_cte_at x23)\<rbrace> liftE (cap_move x21 x22 x23) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 s. \<lbrakk>i = MoveCall x21 x22 x23; (invs and (valid_cap x21 and cte_wp_at ((=) NullCap) x23 and cte_wp_at ((\<noteq>) NullCap) x22 and cte_wp_at (weak_derived x21) x22 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x21) x22 and ex_cte_cap_wp_to is_cnode_cap x23 and real_cte_at x22 and real_cte_at x23)) s\<rbrakk> \<Longrightarrow> (invs and valid_cap x21 and cte_wp_at ((=) NullCap) x23 and tcb_cap_valid x21 x23 and cte_wp_at (weak_derived x21) x22 and cte_wp_at (\<lambda>c. c \<noteq> NullCap) x22 and ex_cte_cap_wp_to (appropriate_cte_cap x21) x23 and K (x22 \<noteq> x23) and K (\<not> is_master_reply_cap x21)) s
 2. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>invs and cte_wp_at (\<lambda>_. True) x3\<rbrace> cap_revoke x3 \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3 s. \<lbrakk>i = RevokeCall x3; (invs and cte_wp_at (\<lambda>_. True) x3) s\<rbrakk> \<Longrightarrow> invs s
 2. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>invs and real_cte_at x4\<rbrace> cap_delete x4 \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x4 s. \<lbrakk>i = DeleteCall x4; (invs and real_cte_at x4) s\<rbrakk> \<Longrightarrow> (invs and emptyable x4) s
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> (x53 = x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x55 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x55 and cte_wp_at ((\<noteq>) NullCap) x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x55 \<noteq> x54 \<and> x54 \<noteq> x55) and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (cap_swap x51 x55 x52 x54) \<lbrace>\<lambda>rv. invs\<rbrace>) \<and> (x53 \<noteq> x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>)
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> x53 = x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x55 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x55 and cte_wp_at ((\<noteq>) NullCap) x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x55 \<noteq> x54 \<and> x54 \<noteq> x55) and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (cap_swap x51 x55 x52 x54) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> x53 \<noteq> x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 = x55\<rbrakk> \<Longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x55 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x55 and cte_wp_at ((\<noteq>) NullCap) x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x55 \<noteq> x54 \<and> x54 \<noteq> x55) and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (cap_swap x51 x55 x52 x54) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> x53 \<noteq> x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 = x55; (invs and (valid_cap x51 and valid_cap x52 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x55 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x55 and cte_wp_at ((\<noteq>) NullCap) x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x55 \<noteq> x54 \<and> x54 \<noteq> x55) and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)) s\<rbrakk> \<Longrightarrow> (invs and ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 and ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 and valid_cap x51 and valid_cap x52 and tcb_cap_valid x51 x54 and tcb_cap_valid x52 x55 and cte_wp_at (weak_derived x51) x55 and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = x51) x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>cc. is_untyped_cap cc \<longrightarrow> cc = x52) x54 and K (x55 \<noteq> x54 \<and> \<not> is_master_reply_cap x51 \<and> \<not> is_master_reply_cap x52)) s
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> x53 \<noteq> x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> x53 \<noteq> x55 \<longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55\<rbrakk> \<Longrightarrow> \<lbrace>invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55\<rbrakk> \<Longrightarrow> \<lbrace>?Q283 x51 x52 x53 x54 x55\<rbrace> liftE (do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; (invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)) s\<rbrakk> \<Longrightarrow> ?Q283 x51 x52 x53 x54 x55 s
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55\<rbrakk> \<Longrightarrow> \<lbrace>?P'301 x51 x52 x53 x54 x55\<rbrace> cap_move x52 x54 x55 \<lbrace>\<lambda>rv s. cte_wp_at ((=) NullCap) x54 s \<and> tcb_cap_valid x51 x54 s \<and> cte_wp_at (weak_derived x51) x53 s \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) x53 s \<and> ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 s \<and> K (x53 \<noteq> x54) s \<and> K (\<not> is_master_reply_cap x51) s\<rbrace>
 2. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; (invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)) s\<rbrakk> \<Longrightarrow> (invs and valid_cap x52 and cte_wp_at ((=) NullCap) x55 and tcb_cap_valid x52 x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 and ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 and K (x54 \<noteq> x55) and K (\<not> is_master_reply_cap x52)) s \<and> s \<turnstile> x51 \<and> ?P'301 x51 x52 x53 x54 x55 s
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55\<rbrakk> \<Longrightarrow> \<lbrace>?P'301 x51 x52 x53 x54 x55\<rbrace> cap_move x52 x54 x55 \<lbrace>\<lambda>rv s. caps_of_state s x54 = Some NullCap \<and> tcb_cap_valid x51 x54 s \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> weak_derived x51 cap) \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> cap \<noteq> NullCap) \<and> ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 s \<and> x53 \<noteq> x54 \<and> \<not> is_master_reply_cap x51\<rbrace>
 2. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; (invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)) s\<rbrakk> \<Longrightarrow> (invs and valid_cap x52 and cte_wp_at ((=) NullCap) x55 and tcb_cap_valid x52 x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 and ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 and K (x54 \<noteq> x55) and K (\<not> is_master_reply_cap x52)) s \<and> s \<turnstile> x51 \<and> ?P'301 x51 x52 x53 x54 x55 s
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; (invs and (valid_cap x51 and valid_cap x52 and real_cte_at x53 and real_cte_at x55 and real_cte_at x54 and cte_wp_at (weak_derived x51) x53 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 and cte_wp_at ((\<noteq>) NullCap) x53 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 and cte_wp_at ((\<noteq>) NullCap) x54 and (\<lambda>y. x53 \<noteq> x54 \<and> x54 \<noteq> x55) and cte_wp_at (\<lambda>c. c = NullCap) x55 and ex_cte_cap_wp_to is_cnode_cap x54 and ex_cte_cap_wp_to is_cnode_cap x55)) s\<rbrakk> \<Longrightarrow> (invs and valid_cap x52 and cte_wp_at ((=) NullCap) x55 and tcb_cap_valid x52 x55 and cte_wp_at (weak_derived x52) x54 and cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 and ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 and K (x54 \<noteq> x55) and K (\<not> is_master_reply_cap x52)) s \<and> s \<turnstile> x51 \<and> ((caps_of_state s)(x55 \<mapsto> x52, x54 \<mapsto> NullCap)) x54 = Some NullCap \<and> tcb_cap_valid x51 x54 s \<and> (\<exists>cap. ((caps_of_state s)(x55 \<mapsto> x52, x54 \<mapsto> NullCap)) x53 = Some cap \<and> weak_derived x51 cap) \<and> (\<exists>cap. ((caps_of_state s)(x55 \<mapsto> x52, x54 \<mapsto> NullCap)) x53 = Some cap \<and> cap \<noteq> NullCap) \<and> (ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 and cte_wp_at (weak_derived x52) x54 and cte_wp_at ((=) NullCap) x55 and K (x54 \<noteq> x55) and K (\<forall>cap'. weak_derived x52 cap' \<longrightarrow> appropriate_cte_cap x51 x52 = appropriate_cte_cap x51 cap')) s \<and> x53 \<noteq> x54 \<and> \<not> is_master_reply_cap x51
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; invs s \<and> s \<turnstile> x51 \<and> s \<turnstile> x52 \<and> real_cte_at x53 s \<and> real_cte_at x55 s \<and> real_cte_at x54 s \<and> cte_wp_at (weak_derived x51) x53 s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 s \<and> cte_wp_at ((\<noteq>) NullCap) x53 s \<and> cte_wp_at (weak_derived x52) x54 s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 s \<and> cte_wp_at ((\<noteq>) NullCap) x54 s \<and> x53 \<noteq> x54 \<and> x54 \<noteq> x55 \<and> cte_wp_at (\<lambda>c. c = NullCap) x55 s \<and> ex_cte_cap_wp_to is_cnode_cap x54 s \<and> ex_cte_cap_wp_to is_cnode_cap x55 s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) NullCap) x55 s \<and> tcb_cap_valid x52 x55 s \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 s \<and> ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 s \<and> \<not> is_master_reply_cap x52 \<and> tcb_cap_valid x51 x54 s \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> weak_derived x51 cap) \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> cap \<noteq> NullCap) \<and> ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 s \<and> cte_wp_at ((=) NullCap) x55 s \<and> (\<forall>cap'. weak_derived x52 cap' \<longrightarrow> appropriate_cte_cap x51 x52 = appropriate_cte_cap x51 cap') \<and> \<not> is_master_reply_cap x51
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; invs s; s \<turnstile> x51; s \<turnstile> x52; real_cte_at x53 s; real_cte_at x55 s; real_cte_at x54 s; cte_wp_at (weak_derived x51) x53 s; cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 s; cte_wp_at ((\<noteq>) NullCap) x53 s; cte_wp_at (weak_derived x52) x54 s; cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 s; cte_wp_at ((\<noteq>) NullCap) x54 s; x53 \<noteq> x54; x54 \<noteq> x55; cte_wp_at (\<lambda>c. c = NullCap) x55 s; ex_cte_cap_wp_to is_cnode_cap x54 s; ex_cte_cap_wp_to is_cnode_cap x55 s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) NullCap) x55 s \<and> tcb_cap_valid x52 x55 s \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 s \<and> ex_cte_cap_wp_to (appropriate_cte_cap x52) x55 s \<and> \<not> is_master_reply_cap x52 \<and> tcb_cap_valid x51 x54 s \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> weak_derived x51 cap) \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> cap \<noteq> NullCap) \<and> ex_cte_cap_wp_to (appropriate_cte_cap x51) x54 s \<and> cte_wp_at ((=) NullCap) x55 s \<and> (\<forall>cap'. weak_derived x52 cap' \<longrightarrow> appropriate_cte_cap x51 x52 = appropriate_cte_cap x51 cap') \<and> \<not> is_master_reply_cap x51
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; x53 \<noteq> x55; invs s; s \<turnstile> x51; s \<turnstile> x52; real_cte_at x53 s; real_cte_at x55 s; real_cte_at x54 s; cte_wp_at (weak_derived x51) x53 s; cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x51) x53 s; cte_wp_at ((\<noteq>) NullCap) x53 s; cte_wp_at (weak_derived x52) x54 s; cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x52) x54 s; cte_wp_at ((\<noteq>) NullCap) x54 s; x53 \<noteq> x54; x54 \<noteq> x55; cte_wp_at (\<lambda>c. c = NullCap) x55 s; ex_cte_cap_wp_to is_cnode_cap x54 s; ex_cte_cap_wp_to is_cnode_cap x55 s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) NullCap) x55 s \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) x54 s \<and> \<not> is_master_reply_cap x52 \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> weak_derived x51 cap) \<and> (\<exists>cap. caps_of_state s x53 = Some cap \<and> cap \<noteq> NullCap) \<and> cte_wp_at ((=) NullCap) x55 s \<and> \<not> is_master_reply_cap x51
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x xa xb xc. \<lbrakk>i = SaveCall (a, b); invs x; ex_cte_cap_wp_to is_cnode_cap (a, b) x; cte_wp_at (\<lambda>c. c = NullCap) (a, b) x; cap_table_at (length b) a x; cte_wp_at ((=) (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x; \<not> xb\<rbrakk> \<Longrightarrow> x \<turnstile> ReplyCap xa False xc \<and> cte_wp_at ((=) NullCap) (a, b) x \<and> tcb_cap_valid (ReplyCap xa False xc) (a, b) x \<and> cte_wp_at (weak_derived (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) (cur_thread x, tcb_cnode_index 3) x \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ReplyCap xa False xc)) (a, b) x \<and> (cur_thread x = a \<longrightarrow> tcb_cnode_index 3 \<noteq> b) \<and> \<not> is_master_reply_cap (ReplyCap xa False xc)
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b x xa xb xc. \<lbrakk>i = SaveCall (a, b); invs x; ex_cte_cap_wp_to is_cnode_cap (a, b) x; cte_wp_at (\<lambda>c. c = NullCap) (a, b) x; cap_table_at (length b) a x; cte_wp_at ((=) (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x; \<not> xb\<rbrakk> \<Longrightarrow> x \<turnstile> ReplyCap xa False xc
 2. \<And>a b x xa xb xc. \<lbrakk>i = SaveCall (a, b); invs x; ex_cte_cap_wp_to is_cnode_cap (a, b) x; cte_wp_at (\<lambda>c. c = NullCap) (a, b) x; cap_table_at (length b) a x; cte_wp_at ((=) (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x; \<not> xb\<rbrakk> \<Longrightarrow> cte_wp_at ((=) NullCap) (a, b) x \<and> tcb_cap_valid (ReplyCap xa False xc) (a, b) x \<and> cte_wp_at (weak_derived (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) (cur_thread x, tcb_cnode_index 3) x \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ReplyCap xa False xc)) (a, b) x \<and> (cur_thread x = a \<longrightarrow> tcb_cnode_index 3 \<noteq> b) \<and> \<not> is_master_reply_cap (ReplyCap xa False xc)
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b x xa xb xc. \<lbrakk>i = SaveCall (a, b); invs x; ex_cte_cap_wp_to is_cnode_cap (a, b) x; cte_wp_at (\<lambda>c. c = NullCap) (a, b) x; cap_table_at (length b) a x; cte_wp_at ((=) (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x; \<not> xb\<rbrakk> \<Longrightarrow> cte_wp_at ((=) NullCap) (a, b) x \<and> tcb_cap_valid (ReplyCap xa False xc) (a, b) x \<and> cte_wp_at (weak_derived (ReplyCap xa False xc)) (cur_thread x, tcb_cnode_index 3) x \<and> cte_wp_at (\<lambda>c. c \<noteq> NullCap) (cur_thread x, tcb_cnode_index 3) x \<and> ex_cte_cap_wp_to (appropriate_cte_cap (ReplyCap xa False xc)) (a, b) x \<and> (cur_thread x = a \<longrightarrow> tcb_cnode_index 3 \<noteq> b) \<and> \<not> is_master_reply_cap (ReplyCap xa False xc)
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>invs and valid_cnode_inv i\<rbrace> case i of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!