Changeset 2669 for src/common/SmallstepExec.ma
 Timestamp:
 Feb 15, 2013, 11:27:58 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/SmallstepExec.ma
r2668 r2669 383 383 (* For now I'm doing this without I/O, to keep things simple. In the place I 384 384 intend to use it (the definition of measurable subtraces, and proofs using 385 that) I should allow I/O for the prefix. *) 386 387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝ 385 that) I should allow I/O for the prefix. 386 387 If the execution has the form 388 389 s1 tr1→ s2 tr2→ … sn trn→ s' 390 391 then the function returns 392 393 〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉 394 *) 395 396 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝ 388 397 match n with 389 398 [ O ⇒ return 〈[ ], s〉 … … 395 404 [ Value trs ⇒ 396 405 ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); 397 return 〈 trs::tl, s'〉406 return 〈〈s, \fst trs〉::tl, s'〉 398 407  Interact _ _ ⇒ Error … (msg UnexpectedIO) 399 408  Wrong m ⇒ Error … m … … 408 417 is_final … fx g s = None ? ∧ 409 418 ∃tr',s',tl. 410 trace = 〈 tr',s'〉::tl ∧419 trace = 〈s,tr'〉::tl ∧ 411 420 step … fx g s = Value … 〈tr',s'〉 ∧ 412 421 exec_steps n O I fx g s' = OK … 〈tl,s''〉. … … 454 463 qed. 455 464 456 let rec gather_trace S (l:list ( trace × S)) on l : trace ≝465 let rec gather_trace S (l:list (S × trace)) on l : trace ≝ 457 466 match l with 458 467 [ nil ⇒ E0 459  cons h t ⇒ (\ fsth)⧺(gather_trace S t)468  cons h t ⇒ (\snd h)⧺(gather_trace S t) 460 469 ]. 461 470 … … 474 483 lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. 475 484 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 476 all … (λts. inv (\snd ts)) trace → 485 all ? (λstr. inv (\fst str)) (tail … trace) → 486 inv s' → 477 487 P (gather_trace ? trace) s' → 478 488 after_n_steps n O I fx g s inv P. 479 489 #n elim n 480 490 [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct 481 #ALL # p whd @p491 #ALL #FI #p whd @p 482 492  #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC 483 493 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 484 494 destruct 485 #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl)) 486 [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl 487 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) 495 #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl))) 496 [ cases m in STEPS; 497 [ whd in ⊢ (??%? → ?); #E destruct /2/ 498  #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct 499 whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ 500 ] 501 ] * #i1 #itl 502 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??)) 488 503 [ @p 504  @FALL 489 505  whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p' 490 506 ] … … 497 513 #n #O #I #fx #g #s #trace #s' #P #EXEC #p 498 514 @(exec_steps_after_n … EXEC) // 499 elim trace /2/ 515 cases trace // #x #trace' 516 elim trace' /2/ 500 517 qed. 501 518 … … 510 527 cases (IH … AFTER') 511 528 #tl * #s' * #STEPS #p 512 %{(〈 tr1,s1〉::tl)} %{s'} %529 %{(〈s,tr1〉::tl)} %{s'} % 513 530 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 514 531 ] qed. … … 526 543 cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' 527 544 cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 528 %{(〈 tr',s'〉::trace1)} %{trace2} %{s1}545 %{(〈s,tr'〉::trace1)} %{trace2} %{s1} 529 546 % 530 547 [ % … … 549 566 ] qed. 550 567 551 (* Show that it corresponds to split_trace … (exec_inf …) *) 568 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'. 569 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 → 570 s = s1. 571 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC 572 lapply (exec_steps_length … EXEC) #E normalize in E; destruct 573 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct 574 % 575 qed. 576 577 (* Show that it corresponds to split_trace … (exec_inf …). 578 We need to adjust the form of trace. *) 579 580 let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝ 581 match l with 582 [ nil ⇒ [〈tr,s'〉] 583  cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s') 584 ]. 585 586 definition switch_trace ≝ 587 λS,l,s'. match l with 588 [ nil ⇒ nil ? 589  cons h t ⇒ switch_trace_aux S (\snd h) t s' 590 ]. 552 591 553 592 lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. 554 593 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 555 594 match is_final … s' with 556 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈 trace, exec_inf_aux … fx g (step … s')〉557  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈 trace, e_stop … tr' r s'〉595 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉 596  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉 558 597 ]. 559 598 #O #I #fx #g #n elim n … … 570 609 >exec_inf_aux_unfold normalize nodelta 571 610 cases (is_final … s') 572 [ %611 [ whd % 573 612  #r %2 %{tr''} % 574 613 ] 575  * # tr1 #s1 #tl1 #E normalize in E; destruct #Esteps614  * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps 576 615 lapply (IH … Esteps) cases (is_final … s') 577 [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 578 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 616 [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps) 617 >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 618 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta % 579 619  normalize nodelta #r * 580 620 [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct 581  * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 621  * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps) 622 >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 582 623 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 583 624 ]
Note: See TracChangeset
for help on using the changeset viewer.