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 ArchSchedule_AI
12imports "../Schedule_AI"
13begin
14
15context Arch begin global_naming ARM
16
17named_theorems Schedule_AI_asms
18
19lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]:
20  "valid invs (do_machine_op (mapM (\<lambda>p. storeWord p 0) S)) (\<lambda>_. invs)"
21  apply (simp add: dom_mapM ef_storeWord)
22  apply (rule mapM_UNIV_wp)
23  apply (simp add: do_machine_op_def split_def)
24  apply wp
25  apply (clarsimp simp: invs_def valid_state_def cur_tcb_def
26                        valid_machine_state_def)
27  apply (rule conjI)
28   apply(erule use_valid[OF _ storeWord_valid_irq_states], simp)
29  apply (erule use_valid)
30   apply (simp add: storeWord_def word_rsplit_0)
31   apply wp
32  apply simp
33  done
34
35crunch device_state_inv[wp]: clearExMonitor "\<lambda>ms. P (device_state ms)"
36
37lemma clearExMonitor_invs [wp]:
38  "\<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace>"
39  apply (wp dmo_invs)
40  apply (clarsimp simp: clearExMonitor_def machine_op_lift_def
41                        machine_rest_lift_def in_monad select_f_def)
42  done
43
44global_naming Arch
45
46lemma arch_stt_invs [wp,Schedule_AI_asms]:
47  "\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
48  apply (simp add: arch_switch_to_thread_def)
49  apply wp
50  done
51
52lemma arch_stt_tcb [wp,Schedule_AI_asms]:
53  "\<lbrace>tcb_at t'\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. tcb_at t'\<rbrace>"
54  apply (simp add: arch_switch_to_thread_def)
55  apply (wp)
56  done
57
58lemma arch_stt_runnable[Schedule_AI_asms]:
59  "\<lbrace>st_tcb_at runnable t\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>r . st_tcb_at runnable t\<rbrace>"
60  apply (simp add: arch_switch_to_thread_def)
61  apply wp
62  done
63
64lemma arch_stit_invs[wp, Schedule_AI_asms]:
65  "\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>"
66  by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def)
67
68lemma arch_stit_tcb_at[wp]:
69  "\<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace>"
70  apply (simp add: arch_switch_to_idle_thread_def )
71  apply wp
72  done
73
74crunch st_tcb_at[wp]: set_vm_root "st_tcb_at P t"
75  (wp: crunch_wps simp: crunch_simps)
76
77crunch ct[wp]: set_vm_root "\<lambda>s. P (cur_thread s)"
78  (wp: crunch_wps simp: crunch_simps)
79
80lemma arch_stit_activatable[wp, Schedule_AI_asms]:
81  "\<lbrace>ct_in_state activatable\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
82  apply (clarsimp simp: arch_switch_to_idle_thread_def)
83  apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift)
84  done
85
86lemma stit_invs [wp,Schedule_AI_asms]:
87  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. invs\<rbrace>"
88  apply (simp add: switch_to_idle_thread_def)
89  apply (wp sct_invs)
90  by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def
91                     pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def)
92
93lemma stit_activatable[Schedule_AI_asms]:
94  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
95  apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def)
96  apply (wp | simp add: ct_in_state_def)+
97  apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_idle_def
98                 elim!: pred_tcb_weaken_strongerE)
99  done
100
101lemma stt_invs [wp,Schedule_AI_asms]:
102  "\<lbrace>invs\<rbrace> switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
103  apply (simp add: switch_to_thread_def)
104  apply wp
105     apply (simp add: trans_state_update[symmetric] del: trans_state_update)
106    apply (rule_tac Q="\<lambda>_. invs and tcb_at t'" in hoare_strengthen_post, wp)
107    apply (clarsimp simp: invs_def valid_state_def valid_idle_def
108                          valid_irq_node_def valid_machine_state_def)
109    apply (fastforce simp: cur_tcb_def obj_at_def
110                     elim: valid_pspace_eqI ifunsafe_pspaceI)
111   apply wp+
112  apply clarsimp
113  apply (simp add: is_tcb_def)
114  done
115end
116
117interpretation Schedule_AI_U?: Schedule_AI_U
118  proof goal_cases
119  interpret Arch .
120  case 1 show ?case
121  by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?)
122  qed
123
124interpretation Schedule_AI?: Schedule_AI
125  proof goal_cases
126  interpret Arch .
127  case 1 show ?case
128  by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?)
129  qed
130
131end
132