1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 *)
10
11theory ArchBCorres2_AI
12imports
13  "../BCorres2_AI"
14begin
15
16context Arch begin global_naming ARM
17
18named_theorems BCorres2_AI_assms
19
20crunch (bcorres)bcorres[wp, BCorres2_AI_assms]: invoke_cnode truncate_state
21  (simp: swp_def ignore: clearMemory without_preemption filterM ethread_set)
22
23crunch (bcorres)bcorres[wp]: create_cap,init_arch_objects,retype_region,delete_objects truncate_state
24  (ignore: freeMemory clearMemory retype_region_ext)
25
26crunch (bcorres)bcorres[wp]: set_extra_badge,derive_cap truncate_state (ignore: storeWord)
27
28crunch (bcorres)bcorres[wp]: invoke_untyped truncate_state
29  (ignore: sequence_x)
30
31crunch (bcorres)bcorres[BCorres2_AI_assms,wp]: set_mcpriority, arch_tcb_set_ipc_buffer,
32          arch_get_sanitise_register_info, arch_post_modify_registers truncate_state
33
34lemma invoke_tcb_bcorres[wp]:
35  fixes a
36  shows "bcorres (invoke_tcb a) (invoke_tcb a)"
37  apply (cases a)
38        apply (wp | wpc | simp)+
39  apply (rename_tac option)
40  apply (case_tac option)
41   apply (wp | wpc | simp)+
42  done
43
44lemma transfer_caps_loop_bcorres[wp]:
45 "bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)"
46  apply (induct caps arbitrary: slots n mi ep)
47   apply simp
48   apply wp
49  apply (case_tac a)
50  apply simp
51  apply (intro impI conjI)
52             apply (wp | simp)+
53  done
54
55lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)"
56  apply (cases a)
57  apply wpsimp
58  apply (rename_tac acap)
59  apply (case_tac acap)
60  apply wpsimp
61  done
62
63lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
64  apply (cases a)
65  apply (wp | simp)+
66  done
67
68lemma make_arch_fault_msg_bcorres[wp,BCorres2_AI_assms]:
69  "bcorres (make_arch_fault_msg a b) (make_arch_fault_msg a b)"
70  by (cases a; wpsimp)
71
72lemma  handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
73  "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
74  by (cases a; wpsimp simp: handle_arch_fault_reply_def)
75
76crunch (bcorres)bcorres[wp, BCorres2_AI_assms]:
77    arch_switch_to_thread,arch_switch_to_idle_thread truncate_state
78
79end
80
81interpretation BCorres2_AI?: BCorres2_AI
82  proof goal_cases
83  interpret Arch .
84  case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?)
85  qed
86
87lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
88
89context Arch begin global_naming ARM
90
91crunch (bcorres)bcorres[wp]: send_signal,arch_perform_invocation truncate_state
92
93crunch (bcorres)bcorres[wp]: send_ipc truncate_state
94  (simp: ignore: getRegister mapME cap_fault_on_failure)
95
96crunch (bcorres)bcorres[wp]: do_reply_transfer truncate_state
97
98lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)"
99  apply (cases c)
100  apply (wp | wpc | simp)+
101  done
102
103lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d)"
104  apply (simp add: decode_cnode_invocation_def)
105  apply (wp | wpc | simp add: split_def | intro impI conjI)+
106  done
107
108crunch (bcorres)bcorres[wp]:
109  decode_set_ipc_buffer, decode_set_space, decode_set_priority,
110  decode_set_mcpriority, decode_set_sched_params, decode_bind_notification,
111  decode_unbind_notification, decode_set_tls_base truncate_state
112
113lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
114     (decode_tcb_configure b (cap.ThreadCap c) d e)"
115  apply (simp add: decode_tcb_configure_def | wp)+
116  done
117
118lemma decode_tcb_invocation_bcorres[wp]:"bcorres (decode_tcb_invocation a b (cap.ThreadCap c) d e) (decode_tcb_invocation a b (cap.ThreadCap c) d e)"
119  apply (simp add: decode_tcb_invocation_def)
120  apply (wp | wpc | simp)+
121  done
122
123lemma create_mapping_entries_bcorres[wp]: "bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)"
124  apply (cases c)
125  apply (wp | simp)+
126  done
127
128lemma ensure_safe_mapping_bcorres[wp]: "bcorres (ensure_safe_mapping a) (ensure_safe_mapping a)"
129  apply (induct rule: ensure_safe_mapping.induct)
130  apply (wp | wpc | simp)+
131  done
132
133crunch (bcorres)bcorres[wp]: handle_invocation truncate_state
134  (simp: syscall_def Let_def gets_the_def
135   ignore: syscall cap_fault_on_failure without_preemption
136           const_on_failure decode_tcb_invocation)
137
138crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap truncate_state
139
140lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)"
141  apply (cases b)
142  apply (simp | wp)+
143  done
144
145lemma vgic_maintenance_bcorres[wp]:
146  "bcorres vgic_maintenance vgic_maintenance"
147  unfolding vgic_maintenance_def
148  by (wpsimp simp: vgic_update_lr_bcorres)
149
150lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)"
151  unfolding handle_reserved_irq_def by wpsimp
152
153lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)"
154  apply (cases b)
155  apply (simp | wp)+
156  done
157
158lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
159  apply (cases e)
160  apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def handle_interrupt_def
161                   handle_reserved_irq_def handle_hypervisor_fault.simps Let_def | intro impI conjI allI | wp | wpc)+
162  done
163
164crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor)
165
166lemma choose_switch_or_idle:
167  "((), s') \<in> fst (choose_thread s) \<Longrightarrow>
168       (\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
169       ((),s') \<in> fst (switch_to_idle_thread s)"
170  apply (simp add: choose_thread_def)
171  apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
172                   arch_switch_to_idle_thread_def in_monad
173                   return_def get_def modify_def put_def
174                    get_thread_state_def
175                   thread_get_def
176                   split: if_split_asm)
177  apply force
178  done
179
180end
181
182end
183