theory Syscall_AC

lemma call_kernel_integrity:
  "\<lbrace>pas_refined aag and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle)
                    and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct
                    and guarded_pas_domain aag and is_subject aag o cur_thread
                    and K (pasMayActivate aag \<and> pasMayEditReadyQueues aag) and (\<lambda>s. s = st)\<rbrace>
   call_kernel ev
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" using call_kernel_integrity' [of st st' ev X] apply (simp add: spec_valid_def) apply (erule hoare_chain) apply clarsimp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct and guarded_pas_domain aag and is_subject aag \<circ> cur_thread and K (pasMayActivate aag \<and> pasMayEditReadyQueues aag) and (\<lambda>s. s = st)\<rbrace> call_kernel ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
using this:
st \<turnstile> \<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and schact_is_rct and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and K (pasMayActivate aag \<and> pasMayEditReadyQueues aag)\<rbrace> call_kernel ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace>

goal (1 subgoal):
 1. \<lbrace>pas_refined aag and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct and guarded_pas_domain aag and is_subject aag \<circ> cur_thread and K (pasMayActivate aag \<and> pasMayEditReadyQueues aag) and (\<lambda>s. s = st)\<rbrace> call_kernel ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = st \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> schact_is_rct s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) st' s \<and> (ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_active s \<or> ct_idle s) \<and> pasMayActivate aag \<and> pasMayEditReadyQueues aag\<rbrace> call_kernel ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> \<Longrightarrow> \<lbrace>pas_refined aag and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct and guarded_pas_domain aag and is_subject aag \<circ> cur_thread and (\<lambda>y. pasMayActivate aag \<and> pasMayEditReadyQueues aag) and (\<lambda>s. s = st)\<rbrace> call_kernel ev \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (pas_refined aag and einvs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) and domain_sep_inv (pasMaySendIrqs aag) st' and schact_is_rct and guarded_pas_domain aag and is_subject aag \<circ> cur_thread and (\<lambda>y. pasMayActivate aag \<and> pasMayEditReadyQueues aag) and (\<lambda>s. s = st)) s \<Longrightarrow> s = st \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> pas_refined aag s \<and> is_subject aag (cur_thread s) \<and> schact_is_rct s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) st' s \<and> (ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> (ct_active s \<or> ct_idle s) \<and> pasMayActivate aag \<and> pasMayEditReadyQueues aag
 2. \<And>rv s. integrity aag X st s \<Longrightarrow> integrity aag X st s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. integrity aag X st s \<Longrightarrow> integrity aag X st s proof (prove)
goal:
No subgoals!