Changeset 1930 for src/Clight/labelSimulation.ma
 Timestamp:
 May 9, 2012, 6:30:41 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1922 r1930 15 15 }. 16 16 17 lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D. 18 \fst (let 〈x,y〉 ≝ e in F x y) = let 〈x,y〉 ≝ e in \fst (F x y). 19 #A #B #C #D * // 20 qed. 21 17 (* Useful for breaking up the labeling functions, because we don't care about 18 *which* cost labels are added here and so can throw away the resulting name 19 generator. *) 22 20 lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D. 23 21 \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) = F (\fst e). … … 25 23 qed. 26 24 27 (* lemma to break up label_expr, label_exprs and label_statement in the labelling28 functions *)25 (* Similarly, lemma to break up label_expr, label_exprs and label_statement in 26 the labelling functions *) 29 27 lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0]. 30 28 (∀u'. P (F (\fst (L syn u)) u')) → … … 43 41 44 42 45 46 43 lemma label_expr_type : ∀e,u. 47 44 typeof (\fst (label_expr e u)) = typeof e. … … 49 46 qed. 50 47 48 (* Formalise the notion of a trace with extra cost labels added. Note that 49 we don't require the left trace to be cost free. *) 51 50 inductive trace_with_extra_labels : trace → trace → Prop ≝ 52 51  twel_0 : trace_with_extra_labels E0 E0 … … 71 70 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx). 72 71 73 lemmalabel_expr_ok : ∀ge,ge',en,m.72 theorem label_expr_ok : ∀ge,ge',en,m. 74 73 related_globals ge ge' → 75 74 (∀e,v,tr. … … 80 79 ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧ 81 80 trace_with_extra_labels tr tr'). 81 (* Proof goes by breaking up the execution in the hypothesis, breaking up the 82 labelling function to get a new term and executing it by rewriting what we 83 learned from the hypothesis. *) 82 84 #ge #ge' #en #m #RG @expr_lvalue_ind_combined 83 85 [ 1,2: normalize /3 by ex_intro, conj/ … … 278 280 ] qed. 279 281 280 (* Plan: 281  extend labelling functions to continuations and hence states 282 NO  this doesn't work because we don't know *which* cost labels to add 283 realistically we'll have to define erasure functions 284 BETTER  use predicate so that we don't need to insist on the absence of 285 cost labels in the source 286  build a simulation relation linking states to their labelled counterparts 287  write a predicate stating that two traces are the same except for some 288 extra costs 289  show some labelling relationship for global environments 290  prove that 291 exec_step ge s1 = = Value … 〈tr,s2〉 → 292 cost_related s1 s1' → 293 ∃tr'. equal_up_to_costs tr tr' ∧ 294 plus ge' s1' tr' s2' ∧ 295 cost_related s2 s2' 296 using some relationship between ge and ge'. 297 *) 298 282 283 (* Now we move on to describe the simulation relation. First, relate the 284 continuations. *) 299 285 inductive cont_with_labels : cont → cont → Prop ≝ 300 286  cwl_stop : cont_with_labels Kstop Kstop … … 322 308 qed. 323 309 310 (* Now define almost all of the simulation relation... *) 324 311 inductive state_with_labels_partial : state → state → Prop ≝ 325 312  swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m) … … 338 325 . 339 326 340 (* We handle the switch states after the rest so that we can reuse the partial 341 result. *) 327 (* ... and add the states where the cases from switch statements are expanded. 328 We do these separately because in the LSdefault case we have to execute a 329 cost label alongside an arbitrary statement, and we want to reuse the result 330 on arbitrary statements we get for state_with_labels_partial. *) 342 331 inductive state_with_labels : state → state → Prop ≝ 343 332  swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s' … … 347 336 . 348 337 338 (* TODO: this (or something like it) ought to be elsewhere. *) 349 339 inductive plus (ge:genv) : state → trace → state → Prop ≝ 350 340  plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2 351 341  plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3. 352 342 353 definition eplus ≝ λn. repeat n io_out io_in clight_fullexec. 354 355 inductive hplus (ge:genv) : state → trace → trace → state → Prop ≝ 356  hplus_one : ∀tr,s2,s1',tr1,tr2,s2'. 357 exec_step ge s1' = OK … 〈tr2,s2'〉 → 358 trace_with_extra_labels tr (tr1⧺tr2) → 359 state_with_labels s2 s2' → 360 hplus ge s1' tr1 tr s2 361  hplus_succ : ∀s1,tr,s2,tr1,tr2,s3. 362 exec_step ge s1 = OK … 〈tr2,s2〉 → 363 hplus ge s2 (tr1⧺tr2) tr s3 → 364 hplus ge s1 tr1 tr s3. 365 343 (* Some details are invariant under labelling. *) 366 344 lemma label_function_return : ∀f. 367 345 fn_return (label_function f) = fn_return f. … … 374 352 qed. 375 353 376 lemma bindIO_inversion: ∀O,I.377 ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.378 (f »= g = return y) →379 ∃x. (f = return x) ∧ (g x = return y).380 #O #I #A #B #f #g #y cases f normalize381 [ #o #k #E destruct382  #a #e %{a} /2 by conj/383  #m #H destruct (H)384 ] qed.385 386 lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v.387 err_to_io … e = Value O I T v →388 e = OK T v.389 #O #I #T *390 [ #e #v #E normalize in E; destruct @refl391  #m #v #E normalize in E; destruct392 ]393 qed.394 395 coercion io_eq_from_res :396 ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res397 on _E:eq (IO ???) ?? to eq (res ?) ??.398 399 lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.400 exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =401 exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.402 #ge #e #m #a #ty #u403 whd in ⊢ (??(????(???%))?); >shift_fst @refl404 qed.405 406 354 lemma label_expr_fun_typeof : ∀a,u. 407 355 fun_typeof (\fst (label_expr a u)) = fun_typeof a. … … 415 363 normalize cases (label_statement ??) #body' #u 416 364 normalize cases (fresh ??) // 365 qed. 366 367 lemma label_fn_params : ∀f. 368 fn_params (label_function f) = fn_params f. 369 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 370 qed. 371 372 lemma label_fn_vars : ∀f. 373 fn_vars (label_function f) = fn_vars f. 374 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 375 qed. 376 377 (* Some annoying rewrite rules *) 378 lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u. 379 exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) = 380 exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty. 381 #ge #e #m #a #ty #u 382 whd in ⊢ (??(????(???%))?); >shift_fst @refl 417 383 qed. 418 384 … … 427 393  #fd' #H #E normalize in E; destruct >(H (refl ??)) // 428 394 ] qed. 429 430 (*431 lemma step_with_labels : ∀ge,s1,s1',tr,s2.432 state_with_labels s1 s1' →433 exec_step ge s1 = OK … 〈tr,s2〉 →434 hplus ge s1' E0 tr s2.435 #ge #Xs1 #Xs1' #tr #s2 *436 [ #f #us #s #k #k' #e #m #KL cases s437 [ #EX inversion KL438 [ #E1 #E2 #_ destruct @hplus_one [3: whd in EX:(??%?) ⊢ (??%?);439 >label_function_return >EX in ⊢ (??%?);  1,2:skip  //  %1440 cases f in EX ⊢ %; #rty #params #vars #body #EX whd in ⊢ (??(match ?% with [_⇒?_⇒?_⇒?_⇒?_⇒?_⇒?_⇒?_⇒?_⇒?])?); >EX441 whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));442 443 lemma step_with_labels : ∀ge,s1,s1',tr,s2.444 state_with_labels s1 s1' →445 exec_step ge s1 = OK … 〈tr,s2〉 →446 ∃n,tr',s2'. eplus n ge s1' = OK … 〈tr',s2'〉 ∧447 trace_with_extra_labels tr tr' ∧448 state_with_labels s2 s2'.449 #ge #Xs1 #Xs1' #tr #s2 *450 [ #f #us #s #k #k' #e #m #KL cases s451 [ #EX %{1} %{tr} inversion KL452 [ #E1 #E2 #_ destruct453 whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));454 whd in EX:(??%?) ⊢ (??(λ_.?(?(??(?????%?)?)?)?));455 normalize in EX:(??%?) ⊢ (??(λ_.?(?(??(%??????)?)?)?));456 % [2: % [ % [ @plus_one whd in EX:(??%?) ⊢ (??%?); >EX whd in ⊢ (??(??(??%???))?); @EX >EX @refl457 *)458 395 459 396 lemma labelled_not_skip : ∀s,u. … … 477 414 [ #E @⊥ @(absurd ? E) @labelled_not_skip // 478 415  /2/ 479 ] qed.480 481 (* TODO: this is from CexecComplete, but should live somewhere else *)482 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.483 #P #f #p #Q #H cases f;484 [ @H485  #np cut False [ @(absurd ? p np)  * ]486 ] qed.487 488 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.489 #P #f #p #Q #H cases f;490 [ #np cut False [ @(absurd ? np p)  * ]491  @H492 416 ] qed. 493 417 … … 527 451 ] qed. 528 452 453 (* Break up labelling function in one go for statements. *) 529 454 lemma blindly_label : ∀u,s. ∀P:statement → Prop. 530 455 match s with … … 557 482 ] qed. 558 483 559 lemma label_fn_params : ∀f. 560 fn_params (label_function f) = fn_params f. 561 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 562 qed. 563 564 lemma label_fn_vars : ∀f. 565 fn_vars (label_function f) = fn_vars f. 566 * #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair // 567 qed. 568 569 (* Apply induction hypothesis while getting Matita to infer the continuations 570 k0 and k0', and the universe u0. *) 484 (* Apply induction hypothesis in label_find_label proof below while getting 485 Matita to infer the continuations k0 and k0', and the universe u0, rather 486 than having to give them explicitly. *) 571 487 lemma lfl_IH : ∀s0,lbl. 572 488 ∀C:option (statement×cont) → option (statement×cont) → Prop. … … 580 496 qed. 581 497 498 (* Finding a goto label in a costlabelled program gives a labelled version of 499 the statement and continuation found by the original function, if any. *) 582 500 lemma label_find_label : ∀lbl,s,k,k',u. 583 501 cont_with_labels k k' → … … 747 665 qed. 748 666 667 749 668 (* We show the main simulation in two stages. First, we show it for all states 750 669 in the relation *except* those for labeled_statements, then we'll show the … … 759 678 trace_with_extra_labels tr tr' ∧ 760 679 state_with_labels s2 s2'. 680 681 (* General plan is like the expressions result, except that we do case analysis 682 on the simulation first, then: break up the original execution, break up the 683 cost labelling, use the earlier results to deal with expressions, then 684 run the labelled version for enough steps. We try to avoid having to write 685 out the final trace and state and "skip" them afterwards. *) 761 686 #ge #ge' #RG #Xs1 #Xs1' #tr #s2 * 762 687 [ #f #us #s #k #k' #e #m #KL cases s … … 1125 1050 ] qed. 1126 1051 1127 lemma step_with_labels : ∀ge,ge'. 1052 1053 theorem step_with_labels : ∀ge,ge'. 1128 1054 related_globals ge ge' → 1129 1055 ∀s1,s1',tr,s2.
Note: See TracChangeset
for help on using the changeset viewer.