Changeset 2895 for src/RTLabs/MeasurableToStructured.ma
 Timestamp:
 Mar 16, 2013, 9:08:19 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2894 r2895 55 55 do m ← init_mem … (λx.[Init_space x]) p; 56 56 let main ≝ prog_main ?? p in 57 do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);57 do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); 58 58 do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b); 59 59 let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in 60 60 return (mk_RTLabs_ext_state (make_global p) s [b] ?). 61 % [ @Ef % ]61 % [ % assumption  % ] 62 62 qed. 63 63 … … 67 67 #p #s #E 68 68 cases (bind_inversion ????? E) E #m * #E1 #E 69 cases (bind_ inversion ????? E) E #b * #E2#E69 cases (bind_as_inversion ????? E) E #b * #Eb #E 70 70 cases (bind_as_inversion ????? E) E #f * #Ef #E 71 71 whd in ⊢ (??%?); >E1 72 whd in ⊢ (??%?); >E 272 whd in ⊢ (??%?); >Eb 73 73 whd in ⊢ (??%?); >Ef 74 74 whd in E:(??%%) ⊢ (??%?); destruct … … 81 81 #p #s #E 82 82 cases (bind_inversion ????? E) E #m * #E1 #E 83 cases (bind_inversion ????? E) E #b * #E 2#E83 cases (bind_inversion ????? E) E #b * #Eb #E 84 84 cases (bind_inversion ????? E) E #f * #Ef #E 85 85 whd in E:(??%%); destruct 86 %{[b]} % [ % [ @Ef % ] ]86 %{[b]} % [ % [ % assumption  % ] ] 87 87 whd in ⊢ (??%?); >E1 88 whd in ⊢ (??%?); >E2 88 whd in ⊢ (??%?); generalize in match (refl ??); 89 >Eb in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Eb' 89 90 whd in ⊢ (??%?); generalize in match (refl ??); 90 91 >Ef in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)?); #Ef' % … … 140 141 lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. 141 142 will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace → 142 will_return ge depth s (make_flat_trace ge n s trace s' EX). 143 ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX). 144 will_return_end … WR = ?. 145 [2: %{s'} @ft_stop ] (* XXX replace ? above? *) 143 146 #ge #trace0 elim trace0 144 147 [ #depth #n #s #s' #EX * … … 169 172 [ #EX #_ 170 173 lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) 171 @wr_base 172 destruct @CL 174 %{(wr_base …)} 175 [ destruct @CL 176  cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?); 177 whd in cEX:(??%%); destruct % 178 ] 173 179  * #s3 #tr3 #tl3 #EX * 174 180 ] 175 181  #depth' whd in ⊢ (?% → ?); #H 176 182 lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) 177 @wr_ret 178 [ destruct @CL 179  @IH @H 183 cases (IH ???? (cft_EX … CFT) H) #WR' #WRe 184 %{(wr_ret …)} 185 [ @WR' 186  destruct @CL 187  @WRe 180 188 ] 181 189 ] 182 190  #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) 183 @wr_step [ %2 destruct @CL  @IH @H ] 191 cases (IH ???? (cft_EX … CFT) H) #WR' #WRe 192 %{(wr_step …)} [ @WR'  %2 destruct @CL  @WRe ] 184 193  #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) 185 @wr_call [ destruct @CL  @IH @H ] 194 cases (IH ???? (cft_EX … CFT) H) #WR' #WRe 195 %{(wr_call …)} [ @WR'  destruct @CL  @WRe ] 186 196  cases (RTLabs_notail … CL) 187 197  #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) 188 @wr_step [ %1 destruct @CL  @IH @H ] 189 ] 190 ] qed. 198 cases (IH ???? (cft_EX … CFT) H) #WR' #WRe 199 %{(wr_step …)} [ @WR'  %1 destruct @CL  @WRe ] 200 ] 201 ] qed. 202 191 203 192 204 lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. … … 446 458 ] qed. 447 459 460 lemma really_no_label : ∀ge,s,obs. 461 ¬as_costed (RTLabs_status ge) s → 462 maybe_label ge s obs = obs. 463 #ge #s #obs 464 whd in ⊢ (?% → ??%?); 465 cases (as_label ??) 466 [ // 467  #l * #H @⊥ @H % #E destruct 468 ] qed. 469 470 448 471 lemma call_ret_event : ∀ge,s,tr,s',obs. 449 472 step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 → … … 478 501 ] qed. 479 502 503 lemma as_call_cs_callee : ∀ge,s,CL,CL'. 504 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'. 505 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E 506 destruct % 507 qed. 508 480 509 lemma itot_call : ∀C,cs,s,rem,cs',trace. 481 510 ∀CL:match cs_classify C s with [ cl_call ⇒ True  _ ⇒ False ]. … … 491 520 qed. 492 521 493 (* WIP 494 lemma as_call_cs_callee : ∀ge,s,CL,CL'. 495 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'. 496 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E 497 destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL' 498 whd in ⊢ (??%%); cases (symbol_for_block ??) 499 522 lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs. 523 as_classifier (RTLabs_status ge) s cl_other → 524 step … RTLabs_ext_pcsys ge s = Value ??? 〈tr,s'〉 → 525 intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 → 526 ∃obs'. 527 obs = (intensional_events_of_events tr) @ obs' ∧ 528 intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs rem = 〈cs',obs'〉. 529 #ge #cs #s #tr #s' #rem #cs #obs #CL #EX 530 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?); 531 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?); 532 >CL #name whd in ⊢ (??%? → ?); 533 cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct 534 %{trace''} /2/ 535 qed. 500 536 501 537 (* observables_trace_label_label emits the cost label for the first step of the … … 527 563 @(eq_obs_tal … EX ITOT) 528 564  cases tal 529 [ #s1 #s2 #ST * #CL #CS #EX565 [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL 530 566 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 531 567 whd in EX:(??%?); destruct … … 555 591 cases (eq_obs_tlr … EX ITOT') 556 592 #OBS' #E4 <E4 % 557 [ >E3 <OBS' whd in ⊢ (??%?); 558 559 560 561 562 ] qed. 563 *) 564 593 [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) % 594  % 595 ] 596  #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL) 597  #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX 598 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX 599 cases (call_ret_event … ST') 600 [ #E2 #E3 >E2 >E3  skip  %1 @CL ] #ITOT 601 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ] 602 #obs' * #E4 #ITOT' 603 <(as_exec_eq_step … ST ST') in EX; #EX 604 cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E 605 >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs 606 lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1 607 cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2 608 cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' % 609 [ >E4 whd in ⊢ (??%?); 610 <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1' 611 >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2' 612 <Eobs % 613  @CS_CH' 614 ] 615  #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX 616 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX 617 #ITOT cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT' 618 <(as_exec_eq_step … ST ST') in EX; #EX 619 cases (eq_obs_tal … EX ITOT') 620 >(really_no_label … CS) #OBS' #CS_CH 621 >(step_cost_event … ST') <OBS' 622 % [ %  @CS_CH ] 623 ] 624 ] qed. 625 626 627 (* TODO move *) 628 lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX. 629 length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n. 630 #ge #n0 elim n0 631 [ #s1 #trace #s2 #EX % 632  #n #IH #s1 #trace #s2 #EX 633 cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct 634 cases (cons_flat_trace ?????? EX) 635 #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH 636 ] qed. 637 638 639 lemma cost_state_is_in_function : ∀ge,s,S,M. 640 RTLabs_cost (mk_RTLabs_ext_state ge s S M) → 641 ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id. 642 #ge * 643 [ #f #fs #m * [*] #fn #S' * #FFP #M #_ 644 %{fn} %{S'} %{(symbol_of_function_block' … FFP)} 645 % [ %  @symbol_of_function_block_ok [ >FFP % #E destruct  % ] ] 646  #fid #fn #args #ret #fs #m #S #M * 647  #rv #rr #fs #m #S #M * 648  #r #S #M * 649 ] qed. 565 650 566 651 … … 594 679 cases (initial_states_OK' … INIT) #S * #M #INIT' 595 680 cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1) 596 #prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1' 681 #prefix'' * #S1 * #M1 682 lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1 683 lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct 684 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' 685 cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END 597 686 lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????) 598 [ @ will_return_equiv assumption599  @ (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)687 [ @RETURNS' 688  @CS1 600 689  @(well_cost_labelled_exec_steps … EXEC1) 601 690 [ assumption … … 603 692 ] 604 693  @WCLge 605  * #s2' #rem #_ #tlr #LEN #STACK #_ 606 %{s1'} %{s2'} % [2: %{tlr} 694  * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?); 695 >RETURNS_END #E destruct 696 %{s1'} %{s2'} %{fn} %{tlr} 607 697 % [ % [ % 608 698 [ whd in ⊢ (??%?); … … 618 708 ] 619 709 ] 620 ] 710 ] cut (length_tlr … tlr = n) 711 [ lapply (make_flat_trace_length ????? EXEC2) <LEN 712 <plus_n_O @(λx.x) ] 713 #LEN' <LEN' in EXEC2; #EXEC2 714 cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting''' 715 lapply (eq_obs_tlr ????????? EXEC2) 621 716 ] 622 717 ]] 623 718 624
Note: See TracChangeset
for help on using the changeset viewer.