Changeset 2202
 Timestamp:
 Jul 17, 2012, 6:57:39 PM (5 years ago)
 Location:
 src
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2176 r2202 1189 1189 1190 1190 lemma not_wrong_init : ∀p. 1191 not_wrong (exec_inf … clight_fullexec p) →1191 not_wrong state (exec_inf … clight_fullexec p) → 1192 1192 ∃s. make_initial_state … p = OK ? s. 1193 #p whd in ⊢ (? % → ?); change with (make_initial_state p) in match (make_initial_state ??? p);1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p); 1194 1194 cases (make_initial_state p) 1195 1195 [ /2/ … … 1225 1225 plus ge s tr s' → 1226 1226 is_final s' = None ? → 1227 steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s')). 1227 steps state tr 1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1229 (exec_inf_aux … clight_fullexec ge (exec_step ge s')). 1229 1230 #ge #s0 #tr0 #s0' #P elim P 1230 1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold 1231 whd in ⊢ (?? %?);1232 whd in ⊢ (???%?); 1232 1233 whd in match (is_final ?????); >NF 1233 1234 %2 1234 1235  #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF 1235 1236 >exec_inf_aux_unfold >EX1 1236 whd in ⊢ (?? %?);1237 whd in ⊢ (???%?); 1237 1238 whd in match (is_final ?????); >(plus_not_final … P2) 1238 1239 %3 @IH // … … 1242 1243 plus ge s tr s' → 1243 1244 is_final s' = Some ? r → 1244 ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1245 (e_stop … tr' r s'). 1245 ∃tr'. steps state tr 1246 (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1247 (e_stop … tr' r s'). 1246 1248 #ge #s0 #tr0 #s0' #r #P elim P 1247 1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold 1248 %{tr} whd in ⊢ (?? %?);1250 %{tr} whd in ⊢ (???%?); 1249 1251 whd in match (is_final ?????); >F 1250 1252 %1 … … 1253 1255 #tr' #S' %{tr'} 1254 1256 >exec_inf_aux_unfold >EX1 1255 whd in ⊢ (?? %?);1257 whd in ⊢ (???%?); 1256 1258 whd in match (is_final ?????); >(plus_not_final … P2) 1257 1259 %3 @S' … … 1263 1265 (s1,s2:state) 1264 1266 (S:state_with_labels s1 s2) 1265 (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))1267 (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))) 1266 1268 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 1267 1269 match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with … … 1299 1301 #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S' 1300 1302 lapply (NWk i) 1301 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (? % → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])1303 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?]) 1302 1304 @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????); 1303 1305 cases (is_final s2') 1304 [ whd in ⊢ (? % → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //1306 [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec // 1305 1307 inversion NW' 1306 1308 [ #H1 #H2 #H3 #H4 #H5 destruct … … 1308 1310  #H14 #H15 #H16 #H17 #H18 destruct 1309 1311 ] 1310  #r whd in ⊢ (? % → ?%%); #NW' @(swl_stop … (steps_stop …)) //1312  #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) // 1311 1313 ] 1312 1314 ] qed. … … 1343 1345 >I2 1344 1346 1345 whd in ⊢ (? % → ? → ?%%);1347 whd in ⊢ (??% → ? → ?%%); 1346 1348 >exec_inf_aux_unfold 1347 1349 >exec_inf_aux_unfold 1348 whd in ⊢ (? % → ? → ?%%);1350 whd in ⊢ (??% → ? → ?%%); 1349 1351 whd in match (is_final ?????); 1350 1352 >(initial_state_is_not_final … I1) 1351 1353 whd in match (is_final ?????); 1352 1354 >(initial_state_is_not_final … I2) 1353 whd in ⊢ (? % → ? → ?%%);1355 whd in ⊢ (??% → ? → ?%%); 1354 1356 1355 1357 #NW #S 
src/Clight/labelSpecification.ma
r2201 r2202 1 1 include "Clight/Cexec.ma". 2 2 include "Clight/label.ma". 3 include "common/Executions.ma". 3 4 4 5 (* Formalise the notion of a trace with extra cost labels added. Note that … … 9 10  twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2). 10 11 11 (* A finite trace is produced by some prefix of an execution. *)12 13 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝14  steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)15  steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e16  steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.17 18 12 (* One execution is simulated by another, but possibly using more steps and 19 13 introducing some cost labels. *) … … 21 15 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝ 22 16  swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2. 23 steps tr2 e2 (e_stop … tr2' r s2) →17 steps state tr2 e2 (e_stop … tr2' r s2) → 24 18 trace_with_extra_labels tr1 tr2 → 25 19 sim_with_labels (e_stop … tr1 r s1) e2 26 20  swl_steps : ∀tr1,tr2,s1,e1,e2,e2'. 27 steps tr2 e2 e2' →21 steps state tr2 e2 e2' → 28 22 trace_with_extra_labels tr1 tr2 → 29 23 sim_with_labels e1 e2' → … … 33 27 sim_with_labels (e_interact … o k1) (e_interact … o k2). 34 28 35 (* We do not consider wrong executions. *)36 37 coinductive not_wrong : execution state io_out io_in → Prop ≝38  nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)39  nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)40  nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).41 42 29 (* Desired result *) 43 30 … … 46 33 let e1 ≝ exec_inf … clight_fullexec p in 47 34 let e2 ≝ exec_inf … clight_fullexec (clight_label p) in 48 not_wrong e1 →35 not_wrong state e1 → 49 36 sim_with_labels e1 e2. 
src/common/SmallstepExec.ma
r2145 r2202 155 155 ]. 156 156 157 (* Some preliminary simulation stuff that's not been used yet.158 record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝159 { es0 :> execstep outty inty160 ; initial : state ?? es0 → Prop161 }.162 157 163 164 alias symbol "and" (instance 2) = "logical and".165 record related_semantics : Type[1] ≝166 { output : Type[0]167 ; input : output → Type[0]168 ; sem1 : execstep' output input169 ; sem2 : execstep' output input170 ; ge1 : genv ?? sem1171 ; ge2 : genv ?? sem2172 ; match_states : state ?? sem1 → state ?? sem2 → Prop173 ; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2174 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r175 }.176 177 178 179 record simulation : Type[1] ≝180 { sems :> related_semantics181 ; sim : ∀st1,st2,t,st1'.182 P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →183 match_states sems st1 st2 →184 ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧185 match_states sems st1' st2'186 }.187 *)
Note: See TracChangeset
for help on using the changeset viewer.