source: src/RTLabs/Traces.ma @ 1637

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

RTLabs structured traces: Add a termination measure to satisfy guardedness check.

File size: 29.3 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      [ mk_Sig 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 → Type[0] ≝
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
231let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
232match T with
233[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
234| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
235| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
236| wr_base _ _ _ _ _ _ ⇒ S O
237].
238include alias "arithmetics/nat.ma".
239
240lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
241#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
242whd in ⊢ (??(??%) → ?);
243>commutative_times
244#H lapply (le_plus_b … H)
245#H lapply (le_to_leb_true … H)
246normalize #E destruct
247qed.
248(*
249lemma wrl_nonzero : ∀ge,d,s,tr,T. ∀P:nat → Prop. (∀x. P (S x)) → P (will_return_length ge d s tr T).
250#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] #P #H @H
251qed.
252*)
253discriminator nat.
254
255lemma will_return_call : ∀ge,depth,s,trace.
256  will_return ge depth s trace →
257  will_return ge (pred depth) s trace.
258#ge #depth #s #trace #H elim H
259[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
260| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
261  cases d in H1 H2 ⊢ %; //
262| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
263  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
264| #s1 #tr #s2 #EX #trc #CL %4 //
265] qed.
266
267lemma will_return_call' : ∀ge,d,s,tr,s',EX,trace.
268  RTLabs_classify s = cl_call →
269  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
270  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
271#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
272[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
273| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
274| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
275| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
276] qed.
277
278lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
279  RTLabs_classify s = cl_return →
280  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
281  match d with
282  [ O ⇒ True
283  | S d' ⇒
284      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
285  ].
286#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
287[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
288| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
289| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
290| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
291] qed.
292
293lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
294  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
295  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
296  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
297#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
298[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
299| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
300| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
301| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
302| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
303| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
304| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
305| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
306] qed.
307
308(* We require that labels appear after branch instructions and at the start of
309   functions.  The first is required for preciseness, the latter for soundness.
310   We will make a separate requirement for there to be a finite number of steps
311   between labels to catch loops for soundness (is this sufficient?). *)
312
313definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
314λf,s. match s return λs. labels_present ? s → Prop with
315[ St_cond _ l1 l2 ⇒ λH.
316    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
317    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
318| St_jumptable _ ls ⇒ λH.
319    (* I did have a dependent version of All here, but it's a pain. *)
320    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
321| _ ⇒ λ_. True
322]. whd in H;
323[ @(proj1 … H)
324| @(proj2 … H)
325] qed.
326
327definition well_cost_labelled_fn : internal_function → Prop ≝
328λf. (∀l. ∀H:present … (f_graph f) l.
329         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
330    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
331[ @lookup_lookup_present | cases (f_entry f) // ] qed.
332
333(* We need to ensure that any code we come across is well-cost-labelled.  We may
334   get function code from either the global environment or the state. *)
335
336definition well_cost_labelled_ge : genv → Prop ≝
337λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
338
339definition well_cost_labelled_state : state → Prop ≝
340λs. match s with
341[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
342| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
343                          All ? (λf. well_cost_labelled_fn (func f)) fs
344| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
345].
346
347lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
348  eval_statement ge s = Value ??? 〈tr,s'〉 →
349  well_cost_labelled_ge ge →
350  well_cost_labelled_state s →
351  well_cost_labelled_state s'.
352#ge #s #tr' #s' #EV cases (eval_perserves … EV)
353[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
354| #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/
355| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
356| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
357| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
358| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
359] qed.
360
361lemma rtlabs_jump_inv : ∀s.
362  RTLabs_classify s = cl_jump →
363  ∃f,fs,m. s = State f fs m ∧
364  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
365  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
366*
367[ #f #fs #m #E
368  %{f} %{fs} %{m} %
369  [ @refl
370  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
371    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
372    [ %1 %{A} %{B} %{C} @refl
373    | %2 %{A} %{B} @refl
374    ]
375  ]
376| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
377| normalize #H8 #H9 #H10 #H11 #H12 destruct
378] qed.
379
380lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
381  eval_statement ge s = Value ??? 〈tr,s'〉 →
382  well_cost_labelled_state s →
383  RTLabs_classify s = cl_jump →
384  RTLabs_cost s' = true.
385#ge #s #tr #s' #EV #H #CL
386cases (rtlabs_jump_inv s CL)
387#fr * #fs * #m * #Es *
388[ * #r * #l1 * #l2 #Estmt
389  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
390  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
391  >Estmt #LP whd in ⊢ (??%? → ?);
392  (* replace with lemma on successors? *)
393  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
394  lapply (Hbody (next fr) (next_ok fr))
395  generalize in ⊢ (???% → ?);
396  >Estmt #LP'
397  whd in ⊢ (% → ?);
398  * #H1 #H2 [ @H1 | @H2 ]
399| * #r * #ls #Estmt
400  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
401  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
402  >Estmt #LP whd in ⊢ (??%? → ?);
403  (* replace with lemma on successors? *)
404  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
405  [ 2: (* later *)
406  | *: #E destruct
407  ]
408  lapply (Hbody (next fr) (next_ok fr))
409  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
410  generalize in ⊢ (??(?%)? → ?);
411  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
412  [ #E1 #E2 whd in E2:(??%?); destruct
413  | #l' #E1 #E2 whd in E2:(??%?); destruct
414    cases (All_nth ???? CP ? E1)
415    #H1 #H2 @H2
416  ]
417] qed.
418
419lemma rtlabs_call_inv : ∀s.
420  RTLabs_classify s = cl_call →
421  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
422* [ #f #fs #m whd in ⊢ (??%? → ?);
423    cases (lookup_present … (next f) (next_ok f)) normalize
424    try #A try #B try #C try #D try #E try #F try #G destruct
425  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
426  | normalize #H411 #H412 #H413 #H414 #H415 destruct
427  ] qed.
428
429lemma well_cost_labelled_call : ∀ge,s,tr,s'.
430  eval_statement ge s = Value ??? 〈tr,s'〉 →
431  well_cost_labelled_state s →
432  RTLabs_classify s = cl_call →
433  RTLabs_cost s' = true.
434#ge #s #tr #s' #EV #WCL #CL
435cases (rtlabs_call_inv s CL)
436#fd * #args * #dst * #stk * #m #E >E in EV WCL;
437whd in ⊢ (??%? → % → ?);
438cases fd
439[ #fn whd in ⊢ (??%? → % → ?);
440  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
441  #m' #b whd in ⊢ (??%? → ?); #E' destruct
442  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
443  @WCL2
444| #fn whd in ⊢ (??%? → % → ?);
445  @bindIO_value #evargs #Eargs
446  @bindIO_value #evres #Eres
447  normalize in Eres; destruct
448] qed.
449
450(* Don't need to know that labels break loops because we have termination. *)
451
452(* A bit of mucking around with the depth to avoid proving termination after
453  termination. *)
454record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
455  new_state : state;
456  remainder : flat_trace io_out io_in ge new_state;
457  cost_labelled : well_cost_labelled_state new_state;
458  new_trace : T new_state;
459  terminates : match depth with
460               [ O ⇒ True
461               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
462               ]
463}.
464
465record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
466  ends : trace_ends_with_ret;
467  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
468}.
469
470definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
471  ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge d T2 l2 ≝
472λge,d,T1,T2,l1,l2,lGE,r,trace.
473  mk_trace_result ge d T2 l2
474    (new_state … r)
475    (remainder … r)
476    (cost_labelled … r)
477    trace
478    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
479                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
480     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r))
481. @(transitive_le … lGE) @(pi2 … TM) qed.
482
483definition replace_sub_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
484  ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge d T2 l2 ≝
485λge,d,T1,T2,l1,l2,lGE,r,trace.
486  mk_sub_trace_result ge d T2 l2
487    (ends … r)
488    (replace_trace … lGE … r trace).
489
490definition myge : nat → nat → Prop ≝ ge.
491
492let rec make_label_return ge depth s
493  (trace: flat_trace io_out io_in ge s)
494  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
495  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
496  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
497  (TERMINATES: will_return ge depth s trace)
498  (TIME: nat)
499  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
500  on TIME : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
501match TIME return λTIME. TIME ≥ ? → ? with
502[ O ⇒ λTERMINATES_IN_TIME. ⊥
503| S TIME ⇒ λTERMINATES_IN_TIME.
504  let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES TIME ? in
505  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
506  [ ends_with_ret ⇒ λr.
507      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
508  | doesnt_end_with_ret ⇒ λr.
509      let r' ≝ make_label_return ge depth (new_state … r)
510                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (pi1 … (terminates … r)) TIME ? in
511        replace_trace … r'
512          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
513  ] (trace_res … r)
514] TERMINATES_IN_TIME
515
516and make_label_label ge depth s
517  (trace: flat_trace io_out io_in ge s)
518  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
519  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
520  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
521  (TERMINATES: will_return ge depth s trace)
522  (TIME: nat)
523  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
524  on TIME : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝
525match TIME return λTIME. TIME ≥ ? → ? with
526[ O ⇒ λTERMINATES_IN_TIME. ⊥
527| S TIME ⇒ λTERMINATES_IN_TIME.
528let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
529  replace_sub_trace … r
530    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
531] TERMINATES_IN_TIME
532
533and make_any_label ge depth s
534  (trace: flat_trace io_out io_in ge s)
535  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
536  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
537  (TERMINATES: will_return ge depth s trace)
538  (TIME: nat)
539  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
540  on TIME : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝
541
542match TIME return λTIME. TIME ≥ ? → ? with
543[ O ⇒ λTERMINATES_IN_TIME. ⊥
544| S TIME ⇒ λTERMINATES_IN_TIME.
545  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
546  [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
547  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
548    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
549    [ cl_other ⇒ λCL.
550        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
551        [ true ⇒ λCS.
552            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
553              doesnt_end_with_ret
554              (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
555        | false ⇒ λCS.
556            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? TIME ? in
557                replace_sub_trace … r
558                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
559        ] (refl ??)
560    | cl_jump ⇒ λCL.
561        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
562          doesnt_end_with_ret
563          (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
564    | cl_call ⇒ λCL.
565        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? TIME ? in
566        let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ? (pi1 … (terminates … r)) TIME ? in
567        replace_sub_trace … r'
568          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
569    | cl_return ⇒ λCL.
570        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
571          ends_with_ret
572          (mk_trace_result ge ???
573            next
574            trace'
575            ?
576            (tal_base_return (RTLabs_status ge) start next ? CL)
577            ?)
578    ] (refl ? (RTLabs_classify start))
579  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
580  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
581] TERMINATES_IN_TIME.
582
583[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
584| //
585| cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le
586| @(trace_label_label_label … (new_trace … r))
587| cases r #H1 #H2 #H3 #H4 * #H5 #H6
588  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
589  @(transitive_le …  (3*(will_return_length … TERMINATES)))
590  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
591    @(monotonic_le_times_r 3 … H6)
592  | @le_S @le_S @le_n
593  ]
594| @le_S_S_to_le @TERMINATES_IN_TIME
595| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
596| @le_n
597| @le_S_S_to_le @TERMINATES_IN_TIME
598| @(wrl_nonzero … TERMINATES_IN_TIME)
599|
600| @(will_return_return … CL TERMINATES)
601| %{tr} @EV
602| @(well_cost_labelled_state_step  … EV) //
603| whd @(will_return_notfn … TERMINATES) %2 @CL
604| %{tr} @EV
605| % whd in ⊢ (% → ?); >CL #E destruct
606| @(well_cost_labelled_jump … EV) //
607| @(well_cost_labelled_state_step  … EV) //
608| 27: @(will_return_call' … CL TERMINATES)
609| cases r #H1 #H2 #H3 #H4 * #H5
610  cases (will_return_call' … CL TERMINATES)
611  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
612| (* oh dear *)
613| %{tr} @EV
614| @(cost_labelled … r)
615| cases r #H72 #H73 #H74 #H75 * #H76 #H78
616  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
617  cases (will_return_call' … TERMINATES) in H78;
618  #X #Y #Z
619  @(transitive_le … (monotonic_lt_times_r 3 … Y))
620  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
621  | //
622  ]
623| @(well_cost_labelled_state_step  … EV) //
624| @(well_cost_labelled_call … EV) //
625| cases (will_return_call' … TERMINATES)
626  #TM #GT @le_S_S_to_le
627  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
628  @(transitive_le … TERMINATES_IN_TIME)
629  @(monotonic_le_times_r 3 … GT)
630| whd @(will_return_notfn … TERMINATES) %1 @CL
631| %{tr} @EV
632| % whd in ⊢ (% → ?); >CL #E destruct
633| @CS
634| @(well_cost_labelled_state_step  … EV) //
635| 39: @(will_return_notfn … TERMINATES) %1 @CL
636| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
637| % whd in ⊢ (% → ?); >CS #E destruct
638| @CL
639| %{tr} @EV
640| @(well_cost_labelled_state_step  … EV) //
641| cases (will_return_notfn … TERMINATES) #TM #GT
642  @le_S_S_to_le
643  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
644  //
645| inversion TERMINATES
646  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
647  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
648  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
649  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
650  ]
651] cases daemon qed.
652
653let rec make_label_return' ge depth s
654  (trace: flat_trace io_out io_in ge s)
655  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
656  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
657  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
658  (TERMINATES: will_return ge depth s trace)
659  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
660make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
661  (2 + 3 * will_return_length … TERMINATES) ?.
662@le_n
663qed.
664 
665(* FIXME: there's trouble at the end of the program because we can't make a step
666   away from the final return.
667   
668   We need to show that the "next pc" is preserved through a function call.
669   
670   Tail-calls are not handled properly (which means that if we try to show the
671   full version with non-termination we'll fail because calls and returns aren't
672   balanced.
673   
674   The guardedness check will reject the recursive definition above; need to
675   rearrange things so that this works properly.
676 *)
Note: See TracBrowser for help on using the repository browser.