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
11(*
12Refinement for handleEvent and syscalls
13*)
14
15theory ArchSyscall_AI
16imports
17  "../Syscall_AI"
18begin
19
20context Arch begin global_naming ARM
21
22named_theorems Syscall_AI_assms
23
24declare arch_get_sanitise_register_info_invs[Syscall_AI_assms]
25crunch pred_tcb_at[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "pred_tcb_at proj P t"
26crunch invs[wp,Syscall_AI_assms]: handle_arch_fault_reply "invs"
27crunch cap_to[wp,Syscall_AI_assms]: handle_arch_fault_reply  "ex_nonz_cap_to c"
28crunch it[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (idle_thread s)"
29crunch caps[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (caps_of_state s)"
30crunch cur_thread[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (cur_thread s)"
31crunch valid_objs[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "valid_objs"
32crunch cte_wp_at[wp,Syscall_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "\<lambda>s. P (cte_wp_at P' p s)"
33declare arch_get_sanitise_register_info_ex_nonz_cap_to[Syscall_AI_assms]
34        make_fault_message_inv[Syscall_AI_assms]
35
36
37crunch typ_at[wp, Syscall_AI_assms]: invoke_irq_control "\<lambda>s. P (typ_at T p s)"
38
39lemma obj_refs_cap_rights_update[simp, Syscall_AI_assms]:
40  "obj_refs (cap_rights_update rs cap) = obj_refs cap"
41  by (simp add: cap_rights_update_def acap_rights_update_def
42         split: cap.split arch_cap.split)
43
44(* FIXME: move to TCB *)
45lemma table_cap_ref_mask_cap [Syscall_AI_assms]:
46  "table_cap_ref (mask_cap R cap) = table_cap_ref cap"
47  by (clarsimp simp add:mask_cap_def table_cap_ref_def acap_rights_update_def
48    cap_rights_update_def split:cap.splits arch_cap.splits)
49
50lemma diminished_no_cap_to_obj_with_diff_ref [Syscall_AI_assms]:
51  "\<lbrakk> cte_wp_at (diminished cap) p s; valid_arch_caps s \<rbrakk>
52      \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s"
53  apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def)
54  apply (frule(1) unique_table_refs_no_cap_asidD)
55  apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def
56    table_cap_ref_mask_cap diminished_def Ball_def)
57  done
58
59lemma getDFSR_invs[wp]:
60  "valid invs (do_machine_op getDFSR) (\<lambda>_. invs)"
61  by (simp add: getDFSR_def do_machine_op_def split_def select_f_returns | wp)+
62
63lemma getFAR_invs[wp]:
64  "valid invs (do_machine_op getFAR) (\<lambda>_. invs)"
65  by (simp add: getFAR_def do_machine_op_def split_def select_f_returns | wp)+
66
67lemma getIFSR_invs[wp]:
68  "valid invs (do_machine_op getIFSR) (\<lambda>_. invs)"
69  by (simp add: getIFSR_def do_machine_op_def split_def select_f_returns | wp)+
70
71lemma hv_invs[wp, Syscall_AI_assms]: "\<lbrace>invs\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace>"
72  apply (cases flt, simp_all)
73  apply (wp|simp)+
74  done
75
76lemma handle_vm_fault_valid_fault[wp, Syscall_AI_assms]:
77  "\<lbrace>\<top>\<rbrace> handle_vm_fault thread ft -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>"
78  apply (cases ft, simp_all)
79   apply (wp no_irq_getDFSR no_irq_getIFSR| simp add: valid_fault_def)+
80  done
81
82lemma hvmf_active [Syscall_AI_assms]:
83  "\<lbrace>st_tcb_at active t\<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace>"
84  apply (cases w, simp_all)
85   apply (wp | simp)+
86  done
87
88lemma hvmf_ex_cap[wp, Syscall_AI_assms]:
89  "\<lbrace>ex_nonz_cap_to p\<rbrace> handle_vm_fault t b \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>"
90  apply (cases b, simp_all)
91   apply (wp | simp)+
92  done
93
94lemma hh_invs[wp, Syscall_AI_assms]:
95  "\<lbrace>invs and ct_active and st_tcb_at active thread and ex_nonz_cap_to thread\<rbrace>
96     handle_hypervisor_fault thread fault
97   \<lbrace>\<lambda>rv. invs\<rbrace>"
98  by (cases fault; wpsimp simp: valid_fault_def)
99
100end
101
102global_interpretation Syscall_AI?: Syscall_AI
103  proof goal_cases
104  interpret Arch .
105  case 1 show ?case by (unfold_locales; (fact Syscall_AI_assms)?)
106  qed
107
108end
109