1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11(* 12 * Theorems linking the L4.verified proofs to our own framework; 13 * typically showing that we prove equivalent results as a sanity 14 * check. 15 *) 16 17theory L4VerifiedLinks 18imports 19 "AutoCorres.AutoCorres" 20 "CLib.Corres_UL_C" 21begin 22 23(* 24 * The ccorresE framework implies the ccorres framework. 25 *) 26lemma ccorresE_ccorres_underlying: 27 "\<lbrakk> ccorresE st check_termination \<Gamma> G G' A B; \<not> exceptions_thrown B \<rbrakk> \<Longrightarrow> 28 ccorres_underlying {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) dc (\<lambda>_. ()) G G' [] A B" 29 apply (clarsimp simp: ccorres_underlying_def dc_def) 30 apply (clarsimp simp: ccorresE_def) 31 apply (erule allE, erule impE, force) 32 apply (erule exec_handlers.cases, simp_all) 33 apply clarsimp 34 apply (frule exceptions_thrown_not_abrupt, simp_all)[1] 35 apply (clarsimp split: xstate.splits) 36 apply (erule allE, erule conjE, erule impE, assumption) 37 apply (clarsimp simp: unif_rrel_def isAbr_def split: xstate.splits) 38 apply (case_tac ta, simp_all) 39 apply (rule bexI [rotated], assumption) 40 apply simp 41 done 42 43(* 44 * The ccorresE framework implies the ccorres framework. 45 *) 46lemma ccorresE_ccorres_underlying': 47 "\<lbrakk> ccorresE st check_termination \<Gamma> G G' A B; no_throw G A \<rbrakk> \<Longrightarrow> 48 ccorres_underlying {(s', s). s' = st s} \<Gamma> dc (\<lambda>_. ()) dc (\<lambda>_. ()) G G' [] A B" 49 apply (clarsimp simp: ccorres_underlying_def dc_def) 50 apply (clarsimp simp: ccorresE_def) 51 apply (erule allE, erule impE, force) 52 apply (erule exec_handlers.cases, simp_all) 53 apply clarsimp 54 apply (erule_tac allE, erule (1) impE) 55 apply clarsimp 56 apply (drule (1) no_throw_Inr) 57 apply fastforce 58 apply fastforce 59 apply (clarsimp split: xstate.splits) 60 apply (erule allE, erule conjE, erule impE, assumption) 61 apply (clarsimp simp: unif_rrel_def isAbr_def split: xstate.splits) 62 apply (case_tac ta, simp_all) 63 apply (rule bexI [rotated], assumption) 64 apply simp 65 done 66 67lemma ac_corres_ccorres_underlying: 68 "ac_corres st check_termination \<Gamma> rx G A B \<Longrightarrow> 69 ccorres_underlying {(a, b). a = st b} \<Gamma> ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr ((\<lambda>_ _. False) \<oplus> (\<lambda>r s. r = rx s)) Inr (\<lambda>_. True) (Collect G) [] A B" 70 apply (clarsimp simp: ac_corres_def ccorres_underlying_def) 71 apply (erule allE, erule impE, force) 72 apply clarsimp 73 apply (erule exec_handlers.cases) 74 apply clarsimp 75 apply (erule allE, erule (1) impE) 76 apply clarsimp 77 apply (case_tac hs) 78 apply clarsimp 79 apply (erule allE, erule (1) impE) 80 apply (clarsimp split: xstate.splits) 81 apply (erule bexI [rotated]) 82 apply (clarsimp simp: unif_rrel_def) 83 apply clarsimp 84 apply clarsimp 85 done 86 87(* 88 * The definition of corresXF and corres_underlying are equivalent, 89 * assuming we don't use the extraction functions. 90 *) 91lemma corres_impl_corresXF: 92 "corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G' \<Longrightarrow> 93 corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'" 94 apply (rule corresXF_I) 95 apply (clarsimp simp: corres_underlying_def corresXF_def) 96 apply (erule allE, erule (1) impE) 97 apply force 98 apply (clarsimp simp: corres_underlying_def corresXF_def) 99 apply (erule allE, erule (1) impE) 100 apply force 101 apply (clarsimp simp: corres_underlying_def corresXF_def) 102 done 103 104lemma corresXF_impl_corres: 105 "\<lbrakk> corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'; no_fail \<top> G \<rbrakk> \<Longrightarrow> 106 corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G'" 107 apply (clarsimp simp: corres_underlying_def corresXF_def no_fail_def) 108 apply (erule allE, erule (1) impE) 109 apply clarsimp 110 apply (erule (1) my_BallE) 111 apply (force split: sum.splits) 112 done 113 114end 115