source: src/RTLabs/Traces.ma @ 2296

Last change on this file since 2296 was 2296, checked in by campbell, 7 years ago

Tidy up some ill-placed definitions.

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