source: src/RTLabs/Traces.ma @ 2313

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

RTLabs cost checker correct.

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