source: src/RTLabs/Traces.ma @ 1654

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

Corrections to structured trace definitions (see the mailing list).
Also update RTLabs work to match.

File size: 34.5 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
231(* The way we will use [will_return] won't satisfy Matita's guardedness check,
232   so we will measure the length of these termination proofs and use an upper
233   bound to show termination of the finite structured trace construction
234   functions. *)
235
236let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
237match T with
238[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
239| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
240| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
241| wr_base _ _ _ _ _ _ ⇒ S O
242].
243
244include alias "arithmetics/nat.ma".
245
246(* Specialised to the particular situation it is used in. *)
247lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
248#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
249whd in ⊢ (??(??%) → ?);
250>commutative_times
251#H lapply (le_plus_b … H)
252#H lapply (le_to_leb_true … H)
253normalize #E destruct
254qed.
255
256(* Inversion lemmas on [will_return] that also note the effect on the length
257   of the proof. *)
258lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
259  RTLabs_classify s = cl_call →
260  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
261  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
262#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
263[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
264| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
265| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
266| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
267] qed.
268
269lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
270  RTLabs_classify s = cl_return →
271  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
272  match d with
273  [ O ⇒ True
274  | S d' ⇒
275      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
276  ].
277#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
278[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
279| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
280| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
281| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
282] qed.
283
284lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
285  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
286  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
287  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
288#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
289[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
290| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
291| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
292| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
293| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
294| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
295| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
296| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
297] qed.
298
299(* We require that labels appear after branch instructions and at the start of
300   functions.  The first is required for preciseness, the latter for soundness.
301   We will make a separate requirement for there to be a finite number of steps
302   between labels to catch loops for soundness (is this sufficient?). *)
303
304definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
305λf,s. match s return λs. labels_present ? s → Prop with
306[ St_cond _ l1 l2 ⇒ λH.
307    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
308    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
309| St_jumptable _ ls ⇒ λH.
310    (* I did have a dependent version of All here, but it's a pain. *)
311    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
312| _ ⇒ λ_. True
313]. whd in H;
314[ @(proj1 … H)
315| @(proj2 … H)
316] qed.
317
318definition well_cost_labelled_fn : internal_function → Prop ≝
319λf. (∀l. ∀H:present … (f_graph f) l.
320         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
321    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
322[ @lookup_lookup_present | cases (f_entry f) // ] qed.
323
324(* We need to ensure that any code we come across is well-cost-labelled.  We may
325   get function code from either the global environment or the state. *)
326
327definition well_cost_labelled_ge : genv → Prop ≝
328λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
329
330definition well_cost_labelled_state : state → Prop ≝
331λs. match s with
332[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
333| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
334                          All ? (λf. well_cost_labelled_fn (func f)) fs
335| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
336].
337
338lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
339  eval_statement ge s = Value ??? 〈tr,s'〉 →
340  well_cost_labelled_ge ge →
341  well_cost_labelled_state s →
342  well_cost_labelled_state s'.
343#ge #s #tr' #s' #EV cases (eval_perserves … EV)
344[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
345| #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/
346| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
347| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
348| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
349| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
350] qed.
351
352lemma rtlabs_jump_inv : ∀s.
353  RTLabs_classify s = cl_jump →
354  ∃f,fs,m. s = State f fs m ∧
355  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
356  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
357*
358[ #f #fs #m #E
359  %{f} %{fs} %{m} %
360  [ @refl
361  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
362    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
363    [ %1 %{A} %{B} %{C} @refl
364    | %2 %{A} %{B} @refl
365    ]
366  ]
367| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
368| normalize #H8 #H9 #H10 #H11 #H12 destruct
369] qed.
370
371lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
372  eval_statement ge s = Value ??? 〈tr,s'〉 →
373  well_cost_labelled_state s →
374  RTLabs_classify s = cl_jump →
375  RTLabs_cost s' = true.
376#ge #s #tr #s' #EV #H #CL
377cases (rtlabs_jump_inv s CL)
378#fr * #fs * #m * #Es *
379[ * #r * #l1 * #l2 #Estmt
380  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
381  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
382  >Estmt #LP whd in ⊢ (??%? → ?);
383  (* replace with lemma on successors? *)
384  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
385  lapply (Hbody (next fr) (next_ok fr))
386  generalize in ⊢ (???% → ?);
387  >Estmt #LP'
388  whd in ⊢ (% → ?);
389  * #H1 #H2 [ @H1 | @H2 ]
390| * #r * #ls #Estmt
391  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
392  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
393  >Estmt #LP whd in ⊢ (??%? → ?);
394  (* replace with lemma on successors? *)
395  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
396  [ 2: (* later *)
397  | *: #E destruct
398  ]
399  lapply (Hbody (next fr) (next_ok fr))
400  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
401  generalize in ⊢ (??(?%)? → ?);
402  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
403  [ #E1 #E2 whd in E2:(??%?); destruct
404  | #l' #E1 #E2 whd in E2:(??%?); destruct
405    cases (All_nth ???? CP ? E1)
406    #H1 #H2 @H2
407  ]
408] qed.
409
410lemma rtlabs_call_inv : ∀s.
411  RTLabs_classify s = cl_call →
412  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
413* [ #f #fs #m whd in ⊢ (??%? → ?);
414    cases (lookup_present … (next f) (next_ok f)) normalize
415    try #A try #B try #C try #D try #E try #F try #G destruct
416  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
417  | normalize #H411 #H412 #H413 #H414 #H415 destruct
418  ] qed.
419
420lemma well_cost_labelled_call : ∀ge,s,tr,s'.
421  eval_statement ge s = Value ??? 〈tr,s'〉 →
422  well_cost_labelled_state s →
423  RTLabs_classify s = cl_call →
424  RTLabs_cost s' = true.
425#ge #s #tr #s' #EV #WCL #CL
426cases (rtlabs_call_inv s CL)
427#fd * #args * #dst * #stk * #m #E >E in EV WCL;
428whd in ⊢ (??%? → % → ?);
429cases fd
430[ #fn whd in ⊢ (??%? → % → ?);
431  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
432  #m' #b whd in ⊢ (??%? → ?); #E' destruct
433  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
434  @WCL2
435| #fn whd in ⊢ (??%? → % → ?);
436  @bindIO_value #evargs #Eargs
437  @bindIO_value #evres #Eres
438  normalize in Eres; destruct
439] qed.
440
441(* Don't need to know that labels break loops because we have termination. *)
442
443(* A bit of mucking around with the depth to avoid proving termination after
444   termination.  Note that we keep a proof that our upper bound on the length
445   of the termination proof is respected. *)
446record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
447  new_state : state;
448  remainder : flat_trace io_out io_in ge new_state;
449  cost_labelled : well_cost_labelled_state new_state;
450  new_trace : T new_state;
451  terminates : match depth with
452               [ O ⇒ True
453               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
454               ]
455}.
456
457(* The same with a flag indicating whether the function returned, as opposed to
458   encountering a label. *)
459record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
460  ends : trace_ends_with_ret;
461  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
462}.
463
464(* We often return the result from a recursive call with an addition to the
465   structured trace, so we define a couple of functions to help.  The bound on
466   the size of the termination proof might need to be relaxed, too. *)
467
468definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
469  ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge d T2 l2 ≝
470λge,d,T1,T2,l1,l2,lGE,r,trace.
471  mk_trace_result ge d T2 l2
472    (new_state … r)
473    (remainder … r)
474    (cost_labelled … r)
475    trace
476    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
477                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
478     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r))
479. @(transitive_le … lGE) @(pi2 … TM) qed.
480
481definition replace_sub_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
482  ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge d T2 l2 ≝
483λge,d,T1,T2,l1,l2,lGE,r,trace.
484  mk_sub_trace_result ge d T2 l2
485    (ends … r)
486    (replace_trace … lGE … r trace).
487
488(* Small syntax hack to avoid ambiguous input problems. *)
489definition myge : nat → nat → Prop ≝ ge.
490
491let rec make_label_return ge depth s
492  (trace: flat_trace io_out io_in ge s)
493  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
494  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
495  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
496  (TERMINATES: will_return ge depth s trace)
497  (TIME: nat)
498  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
499  on TIME : trace_result ge depth
500              (trace_label_return (RTLabs_status ge) s)
501              (will_return_length … TERMINATES) ≝
502             
503match TIME return λTIME. TIME ≥ ? → ? with
504[ O ⇒ λTERMINATES_IN_TIME. ⊥
505| S TIME ⇒ λTERMINATES_IN_TIME.
506
507  let r ≝ make_label_label ge depth s
508            trace
509            ENV_COSTLABELLED
510            STATE_COSTLABELLED
511            STATEMENT_COSTLABEL
512            TERMINATES
513            TIME ? in
514  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
515  [ ends_with_ret ⇒ λr.
516      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
517  | doesnt_end_with_ret ⇒ λr.
518      let r' ≝ make_label_return ge depth (new_state … r)
519                 (remainder … r)
520                 ENV_COSTLABELLED
521                 (cost_labelled … r) ?
522                 (pi1 … (terminates … r)) TIME ? in
523        replace_trace … r'
524          (tlr_step (RTLabs_status ge) s (new_state … r)
525            (new_state … r') (new_trace … r) (new_trace … r'))
526  ] (trace_res … r)
527
528] TERMINATES_IN_TIME
529
530
531and make_label_label ge depth s
532  (trace: flat_trace io_out io_in ge s)
533  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
534  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
535  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
536  (TERMINATES: will_return ge depth s trace)
537  (TIME: nat)
538  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
539  on TIME : sub_trace_result ge depth
540              (λends. trace_label_label (RTLabs_status ge) ends s)
541              (will_return_length … TERMINATES) ≝
542             
543match TIME return λTIME. TIME ≥ ? → ? with
544[ O ⇒ λTERMINATES_IN_TIME. ⊥
545| S TIME ⇒ λTERMINATES_IN_TIME.
546
547let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
548  replace_sub_trace … r
549    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
550
551] TERMINATES_IN_TIME
552
553
554and make_any_label ge depth s
555  (trace: flat_trace io_out io_in ge s)
556  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
557  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
558  (TERMINATES: will_return ge depth s trace)
559  (TIME: nat)
560  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
561  on TIME : sub_trace_result ge depth
562              (λends. trace_any_label (RTLabs_status ge) ends s)
563              (will_return_length … TERMINATES) ≝
564
565match TIME return λTIME. TIME ≥ ? → ? with
566[ O ⇒ λTERMINATES_IN_TIME. ⊥
567| S TIME ⇒ λTERMINATES_IN_TIME.
568
569  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
570  [ ft_stop st FINAL ⇒
571      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
572
573  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
574    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
575    [ cl_other ⇒ λCL.
576        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
577        (* We're about to run into a label. *)
578        [ true ⇒ λCS.
579            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
580              doesnt_end_with_ret
581              (mk_trace_result ge ??? next trace' ?
582                (tal_base_not_return (RTLabs_status ge) start next ???) ?)
583        (* An ordinary step, keep going. *)
584        | false ⇒ λCS.
585            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
586                replace_sub_trace … r
587                  (tal_step_default (RTLabs_status ge) (ends … r)
588                     start next (new_state … r) ? (new_trace … r) ??)
589        ] (refl ??)
590       
591    | cl_jump ⇒ λCL.
592        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
593          doesnt_end_with_ret
594          (mk_trace_result ge ??? next trace' ?
595            (tal_base_not_return (RTLabs_status ge) start next ???) ?)
596           
597    | cl_call ⇒ λCL.
598        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
599        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
600        (* We're about to run into a label, use base case for call *)
601        [ true ⇒ λCS.
602            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
603            doesnt_end_with_ret
604            (replace_trace … r
605              (tal_base_call (RTLabs_status ge) start next (new_state … r)
606                ? CL ? (new_trace … r) CS))
607        (* otherwise use step case *)
608        | false ⇒ λCS.
609            let r' ≝ make_any_label ge depth
610                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
611                       (pi1 … (terminates … r)) TIME ? in
612            replace_sub_trace … r'
613              (tal_step_call (RTLabs_status ge) (ends … r')
614                start next (new_state … r) (new_state … r') ? CL ?
615                (new_trace … r) ? (new_trace … r'))
616        ] (refl ??)
617
618    | cl_return ⇒ λCL.
619        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
620          ends_with_ret
621          (mk_trace_result ge ???
622            next
623            trace'
624            ?
625            (tal_base_return (RTLabs_status ge) start next ? CL)
626            ?)
627    ] (refl ? (RTLabs_classify start))
628   
629  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
630 
631  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
632] TERMINATES_IN_TIME.
633
634[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
635| //
636| cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le
637| @(trace_label_label_label … (new_trace … r))
638| cases r #H1 #H2 #H3 #H4 * #H5 #H6
639  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
640  @(transitive_le …  (3*(will_return_length … TERMINATES)))
641  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
642    @(monotonic_le_times_r 3 … H6)
643  | @le_S @le_S @le_n
644  ]
645| @le_S_S_to_le @TERMINATES_IN_TIME
646| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
647| @le_n
648| @le_S_S_to_le @TERMINATES_IN_TIME
649| @(wrl_nonzero … TERMINATES_IN_TIME)
650| (* Bad - we've reached the end of the trace; need to fix semantics so that
651     this can't happen *)
652| @(will_return_return … CL TERMINATES)
653| %{tr} @EV
654| @(well_cost_labelled_state_step  … EV) //
655| whd @(will_return_notfn … TERMINATES) %2 @CL
656| %{tr} @EV
657| %1 whd @CL
658| @(well_cost_labelled_jump … EV) //
659| @(well_cost_labelled_state_step  … EV) //
660| %{tr} @EV
661| (* TODO oh dear *)
662| cases (will_return_call … TERMINATES) #H @le_S_to_le
663| cases r #H1 #H2 #H3 #H4 * #H5
664  cases (will_return_call … CL TERMINATES)
665  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
666| whd in ⊢ (?%); >CS % #E destruct
667| (* TODO oh dear *)
668| %{tr} @EV
669| @(cost_labelled … r)
670| cases r #H72 #H73 #H74 #H75 * #H76 #H78
671  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
672  cases (will_return_call … TERMINATES) in H78;
673  #X #Y #Z
674  @(transitive_le … (monotonic_lt_times_r 3 … Y))
675  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
676  | //
677  ]
678| @(well_cost_labelled_state_step  … EV) //
679| @(well_cost_labelled_call … EV) //
680| skip
681| cases (will_return_call … TERMINATES)
682  #TM #GT @le_S_S_to_le
683  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
684  @(transitive_le … TERMINATES_IN_TIME)
685  @(monotonic_le_times_r 3 … GT)
686| whd @(will_return_notfn … TERMINATES) %1 @CL
687| %{tr} @EV
688| %2 whd @CL
689| @CS
690| @(well_cost_labelled_state_step  … EV) //
691| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
692| % whd in ⊢ (% → ?); >CS #E destruct
693| @CL
694| %{tr} @EV
695| @(well_cost_labelled_state_step  … EV) //
696| %1 @CL
697| cases (will_return_notfn … TERMINATES) #TM #GT
698  @le_S_S_to_le
699  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
700  //
701| inversion TERMINATES
702  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
703  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
704  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
705  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
706  ]
707] cases daemon qed.
708
709(* We can initialise TIME with a suitably large value based on the length of the
710   termination proof. *)
711let rec make_label_return' ge depth s
712  (trace: flat_trace io_out io_in ge s)
713  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
714  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
715  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
716  (TERMINATES: will_return ge depth s trace)
717  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
718make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
719  (2 + 3 * will_return_length … TERMINATES) ?.
720@le_n
721qed.
722 
723(* FIXME: there's trouble at the end of the program because we can't make a step
724   away from the final return.
725   
726   We need to show that the "next pc" is preserved through a function call.
727   
728   Tail-calls are not handled properly (which means that if we try to show the
729   full version with non-termination we'll fail because calls and returns aren't
730   balanced.
731 *)
732
733inductive inhabited (T:Type[0]) : Prop ≝
734| witness : T → inhabited T.
735
736(* We also require that program's traces are soundly labelled: for any state
737   in the execution, we can give a distance to a labelled state or termination.
738   
739   Note that this differs from the syntactic notions in earlier languages
740   because it is a global property.  In principle, we would have a loop broken
741   only by a call to a function (which necessarily has a label) and no local
742   cost label.
743 *)
744
745let rec nth_state ge s
746  (trace: flat_trace io_out io_in ge s)
747  n
748  on n : option state ≝
749match n with
750[ O ⇒ Some ? s
751| S n' ⇒
752  match trace with
753  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
754  | _ ⇒ None ?
755  ]
756].
757
758definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
759λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
760
761lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
762  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
763  soundly_labelled_trace ge s' trace'.
764#ge #s #tr #s' #EV #trace' #H
765#n cases (H (S n)) #m #H' %{m} @H'
766qed.
767
768(* When constructing an infinite trace, we need to be able to grab the finite
769   portion of the trace for the next [trace_label_diverges] constructor.  We
770   use the fact that the trace is soundly labelled to achieve this. *)
771
772inductive finite_prefix (ge:genv) : state → Type[0] ≝
773| fp_tal : ∀s,s'.
774           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
775           flat_trace io_out io_in ge s' →
776           finite_prefix ge s
777| fp_tac : ∀s,s'.
778           trace_any_call (RTLabs_status ge) s s' →
779           flat_trace io_out io_in ge s' →
780           finite_prefix ge s
781.
782
783definition fp_add_default : ∀ge,s,s'.
784  RTLabs_classify s = cl_other →
785  finite_prefix ge s' →
786  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
787  RTLabs_cost s' = false →
788  finite_prefix ge s ≝
789λge,s,s',OTHER,fp.
790match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
791[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
792    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER ?)
793    rem
794| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
795    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER ?) rem
796].
797% whd in ⊢ (% → ?); >NOT_COST #E destruct
798qed.
799(* I'll come back to this.
800definition fp_add_terminating_call : ∀ge,s,s1,s'.
801  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
802  ∀CALL:RTLabs_classify s = cl_call.
803  finite_prefix ge s' →
804  trace_label_return (RTLabs_status ge) s1 s' →
805  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
806  finite_prefix ge s ≝
807λge,s,s1,s',EVAL,CALL,fp.
808match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → finite_prefix ge s with
809[ fp_tal s' sf TAL rem ⇒ λTLR,RET. fp_tal ge s sf
810    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR TAL)
811    rem
812| fp_tac s' sf TAC rem ⇒ λTLR,RET. fp_tac ge s sf
813    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR TAC)
814    rem
815].
816*)
817(*
818let corec make_label_diverges ge s
819  (trace: flat_trace io_out io_in ge s)
820  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
821  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
822  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
823  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
824  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
825  : trace_label_diverges (RTLabs_status ge) s ≝ ?
826.
827*)
Note: See TracBrowser for help on using the repository browser.