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