source: src/RTLabs/Traces.ma @ 1682

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

Complete proof for as_after_return for RTLabs.

File size: 48.4 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 RTLabs_cost : state → bool ≝
23λs. match s with
24[ State f fs m ⇒
25    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
26| _ ⇒ false
27].
28
29definition RTLabs_status : genv → abstract_status ≝
30λge.
31  mk_abstract_status
32    state
33    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
34    (λs,c. RTLabs_classify s = c)
35    (λs. RTLabs_cost s = true)
36    (λs,s'. match s with
37      [ mk_Sig s p ⇒
38        match s return λs. RTLabs_classify s = cl_call → ? with
39        [ Callstate fd args dst stk m ⇒
40          λ_. match s' with
41          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
42          | _ ⇒ False
43          ]
44        | State f fs m ⇒ λH.⊥
45        | _ ⇒ λH.⊥
46        ] p
47      ]).
48[ normalize in H; destruct
49| whd in H:(??%?);
50  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
51  normalize try #a try #b try #c try #d try #e try #g try #h destruct
52] qed.
53
54lemma RTLabs_not_cost : ∀ge,s.
55  RTLabs_cost s = false →
56  ¬ as_costed (RTLabs_status ge) s.
57#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
58qed.
59
60(* Before attempting to construct a structured trace, let's show that we can
61   form flat traces with evidence that they were constructed from an execution.
62   
63   For now we don't consider I/O. *)
64
65
66coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
67| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
68| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
69| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
70
71(* add I/O? *)
72coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
73| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
74| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
75| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
76
77let corec make_flat_trace ge s
78  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
79  flat_trace io_out io_in ge s ≝
80let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
81match e return λx. e = x → ? with
82[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
83| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
84| e_wrong m ⇒ λE. ft_wrong … s m ?
85| e_interact o f ⇒ λE. ⊥
86] (refl ? e).
87[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
88  cases (eval_statement ge s)
89  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
90  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
91    >(?:is_final ????? = RTLabs_is_final s1) //
92    lapply (refl ? (RTLabs_is_final s1))
93    cases (RTLabs_is_final s1) in ⊢ (???% → %);
94    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
95    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
96    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
97    ]
98  | *: #m whd in ⊢ (??%? → ?); #E destruct
99  ]
100| whd in E:(??%?); >exec_inf_aux_unfold in E;
101  cases (eval_statement ge s)
102  [ #O #K whd in ⊢ (??%? → ?); #E destruct
103  | * #tr #s1 whd in ⊢ (??%? → ?);
104    cases (is_final ?????)
105    [ whd in ⊢ (??%? → ?); #E destruct @refl
106    | #i whd in ⊢ (??%? → ?); #E destruct
107    ]
108  | #m whd in ⊢ (??%? → ?); #E destruct
109  ]
110| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
111  cases (eval_statement ge s)
112  [ #O #K whd in ⊢ (??%? → ?); #E destruct
113  | * #tr #s1 whd in ⊢ (??%? → ?);
114    cases (is_final ?????)
115    [ whd in ⊢ (??%? → ?); #E
116      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
117      destruct
118      inversion H
119      [ #a #b #c #E1 destruct
120      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
121      | #m #E1 destruct
122      ]
123    | #i whd in ⊢ (??%? → ?); #E destruct
124    ]
125  | #m whd in ⊢ (??%? → ?); #E destruct
126  ]
127| whd in E:(??%?); >exec_inf_aux_unfold in E;
128  cases (eval_statement ge s)
129  [ #O #K whd in ⊢ (??%? → ?); #E destruct
130  | * #tr1 #s1 whd in ⊢ (??%? → ?);
131    cases (is_final ?????)
132    [ whd in ⊢ (??%? → ?); #E destruct
133    | #i whd in ⊢ (??%? → ?); #E destruct
134    ]
135  | #m whd in ⊢ (??%? → ?); #E destruct @refl
136  ]
137| whd in E:(??%?); >E in H; #H
138  inversion H
139  [ #a #b #c #E destruct
140  | #a #b #c #d #E1 destruct
141  | #m #E1 destruct
142  ]
143] qed.
144
145let corec make_whole_flat_trace p s
146  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
147  (I:make_initial_state ??? p = OK ? s) :
148  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
149let ge ≝ make_global … p in
150let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
151match e return λx. e = x → ? with
152[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
153| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
154| e_wrong m ⇒ λE. ⊥
155| e_interact o f ⇒ λE. ⊥
156] (refl ? e).
157[ whd in E:(??%?); >exec_inf_aux_unfold in E;
158  whd in ⊢ (??%? → ?);
159  >(?:is_final ????? = RTLabs_is_final s) //
160  lapply (refl ? (RTLabs_is_final s))
161  cases (RTLabs_is_final s) in ⊢ (???% → %);
162  [ #_ whd in ⊢ (??%? → ?); #E destruct
163  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
164  ]
165| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
166  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
167  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
168    [ #a #b #c #E1 destruct
169    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
170      @H1
171    | #m #E1 destruct
172    ]
173  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
174  ]
175| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
176  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
177| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
178  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
179] qed.
180
181(* Need a way to choose whether a called function terminates.  Then,
182     if the initial function terminates we generate a purely inductive structured trace,
183     otherwise we start generating the coinductive one, and on every function call
184       use the choice method again to decide whether to step over or keep going.
185
186Not quite what we need - have to decide on seeing each label whether we will see
187another or hit a non-terminating call?
188
189Also - need the notion of well-labelled in order to break loops.
190
191
192
193outline:
194
195 does function terminate?
196 - yes, get (bound on the number of steps until return), generate finite
197        structure using bound as termination witness
198 - no,  get (¬ bound on steps to return), start building infinite trace out of
199        finite steps.  At calls, check for termination, generate appr. form.
200
201generating the finite parts:
202
203We start with the status after the call has been executed; well-labelling tells
204us that this is a labelled state.  Now we want to generate a trace_label_return
205and also return the remainder of the flat trace.
206
207*)
208
209(* [will_return ge depth s trace] says that after a finite number of steps of
210   [trace] from [s] we reach the return state for the current function.  [depth]
211   performs the call/return counting necessary for handling deeper function
212   calls.  It should be zero at the top level. *)
213inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
214| wr_step : ∀s,tr,s',depth,EX,trace.
215    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
216    will_return ge depth s' trace →
217    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
218| wr_call : ∀s,tr,s',depth,EX,trace.
219    RTLabs_classify s = cl_call →
220    will_return ge (S depth) s' trace →
221    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
222| wr_ret : ∀s,tr,s',depth,EX,trace.
223    RTLabs_classify s = cl_return →
224    will_return ge depth s' trace →
225    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
226    (* Note that we require the ability to make a step after the return (this
227       corresponds to somewhere that will be guaranteed to be a label at the
228       end of the compilation chain). *)
229| wr_base : ∀s,tr,s',EX,trace.
230    RTLabs_classify s = cl_return →
231    will_return ge O s (ft_step ?? ge s tr s' EX trace)
232.
233
234(* The way we will use [will_return] won't satisfy Matita's guardedness check,
235   so we will measure the length of these termination proofs and use an upper
236   bound to show termination of the finite structured trace construction
237   functions. *)
238
239let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
240match T with
241[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
242| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
243| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
244| wr_base _ _ _ _ _ _ ⇒ S O
245].
246
247include alias "arithmetics/nat.ma".
248
249(* Specialised to the particular situation it is used in. *)
250lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
251#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
252whd in ⊢ (??(??%) → ?);
253>commutative_times
254#H lapply (le_plus_b … H)
255#H lapply (le_to_leb_true … H)
256normalize #E destruct
257qed.
258
259(* Inversion lemmas on [will_return] that also note the effect on the length
260   of the proof. *)
261lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
262  RTLabs_classify s = cl_call →
263  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
264  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
265#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
266[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
267| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
268| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
269| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
270] qed.
271
272lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
273  RTLabs_classify s = cl_return →
274  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
275  match d with
276  [ O ⇒ True
277  | S d' ⇒
278      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
279  ].
280#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
281[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
282| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
283| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
284| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
285] qed.
286
287lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
288  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
289  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
290  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
291#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
292[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
293| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
294| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
295| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
296| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
297| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
298| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
299| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
300] qed.
301
302(* We require that labels appear after branch instructions and at the start of
303   functions.  The first is required for preciseness, the latter for soundness.
304   We will make a separate requirement for there to be a finite number of steps
305   between labels to catch loops for soundness (is this sufficient?). *)
306
307definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
308λf,s. match s return λs. labels_present ? s → Prop with
309[ St_cond _ l1 l2 ⇒ λH.
310    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
311    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
312| St_jumptable _ ls ⇒ λH.
313    (* I did have a dependent version of All here, but it's a pain. *)
314    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
315| _ ⇒ λ_. True
316]. whd in H;
317[ @(proj1 … H)
318| @(proj2 … H)
319] qed.
320
321definition well_cost_labelled_fn : internal_function → Prop ≝
322λf. (∀l. ∀H:present … (f_graph f) l.
323         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
324    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
325[ @lookup_lookup_present | cases (f_entry f) // ] qed.
326
327(* We need to ensure that any code we come across is well-cost-labelled.  We may
328   get function code from either the global environment or the state. *)
329
330definition well_cost_labelled_ge : genv → Prop ≝
331λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
332
333definition well_cost_labelled_state : state → Prop ≝
334λs. match s with
335[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
336| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
337                          All ? (λf. well_cost_labelled_fn (func f)) fs
338| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
339].
340
341lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
342  eval_statement ge s = Value ??? 〈tr,s'〉 →
343  well_cost_labelled_ge ge →
344  well_cost_labelled_state s →
345  well_cost_labelled_state s'.
346#ge #s #tr' #s' #EV cases (eval_perserves … EV)
347[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
348| #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/
349(*
350| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
351*)
352| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
353| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
354| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
355] qed.
356
357lemma rtlabs_jump_inv : ∀s.
358  RTLabs_classify s = cl_jump →
359  ∃f,fs,m. s = State f fs m ∧
360  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
361  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
362*
363[ #f #fs #m #E
364  %{f} %{fs} %{m} %
365  [ @refl
366  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
367    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
368    [ %1 %{A} %{B} %{C} @refl
369    | %2 %{A} %{B} @refl
370    ]
371  ]
372| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
373| normalize #H8 #H9 #H10 #H11 #H12 destruct
374] qed.
375
376lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
377  eval_statement ge s = Value ??? 〈tr,s'〉 →
378  well_cost_labelled_state s →
379  RTLabs_classify s = cl_jump →
380  RTLabs_cost s' = true.
381#ge #s #tr #s' #EV #H #CL
382cases (rtlabs_jump_inv s CL)
383#fr * #fs * #m * #Es *
384[ * #r * #l1 * #l2 #Estmt
385  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
386  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
387  >Estmt #LP whd in ⊢ (??%? → ?);
388  (* replace with lemma on successors? *)
389  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
390  lapply (Hbody (next fr) (next_ok fr))
391  generalize in ⊢ (???% → ?);
392  >Estmt #LP'
393  whd in ⊢ (% → ?);
394  * #H1 #H2 [ @H1 | @H2 ]
395| * #r * #ls #Estmt
396  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
397  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
398  >Estmt #LP whd in ⊢ (??%? → ?);
399  (* replace with lemma on successors? *)
400  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
401  [ 2: (* later *)
402  | *: #E destruct
403  ]
404  lapply (Hbody (next fr) (next_ok fr))
405  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
406  generalize in ⊢ (??(?%)? → ?);
407  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
408  [ #E1 #E2 whd in E2:(??%?); destruct
409  | #l' #E1 #E2 whd in E2:(??%?); destruct
410    cases (All_nth ???? CP ? E1)
411    #H1 #H2 @H2
412  ]
413] qed.
414
415lemma rtlabs_call_inv : ∀s.
416  RTLabs_classify s = cl_call →
417  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
418* [ #f #fs #m whd in ⊢ (??%? → ?);
419    cases (lookup_present … (next f) (next_ok f)) normalize
420    try #A try #B try #C try #D try #E try #F try #G destruct
421  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
422  | normalize #H411 #H412 #H413 #H414 #H415 destruct
423  ] qed.
424
425lemma well_cost_labelled_call : ∀ge,s,tr,s'.
426  eval_statement ge s = Value ??? 〈tr,s'〉 →
427  well_cost_labelled_state s →
428  RTLabs_classify s = cl_call →
429  RTLabs_cost s' = true.
430#ge #s #tr #s' #EV #WCL #CL
431cases (rtlabs_call_inv s CL)
432#fd * #args * #dst * #stk * #m #E >E in EV WCL;
433whd in ⊢ (??%? → % → ?);
434cases fd
435[ #fn whd in ⊢ (??%? → % → ?);
436  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
437  #m' #b whd in ⊢ (??%? → ?); #E' destruct
438  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
439  @WCL2
440| #fn whd in ⊢ (??%? → % → ?);
441  @bindIO_value #evargs #Eargs
442  whd in ⊢ (??%? → ?);
443  #E' destruct
444] qed.
445
446
447(* The preservation of (most of) the stack is useful to show as_after_return.
448   We do this by showing that during the execution of a function the lower stack
449   frames never change, and that after returning from the function we preserve
450   the identity of the next instruction to execute.
451 *)
452
453inductive stack_of_state : list frame → state → Prop ≝
454| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
455| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
456| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
457.
458
459inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
460| sp_normal : ∀fs,s1,s2.
461    stack_of_state fs s1 →
462    stack_of_state fs s2 →
463    stack_preserved doesnt_end_with_ret s1 s2
464| sp_finished : ∀s1,f,f',fs,m.
465    next f = next f' →
466    stack_of_state (f::fs) s1 →
467    stack_preserved ends_with_ret s1 (State f' fs m).
468
469discriminator list.
470
471lemma stack_of_state_eq : ∀fs,fs',s.
472  stack_of_state fs s →
473  stack_of_state fs' s →
474  fs = fs'.
475#fs0 #fs0' #s0 *
476[ #f #fs #m #H inversion H
477  #a #b #c #d #e #g try #h try #i try #j destruct @refl
478| #fd #args #dst #f #fs #m #H inversion H
479  #a #b #c #d #e #g try #h try #i try #j destruct @refl
480| #rtv #dst #fs #m #H inversion H
481  #a #b #c #d #e #g try #h try #i try #j destruct @refl
482] qed.
483
484lemma stack_preserved_join : ∀e,s1,s2,s3.
485  stack_preserved doesnt_end_with_ret s1 s2 →
486  stack_preserved e s2 s3 →
487  stack_preserved e s1 s3.
488#e1 #s1 #s2 #s3 #H1 inversion H1
489[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
490  #H2 inversion H2
491  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
492    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
493  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
494    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
495  ]
496| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
497] qed.
498
499lemma stack_preserved_return : ∀ge,s1,s2,tr.
500  RTLabs_classify s1 = cl_return →
501  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
502  stack_preserved ends_with_ret s1 s2.
503#ge *
504[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
505  cases (lookup_present ??? (next f) (next_ok f)) in E;
506  normalize #a try #b try #c try #d try #e try #f try #g destruct
507| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
508| #res #dst *
509  [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct
510  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
511    whd in EV:(??%?); destruct @(sp_finished ? f) //
512  ]
513] qed.
514
515lemma stack_preserved_step : ∀ge,s1,s2,tr.
516  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
517  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
518  stack_preserved doesnt_end_with_ret s1 s2.
519#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
520[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
521| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
522| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
523  normalize in CL; cases CL #E destruct
524| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
525| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
526  #E normalize in E; destruct
527] qed.
528
529lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
530  RTLabs_classify s1 = cl_call →
531  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
532  stack_preserved ends_with_ret s2 s3 →
533  stack_preserved doesnt_end_with_ret s1 s3.
534#ge #s1 #s2 #s3 #tr #CL #EV #SP
535cases (rtlabs_call_inv … CL)
536#fd * #args * #dst * #stk * #m #E destruct
537inversion SP
538[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
539| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
540  inversion (eval_perserves … EV)
541  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
542  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
543  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
544    inversion S
545    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
546    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
547    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
548    ]
549  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
550  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
551  ]
552] qed.
553 
554lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
555  ∀CL : RTLabs_classify s1 = cl_call.
556  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
557  stack_preserved ends_with_ret s2 s3 →
558  as_after_return (RTLabs_status ge) «s1,CL» s3.
559#ge #s1 #s2 #s3 #tr #CL #EV #S23
560cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
561inversion S23
562[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
563| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
564  inversion (eval_perserves … EV)
565  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
566  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
567  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
568    inversion S
569    [ #fy #fsy #my #E1 #E2 #E3 destruct @N
570    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
571    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
572    ]
573  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
574  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
575  ]
576] qed.
577
578(* Don't need to know that labels break loops because we have termination. *)
579
580(* A bit of mucking around with the depth to avoid proving termination after
581   termination.  Note that we keep a proof that our upper bound on the length
582   of the termination proof is respected. *)
583record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
584  new_state : state;
585  remainder : flat_trace io_out io_in ge new_state;
586  cost_labelled : well_cost_labelled_state new_state;
587  new_trace : T new_state;
588  stack_ok : stack_preserved ends start new_state;
589  terminates : match depth with
590               [ O ⇒ True
591               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
592               ]
593}.
594
595(* The same with a flag indicating whether the function returned, as opposed to
596   encountering a label. *)
597record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
598  ends : trace_ends_with_ret;
599  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start (T ends) limit
600}.
601
602(* We often return the result from a recursive call with an addition to the
603   structured trace, so we define a couple of functions to help.  The bound on
604   the size of the termination proof might need to be relaxed, too. *)
605
606definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
607  ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝
608λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
609  mk_trace_result ge d e2 s2 T2 l2
610    (new_state … r)
611    (remainder … r)
612    (cost_labelled … r)
613    trace
614    SP
615    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
616                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
617     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r))
618. @(transitive_le … lGE) @(pi2 … TM) qed.
619
620definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
621  ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝
622λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
623  mk_sub_trace_result ge d s2 T2 l2
624    (ends … r)
625    (replace_trace … lGE … r trace SP).
626
627(* Small syntax hack to avoid ambiguous input problems. *)
628definition myge : nat → nat → Prop ≝ ge.
629
630let rec make_label_return ge depth s
631  (trace: flat_trace io_out io_in ge s)
632  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
633  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
634  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
635  (TERMINATES: will_return ge depth s trace)
636  (TIME: nat)
637  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
638  on TIME : trace_result ge depth ends_with_ret s
639              (trace_label_return (RTLabs_status ge) s)
640              (will_return_length … TERMINATES) ≝
641             
642match TIME return λTIME. TIME ≥ ? → ? with
643[ O ⇒ λTERMINATES_IN_TIME. ⊥
644| S TIME ⇒ λTERMINATES_IN_TIME.
645
646  let r ≝ make_label_label ge depth s
647            trace
648            ENV_COSTLABELLED
649            STATE_COSTLABELLED
650            STATEMENT_COSTLABEL
651            TERMINATES
652            TIME ? in
653  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
654  [ ends_with_ret ⇒ λr.
655      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
656  | doesnt_end_with_ret ⇒ λr.
657      let r' ≝ make_label_return ge depth (new_state … r)
658                 (remainder … r)
659                 ENV_COSTLABELLED
660                 (cost_labelled … r) ?
661                 (pi1 … (terminates … r)) TIME ? in
662        replace_trace … r'
663          (tlr_step (RTLabs_status ge) s (new_state … r)
664            (new_state … r') (new_trace … r) (new_trace … r')) ?
665  ] (trace_res … r)
666
667] TERMINATES_IN_TIME
668
669
670and make_label_label ge depth s
671  (trace: flat_trace io_out io_in ge s)
672  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
673  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
674  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
675  (TERMINATES: will_return ge depth s trace)
676  (TIME: nat)
677  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
678  on TIME : sub_trace_result ge depth s
679              (λends. trace_label_label (RTLabs_status ge) ends s)
680              (will_return_length … TERMINATES) ≝
681             
682match TIME return λTIME. TIME ≥ ? → ? with
683[ O ⇒ λTERMINATES_IN_TIME. ⊥
684| S TIME ⇒ λTERMINATES_IN_TIME.
685
686let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
687  replace_sub_trace … r
688    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
689
690] TERMINATES_IN_TIME
691
692
693and make_any_label ge depth s
694  (trace: flat_trace io_out io_in ge s)
695  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
696  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
697  (TERMINATES: will_return ge depth s trace)
698  (TIME: nat)
699  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
700  on TIME : sub_trace_result ge depth s
701              (λends. trace_any_label (RTLabs_status ge) ends s)
702              (will_return_length … TERMINATES) ≝
703
704match TIME return λTIME. TIME ≥ ? → ? with
705[ O ⇒ λTERMINATES_IN_TIME. ⊥
706| S TIME ⇒ λTERMINATES_IN_TIME.
707
708  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 s (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
709  [ ft_stop st FINAL ⇒
710      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
711
712  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
713    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
714    [ cl_other ⇒ λCL.
715        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
716        (* We're about to run into a label. *)
717        [ true ⇒ λCS.
718            mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
719              doesnt_end_with_ret
720              (mk_trace_result ge … next trace' ?
721                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
722        (* An ordinary step, keep going. *)
723        | false ⇒ λCS.
724            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
725                replace_sub_trace … r
726                  (tal_step_default (RTLabs_status ge) (ends … r)
727                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
728        ] (refl ??)
729       
730    | cl_jump ⇒ λCL.
731        mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
732          doesnt_end_with_ret
733          (mk_trace_result ge ????? next trace' ?
734            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
735           
736    | cl_call ⇒ λCL.
737        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
738        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
739        (* We're about to run into a label, use base case for call *)
740        [ true ⇒ λCS.
741            mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
742            doesnt_end_with_ret
743            (replace_trace … r
744              (tal_base_call (RTLabs_status ge) start next (new_state … r)
745                ? CL ? (new_trace … r) CS) ?)
746        (* otherwise use step case *)
747        | false ⇒ λCS.
748            let r' ≝ make_any_label ge depth
749                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
750                       (pi1 … (terminates … r)) TIME ? in
751            replace_sub_trace … r'
752              (tal_step_call (RTLabs_status ge) (ends … r')
753                start next (new_state … r) (new_state … r') ? CL ?
754                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
755        ] (refl ??)
756
757    | cl_return ⇒ λCL.
758        mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
759          ends_with_ret
760          (mk_trace_result ge ?????
761            next
762            trace'
763            ?
764            (tal_base_return (RTLabs_status ge) start next ? CL)
765            ?
766            ?)
767    ] (refl ? (RTLabs_classify start))
768   
769  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
770 
771  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
772] TERMINATES_IN_TIME.
773
774[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
775| //
776| cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le
777| @(stack_preserved_join … (stack_ok … r)) //
778| @(trace_label_label_label … (new_trace … r))
779| cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT
780  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
781  @(transitive_le …  (3*(will_return_length … TERMINATES)))
782  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
783    @(monotonic_le_times_r 3 … LT)
784  | @le_S @le_S @le_n
785  ]
786| @le_S_S_to_le @TERMINATES_IN_TIME
787| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
788| @le_n
789| @le_S_S_to_le @TERMINATES_IN_TIME
790| @(wrl_nonzero … TERMINATES_IN_TIME)
791| (* Bad - we've reached the end of the trace; need to fix semantics so that
792     this can't happen *)
793| @(will_return_return … CL TERMINATES)
794| /2 by stack_preserved_return/
795| %{tr} @EV
796| @(well_cost_labelled_state_step  … EV) //
797| whd @(will_return_notfn … TERMINATES) %2 @CL
798| @stack_preserved_step /2/
799| %{tr} @EV
800| %1 whd @CL
801| @(well_cost_labelled_jump … EV) //
802| @(well_cost_labelled_state_step  … EV) //
803| @(stack_preserved_call … EV (stack_ok … r)) //
804| %{tr} @EV
805| @RTLabs_after_call //
806| cases (will_return_call … TERMINATES) #H @le_S_to_le
807| cases r #H1 #H2 #H3 #H4 #H5 * #H6
808  cases (will_return_call … CL TERMINATES)
809  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
810| @RTLabs_after_call //
811| %{tr} @EV
812| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
813| @(cost_labelled … r)
814| cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78
815  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
816  cases (will_return_call … TERMINATES) in H78;
817  #X #Y #Z
818  @(transitive_le … (monotonic_lt_times_r 3 … Y))
819  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
820  | //
821  ]
822| @(well_cost_labelled_state_step  … EV) //
823| @(well_cost_labelled_call … EV) //
824| skip
825| cases (will_return_call … TERMINATES)
826  #TM #GT @le_S_S_to_le
827  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
828  @(transitive_le … TERMINATES_IN_TIME)
829  @(monotonic_le_times_r 3 … GT)
830| whd @(will_return_notfn … TERMINATES) %1 @CL
831| @(stack_preserved_step … EV) /2/
832| %{tr} @EV
833| %2 whd @CL
834| @(well_cost_labelled_state_step  … EV) //
835| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
836| @CL
837| %{tr} @EV
838| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
839| @(well_cost_labelled_state_step  … EV) //
840| %1 @CL
841| cases (will_return_notfn … TERMINATES) #TM #GT
842  @le_S_S_to_le
843  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
844  //
845| inversion TERMINATES
846  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
847  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
848  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
849  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
850  ]
851] cases daemon qed.
852
853(* We can initialise TIME with a suitably large value based on the length of the
854   termination proof. *)
855let rec make_label_return' ge depth s
856  (trace: flat_trace io_out io_in ge s)
857  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
858  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
859  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
860  (TERMINATES: will_return ge depth s trace)
861  : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
862make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
863  (2 + 3 * will_return_length … TERMINATES) ?.
864@le_n
865qed.
866 
867(* FIXME: there's trouble at the end of the program because we can't make a step
868   away from the final return.
869   
870   We need to show that the "next pc" is preserved through a function call.
871   
872   Tail-calls are not handled properly (which means that if we try to show the
873   full version with non-termination we'll fail because calls and returns aren't
874   balanced.
875 *)
876
877inductive inhabited (T:Type[0]) : Prop ≝
878| witness : T → inhabited T.
879
880(* We also require that program's traces are soundly labelled: for any state
881   in the execution, we can give a distance to a labelled state or termination.
882   
883   Note that this differs from the syntactic notions in earlier languages
884   because it is a global property.  In principle, we would have a loop broken
885   only by a call to a function (which necessarily has a label) and no local
886   cost label.
887 *)
888
889let rec nth_state ge s
890  (trace: flat_trace io_out io_in ge s)
891  n
892  on n : option state ≝
893match n with
894[ O ⇒ Some ? s
895| S n' ⇒
896  match trace with
897  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
898  | _ ⇒ None ?
899  ]
900].
901
902definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
903λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
904
905lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
906  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
907  soundly_labelled_trace ge s' trace'.
908#ge #s #tr #s' #EV #trace' #H
909#n cases (H (S n)) #m #H' %{m} @H'
910qed.
911
912
913
914definition soundly_labelled_frame : frame → Prop ≝
915λf. soundly_labelled_pc (f_graph (func f)) (next f).
916
917definition soundly_labelled_state : state → Prop ≝
918λs. match s with
919[ State f _ _ ⇒ soundly_labelled_frame f
920| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
921| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
922].
923definition frame_steps_to_label_bound : frame → nat → Prop ≝
924λf. steps_to_label_bound (f_graph (func f)) (next f).
925
926inductive state_steps_to_label_bound : state → nat → Prop ≝
927| sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2)
928| sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S (n*2))
929| sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S (n*2))
930.
931
932(*
933lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.
934  state_steps_to_label_bound (State f fs m) (S (S n)) →
935  ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →
936  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
937  state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]).
938#ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H
939[ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct
940  cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ]
941  #NC whd in ⊢ (??%? → ?);
942  generalize in ⊢ (??(?%)? → ?);
943  lapply (steps_to_label_bound_inv_step … H1 next_ok NC)
944  cases (lookup_present ??? next next_ok)
945  [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
946  | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
947  | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
948  | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
949  | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
950  | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
951  | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
952  | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
953  | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
954  | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
955  | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
956  | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
957  | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
958  | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
959  ]
960*)
961(* When constructing an infinite trace, we need to be able to grab the finite
962   portion of the trace for the next [trace_label_diverges] constructor.  We
963   use the fact that the trace is soundly labelled to achieve this. *)
964
965inductive finite_prefix (ge:genv) : state → Prop ≝
966| fp_tal : ∀s,s'.
967           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
968           flat_trace io_out io_in ge s' →
969           finite_prefix ge s
970| fp_tac : ∀s,s'.
971           trace_any_call (RTLabs_status ge) s s' →
972           flat_trace io_out io_in ge s' →
973           finite_prefix ge s
974.
975
976definition fp_add_default : ∀ge,s,s'.
977  RTLabs_classify s = cl_other →
978  finite_prefix ge s' →
979  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
980  RTLabs_cost s' = false →
981  finite_prefix ge s ≝
982λge,s,s',OTHER,fp.
983match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
984[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
985    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
986    rem
987| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
988    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
989].
990
991definition fp_add_terminating_call : ∀ge,s,s1,s'.
992  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
993  ∀CALL:RTLabs_classify s = cl_call.
994  finite_prefix ge s' →
995  trace_label_return (RTLabs_status ge) s1 s' →
996  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
997  RTLabs_cost s' = false →
998  finite_prefix ge s ≝
999λge,s,s1,s',EVAL,CALL,fp.
1000match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with
1001[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1002    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1003    rem
1004| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
1005    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1006    rem
1007].
1008
1009definition termination_oracle ≝ ∀ge,depth,s,trace.
1010  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1011
1012let rec finite_segment ge s n trace
1013  (ORACLE: termination_oracle)
1014  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1015  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1016  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
1017  (LABEL_LIMIT: state_steps_to_label_bound s n)
1018  on n : finite_prefix ge s ≝
1019match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
1020[ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
1021| S n' ⇒
1022    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
1023    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
1024    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
1025        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1026        [ cl_other ⇒ λCL.
1027            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1028            [ true ⇒ λCS.
1029                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
1030            | false ⇒ λCS.
1031                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in
1032                fp_add_default ge ?? CL fs ? CS
1033            ] (refl ??)
1034        | cl_jump ⇒ λCL.
1035            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
1036        | cl_call ⇒ λCL.
1037            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
1038            [ or_introl TERMINATES ⇒
1039              match TERMINATES with [ witness TERMINATES ⇒
1040                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1041                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
1042                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr)
1043                | false ⇒ λCS. ? (* broken - we don't know the new value of n *)
1044                    (*let fs ≝ finite_segment ge (new_status … tlr) ??????????????
1045                    fp_add_terminating_call … (new_trace … tlr) ? CS*)
1046                ] (refl ??)
1047              ]
1048            | or_intror NO_TERMINATION ⇒
1049                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
1050            ]
1051        | cl_return ⇒ λCL. ⊥
1052        ] (refl ??)
1053    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
1054    ]
1055] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT.
1056[
1057| 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
1058| @(absurd ?? NO_TERMINATION)
1059     %{0} % @wr_base //
1060| @(well_cost_labelled_jump … EV) //
1061| 5,6,8: /2/
1062|
1063|
1064| @(well_cost_labelled_state_step … EV) //
1065| @(well_cost_labelled_call … EV) //
1066| 12,13,14: /2/
1067| @(well_cost_labelled_state_step … EV) //
1068| @(not_to_not … NO_TERMINATION)
1069  * #depth * #TERM %{depth} % @wr_step /2/
1070] cases daemon qed.
1071
1072(*
1073let corec make_label_diverges ge s
1074  (trace: flat_trace io_out io_in ge s)
1075  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1076  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1077  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1078  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
1079  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
1080  : trace_label_diverges (RTLabs_status ge) s ≝ ?
1081.
1082*)
Note: See TracBrowser for help on using the repository browser.