Changeset 3007 for src/Cminor/toRTLabsCorrectness.ma
 Timestamp:
 Mar 28, 2013, 2:59:43 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabsCorrectness.ma
r2601 r3007 4 4 include "Cminor/toRTLabs.ma". 5 5 6 record cminor_rtlabs_inv : Type[0] ≝ { 7 ge_cm : cm_genv; 8 ge_ra : RTLabs_genv 6 record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ { 9 7 }. 10 axiom cminor_rtlabs_rel : cminor_rtlabs_inv → Cminor_state → RTLabs_state → Prop. 8 axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop. 9 10 axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'. 11 cminor_rtlabs_rel gc gr INV s s' → 12 Cminor_labelled s = RTLabs_cost s'. 11 13 12 14 (* Conjectured simulation results … … 14 16 We split these based on the start state: 15 17 16 1. ‘normal’ states take some [S n] normal steps and simulates them by [m]17 normal steps in RTLabs ([m] can be zero if the Cminor program executed an18 St_skip);19 2. call and return steps are simulated by a call/return step plus [m] normal20 steps (to copy stack allocated parameters / results);and18 1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs 19 ([n] can be zero if the Cminor program executed an St_skip); 20 2. call and return state steps are simulated by a call/return state step (we 21 don't add anything extra in this stage, it happens in Clight to Cminor); 22 and 21 23 3. lone cost label steps are simulates by a lone cost label step 24 25 Most of the work in this stage is splitting the execution of complex Cminor 26 statements into individual RTLabs steps. This doesn't contradict 2 above  27 the expansion of function parameters, return expressions, etc is done for 28 the function call / return *statement*, whereas the call / return *state* is 29 a Callstate / Returnstate that is the second half of the operation. 22 30 23 31 Note that we'll need something more to show that nontermination is … … 36 44 λs. match RTLabs_classify s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 37 45 46 axiom cminor_measure : Cminor_state → nat. 47 38 48 axiom cminor_rtlabs_normal : 39 ∀INV:cminor_rtlabs_inv. 49 ∀ge_cm,ge_ra. 50 ∀INV:cminor_rtlabs_inv ge_cm ge_ra. 40 51 ∀s1,s1',s2,tr. 41 cminor_rtlabs_rel INV s1 s1' →52 cminor_rtlabs_rel … INV s1 s1' → 42 53 cminor_normal s1 → 43 54 ¬ Cminor_labelled s1 → 44 ∃n. after_n_steps (S n) … Cminor_exec (ge_cm INV) s1 (λs.cminor_normal s ∧ ¬ Cminor_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)→45 ∃ m. after_n_steps m … RTLabs_exec (ge_ra INV)s1' (λs.rtlabs_normal s) (λtr',s2'.55 step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → 56 ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'. 46 57 tr = tr' ∧ 47 cminor_rtlabs_rel INV s2 s2' 58 (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧ 59 cminor_rtlabs_rel … INV s2 s2' 48 60 ). 49 61 50 62 axiom cminor_rtlabs_call_return : 51 ∀INV:cminor_rtlabs_inv. 63 ∀ge_cm,ge_ra. 64 ∀INV:cminor_rtlabs_inv ge_cm ge_ra. 52 65 ∀s1,s1',s2,tr. 53 cminor_rtlabs_rel INV s1 s1' →66 cminor_rtlabs_rel … INV s1 s1' → 54 67 match Cminor_classify s1 with [ cl_call ⇒ true  cl_return ⇒ true  _ ⇒ false ] → 55 after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)→56 ∃m. after_n_steps (S m) … RTLabs_exec (ge_ra INV)s1' (λs.rtlabs_normal s) (λtr',s2'.68 step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → 69 after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'. 57 70 tr = tr' ∧ 58 cminor_rtlabs_rel INV s2 s2'71 cminor_rtlabs_rel … INV s2 s2' 59 72 ). 60 73 61 74 axiom cminor_rtlabs_cost : 62 ∀INV:cminor_rtlabs_inv. 75 ∀ge_cm,ge_ra. 76 ∀INV:cminor_rtlabs_inv ge_cm ge_ra. 63 77 ∀s1,s1',s2,tr. 64 cminor_rtlabs_rel INV s1 s1' →78 cminor_rtlabs_rel … INV s1 s1' → 65 79 Cminor_labelled s1 → 66 after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)→67 after_n_steps 1 … RTLabs_exec (ge_ra INV)s1' (λs.true) (λtr',s2'.80 step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → 81 after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'. 68 82 tr = tr' ∧ 69 cminor_rtlabs_rel INV s2 s2'83 cminor_rtlabs_rel … INV s2 s2' 70 84 ). 71 85 72 (* Note that we start from the "no initialisation" version of the Cminor 73 semantics. I plan to prove the initialisation generation separately. *) 86 axiom cminor_rtlabs_init : 87 ∀p,s. 88 make_initial_state … Cminor_fullexec p = OK … s → 89 let p' ≝ cminor_to_rtlabs p in 90 ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p'). 91 ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧ 92 cminor_rtlabs_rel … INV s s'. 74 93 75 axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'. 76 cminor_noinit_to_rtlabs cm_program = ra_program → 77 make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s → 78 make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' → 79 ∃INV. cminor_rtlabs_rel INV s s'. 94 include "common/FEMeasurable.ma". 95 include "Cminor/Cminor_classified_system.ma". 96 include "RTLabs/RTLabs_classified_system.ma". 80 97 98 include "common/ExtraMonads.ma". 99 100 lemma Cminor_return_E0 : ∀ge,s,tr,s'. 101 step … Cminor_exec ge s = Value … 〈tr,s'〉 → 102 Cminor_classify s = cl_return → 103 tr = E0. 104 #ge * 105 [ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct 106  #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct 107  #v #m * 108 [ #tr #s' #STEP #_ 109 cases v in STEP; [ #E whd in E:(??%?); destruct ] 110 * [1,3,4: normalize #A try #B destruct ] 111 * #v #STEP whd in STEP:(??%?); destruct % 112  cases v 113 [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct // 114  normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct 115 ] 116  #v' * 117 [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct 118  #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct // 119 ] 120 ] 121 ] 122  #r #tr #s' #ST #CL normalize in CL; destruct 123 ] qed. 124 125 definition cminor_rtlabs_meas_sim : meas_sim ≝ 126 mk_meas_sim 127 Cminor_pcs 128 RTLabs_pcs 129 (λcmp,rap. cminor_to_rtlabs cmp = rap) 130 cminor_rtlabs_inv 131 cminor_rtlabs_rel 132 ? (* rel_normal *) 133 ? (* rel_labelled *) 134 ? (* rel_classify_call *) 135 ? (* rel_classify_return *) 136 ? (* rel_callee *) 137 ? (* labelled_normal_1 *) 138 ? (* labelled_normal_2 *) 139 ? (* notailcalls *) 140 (λ_.cminor_measure) 141 ? (* sim_normal *) 142 ? (* sim_call_nolabel *) 143 ? (* sim_call_label *) 144 ? (* sim_return *) 145 ? (* sim_cost *) 146 ? (* sim_init *) 147 . 148 [ (* rel_normal *) 149  (* rel_labelled *) 150 @cminor_rtlabs_rel_labelled 151  (* rel_classify_call *) 152  (* rel_classify_return *) 153  (* rel_callee *) 154  (* labelled_normal_1 *) 155 #g * // 156  (* labelled_normal_2 *) 157 #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???); 158 cases (next_instruction f) // 159  (* notailcalls *) 160 #g @Cminor_notailcalls 161  (* sim_normal *) 162 #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP 163 cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP) 164 #m #AFTER %{m} @(after_n_covariant … AFTER) 165 #tr' #s * * #H1 #H2 #H3 /3/ 166  (* sim_call_nolabel *) 167 #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0} 168 @(cminor_rtlabs_call_return … R1 … STEP) 169 change with (Cminor_classify ?) in CL1:(??%?); >CL1 % 170  (* sim_call_label *) 171 #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1} 172 lapply (cminor_rtlabs_call_return … R1 … STEP1) 173 [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ] 174 #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct 175 % [ % 176 [ % 177  change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2 178 ] lapply (cminor_rtlabs_cost … R' … CS2 STEP2) 179 #AFTER2 cases (after_1_step … AFTER2) 180 #trx * #sx * * #NFx #STEPx * #E #Rx destruct 181 whd >NFx whd >STEPx whd /3/ 182 ] 183  (* sim_return *) 184 #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0} 185 lapply (cminor_rtlabs_call_return … R1 … STEP) 186 [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ] 187 >(Cminor_return_E0 … STEP CL1) 188 #AFTER %{(refl ??)} @AFTER 189  (* sim_cost *) 190 #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP 191 @(cminor_rtlabs_cost … R1 … STEP) 192 @CS1 193  (* sim_init *) 194 #p #p' #s #COMPILE destruct #INIT 195 cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R 196 %{s'} % [ @INIT'  %{INV} @R ] 197 ] cases daemon qed.
Note: See TracChangeset
for help on using the changeset viewer.