Changeset 3007
 Timestamp:
 Mar 28, 2013, 2:59:43 PM (4 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/Cminor_abstract.ma
r2737 r3007 42 42 definition CmCallstate ≝ Callstate. 43 43 44 lemma Cminor_notailcalls : ∀s. Cminor_classify s ≠ cl_tailcall. 45 * #a try #b try #c try #d try #e try #f try #g try #h try #i try #j 46 normalize % #E destruct 47 qed. 
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. 
src/common/FEMeasurable.ma
r2990 r3007 22 22 Note: as we're interested in measurable subtraces, we don't have to worry 23 23 about the execution "going wrong." 24 25 For call and return states we only allow the addition of extra steps *after* 26 the corresponding call or return state (i.e., the simulation must always 27 start with it). This is true in the frontend: Callstate and Returnstate 28 are the second half of calls and returns, the first is the instruction for 29 the call or return which is translated as a "normal" step, where any extra 30 instructions for before the action are added. 24 31 *) 25 32 … … 29 36 ms_compiled : program … ms_C1 → program … ms_C2 → Prop; 30 37 ms_inv : ? → ? → Type[0]; 31 ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);32 38 ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; 33 39 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2; … … 192 198 ms_rel MS g g' INV sr sr'. 193 199 194 * #C1 #C2 #compiled #inv # stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init200 * #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init 195 201 #g #g' #INV #s1 #s1' #REL 196 202 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' … … 447 453 measurable trace, so the end is no longer in the relation. ☹ *) 448 454 449 * #C1 #C2 #compiled #inv # stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init455 * #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init 450 456 #g #g' #INV #s1 #s1' #depth #callstack #REL 451 457 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1'
Note: See TracChangeset
for help on using the changeset viewer.