1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8 * Toplevel capDL refinement theorem. 9 *) 10 11theory Refine_D 12imports Syscall_DR 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17text \<open> 18 Toplevel @{text dcorres} theorem. 19\<close> 20 21lemma valid_etcbs_sched: "valid_sched s \<longrightarrow> valid_etcbs s" by (fastforce simp: valid_sched_def) 22 23lemma handle_event_invs_and_valid_sched: 24 "\<lbrace>invs and valid_sched and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) 25 and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> Syscall_A.handle_event e 26 \<lbrace>\<lambda>rv. invs and valid_sched\<rbrace>" 27 by ((wp he_invs handle_event_valid_sched), clarsimp) 28 29lemma dcorres_call_kernel: 30 "dcorres dc \<top> 31 (invs and valid_sched and valid_pdpt_objs 32 and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) 33 and (\<lambda>s. scheduler_action s = resume_cur_thread)) 34 (Syscall_D.call_kernel e) (Syscall_A.call_kernel e)" 35 apply (simp_all add: Syscall_D.call_kernel_def Syscall_A.call_kernel_def) 36 apply (rule corres_guard_imp) 37 apply (rule corres_split) 38 prefer 2 39 apply (rule corres_split_handle [OF _ handle_event_corres]) 40 prefer 4 41 apply (subst bind_return[symmetric]) 42 apply (rule corres_split) 43 apply (rule activate_thread_corres[unfolded fun_app_def]) 44 apply simp 45 apply (rule schedule_dcorres) 46 apply (wp schedule_valid_sched | strengthen valid_etcbs_sched)+ 47 apply (simp add: handle_pending_interrupts_def) 48 apply (rule corres_split [OF _ get_active_irq_corres]) 49 apply (clarsimp simp: when_def split: option.splits) 50 apply (rule handle_interrupt_corres[simplified dc_def]) 51 apply ((wp | simp)+)[3] 52 apply (rule hoare_post_imp_dc2E, rule handle_event_invs_and_valid_sched) 53 apply (clarsimp simp: invs_def valid_state_def) 54 apply (simp add: conj_comms if_apply_def2 non_kernel_IRQs_def 55 | wp | strengthen valid_etcbs_sched valid_idle_invs_strg)+ 56 apply (rule valid_validE2) 57 apply (rule hoare_vcg_conj_lift) 58 apply (rule he_invs) 59 apply (rule handle_event_valid_sched) 60 apply (fastforce intro: active_from_running simp: valid_sched_def)+ 61 done 62 63end 64 65end 66