1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8 * Toplevel capDL refinement theorem.
9 *)
10
11theory Refine_D
12imports Syscall_DR
13begin
14
15context begin interpretation Arch . (*FIXME: arch_split*)
16
17text \<open>
18  Toplevel @{text dcorres} theorem.
19\<close>
20
21lemma valid_etcbs_sched: "valid_sched s \<longrightarrow> valid_etcbs s" by (fastforce simp: valid_sched_def)
22
23lemma handle_event_invs_and_valid_sched:
24  "\<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)
25      and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> Syscall_A.handle_event e
26  \<lbrace>\<lambda>rv. invs and valid_sched\<rbrace>"
27  by ((wp he_invs handle_event_valid_sched), clarsimp)
28
29lemma dcorres_call_kernel:
30  "dcorres dc \<top>
31          (invs and valid_sched and valid_pdpt_objs
32             and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)
33             and  (\<lambda>s. scheduler_action s = resume_cur_thread))
34          (Syscall_D.call_kernel e) (Syscall_A.call_kernel e)"
35  apply (simp_all add: Syscall_D.call_kernel_def Syscall_A.call_kernel_def)
36  apply (rule corres_guard_imp)
37    apply (rule corres_split)
38       prefer 2
39       apply (rule corres_split_handle [OF _ handle_event_corres])
40         prefer 4
41         apply (subst bind_return[symmetric])
42         apply (rule corres_split)
43            apply (rule activate_thread_corres[unfolded fun_app_def])
44           apply simp
45           apply (rule schedule_dcorres)
46          apply (wp schedule_valid_sched | strengthen valid_etcbs_sched)+
47        apply (simp add: handle_pending_interrupts_def)
48        apply (rule corres_split [OF _ get_active_irq_corres])
49          apply (clarsimp simp: when_def split: option.splits)
50          apply (rule handle_interrupt_corres[simplified dc_def])
51         apply ((wp | simp)+)[3]
52      apply (rule hoare_post_imp_dc2E, rule handle_event_invs_and_valid_sched)
53      apply (clarsimp simp: invs_def valid_state_def)
54     apply (simp add: conj_comms if_apply_def2 non_kernel_IRQs_def
55            | wp | strengthen valid_etcbs_sched valid_idle_invs_strg)+
56    apply (rule valid_validE2)
57      apply (rule hoare_vcg_conj_lift)
58       apply (rule he_invs)
59      apply (rule handle_event_valid_sched)
60     apply (fastforce intro: active_from_running simp: valid_sched_def)+
61  done
62
63end
64
65end
66