source: src/common/StatusSimulation.ma @ 2799

Last change on this file since 2799 was 2799, checked in by tranquil, 8 years ago
  • added taaf_to_taa, conversion from trace_any_any_free to trace_any_any, with a proof obbligation
File size: 38.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/StructuredTraces.ma".
16
17(* We work with two relations on states in parallel, as well as two derived ones.
18   sem_rel is the classic semantic relation between states, keeping track of
19   memory and how program counters are mapped between languages.
20   call_rel keeps track of what pcs corresponding calls have and just that:
21   this is different than corresponance between program counters in sem_rel when
22   CALL f ↦ instr* CALL f instr* *)
23
24record status_rel
25  (S1 : abstract_status)
26  (S2 : abstract_status)
27  : Type[1] ≝
28  { sem_rel :2> S1 → S2 → Prop
29  (* this is kept separate, as not necessarily carrier will
30     synchronise on calls. It should state the minimal properties
31     necessary for as_after_return (typically just the program counter)
32     maybe what function is called too? *)
33  ; call_rel : (Σs.as_classifier S1 s cl_call) →
34               (Σs.as_classifier S2 s cl_call) → Prop
35  ; sim_final :
36    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
37  }.
38
39(* The two derived relations are
40   label_rel which tells that the two states are colabelled
41   ret_rel which tells that two return states are in relation: the idea is that
42   it happens when "going back" through as_after_return on one side we get
43   a pair of call_rel related states, then we enjoy as_after_return also on the
44   other. Roughly call_rel will store just enough information so that we can
45   advance locally on a return step and build structured traces any way *)
46
47(* if we later generalise, we should move this inside status_rel *)
48definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
49
50definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
51  λs1_ret,s2_ret.
52  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
53                 call_rel ?? R s1_pre s2_pre →
54                 as_after_return S2 s2_pre s2_ret.
55
56(* the equivalent of a collapsable trace_any_label where we do not force
57   costedness of the lookahead status *)
58inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
59| taaf_base : ∀s.trace_any_any_free S s s
60| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
61  as_classifier S s2 cl_other →
62  trace_any_any_free S s1 s3
63| taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
64  as_classifier S s2 cl_jump →
65  as_costed S s3 →
66  trace_any_any_free S s1 s3.
67
68definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
69match taaf with
70[ taaf_base _ ⇒ false
71| _ ⇒ true
72].
73
74(* the base property we ask for simulation to work depends on the status_class
75   S will mark semantic relation, C call relation, L label relation, R return relation *)
76
77definition status_simulation ≝
78  λS1 : abstract_status.
79  λS2 : abstract_status.
80  λsim_status_rel : status_rel S1 S2.
81    ∀st1,st1',st2.as_execute S1 st1 st1' →
82    sim_status_rel st1 st2 →
83      match as_classify … st1 with
84      [ cl_call ⇒ ∀prf.
85        (*
86             st1' ------------S----------\
87              ↑ \                         \
88             st1 \--L--\                   \
89              | \       \                   \
90              S  \-C-\  st2_after_call →taa→ st2'
91              |       \     ↑
92             st2 →taa→ st2_pre_call
93        *)
94        ∃st2_pre_call.
95        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
96        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
97        ∃st2_after_call,st2'.
98        ∃taa2 : trace_any_any … st2 st2_pre_call.
99        ∃taa2' : trace_any_any … st2_after_call st2'.
100        as_execute … st2_pre_call st2_after_call ∧
101        sim_status_rel st1' st2' ∧
102        label_rel … st1' st2_after_call
103      | cl_tailcall ⇒ ∀prf.
104        (*
105             st1' ------------S----------\
106              ↑ \                         \
107             st1 \--L--\                   \
108              |         \                   \
109              S         st2_after_call →taa→ st2'
110              |             ↑
111             st2 →taa→ st2_pre_call
112        *)
113        ∃st2_pre_call.
114        as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
115        ∃st2_after_call,st2'.
116        ∃taa2 : trace_any_any … st2 st2_pre_call.
117        ∃taa2' : trace_any_any … st2_after_call st2'.
118        as_execute … st2_pre_call st2_after_call ∧
119        sim_status_rel st1' st2' ∧
120        label_rel … st1' st2_after_call
121      | cl_return ⇒
122        (*
123             st1
124            / ↓
125           | st1'----------S,L------------\
126           S   \                           \
127            \   \-----R-------\            |     
128             \                 |           |
129             st2 →taa→ st2_ret |           |
130                          ↓   /            |
131                     st2_after_ret →taaf→ st2'
132
133           we also ask that st2_after_ret be not labelled if the taaf tail is
134           not empty
135        *)
136        ∃st2_ret,st2_after_ret,st2'.
137        ∃taa2 : trace_any_any … st2 st2_ret.
138        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
139        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
140        as_classifier … st2_ret cl_return ∧
141        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
142        ret_rel … sim_status_rel st1' st2_after_ret ∧
143        label_rel … st1' st2'
144      | cl_other ⇒
145          (*         
146          st1 → st1'
147            |      \
148            S      S,L
149            |        \
150           st2 →taaf→ st2'
151           
152           the taaf can be empty (e.g. tunneling) but we ask it must not be the
153           case when both st1 and st1' are labelled (we would be able to collapse
154           labels otherwise)
155         *)
156        ∃st2'.
157        ∃taa2 : trace_any_any_free … st2 st2'.
158        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
159        sim_status_rel st1' st2' ∧
160        label_rel … st1' st2'
161      | cl_jump ⇒
162        (* just like cl_other, but with a hypothesis more *)
163        as_costed … st1' →
164        ∃st2'.
165        ∃taa2 : trace_any_any_free … st2 st2'.
166        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
167        sim_status_rel st1' st2' ∧
168        label_rel … st1' st2'
169    ].
170
171
172(* some useful lemmas *)
173
174let rec taa_append_taa S st1 st2 st3
175  (taa : trace_any_any S st1 st2) on taa :
176  trace_any_any S st2 st3 →
177  trace_any_any S st1 st3 ≝
178  match taa
179  with
180  [ taa_base st1' ⇒ λst3,taa2.taa2
181  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
182    taa_step ???? H I J (taa_append_taa … tl taa2)
183  ] st3.
184
185definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
186if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
187trace_any_any S s1 s2 ≝
188λS,s1,s2,taaf.
189match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
190  trace_any_any S s1 s2 with
191[ taaf_base s ⇒ λ_.taa_base …
192| taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
193  taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
194| taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
195].
196
197lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
198  ∀taa1 : trace_any_any S s1 s2.
199  ∀taa2 : trace_any_any S s2 s3.
200  ∀tal : trace_any_label S fl s3 s4.
201  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
202#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
203[ #s1 #taa2 #tal %
204| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
205  normalize >IH %
206]
207qed.
208
209lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
210  ∀taa1 : trace_any_any S s1 s2.
211  ∀taa2 : trace_any_any S s2 s3.
212  ∀taa3 : trace_any_any S s3 s4.
213  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
214  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
215#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
216[ #s1 #taa2 #tal %
217| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
218  normalize >IH %
219]
220qed.
221
222let rec taa_append_tal_rel S1 fl1 st1 st1'
223  (tal1 : trace_any_label S1 fl1 st1 st1')
224  S2 st2 st2mid fl2 st2'
225  (taa2 : trace_any_any S2 st2 st2mid)
226  (tal2 : trace_any_label S2 fl2 st2mid st2')
227  on tal1 :
228  tal_rel … tal1 tal2 →
229  tal_rel … tal1 (taa2 @ tal2) ≝
230match tal1 return λfl1,st1,st1',tal1.? with
231  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
232  | tal_base_return st1 st1' _ _ ⇒ ?
233  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
234  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ?
235  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
236  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
237  ].
238[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
239| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
240| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
241  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
242  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
243  ]
244| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ'
245| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
246  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
247  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
248  ]
249| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
250]
251destruct
252<associative_taa_append_tal
253  [1,2,3,4,5:%{(refl …)}] %{st2mid}
254  [1,2:|*: %{G2} %{EQcall} ]
255  %{(taa_append_taa … taa2 taa2')}
256  [1,2: %{H2} %{G2} [%{K2}] %
257  |5: %{st2mid'} %{H2} %{tlr2} % //
258  |*: %{st2mid'} %{H2}
259    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
260    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
261  ]
262qed.
263
264(*
265check trace_any_label_label
266let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
267  on tal : as_costed … st2 ≝
268  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
269  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
270  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
271  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
272  | tal_base_return _ _ _ _ ⇒ λprf.⊥
273  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
274  ] (refl …).
275[ destruct
276|*: >prf %
277]
278qed.
279*)
280
281lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
282  if taa_non_empty … taa then ¬as_costed … s2 else True.
283#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
284[ #s1 %
285| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
286  [ #s2 #H #K #_ assumption
287  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
288  ]
289]
290qed.
291
292let rec tal_collapsable_to_rel S fl st1 st2
293  (tal : trace_any_label S fl st1 st2) on tal :
294  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
295  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
296  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
297  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
298  with
299  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
300  | tal_base_not_return _ st2' _ _ K ⇒ ?
301  | _ ⇒ Ⓧ
302  ].
303* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
304qed.
305
306let rec tal_collapsable_eq_flag S fl st1 st2
307  (tal : trace_any_label S fl st1 st2) on tal :
308  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
309  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
310  with
311  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
312  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
313  | _ ⇒ Ⓧ
314  ].
315
316let rec tal_collapsable_split S fl st1 st2
317  (tal : trace_any_label S fl st1 st2) on tal :
318  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
319  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
320  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
321  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
322  with
323  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
324  | tal_base_not_return st1' st2' H I J ⇒ ?
325  | _ ⇒ Ⓧ
326  ].
327[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
328| #coll
329  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
330  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
331  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
332  #EQ >EQ %
333]
334qed.
335
336lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
337tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
338  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
339#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
340elim (tal_collapsable_split … coll) lapply tal
341 >(tal_collapsable_eq_flag … coll) -tal #tal
342#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
343%[|%[|%[|%[|%[| % ]]]]]
344qed.
345
346definition taaf_append_tal : ∀S,st1,fl,st2,st3.
347  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
348  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
349  match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
350  trace_any_label S fl st1 st3 with
351  [ taaf_base s ⇒ λ_.λtal.tal
352  | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
353  | taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J)
354  ]. 
355
356lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
357  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
358  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
359#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize
360[ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ]
361#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
362change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
363<associative_taa_append_tal /2 by taa_append_tal_rel/
364qed.
365
366(* little helpers *)
367lemma if_else_True : ∀b,P.P → if b then P else True.
368* // qed-.
369lemma if_then_True : ∀b,P.P → if b then True else P.
370* // qed-.
371
372include alias "basics/logic.ma".
373
374let rec status_simulation_produce_tlr S1 S2 R
375(* we start from this situation
376     st1 →→→→tlr→→→→ st1'
377      | \
378      L  \---S--\
379      |          \
380   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
381                        by the preceding call)
382   
383   and we produce
384     st1 →→→→tlr→→→→ st1'
385             \\      /  \
386             //     R    \-L,S-\
387             \\     |           \
388   st2_lab →tlr→ st2_mid →taaf→ st2'
389*)
390  st1 st1' st2_lab st2
391  (tlr1 : trace_label_return S1 st1 st1')
392  (taa2_pre : trace_any_any S2 st2_lab st2)
393  (sim_execute : status_simulation S1 S2 R)
394  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
395  ∃st2_mid.∃st2'.
396  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
397  ∃taa2 : trace_any_any_free … st2_mid st2'.
398  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
399  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
400  tlr_rel … tlr1 tlr2 ≝
401 match tlr1 with
402 [ tlr_base st1 st1' tll1 ⇒ ?
403 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
404 ]
405and status_simulation_produce_tll S1 S2 R
406(* we start from this situation
407     st1 →→→→tll→→→ st1'
408      | \
409      L  \---S--\
410      |          \
411   st2_lab →taa→ st2
412   
413   and if the tll is a returning one we produce a diagram like the one for tlr,
414   otherwise a simpler:
415     st1 →→→→tll→→→→ st1'
416             \\       |
417             //      L,S
418             \\       |
419   st2_lab →→→tll→→→ st2'
420*)
421  fl st1 st1' st2_lab st2
422  (tll1 : trace_label_label S1 fl st1 st1')
423  (taa2_pre : trace_any_any S2 st2_lab st2)
424  (sim_execute : status_simulation S1 S2 R)
425   on tll1 : R st1 st2 → label_rel … st1 st2_lab →
426    match fl with
427    [ ends_with_ret ⇒
428      ∃st2_mid.∃st2'.
429      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
430      ∃taa2 : trace_any_any_free … st2_mid st2'.
431      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
432      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
433      tll_rel … tll1 tll2
434    | doesnt_end_with_ret ⇒
435      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
436      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
437    ] ≝
438  match tll1 with
439  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
440  ]
441and status_simulation_produce_tal S1 S2 R
442(* we start from this situation
443     st1 →→tal→→ st1'
444      |
445      S
446      |
447     st2
448   
449   and if the tal is a returning one we produce a diagram like the one for tlr,
450   otherwise we allow for two possibilities:
451   either
452
453     st1 →→tal→→ st1'
454            \\    |
455            //   L,S
456            \\    |
457     st2 →→tal→→ st2'
458
459   or we do not advance from st2:
460
461     st1 →→tal→→ st1'  collapsable, and st1 uncosted
462                /
463         /-L,S-/
464        /
465     st2
466*)
467  fl st1 st1' st2
468  (tal1 : trace_any_label S1 fl st1 st1')
469  (sim_execute : status_simulation S1 S2 R)
470   on tal1 : R st1 st2 →
471    match fl with
472    [ ends_with_ret ⇒
473      ∃st2_mid.∃st2'.
474      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
475      ∃taa2 : trace_any_any_free … st2_mid st2'.
476      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
477      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
478      tal_rel … tal1 tal2
479    | doesnt_end_with_ret ⇒
480      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
481       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
482      (* empty *)
483      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
484    ] ≝
485  match tal1 with
486  [ tal_base_not_return st1' st1'' H G K ⇒ ?
487  | tal_base_return st1' st1'' H G ⇒ ?
488  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
489  | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ?
490  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
491  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
492  ].
493#st1_R_st2
494[1,2,3: #st1_L_st2_lab ]
495[ (* tlr_base *)
496  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
497  #st2_mid * #st2' * #tll2 #H
498  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
499| (* tlr_step *)
500  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
501  #st2_mid * #tll2 ** #H1 #H2 #H3
502  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
503  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
504  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
505  %{H4} %{H3 H5}
506| (* tll_base *)
507  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
508  cases fl1' in tal1; normalize nodelta #tal1 *
509  [3: * #_ #ABS elim (absurd … H ABS) ]
510  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
511  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
512  [1,3: whd <st1_L_st2_lab assumption
513  |*: [%{taa2} ] %{H1} %
514    [1,3: change with (opt_safe ??? = opt_safe ???)
515      @opt_safe_elim #a #EQ1
516      @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
517    |*: @taa_append_tal_rel assumption
518    ]
519  ]
520| (* tal_base_non_return *) whd
521  cases G -G #G
522  lapply (sim_execute … H st1_R_st2)
523  (* without try it fails... why? *)
524  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
525  [ #H lapply (H K) -H ] *
526  #st2' ** -st2 -st2'
527  [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *)
528    ** whd in ⊢ (%→?); *
529    [1,3: #ncost #R' #L' %2 /4 by conj/
530    |*: * #ABS elim (ABS K)
531    ]
532  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ]
533    *** #st1_R_st2' #st1_L_st2' %1
534    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
535    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
536    % /2 by conj/
537    % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
538  ]
539| (* tal_base_return *) whd
540  lapply (sim_execute … H st1_R_st2)
541  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
542  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
543  ***** #ncost #J2 #K2
544  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
545  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
546  % [ /4 by conj/ ]
547  %[ % | %[|%[|%[|%[| % ]]]]]]]
548| (* tal_base_call *) whd
549  lapply (sim_execute … H st1_R_st2)
550  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
551  #H elim (H G) -H
552  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
553  #st1_R_st2_mid #st1_L_st2_after_call
554  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
555  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
556  [ #st2' #tlr2 *****
557  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
558    #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
559  ]
560  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
561  %{st2'}
562  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
563    [3: % [ % assumption ]
564      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
565    ]
566  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
567    [2: %1{J2} |6: %2{J2}
568    |4,8: % try (% assumption)
569      % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
570        % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
571      ]]]]]]]]]]
572    ]
573  ]
574  [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption
575  |*: whd <st1_L_st2' assumption
576  ]
577| (* tal_base_tailcall *) whd
578  lapply (sim_execute … H st1_R_st2)
579  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
580  #H elim (H G) -H
581  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
582  #st1_R_st2_mid #st1_L_st2_after_call
583  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
584  #st2_after_ret * #st2' * #tlr2 * #taa2''
585  * #props #S
586  %{st2_after_ret} %{st2'}
587  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
588  %{taa2''}
589  %{props}
590  % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
591| (* tal_step_call *)
592  lapply (sim_execute … H st1_R_st2)
593  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
594  #H elim (H G) -H
595  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
596  #st1_R_st2_mid #st1_L_st2_after_call
597  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
598  #st2_after_ret * #st2' * #tlr2 * #taa2''
599  ****
600  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
601  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
602  cases fl1' in tl1; #tl1 *
603  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
604    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
605    [4: %{taa2'''} % [ /4 by conj/ ]
606      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
607    ]]]
608  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
609    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
610    [4: % [ /2 by conj/ ]
611      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
612    ]]
613  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
614    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
615    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
616      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
617      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
618      [3: % [ /2 by conj/ ]
619      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
620    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
621      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
622      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
623      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
624      [2: %1{J2'} |6: %2{J2'}
625      |4,8: % [1,3: /2 by conj/]
626        %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
627          %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
628        ]]]]]]]]]]
629      ]]
630    ]
631  ]
632  [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption
633  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
634    [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
635    |*: normalize nodelta //
636    ]
637  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
638  |*: whd <st1_L_st2'' @(trace_any_label_label … tl1)
639  ]
640| (* step_default *)
641  lapply (sim_execute … H st1_R_st2)
642  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
643  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
644  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
645  cases fl1' in tl1; #tl1 *
646  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
647    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
648      [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
649    ]]
650  | *#st2' *#tal2 *#H #G %1
651    %[| %{(taaf_append_tal … taa2 ? tal2)}
652      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
653    ]
654  | (* can't happen *)
655    *** #_ #L' elim (absurd ?? K)
656    whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1)
657  ]
658  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
659]
660qed.
661
662(* finite flat traces, with recursive structure right to left. The list of
663   identifiers represents the call stack *)
664
665inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
666| ft_start : flat_trace S start start [ ]
667| ft_advance_flat :
668  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
669  ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) →
670  flat_trace S start st2 stack
671| ft_advance_call :
672  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
673  ∀prf : as_classifier ? st1 cl_call.
674  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
675| ft_advance_tailcall :
676  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
677  ∀prf : as_classifier ? st1 cl_tailcall.
678  flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack)
679| ft_advance_ret :
680  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
681  as_classifier ? st1 cl_return →
682  flat_trace S start st2 stack.
683
684let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
685  (taa : trace_any_any S st2 st3)
686on taa : flat_trace S st1 st3 stack ≝
687match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
688[ taa_base s ⇒ λacc.acc
689| taa_step st1 st2 st3 H G _ tl ⇒
690  λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
691] ft.
692
693lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
694  ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
695  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
696#S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
697/2/
698qed.
699
700definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
701  λtaaf : trace_any_any_free S st2 st3.
702  match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
703  [ taaf_base s ⇒ λft.ft
704  | taaf_step s1 s2 s3 pre H G ⇒
705    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
706  | taaf_step_jump s1 s2 s3 pre H G K ⇒
707    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K))
708  ] ft.
709
710definition option_to_list : ∀A.option A → list A ≝ λA,x.
711  match x with
712  [ Some x ⇒ [x]
713  | None ⇒ [ ]
714  ].
715
716(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
717let rec ft_observables_aux acc S st st' stack
718  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
719match ft with
720[ ft_start ⇒ acc
721| ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
722  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
723  ft_observables_aux (add @ acc) … pre1
724| ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
725  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
726  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
727  ft_observables_aux (add @ acc) … pre1
728| ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
729  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
730  let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
731  ft_observables_aux (add @ acc) … pre1
732| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
733  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
734  let add ≝ add @ [IEVret f] in
735  ft_observables_aux (add @ acc) … pre1
736].
737
738definition ft_observables ≝ ft_observables_aux [ ].
739
740lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
741  ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
742#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
743[ // ]
744#st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
745whd in ⊢ (??%(??%?));
746>IH >IH >append_nil //
747qed.
748
749lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
750  ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
751    ft_observables … ft @
752    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
753#S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
754[ #st2 #ft >append_nil % ]
755#st2 #st3 #st4 #H #K #G #taa #IH #ft
756normalize in ⊢ (??(?????%)?); >IH
757-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
758[ #st3 #H #G
759| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
760  >(not_costed_no_label … G)
761] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
762qed.
763
764lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
765  ∀ft : flat_trace S st1 st2 stack.
766  ∀taa : trace_any_any S st2 st3.
767  ∀H : as_execute S st3 st4.∀G.
768  ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
769  ft_observables … ft @
770  option_to_list … (!l←as_label … st2;return IEVcost l) @
771  [IEVcall (as_call_ident … «st3, G»)].
772#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
773whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
774>ft_extend_taa_obs
775lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
776[ #st2 * #ft #H #G >append_nil %
777| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
778  >(not_costed_no_label … K)
779  normalize nodelta //
780]
781qed.
782
783lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
784  ∀ft : flat_trace S st1 st2 (f :: stack).
785  ∀taa : trace_any_any S st2 st3.
786  ∀H : as_execute S st3 st4.∀G.
787  ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
788  ft_observables … ft @
789  option_to_list … (!l←as_label … st2;return IEVcost l) @
790  [IEVtailcall f (as_tailcall_ident … «st3, G»)].
791#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
792whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
793>ft_extend_taa_obs
794lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
795[ #st2 * #ft #H #G >append_nil %
796| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
797  >(not_costed_no_label … K)
798  normalize nodelta //
799]
800qed.
801
802lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
803  ∀ft : flat_trace S st1 st2 (f :: stack).
804  ∀taa : trace_any_any S st2 st3.
805  ∀H : as_execute S st3 st4.∀G.
806  ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
807    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
808#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
809whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
810>ft_extend_taa_obs
811lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
812[ #st2 * #ft #H >append_nil %
813| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
814  >(not_costed_no_label … K)
815  normalize nodelta //
816]
817qed.
818
819lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
820  ∀ft : flat_trace S st1 st2 stack.
821  ∀taa : trace_any_any S st2 st3.
822  ∀H : as_execute S st3 st4.∀G.
823  ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
824    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
825#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
826whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
827>ft_extend_taa_obs
828lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
829[ #st2 * #ft #H >append_nil %
830| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
831  >(not_costed_no_label … K)
832  normalize nodelta >append_nil //
833]
834qed.
835
836lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
837  ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
838    ft_observables … ft @
839    if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
840#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
841[ #st2 #ft >append_nil % ]
842#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
843@ft_extend_taa_advance_flat_obs
844qed.
845
846(* little helper to avoid splitting equal cases *)
847lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
848
849theorem status_simulation_produce_ft :
850(* from
851
852  st1 →→→ft→→→ st1'
853   |
854  R,L
855   |
856  st2
857
858  we produce
859 
860  st1 →→→ft→→→ st1'-------\
861         //      \         \
862         \\       L         S
863         //       |          \
864  st2 →→→ft→→→ st2_lab →taa→ st2'
865 
866  so that from any tlr or tll following st1' we can produce the corresponding
867  structured trace from st2_lab using the previous result
868*)
869  ∀S1,S2.
870  ∀R.
871  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
872  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
873  ∃st2_lab,st2'.
874  ∃ft2 : flat_trace S2 st2 st2_lab stack.
875  ∃taa : trace_any_any S2 st2_lab st2'.
876  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
877#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
878[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
879|*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
880  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
881  [1,2: (* other/jump *)
882    lapply (sim_execute … ex G')
883    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
884    [ #H lapply (H ncost_st1') -H ] *
885    #st2' *#taaf ** #ncost #G'' #H''
886    %{st2'} %{st2'}
887    %[1,3:
888      @(ft_extend_taaf … taaf)
889      @(ft_extend_taa … taa)
890      assumption]
891    %{(taa_base …)}
892    % [1,3: %{H'' G''} ]
893    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
894    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
895    [1,4: #st2' #H'' #taa * #ncost
896      >ft_extend_taa_obs <L'
897      [1,3: >(not_costed_no_label … ncost) >if_eq >S %
898      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
899        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
900          >not_costed_no_label
901          [1,3: >append_nil @S ]
902          whd in ⊢ (?%); >L' <H'' assumption
903        |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
904          >S %
905        ]
906      ]
907    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
908      whd in ⊢ (???(?????%));
909      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
910      >S >L' %
911    ]
912  |3: (* tailcall *)
913    lapply (sim_execute … ex G')
914    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
915    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
916    * #taa2 * #taa2' ** #ex' #G'' #H''
917    lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
918    generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
919    <EQcall in ⊢ (%→???%%→%);
920    #ft1' #EQft1'
921    %{st2_after_call} %{st2'}
922    %[@(ft_advance_tailcall … f … ex' cl')
923      @(ft_extend_taa … (taa_append_taa … taa taa2))
924      assumption]
925    %{taa2'}
926    % [ %{H'' G''} ]
927    >ft_extend_taa_advance_tailcall_obs
928    lapply EQft1' lapply ft1' -ft1'
929    >EQcall in ⊢ (%→???%%→%);
930    #ft1' #EQft1' destruct (EQft1')
931    whd in ⊢ (??%?);
932    >ft_observables_aux_def >append_nil
933    >S >L' %
934  |4: (* ret *)
935    lapply (sim_execute … ex G')
936    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
937    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
938    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
939    %[@(ft_extend_taaf … taa2')
940      @(ft_advance_ret … f … ex' cl')
941      @(ft_extend_taa … (taa_append_taa … taa taa2))
942      assumption]
943    %{(taa_base …)}
944    % [ %{H'' G''} ]
945    >ft_extend_taaf_obs
946    >ft_extend_taa_advance_ret_obs
947    whd in ⊢ (??%?);
948    >ft_observables_aux_def >append_nil
949    lapply ncost cases taa2' -st2_after_ret -st2'
950    [ #st2' * >append_nil
951    |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
952      >(not_costed_no_label … ncost)
953      >if_eq >append_nil
954    ]
955    >S >L' %
956  |5: (* call *)
957    lapply (sim_execute … ex G')
958    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
959    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
960    * #taa2 * #taa2' ** #ex' #G'' #H''
961    %{st2_after_call} %{st2'}
962    lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
963    generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
964    <EQcall in ⊢ (%→???%%→%);
965    #ft1' #EQft1'
966    %[@(ft_advance_call … ex' cl')
967      @(ft_extend_taa … (taa_append_taa … taa taa2))
968      assumption]
969    %{taa2'}
970    % [ %{H'' G''} ]
971    >ft_extend_taa_advance_call_obs
972    lapply EQft1' lapply ft1' -ft1'
973    >EQcall in ⊢ (%→???%%→%);
974    #ft1' #EQft1' destruct (EQft1')
975    whd in ⊢ (??%?);
976    >ft_observables_aux_def >append_nil
977    >S >L' %
978  ]
979]
980qed.
Note: See TracBrowser for help on using the repository browser.