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 recycle_cap_ext)
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[wp]: set_mcpriority truncate_state
32
33lemma invoke_tcb_bcorres[wp]:
34  fixes a
35  shows "bcorres (invoke_tcb a) (invoke_tcb a)"
36  apply (cases a)
37        apply (wp | wpc | simp)+
38  apply (rename_tac option)
39  apply (case_tac option)
40   apply (wp | wpc | simp)+
41  done
42
43lemma transfer_caps_loop_bcorres[wp]:
44 "bcorres (transfer_caps_loop ep buffer n caps slots mi) (transfer_caps_loop ep buffer n caps slots mi)"
45  apply (induct caps arbitrary: slots n mi ep)
46   apply simp
47   apply wp
48  apply (case_tac a)
49  apply simp
50  apply (intro impI conjI)
51             apply (wp | simp)+
52  done
53
54lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_irq_control a)"
55  apply (cases a)
56  apply (wp | simp add: arch_invoke_irq_control_def)+
57  done
58
59lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
60  apply (cases a)
61  apply (wp | simp)+
62  done
63
64crunch (bcorres)bcorres[wp]: send_ipc,send_signal,do_reply_transfer,arch_perform_invocation truncate_state
65  (simp: gets_the_def swp_def ignore: freeMemory clearMemory get_register loadWord cap_fault_on_failure
66         set_register storeWord lookup_error_on_failure getRestartPC getRegister mapME)
67
68lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)"
69  apply (cases c)
70  apply (wp | wpc | simp)+
71  done
72
73lemma decode_cnode_invocation[wp]: "bcorres (decode_cnode_invocation a b c d) (decode_cnode_invocation a b c d)"
74  apply (simp add: decode_cnode_invocation_def)
75  apply (wp | wpc | simp add: split_def | intro impI conjI)+
76  done
77
78crunch (bcorres)bcorres[wp]:
79  decode_set_ipc_buffer,decode_set_space,decode_set_priority,decode_set_mcpriority,
80  decode_bind_notification,decode_unbind_notification truncate_state
81
82lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
83     (decode_tcb_configure b (cap.ThreadCap c) d e)"
84  apply (simp add: decode_tcb_configure_def | wp)+
85  done
86
87lemma 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)"
88  apply (simp add: decode_tcb_invocation_def)
89  apply (wp | wpc | simp)+
90  done
91
92lemma create_mapping_entries_bcorres[wp]: "bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)"
93  apply (cases c)
94  apply (wp | simp)+
95  done
96
97lemma ensure_safe_mapping_bcorres[wp]: "bcorres (ensure_safe_mapping a) (ensure_safe_mapping a)"
98  apply (induct rule: ensure_safe_mapping.induct)
99  apply (wp | wpc | simp)+
100  done
101
102crunch (bcorres)bcorres[wp]: handle_invocation truncate_state
103  (simp: syscall_def Let_def gets_the_def ignore: get_register syscall cap_fault_on_failure
104         set_register without_preemption const_on_failure)
105
106crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap truncate_state
107
108lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)"
109  apply (cases b)
110  apply (simp | wp)+
111  done
112
113lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)"
114  apply (cases e)
115  apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def handle_interrupt_def Let_def | intro impI conjI allI | wp | wpc)+
116  done
117
118crunch (bcorres)bcorres[wp]: guarded_switch_to,switch_to_idle_thread truncate_state (ignore: storeWord clearExMonitor)
119
120lemma choose_switch_or_idle:
121  "((), s') \<in> fst (choose_thread s) \<Longrightarrow>
122       (\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
123       ((),s') \<in> fst (switch_to_idle_thread s)"
124  apply (simp add: choose_thread_def)
125  apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
126                   arch_switch_to_idle_thread_def in_monad
127                   return_def get_def modify_def put_def
128                    get_thread_state_def
129                   thread_get_def
130                   split: split_if_asm)
131  apply force
132  done
133
134end
135
136end
137