source: src/common/StatusSimulation.ma @ 2755

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