theory FinalCaps

lemma invoke_cnode_silc_inv:
  "\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i
                    and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<rbrace>
   invoke_cnode i
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding invoke_cnode_def apply (case_tac i) apply (wp cap_insert_silc_inv | simp)+ apply (fastforce simp: silc_inv_def authorised_cnode_inv_def) apply (wp cap_move_silc_inv | simp)+ apply (fastforce simp: silc_inv_def authorised_cnode_inv_def) apply (wp cap_revoke_silc_inv | simp)+ apply (fastforce simp: authorised_cnode_inv_def) apply (wp cap_delete_silc_inv_not_transferable | simp)+ apply (force simp: authorised_cnode_inv_def intro: real_cte_emptyable_strg[rule_format]) apply (rule hoare_pre) apply (wp cap_move_silc_inv cap_swap_silc_inv cap_move_cte_wp_at_other
            | simp split del: if_split)+ apply (fastforce simp: silc_inv_def authorised_cnode_inv_def) apply (wp cap_move_silc_inv get_cap_wp | wpc | simp)+ apply (clarsimp simp: silc_inv_def authorised_cnode_inv_def) apply (erule cte_wp_at_weak_derived_ReplyCap) apply (wp cancel_badged_sends_silc_inv | simp | wpc | rule hoare_pre)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<rbrace> invoke_cnode i \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13. i = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>i = InsertCall x11 x12 x13; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag 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) \<and> authorised_cnode_inv aag (InsertCall x11 x12 x13) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst x12) = pasObjectAbs aag (fst x13) \<and> pasObjectAbs aag (fst x13) \<noteq> SilcLabel
 2. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 6. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 7. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23. i = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 6. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 s. \<lbrakk>i = MoveCall x21 x22 x23; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> s \<turnstile> x21 \<and> cte_wp_at ((=) NullCap) x23 s \<and> cte_wp_at ((\<noteq>) NullCap) x22 s \<and> cte_wp_at (weak_derived x21) x22 s \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> c = x21) x22 s \<and> ex_cte_cap_wp_to is_cnode_cap x23 s \<and> real_cte_at x22 s \<and> real_cte_at x23 s \<and> authorised_cnode_inv aag (MoveCall x21 x22 x23) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> pasObjectAbs aag (fst x22) = pasObjectAbs aag (fst x23) \<and> pasObjectAbs aag (fst x23) \<noteq> SilcLabel
 2. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 6. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3. i = RevokeCall x3 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x3 s. \<lbrakk>i = RevokeCall x3; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> cte_wp_at (\<lambda>_. True) x3 s \<and> authorised_cnode_inv aag (RevokeCall x3) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> is_subject aag (fst x3)
 2. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 5. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x4. i = DeleteCall x4 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x4 s. \<lbrakk>i = DeleteCall x4; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> real_cte_at x4 s \<and> authorised_cnode_inv aag (DeleteCall x4) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> emptyable x4 s \<and> is_subject aag (fst x4)
 2. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x54 x55. i = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>?Q101 x51 x52 x53 x54 x55\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; (silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread) s\<rbrakk> \<Longrightarrow> ?Q101 x51 x52 x53 x54 x55 s
 3. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 4. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x51 x52 x53 x54 x55 s. \<lbrakk>i = RotateCall x51 x52 x53 x54 x55; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag 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> (x53 \<noteq> x55 \<longrightarrow> 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 \<and> authorised_cnode_inv aag (RotateCall x51 x52 x53 x54 x55) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (x53 = x55 \<longrightarrow> cte_wp_at (weak_derived x51) x55 s \<and> pasObjectAbs aag (fst x55) = pasObjectAbs aag (fst x54) \<and> pasObjectAbs aag (fst x54) \<noteq> SilcLabel) \<and> (x53 \<noteq> x55 \<longrightarrow> pasObjectAbs aag (fst x54) = pasObjectAbs aag (fst x55) \<and> pasObjectAbs aag (fst x55) \<noteq> SilcLabel \<and> pasObjectAbs aag (fst x53) = pasObjectAbs aag (fst x54) \<and> pasObjectAbs aag (fst x54) \<noteq> SilcLabel)
 2. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 3. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6. i = SaveCall x6 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace>
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x6 s. \<lbrakk>i = SaveCall x6; silc_inv aag st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> ex_cte_cap_wp_to is_cnode_cap x6 s \<and> cte_wp_at (\<lambda>c. c = NullCap) x6 s \<and> real_cte_at x6 s \<and> authorised_cnode_inv aag (SaveCall x6) s \<and> is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (cur_thread s, tcb_cnode_index 3) s \<longrightarrow> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> cte_wp_at (weak_derived (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s \<and> pasSubject aag = pasObjectAbs aag (fst x6) \<and> pasObjectAbs aag (fst x6) \<noteq> SilcLabel)
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b s x xa xb. \<lbrakk>i = SaveCall (a, b); SilcLabel \<noteq> pasSubject aag; \<forall>x. pasObjectAbs aag x = SilcLabel \<longrightarrow> (\<exists>sz. cap_table_at sz x s); \<forall>y. (\<exists>auth. (y, auth, SilcLabel) \<in> pasPolicy aag) \<longrightarrow> y = SilcLabel; \<forall>a b cap. cte_wp_at ((=) cap) (a, b) s \<and> \<not> intra_label_cap aag (a, b) s \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps cap s) \<and> pasObjectAbs aag a = SilcLabel); all_children (\<lambda>x. pasObjectAbs aag (fst x) = SilcLabel) (cdt s); silc_dom_equiv aag st s; \<forall>a. pasObjectAbs aag a = SilcLabel \<longrightarrow> (\<forall>b. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> is_transferable_cap cap) (a, b) st); invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; is_subject aag a; is_subject aag (cur_thread s); cte_wp_at ((=) (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s; \<not> xa\<rbrakk> \<Longrightarrow> cte_wp_at (weak_derived (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s
 2. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x7. i = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and valid_cnode_inv i and authorised_cnode_inv aag i and is_subject aag \<circ> cur_thread\<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>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!