Changeset 3081 for src/Clight
 Timestamp:
 Apr 3, 2013, 5:54:34 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCastsMeasurable.ma
r3063 r3081 2 2 include "common/FEMeasurable.ma". 3 3 include "Clight/Clight_classified_system.ma". 4 5 (* TODO: move *)6 lemma step_not_final : ∀ge,s,tr,s'.7 exec_step ge s = Value … 〈tr,s'〉 →8 is_final s = None ?.9 #ge * //10 #r #tr #s' #ST whd in ST:(??%?); destruct11 qed.12 4 13 5 lemma state_cast_labelled : ∀s,s'. … … 35 27 ] 36 28 ] qed. 29 30 (* Put cast simplification simulation into form that FEMeasurable needs. 31 Note that sim_call_label is just sticking together two normal steps  we 32 never add extra steps here, so we don't need to worry about moving cost 33 labels to the start of the function. *) 37 34 38 35 definition simplify_measurable_sim : meas_sim ≝ … … 86 83 cases (cast_correction … RG … S1 ST) 87 84 #s2' * #ST' #S2 %{1} whd 88 whd in match (is_final … s1'); >( step_not_final … ST')85 whd in match (is_final … s1'); >(cl_step_not_final … ST') 89 86 whd whd in match (step … Clight_pcs ge' s1'); >ST' 90 87 whd % [ %  assumption ] … … 93 90 cases (cast_correction … RG … S1 ST) 94 91 #s2' * #ST' #S2 %{0} whd 95 whd in match (is_final … s1'); >( step_not_final … ST')92 whd in match (is_final … s1'); >(cl_step_not_final … ST') 96 93 whd whd in match (step … Clight_pcs ge' s1'); >ST' 97 94 whd % [ %  assumption ] … … 103 100 #s3' * #ST2' #S3 104 101 %{1} whd 105 whd in match (is_final … s1'); >( step_not_final … ST1')102 whd in match (is_final … s1'); >(cl_step_not_final … ST1') 106 103 whd whd in match (step … Clight_pcs ge' s1'); >ST1' 107 104 whd % [ % [ %  change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ] 108 whd whd in match (is_final … s2'); >( step_not_final … ST2')105 whd whd in match (is_final … s2'); >(cl_step_not_final … ST2') 109 106 whd whd in match (step … Clight_pcs ge' s2'); >ST2' 110 107 whd % [ %  assumption ] … … 114 111 #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ] 115 112 whd 116 whd in match (is_final … s1'); >( step_not_final … ST')113 whd in match (is_final … s1'); >(cl_step_not_final … ST') 117 114 whd whd in match (step … Clight_pcs ge' s1'); >ST' 118 115 whd % [ >(return_E0 … ST) // assumption  assumption ] … … 121 118 cases (cast_correction … RG … S1 ST) 122 119 #s2' * #ST' #S2 whd 123 whd in match (is_final … s1'); >( step_not_final … ST')120 whd in match (is_final … s1'); >(cl_step_not_final … ST') 124 121 whd whd in match (step … Clight_pcs ge' s1'); >ST' 125 122 whd % [ %  assumption ] 
src/Clight/SwitchAndLabel.ma
r3047 r3081 2 2 include "Clight/labelSimulation.ma". 3 3 4 5 lemma after_aux_result : ∀avs,n,s,tr,P. 6 after_aux avs n s tr P → 7 ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 8 #avs #n elim n 9 [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A  % ] 10  #n' #IH #s #tr #P 11 whd in ⊢ (% → ?); 12 lapply (refl ? (is_final … s)) 13 cases (is_final … s) in ⊢ (???% → %); 14 [ #F whd in ⊢ (% → ?); 15 lapply (refl ? (step … s)) 16 cases (step … s) in ⊢ (???% → %); 17 [ #o #k #_ * 18  * #tr1 #s1 #ST whd in ⊢ (% → ?); 19 cases n' in IH ⊢ %; 20 [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd %  skip ]  skip ] 21  #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %); 22 [ #INV #AF 23 cases (IH … AF) #tr' * #s' * #p #AF' 24 % [2: % [2: %{p} whd >F whd >ST whd >INV @AF'  skip ]  skip ] 25  #_ * 26 ] 27 ] 28  #m #_ * 29 ] 30  #r #F * 31 ] 32 ] qed. 33 34 lemma after_n_result : ∀n,O,I,exec,g,s,P,inv. 35 after_n_steps n O I exec g s inv P → 36 ∃tr',s'. 37 P tr' s' ∧ 38 after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 39 #n #O #I #exec #g #s #P #inv #A 40 cases (after_aux_result … A) #tr * #s' * #p #A' 41 %{tr} %{s'} %{p} @A' 42 qed. 43 44 45 lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s. 46 after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) → 47 ∃tr1,tr2,s1. 48 is_final … exec g s = None ? ∧ 49 step … exec g s = Value … 〈tr1,s1〉 ∧ 50 tr = tr1⧺tr2 ∧ 51 after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉). 52 #n #O #I #exec #g #tr #s' #s #A 53 cases (after_1_of_n_steps … A) 54 #tr1 * #s1 * * * #F #ST #_ #A' 55 cases (after_n_result … A') 56 #tr'' * #s'' * #E #A'' destruct 57 % [2: % [2: % [2: % [ % [% [ @F  @ST ]  % ]  @A'' ]  skip ]  skip ]  skip ] 58 qed. 59 60 theorem steps_with_labels : ∀ge,ge'. 4 (* Combine the results about switch removal and labelling to provide a single 5 result linking the input Clight program with the cost labelled Clight 6 program. *) 7 8 (* First lift the step result for labelling to a finite run of steps. *) 9 10 lemma steps_with_labels : ∀ge,ge'. 61 11 related_globals_gen … label_fundef ge ge' → 62 12 ∀n,s1,s1',tr,s2. … … 138 88 #tr #s #tr' #s' #E destruct % 139 89 qed. 90 91 (* Now build the coinduction simulation, taking one step to many after switch 92 removal, then use steps_with_labels to take those to the cost labelled 93 version. *) 140 94 141 95 let corec build_exec … … 210 164 ] qed. 211 165 166 (* And deal with the start of the program to tie up everything nicely. *) 167 212 168 theorem switch_and_labelling_sim : ∀p. 213 169 let e1 ≝ exec_inf … clight_fullexec p in
Note: See TracChangeset
for help on using the changeset viewer.