Changeset 2839
 Timestamp:
 Mar 11, 2013, 12:18:05 PM (5 years ago)
 Location:
 src/RTLabs
 Files:

 1 added
 1 edited
 1 copied
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_partial_traces.ma
r2800 r2839 1 2 (* This deals with the construction of structured traces of finite parts of 3 RTLabs program executions. It will be used as part of the whole compiler's 4 intensional correctness proof. 5 6 It was originally based on RTLabs/RTLabs_traces.ma, which constructs whole 7 execution structured traces, but dealing with the whole program execution 8 is unnecessary, it requires classical reasoning for deciding when functions 9 terminate and it doesn't fit well with some of the other definitions. 10 11 In principle we could clean this up a little by harmonising some of the 12 definitions with other parts of the development. *) 1 13 2 14 include "RTLabs/RTLabs_abstract.ma". … … 50 62 qed. 51 63 52 (* Before attempting to construct a structured trace, let's show that we can 53 form flat traces with evidence that they were constructed from an execution. 54 As with the structured traces, we only consider good traces (i.e., ones 55 which don't go wrong). 56 57 For now we don't consider I/O. *) 58 59 60 coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ 61  noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) 62  noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) 63  noio_wrong : ∀m. exec_no_io o i (e_wrong … m). 64 65 (* add I/O? *) 66 coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ 67  ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s 64 inductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ 65  ft_stop : ∀s. flat_trace o i ge s 68 66  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s. 69 67 70 let corec make_flat_trace ge s 71 (NF:RTLabs_is_final s = None ?) 72 (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) 73 (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 74 flat_trace io_out io_in ge s ≝ 75 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in 76 match e return λx. e = x → ? with 77 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) 78  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???) 79  e_wrong m ⇒ λE. ⊥ 80  e_interact o f ⇒ λE. ⊥ 81 ] (refl ? e). 82 [ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E; 83 cases (eval_statement ge s) 84 [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct 85  2,5: * #tr #s1 whd in ⊢ (??%? → ?); 86 >(?:is_final ????? = RTLabs_is_final s1) // 87 lapply (refl ? (RTLabs_is_final s1)) 88 cases (RTLabs_is_final s1) in ⊢ (???% → %); 89 [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct % 90  #i #_ whd in ⊢ (??%? → ?); #E destruct @refl 91  #i #E whd in ⊢ (??%? → ?); #E2 destruct 92 ] 93  *: #m whd in ⊢ (??%? → ?); #E destruct 94 ] 95  whd in E:(??%?); >exec_inf_aux_unfold in E; 96 cases (eval_statement ge s) 97 [ #o #K whd in ⊢ (??%? → ?); #E destruct 98  * #tr #s1 whd in ⊢ (??%? → ?); 99 lapply (refl ? (RTLabs_is_final s1)) 100 change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?_⇒?])? → ?); 101 cases (RTLabs_is_final s1) in ⊢ (???% → %); 102 [ #F #E whd in E:(??%?); destruct 103  #r #F #E whd in E:(??%?); destruct >F % #E destruct 104 ] 105  #m #E whd in E:(??%?); destruct 106 ] 107  whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; 108 cases (eval_statement ge s) 109 [ #O #K whd in ⊢ (??%? → ?); #E destruct 110  * #tr #s1 whd in ⊢ (??%? → ?); 111 cases (is_final ?????) 112 [ whd in ⊢ (??%? → ?); #E 113 change with (eval_statement ge s1) in E:(??(??????(?????%))?); 114 destruct 115 inversion H 116 [ #a #b #c #E1 destruct 117  #trx #sx #ex #H1 #E2 #E3 destruct @H1 118  #m #E1 destruct 119 ] 120  #i whd in ⊢ (??%? → ?); #E destruct 121 ] 122  #m whd in ⊢ (??%? → ?); #E destruct 123 ] 124  whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E; 125 cases (eval_statement ge s) 126 [ #O #K whd in ⊢ (??%? → ?); #E destruct 127  * #tr #s1 whd in ⊢ (??%? → ?); 128 cases (is_final ?????) 129 [ whd in ⊢ (??%? → ?); #E 130 change with (eval_statement ge s1) in E:(??(??????(?????%))?); 131 destruct 132 inversion NW 133 [ #a #b #c #E1 #_ destruct 134  #trx #sx #ex #H1 #E2 #E3 destruct @H1 135  #o #k #K #E1 destruct 136 ] 137  #i whd in ⊢ (??%? → ?); #E destruct 138 ] 139  #m whd in ⊢ (??%? → ?); #E destruct 140 ] 141  whd in E:(??%?); >exec_inf_aux_unfold in E; 142 cases (eval_statement ge s) 143 [ #o #K whd in ⊢ (??%? → ?); #E destruct 144  * #tr #s1 whd in ⊢ (??%? → ?); 145 lapply (refl ? (RTLabs_is_final s1)) 146 change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?_⇒?])? → ?); 147 cases (RTLabs_is_final s1) in ⊢ (???% → %); 148 [ #F #E whd in E:(??%?); destruct @F 149  #r #F #E whd in E:(??%?); destruct 150 ] 151  #m #E whd in E:(??%?); destruct 152 ] 153  whd in E:(??%?); >E in NW; #X inversion X 154 #A #B #C #D #E destruct 155  whd in E:(??%?); >E in H; #H inversion H 156 #A #B #C try #D try #E destruct 157 ] qed. 158 159 definition make_whole_flat_trace : ∀p,s. 160 exec_no_io … (exec_inf … RTLabs_fullexec p) → 161 not_wrong … (exec_inf … RTLabs_fullexec p) → 162 make_initial_state ??? p = OK ? s → 163 flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ 164 λp,s,H,NW,I. 165 let ge ≝ make_global … p in 166 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in 167 match e return λx. e = x → ? with 168 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? 169  e_step _ _ e' ⇒ λE. make_flat_trace ge s ??? 170  e_wrong m ⇒ λE. ⊥ 171  e_interact o f ⇒ λE. ⊥ 172 ] (refl ? e). 173 [ whd in E:(??%?); >exec_inf_aux_unfold in E; 174 whd in ⊢ (??%? → ?); 175 change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?_⇒?])? → ?); 176 cases (RTLabs_is_final s) 177 [ #E whd in E:(??%?); destruct 178  #r #E % #E' destruct 179 ] 180  @(initial_state_is_not_final … I) 181  whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?); 182 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????) 183 [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H 184 [ #a #b #c #E1 destruct 185  #tr1 #s1 #e1 #H1 #E1 #E2 E2 I destruct (E1) 186 @H1 187  #o #k #K #E1 destruct 188 ] 189  #i whd in ⊢ (??%? → ??% → ?); #E destruct 190 ] 191  whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); 192 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) 193 [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H 194 [ #a #b #c #E1 destruct 195  #tr1 #s1 #e1 #H1 #E1 #E2 E2 I destruct (E1) 196 @H1 197  #m #E1 destruct 198 ] 199  #i whd in ⊢ (??%? → ???% → ?); #E destruct 200 ] 201  whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 202 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 203  whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); 204 cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct 205 ] qed. 68 let rec make_flat_trace ge n s trace s' (EX:exec_steps n … RTLabs_fullexec ge s = return 〈trace,s'〉) on n : flat_trace io_out io_in ge s ≝ 69 match n return λn. exec_steps n ????? = ? → ? with 70 [ O ⇒ λ_. ft_stop … s 71  S m ⇒ λEX'. 72 match eval_statement ge s return λx. eval_statement ?? = x → ? with 73 [ Value ts ⇒ λEV. ft_step ??? s (\fst ts) (\snd ts) ? (make_flat_trace ge m (\snd ts) (tail … trace) s' ?) 74  _ ⇒ λEV. ⊥ 75 ] (refl ??) 76 ] EX. 77 [ cases (exec_steps_S … EX') #_ * #tr' * #s1 * #tl * * #E #ST #_ 78 change with (eval_statement ??) in ST:(??%?); >EV in ST; 79 #ST destruct 80  // 81  cases (exec_steps_S … EX') #_ * #tr' * #s1 * #tl * * #E #ST #STEPS 82 change with (eval_statement ??) in ST:(??%?); >EV in ST; 83 #ST destruct 84 @STEPS 85  cases (exec_steps_S … EX') #_ * #tr' * #s1 * #tl * * #E #ST #_ 86 change with (eval_statement ??) in ST:(??%?); >EV in ST; 87 #ST destruct 88 ] qed. 89 90 lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'. 91 ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉. 92 Σs1. ∃ST,EX'. make_flat_trace ge (S n) s (hd::trace) s' EX = ft_step ??? s (\snd hd) s1 ST (make_flat_trace ge n s1 trace s' EX'). 93 #ge #n #s #hd #trace #s' #EX 94 lapply (refl ? (eval_statement ge s)) 95 cases (eval_statement ge s) in ⊢ (???% → ?); 96 [ #o #k  3: #m ] 97 [ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct 98 change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct 99 ] * #tr #s1 #EV 100 %{s1} 101 cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct 102 change with (eval_statement ??) in ⊢ (??%? → ?); >EV in ⊢ (% → ?); #E destruct #EX' 103 %{EV} %{EX'} 104 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); 105 >EV in ⊢ (???% → ??(match % with [_⇒?_⇒?_⇒?]?)?); 106 #ST' whd in ⊢ (??%?); % 107 qed. 206 108 207 109 (* Need a way to choose whether a called function terminates. Then, … … 928 830 myge ? (times 3 (will_return_length ??? trace TM)) → 929 831 sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with 930 [ ft_stop st FINAL⇒832 [ ft_stop st ⇒ 931 833 λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 932 834 … … 1489 1391 @⊥ @(absurd ?? CL) @refl 1490 1392 qed. 1491 1393 (* 1492 1394 definition termination_oracle ≝ ∀ge,depth,s,trace. 1493 1395 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). … … 1637 1539 ] 1638 1540 ] qed. 1639 1541 *) 1640 1542 lemma simplify_cl : ∀ge,s,c. 1641 1543 as_classifier (RTLabs_status ge) s c → … … 1645 1547 destruct // 1646 1548 qed. 1647 1549 (* 1648 1550 (* NB: This isn't quite what I'd like. Ideally, we'd show the existence of 1649 1551 a trace_label_diverges value, but I only know how to construct those … … 1777 1679 ] 1778 1680 ] qed. 1779 1681 *) 1780 1682 lemma init_state_is : ∀p,s. 1781 1683 make_initial_state p = OK ? s → … … 1828 1730 * #id * #fn // * /2/ 1829 1731 qed. 1830 1732 (* 1831 1733 theorem program_trace_exists : 1832 1734 termination_oracle → … … 1858 1760  @(proj2 ?? (well_cost_labelled_initial … I WCL)) 1859 1761 ] qed. 1860 1762 *) 1861 1763 1862 1764 lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge. … … 1989 1891 [ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac 1990 1892 ] EX''. 1991 1893 (* 1992 1894 (* Now reconstruct the flat_trace of a diverging execution. Note that we need 1993 1895 to take care to satisfy the guardedness condition by witnessing the fact that … … 2085 1987 @flat_traces_are_determined_by_starting_point 2086 1988 qed. 2087 1989 *) 2088 1990 2089 1991 
src/RTLabs/RTLabs_traces.ma
r2760 r2839 1 2 (* This file shows that structured traces can be generated for entire executions 3 of RTLabs programs (given no failure or I/O). It stands alone; the file 4 RTLabs/RTLabs_partial_traces.ma contains a finite variant that is used for 5 the compiler proofs. *) 1 6 2 7 include "RTLabs/RTLabs_abstract.ma".
Note: See TracChangeset
for help on using the changeset viewer.