source: src/RTLabs/Traces.ma @ 1595

Last change on this file since 1595 was 1595, checked in by campbell, 8 years ago

We don't need an explicit termination count when building traces.

File size: 27.1 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5discriminator status_class.
6
7(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
8       will be added later (LTL → LIN). *)
9
10definition RTLabs_classify : state → status_class ≝
11λs. match s with
12[ State f _ _ ⇒
13    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
14    [ St_cond _ _ _ ⇒ cl_jump
15    | St_jumptable _ _ ⇒ cl_jump
16    | _ ⇒ cl_other
17    ]
18| Callstate _ _ _ _ _ ⇒ cl_call
19| Returnstate _ _ _ _ ⇒ cl_return
20].
21
22definition is_cost_label : statement → bool ≝
23λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
24
25definition RTLabs_cost : state → bool ≝
26λs. match s with
27[ State f fs m ⇒
28    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
29| _ ⇒ false
30].
31
32definition RTLabs_status : genv → abstract_status ≝
33λge.
34  mk_abstract_status
35    state
36    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
37    (λs,c. RTLabs_classify s = c)
38    (λs. RTLabs_cost s = true)
39    (λs,s'. match s with
40      [ dp s p ⇒
41        match s return λs. RTLabs_classify s = cl_call → ? with
42        [ Callstate fd args dst stk m ⇒
43          λ_. match s' with
44          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
45          | _ ⇒ False
46          ]
47        | State f fs m ⇒ λH.⊥
48        | _ ⇒ λH.⊥
49        ] p
50      ]).
51[ normalize in H; destruct
52| whd in H:(??%?);
53  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
54  normalize try #a try #b try #c try #d try #e try #g try #h destruct
55] qed.
56
57(* Before attempting to construct a structured trace, let's show that we can
58   form flat traces with evidence that they were constructed from an execution.
59   
60   For now we don't consider I/O. *)
61
62
63coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
64| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
65| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
66| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
67
68(* add I/O? *)
69coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
70| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
71| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
72| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
73
74let corec make_flat_trace ge s
75  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
76  flat_trace io_out io_in ge s ≝
77let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
78match e return λx. e = x → ? with
79[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
80| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
81| e_wrong m ⇒ λE. ft_wrong … s m ?
82| e_interact o f ⇒ λE. ⊥
83] (refl ? e).
84[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
85  cases (eval_statement ge s)
86  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
87  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
88    >(?:is_final ????? = RTLabs_is_final s1) //
89    lapply (refl ? (RTLabs_is_final s1))
90    cases (RTLabs_is_final s1) in ⊢ (???% → %);
91    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
92    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
93    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
94    ]
95  | *: #m whd in ⊢ (??%? → ?); #E destruct
96  ]
97| whd in E:(??%?); >exec_inf_aux_unfold in E;
98  cases (eval_statement ge s)
99  [ #O #K whd in ⊢ (??%? → ?); #E destruct
100  | * #tr #s1 whd in ⊢ (??%? → ?);
101    cases (is_final ?????)
102    [ whd in ⊢ (??%? → ?); #E destruct @refl
103    | #i whd in ⊢ (??%? → ?); #E destruct
104    ]
105  | #m 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:(??%?); >exec_inf_aux_unfold in E;
125  cases (eval_statement ge s)
126  [ #O #K whd in ⊢ (??%? → ?); #E destruct
127  | * #tr1 #s1 whd in ⊢ (??%? → ?);
128    cases (is_final ?????)
129    [ whd in ⊢ (??%? → ?); #E destruct
130    | #i whd in ⊢ (??%? → ?); #E destruct
131    ]
132  | #m whd in ⊢ (??%? → ?); #E destruct @refl
133  ]
134| whd in E:(??%?); >E in H; #H
135  inversion H
136  [ #a #b #c #E destruct
137  | #a #b #c #d #E1 destruct
138  | #m #E1 destruct
139  ]
140] qed.
141
142let corec make_whole_flat_trace p s
143  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
144  (I:make_initial_state ??? p = OK ? s) :
145  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
146let ge ≝ make_global … p in
147let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
148match e return λx. e = x → ? with
149[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
150| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
151| e_wrong m ⇒ λE. ⊥
152| e_interact o f ⇒ λE. ⊥
153] (refl ? e).
154[ whd in E:(??%?); >exec_inf_aux_unfold in E;
155  whd in ⊢ (??%? → ?);
156  >(?:is_final ????? = RTLabs_is_final s) //
157  lapply (refl ? (RTLabs_is_final s))
158  cases (RTLabs_is_final s) in ⊢ (???% → %);
159  [ #_ whd in ⊢ (??%? → ?); #E destruct
160  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
161  ]
162| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
163  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
164  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
165    [ #a #b #c #E1 destruct
166    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
167      @H1
168    | #m #E1 destruct
169    ]
170  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
171  ]
172| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
173  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
174| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
175  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
176] qed.
177
178(* Need a way to choose whether a called function terminates.  Then,
179     if the initial function terminates we generate a purely inductive structured trace,
180     otherwise we start generating the coinductive one, and on every function call
181       use the choice method again to decide whether to step over or keep going.
182
183Not quite what we need - have to decide on seeing each label whether we will see
184another or hit a non-terminating call?
185
186Also - need the notion of well-labelled in order to break loops.
187
188
189
190outline:
191
192 does function terminate?
193 - yes, get (bound on the number of steps until return), generate finite
194        structure using bound as termination witness
195 - no,  get (¬ bound on steps to return), start building infinite trace out of
196        finite steps.  At calls, check for termination, generate appr. form.
197
198generating the finite parts:
199
200We start with the status after the call has been executed; well-labelling tells
201us that this is a labelled state.  Now we want to generate a trace_label_return
202and also return the remainder of the flat trace.
203
204*)
205
206(* [will_return ge depth s trace] says that after a finite number of steps of
207   [trace] from [s] we reach the return state for the current function.  [depth]
208   performs the call/return counting necessary for handling deeper function
209   calls.  It should be zero at the top level. *)
210inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
211| wr_step : ∀s,tr,s',depth,EX,trace.
212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
213    will_return ge depth s' trace →
214    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
215| wr_call : ∀s,tr,s',depth,EX,trace.
216    RTLabs_classify s = cl_call →
217    will_return ge (S depth) s' trace →
218    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
219| wr_ret : ∀s,tr,s',depth,EX,trace.
220    RTLabs_classify s = cl_return →
221    will_return ge depth s' trace →
222    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
223    (* Note that we require the ability to make a step after the return (this
224       corresponds to somewhere that will be guaranteed to be a label at the
225       end of the compilation chain). *)
226| wr_base : ∀s,tr,s',EX,trace.
227    RTLabs_classify s = cl_return →
228    will_return ge O s (ft_step ?? ge s tr s' EX trace)
229.
230
231discriminator nat.
232
233lemma will_return_call : ∀ge,depth,s,trace.
234  will_return ge depth s trace →
235  will_return ge (pred depth) s trace.
236#ge #depth #s #trace #H elim H
237[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
238| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
239  cases d in H1 H2 ⊢ %; //
240| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
241  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
242| #s1 #tr #s2 #EX #trc #CL %4 //
243] qed.
244
245(*
246(* If we'll return then we must return from calls. *)
247lemma will_return_call : ∀ge,depth,s,trace.
248  will_return ge (S depth) s trace →
249  will_return ge depth s trace.
250#ge #depth #s #trace #H elim H in ⊢ ?;
251[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
252| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
253| #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/
254| #H215 #H216 #H217 #H218 #H219 #H220 #H221
255  inversion H221
256  [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct
257  | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct
258  | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct
259  | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct
260] qed. check will_return_call.
261| #H130 #H131 #H132 #H133 #H134 #H135
262  inversion H
263  [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct
264    cases H196 #E destruct
265 
266
267let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace)
268  on H : will_return ge depth s trace ≝
269match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with
270[ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ?
271| wr_call s tr s' d EX trace CL H' ⇒ λE. ?
272| wr_ret s tr s' d EX trace CL H' ⇒ λE. ?
273| wr_base s tr s' EX trace CL ⇒ λE. ?
274] (refl ? (S depth)).
275[ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H')
276  @(will_return_call … H'')
277| *: cases daemon ] qed.
278| %2 /2/
279| destruct cases d in H' ⊢ %;
280  [ #H' @wr_base //
281  | #d' #H' %3 /2/
282  ]
283| destruct
284] qed.
285
286(* If we'll return then we must return from calls. *)
287lemma will_return_call : ∀ge,depth,s,trace.
288  will_return ge (S depth) s trace →
289  will_return ge depth s trace.
290#ge #depth #s #trace #H lapply (refl ? (S depth))
291generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %);
292[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/
293| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3
294 
295discriminator nat.
296
297
298
299(* Find time until a nested call completes. *)
300lemma nth_is_return_down : ∀ge,n,depth,s,trace.
301  nth_is_return ge n (S depth) s trace →
302  ∃m. nth_is_return ge m depth s trace.
303#ge #n elim n
304(* It's impossible to run out of time... *)
305[ #depth #s #trace #H inversion H
306  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
307  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
308  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
309  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
310  ]
311| #n' #IH #depth #s #trace #H inversion H
312  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
313    cases (IH depth s1' trace1 ?)
314    [ #m' #H' %{(S m')} %1 //
315    | //
316    ]
317  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
318    cases (IH (S depth) s1' trace1 ?)
319    [ #m' #H' %{(S m')} %2 //
320    | //
321    ]
322  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
323    cases (depth1) in H2 ⊢ %;
324    [ #H2 %{O} %4 //
325    | #depth' #H2 cases (IH depth' s1' trace1 ?)
326      [ #m' #H' %{(S m')} %3 //
327      | //
328      ]
329    ]
330  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
331  ]
332] qed.
333
334lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
335  RTLabs_classify s = cl_call →
336  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
337  ∃m. nth_is_return ge m O s' trace.
338#ge #n #s #tr #s' #EX #trace #CLASS #H
339inversion H
340[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
341  -H2 destruct >H1 in CLASS; #E destruct
342| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
343  @nth_is_return_down //
344| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
345  -H2 destruct
346| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
347] qed.
348
349lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
350  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
351  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
352  nth_is_return ge (pred n) O s' trace.
353#ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
354[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
355| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
356| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
357| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
358| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
359| #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
360| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
361| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
362] qed.
363*)
364
365lemma will_return_notfn : ∀ge,s,tr,s',EX,trace.
366  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
367  will_return ge O s (ft_step ?? ge s tr s' EX trace) →
368  will_return ge O s' trace.
369#ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM
370[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
371| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
372| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct
373| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
374| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
375| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
376| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct
377| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
378] qed.
379
380(* We require that labels appear after branch instructions and at the start of
381   functions.  The first is required for preciseness, the latter for soundness.
382   We will make a separate requirement for there to be a finite number of steps
383   between labels to catch loops for soundness (is this sufficient?). *)
384
385definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
386λf,s. match s return λs. labels_present ? s → Prop with
387[ St_cond _ l1 l2 ⇒ λH.
388    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
389    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
390| St_jumptable _ ls ⇒ λH.
391    (* I did have a dependent version of All here, but it's a pain. *)
392    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
393| _ ⇒ λ_. True
394]. whd in H;
395[ @(proj1 … H)
396| @(proj2 … H)
397] qed.
398
399definition well_cost_labelled_fn : internal_function → Prop ≝
400λf. (∀l. ∀H:present … (f_graph f) l.
401         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
402    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
403[ @lookup_lookup_present | cases (f_entry f) // ] qed.
404
405(* We need to ensure that any code we come across is well-cost-labelled.  We may
406   get function code from either the global environment or the state. *)
407
408definition well_cost_labelled_ge : genv → Prop ≝
409λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
410
411definition well_cost_labelled_state : state → Prop ≝
412λs. match s with
413[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
414| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
415                          All ? (λf. well_cost_labelled_fn (func f)) fs
416| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
417].
418
419lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
420  eval_statement ge s = Value ??? 〈tr,s'〉 →
421  well_cost_labelled_ge ge →
422  well_cost_labelled_state s →
423  well_cost_labelled_state s'.
424#ge #s #tr' #s' #EV cases (eval_perserves … EV)
425[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
426| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
427| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
428| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
429| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
430| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
431] qed.
432
433lemma rtlabs_jump_inv : ∀s.
434  RTLabs_classify s = cl_jump →
435  ∃f,fs,m. s = State f fs m ∧
436  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
437  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
438*
439[ #f #fs #m #E
440  %{f} %{fs} %{m} %
441  [ @refl
442  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
443    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
444    [ %1 %{A} %{B} %{C} @refl
445    | %2 %{A} %{B} @refl
446    ]
447  ]
448| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
449| normalize #H8 #H9 #H10 #H11 #H12 destruct
450] qed.
451
452lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
453  eval_statement ge s = Value ??? 〈tr,s'〉 →
454  well_cost_labelled_state s →
455  RTLabs_classify s = cl_jump →
456  RTLabs_cost s' = true.
457#ge #s #tr #s' #EV #H #CL
458cases (rtlabs_jump_inv s CL)
459#fr * #fs * #m * #Es *
460[ * #r * #l1 * #l2 #Estmt
461  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
462  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
463  >Estmt #LP whd in ⊢ (??%? → ?);
464  (* replace with lemma on successors? *)
465  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
466  lapply (Hbody (next fr) (next_ok fr))
467  generalize in ⊢ (???% → ?);
468  >Estmt #LP'
469  whd in ⊢ (% → ?);
470  * #H1 #H2 [ @H1 | @H2 ]
471| * #r * #ls #Estmt
472  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
473  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
474  >Estmt #LP whd in ⊢ (??%? → ?);
475  (* replace with lemma on successors? *)
476  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
477  [ 2: (* later *)
478  | *: #E destruct
479  ]
480  lapply (Hbody (next fr) (next_ok fr))
481  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
482  generalize in ⊢ (??(?%)? → ?);
483  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
484  [ #E1 #E2 whd in E2:(??%?); destruct
485  | #l' #E1 #E2 whd in E2:(??%?); destruct
486    cases (All_nth ???? CP ? E1)
487    #H1 #H2 @H2
488  ]
489] qed.
490
491lemma rtlabs_call_inv : ∀s.
492  RTLabs_classify s = cl_call →
493  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
494* [ #f #fs #m whd in ⊢ (??%? → ?);
495    cases (lookup_present … (next f) (next_ok f)) normalize
496    try #A try #B try #C try #D try #E try #F try #G destruct
497  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
498  | normalize #H411 #H412 #H413 #H414 #H415 destruct
499  ] qed.
500
501lemma well_cost_labelled_call : ∀ge,s,tr,s'.
502  eval_statement ge s = Value ??? 〈tr,s'〉 →
503  well_cost_labelled_state s →
504  RTLabs_classify s = cl_call →
505  RTLabs_cost s' = true.
506#ge #s #tr #s' #EV #WCL #CL
507cases (rtlabs_call_inv s CL)
508#fd * #args * #dst * #stk * #m #E >E in EV WCL;
509whd in ⊢ (??%? → % → ?);
510cases fd
511[ #fn whd in ⊢ (??%? → % → ?);
512  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
513  #m' #b whd in ⊢ (??%? → ?); #E' destruct
514  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
515  @WCL2
516| #fn whd in ⊢ (??%? → % → ?);
517  @bindIO_value #evargs #Eargs
518  @bindIO_value #evres #Eres
519  normalize in Eres; destruct
520] qed.
521
522(* Don't need to know that labels break loops because we have termination. *)
523
524record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
525  new_state : state;
526  remainder : flat_trace io_out io_in ge new_state;
527  cost_labelled : well_cost_labelled_state new_state;
528  new_trace : T new_state
529}.
530
531record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
532  ends : trace_ends_with_ret;
533  trace_res :> trace_result ge (T ends);
534  terminates :
535    (* We handle returns specially *)
536    match ends with
537    [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res)
538    | ends_with_ret ⇒ True
539    ]
540}.
541
542definition replace_sub_trace : ∀ge,T1,T2.
543  ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝
544λge,T1,T2,r,trace.
545  mk_sub_trace_result ge T2
546    (ends … r)
547    (mk_trace_result ge (T2 (ends … r))
548      (new_state … r)
549      (remainder … r)
550      (cost_labelled … r)
551      trace
552    )
553    (terminates … r)
554.
555
556definition replace_trace : ∀ge,T1,T2.
557  ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝
558λge,T1,T2,r,trace.
559  mk_trace_result ge T2
560    (new_state … r)
561    (remainder … r)
562    (cost_labelled … r)
563    trace
564.
565
566let rec make_label_return ge s
567  (trace: flat_trace io_out io_in ge s)
568  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
569  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
570  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
571  (TERMINATES: will_return ge O s trace)
572  : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝
573
574  let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
575  match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with
576  [ ends_with_ret ⇒ λtll,term.
577      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
578  | doesnt_end_with_ret ⇒ λtll,term.
579      let r' ≝ make_label_return ge (new_state … r)
580                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in
581        replace_trace … r'
582          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
583  ] (new_trace … r) (terminates … r)
584
585and make_label_label ge s
586  (trace: flat_trace io_out io_in ge s)
587  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
588  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
589  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
590  (TERMINATES: will_return ge O s trace)
591  : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
592let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
593  replace_sub_trace ??? r
594    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
595
596and make_any_label ge s
597  (trace: flat_trace io_out io_in ge s)
598  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
599  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
600  (TERMINATES: will_return ge O s trace)
601  : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
602match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
603[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
604| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
605    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
606    [ cl_other ⇒ λCL.
607        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
608        [ true ⇒ λCS.
609            mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
610        | false ⇒ λCS.
611            let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in
612                replace_sub_trace ??? r
613                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
614        ] (refl ??)
615    | cl_jump ⇒ λCL.
616        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
617    | cl_call ⇒ λCL.
618        let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in
619        let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
620        replace_sub_trace ??? r'
621          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
622    | cl_return ⇒ λCL.
623        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
624    ] (refl ? (RTLabs_classify start))
625| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
626] STATE_COSTLABELLED TERMINATES.
627
628[ @(trace_label_label_label … tll)
629|
630| %{tr} @EV
631| @(well_cost_labelled_state_step  … EV) //
632| @I
633| %{tr} @EV
634| % whd in ⊢ (% → ?); >CL #E destruct
635| @(well_cost_labelled_jump … EV) //
636| @(well_cost_labelled_state_step  … EV) //
637| @(will_return_notfn … TERMINATES) %2 @CL
638| (* oh dear *)
639| %{tr} @EV
640| @(cost_labelled … r)
641|
642|
643|
644
645 @(well_cost_labelled_state_step  … EV) //
646| % whd in ⊢ (% → ?); >CL #E destruct
647| @CS
648| @(nth_is_return_notfn … TERMINATES) %1 @CL
649| % whd in ⊢ (% → ?); >CS #E destruct
650| @CL
651| %{tr} @EV
652| @(well_cost_labelled_state_step  … EV) //
653| @(nth_is_return_notfn … TERMINATES) %1 @CL
654| inversion TERMINATES
655  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
656  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
657  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
658  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
659  ]
660|
661
662
663 
664(* FIXME: there's trouble at the end of the program because we can't make a step
665   away from the final return. *)
Note: See TracBrowser for help on using the repository browser.