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