source: src/RTLabs/Traces.ma @ 2218

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

Separate out cost properties required of RTLabs programs from the
structured traces proofs. Tidy up a bit.

File size: 101.0 KB
RevLine 
[1537]1
2include "RTLabs/semantics.ma".
[2218]3include "RTLabs/CostSpec.ma".
[1537]4include "common/StructuredTraces.ma".
5
[1552]6discriminator status_class.
[1537]7
[2044]8(* We augment states with a stack of function blocks (i.e. pointers) so that we
9   can make sensible "program counters" for the abstract state definition, along
10   with a proof that we will get the correct code when we do the lookup (which
11   is done to find cost labels given a pc).
12   
13   Adding them to the semantics is an alternative, more direct approach.
14   However, it makes animating the semantics extremely difficult, because it
15   is hard to avoid normalising and displaying irrelevant parts of the global
16   environment and proofs.
17   
18   We use blocks rather than identifiers because the global environments go
19
20     identifier → block → definition
21   
22   and we'd have to introduce backwards lookups to find identifiers for
23   function pointers.
24 *)
25
26definition Ras_Fn_Match ≝
27λge,state,fn_stack.
28  match state with
29  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
30  | Callstate fd _ _ fs _ ⇒
31      match fn_stack with
32      [ nil ⇒ False
33      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
34        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
35      ]
36  | Returnstate _ _ fs _ ⇒
37      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
38  | Finalstate _ ⇒ fn_stack = [ ]
39  ].
40
41record RTLabs_state (ge:genv) : Type[0] ≝ {
42  Ras_state :> state;
43  Ras_fn_stack : list block;
44  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
45}.
46
47(* Given a plain step of the RTLabs semantics, give the next state along with
48   the shadow stack of function block numbers.  Carefully defined so that the
49   coercion back to the plain state always reduces. *)
50definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
51  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
52λge,s,s',t,EX. mk_RTLabs_state ge s'
53 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
54 ?.
55cases s' in EX ⊢ %;
56[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
57  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
58    whd cases stk in mtc ⊢ %; [ * ]
59    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
60    | @M2 ]
61  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
62  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
63    whd cases stk in mtc ⊢ %; [ * ]
64    #hd #tl #H @H
65  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
66  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
67    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
68    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
69  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
70  ]
71| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
72  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
73  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
74  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
75    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
76    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
77  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
78  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
79  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
80  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
81  ]
82| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
83  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
84  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
85  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
86  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
87    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
88  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
89  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
90  ]
91| #r #EX whd @refl
92] qed.
93
94
[1565]95(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
96       will be added later (LTL → LIN). *)
[1552]97
[1563]98definition RTLabs_classify : state → status_class ≝
99λs. match s with
[1565]100[ State f _ _ ⇒
101    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
102    [ St_cond _ _ _ ⇒ cl_jump
103    | St_jumptable _ _ ⇒ cl_jump
104    | _ ⇒ cl_other
105    ]
[1563]106| Callstate _ _ _ _ _ ⇒ cl_call
107| Returnstate _ _ _ _ ⇒ cl_return
[1713]108| Finalstate _ ⇒ cl_other
[1563]109].
[1552]110
[2218]111(* As with is_cost_label/cost_label_of we define a boolean function as well
112   as one which extracts the cost label so that we can use it in hypotheses
113   without naming the cost label. *)
[1705]114
[1583]115definition RTLabs_cost : state → bool ≝
116λs. match s with
117[ State f fs m ⇒
[1586]118    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
[1583]119| _ ⇒ false
120].
[1552]121
[1960]122definition RTLabs_cost_label : state → option costlabel ≝
123λs. match s with
124[ State f fs m ⇒
125    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
126| _ ⇒ None ?
127].
128
[2218]129(* "Program counters" need to identify the current state, either as a pair of
130   the function and current instruction, or the function being entered or
131   left.  Functions are identified by their function pointer block because
132   this avoids introducing functions to map back pointers to function ids using
133   the global environment.  (See the comment at the start of this file, too.) *)
134
[2044]135inductive RTLabs_pc : Type[0] ≝
136| rapc_state : block → label → RTLabs_pc
137| rapc_call : block → RTLabs_pc
138| rapc_ret : option block → RTLabs_pc
139| rapc_fin : RTLabs_pc
140.
141
142definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
143λx,y. match x with
144[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
145| rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2 | _ ⇒ false ]
146| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2 | _ ⇒ false ]
147| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
148].
149
150definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
151whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq;
152* [ #b1 #l1 | #b1 | * [2: #b1 ] | ]
153* [ 1,5,9,13,17: #b2 #l2 | 2,6,10,14,18: #b2 | 3,7,11,15,19: * [2,4,6,8,10: #b2] | *: ]
154normalize nodelta
155[ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct | *: * #NE ] ]
156[ 1,4: @eq_identifier_elim [ 1,3: #E destruct | *: * #NE ] ]
157normalize % #E destruct try (cases (NE (refl ??))) @refl
[1960]158qed.
159
[2044]160definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
161λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
162match s' return λs'. Ras_Fn_Match ? s' ? → ? with
163[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
164| Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call b ]
165| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
166| Finalstate _ ⇒ λmtc. rapc_fin
167] mtc0 ].
168whd in mtc; cases mtc
169qed.
170
171definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
172λge,pc.
173match pc with
174[ rapc_state b l ⇒
175  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
176    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
177| _ ⇒ None ?
178].
179
[1960]180definition RTLabs_status : genv → abstract_status ≝
[1537]181λge.
[1960]182  mk_abstract_status
[2044]183    (RTLabs_state ge)
184    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
185    RTLabs_deqset
186    (RTLabs_state_to_pc ge)
[1563]187    (λs,c. RTLabs_classify s = c)
[2044]188    (RTLabs_pc_to_cost_label ge)
[1537]189    (λs,s'. match s with
[1601]190      [ mk_Sig s p ⇒
[1563]191        match s return λs. RTLabs_classify s = cl_call → ? with
[1537]192        [ Callstate fd args dst stk m ⇒
193          λ_. match s' with
[1736]194          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
195          | Finalstate r ⇒ stk = [ ]
[1537]196          | _ ⇒ False
197          ]
198        | State f fs m ⇒ λH.⊥
199        | _ ⇒ λH.⊥
200        ] p
[1960]201      ])
[1880]202  (λs. RTLabs_is_final s ≠ None ?).
[1960]203[ normalize in H; destruct
204| normalize in H; destruct
205| whd in H:(??%?);
[1565]206  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
[1877]207  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
[1563]208] qed.
[1559]209
[1960]210(* Allow us to move between the different notions of when a state is cost
211   labelled. *)
212
[2044]213lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge.
214  RTLabs_cost s = true ↔
[1960]215  as_costed (RTLabs_status ge) s.
[2044]216cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
217#ge * *
218[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
219  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
220  whd in match (as_pc_of ??);
221  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
222  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
223  >(lookup_lookup_present … nok)
224  whd in ⊢ (?(??%?)(?(??%?)));
225  % cases (lookup_present ?? (f_graph func) ??) normalize
[1960]226  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
[2044]227  try (% #E' destruct)
228  cases (NONE ?) assumption
229| #fd #args #dst #fs #m #stk #mtc %
230  [ #E normalize in E; destruct
231  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
232    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
233    #H cases (NONE H)
234  ]
235| #v #dst #fs #m #stk #mtc %
236  [ #E normalize in E; destruct
237  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
238    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
239    #H cases (NONE H)
240  ]
241| #r #stk #mtc %
242  [ #E normalize in E; destruct
243  | #E normalize in E; cases (NONE E)
244  ]
[1960]245] qed.
246
[2044]247lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge.
[1670]248  RTLabs_cost s = false →
249  ¬ as_costed (RTLabs_status ge) s.
[2044]250#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
251qed.
[1670]252
[1559]253(* Before attempting to construct a structured trace, let's show that we can
254   form flat traces with evidence that they were constructed from an execution.
255   
256   For now we don't consider I/O. *)
257
258
259coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
260| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
261| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
262| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
263
264(* add I/O? *)
265coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
266| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
267| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
[1880]268| ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
[1559]269
[1707]270coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
271| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
272| nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr').
273
274lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
275  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
276  not_wrong o i ge s' tr'.
277#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
278[ #H105 #H106 #H107 #H108 #H109 destruct
279| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
280] qed.
281
[1559]282let corec make_flat_trace ge s
[1880]283  (NF:RTLabs_is_final s = None ?)
[1559]284  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
285  flat_trace io_out io_in ge s ≝
286let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
287match e return λx. e = x → ? with
288[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
[1880]289| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??)
290| e_wrong m ⇒ λE. ft_wrong … s m ??
[1559]291| e_interact o f ⇒ λE. ⊥
292] (refl ? e).
293[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
294  cases (eval_statement ge s)
295  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
296  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
297    >(?:is_final ????? = RTLabs_is_final s1) //
298    lapply (refl ? (RTLabs_is_final s1))
299    cases (RTLabs_is_final s1) in ⊢ (???% → %);
300    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
301    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
302    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
303    ]
304  | *: #m whd in ⊢ (??%? → ?); #E destruct
305  ]
306| whd in E:(??%?); >exec_inf_aux_unfold in E;
307  cases (eval_statement ge s)
308  [ #O #K whd in ⊢ (??%? → ?); #E destruct
309  | * #tr #s1 whd in ⊢ (??%? → ?);
310    cases (is_final ?????)
311    [ whd in ⊢ (??%? → ?); #E destruct @refl
312    | #i whd in ⊢ (??%? → ?); #E destruct
313    ]
314  | #m whd in ⊢ (??%? → ?); #E destruct
315  ]
316| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
317  cases (eval_statement ge s)
318  [ #O #K whd in ⊢ (??%? → ?); #E destruct
319  | * #tr #s1 whd in ⊢ (??%? → ?);
320    cases (is_final ?????)
321    [ whd in ⊢ (??%? → ?); #E
322      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
323      destruct
324      inversion H
325      [ #a #b #c #E1 destruct
326      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
327      | #m #E1 destruct
328      ]
329    | #i whd in ⊢ (??%? → ?); #E destruct
330    ]
331  | #m whd in ⊢ (??%? → ?); #E destruct
332  ]
333| whd in E:(??%?); >exec_inf_aux_unfold in E;
334  cases (eval_statement ge s)
[1880]335  [ #o #K whd in ⊢ (??%? → ?); #E destruct
336  | * #tr #s1 whd in ⊢ (??%? → ?);
337    lapply (refl ? (RTLabs_is_final s1))
338    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
339    cases (RTLabs_is_final s1) in ⊢ (???% → %);
340    [ #F #E whd in E:(??%?); destruct @F
341    | #r #F #E whd in E:(??%?); destruct
342    ]
343  | #m #E whd in E:(??%?); destruct
344  ]
345| @NF
346| whd in E:(??%?); >exec_inf_aux_unfold in E;
347  cases (eval_statement ge s)
[1559]348  [ #O #K whd in ⊢ (??%? → ?); #E destruct
349  | * #tr1 #s1 whd in ⊢ (??%? → ?);
350    cases (is_final ?????)
351    [ whd in ⊢ (??%? → ?); #E destruct
352    | #i whd in ⊢ (??%? → ?); #E destruct
353    ]
354  | #m whd in ⊢ (??%? → ?); #E destruct @refl
355  ]
356| whd in E:(??%?); >E in H; #H
357  inversion H
358  [ #a #b #c #E destruct
359  | #a #b #c #d #E1 destruct
360  | #m #E1 destruct
361  ]
362] qed.
363
364let corec make_whole_flat_trace p s
365  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
366  (I:make_initial_state ??? p = OK ? s) :
367  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
368let ge ≝ make_global … p in
369let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
370match e return λx. e = x → ? with
371[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
[1880]372| e_step _ _ e' ⇒ λE. make_flat_trace ge s ??
[1559]373| e_wrong m ⇒ λE. ⊥
374| e_interact o f ⇒ λE. ⊥
375] (refl ? e).
376[ whd in E:(??%?); >exec_inf_aux_unfold in E;
377  whd in ⊢ (??%? → ?);
[1880]378  change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
379  cases (RTLabs_is_final s)
380  [ #E whd in E:(??%?); destruct
381  | #r #E % #E' destruct
[1559]382  ]
[1880]383| @(initial_state_is_not_final … I)
[1559]384| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
385  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
386  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
387    [ #a #b #c #E1 destruct
388    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
389      @H1
390    | #m #E1 destruct
391    ]
392  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
393  ]
394| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
395  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
396| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
397  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
398] qed.
399
[1563]400(* Need a way to choose whether a called function terminates.  Then,
401     if the initial function terminates we generate a purely inductive structured trace,
402     otherwise we start generating the coinductive one, and on every function call
403       use the choice method again to decide whether to step over or keep going.
404
405Not quite what we need - have to decide on seeing each label whether we will see
406another or hit a non-terminating call?
407
408Also - need the notion of well-labelled in order to break loops.
409
410
411
412outline:
413
414 does function terminate?
415 - yes, get (bound on the number of steps until return), generate finite
416        structure using bound as termination witness
417 - no,  get (¬ bound on steps to return), start building infinite trace out of
418        finite steps.  At calls, check for termination, generate appr. form.
419
420generating the finite parts:
421
422We start with the status after the call has been executed; well-labelling tells
423us that this is a labelled state.  Now we want to generate a trace_label_return
424and also return the remainder of the flat trace.
425
426*)
427
[1595]428(* [will_return ge depth s trace] says that after a finite number of steps of
429   [trace] from [s] we reach the return state for the current function.  [depth]
430   performs the call/return counting necessary for handling deeper function
431   calls.  It should be zero at the top level. *)
[1637]432inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
[1595]433| wr_step : ∀s,tr,s',depth,EX,trace.
[1565]434    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
[1595]435    will_return ge depth s' trace →
436    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
437| wr_call : ∀s,tr,s',depth,EX,trace.
[1563]438    RTLabs_classify s = cl_call →
[1595]439    will_return ge (S depth) s' trace →
440    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
441| wr_ret : ∀s,tr,s',depth,EX,trace.
[1563]442    RTLabs_classify s = cl_return →
[1595]443    will_return ge depth s' trace →
444    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
[1583]445    (* Note that we require the ability to make a step after the return (this
446       corresponds to somewhere that will be guaranteed to be a label at the
447       end of the compilation chain). *)
[1595]448| wr_base : ∀s,tr,s',EX,trace.
[1563]449    RTLabs_classify s = cl_return →
[1595]450    will_return ge O s (ft_step ?? ge s tr s' EX trace)
[1563]451.
452
[1638]453(* The way we will use [will_return] won't satisfy Matita's guardedness check,
454   so we will measure the length of these termination proofs and use an upper
455   bound to show termination of the finite structured trace construction
456   functions. *)
457
[1637]458let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
459match T with
460[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
461| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
462| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
463| wr_base _ _ _ _ _ _ ⇒ S O
464].
[1638]465
[1637]466include alias "arithmetics/nat.ma".
467
[1638]468(* Specialised to the particular situation it is used in. *)
[1637]469lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
470#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
471whd in ⊢ (??(??%) → ?);
472>commutative_times
473#H lapply (le_plus_b … H)
474#H lapply (le_to_leb_true … H)
475normalize #E destruct
476qed.
[1719]477   
478let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝
479match T with
480[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
481| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
482| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
483| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
484].
[1563]485
[1638]486(* Inversion lemmas on [will_return] that also note the effect on the length
487   of the proof. *)
488lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
[1637]489  RTLabs_classify s = cl_call →
490  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
[1719]491  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
[1637]492#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
493[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
[1719]494| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
[1637]495| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
496| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
497] qed.
[1595]498
[1637]499lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
500  RTLabs_classify s = cl_return →
501  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
502  match d with
[1719]503  [ O ⇒ will_return_end … TM = ❬s', trace❭
[1637]504  | S d' ⇒
[1719]505      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
[1637]506  ].
507#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
508[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
509| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
[1719]510| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
511| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
[1637]512] qed.
513
[1596]514lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
[1637]515  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
516  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
[1719]517  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
[1596]518#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
[1719]519[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
[1637]520| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
521| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
522| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
[1719]523| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
[1637]524| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
525| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
526| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
[1595]527] qed.
528
[1719]529(* When it comes to building bits of nonterminating executions we'll need to be
530   able to glue termination proofs together. *)
531
532lemma will_return_prepend : ∀ge,d1,s1,t1.
533  ∀T1:will_return ge d1 s1 t1.
534  ∀d2,s2,t2.
535  will_return ge d2 s2 t2 →
536  will_return_end … T1 = ❬s2, t2❭ →
537  will_return ge (d1 + S d2) s1 t1.
538#ge #d1 #s1 #tr1 #T1 elim T1
539[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
540  %1 // @(IH … T2) @E
541| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
542| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
543| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
544] qed.
545
546discriminator nat.
547
548lemma will_return_remove_call : ∀ge,d1,s1,t1.
549  ∀T1:will_return ge d1 s1 t1.
550  ∀d2.
551  will_return ge (d1 + S d2) s1 t1 →
552  ∀s2,t2.
553  will_return_end … T1 = ❬s2, t2❭ →
554  will_return ge d2 s2 t2.
555(* The key part of the proof is to show that the two termination proofs follow
556   the same pattern. *)
557#ge #d1x #s1x #t1x #T1 elim T1
558[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
559  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
560                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
561                   >H21 in CL; * #E destruct
562                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
563                   >H35 in CL; * #E destruct
564                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
565                   >H48 in CL; * #E destruct
566                 ]
567  | @E
568  ]
569| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
570  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
571                   >CL in H7; * #E destruct
572                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
573                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
574                   >H35 in CL; #E destruct
575                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
576                   >H48 in CL; #E destruct
577                 ]
578  | @E
579  ]
580| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
581  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
582                   >CL in H7; * #E destruct
583                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
584                   >H21 in CL; #E destruct
585                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
586                   whd in H38:(??%??); destruct //
587                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
588                   whd in H49:(??%??); @⊥ destruct
589                 ]
590  | @E
591  ]
592| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
593  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
594                 >CL in H7; * #E destruct
595               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
596                 >H21 in CL; #E destruct
597               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
598                 whd in H38:(??%??); destruct //
599               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
600                 whd in H49:(??%??); @⊥ destruct
601               ]
602] qed.
603
[1764]604lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
605  ∀T:will_return ge d s t.
606  not_wrong io_out io_in ge s t →
607  will_return_end … T = ❬s', t'❭ →
608  not_wrong io_out io_in ge s' t'.
609#ge #d #s #t #s' #t' #T elim T
610[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
611  [ inversion NW
612    [ #H1 #H2 #H3 #H4 #H5 destruct
613    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
614    ]
615  | @E
616  ]
617| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
618  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
619  | @E
620  ]
621| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
622  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
623  | @E
624  ]
625| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
626  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
627] qed.
628
[1806]629
630lemma will_return_lower : ∀ge,d,s,t.
631  will_return ge d s t →
632  ∀d'. d' ≤ d →
633  will_return ge d' s t.
634#ge #d0 #s0 #t0 #TM elim TM
635[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
636| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
637| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
638  [ #LE @wr_base //
639  | #d' #LE %3 // @IH /2/
640  ]
641| #s #tr #s' #EX #tr #CL *
642  [ #_ @wr_base //
643  | #d' #LE @⊥ /2/
644  ]
645] qed.
646
[1565]647(* We need to ensure that any code we come across is well-cost-labelled.  We may
648   get function code from either the global environment or the state. *)
649
650definition well_cost_labelled_ge : genv → Prop ≝
[2044]651λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
[1565]652
653definition well_cost_labelled_state : state → Prop ≝
654λs. match s with
655[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
656| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
657                          All ? (λf. well_cost_labelled_fn (func f)) fs
658| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
[1713]659| Finalstate _ ⇒ True
[1565]660].
661
[1583]662lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
663  eval_statement ge s = Value ??? 〈tr,s'〉 →
664  well_cost_labelled_ge ge →
665  well_cost_labelled_state s →
666  well_cost_labelled_state s'.
[2025]667#ge #s #tr' #s' #EV cases (eval_preserves … EV)
[1583]668[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
669| #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/
[1681]670(*
[1583]671| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
[1681]672*)
[1583]673| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
674| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
675| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
[1713]676| //
[1583]677] qed.
678
[1586]679lemma rtlabs_jump_inv : ∀s.
680  RTLabs_classify s = cl_jump →
681  ∃f,fs,m. s = State f fs m ∧
682  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
683  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
684*
685[ #f #fs #m #E
686  %{f} %{fs} %{m} %
687  [ @refl
688  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
[1877]689    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
[1586]690    [ %1 %{A} %{B} %{C} @refl
691    | %2 %{A} %{B} @refl
692    ]
693  ]
694| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
695| normalize #H8 #H9 #H10 #H11 #H12 destruct
[1713]696| #r #E normalize in E; destruct
[1586]697] qed.
698
699lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
700  eval_statement ge s = Value ??? 〈tr,s'〉 →
701  well_cost_labelled_state s →
702  RTLabs_classify s = cl_jump →
703  RTLabs_cost s' = true.
704#ge #s #tr #s' #EV #H #CL
705cases (rtlabs_jump_inv s CL)
706#fr * #fs * #m * #Es *
707[ * #r * #l1 * #l2 #Estmt
708  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
709  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
710  >Estmt #LP whd in ⊢ (??%? → ?);
711  (* replace with lemma on successors? *)
[1960]712  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
[1586]713  lapply (Hbody (next fr) (next_ok fr))
714  generalize in ⊢ (???% → ?);
715  >Estmt #LP'
716  whd in ⊢ (% → ?);
717  * #H1 #H2 [ @H1 | @H2 ]
718| * #r * #ls #Estmt
719  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
720  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
721  >Estmt #LP whd in ⊢ (??%? → ?);
722  (* replace with lemma on successors? *)
[2184]723  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
[1586]724  [ 2: (* later *)
725  | *: #E destruct
726  ]
727  lapply (Hbody (next fr) (next_ok fr))
728  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
729  generalize in ⊢ (??(?%)? → ?);
730  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
731  [ #E1 #E2 whd in E2:(??%?); destruct
732  | #l' #E1 #E2 whd in E2:(??%?); destruct
733    cases (All_nth ???? CP ? E1)
734    #H1 #H2 @H2
735  ]
736] qed.
737
[1595]738lemma rtlabs_call_inv : ∀s.
739  RTLabs_classify s = cl_call →
740  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
741* [ #f #fs #m whd in ⊢ (??%? → ?);
742    cases (lookup_present … (next f) (next_ok f)) normalize
[1877]743    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
[1595]744  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
745  | normalize #H411 #H412 #H413 #H414 #H415 destruct
[1713]746  | normalize #H1 #H2 destruct
[1595]747  ] qed.
[1586]748
[1595]749lemma well_cost_labelled_call : ∀ge,s,tr,s'.
750  eval_statement ge s = Value ??? 〈tr,s'〉 →
751  well_cost_labelled_state s →
752  RTLabs_classify s = cl_call →
753  RTLabs_cost s' = true.
754#ge #s #tr #s' #EV #WCL #CL
755cases (rtlabs_call_inv s CL)
756#fd * #args * #dst * #stk * #m #E >E in EV WCL;
757whd in ⊢ (??%? → % → ?);
758cases fd
759[ #fn whd in ⊢ (??%? → % → ?);
[2184]760  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
[1595]761  #m' #b whd in ⊢ (??%? → ?); #E' destruct
762  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
763  @WCL2
764| #fn whd in ⊢ (??%? → % → ?);
765  @bindIO_value #evargs #Eargs
[1656]766  whd in ⊢ (??%? → ?);
767  #E' destruct
[1595]768] qed.
769
[1681]770
771(* The preservation of (most of) the stack is useful to show as_after_return.
[1682]772   We do this by showing that during the execution of a function the lower stack
773   frames never change, and that after returning from the function we preserve
774   the identity of the next instruction to execute.
[2044]775   
776   Note: since this was first written I've introduced the shadow stack of
777   function blocks.  It might be possible to replace some or all of the stack
778   preservation with that.
[1682]779 *)
780
781inductive stack_of_state : list frame → state → Prop ≝
782| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
783| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
784| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
785.
786
[1681]787inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
[1682]788| sp_normal : ∀fs,s1,s2.
789    stack_of_state fs s1 →
790    stack_of_state fs s2 →
791    stack_preserved doesnt_end_with_ret s1 s2
792| sp_finished : ∀s1,f,f',fs,m.
793    next f = next f' →
[1736]794    frame_rel f f' →
[1682]795    stack_of_state (f::fs) s1 →
[1713]796    stack_preserved ends_with_ret s1 (State f' fs m)
[1736]797| sp_stop : ∀s1,r.
798    stack_of_state [ ] s1 →
799    stack_preserved ends_with_ret s1 (Finalstate r)
800| sp_top : ∀fd,args,dst,m,r.
801    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
[1713]802.
[1681]803
[1682]804discriminator list.
[1681]805
[1682]806lemma stack_of_state_eq : ∀fs,fs',s.
807  stack_of_state fs s →
808  stack_of_state fs' s →
809  fs = fs'.
810#fs0 #fs0' #s0 *
811[ #f #fs #m #H inversion H
[1713]812  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
[1682]813| #fd #args #dst #f #fs #m #H inversion H
[1713]814  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
[1682]815| #rtv #dst #fs #m #H inversion H
[1713]816  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
[1682]817] qed.
818
[1713]819lemma stack_preserved_final : ∀e,r,s.
[1736]820  ¬stack_preserved e (Finalstate r) s.
821#e #r #s % #H inversion H
[1713]822[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
823  inversion SOS #a #b #c #d #e #f try #g try #h destruct
[1736]824| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
[1713]825  inversion SOS #a #b #c #d #e #f try #g try #h destruct
[1736]826| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
827  inversion SOS #a #b #c #d #e #f try #g try #h destruct
828| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
[1713]829] qed.
830
[1681]831lemma stack_preserved_join : ∀e,s1,s2,s3.
832  stack_preserved doesnt_end_with_ret s1 s2 →
833  stack_preserved e s2 s3 →
834  stack_preserved e s1 s3.
835#e1 #s1 #s2 #s3 #H1 inversion H1
[1682]836[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
837  #H2 inversion H2
838  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
839    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
[1736]840  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
[1682]841    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
[1736]842  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
843  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
844    inversion S2
845    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
846    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
847    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
848    ]
[1681]849  ]
[1682]850| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
[1713]851| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
[1736]852  cases (stack_preserved_final … H) #r #E destruct
853| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
854  @(absurd … F) //
[1681]855] qed.
856
[1682]857lemma stack_preserved_return : ∀ge,s1,s2,tr.
[1681]858  RTLabs_classify s1 = cl_return →
859  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
860  stack_preserved ends_with_ret s1 s2.
861#ge *
862[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
863  cases (lookup_present ??? (next f) (next_ok f)) in E;
[1877]864  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
[1681]865| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
866| #res #dst *
[1736]867  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
868    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
[1960]869  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV
[1682]870    whd in EV:(??%?); destruct @(sp_finished ? f) //
[1736]871    cases f //
[1681]872  ]
[1713]873| #r #s2 #tr #E normalize in E; destruct
[1681]874] qed.
875
876lemma stack_preserved_step : ∀ge,s1,s2,tr.
877  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
878  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
879  stack_preserved doesnt_end_with_ret s1 s2.
[2025]880#ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
[1681]881[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
882| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
883| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
884  normalize in CL; cases CL #E destruct
885| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
886| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
887  #E normalize in E; destruct
[1713]888| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
[1681]889] qed.
890
891lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
892  RTLabs_classify s1 = cl_call →
893  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
894  stack_preserved ends_with_ret s2 s3 →
895  stack_preserved doesnt_end_with_ret s1 s3.
896#ge #s1 #s2 #s3 #tr #CL #EV #SP
897cases (rtlabs_call_inv … CL)
898#fd * #args * #dst * #stk * #m #E destruct
[1682]899inversion SP
900[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
[1736]901| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
[2025]902  inversion (eval_preserves … EV)
[1682]903  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
904  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
905  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
906    inversion S
907    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
908    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
909    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
910    ]
911  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
912  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
[1713]913  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
[1682]914  ]
[1736]915| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
[2025]916  inversion (eval_preserves … EV)
[1736]917  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
918  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
919  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
920    inversion S1
921    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
922    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
923    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
924    ]
925  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
926  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
927  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
928  ]
929| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
[1682]930] qed.
931 
[2044]932lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.∀tr.
[1682]933  ∀CL : RTLabs_classify s1 = cl_call.
934  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
935  stack_preserved ends_with_ret s2 s3 →
936  as_after_return (RTLabs_status ge) «s1,CL» s3.
[2044]937#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #tr #CL #EV #S23
[1682]938cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
[2044]939whd
[1682]940inversion S23
941[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
[2044]942| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct whd
[2025]943  inversion (eval_preserves … EV)
[1682]944  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
945  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
946  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
947    inversion S
[1736]948    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
[1682]949    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
950    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
951    ]
952  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
953  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
[1713]954  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
[1682]955  ]
[1736]956| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
[2025]957  inversion (eval_preserves … EV)
[1736]958  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
959  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
960  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
961    inversion S1
962    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
963    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
964    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
965    ]
966  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
967  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
968  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
969  ]
970| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
[1682]971] qed.
[1681]972
[1574]973(* Don't need to know that labels break loops because we have termination. *)
974
[1596]975(* A bit of mucking around with the depth to avoid proving termination after
[1638]976   termination.  Note that we keep a proof that our upper bound on the length
977   of the termination proof is respected. *)
[1719]978record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
[2044]979  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
[1719]980  (original_terminates: will_return ge depth start full)
[2044]981  (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
[1719]982{
[2044]983  new_state : RTLabs_state ge;
[1574]984  remainder : flat_trace io_out io_in ge new_state;
985  cost_labelled : well_cost_labelled_state new_state;
[1596]986  new_trace : T new_state;
[1681]987  stack_ok : stack_preserved ends start new_state;
[1719]988  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
989               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
990               | S d ⇒ ΣTM:will_return ge d new_state remainder.
[2044]991                         gt limit (will_return_length … TM) ∧
[1719]992                         will_return_end … original_terminates = will_return_end … TM
[1596]993               ]
[1574]994}.
995
[1638]996(* The same with a flag indicating whether the function returned, as opposed to
997   encountering a label. *)
[1719]998record sub_trace_result (ge:genv) (depth:nat)
[2044]999  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
[1719]1000  (original_terminates: will_return ge depth start full)
[2044]1001  (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
[1719]1002{
[1594]1003  ends : trace_ends_with_ret;
[1719]1004  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
[1594]1005}.
1006
[1638]1007(* We often return the result from a recursive call with an addition to the
1008   structured trace, so we define a couple of functions to help.  The bound on
1009   the size of the termination proof might need to be relaxed, too. *)
1010
[2044]1011definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
[1719]1012  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
1013    will_return_end … TM1 = will_return_end … TM2 →
[1712]1014    T2 (new_state … r) →
[1719]1015    stack_preserved e s2 (new_state … r) →
1016    trace_result ge d e s2 t2 TM2 T2 l2 ≝
1017λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1018  mk_trace_result ge d e s2 t2 TM2 T2 l2
[1574]1019    (new_state … r)
1020    (remainder … r)
1021    (cost_labelled … r)
[1594]1022    trace
[1681]1023    SP
[1719]1024    ?
1025    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
[1637]1026                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
[1719]1027     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
1028.
1029cases e in r ⊢ %;
1030[ <TME -TME * cases d in TM1 TM2 ⊢ %;
1031  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
1032  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
1033    %{TMa} % // @(transitive_le … lGE) @L1
1034  ]
1035| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
1036   * #TMa * #L1 #TME
1037    %{TMa} % // @(transitive_le … lGE) @L1
1038] qed.
[1574]1039
[2044]1040definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
[1719]1041  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
1042    will_return_end … TM1 = will_return_end … TM2 →
[1712]1043    T2 (ends … r) (new_state … r) →
1044    stack_preserved (ends … r) s2 (new_state … r) →
[1719]1045    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
1046λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1047  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
[1637]1048    (ends … r)
[1719]1049    (replace_trace … lGE … r TME trace SP).
[1637]1050
[1638]1051(* Small syntax hack to avoid ambiguous input problems. *)
[1637]1052definition myge : nat → nat → Prop ≝ ge.
1053
[2044]1054let rec make_label_return ge depth (s:RTLabs_state ge)
[1565]1055  (trace: flat_trace io_out io_in ge s)
1056  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
[1574]1057  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
[1583]1058  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
[1596]1059  (TERMINATES: will_return ge depth s trace)
[1637]1060  (TIME: nat)
1061  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
[1719]1062  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
[1638]1063              (trace_label_return (RTLabs_status ge) s)
[2044]1064              (will_return_length … TERMINATES) ≝
[1638]1065             
[1637]1066match TIME return λTIME. TIME ≥ ? → ? with
1067[ O ⇒ λTERMINATES_IN_TIME. ⊥
1068| S TIME ⇒ λTERMINATES_IN_TIME.
[1638]1069
1070  let r ≝ make_label_label ge depth s
1071            trace
1072            ENV_COSTLABELLED
1073            STATE_COSTLABELLED
1074            STATEMENT_COSTLABEL
1075            TERMINATES
1076            TIME ? in
[1719]1077  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
1078                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
[1596]1079  [ ends_with_ret ⇒ λr.
[1712]1080      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
[1596]1081  | doesnt_end_with_ret ⇒ λr.
1082      let r' ≝ make_label_return ge depth (new_state … r)
[1638]1083                 (remainder … r)
1084                 ENV_COSTLABELLED
1085                 (cost_labelled … r) ?
1086                 (pi1 … (terminates … r)) TIME ? in
[1712]1087        replace_trace … r' ?
[1638]1088          (tlr_step (RTLabs_status ge) s (new_state … r)
[1681]1089            (new_state … r') (new_trace … r) (new_trace … r')) ?
[1596]1090  ] (trace_res … r)
[1638]1091
[1637]1092] TERMINATES_IN_TIME
[1574]1093
[1638]1094
[2044]1095and make_label_label ge depth (s:RTLabs_state ge)
[1574]1096  (trace: flat_trace io_out io_in ge s)
1097  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1098  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
[1583]1099  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
[1596]1100  (TERMINATES: will_return ge depth s trace)
[1637]1101  (TIME: nat)
1102  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
[1719]1103  on TIME : sub_trace_result ge depth s trace TERMINATES
[1638]1104              (λends. trace_label_label (RTLabs_status ge) ends s)
1105              (will_return_length … TERMINATES) ≝
1106             
[1637]1107match TIME return λTIME. TIME ≥ ? → ? with
1108[ O ⇒ λTERMINATES_IN_TIME. ⊥
1109| S TIME ⇒ λTERMINATES_IN_TIME.
[1638]1110
[1637]1111let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
[1712]1112  replace_sub_trace … r ?
[1960]1113    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
[1638]1114
[1637]1115] TERMINATES_IN_TIME
[1574]1116
[1638]1117
[2044]1118and make_any_label ge depth (s0:RTLabs_state ge)
1119  (trace: flat_trace io_out io_in ge s0)
[1574]1120  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
[2044]1121  (STATE_COSTLABELLED: well_cost_labelled_state s0)  (* functions in the state *)
1122  (TERMINATES: will_return ge depth s0 trace)
[1637]1123  (TIME: nat)
1124  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
[2044]1125  on TIME : sub_trace_result ge depth s0 trace TERMINATES
1126              (λends. trace_any_label (RTLabs_status ge) ends s0)
[1638]1127              (will_return_length … TERMINATES) ≝
[1637]1128
1129match TIME return λTIME. TIME ≥ ? → ? with
1130[ O ⇒ λTERMINATES_IN_TIME. ⊥
1131| S TIME ⇒ λTERMINATES_IN_TIME.
[2044]1132  match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1133                                      well_cost_labelled_state s →
1134                                      ∀TM:will_return ??? trace.
1135                                      myge ? (times 3 (will_return_length ??? trace TM)) →
1136                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
1137  with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
1138  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1139                               well_cost_labelled_state s →
[1719]1140                               ∀TM:will_return ??? trace.
1141                               myge ? (times 3 (will_return_length ??? trace TM)) →
[2044]1142                               sub_trace_result ge depth (mk_RTLabs_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_state ge s stk mtc)) (will_return_length … TM) with
[1638]1143  [ ft_stop st FINAL ⇒
[2044]1144      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
[1638]1145
[2044]1146  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
1147    let start' ≝ mk_RTLabs_state ge start stk mtc in
1148    let next' ≝ next_state ? start' ?? EV in
1149    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
[1583]1150    [ cl_other ⇒ λCL.
[2044]1151        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
[1638]1152        (* We're about to run into a label. *)
[1960]1153        [ true ⇒ λCS.
[2044]1154            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
[1596]1155              doesnt_end_with_ret
[2044]1156              (mk_trace_result ge … next' trace' ?
1157                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
[1638]1158        (* An ordinary step, keep going. *)
[1583]1159        | false ⇒ λCS.
[2044]1160            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
1161                replace_sub_trace ????????????? r ?
[1638]1162                  (tal_step_default (RTLabs_status ge) (ends … r)
[2044]1163                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
[1583]1164        ] (refl ??)
[1638]1165       
[1586]1166    | cl_jump ⇒ λCL.
[2044]1167        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
[1596]1168          doesnt_end_with_ret
[2044]1169          (mk_trace_result ge … next' trace' ?
1170            (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
[1638]1171           
[1595]1172    | cl_call ⇒ λCL.
[2044]1173        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
1174        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
[1654]1175        (* We're about to run into a label, use base case for call *)
1176        [ true ⇒ λCS.
[2044]1177            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
[1654]1178            doesnt_end_with_ret
[1719]1179            (mk_trace_result ge …
[2044]1180              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
1181                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
[1654]1182        (* otherwise use step case *)
1183        | false ⇒ λCS.
1184            let r' ≝ make_any_label ge depth
1185                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
1186                       (pi1 … (terminates … r)) TIME ? in
[1712]1187            replace_sub_trace … r' ?
[1654]1188              (tal_step_call (RTLabs_status ge) (ends … r')
[2044]1189                start' next' (new_state … r) (new_state … r') ? CL ?
[1681]1190                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
[1654]1191        ] (refl ??)
[1638]1192
[1594]1193    | cl_return ⇒ λCL.
[2044]1194        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
[1596]1195          ends_with_ret
[1719]1196          (mk_trace_result ge …
[2044]1197            next'
[1596]1198            trace'
1199            ?
[2044]1200            (tal_base_return (RTLabs_status ge) start' next' ? CL)
[1681]1201            ?
[1596]1202            ?)
[1583]1203    ] (refl ? (RTLabs_classify start))
[1638]1204   
[2044]1205  | ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥
[1638]1206 
[2044]1207  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
[1637]1208] TERMINATES_IN_TIME.
[1574]1209
[1637]1210[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1211| //
[1712]1212| //
[1719]1213| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1214| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
[1681]1215| @(stack_preserved_join … (stack_ok … r)) //
[2044]1216| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
[1719]1217| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
[1637]1218  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1219  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1220  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
[1681]1221    @(monotonic_le_times_r 3 … LT)
[1637]1222  | @le_S @le_S @le_n
1223  ]
1224| @le_S_S_to_le @TERMINATES_IN_TIME
1225| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1226| @le_n
[1712]1227| //
[2044]1228| @(proj1 … (RTLabs_costed …)) //
[1637]1229| @le_S_S_to_le @TERMINATES_IN_TIME
1230| @(wrl_nonzero … TERMINATES_IN_TIME)
[1713]1231| (* We can't reach the final state because the function terminates with a
1232     return *)
1233  inversion TERMINATES
1234  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1235  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1236  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1237  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1238  ]
[1637]1239| @(will_return_return … CL TERMINATES)
[2044]1240| @(stack_preserved_return … EV) //
1241| %{tr} %{EV} @refl
[1586]1242| @(well_cost_labelled_state_step  … EV) //
[1596]1243| whd @(will_return_notfn … TERMINATES) %2 @CL
[2044]1244| @(stack_preserved_step … EV) /2/
1245| %{tr} %{EV} %
[1654]1246| %1 whd @CL
[2044]1247| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
[1594]1248| @(well_cost_labelled_state_step  … EV) //
[1719]1249| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1250  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1251    #TMx * #LT' #_ @LT'
1252  | <EQr cases (will_return_call … CL TERMINATES)
1253    #TM' * #_ #EQ' @EQ'
1254  ]
[1682]1255| @(stack_preserved_call … EV (stack_ok … r)) //
[2044]1256| %{tr} %{EV} %
1257| @(RTLabs_after_call … next') [2: @EV | skip | // ]
[1719]1258| @(cost_labelled … r)
1259| skip
1260| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1261  @(transitive_lt … LT)
1262  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1263| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
[2044]1264  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
1265| @(RTLabs_after_call … next') [2: @EV | skip | // ]
1266| %{tr} %{EV} %
[1682]1267| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
[1595]1268| @(cost_labelled … r)
[1719]1269| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
[1637]1270  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
[1719]1271  cases (will_return_call … TERMINATES) in GT;
1272  #X * #Y #_ #Z
[1637]1273  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1274  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1275  | //
1276  ]
[1596]1277| @(well_cost_labelled_state_step  … EV) //
1278| @(well_cost_labelled_call … EV) //
[1638]1279| cases (will_return_call … TERMINATES)
[1719]1280  #TM * #GT #_ @le_S_S_to_le
[1637]1281  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1282  @(transitive_le … TERMINATES_IN_TIME)
1283  @(monotonic_le_times_r 3 … GT)
[1596]1284| whd @(will_return_notfn … TERMINATES) %1 @CL
[1682]1285| @(stack_preserved_step … EV) /2/
[2044]1286| %{tr} %{EV} %
[1654]1287| %2 whd @CL
[1596]1288| @(well_cost_labelled_state_step  … EV) //
[1719]1289| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
[2044]1290| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
[1594]1291| @CL
[2044]1292| %{tr} %{EV} %
[1682]1293| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
[1594]1294| @(well_cost_labelled_state_step  … EV) //
[1638]1295| %1 @CL
[1719]1296| cases (will_return_notfn … TERMINATES) #TM * #GT #_
[1637]1297  @le_S_S_to_le
1298  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1299  //
[1574]1300| inversion TERMINATES
[1637]1301  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
1302  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
1303  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
1304  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
[1583]1305  ]
[1713]1306] qed.
[1583]1307
[1638]1308(* We can initialise TIME with a suitably large value based on the length of the
1309   termination proof. *)
[2044]1310let rec make_label_return' ge depth (s:RTLabs_state ge)
[1637]1311  (trace: flat_trace io_out io_in ge s)
1312  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1313  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1314  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1315  (TERMINATES: will_return ge depth s trace)
[1719]1316  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
[1637]1317make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1318  (2 + 3 * will_return_length … TERMINATES) ?.
1319@le_n
1320qed.
[1574]1321 
[1713]1322(* Tail-calls would not be handled properly (which means that if we try to show the
[1617]1323   full version with non-termination we'll fail because calls and returns aren't
1324   balanced.
[1651]1325 *)
1326
1327inductive inhabited (T:Type[0]) : Prop ≝
1328| witness : T → inhabited T.
1329
1330
[1705]1331(* Define a notion of sound labellings of RTLabs programs. *)
[1675]1332
[1705]1333definition actual_successor : state → option label ≝
1334λs. match s with
1335[ State f fs m ⇒ Some ? (next f)
1336| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1337| Returnstate _ _ _ _ ⇒ None ?
[1713]1338| Finalstate _ ⇒ None ?
[1705]1339].
1340
1341lemma nth_opt_Exists : ∀A,n,l,a.
1342  nth_opt A n l = Some A a →
1343  Exists A (λa'. a' = a) l.
1344#A #n elim n
1345[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1346| #m #IH *
1347  [ #a #E normalize in E; destruct
1348  | #a #l #a' #E %2 @IH @E
1349  ]
1350] qed.
1351
1352lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1353  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1354  RTLabs_classify s' = cl_return ∨
1355  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1356#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1357whd in ⊢ (??%? → ?);
1358generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1359[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1360| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
[1960]1361| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1362| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1363| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1364| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1365| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1366| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1367| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1368| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
1369| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
[2184]1370  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
[1705]1371  whd in ⊢ (??%? → ?);
1372  generalize in ⊢ (??(?%)? → ?);
1373  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1374  [ #e #E normalize in E; destruct
1375  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1376  ]
[1960]1377| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
[1705]1378] qed.
1379
[1707]1380(*
[1706]1381lemma steps_to_label_bound_inv : ∀g,l,n.
[1705]1382  steps_to_label_bound g l n →
[1706]1383  ∀H. let stmt ≝ lookup_present … g l H in
1384  ∃n'. n = steps_for_statement stmt + n' ∧
[1705]1385  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
[1706]1386        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
1387        steps_to_label_bound g l' n').
1388#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
1389% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
1390qed.
[1707]1391  *) 
[1719]1392
[1707]1393(*
[1705]1394definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1395
1396let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1397  soundly_labelled_pc (f_graph fn) (f_entry fn).
1398
1399
[1675]1400definition soundly_labelled_frame : frame → Prop ≝
1401λf. soundly_labelled_pc (f_graph (func f)) (next f).
1402
1403definition soundly_labelled_state : state → Prop ≝
1404λs. match s with
1405[ State f _ _ ⇒ soundly_labelled_frame f
1406| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1407| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1408].
[1707]1409*)
1410definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1411λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1412definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1413λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
[1705]1414
[1707]1415inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1416| sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n
1417| sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
1418| sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n)
[1675]1419.
1420
[1707]1421lemma state_bound_on_steps_to_cost_zero : ∀s.
1422  ¬ state_bound_on_steps_to_cost s O.
[1705]1423#s % #H inversion H
[1707]1424[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1425  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1426  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
[1705]1427| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1428| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1429] qed.
1430
1431lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1432  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1433  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
[1713]1434  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
[1705]1435#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1436whd in ⊢ (??%? → ?);
1437generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1438[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1439| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
[1960]1440| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1441| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1442| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1443| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1444| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1445| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1446| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1447| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1448| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
[2184]1449  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
[1705]1450  whd in ⊢ (??%? → ?);
1451  generalize in ⊢ (??(?%)? → ?);
1452  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1453  [ #e #E normalize in E; destruct
1454  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1455  ]
[1960]1456| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
[1705]1457] qed.
1458
[2044]1459lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
[1736]1460  state_bound_on_steps_to_cost s (S n) →
1461  ∀CL:RTLabs_classify s = cl_call.
1462  as_after_return (RTLabs_status ge) «s, CL» s' →
1463  RTLabs_cost s' = false →
1464  state_bound_on_steps_to_cost s' n.
[2044]1465#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); -stk -stk' lapply CL -CL inversion H
[1736]1466[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1467  #fn * #args * #dst * #stk * #m' #E destruct
1468| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1469  whd in S; #CL cases s'
1470  [ #f' #fs' #m' * #N #F #CS
1471    %1 whd
1472    inversion S
1473    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1474      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1475    | #l #n #B #E1 #E2 #_ destruct <N <F @B
1476    ]
1477  | #fd' #args' #dst' #fs' #m' *
1478  | #rv #dst' #fs' #m' *
1479  | #r #E normalize in E; destruct
1480  ]
1481| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1482] qed.
1483
[1707]1484lemma bound_after_step : ∀ge,s,tr,s',n.
1485  state_bound_on_steps_to_cost s (S n) →
[1705]1486  eval_statement ge s = Value ??? 〈tr, s'〉 →
[1706]1487  RTLabs_cost s' = false →
[1705]1488  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
[1707]1489   state_bound_on_steps_to_cost s' n.
1490#ge #s #tr #s' #n #BOUND1 inversion BOUND1
[1705]1491[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1492  #EVAL cases (eval_successor … EVAL)
1493  [ /3/
1494  | * #l * #S1 #S2 #NC %2
[1707]1495  (*
1496    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1497    *)
1498    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
[2025]1499    inversion (eval_preserves … EVAL)
[1707]1500    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1501      >(eval_steps … EVAL) in E2; #En normalize in En;
1502      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1503      %1 inversion (IH … S2)
1504      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1505        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1506        whd in S1:(??%?); destruct >NC in CSx; *
1507      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
[1706]1508      ]
[1707]1509    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1510      >(eval_steps … EVAL) in E2; #En normalize in En;
1511      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1512      %2 @IH normalize in S1; destruct @S2
1513    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
[1705]1514      destruct
[1707]1515    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
[1705]1516      normalize in S1; destruct
[1707]1517    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
[1713]1518    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
[1705]1519    ]
1520  ]
1521| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1522  /3/
1523| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
[2025]1524  #EVAL #NC %2 inversion (eval_preserves … EVAL)
[1705]1525  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1526  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1527  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1528  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1529  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1530    %1 whd in FS ⊢ %;
[1736]1531    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
1532    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
[1705]1533    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
1534    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
[1707]1535    inversion FS
1536    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1537        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
1538        >NC in CSx; *
1539    | #lx #nx #H #E1x #E2x #_ destruct @H
1540    ]
[1713]1541  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
[1705]1542  ]
1543] qed.
[1806]1544
1545
1546
1547
1548definition soundly_labelled_ge : genv → Prop ≝
[2044]1549λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
[1806]1550
1551definition soundly_labelled_state : state → Prop ≝
1552λs. match s with
1553[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1554| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1555                          All ? (λf. soundly_labelled_fn (func f)) fs
1556| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1557| Finalstate _ ⇒ True
1558].
1559
1560lemma steps_from_sound : ∀s.
1561  RTLabs_cost s = true →
1562  soundly_labelled_state s →
1563  ∃n. state_bound_on_steps_to_cost s n.
1564* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
1565whd in ⊢ (% → ?); * #SLF #_
1566cases (SLF (next f) (next_ok f)) #n #B1
1567%{n} % @B1
1568qed.
1569
1570lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1571  soundly_labelled_ge ge →
1572  eval_statement ge s = Value ??? 〈tr,s'〉 →
1573  soundly_labelled_state s →
1574  soundly_labelled_state s'.
1575#ge #s #tr #s' #ENV #EV #S
[2025]1576inversion (eval_preserves … EV)
[1806]1577[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1578  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1579| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1580  whd in S ⊢ %; %
1581  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1582  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1583  ]
1584| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1585  whd in S ⊢ %; @S
1586| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1587  whd in S ⊢ %; cases S //
1588| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
1589  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1590| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1591] qed.
1592
1593lemma soundly_labelled_state_preserved : ∀s,s'.
1594  stack_preserved ends_with_ret s s' →
1595  soundly_labelled_state s →
1596  soundly_labelled_state s'.
1597#s0 #s0' #SP inversion SP
1598[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1599| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
1600  inversion S1
1601  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
1602    * #_ #S whd in S;
1603    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1604    destruct @S
1605  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
1606    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1607    destruct @S
1608  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
1609    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1610    destruct @S
1611  ]
1612| //
1613| //
1614] qed.
1615
[1653]1616(* When constructing an infinite trace, we need to be able to grab the finite
1617   portion of the trace for the next [trace_label_diverges] constructor.  We
1618   use the fact that the trace is soundly labelled to achieve this. *)
1619
[2044]1620record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
[1805]1621  ro_well_cost_labelled: well_cost_labelled_state s;
[1806]1622  ro_soundly_labelled: soundly_labelled_state s;
[1805]1623  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1624  ro_not_undefined: not_wrong … t;
1625  ro_not_final: RTLabs_is_final s = None ?
1626}.
1627
[2044]1628inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
1629| fp_tal : ∀s,s':RTLabs_state ge.
[1653]1630           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
[1805]1631           ∀t:flat_trace io_out io_in ge s'.
1632           remainder_ok ge s' t →
[1653]1633           finite_prefix ge s
[2044]1634| fp_tac : ∀s1,s2,s3:RTLabs_state ge.
[1806]1635           trace_any_call (RTLabs_status ge) s1 s2 →
1636           well_cost_labelled_state s2 →
[2044]1637           as_execute (RTLabs_status ge) s2 s3 →
[1806]1638           ∀t:flat_trace io_out io_in ge s3.
1639           remainder_ok ge s3 t →
1640           finite_prefix ge s1
[1653]1641.
1642
[2044]1643definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
[1653]1644  RTLabs_classify s = cl_other →
1645  finite_prefix ge s' →
[2044]1646  as_execute (RTLabs_status ge) s s' →
[1653]1647  RTLabs_cost s' = false →
1648  finite_prefix ge s ≝
1649λge,s,s',OTHER,fp.
[2044]1650match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
[1805]1651[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
[1670]1652    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
[1805]1653    rem rok
[2044]1654| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
[1806]1655    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1656    WCL2 EV rem rok
[1653]1657].
[1670]1658
[2044]1659definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
1660  as_execute (RTLabs_status ge) s s1 →
[1653]1661  ∀CALL:RTLabs_classify s = cl_call.
[1806]1662  finite_prefix ge s'' →
1663  trace_label_return (RTLabs_status ge) s1 s'' →
1664  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1665  RTLabs_cost s'' = false →
[1653]1666  finite_prefix ge s ≝
[1806]1667λge,s,s1,s'',EVAL,CALL,fp.
[2044]1668match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
[1806]1669[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1670    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
[1805]1671    rem rok
[2044]1672| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
[1806]1673    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1674    WCL2 EV rem rok
[1653]1675].
[1670]1676
[1765]1677lemma not_return_to_not_final : ∀ge,s,tr,s'.
1678  eval_statement ge s = Value ??? 〈tr, s'〉 →
1679  RTLabs_classify s ≠ cl_return →
1680  RTLabs_is_final s' = None ?.
1681#ge #s #tr #s' #EV
[2025]1682inversion (eval_preserves … EV) //
[1765]1683#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1684@⊥ @(absurd ?? CL) @refl
1685qed.
1686
[1670]1687definition termination_oracle ≝ ∀ge,depth,s,trace.
[1671]1688  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
[1670]1689
[2044]1690let rec finite_segment ge (s:RTLabs_state ge) n trace
[1670]1691  (ORACLE: termination_oracle)
[1805]1692  (TRACE_OK: remainder_ok ge s trace)
[1670]1693  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
[1806]1694  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
[1707]1695  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
[2044]1696  on n : finite_prefix ge s ≝
[1707]1697match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
[1705]1698[ O ⇒ λLABEL_LIMIT. ⊥
[2044]1699| S n' ⇒
1700  match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace'.
1701    match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_state ge s ? mtc) with
1702    [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
1703    | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
1704        let start' ≝ mk_RTLabs_state ge start stk mtc in
1705        let next' ≝ next_state ge start' next tr EV in
[1670]1706        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1707        [ cl_other ⇒ λCL.
[1805]1708            let TRACE_OK' ≝ ? in
[1670]1709            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1710            [ true ⇒ λCS.
[2044]1711                fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
[1670]1712            | false ⇒ λCS.
[2044]1713                let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1714                fp_add_default ge start' next' CL fs ? CS
[1670]1715            ] (refl ??)
1716        | cl_jump ⇒ λCL.
[2044]1717            fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
[1707]1718        | cl_call ⇒ λCL.
[2044]1719            match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
[1671]1720            [ or_introl TERMINATES ⇒
1721              match TERMINATES with [ witness TERMINATES ⇒
[2044]1722                let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
[1805]1723                let TRACE_OK' ≝ ? in
[2044]1724                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
1725                [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
[1707]1726                | false ⇒ λCS.
[1812]1727                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
[1707]1728                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
[1671]1729                ] (refl ??)
1730              ]
1731            | or_intror NO_TERMINATION ⇒
[2044]1732                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?
[1707]1733            ]
[1670]1734        | cl_return ⇒ λCL. ⊥
1735        ] (refl ??)
[2044]1736    | ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
1737    ] mtc0
1738  ] trace TRACE_OK
[1705]1739] LABEL_LIMIT.
[1707]1740[ cases (state_bound_on_steps_to_cost_zero s) /2/
[1805]1741| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1742| @(absurd ?? (ro_no_termination … TRACE_OK))
[1670]1743     %{0} % @wr_base //
[2044]1744| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
1745| 5,6,9,10,11: /3/
1746| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
1747  % [ @(well_cost_labelled_state_step … EV) //
1748    | @(soundly_labelled_state_step … EV) //
[1805]1749    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
[2044]1750    | @(still_not_wrong … EV) //
[1805]1751    | @(not_return_to_not_final … EV) >CL % #E destruct
1752    ]
[2044]1753| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
1754| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
1755| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
1756  @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
[1805]1757| % [ /2/
[1806]1758    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
[2044]1759      @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
[1805]1760    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1761      @wr_call //
1762      @(will_return_prepend … TERMINATES … TM1)
1763      cases (terminates … tlr) //
1764    | @(will_return_not_wrong … TERMINATES)
[2044]1765      [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK)
[1805]1766      | cases (terminates … tlr) //
1767      ]
1768    | (* By stack preservation we cannot be in the final state *)
1769      inversion (stack_ok … tlr)
1770      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1771      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
[2044]1772      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct whd in S:(??%); -next' -s0
[1805]1773        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
[2025]1774        inversion (eval_preserves … EV)
[2044]1775        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 @⊥ -next destruct ]
1776        #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
[1805]1777        inversion S
1778        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
1779        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1780           so we can use it as a witness that at least one frame exists *)
1781        inversion LABEL_LIMIT
1782        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1783      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1784      ]
1785    ]
[2044]1786| @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
1787| @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
[1806]1788| /2/
[2044]1789| %{tr} %{EV} %
1790| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
1791  % [ @(well_cost_labelled_state_step … EV) /2/
[1806]1792    | @(soundly_labelled_state_step … EV) /2/
1793    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1794      @(will_return_lower … TM) //
1795    | @(still_not_wrong … EV) /2/
1796    | @(not_return_to_not_final … EV) >CL % #E destruct
1797    ]
[2044]1798| %2 @CL
1799| 21,22: %{tr} %{EV} %
[1707]1800| cases (bound_after_step … LABEL_LIMIT EV ?)
[1805]1801  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
[1707]1802    inversion trace'
[1805]1803    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
[1765]1804      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1805      % >CL #E destruct
[1805]1806    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
[1765]1807      @wr_base //
[1805]1808    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
1809      inversion (ro_not_undefined … TRACE_OK)
[1707]1810      [ #H137 #H138 #H139 #H140 #H141 destruct
[1880]1811      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
[1707]1812        inversion H148
1813        [ #H153 #H154 #H155 #H156 #H157 destruct
1814        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
1815        ]
1816      ]
1817    ]
1818    ]
1819    | >CL #E destruct
1820    ]
1821  | //
1822  | //
1823  ]
[2044]1824| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
1825  % [ @(well_cost_labelled_state_step … EV) //
1826    | @(soundly_labelled_state_step … EV) //
[1805]1827    | @(not_to_not … (ro_no_termination … TRACE_OK))
1828      * #depth * #TERM %{depth} % @wr_step /2/
1829    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
1830    | @(not_return_to_not_final … EV) >CL % #E destruct
1831    ]
1832| inversion (ro_not_undefined … TRACE_OK)
[1707]1833  [ #H169 #H170 #H171 #H172 #H173 destruct
1834  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
1835  ]
[1765]1836] qed.
[1670]1837
[1808]1838(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1839       a trace_label_diverges value, but I only know how to construct those
1840       using a cofixpoint in Type[0], which means I can't use the termination
1841       oracle.
[1806]1842*)
[1784]1843
[2044]1844let corec make_label_diverges ge (s:RTLabs_state ge)
[1651]1845  (trace: flat_trace io_out io_in ge s)
[1784]1846  (ORACLE: termination_oracle)
[1805]1847  (TRACE_OK: remainder_ok ge s trace)
[1651]1848  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
[1784]1849  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
[1651]1850  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
[1808]1851  : trace_label_diverges_exists (RTLabs_status ge) s ≝
[1812]1852match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
[1784]1853[ ex_intro n B ⇒
[1812]1854    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
[2044]1855      return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
[1784]1856    with
[1805]1857    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
[1812]1858        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
[2044]1859            tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
[1808]1860(*
[1812]1861        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
[1784]1862        [ ex_intro T' _ ⇒
1863            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
[1808]1864        ]*)
[2044]1865    | fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
[1812]1866        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
[2044]1867            tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
[1808]1868(*
[1812]1869        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
[1806]1870        [ ex_intro T' _ ⇒
1871            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
[1808]1872        ]*)
[1784]1873    ] STATEMENT_COSTLABEL
1874].
[2044]1875[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
1876| @EV
[1806]1877| @(trace_any_call_call … T)
[2044]1878| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T)
[1812]1879] qed.
1880
[1880]1881lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'.
1882  make_initial_state p = OK ? s1 →
1883  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
1884  stack_preserved ends_with_ret s2 s' →
1885  RTLabs_is_final s' ≠ None ?.
1886#ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?);
1887@bind_ok #m #_
1888@bind_ok #b #_
1889@bind_ok #f #_
1890#E destruct
[2025]1891#EV #SP inversion (eval_preserves … EV)
[1880]1892[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
1893     inversion SP
1894     [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct
1895     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct
1896          inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct
1897     ]
1898| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct
1899] qed.
1900
1901lemma initial_state_is_call : ∀p,s.
1902  make_initial_state p = OK ? s →
1903  RTLabs_classify s = cl_call.
1904#p #s whd in ⊢ (??%? → ?);
1905@bind_ok #m #_
1906@bind_ok #b #_
1907@bind_ok #f #_
1908#E destruct
1909@refl
1910qed.
1911
[2044]1912let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
[1812]1913  (ORACLE: termination_oracle)
1914  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1915  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
[2044]1916  : ∀trace: flat_trace io_out io_in ge s.
1917    ∀INITIAL: make_initial_state p = OK state s.
[1880]1918    ∀NOT_WRONG: not_wrong ??? s trace.
[1812]1919    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
1920    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
[2044]1921    trace_whole_program_exists (RTLabs_status ge) s ≝
1922match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1923                   make_initial_state p = OK ? s →
1924                   not_wrong ??? s trace →
1925                   well_cost_labelled_state s →
1926                   soundly_labelled_state s →
1927                   trace_whole_program_exists (RTLabs_status ge) s with
1928[ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace.
1929match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1930                             make_initial_state p = OK state s →
[1880]1931                             not_wrong ??? s trace →
[1812]1932                             well_cost_labelled_state s →
1933                             soundly_labelled_state s →
[2044]1934                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
1935[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
[1880]1936    let IS_CALL ≝ initial_state_is_call … INITIAL in
[2044]1937    let s' ≝ mk_RTLabs_state ge s stk mtc in
1938    let next' ≝ next_state ge s' next tr EV in
[1812]1939    match ORACLE ge O next trace' with
1940    [ or_introl TERMINATES ⇒
1941        match TERMINATES with
1942        [ witness TERMINATES ⇒
[2044]1943          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1944          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
[1812]1945        ]
[2044]1946    | or_intror NO_TERMINATION ⇒
1947        twp_diverges (RTLabs_status ge) s' next' IS_CALL ?
1948         (make_label_diverges ge next' trace' ORACLE ?
[1812]1949            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1950    ]
[2044]1951| ft_stop st FINAL ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
1952| ft_wrong start m NF EV ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
1953] mtc0 ].
[1880]1954[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
[1812]1955  cases FINAL #E @E @refl
[2044]1956| %{tr} %{EV} %
[1880]1957| @(after_the_initial_call_is_the_final_state … INITIAL EV)
1958  @(stack_ok … tlr)
[1812]1959| @(well_cost_labelled_state_step … EV) //
1960| @(well_cost_labelled_call … EV) //
[2044]1961| %{tr} %{EV} %
[1812]1962| @(well_cost_labelled_call … EV) //
1963| % [ @(well_cost_labelled_state_step … EV) //
1964    | @(soundly_labelled_state_step … EV) //
1965    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1966    | @(still_not_wrong … NOT_WRONG)
1967    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1968    ]
1969| inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
1970] qed.
1971
1972(*
1973theorem program_trace_exists :
1974  termination_oracle →
1975  ∀p:RTLabs_program.
1976  ∀s:state.
1977  ∀I: make_initial_state p = OK ? s.
1978 
1979  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1980 
1981  ∀NOIO:exec_no_io … plain_trace.
1982 
1983  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
1984 
1985  trace_whole_program_exists (RTLabs_status (make_global p)) s.
1986#ORACLE #p #s #I
1987letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1988#NOIO
1989letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
1990whd
1991@(whole_structured_trace_exists … flat_trace)
1992//
1993[ whd
[1880]1994*)
1995
[2044]1996lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
1997  as_execute (RTLabs_status ge) s s' →
1998  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
1999#ge #s #s' * #tr * #EX #_ %{tr} @EX
2000qed.
2001
[1880]2002(* as_execute might be in Prop, but because the semantics is deterministic
2003   we can retrieve the event trace anyway. *)
[2044]2004
2005let rec deprop_execute ge (s,s':state)
2006  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
[1880]2007: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
[2044]2008match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
[1880]2009[ Value ts ⇒ λY. «fst … ts, ?»
2010| _ ⇒ λY. ⊥
2011] X.
2012[ 1,3: cases Y #x #E destruct
2013| cases Y #trP #E destruct @refl
2014] qed.
2015
[2044]2016let rec deprop_as_execute ge (s,s':RTLabs_state ge)
2017  (X:as_execute (RTLabs_status ge) s s')
2018: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
2019deprop_execute ge s s' ?.
2020cases X #tr * #EX #_ %{tr} @EX
2021qed.
2022
[1880]2023(* A non-empty finite section of a flat_trace *)
2024inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
2025| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
2026| pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''.
2027
2028let rec append_partial_flat_trace o i ge s1 s2 s3
2029  (tr1:partial_flat_trace o i ge s1 s2)
2030on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
2031match tr1 with
2032[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
2033| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
2034].
2035
2036let rec partial_to_flat_trace o i ge s1 s2
2037  (tr:partial_flat_trace o i ge s1 s2)
2038on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
2039match tr with
2040[ pft_base s tr s' EX ⇒ ft_step … EX
2041| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
2042].
2043
2044(* Extract a flat trace from a structured one. *)
[2044]2045let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
[1880]2046  (tr:trace_label_return (RTLabs_status ge) s s')
2047on tr :
2048  partial_flat_trace io_out io_in ge s s' ≝
2049match tr with
[1960]2050[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
[1880]2051| tlr_step s1 s2 s3 tll tlr ⇒
2052  append_partial_flat_trace …
[1960]2053    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
2054    (flat_trace_of_label_return ge s2 s3 tlr)
[1880]2055]
[2044]2056and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
[1880]2057  (tr:trace_label_label (RTLabs_status ge) ends s s')
2058on tr :
2059  partial_flat_trace io_out io_in ge s s' ≝
2060match tr with
[1960]2061[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
[1880]2062]
[2044]2063and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
[1880]2064  (tr:trace_any_label (RTLabs_status ge) ends s s')
2065on tr :
2066  partial_flat_trace io_out io_in ge s s' ≝
2067match tr with
2068[ tal_base_not_return s1 s2 EX CL CS ⇒
2069    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2070    pft_base … EX' ]
2071| tal_base_return s1 s2 EX CL ⇒
2072    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2073    pft_base … EX' ]
2074| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
[1960]2075    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
[1880]2076    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2077    pft_step … EX' suffix' ]
2078| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
2079    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2080    pft_step … EX'
2081      (append_partial_flat_trace …
[1960]2082        (flat_trace_of_label_return ge ?? tlr)
2083        (flat_trace_of_any_label ge ??? tal))
[1880]2084    ]
2085| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
2086    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
[1960]2087      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
[1880]2088    ]
2089].
2090
2091
2092(* We take an extra step so that we can always return a non-empty trace to
2093   satisfy the guardedness condition in the cofixpoint. *)
[2044]2094let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
[1880]2095  (tr:trace_any_call (RTLabs_status ge) s s')
2096  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2097on tr :
[2044]2098  partial_flat_trace io_out io_in ge s s'' ≝
2099match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
[1880]2100[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
2101| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
2102    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
2103    pft_step … EX'
2104      (append_partial_flat_trace …
[1960]2105        (flat_trace_of_label_return ge ?? tlr)
2106        (flat_trace_of_any_call ge … tac EX''))
[1880]2107    ]
2108| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
2109    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2110    pft_step … EX'
[1960]2111     (flat_trace_of_any_call ge … tal EX'')
[1880]2112    ]
2113] EX''.
2114
[2044]2115let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
[1880]2116  (tr:trace_label_call (RTLabs_status ge) s s')
2117  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2118on tr :
2119  partial_flat_trace io_out io_in ge s s'' ≝
2120match tr with
[1960]2121[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
[1880]2122] EX''.
2123
2124(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
2125   to take care to satisfy the guardedness condition by witnessing the fact that
2126   the partial traces are non-empty. *)
[2044]2127let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
[1880]2128  (tr:trace_label_diverges (RTLabs_status ge) s)
2129: flat_trace io_out io_in ge s ≝
[2044]2130match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
[1880]2131[ tld_step sx sy tll tld ⇒
[2044]2132  match sy in RTLabs_state return λsy:RTLabs_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_state sy' stk mtc0 ⇒
2133    λtll.
2134    match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s2 stk mtc) → flat_trace ??? s1 with
2135    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2136    | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
2137    ] mtc0 ] tll tld
2138| tld_base s1 s2 s3 tlc EX CL tld ⇒
2139  match s3 in RTLabs_state return λs3:RTLabs_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_state s3' stk mtc0 ⇒
2140    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2141      match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s3 stk mtc) → flat_trace ??? s1 with
2142      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2143      | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
2144      ] mtc0
[1880]2145    ]
[2044]2146  ] EX tld
[1880]2147]
2148(* Helper to keep adding the partial trace without violating the guardedness
2149   condition. *)
[2044]2150and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
2151: partial_flat_trace io_out io_in ge s s' →
2152  trace_label_diverges (RTLabs_status ge) s' →
2153  flat_trace io_out io_in ge s ≝
2154match s' return λs':RTLabs_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_state sx stk mtc ⇒
2155λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s' ? mtc) → flat_trace io_out io_in ge s with
2156[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
2157| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_state ge s3 stk mtc) tr' tr)
2158] mtc ]
2159.
[1880]2160
[2044]2161
[1880]2162coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2163| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2164| eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2)
2165| eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX).
2166
2167(* XXX move to semantics *)
2168lemma final_cannot_move : ∀ge,s.
2169  RTLabs_is_final s ≠ None ? →
2170  ∃err. eval_statement ge s = Wrong ??? err.
2171#ge *
2172[ #f #fs #m * #F cases (F ?) @refl
2173| #a #b #c #d #e * #F cases (F ?) @refl
2174| #a #b #c #d * #F cases (F ?) @refl
2175| #r #F % [2: @refl | skip ]
2176] qed.
2177
2178let corec flat_traces_are_determined_by_starting_point ge s tr1
2179: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2180match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2181[ ft_stop s F ⇒ λtr2. ?
2182| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2183    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2184    [ ft_stop s F ⇒ λEX. ?
2185    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2186    | ft_wrong s m NF EX' ⇒ λEX. ?
2187    ] EX0
2188| ft_wrong s m NF EX ⇒ λtr2. ?
2189].
2190[ inversion tr2 in tr1 F;
2191  [ #s #F #_ #_ #tr1 #F' @eft_stop
2192  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2193    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2194  | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/
2195  ]
2196| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2197| -EX0
2198  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2199  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2200  -E -EX' -tr2' #tr2' #EX'
2201  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2202  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2203  -E -EX' #EX'
2204    @eft_step @flat_traces_are_determined_by_starting_point
2205| @⊥ >EX in EX'; #E destruct
2206| inversion tr2 in NF EX;
2207  [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/
2208  | #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct
2209  | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.
2210    #E destruct
2211    @eft_wrong
2212  ]
2213] qed.
2214
[2044]2215let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
[1880]2216  (str:trace_label_diverges (RTLabs_status ge) s)
2217  (tr:flat_trace io_out io_in ge s)
[1960]2218: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
[1880]2219@flat_traces_are_determined_by_starting_point
2220qed.
2221
[2044]2222let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
[1880]2223  (tr:trace_whole_program (RTLabs_status ge) s)
2224on tr : flat_trace io_out io_in ge s ≝
[2044]2225match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
[1880]2226[ twp_terminating s1 s2 sf CL EX tlr F ⇒
[2044]2227    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2228      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
[1880]2229    ]
2230| twp_diverges s1 s2 CL EX tld ⇒
2231    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
[1960]2232      ft_step … EX' (flat_trace_of_label_diverges … tld)
[1880]2233    ]
2234].
2235
[2044]2236let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
[1880]2237  (str:trace_whole_program (RTLabs_status ge) s)
2238  (tr:flat_trace io_out io_in ge s)
[1960]2239: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
[1880]2240@flat_traces_are_determined_by_starting_point
2241qed.
Note: See TracBrowser for help on using the repository browser.