theory Syscall_AC

lemma handle_invocation_respects:
  "\<lbrace>integrity aag X st and 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 and ((=) st)\<rbrace>
   handle_invocation calling blocking
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: handle_invocation_def split_def) apply (wp syscall_valid without_preemption_wp handle_fault_integrity_autarch
            reply_from_kernel_integrity_autarch
            set_thread_state_integrity_autarch
            hoare_vcg_conj_lift
            hoare_vcg_all_lift_R hoare_vcg_all_lift
         | rule hoare_drop_imps
         | wpc
         | simp add: if_apply_def2
                split del: if_split)+ apply (simp add: conj_comms pred_conj_def comp_def if_apply_def2 split del: if_split
                | wp perform_invocation_respects set_thread_state_pas_refined
                   set_thread_state_authorised
                   set_thread_state_runnable_valid_sched
                   set_thread_state_integrity_autarch
                   sts_first_restart
                   decode_invocation_authorised
                   lookup_extra_caps_auth lookup_extra_caps_authorised
                   set_thread_state_integrity_autarch
                   lookup_cap_and_slot_cur_auth lookup_cap_and_slot_authorised
                   hoare_vcg_const_imp_lift perform_invocation_pas_refined
                   set_thread_state_ct_st hoare_vcg_const_imp_lift_R
                   lookup_cap_and_slot_valid_fault3
                | (rule valid_validE, strengthen invs_vobjs_strgs))+ by (fastforce intro: st_tcb_ex_cap' guarded_to_cur_domain
                 simp: ct_in_state_def runnable_eq_active)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and 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 and (=) st\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and 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 and (=) st\<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>_. integrity aag X st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?B10 thread info ptr rv ()\<rbrace> perform_invocation blocking calling rv \<lbrace>\<lambda>reply s. integrity aag X st s \<and> (calling \<longrightarrow> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> is_subject aag thread) \<and> (\<not> calling \<longrightarrow> integrity aag X st s) \<and> is_subject aag thread \<and> integrity aag X st s\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err5 thread info ptr rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt5 thread info ptr rv\<rbrace> doE args <- liftE (get_mrs thread (snd (snd (snd rv))) info);
decode_invocation (mi_label info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err5 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then integrity aag X st and pas_refined aag and valid_objs and K (is_subject aag thread) else integrity aag X st\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B4 thread info ptr\<rbrace> 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 \<lbrace>?P_no_flt5 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then pas_refined aag and integrity aag X st and is_subject aag \<circ> cur_thread and invs and K (valid_fault ft) and K (is_subject aag thread) else integrity aag X st\<rbrace>
 5. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (liftM to_bl (as_user thread (getRegister cap_register))) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 7. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 8. \<And>s. (integrity aag X st and 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 and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. schact_is_rct st \<and> invs st \<and> pas_refined aag st \<and> guarded_pas_domain aag st \<and> domain_sep_inv (pasMaySendIrqs aag) st' st \<and> valid_list st \<and> is_subject aag (cur_thread st) \<and> ct_active st \<and> valid_sched st \<Longrightarrow> valid_arch_state st \<and> valid_vspace_objs st \<and> pspace_aligned st \<and> valid_objs st \<and> simple_sched_action st \<and> (blocking \<longrightarrow> valid_objs st) \<and> (calling \<longrightarrow> valid_objs st) \<and> ex_nonz_cap_to (cur_thread st) st \<and> st_tcb_at runnable (cur_thread st) st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'1001 (cur_thread st)) st \<and> st_tcb_at active (cur_thread st) st \<and> (\<not> calling \<longrightarrow> valid_arch_state st \<and> valid_vspace_objs st \<and> pspace_aligned st \<and> valid_objs st \<and> simple_sched_action st \<and> ex_nonz_cap_to (cur_thread st) st \<and> st_tcb_at runnable (cur_thread st) st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'1002 (cur_thread st)) st \<and> st_tcb_at active (cur_thread st) st) \<and> (calling \<longrightarrow> valid_arch_state st \<and> valid_vspace_objs st \<and> pspace_aligned st \<and> valid_objs st \<and> simple_sched_action st \<and> ex_nonz_cap_to (cur_thread st) st \<and> st_tcb_at runnable (cur_thread st) st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'1003 (cur_thread st)) st \<and> pas_cur_domain aag st \<and> st_tcb_at active (cur_thread st) st)