theory Syscall_AC

lemma handle_invocation_pas_refined:
  "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'
                    and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace>
   handle_invocation calling blocking
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: handle_invocation_def split_def) apply (cases blocking, simp) 
  (* slow ~30s *)
   by ((wp syscall_valid without_preemption_wp handle_fault_pas_refined
             set_thread_state_pas_refined set_thread_state_runnable_valid_sched
             perform_invocation_pas_refined hoare_vcg_conj_lift hoare_vcg_all_lift
             rfk_invs sts_st_tcb_at'' sts_ct_in_state
       | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
       | wpc
       | rule hoare_drop_imps
       | simp add: if_apply_def2 conj_comms split del: if_split
              del: hoare_True_E_R)+,
      (wp lookup_extra_caps_auth lookup_extra_caps_authorised decode_invocation_authorised
          lookup_cap_and_slot_authorised lookup_cap_and_slot_cur_auth as_user_pas_refined
          lookup_cap_and_slot_valid_fault3 hoare_vcg_const_imp_lift_R
       | simp add: comp_def runnable_eq_active split del: if_split)+,
       fastforce intro: guarded_to_cur_domain if_live_then_nonz_capD
                  simp: ct_in_state_def st_tcb_at_def live_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. blocking \<Longrightarrow> \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (handle_fault thread) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation True calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<not> blocking \<Longrightarrow> \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. blocking \<Longrightarrow> \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (handle_fault thread) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation True calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<not> blocking \<Longrightarrow> \<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and einvs and ct_active and schact_is_rct and is_subject aag \<circ> cur_thread\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
ptr <- liftE (liftM to_bl (as_user thread (getRegister cap_register)));
syscall (doE p <- cap_fault_on_failure (of_bl ptr) False (lookup_cap_and_slot thread ptr);
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>p. doE args <- liftE (get_mrs thread (snd (snd (snd p))) info);
decode_invocation (mi_label info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (get_thread_state thread >>= case_thread_state (return ()) (return ()) (do y <- when calling (reply_from_kernel thread (0, reply));
set_thread_state thread Running
od) (\<lambda>word receiver_payload_ext. return ()) (\<lambda>word sender_payload_ext. return ()) (return ()) (\<lambda>word. return ()) (return ()))
odE)
odE \<lbrace>\<lambda>_. pas_refined aag\<rbrace>