Changeset 3156
 Timestamp:
 Apr 17, 2013, 3:24:22 PM (6 years ago)
 Location:
 src
 Files:

 1 deleted
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r3145 r3156 624 624 ] qed. 625 625 626 (* TODO: move to somewhere common *) 627 definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝ 628 λC,p,m. 629 let g ≝ make_global … (pcs_exec … C) p in 630 let C' ≝ pcs_to_cs C g in 631 ! s0 ← make_initial_state … p; 632 ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; 633 return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉. 634 635 636 (* I'm not entirely certain that existentially quantifying fn is the right thing 637 to do. In principle we must provide the right one to satisfy the condition 638 about observables, but perhaps we ought to show how to produce it explicitly. 639 *) 640 626 (* We need to put the prefix of the measurable trace into the backend's 627 preferred form of flat trace. For some reason this is backwards. 628 629 As well as forming the trace itself, we need to show that the definition 630 for extracting observables and the call stack for stack space gives the same 631 answer, and that a side condition from the fact that the program is well cost 632 labelled is fulfilled (I don't think that is strictly necessary, but allows 633 the simulation results for structured traces to be reused for the flat 634 ones). *) 635 636 include "common/StatusSimulation.ma". 637 638 (* Backwards version of exec_steps_S *) 639 640 lemma exec_steps_snoc_inv : ∀O,I,fx,g,n,s,trace,s''. 641 exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 → 642 ∃tr',s',liat. 643 is_final … fx g s' = None ? ∧ 644 trace = liat@[〈s',tr'〉] ∧ 645 step … fx g s' = Value … 〈tr',s''〉 ∧ 646 exec_steps n O I fx g s = OK … 〈liat,s'〉. 647 #O #I #fx #g #n elim n 648 [ #s #trace #s'' 649 whd in ⊢ (??%? → ?); 650 lapply (refl ? (is_final … s)) 651 cases (is_final … s) in ⊢ (???% → %); 652 [ #NF  #r #F #EXEC whd in EXEC:(??%%); destruct ] 653 whd in ⊢ (??%? → ?); 654 lapply (refl ? (step … s)) 655 cases (step … s) in ⊢ (???% → %); 656 [ #o #k #_ #EXEC whd in EXEC:(??%%); destruct  3: #m #_ #EXEC whd in EXEC:(??%%); destruct ] 657 * #tr' #s' #STEP whd in ⊢ (??%% → ?); #E destruct 658 %{tr'} %{s} %{[ ]} % [ % [ % [ @NF  % ]  @STEP ]  % ] 659  #m #IH 660 #s #trace #s'' 661 whd in ⊢ (??%? → ?); 662 lapply (refl ? (is_final … s)) 663 cases (is_final … s) in ⊢ (???% → %); 664 [ #NF  #r #F #EXEC whd in EXEC:(??%%); destruct ] 665 whd in ⊢ (??%? → ?); 666 lapply (refl ? (step … s)) 667 cases (step … s) in ⊢ (???% → %); 668 [ #o #k #_ #EXEC whd in EXEC:(??%%); destruct  3: #m #_ #EXEC whd in EXEC:(??%%); destruct ] 669 * #tr' #s' #STEP whd in ⊢ (??%% → ?); 670 lapply (refl ? (exec_steps (S m) O I fx g s')) cases (exec_steps … s') in ⊢ (???% → %); 671 [2: #m #_ #E whd in E:(??%?); destruct ] 672 * #trace' #s''' #EXEC' #E whd in E:(??%%); destruct 673 cases (IH … EXEC') #tr'' * #s''' * #liat * * * #NF' #E destruct #STEP' #EXEC'' 674 %{tr''} %{s'''} %{(〈s,tr'〉::liat)} % [ % [ % [ @NF'  % ]  @STEP' ] 675 whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >EXEC'' % 676 ] 677 ] qed. 678 679 lemma RTLabs_step_tr_matches_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. 680 eval_statement ge s = Value … 〈tr,s'〉 → 681 intensional_events_of_events tr = option_to_list … (! l ← as_label (RTLabs_status ge) s; return IEVcost l). 682 #ge #s #tr #s' #EV 683 cases (only_plain_step_events_is_one_cost … EV) 684 [ * #cl * #E1 #CS >E1 <RTLabs_as_label >CS % 685  * #E1 >E1 #CS <RTLabs_as_label >CS % 686 ] qed. 687 688 lemma RTLabs_return_not_label : ∀ge,s. 689 as_classify (RTLabs_status ge) s = cl_return → 690 as_label … s = None ?. 691 #ge * * 692 [ #f #fs #m #S #M whd in ⊢ (??%? → ?); cases (next_instruction f) normalize nodelta #a try #b try #c try #d try #e try #f try #g try #h try #i destruct 693  #a #b #c #d #e #f #g #h #E whd in E:(??%?); destruct 694  #a #b #c #d * [2: #e #f] #g #h % 695  // 696 ] qed. 697 698 lemma RTLabs_call_not_label : ∀ge,s. 699 as_classify (RTLabs_status ge) s = cl_call → 700 as_label … s = None ?. 701 #ge * * 702 [ #f #fs #m #S #M whd in ⊢ (??%? → ?); cases (next_instruction f) normalize nodelta #a try #b try #c try #d try #e try #f try #g try #h try #i destruct 703  #a #b #c #d #e #f * [*] #g #h #i #j % 704  #a #b #c #d * [2: #e #f] #g #h % 705  // 706 ] qed. 707 708 (* The main part of showing the the observables and call stack are the same. *) 709 710 lemma extend_ft_stack_observables : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀ft,cs',cs,itr,itr',tr,H1,H2. 711 eval_statement ge s2 = Value … 〈tr,s3〉 → 712 ft_stack_observables (RTLabs_status ge) s1 s2 ft = 〈cs',itr'〉 → 713 intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcs ge) cs' [〈s2,tr〉] = 〈cs,itr〉 → 714 ft_stack_observables (RTLabs_status ge) s1 s3 (ft_advance (RTLabs_status ge) s1 s2 s3 ft H1 H2) = 〈cs,itr'@itr〉. 715 #ge #s1 #s2 #s3 #ft #cs' #cs #itr #itr' #tr #H1 #H2 #EVAL #FT 716 whd in ⊢ (??%? → ?); @pair_elim #cs1 #itr1 #ITR1 717 whd in ⊢ (??%? → ?); #ITR2 destruct >(RTLabs_step_tr_matches_label … EVAL) >append_nil 718 whd in ⊢ (??%?); >FT FT 719 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); cases (as_classify (RTLabs_status ge) s2) in ⊢ (???% → %); 720 #CL whd in ⊢ (??%?); 721 [ cases cs' in ITR1 ⊢ %; [2: #fn #cs1 ] 722 whd in ⊢ (??%? → ??%?); 723 generalize in ⊢ (??(?%)? → ?); 724 change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??); 725 >CL #f whd in ⊢ (??%? → ?); #E destruct >(RTLabs_return_not_label … CL) % 726  whd in ITR1:(??%?); lapply ITR1 generalize in ⊢ (??(?%)? → ?); 727 change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??); 728 >CL #f whd in ⊢ (??%? → ?); #E destruct % 729  cut (match cs_classify (pcs_to_cs RTLabs_ext_pcs ge) s2 with [ cl_call ⇒ True  _ ⇒ False ]) 730 [ change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??); >CL % ] 731 #CL' 732 >(as_call_cs_callee … CL') change with (cs_callee (pcs_to_cs RTLabs_ext_pcs ge) s2 CL') in match (cs_callee ???); 733 whd in ITR1:(??%?); lapply ITR1 @(generalize_callee … CL') 734 change with (cs_classify (pcs_to_cs RTLabs_ext_pcs ge) s2) in match (as_classify ??) in CL; 735 >CL in CL' ⊢ %; * #f whd in ⊢ ( 736 ??%? → ?); #E destruct 737 >(RTLabs_call_not_label ?? CL) % 738  cases (RTLabs_notail … CL) 739  whd in ITR1:(??%?); lapply ITR1 generalize in ⊢ (??(?%)? → ?); 740 change with (as_classify (RTLabs_status ge) s2) in match (cs_classify ??); 741 >CL #f whd in ⊢ (??%? → ?); #E destruct % 742 ] qed. 743 744 (* The side condition concerning cost labelling. *) 745 746 lemma RTLabs_enforce_costedness : ∀ge,tr. ∀s,s':RTLabs_ext_state ge. 747 well_cost_labelled_state (Ras_state … s) → 748 eval_statement ge s = Value … 〈tr,s'〉 → 749 enforce_costedness (RTLabs_status ge) s s'. 750 #ge #tr #s #s' #WCL #EVAL 751 lapply (well_cost_labelled_jump … EVAL WCL) 752 whd in ⊢ (? → %); whd in match (is_cl_jump ??); 753 change with (RTLabs_classify s) in match (as_classify ??); 754 cases (RTLabs_classify s) // 755 #H @(proj1 … (RTLabs_costed …)) @H % 756 qed. 757 758 lemma well_cost_labelled_exec_ext_steps : ∀n,g. ∀s:RTLabs_ext_state g.∀trace.∀s':RTLabs_ext_state g. 759 well_cost_labelled_ge g → 760 exec_steps n ?? RTLabs_ext_fullexec g s = OK ? 〈trace,s'〉 → 761 well_cost_labelled_state s → 762 well_cost_labelled_state s'. 763 #n #g elim n 764 [ #s #trace #s' #_ #E whd in E:(??%%); destruct // 765  #m #IH #s #trace #s' #WCLge #EX 766 cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' 767 #WCLs @(IH … WCLge … EX') 768 @(well_cost_labelled_state_step … (drop_exec_ext … STEP) WCLge WCLs) 769 ] qed. 770 771 lemma build_back_end_flat_trace : ∀ge,n,s0,tr,s1,cs,itr. 772 exec_steps n … RTLabs_ext_fullexec ge s0 = return 〈tr,s1〉 → 773 well_cost_labelled_ge ge → 774 well_cost_labelled_state (Ras_state … s0) → 775 intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcs ge) [ ] tr = 〈cs,itr〉 → 776 ∃ft:flat_trace (RTLabs_status ge) s0 s1. 777 ft_stack_observables … ft = 〈cs,itr〉. 778 #ge #n elim n 779 [ #s0 #tr #s1 #cs #itr #EXEC #_ #_ #ITOT 780 whd in EXEC:(??%%); destruct whd in ITOT:(??%%); destruct 781 %{(ft_start …)} % 782  #m #IH #s0 #tr #s1 #cs #itr #EXEC #WCLge #WCL0 783 cases (exec_steps_snoc_inv … EXEC) 784 #tr' * #s' * #liat * * * #NF #E #STEP #EXEC' destruct 785 >int_trace_append' @pair_elim #cs1 #itr1 @pair_elim #cs2 #itr2 #ITOT2 #ITOT1 786 #E destruct 787 cases (IH … EXEC' WCLge WCL0 ITOT1) 788 #ft #FT %{(ft_advance … ft ??)} 789 [ @(RTLabs_enforce_costedness … (drop_exec_ext … STEP)) 790 @(well_cost_labelled_exec_ext_steps … EXEC') // 791  @(as_eval_ext_statement … STEP) 792  @(extend_ft_stack_observables … FT ITOT2) @drop_exec_ext @STEP 793 ] 794 ] qed. 795 796 797 (* Now bring the parts together. *) 641 798 642 799 theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting. … … 644 801 measurable RTLabs_pcs p m n stack_cost max → 645 802 observables RTLabs_pcs p m n = return 〈prefix,interesting〉 → 646 ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 647 exec_steps_with_obs RTLabs_ext_pcs p m = return 〈sm, prefix〉 ∧ 803 ∃s0,sm,sn,fn. 804 make_ext_initial_state p = return s0 ∧ 805 ∃ft:flat_trace (RTLabs_status (make_global p)) s0 sm. 806 ft_current_function … ft = Some … fn ∧ 807 ft_observables … ft = prefix ∧ 808 ∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. 648 809 tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧ 649 810 le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧ … … 686 847  * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?); 687 848 >RETURNS_END #E destruct 688 %{ s1'} %{s2'} %{fn} %{tlr}689 % [ % [ % 690 [ whd in ⊢ (??%?); 691 change with (make_ext_initial_state p) in match (make_initial_state ????); 692 >INIT' whd in ⊢ (??%?); 693 >EXEC1' whd in ⊢ (??%?); >ITOT1'%694 @tlr_sound_unrepeating849 %{(mk_RTLabs_ext_state (make_global p) s0 S M)} %{s1'} %{s2'} %{fn} %{INIT'} 850 cases (build_back_end_flat_trace … EXEC1' WCLge ? ITOT1') 851 [2: @(proj1 … (well_cost_labelled_initial … INIT WCLP)) ] 852 #ft #FTobs %{ft} % [ % [ whd in ⊢ (??%?); whd in match (ft_stack ????); >FTobs %  whd in ⊢ (??%?); >FTobs % ] ] 853 %{tlr} 854 % [ % 855 [ @tlr_sound_unrepeating 695 856 [ @SLge 696 857  @(soundly_labelled_exec_steps … EXEC1) … … 699 860 ] 700 861 ] 701 ] >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)862  >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x) 702 863 ] cut (length_tlr … tlr = n) 703 864 [ lapply (make_flat_trace_length ????? EXEC2) <LEN … … 708 869 ] 709 870 ] qed. 710 
src/correctness.ma
r3145 r3156 23 23 let ctrace ≝ costlabels_of_observables itrace in 24 24 Σ_{l ∈ ctrace}(costmap l). 25 26 definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝ 27 λC,p,m. 28 let g ≝ make_global … (pcs_exec … C) p in 29 let C' ≝ pcs_to_cs C g in 30 ! s0 ← make_initial_state … p; 31 ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; 32 return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉. 25 33 26 34 definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝ … … 85 93 86 94 (* atm they are all axioms *) 87 include "RTLabs/RTLabsExecToTrace.ma".88 95 include "RTLabs/RTLabsToRTLAxiom.ma". 89 96 include "RTL/RTL_separate_to_overflow.ma". … … 166 173 #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs cm_m1 cm_m2 167 174 #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS) 168 #ra_s 1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix#ra_unrepeating #ra_max #ra_obs'175 #ra_s0 * #ra_s1 * #ra_s2 * #fn * #ra_init * #ra_ft * * #ra_ft_fn #ra_ft_obs * #ra_tlr * * #ra_unrepeating #ra_max #ra_obs' 169 176 >OBS ra_meas 170 cases (produce_rtlabs_flat_trace … ra_exec_prefix)171 #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs172 177 %{prefix} %{subtrace} %{fn} %[%] 173 %{ra_init_ok ra_max} 174 %{ra_unrepeating EQ_ra_pref_obs ra_obs'} 175 (* fn is the current function ... *) cases daemon 178 %{ra_init ra_max} 179 %{ra_unrepeating ra_ft_obs ra_ft_fn ra_obs'} 176 180 qed. 177 181
Note: See TracChangeset
for help on using the changeset viewer.