Changeset 2690
 Timestamp:
 Feb 21, 2013, 7:24:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2685 r2690 33 33 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; 34 34 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2; 35 (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *) 35 36 ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2; 36 37 ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H'; … … 66 67 match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true  cl_return ⇒ true  _ ⇒ false] → 67 68 ¬ pcs_labelled ms_C1 g1 s1 → 69 (* NB: calls and returns don't emit timing cost labels; otherwise we would 70 have to worry about whether the cost labels seen at the final return of 71 the measured trace might appear in the target in subsequent steps that 72 are *after* the new measurable subtrace. Also note that extra steps are 73 introduced in the frontend: to perform variable saves on entry and to 74 write back the result *after* exit. The latter do not get included in 75 the measurable subtrace because it stops at the return, and they are the 76 caller's responsibility. *) 68 77 ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → 69 ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 70 tr = tr' ∧ 78 ∃m. tr = E0 ∧ 79 after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 80 E0 = tr' ∧ 71 81 ms_rel g1 g2 INV s2 s2' 72 82 ); … … 83 93 ); 84 94 sim_init : 85 ∀p1,p2,s ,s'.95 ∀p1,p2,s. 86 96 ms_compiled p1 p2 → 87 97 make_initial_state ?? ms_C1 p1 = OK ? s → 88 make_initial_state ?? ms_C2 p2 = OK ? s' →98 ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧ 89 99 ∃INV. ms_rel ?? INV s s' 90 100 }. 91 101 92 (* TODO: obs eq *) 102 93 103 (* 94 104 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. … … 186 196 qed. 187 197 188 (* WIP commented out*) 198 189 199 lemma prefix_preserved : 190 200 ∀MS:meas_sim. … … 265 275 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 266 276 [2,4: >CL %] 267 #m' #AFTER1'277 #m' * #Etr #AFTER1' 268 278 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 269 279 [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] … … 276 286  destruct cases (exec_steps_S … EXEC1') 277 287 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 278 destruct 288 destruct >Etrace 279 289 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 280 290 [1,3: whd in match (cs_classify ??); >CL % … … 286 296  destruct cases (exec_steps_S … EXEC1') 287 297 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 288 destruct 298 destruct >Etrace 289 299 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 290 300 [ whd in match (cs_classify ??); >CL % … … 299 309 ] 300 310 ] qed. 301 302 303 311 312 definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝ 313 λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return. 314 315 lemma ends_at_return_append : ∀C,g,t1,t2. 316 ends_at_return C g t2 → 317 ends_at_return C g (t1@t2). 318 #C #g #t1 #t2 * #x * #tr * #s * #E >E #CL 319 %{(t1@x)} %{tr} %{s} % /2/ 320 qed. 321 322 lemma will_return_aux_normal : ∀C,depth,t1,t2. 323 all … (λstr. normal_state C (\fst str)) t1 → 324 will_return_aux C depth (t1@t2) = will_return_aux C depth t2. 325 #C #depth #t1 #t2 elim t1 326 [ #_ % 327  * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl 328 whd in ⊢ (??%?); 329 cases (normal_state_inv … N1) #CL >CL 330 @IH @Ntl 331 ] qed. 332 333 lemma measurable_subtrace_preserved : 334 ∀MS:meas_sim. 335 ∀g,g'. 336 ∀INV:ms_inv MS g g'. 337 ∀s1,s1',depth,callstack. 338 ms_rel MS g g' INV s1 s1' → 339 340 let C ≝ pcs_to_cs (ms_C1 MS) g in 341 let C' ≝ pcs_to_cs (ms_C2 MS) g' in 342 343 ∀m,interesting,sf. 344 exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 → 345 ends_at_return (ms_C1 MS) g interesting → 346 will_return_aux C depth interesting → 347 348 ∃m',interesting',sf'. 349 exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧ 350 (* The obs trace equality almost gives this, but doesn't ensure the 351 cost/return are exactly at the ends *) 352 ends_at_return (ms_C2 MS) g' interesting' ∧ 353 bool_to_Prop (will_return_aux C' depth interesting') ∧ 354 355 intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'. 356 (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it 357 isn't true if the final return step is expanded into the caller, e.g., 358 in Clight → Cminor we added an instruction to callers if they need to 359 store the result in memory. This extra step doesn't form part of the 360 measurable trace, so the end is no longer in the relation. ☹ *) 361 362 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init 363 #g #g' #INV #s1 #s1' #depth #callstack #REL 364 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' 365 generalize in match callstack; generalize in match depth; callstack depth 366 elim m0 367 [ (* "fake" base case  we can never have zero steps *) 368 #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC 369 whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct 370  #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS 371 cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 372 cases (true_or_false_Prop … (pcs_labelled … s1)) 373 [ #CS 374 lapply (sim_cost … REL CS STEP1) 375 #AFTER1' 376 cases (after_n_exec_steps … AFTER1') 377 #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2 378 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 379 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' 380 cases (IH depth current_stack … R2 … EXEC2 ??) 381 [ (* End must be later, and still a return *) 382 2: destruct cases END * 383 [ * #trE * #sE * #E whd in E:(???%); destruct 384 #CL cases (pnormal_state_inv … N1) >CL #E destruct 385  #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 386 %{t} %{trE} %{sE} /2/ 387 ] 388  3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; 389 cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS 390 ] 391 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 392 %{(1+m'')} %{(interesting'@interesting'')} %{sf''} 393 % [ % [ % 394 [ @(exec_steps_join … EXEC1') @EXEC'' 395  @ends_at_return_append assumption 396 ] cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 397 whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) 398 cases (pnormal_state_inv … N1) #CL >CL @RETURNS'' 399 ] destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // 400 cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 401 <all_1 assumption 402 ] 403 404  #NCS 405 cases (true_or_false_Prop (pnormal_state C1 g s1)) 406 [ #NORMAL 407 (* XXX should set things up so that notb_Prop isn't needed *) 408 cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) 409 #n' #AFTER1' 410 cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) 411 cases (IH depth current_stack … R2 … EXEC2 ??) 412 [ (* End must be later, and still a return *) 413 2: destruct cases END * 414 [ * #trE * #sE * #E whd in E:(???%); destruct 415 #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct 416  #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 417 %{t} %{trE} %{sE} /2/ 418 ] 419  3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; 420 cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS 421 ] 422 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 423 %{(n'+m'')} %{(interesting'@interesting'')} %{sf''} 424 % [ % [ % 425 [ @(exec_steps_join … EXEC1') @EXEC'' 426  @ends_at_return_append assumption 427 ] >will_return_aux_normal 428 [ @RETURNS'' 429  cases n' in EXEC1'; 430 [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) % 431  #n'' #EXEC cases (exec_steps_S … EXEC) 432 #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct 433 @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL  @INV ] 434 ] 435 ] 436 ] destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 437 [ assumption 438  cases interesting' in EXEC1' INV ⊢ %; 439 [ // 440  * #sx #trx #tl #EXEC1' #INV 441 <(exec_steps_first … EXEC1') 442 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL 443 @INV 444 ] 445  @OBS'' 446 ] 447 ] 448 449  #CALLRET 450 cases trace2 in E1 EXEC2; 451 (* For a return we might hit the end  this is the real base case. *) 452 [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL 453 cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ] 454 #E1 normalize in E1; destruct 455 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 456 [2: >CL %] 457 #m' * #Etr #AFTER1' destruct 458 cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2' 459 cut (tr1' = E0) [ 460 cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_ 461 cases (Eapp_E0_inv … (sym_eq … H)) // 462 ] #E1 destruct 463 %{1} %{[〈s1',E0〉]} %{s2'} 464 % [ % [ % 465 [ whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); % 466  %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption 467 ] whd in RETURNS:(?%) ⊢ (?%); 468 whd in match (cs_classify ??) in RETURNS; 469 whd in match (cs_classify ??); <(rel_classify … REL) 470 >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%); 471 cases depth [ //  #d * ] 472 ] <(append_nil … [〈s1',E0〉]) 473 change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?); 474 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 475 [ @CL 476  whd in ⊢ (??%?); <(rel_classify … REL) @CL 477  % 478  % 479 ] 480 ] 481 ] * #s2x #tr2 #trace3 #E1 #EXEC2 482 cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) 483 [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; 484 lapply (no_tailcalls … s1) 485 cases (pcs_classify … s1) in CALLRET ⊢ %; 486 [ 1,3: #_ #_ /2/ 487  *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) 488 ] 489 ] * #CL 490 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 491 [2,4: >CL %] 492 #m' * #Etr #AFTER1' 493 cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 494 [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 495 letin next_depth ≝ (S depth) 496  letin next_stack ≝ (tail … current_stack) 497 letin next_depth ≝ (pred depth) 498 ] 499 cases (IH next_depth next_stack … R2 … EXEC2 ??) 500 [(* End must be later, and still a return *) 501 2,5: destruct cases END * 502 [1,3: * #trE * #sE * #E whd in E:(???%); destruct 503 *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 504 %{t} %{trE} %{sE} /2/ 505 ] 506  3: destruct whd in RETURNS:(?%); 507 whd in match (cs_classify ??) in RETURNS; 508 >CL in RETURNS; // 509  6: destruct whd in RETURNS:(?%); 510 whd in match (cs_classify ??) in RETURNS; 511 >CL in RETURNS; whd in ⊢ (?% → ?); 512 whd in match next_depth; cases depth 513 [ *  #d' // ] 514 ] 515 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 516 %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} 517 % [1,3: % [1,3: % 518 [1,3: @(exec_steps_join … EXEC1') @EXEC'' 519 2,4: @ends_at_return_append assumption 520 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 521 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 522 <(rel_classify … REL) >CL whd in ⊢ (?%); 523 >will_return_aux_normal // 524  cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 525 destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; 526 <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); 527 whd in match next_depth in RETURNS''; 528 cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ 529 whd in ⊢ (?%); 530 >will_return_aux_normal [ @RETURNS''  @INV ] 531 ] destruct cases (exec_steps_S … EXEC1') 532 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 533 destruct >Etrace 534 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 535 [1,3: whd in match (cs_classify ??); >CL % 536 2,4: whd in match (cs_classify ??); <(rel_classify … REL) >CL % 537  @INV 538  assumption 539  @(rel_callee … REL) 540 ] 541  destruct cases (exec_steps_S … EXEC1') 542 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 543 destruct >Etrace 544 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 545 [ whd in match (cs_classify ??); >CL % 546  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 547  @INV 548  assumption 549 ] 550 ] 551 ] 552 ] 553 ] qed. 554 555 lemma label_to_ret_inv : ∀C,m,g,s,trace,s'. 556 exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → 557 trace_is_label_to_return (pcs_to_cs … C g) trace → 558 bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace. 559 #C #m #g #s #trace #s' #EXEC 560 * #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct 561 >(exec_steps_first … EXEC) 562 % 563 [ @CS 564  %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL 565 ] qed. 566 567 lemma build_label_to_ret : ∀C,m,g,s,trace,s'. 568 (∀s. pcs_labelled C g s → pnormal_state C g s) → 569 exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → 570 pcs_labelled C g s → 571 ends_at_return C g trace → 572 trace_is_label_to_return (pcs_to_cs … C g) trace. 573 #C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL 574 destruct 575 cases trace' in EXEC ⊢ %; 576 [ #EXEC >(exec_steps_first … EXEC) in CS; #CS 577 cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct 578  * #s1 #tr1 #trace1 #EXEC 579 %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ %  <(exec_steps_first … EXEC) @CS ]  @CL ] 580 ] qed. 581 582 (* TODO: explicitly mention observables *) 304 583 theorem measured_subtrace_preserved : 305 584 ∀MS:meas_sim. … … 308 587 measurable (ms_C1 MS) p1 m n stack_cost max → 309 588 ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max. 310 589 #MS #p1 #p2 #m #n #stack_cost #max #compiled 590 * #s0 * #prefix * #s1 * #interesting * #s2 591 whd in ⊢ (? → ??(λ_.??(λ_.%))); 592 letin g ≝ (make_global … (pcs_exec … ) p1) 593 letin g' ≝ (make_global … (pcs_exec … ) p2) 594 letin C ≝ (pcs_to_cs ? g) 595 letin C' ≝ (pcs_to_cs ? g') 596 * * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX 597 598 cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0 599 cases (label_to_ret_inv … EXEC1 TLR) 600 #CS1 #ENDS 601 602 cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1) 603 #m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1 604 605 cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS) 606 #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' 607 608 %{m'} %{n'} %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'} 609 % [ % [ % [ % [ % 610 [ assumption 611  assumption 612 ] assumption 613 ] @(build_label_to_ret … EXEC1' ? ENDS') 614 [ #s #CS @(ms_labelled_normal_2 … CS) 615  <(ms_rel_labelled … R1) @CS1 616 ] 617 ] @RETURNS' 618 ] cases daemon (* TODO! *) 619 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.