source: src/RTLabs/Traces.ma @ 2475

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

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

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