 Timestamp:
 Mar 27, 2013, 7:00:14 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2953 r2989 60 60 (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1)) 61 61 ); 62 sim_call : 62 (* Naughty code without a cost label will end up being rejected, but we don't 63 have local information about that. *) 64 sim_call_nolabel : 63 65 ∀g1,g2. 64 66 ∀INV:ms_inv g1 g2. … … 67 69 pcs_classify ms_C1 g1 s1 = cl_call → 68 70 ¬ 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. *) 77 ∀s2,tr. 78 if pcs_labelled ms_C1 g1 s2 then 79 (∃si,tri1,tri2. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tri1,si〉 ∧ 80 bool_to_Prop (pcs_labelled ms_C1 g1 si) ∧ 81 step … (pcs_exec ms_C1) g1 si = Value … 〈tri1,s2〉 ∧ 82 tr = tri1 ⧺ tri2) 83 else 84 (step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉) 85 → 71 ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → 72 ¬ pcs_labelled ms_C1 g1 s2 → 86 73 ∃m. 87 74 after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 88 75 tr = tr' ∧ 89 76 ms_rel g1 g2 INV s2 s2' 77 ); 78 (* Note that extra steps are introduced in the frontend to perform variable 79 saves on entry. If there's a cost label (and there ought to be!) then we 80 move it forward, so have to include it in the simulation. Unfortunately 81 that's a little messy. *) 82 sim_call_label : 83 ∀g1,g2. 84 ∀INV:ms_inv g1 g2. 85 ∀s1,s1'. 86 ms_rel g1 g2 INV s1 s1' → 87 pcs_classify ms_C1 g1 s1 = cl_call → 88 ¬ pcs_labelled ms_C1 g1 s1 → 89 ∀s2,tr2,s3,tr3. 90 step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 → 91 pcs_labelled ms_C1 g1 s2 → 92 step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 → 93 ∃m. 94 after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. 95 tr2 = tr' ∧ 96 bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧ 97 (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'. 98 tr'' = tr3 ∧ 99 ms_rel g1 g2 INV s3 s3')) 90 100 ); 91 101 sim_return : … … 226 236 227 237 228 (* TODO repair proof229 238 230 239 lemma prefix_preserved : … … 239 248 pcs_labelled (ms_C1 MS) g sf → 240 249 250 (* Needed to ensure we can get back into the relation after a call *) 251 (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) → 252 241 253 ∃m',prefix',sf'. 242 254 exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ 243 255 bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧ 244 256 intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧ 245 ms_rel MS g g' INV sf sf'. 246 * #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 257 258 259 (* We may need to make extra steps to get back into the relation. In 260 particular, the Clight to Cminor stage adds stores to the stack after 261 the function call, but must preserve the position of the cost label at 262 the head of the function, so we may need to move past these stores. *) 263 ∃r,r',ex,ex',sr,sr'. 264 exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧ 265 bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧ 266 exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧ 267 bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧ 268 (∀cs. intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) cs ex = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') cs ex') ∧ 269 ms_rel MS g g' INV sr sr'. 270 271 * #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_nolabel #sim_call_label #sim_return #sim_cost #sim_init 247 272 #g #g' #INV #s1 #s1' #REL 248 273 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' 249 274 generalize in match [ ]; (* current call stack *) 250 elim m0 251 [ # current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf275 @(nat_elim1 m0) * 276 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_ 252 277 %{0} %{[]} %{s1'} 253 % [ % //  // ]254  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf 278 % [ % [ % [ //  <(rel_labelled … REL) // ]  // ]  %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ] 279  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP 255 280 cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 256 281 cases (true_or_false_Prop … (pcs_labelled … s1)) … … 262 287 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 263 288 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' 264 cases (IH current_stack … R2 … EXEC2 CSf)265 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''289 cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] 290 #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' 266 291 %{(1+m'')} %{(prefix'@prefix'')} %{sf''} 267 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 268  destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // 269 cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 270 <all_1 assumption 271 ] assumption 272 ] 292 % [ % [ % 293 [ @(exec_steps_join … EXEC1') @EXEC'' 294  @CS'' 295 ] destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // 296 cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct 297 <all_1 assumption 298 ] assumption 299 ] 273 300 274 301  #NCS … … 279 306 #n' #AFTER1' 280 307 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) 281 cases (IH current_stack … R2 … EXEC2 CSf)282 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R''308 cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] 309 #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' 283 310 %{(n'+m'')} %{(prefix'@prefix'')} %{sf''} 284 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 285  destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 286 [ assumption 287  cases prefix' in EXEC1' INV ⊢ %; 288 [ // 289  * #sx #trx #tl #EXEC1' #INV 290 <(exec_steps_first … EXEC1') 291 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL 292 @INV 293 ] 294  @OBS'' ] ] 295  @R'' 296 ] 311 % [ % [ % 312 [ @(exec_steps_join … EXEC1') @EXEC'' 313  @CS'' 314 ] destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 315 [ assumption 316  cases prefix' in EXEC1' INV ⊢ %; 317 [ // 318  * #sx #trx #tl #EXEC1' #INV 319 <(exec_steps_first … EXEC1') 320 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL 321 @INV 322 ] 323  @OBS'' 324 ] 325 ] @R'' 326 ] 327 297 328  #CALLRET 298 329 cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) … … 304 335 ] 305 336 ] * #CL 306 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 307 [2,4: >CL %] 308 #m' * #Etr #AFTER1' 309 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 310 [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 311  letin next_stack ≝ (tail … current_stack) 312 ] 313 cases (IH next_stack … R2 … EXEC2 CSf) 314 #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' 315 %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} 316 % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC'' 317  destruct cases (exec_steps_S … EXEC1') 318 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 319 destruct >Etrace 320 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 321 [ whd in match (cs_classify ??); >CL % 322  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 323  @INV 324  assumption 325  @(rel_callee … REL) 337 [ cases (true_or_false_Prop … (pcs_labelled … s2)) 338 [ #CS2 339 (* Can we execute another step now, or shall we wait for later? *) 340 cases m in IH EXEC2; 341 [ #_ (* Nope, use extra step to get back into relation *) 342 #EXEC2 whd in EXEC2:(??%%); destruct 343 cases EXTRA_STEP #trx * #sx #EXTRA EXTRA_STEP 344 cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct 345 cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP) 346 #m' #AFTER1' 347 cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2' 348 cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3 349 %{1} %{prefix1'} %{s2'} 350 % [ % [ % 351 [ @EXEC1' 352  @CS2' 353 ] destruct cases (exec_steps_S … EXEC1') 354 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 355 destruct <(append_nil … (?::prefix2)) in ⊢ (???%); 356 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 357 [ whd in match (cs_classify ??); >CL % 358  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 359  @INV1 360  % 361  @(rel_callee … REL) 362 ] 363 ] %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'} 364 cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2') 365 [ cases prefix2' in EXEC2' INV2 ⊢ %; 366 [ // 367  * #sp #trp #tlp #EXEC2' #INV2 368 whd in ⊢ (?%); <(exec_steps_first … EXEC2') 369 >labelled_normal2 // 370 ] 371 ] #Np2' 372 % [ % [ % [ % [ % 373 [ @EXTRA 374  whd in ⊢ (?%); >labelled_normal1 // 375 ] @EXEC2' 376 ] @Np2' 377 ] #cs <(append_nil … prefix2') <Etrace2 378 @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 379 [ <normal_state_p @labelled_normal1 // 380  @Np2' 381  // 382 ] 383 ] @R3 384 ] 385 ] 386 (* We can execute the cost label, too. *) 387  #m1 #IH #EXEC2 388 cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3 389 cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2) 390 #m' #AFTER1' 391 cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2' 392 cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3 393 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 394 cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ] 395 #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 396 %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''} 397 % [ % [ % 398 [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' 399  @CSf'' 400 ] destruct cases (exec_steps_S … EXEC1') 401 #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2'' 402 whd in EXEC2'':(??%%); 403 destruct 404 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 405 [ whd in match (cs_classify ??); >CL % 406  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 407  % 408  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 409 [ <normal_state_p @labelled_normal1 @CS2 410  cases prefix2' in EXEC2' INV2 ⊢ %; 411 [ // 412  * #sy #try #tly #EXEC2' #INV2 413 <(exec_steps_first … EXEC2') 414 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 // 415 ] 416  assumption 417 ] 418  @(rel_callee … REL) 419 ] 420 ] @R'' 421 ] 326 422 ] 327  destruct cases (exec_steps_S … EXEC1') 328 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 329 destruct >Etrace 330 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 331 [ whd in match (cs_classify ??); >CL % 332  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 333  @INV 334  assumption 423 424  #NCS2 425 cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) 426 [2: >CL %  3: @notb_Prop @NCS2 ] 427 #m' #AFTER1' 428 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 429 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 430 cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] 431 #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 432 %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} 433 % [ % [ % 434 [ @(exec_steps_join … EXEC1') @EXEC'' 435  @CSf'' 436 ] destruct cases (exec_steps_S … EXEC1') 437 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 438 destruct 439 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 440 [ whd in match (cs_classify ??); >CL % 441  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 442  @INV 443  assumption 444  @(rel_callee … REL) 445 ] 446 ] @R'' 335 447 ] 336 448 ] 337  2,4: @R'' 449 450  cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] 451 #m' * #Etr #AFTER1' 452 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 453 letin next_stack ≝ (tail … current_stack) 454 cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //] 455 #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' 456 %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} 457 % [ % [ % 458 [ @(exec_steps_join … EXEC1') @EXEC'' 459  @CSf'' 460 ] destruct cases (exec_steps_S … EXEC1') 461 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 462 destruct >Etrace 463 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 464 [ whd in match (cs_classify ??); >CL % 465  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 466  @INV 467  assumption 468 ] 469 ] @R'' 470 ] 338 471 ] 339 472 ] … … 391 524 measurable trace, so the end is no longer in the relation. ☹ *) 392 525 393 * #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_init526 * #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_nolabel #sim_call_label #sim_return #sim_cost #sim_init 394 527 #g #g' #INV #s1 #s1' #depth #callstack #REL 395 528 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' 396 529 generalize in match callstack; generalize in match depth; callstack depth 397 elim m0 398 [ (* "fake" base case  we can never have zero steps *)530 @(nat_elim1 m0) * 531 [ #_ (* "fake" base case  we can never have zero steps *) 399 532 #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC 400 533 whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct … … 409 542 cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 410 543 cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' 411 cases (IH depth current_stack … R2 … EXEC2 ??) 412 [ (* End must be later, and still a return *) 413 2: destruct cases END * 544 cases (IH m ? depth current_stack … R2 … EXEC2 ??) 545 [ 2: // 546  (* End must be later, and still a return *) 547 3: destruct cases END * 414 548 [ * #trE * #sE * #E whd in E:(???%); destruct 415 549 #CL cases (pnormal_state_inv … N1) >CL #E destruct … … 417 551 %{t} %{trE} %{sE} /2/ 418 552 ] 419  3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;553  4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; 420 554 cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS 421 555 ] … … 440 574 #n' #AFTER1' 441 575 cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) 442 cases (IH depth current_stack … R2 … EXEC2 ??) 443 [ (* End must be later, and still a return *) 444 2: destruct cases END * 576 cases (IH m ? depth current_stack … R2 … EXEC2 ??) 577 [ 2: // 578  (* End must be later, and still a return *) 579 3: destruct cases END * 445 580 [ * #trE * #sE * #E whd in E:(???%); destruct 446 581 #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct … … 448 583 %{t} %{trE} %{sE} /2/ 449 584 ] 450  3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS;585  4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; 451 586 cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS 452 587 ] … … 484 619 cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ] 485 620 #E1 normalize in E1; destruct 486 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 487 [2: >CL %] 621 cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] 488 622 #m' * #Etr #AFTER1' destruct 489 623 cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2' … … 510 644 ] 511 645 ] 512 ] * #s2x #tr2 #trace3 #E1 #EXEC2 646 ] 647 (* Not at the end *) 648 * #s2x #tr2 #trace3 #E1 #EXEC2 513 649 cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) 514 650 [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; … … 519 655 ] 520 656 ] * #CL 521 cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) 522 [2,4: >CL %] 657 658 [ cases (true_or_false_Prop … (pcs_labelled … s2)) 659 [ #CS2 660 (* We can't stop here *) 661 cases m in IH EXEC2; 662 [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ] 663 #m1 #IH #EXEC2 664 cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3 665 cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2) 666 #m' #AFTER1' 667 cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2' 668 cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3 669 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 670 letin next_depth ≝ (S depth) 671 cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2 672 cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??) 673 [ 2: // 674  (* End must be later, and still a return *) 675 3: destruct cases END * 676 [ * #trE * #sE * #E whd in E:(???%); destruct 677  *: #h1 * 678 [ * #trE * #sE * #E normalize in E:(???%); destruct 679 #CL cases (pnormal_state_inv … N2) >CL #E destruct 680  #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL 681 %{t} %{trE} %{sE} /2/ 682 ] 683 ] 684  4: destruct whd in RETURNS:(?%); 685 whd in match (cs_classify ??) in RETURNS; 686 >CL in RETURNS; whd in ⊢ (?% → ?); 687 cases (pnormal_state_inv … N2) #CL2 688 whd in match (cs_classify ??); >CL2 // 689 ] 690 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 691 %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''} 692 % [ % [ % 693 [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' 694  @ends_at_return_append @ends_at_return_append assumption 695 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'' 696 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 697 <(rel_classify … REL) >CL whd in ⊢ (?%); whd in INV1:(?(???%)); 698 >will_return_aux_normal [2: @INV1 ] 699 >will_return_aux_normal 700 [ // 701  cases interesting2' in EXEC2' INV2 ⊢ %; 702 [ // 703  * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL 704 whd in ⊢ (?%); <normal_state_p >(labelled_normal2 … CS2') @TL 705 ] 706 ] 707 ] destruct cases (exec_steps_S … EXEC1') 708 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'' 709 destruct 710 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 711 [ whd in match (cs_classify ??); >CL % 712  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 713  @INV1 714  @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 715 (* Repeats bits of proof above, could compress *) 716 [ <normal_state_p @labelled_normal1 @CS2 717  cases interesting2' in EXEC2' INV2 ⊢ %; 718 [ // 719  * #sy #try #tly #EXEC2' #INV2 720 <(exec_steps_first … EXEC2') 721 whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 // 722 ] 723  assumption 724 ] 725  @(rel_callee … REL) 726 ] 727 ] 728 729  #NCS2 730 cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) 731 [2: >CL %  3: @notb_Prop @NCS2 ] 732 #m' #AFTER1' 733 cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 734 letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 735 letin next_depth ≝ (S depth) 736 cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) 737 [ 2: // 738  (* End must be later, and still a return *) 739 3: destruct cases END * 740 [ * #trE * #sE * #E whd in E:(???%); destruct 741  *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 742 %{t} %{trE} %{sE} /2/ 743 ] 744  4: destruct whd in RETURNS:(?%); 745 whd in match (cs_classify ??) in RETURNS; 746 >CL in RETURNS; // 747 ] 748 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 749 %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} 750 % [ % [ % 751 [ @(exec_steps_join … EXEC1') @EXEC'' 752  @ends_at_return_append assumption 753 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 754 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 755 <(rel_classify … REL) >CL whd in ⊢ (?%); 756 >will_return_aux_normal // 757 ] destruct cases (exec_steps_S … EXEC1') 758 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 759 destruct 760 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 761 [ whd in match (cs_classify ??); >CL % 762  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 763  @INV 764  assumption 765  @(rel_callee … REL) 766 ] 767 ] 768 ] 769  770 771 cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] 523 772 #m' * #Etr #AFTER1' 524 773 cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 525 [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] 526 letin next_depth ≝ (S depth) 527  letin next_stack ≝ (tail … current_stack) 528 letin next_depth ≝ (pred depth) 529 ] 530 cases (IH next_depth next_stack … R2 … EXEC2 ??) 531 [(* End must be later, and still a return *) 532 2,5: destruct cases END * 533 [1,3: * #trE * #sE * #E whd in E:(???%); destruct 534 *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 774 letin next_stack ≝ (tail … current_stack) 775 letin next_depth ≝ (pred depth) 776 cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) 777 [ 2: // 778  (* End must be later, and still a return *) 779 3: destruct cases END * 780 [ * #trE * #sE * #E whd in E:(???%); destruct 781  *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL 535 782 %{t} %{trE} %{sE} /2/ 536 783 ] 537  3: destruct whd in RETURNS:(?%); 538 whd in match (cs_classify ??) in RETURNS; 539 >CL in RETURNS; // 540  6: destruct whd in RETURNS:(?%); 784  4: destruct whd in RETURNS:(?%); 541 785 whd in match (cs_classify ??) in RETURNS; 542 786 >CL in RETURNS; whd in ⊢ (?% → ?); … … 546 790 #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' 547 791 %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} 548 % [1,3: % [1,3: % 549 [1,3: @(exec_steps_join … EXEC1') @EXEC'' 550 2,4: @ends_at_return_append assumption 551 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 552 destruct whd in ⊢ (?%); whd in match (cs_classify ??); 553 <(rel_classify … REL) >CL whd in ⊢ (?%); 554 >will_return_aux_normal // 555  cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 556 destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; 557 <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); 558 whd in match next_depth in RETURNS''; 559 cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ 560 whd in ⊢ (?%); 561 >will_return_aux_normal [ @RETURNS''  @INV ] 562 ] destruct cases (exec_steps_S … EXEC1') 563 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 564 destruct >Etrace 565 @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 566 [ whd in match (cs_classify ??); >CL % 567  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 568  @INV 569  assumption 570  @(rel_callee … REL) 571 ] 572  destruct cases (exec_steps_S … EXEC1') 573 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 574 destruct >Etrace 575 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 576 [ whd in match (cs_classify ??); >CL % 577  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 578  @INV 579  assumption 580 ] 581 ] 792 % [ % [ % 793 [ @(exec_steps_join … EXEC1') @EXEC'' 794  @ends_at_return_append assumption 795 ] cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' 796 destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; 797 <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); 798 whd in match next_depth in RETURNS''; 799 cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ 800 whd in ⊢ (?%); 801 >will_return_aux_normal [ @RETURNS''  @INV ] 802 ] destruct cases (exec_steps_S … EXEC1') 803 #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' 804 destruct >Etrace 805 @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) 806 [ whd in match (cs_classify ??); >CL % 807  whd in match (cs_classify ??); <(rel_classify … REL) >CL % 808  @INV 809  assumption 810 ] 582 811 ] 583 812 ] … … 610 839 %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ %  <(exec_steps_first … EXEC) @CS ]  @CL ] 611 840 ] qed. 841 842 (* TODO: move*) 843 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z. 844 #x0 elim x0 845 [ #y %{y} %2 % 846  #x #IH * 847 [ %{(S x)} %1 % 848  #y cases (IH y) #z * 849 [ #H %{z} %1 >H // 850  #H %{z} %2 >H // 851 ] 852 ] 853 ] qed. 854 855 lemma all_append : ∀A,p,l1,l2. 856 all A p (l1@l2) → 857 all A p l1 ∧ all A p l2. 858 #A #p #l1 elim l1 859 [ // 860  #h #t #IH #l2 861 whd in ⊢ (?% → ?(?%?)); 862 cases (p h) // 863 @IH 864 ] qed. 865 866 867 lemma ends_at_return_normal : ∀C,g,t1,t2. 868 ends_at_return C g (t1@t2) → 869 all … (λst. pnormal_state C g (\fst st)) t1 → 870 ends_at_return C g t2. 871 #C #g #t1 elim t1 872 [ // 873  * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1 874 [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?); 875 lapply (pnormal_state_inv … s2) 876 cases (pnormal_state … s2) 877 [ #H cases (H I) >CL #E' destruct 878  #_ * 879 ] 880  * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL 881 @IH 882 [ %{tl'} %{tr2} %{s2} >e0 % // 883  whd in ALL:(?%); cases (pnormal_state … s') in ALL; 884 [ //  * ] 885 ] 886 ] 887 ] qed. 888 612 889 613 890 … … 634 911 635 912 cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1) 636 #m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1 637 638 cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS) 913 (* Need an extra step from the source in case we end up at a label after a 914 function call. *) 915 [2: cases n in EXEC1; 916 [ #E whd in E:(??%?); destruct cases RETURNS 917  #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_ 918 %{ex} %{sx} @EX1 919 ] 920 ] 921 #m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0 922 * #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1 923 924 (* Show that the extra r steps we need to get back into the relation are a 925 prefix of the measurable subtrace. *) 926 cut (∃nr,interesting2. n = r + nr ∧ 927 exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧ 928 interesting = interesting1 @ interesting2) 929 [ cases (plus_split n r) #nr * 930 [ #En %{nr} >En in EXEC1; #EXEC1 931 cases (exec_steps_split … EXEC1) 932 #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E 933 >EXECr in EXEC1x; #E1x destruct 934 %{interesting2} % [ % [ %  assumption ]  % ] 935  #En @⊥ 936 >En in EXECr; #EXECr cases (exec_steps_split … EXECr) 937 #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct 938 #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2 939 cases ENDS #le * #tre * #se * #Ee #CLe destruct 940 cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?); 941 lapply (pnormal_state_inv … se) cases (pnormal_state … se) 942 [ #H cases (H I) >CLe #E destruct 943  #_ * 944 ] 945 ] 946 ] 947 * #nr * #interesting2 * * #En #EXECr2 #Ei destruct 948 949 whd in RETURNS:(?%); 950 >will_return_aux_normal in RETURNS; 951 [2: @Nr] #RETURNS 952 953 lapply (ends_at_return_normal … ENDS Nr) 954 #ENDS2 955 956 cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS) 639 957 #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' 640 958 641 cut (intensional_trace_of_trace C [ ] (prefix@interesting ) =642 intensional_trace_of_trace C' [ ] (prefix'@interesting '))643 [ >int_trace_append' > int_trace_append'959 cut (intensional_trace_of_trace C [ ] (prefix@interesting1) = 960 intensional_trace_of_trace C' [ ] (prefix'@interesting1')) 961 [ >int_trace_append' >(int_trace_append' C') 644 962 <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair 963 <OBS1 % 964 ] #OBS01 965 966 cut (intensional_trace_of_trace C [ ] (prefix@interesting1@interesting2) = 967 intensional_trace_of_trace C' [ ] (prefix'@interesting1'@interesting')) 968 [ <associative_append <associative_append 969 >int_trace_append' >(int_trace_append' C') 970 <OBS01 971 @breakup_pair @breakup_pair @breakup_pair @breakup_pair 645 972 <OBS' % 646 973 ] #Eobs 647 974 648 %{m'} %{n'} % 649 [ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'} 975 lapply (exec_steps_join … EXECr' EXEC1') 976 #EXECr'' 977 978 %{m'} %{(r' + n')} % 979 [ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'} 650 980 % [ % [ % [ % [ % 651 981 [ assumption 652 982  assumption 653 983 ] assumption 654 ] @(build_label_to_ret … EXEC 1' ? ENDS')984 ] @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS')) 655 985 [ #s #CS @(ms_labelled_normal_2 … CS) 656  <(ms_rel_labelled … R1) @CS1 986  <(ms_rel_labelled … R1) @CS1' 657 987 ] 658 ] @RETURNS'988 ] whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS' 659 989 ] <Eobs @MAX 660 990 ] 661 991  >INIT >INIT' 662 992 whd in ⊢ (??%%); >EXEC0 >EXEC0' 663 whd in ⊢ (??%%); >EXEC1 >EXEC1' 664 whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %; 665 #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % 993 whd in ⊢ (??%%); >EXEC1 >EXECr'' 994 whd in ⊢ (??%%); >int_trace_append' in OBS'; <OBS0 995 cases (intensional_trace_of_trace C [ ] prefix) 996 #cs #prefixtr whd in ⊢ (??(??(???%)?)(??(???%)?) → ??%%); 997 >int_trace_append' >int_trace_append' <OBS1 998 @breakup_pair @breakup_pair @breakup_pair @breakup_pair @breakup_pair 999 #OBS' <OBS' % 666 1000 ] qed. 667 *)
Note: See TracChangeset
for help on using the changeset viewer.