theory Decode_IF

lemma decode_tcb_invocation_reads_respects_f:
  notes respects_f = reads_respects_f[where st=st and Q=\<top>]
  shows
    "reads_respects_f aag l (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and
                             valid_objs and zombies_final and
                             K (is_subject aag t \<and> (\<forall>x \<in> set excaps. is_subject aag (fst (snd x)))
                                                 \<and> (\<forall>x \<in> set excaps. pas_cap_cur_auth aag (fst x))))
                      (decode_tcb_invocation label args (ThreadCap t) slot excaps)" unfolding decode_tcb_invocation_def decode_read_registers_def decode_write_registers_def
            decode_copy_registers_def decode_tcb_configure_def decode_set_space_def
            decode_bind_notification_def decode_set_ipc_buffer_def fun_app_def
            decode_unbind_notification_def decode_set_tls_base_def apply (simp add: unlessE_def[symmetric] unlessE_whenE split del: if_split
             cong: gen_invocation_labels.case_cong) apply (rule equiv_valid_guard_imp) apply (wp (once) requiv_cur_thread_eq range_check_ev respects_f[OF derive_cap_rev]
                    derive_cap_inv slot_cap_long_running_delete_reads_respects_f[where st=st]
                    respects_f[OF check_valid_ipc_buffer_rev] check_valid_ipc_buffer_inv
                    respects_f[OF decode_set_priority_rev] respects_f[OF decode_set_mcpriority_rev]
                    respects_f[OF decode_set_sched_params_rev]
                    respects_f[OF get_simple_ko_reads_respects]
                    respects_f[OF get_bound_notification_reads_respects']
          | wp (once) whenE_throwError_wp
          | wp (once) hoare_drop_imps
          | wpc
          | simp add: if_apply_def2 split del: if_split add: o_def split_def)+ apply (simp add: get_tcb_ctable_ptr_def get_tcb_vtable_ptr_def) apply (subgoal_tac "\<not>length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))") prefer 2 apply (fastforce intro: nth_mem) apply (subgoal_tac "excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))") prefer 2 apply (fastforce intro: nth_mem) apply (intro allI impI conjI; (rule disjI1 | fastforce simp: reads_equiv_f_def)) apply (rule reads_ep[where auth="Receive",simplified]) apply (cases excaps; simp) by (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and valid_objs and zombies_final and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) (decode_tcb_invocation label args (ThreadCap t) slot excaps) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and valid_objs and zombies_final and K (is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) (case gen_invocation_type label of TCBReadRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 (word_of_nat (length frameRegisters + length gpRegisters));
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters)
odE | TCBWriteRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) (throwError TruncatedMessage);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE | TCBCopyRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (map fst excaps = []) (throwError TruncatedMessage);
src_tcb <- case map fst excaps of [] \<Rightarrow> throwError (InvalidCapability 1) | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError (InvalidCapability 1);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
returnOk (CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters)
odE | TCBConfigure \<Rightarrow> doE whenE (length args < 4) (throwError TruncatedMessage);
whenE (length excaps < 3) (throwError TruncatedMessage);
fault_ep <- returnOk (args ! 0);
croot_data <- returnOk (args ! 1);
vroot_data <- returnOk (args ! 2);
crootvroot <- returnOk (take 2 excaps);
buffer_cap <- returnOk (excaps ! 2);
buffer <- returnOk (args ! 3);
set_params <- doE whenE (length [buffer] = 0) (throwError TruncatedMessage);
whenE (length [buffer_cap] = 0) (throwError TruncatedMessage);
buffer <- returnOk (data_to_vref ([buffer] ! 0));
(bcap, bslot) <- returnOk ([buffer_cap] ! 0);
newbuf <- if buffer = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer buffer buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl (obj_ref_of (ThreadCap t)) slot None None None None None (Some (buffer, newbuf)))
odE;
set_space <- doE whenE (length [fault_ep, croot_data, vroot_data] < 3 \<or> length crootvroot < 2) (throwError TruncatedMessage);
fault_epa <- returnOk ([fault_ep, croot_data, vroot_data] ! 0);
croot_dataa <- returnOk ([fault_ep, croot_data, vroot_data] ! 1);
vroot_data <- returnOk ([fault_ep, croot_data, vroot_data] ! 2);
croot_arg <- returnOk (crootvroot ! 0);
vroot_arg <- returnOk (crootvroot ! 1);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr (obj_ref_of (ThreadCap t)))));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr (obj_ref_of (ThreadCap t)))));
unlessE (can_chg_cr \<and> can_chg_vr) (throwError IllegalOperation);
croot_cap <- returnOk (fst croot_arg);
croot_slot <- returnOk (snd croot_arg);
croot_cap' <- derive_cap croot_slot ((if croot_dataa = 0 then id else update_cap_data False croot_dataa) croot_cap);
unlessE (is_cnode_cap croot_cap') (throwError IllegalOperation);
croot <- returnOk (croot_cap', croot_slot);
vroot_cap <- returnOk (fst vroot_arg);
vroot_slot <- returnOk (snd vroot_arg);
vroot_cap' <- derive_cap vroot_slot ((if vroot_data = 0 then id else update_cap_data False vroot_data) vroot_cap);
unlessE (is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
vroot <- returnOk (vroot_cap', vroot_slot);
returnOk (ThreadControl (obj_ref_of (ThreadCap t)) slot (Some (to_bl fault_epa)) None None (Some croot) (Some vroot) None)
odE;
returnOk (ThreadControl (obj_ref_of (ThreadCap t)) slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot excaps | TCBSetIPCBuffer \<Rightarrow> doE whenE (length args = 0) (throwError TruncatedMessage);
whenE (length excaps = 0) (throwError TruncatedMessage);
buffer <- returnOk (data_to_vref (args ! 0));
(bcap, bslot) <- returnOk (excaps ! 0);
newbuf <- if buffer = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer buffer buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl (obj_ref_of (ThreadCap t)) slot None None None None None (Some (buffer, newbuf)))
odE | TCBSetSpace \<Rightarrow> doE whenE (length args < 3 \<or> length excaps < 2) (throwError TruncatedMessage);
fault_ep <- returnOk (args ! 0);
croot_data <- returnOk (args ! 1);
vroot_data <- returnOk (args ! 2);
croot_arg <- returnOk (excaps ! 0);
vroot_arg <- returnOk (excaps ! 1);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr (obj_ref_of (ThreadCap t)))));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr (obj_ref_of (ThreadCap t)))));
unlessE (can_chg_cr \<and> can_chg_vr) (throwError IllegalOperation);
croot_cap <- returnOk (fst croot_arg);
croot_slot <- returnOk (snd croot_arg);
croot_cap' <- derive_cap croot_slot ((if croot_data = 0 then id else update_cap_data False croot_data) croot_cap);
unlessE (is_cnode_cap croot_cap') (throwError IllegalOperation);
croot <- returnOk (croot_cap', croot_slot);
vroot_cap <- returnOk (fst vroot_arg);
vroot_slot <- returnOk (snd vroot_arg);
vroot_cap' <- derive_cap vroot_slot ((if vroot_data = 0 then id else update_cap_data False vroot_data) vroot_cap);
unlessE (is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
vroot <- returnOk (vroot_cap', vroot_slot);
returnOk (ThreadControl (obj_ref_of (ThreadCap t)) slot (Some (to_bl fault_ep)) None None (Some croot) (Some vroot) None)
odE | TCBSuspend \<Rightarrow> returnOk (Suspend (obj_ref_of (ThreadCap t))) | TCBResume \<Rightarrow> returnOk (Resume (obj_ref_of (ThreadCap t))) | TCBBindNotification \<Rightarrow> case ThreadCap t of ThreadCap tcb \<Rightarrow> doE whenE (length excaps = 0) (throwError TruncatedMessage);
nTFN <- liftE (get_bound_notification tcb);
case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
whenE (AllowRecv \<notin> rights) (throwError IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (WaitingNtfn list, b) \<Rightarrow> throwError IllegalOperation | (_, None) \<Rightarrow> returnOk () | (_, Some a) \<Rightarrow> throwError IllegalOperation;
returnOk (NotificationControl tcb (Some ntfnptr))
odE | _ \<Rightarrow> throwError IllegalOperation | TCBUnbindNotification \<Rightarrow> case ThreadCap t of ThreadCap tcb \<Rightarrow> doE nTFN <- liftE (get_bound_notification tcb);
case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl tcb None)
odE | _ \<Rightarrow> throwError IllegalOperation | TCBSetTLSBase \<Rightarrow> doE whenE (length args = 0) (throwError TruncatedMessage);
returnOk (SetTLSBase (obj_ref_of (ThreadCap t)) (UCAST(32 \<rightarrow> 32) (args ! 0)))
odE | _ \<Rightarrow> throwError IllegalOperation) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and valid_objs and zombies_final and (\<lambda>y. is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) (case gen_invocation_type label of TCBReadRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 (word_of_nat (length frameRegisters + length gpRegisters));
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters)
odE | TCBWriteRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) (throwError TruncatedMessage);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE | TCBCopyRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (map fst excaps = []) (throwError TruncatedMessage);
src_tcb <- case map fst excaps of [] \<Rightarrow> throwError (InvalidCapability 1) | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError (InvalidCapability 1);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
returnOk (CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters)
odE | TCBConfigure \<Rightarrow> doE y <- whenE (length args < 4) (throwError TruncatedMessage);
y <- whenE (length excaps < 3) (throwError TruncatedMessage);
set_params <- case excaps ! 2 of (bcap, bslot) \<Rightarrow> doE newbuf <- if data_to_vref (args ! 3) = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer (data_to_vref (args ! 3)) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 3), newbuf)))
odE;
set_space <- doE y <- whenE (min (length excaps) 2 < 2) (throwError TruncatedMessage);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- whenE (can_chg_cr \<longrightarrow> \<not> can_chg_vr) (throwError IllegalOperation);
croot_cap' <- derive_cap (snd (excaps ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (excaps ! 0)));
y <- whenE (\<not> is_cnode_cap croot_cap') (throwError IllegalOperation);
vroot_cap' <- derive_cap (snd (excaps ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (excaps ! Suc 0)));
y <- whenE (\<not> is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (excaps ! 0))) (Some (vroot_cap', snd (excaps ! Suc 0))) None)
odE;
returnOk (ThreadControl t slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot excaps | TCBSetIPCBuffer \<Rightarrow> doE y <- whenE (args = []) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
case excaps ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if data_to_vref (args ! 0) = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer (data_to_vref (args ! 0)) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), newbuf)))
odE
odE | TCBSetSpace \<Rightarrow> doE y <- whenE (length args < 3 \<or> length excaps < 2) (throwError TruncatedMessage);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- whenE (can_chg_cr \<longrightarrow> \<not> can_chg_vr) (throwError IllegalOperation);
croot_cap' <- derive_cap (snd (excaps ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (excaps ! 0)));
y <- whenE (\<not> is_cnode_cap croot_cap') (throwError IllegalOperation);
vroot_cap' <- derive_cap (snd (excaps ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (excaps ! Suc 0)));
y <- whenE (\<not> is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (excaps ! 0))) (Some (vroot_cap', snd (excaps ! Suc 0))) None)
odE | TCBSuspend \<Rightarrow> returnOk (Suspend t) | TCBResume \<Rightarrow> returnOk (Resume t) | TCBBindNotification \<Rightarrow> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of WaitingNtfn list \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError IllegalOperation;
returnOk (NotificationControl t (Some ntfnptr))
odE | TCBUnbindNotification \<Rightarrow> doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl t None)
odE | TCBSetTLSBase \<Rightarrow> doE y <- whenE (args = []) (throwError TruncatedMessage);
returnOk (SetTLSBase t (args ! 0))
odE | _ \<Rightarrow> throwError IllegalOperation) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q32 (case gen_invocation_type label of TCBReadRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # x \<Rightarrow> doE range_check n 1 (word_of_nat (length frameRegisters + length gpRegisters));
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (ReadRegisters p (flags !! 0) n ArchDefaultExtraRegisters)
odE | TCBWriteRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | [flags] \<Rightarrow> throwError TruncatedMessage | flags # n # values \<Rightarrow> doE whenE (length values < unat n) (throwError TruncatedMessage);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
self <- liftE (gets cur_thread);
whenE (p = self) (throwError IllegalOperation);
returnOk (WriteRegisters p (flags !! 0) (take (unat n) values) ArchDefaultExtraRegisters)
odE | TCBCopyRegisters \<Rightarrow> case args of [] \<Rightarrow> throwError TruncatedMessage | flags # x \<Rightarrow> doE suspend_source <- returnOk (flags !! 0);
resume_target <- returnOk (flags !! 1);
transfer_frame <- returnOk (flags !! 2);
transfer_integer <- returnOk (flags !! 3);
whenE (map fst excaps = []) (throwError TruncatedMessage);
src_tcb <- case map fst excaps of [] \<Rightarrow> throwError (InvalidCapability 1) | ThreadCap p # x \<Rightarrow> returnOk p | _ # x \<Rightarrow> throwError (InvalidCapability 1);
p <- case ThreadCap t of ThreadCap p \<Rightarrow> returnOk p;
returnOk (CopyRegisters p src_tcb suspend_source resume_target transfer_frame transfer_integer ArchDefaultExtraRegisters)
odE | TCBConfigure \<Rightarrow> doE y <- whenE (length args < 4) (throwError TruncatedMessage);
y <- whenE (length excaps < 3) (throwError TruncatedMessage);
set_params <- case excaps ! 2 of (bcap, bslot) \<Rightarrow> doE newbuf <- if data_to_vref (args ! 3) = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer (data_to_vref (args ! 3)) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 3), newbuf)))
odE;
set_space <- doE y <- whenE (min (length excaps) 2 < 2) (throwError TruncatedMessage);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- whenE (can_chg_cr \<longrightarrow> \<not> can_chg_vr) (throwError IllegalOperation);
croot_cap' <- derive_cap (snd (excaps ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (excaps ! 0)));
y <- whenE (\<not> is_cnode_cap croot_cap') (throwError IllegalOperation);
vroot_cap' <- derive_cap (snd (excaps ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (excaps ! Suc 0)));
y <- whenE (\<not> is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (excaps ! 0))) (Some (vroot_cap', snd (excaps ! Suc 0))) None)
odE;
returnOk (ThreadControl t slot (tc_new_fault_ep set_space) None None (tc_new_croot set_space) (tc_new_vroot set_space) (tc_new_buffer set_params))
odE | TCBSetPriority \<Rightarrow> decode_set_priority args (ThreadCap t) slot excaps | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority args (ThreadCap t) slot excaps | TCBSetSchedParams \<Rightarrow> decode_set_sched_params args (ThreadCap t) slot excaps | TCBSetIPCBuffer \<Rightarrow> doE y <- whenE (args = []) (throwError TruncatedMessage);
y <- whenE (excaps = []) (throwError TruncatedMessage);
case excaps ! 0 of (bcap, bslot) \<Rightarrow> doE newbuf <- if data_to_vref (args ! 0) = 0 then returnOk None else doE buffer_cap <- derive_cap bslot bcap;
check_valid_ipc_buffer (data_to_vref (args ! 0)) buffer_cap;
returnOk (Some (buffer_cap, bslot))
odE;
returnOk (ThreadControl t slot None None None None None (Some (data_to_vref (args ! 0), newbuf)))
odE
odE | TCBSetSpace \<Rightarrow> doE y <- whenE (length args < 3 \<or> length excaps < 2) (throwError TruncatedMessage);
can_chg_cr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_ctable_ptr t)));
can_chg_vr <- liftE (liftM Not (slot_cap_long_running_delete (get_tcb_vtable_ptr t)));
y <- whenE (can_chg_cr \<longrightarrow> \<not> can_chg_vr) (throwError IllegalOperation);
croot_cap' <- derive_cap (snd (excaps ! 0)) ((if args ! Suc 0 = 0 then id else update_cap_data False (args ! Suc 0)) (fst (excaps ! 0)));
y <- whenE (\<not> is_cnode_cap croot_cap') (throwError IllegalOperation);
vroot_cap' <- derive_cap (snd (excaps ! Suc 0)) ((if args ! 2 = 0 then id else update_cap_data False (args ! 2)) (fst (excaps ! Suc 0)));
y <- whenE (\<not> is_valid_vtable_root vroot_cap') (throwError IllegalOperation);
returnOk (ThreadControl t slot (Some (to_bl (args ! 0))) None None (Some (croot_cap', snd (excaps ! 0))) (Some (vroot_cap', snd (excaps ! Suc 0))) None)
odE | TCBSuspend \<Rightarrow> returnOk (Suspend t) | TCBResume \<Rightarrow> returnOk (Resume t) | TCBBindNotification \<Rightarrow> doE y <- whenE (excaps = []) (throwError TruncatedMessage);
nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> returnOk () | Some x \<Rightarrow> throwError IllegalOperation;
(ntfnptr, rights) <- case fst (hd excaps) of NotificationCap ptr x r \<Rightarrow> returnOk (ptr, r) | _ \<Rightarrow> throwError IllegalOperation;
y <- whenE (AllowRead \<notin> rights) (throwError IllegalOperation);
ntfn <- liftE (get_notification ntfnptr);
y <- case ntfn_obj ntfn of WaitingNtfn list \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throwError IllegalOperation;
returnOk (NotificationControl t (Some ntfnptr))
odE | TCBUnbindNotification \<Rightarrow> doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl t None)
odE | TCBSetTLSBase \<Rightarrow> doE y <- whenE (args = []) (throwError TruncatedMessage);
returnOk (SetTLSBase t (args ! 0))
odE | _ \<Rightarrow> throwError IllegalOperation)
 2. \<And>s. (silc_inv aag st and pas_refined aag and is_subject aag \<circ> cur_thread and valid_objs and zombies_final and (\<lambda>y. is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)))) s \<Longrightarrow> ?Q32 s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)) \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (get_tcb_ctable_ptr t)) \<and> is_subject aag (fst (get_tcb_vtable_ptr t)) \<and> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (get_tcb_ctable_ptr t)) \<and> is_subject aag (fst (get_tcb_vtable_ptr t)) \<and> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)) \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x))
 2. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)) \<Longrightarrow> \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))) proof (prove)
goal (2 subgoals):
 1. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)) \<Longrightarrow> \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))
 2. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))); excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x))
 2. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))\<rbrakk> \<Longrightarrow> excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2)))\<rbrakk> \<Longrightarrow> excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))
 2. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))); excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))); excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))\<rbrakk> \<Longrightarrow> (gen_invocation_type label = TCBReadRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBWriteRegisters \<longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> (\<exists>x xb. xa = x # xb) \<longrightarrow> (\<forall>s t. reads_equiv_f aag s t \<and> affects_equiv aag l s t \<longrightarrow> cur_thread s = cur_thread t))) \<and> (gen_invocation_type label = TCBConfigure \<longrightarrow> \<not> length args < 4 \<longrightarrow> \<not> length excaps < 3 \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 2 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 3) \<noteq> 0 \<longrightarrow> is_subject aag a) \<and> ((\<exists>x a b. excaps ! 2 = (x, a, b)) \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))))) \<and> (gen_invocation_type label = TCBSetIPCBuffer \<longrightarrow> args \<noteq> [] \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x a. (\<exists>b. excaps ! 0 = (x, a, b)) \<longrightarrow> data_to_vref (args ! 0) \<noteq> 0 \<longrightarrow> is_subject aag a)) \<and> (gen_invocation_type label = TCBSetSpace \<longrightarrow> \<not> length args < 3 \<and> \<not> length excaps < 2 \<longrightarrow> is_subject aag (fst (snd (excaps ! 0)))) \<and> (gen_invocation_type label = TCBBindNotification \<longrightarrow> excaps \<noteq> [] \<longrightarrow> (\<forall>x xa xb. fst (hd excaps) = NotificationCap x xa xb \<longrightarrow> AllowRead \<in> xb \<longrightarrow> aag_can_read_or_affect aag l x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))); excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))); gen_invocation_type label = TCBBindNotification; excaps \<noteq> []; fst (hd excaps) = NotificationCap x xa xb; AllowRead \<in> xb\<rbrakk> \<Longrightarrow> aag_can_read aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> (\<forall>x\<in>set excaps. is_subject aag (fst (snd x))) \<and> (\<forall>x\<in>set excaps. pas_cap_cur_auth aag (fst x)); \<not> length excaps < 3 \<longrightarrow> is_subject aag (fst (snd (excaps ! 2))); excaps \<noteq> [] \<longrightarrow> is_subject aag (fst (snd (excaps ! 0))); gen_invocation_type label = TCBBindNotification; excaps \<noteq> []; fst (hd excaps) = NotificationCap x xa xb; AllowRead \<in> xb\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb a list. \<lbrakk>silc_inv aag st s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag t \<and> is_subject aag (fst (snd a)) \<and> (\<forall>x\<in>set list. is_subject aag (fst (snd x))) \<and> pas_cap_cur_auth aag (NotificationCap x xa xb) \<and> (\<forall>x\<in>set list. pas_cap_cur_auth aag (fst x)); gen_invocation_type label = TCBBindNotification; fst a = NotificationCap x xa xb; AllowRead \<in> xb; excaps = a # list\<rbrakk> \<Longrightarrow> (pasSubject aag, Receive, pasObjectAbs aag x) \<in> pasPolicy aag