theory Syscall_AC

lemma call_kernel_pas_refined:
  "\<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag
          and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle)
          and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
   call_kernel ev
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (simp add: call_kernel_def ) apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined
            do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv
         | simp add: if_fun_split
         | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ apply (wp he_invs handle_event_pas_refined) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> call_kernel ev \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> do y <- handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> handle_event ev \<lbrace>\<lambda>r s. pas_refined aag s \<and> invs s\<rbrace>, \<lbrace>\<lambda>r s. pas_refined aag s \<and> invs s \<and> pas_refined aag s \<and> invs s\<rbrace>
 2. \<And>s. (einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st') s \<Longrightarrow> (pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) ?st'74 and einvs and schact_is_rct and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<and> (invs s \<and> (ev \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> (pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) ?st'78 and einvs and schact_is_rct and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<and> (invs s \<and> (ev \<noteq> Interrupt \<longrightarrow> ct_active s)) \<and> (pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) ?st'82 and einvs and schact_is_rct and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)) s \<and> invs s \<and> (ev \<noteq> Interrupt \<longrightarrow> ct_active s) proof (prove)
goal:
No subgoals!