theory Syscall_IF

lemma invoke_cnode_reads_respects_f_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_f_g aag l
           (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs
                            and simple_sched_action and valid_cnode_inv ci
                            and (\<lambda>s. is_subject aag (cur_thread s))
                            and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci)
           (invoke_cnode ci)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f_g) apply (rule invoke_cnode_reads_respects_f[where st=st, OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp invoke_cnode_globals_equiv) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) (invoke_cnode ci) proof (prove)
goal (2 subgoals):
 1. reads_respects_f_g aag l ?Q (invoke_cnode ci)
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P3 (invoke_cnode ci)
 2. doesnt_touch_globals ?Q3 (invoke_cnode ci)
 3. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (invoke_cnode ci)
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> (silc_inv aag st and only_timer_irq_inv ?irq6 ?st'6 and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> (silc_inv aag st and only_timer_irq_inv ?irq6 ?st'6 and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q3) s \<Longrightarrow> (globals_equiv st and invs and valid_cnode_inv ci) s
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> (silc_inv aag st and only_timer_irq_inv ?irq6 ?st'6 and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci and ?Q3) s proof (prove)
goal:
No subgoals!