1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7theory Interrupt_AC
8imports
9  Finalise_AC
10begin
11
12context begin interpretation Arch . (*FIXME: arch_split*)
13
14definition
15  arch_authorised_irq_ctl_inv :: "'a PAS \<Rightarrow> Invocations_A.arch_irq_control_invocation \<Rightarrow> bool"
16where
17  "arch_authorised_irq_ctl_inv aag cinv \<equiv>
18     case cinv of
19         (ArchIRQControlIssue irq x1 x2 trigger) \<Rightarrow>
20                                 is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and>
21                                 (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag"
22
23definition
24  authorised_irq_ctl_inv :: "'a PAS \<Rightarrow> Invocations_A.irq_control_invocation \<Rightarrow> bool"
25where
26  "authorised_irq_ctl_inv aag cinv \<equiv>
27     case cinv of
28         IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and>
29                                  (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag
30        | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv"
31
32lemma arch_invoke_irq_control_pas_refined:
33  "\<lbrace>pas_refined aag and valid_mdb and arch_irq_control_inv_valid irq_ctl_inv and
34     K (arch_authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
35     arch_invoke_irq_control irq_ctl_inv
36   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
37  apply (cases irq_ctl_inv; simp)
38  apply (wpsimp wp: cap_insert_pas_refined_not_transferable)
39  apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
40                        arch_authorised_irq_ctl_inv_def aag_cap_auth_def
41                        arch_irq_control_inv_valid_def)
42  done
43
44lemma invoke_irq_control_pas_refined:
45  "\<lbrace>pas_refined aag and valid_mdb and irq_control_inv_valid irq_ctl_inv
46      and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
47     invoke_irq_control irq_ctl_inv
48   \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
49  apply (cases irq_ctl_inv; simp)
50  apply (wpsimp wp: cap_insert_pas_refined_not_transferable)
51   apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
52                         authorised_irq_ctl_inv_def aag_cap_auth_def)
53  apply (wp arch_invoke_irq_control_pas_refined)
54  apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
55                        authorised_irq_ctl_inv_def aag_cap_auth_def)
56  done
57
58definition
59  authorised_irq_hdl_inv :: "'a PAS \<Rightarrow> Invocations_A.irq_handler_invocation \<Rightarrow> bool"
60where
61  "authorised_irq_hdl_inv aag hinv \<equiv>
62     case hinv of
63         irq_handler_invocation.SetIRQHandler word cap x \<Rightarrow>
64                   is_subject aag (fst x) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag word
65       | irq_handler_invocation.ClearIRQHandler word     \<Rightarrow> is_subject_irq aag word
66       | _                                               \<Rightarrow> True"
67
68lemma emptyable_irq_node:
69  "emptyable (interrupt_irq_node s x21, []) s"
70  by (simp add:emptyable_def tcb_cnode_index_def)
71
72lemma pas_refined_is_subject_irqD:
73  "\<lbrakk>is_subject_irq aag irq ; pas_refined aag s \<rbrakk> \<Longrightarrow> is_subject aag (interrupt_irq_node s irq)"
74  by (simp add:pas_refined_def irq_map_wellformed_aux_def)
75
76lemma invoke_irq_handler_pas_refined:
77  "\<lbrace>pas_refined aag and invs and irq_handler_inv_valid irq_inv
78       and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace>
79     invoke_irq_handler irq_inv
80   \<lbrace>\<lambda>rv (s::det_ext state). pas_refined aag s\<rbrace>"
81  apply (rule hoare_gen_asm)
82  apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def)
83    apply (wp cap_insert_pas_refined_not_transferable delete_one_caps_of_state
84          | strengthen invs_mdb aag_Control_owns_strg
85          | simp add: pas_refined_wellformed cte_wp_at_caps_of_state)+
86    apply (rename_tac irq cap slot)
87    apply (rule_tac Q =
88            "\<lambda> irq_slot. K(irq_slot \<noteq> slot) and invs and emptyable irq_slot
89                     and cte_wp_at can_fast_finalise irq_slot
90                     and not cte_wp_at is_transferable_cap slot
91                     and K(is_subject aag (fst irq_slot))" in hoare_post_imp)
92     apply (force simp: cte_wp_at_caps_of_state)
93    apply simp
94    apply (wp get_irq_slot_different)
95
96   apply (clarsimp simp: emptyable_irq_node cte_wp_at_caps_of_state)
97   apply (fastforce simp: interrupt_derived_def is_cap_simps cap_master_cap_def split: cap.splits)
98  apply (wp delete_one_caps_of_state | simp add: get_irq_slot_def)+
99  apply (fastforce dest: pas_refined_is_subject_irqD)
100  done
101
102
103lemma invoke_irq_control_respects:
104  "\<lbrace>integrity aag X st and pas_refined aag and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
105     invoke_irq_control irq_ctl_inv
106   \<lbrace>\<lambda>y. integrity aag X st\<rbrace>"
107  apply (rule hoare_gen_asm)
108  apply (cases irq_ctl_inv)
109  subgoal \<comment>\<open>generic case\<close>
110    apply (simp add: authorised_irq_ctl_inv_def)
111    apply (wp cap_insert_integrity_autarch aag_Control_into_owns_irq | simp | blast)+
112    done
113  subgoal for arch_irq_ctl_inv \<comment>\<open>arch case\<close>
114    apply (simp add: arch_authorised_irq_ctl_inv_def authorised_irq_ctl_inv_def)
115    apply (case_tac arch_irq_ctl_inv, clarsimp simp add: setIRQTrigger_def)
116    apply (wp cap_insert_integrity_autarch aag_Control_into_owns_irq dmo_mol_respects do_machine_op_pas_refined | simp)+
117    apply auto
118    done
119  done
120
121lemma integrity_irq_masks [iff]:
122  "integrity aag X st (s\<lparr>machine_state := machine_state s \<lparr>irq_masks := v \<rparr>\<rparr>) = integrity aag X st s"
123  unfolding integrity_def
124  by simp
125
126lemma invoke_irq_handler_respects:
127  "\<lbrace>integrity aag X st and pas_refined aag and einvs and
128       K (authorised_irq_hdl_inv aag irq_inv)\<rbrace>
129     invoke_irq_handler irq_inv
130   \<lbrace>\<lambda>y. integrity aag X st\<rbrace>"
131  apply (rule hoare_gen_asm)
132  apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def)
133  apply (rule hoare_pre)
134  apply (wp cap_insert_integrity_autarch get_irq_slot_owns dmo_wp | simp add: maskInterrupt_def )+
135  done
136
137lemma decode_irq_control_invocation_authorised [wp]:
138  "\<lbrace>pas_refined aag
139      and K (is_subject aag (fst slot)
140              \<and> (\<forall>cap \<in> set caps. pas_cap_cur_auth aag cap)
141              \<and> (args \<noteq> [] \<longrightarrow>
142                  (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
143    decode_irq_control_invocation info_label args slot caps
144  \<lbrace>\<lambda>x s. authorised_irq_ctl_inv aag x\<rbrace>, -"
145  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def
146  apply (rule hoare_gen_asmE)
147  apply (rule hoare_pre)
148   apply (simp add: Let_def split del: if_split cong: if_cong)
149   apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
150         | strengthen  aag_Control_owns_strg
151         | simp add: o_def del: hoare_True_E_R)+
152  apply (cases args, simp_all)
153  apply (cases caps, simp_all)
154  apply (simp add: ucast_mask_drop)
155  apply (auto simp: is_cap_simps cap_auth_conferred_def
156                    pas_refined_wellformed
157                    pas_refined_all_auth_is_owns aag_cap_auth_def)
158  done
159
160lemma decode_irq_handler_invocation_authorised [wp]:
161  "\<lbrace>K (is_subject_irq aag irq
162         \<and> (\<forall>cap_slot \<in> set caps. pas_cap_cur_auth aag (fst cap_slot)
163                                \<and> is_subject aag (fst (snd cap_slot))))\<rbrace>
164    decode_irq_handler_invocation info_label irq caps
165  \<lbrace>\<lambda>x s. authorised_irq_hdl_inv aag x\<rbrace>, -"
166  unfolding decode_irq_handler_invocation_def authorised_irq_hdl_inv_def
167  apply (rule hoare_pre)
168   apply (simp add: Let_def split_def split del: if_split cong: if_cong)
169   apply wp
170  apply (auto dest!: hd_in_set)
171  done
172
173end
174
175end
176