source: src/common/StatusSimulation.ma @ 2624

Last change on this file since 2624 was 2553, checked in by tranquil, 8 years ago

as_classify changed to a partial function
added a status for tailcalls

File size: 38.0 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) *)
709
710inductive intensional_event : Type[0] ≝
711| IEVcost : costlabel → intensional_event
712| IEVcall : ident → intensional_event
713| IEVtailcall : ident → ident → intensional_event
714| IEVret : ident → intensional_event.
715
716let rec ft_observables_aux acc S st st' stack
717  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
718match ft with
719[ ft_start ⇒ acc
720| ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
721  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
722  ft_observables_aux (add @ acc) … pre1
723| ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
724  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
725  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
726  ft_observables_aux (add @ acc) … pre1
727| ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒
728  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
729  let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in
730  ft_observables_aux (add @ acc) … pre1
731| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
732  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
733  let add ≝ add @ [IEVret f] in
734  ft_observables_aux (add @ acc) … pre1
735].
736
737definition ft_observables ≝ ft_observables_aux [ ].
738
739lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
740  ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
741#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
742[ // ]
743#st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc
744whd in ⊢ (??%(??%?));
745>IH >IH >append_nil //
746qed.
747
748lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
749  ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
750    ft_observables … ft @
751    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
752#S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
753[ #st2 #ft >append_nil % ]
754#st2 #st3 #st4 #H #K #G #taa #IH #ft
755normalize in ⊢ (??(?????%)?); >IH
756-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
757[ #st3 #H #G
758| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
759  >(not_costed_no_label … G)
760] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
761qed.
762
763lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
764  ∀ft : flat_trace S st1 st2 stack.
765  ∀taa : trace_any_any S st2 st3.
766  ∀H : as_execute S st3 st4.∀G.
767  ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
768  ft_observables … ft @
769  option_to_list … (!l←as_label … st2;return IEVcost l) @
770  [IEVcall (as_call_ident … «st3, G»)].
771#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
772whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
773>ft_extend_taa_obs
774lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
775[ #st2 * #ft #H #G >append_nil %
776| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
777  >(not_costed_no_label … K)
778  normalize nodelta //
779]
780qed.
781
782lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4.
783  ∀ft : flat_trace S st1 st2 (f :: stack).
784  ∀taa : trace_any_any S st2 st3.
785  ∀H : as_execute S st3 st4.∀G.
786  ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) =
787  ft_observables … ft @
788  option_to_list … (!l←as_label … st2;return IEVcost l) @
789  [IEVtailcall f (as_tailcall_ident … «st3, G»)].
790#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
791whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
792>ft_extend_taa_obs
793lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
794[ #st2 * #ft #H #G >append_nil %
795| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
796  >(not_costed_no_label … K)
797  normalize nodelta //
798]
799qed.
800
801lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
802  ∀ft : flat_trace S st1 st2 (f :: stack).
803  ∀taa : trace_any_any S st2 st3.
804  ∀H : as_execute S st3 st4.∀G.
805  ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
806    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
807#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
808whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
809>ft_extend_taa_obs
810lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
811[ #st2 * #ft #H >append_nil %
812| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
813  >(not_costed_no_label … K)
814  normalize nodelta //
815]
816qed.
817
818lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
819  ∀ft : flat_trace S st1 st2 stack.
820  ∀taa : trace_any_any S st2 st3.
821  ∀H : as_execute S st3 st4.∀G.
822  ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
823    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
824#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
825whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
826>ft_extend_taa_obs
827lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
828[ #st2 * #ft #H >append_nil %
829| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
830  >(not_costed_no_label … K)
831  normalize nodelta >append_nil //
832]
833qed.
834
835lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
836  ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
837    ft_observables … ft @
838    if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
839#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
840[ #st2 #ft >append_nil % ]
841#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
842@ft_extend_taa_advance_flat_obs
843qed.
844
845(* little helper to avoid splitting equal cases *)
846lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
847
848theorem status_simulation_produce_ft :
849(* from
850
851  st1 →→→ft→→→ st1'
852   |
853  R,L
854   |
855  st2
856
857  we produce
858 
859  st1 →→→ft→→→ st1'-------\
860         //      \         \
861         \\       L         S
862         //       |          \
863  st2 →→→ft→→→ st2_lab →taa→ st2'
864 
865  so that from any tlr or tll following st1' we can produce the corresponding
866  structured trace from st2_lab using the previous result
867*)
868  ∀S1,S2.
869  ∀R.
870  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
871  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
872  ∃st2_lab,st2'.
873  ∃ft2 : flat_trace S2 st2 st2_lab stack.
874  ∃taa : trace_any_any S2 st2_lab st2'.
875  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
876#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
877[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
878|*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1']
879  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
880  [1,2: (* other/jump *)
881    lapply (sim_execute … ex G')
882    try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); normalize nodelta
883    [ #H lapply (H ncost_st1') -H ] *
884    #st2' *#taaf ** #ncost #G'' #H''
885    %{st2'} %{st2'}
886    %[1,3:
887      @(ft_extend_taaf … taaf)
888      @(ft_extend_taa … taa)
889      assumption]
890    %{(taa_base …)}
891    % [1,3: %{H'' G''} ]
892    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
893    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
894    [1,4: #st2' #H'' #taa * #ncost
895      >ft_extend_taa_obs <L'
896      [1,3: >(not_costed_no_label … ncost) >if_eq >S %
897      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
898        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
899          >not_costed_no_label
900          [1,3: >append_nil @S ]
901          whd in ⊢ (?%); >L' <H'' assumption
902        |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
903          >S %
904        ]
905      ]
906    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
907      whd in ⊢ (???(?????%));
908      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
909      >S >L' %
910    ]
911  |3: (* tailcall *)
912    lapply (sim_execute … ex G')
913    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
914    * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
915    * #taa2 * #taa2' ** #ex' #G'' #H''
916    lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl))
917    generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%);
918    <EQcall in ⊢ (%→???%%→%);
919    #ft1' #EQft1'
920    %{st2_after_call} %{st2'}
921    %[@(ft_advance_tailcall … f … ex' cl')
922      @(ft_extend_taa … (taa_append_taa … taa taa2))
923      assumption]
924    %{taa2'}
925    % [ %{H'' G''} ]
926    >ft_extend_taa_advance_tailcall_obs
927    lapply EQft1' lapply ft1' -ft1'
928    >EQcall in ⊢ (%→???%%→%);
929    #ft1' #EQft1' destruct (EQft1')
930    whd in ⊢ (??%?);
931    >ft_observables_aux_def >append_nil
932    >S >L' %
933  |4: (* ret *)
934    lapply (sim_execute … ex G')
935    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); *
936    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
937    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
938    %[@(ft_extend_taaf … taa2')
939      @(ft_advance_ret … f … ex' cl')
940      @(ft_extend_taa … (taa_append_taa … taa taa2))
941      assumption]
942    %{(taa_base …)}
943    % [ %{H'' G''} ]
944    >ft_extend_taaf_obs
945    >ft_extend_taa_advance_ret_obs
946    whd in ⊢ (??%?);
947    >ft_observables_aux_def >append_nil
948    lapply ncost cases taa2' -st2_after_ret -st2'
949    [ #st2' * >append_nil
950    |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
951      >(not_costed_no_label … ncost)
952      >if_eq >append_nil
953    ]
954    >S >L' %
955  |5: (* call *)
956    lapply (sim_execute … ex G')
957    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
958    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
959    * #taa2 * #taa2' ** #ex' #G'' #H''
960    %{st2_after_call} %{st2'}
961    lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
962    generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
963    <EQcall in ⊢ (%→???%%→%);
964    #ft1' #EQft1'
965    %[@(ft_advance_call … ex' cl')
966      @(ft_extend_taa … (taa_append_taa … taa taa2))
967      assumption]
968    %{taa2'}
969    % [ %{H'' G''} ]
970    >ft_extend_taa_advance_call_obs
971    lapply EQft1' lapply ft1' -ft1'
972    >EQcall in ⊢ (%→???%%→%);
973    #ft1' #EQft1' destruct (EQft1')
974    whd in ⊢ (??%?);
975    >ft_observables_aux_def >append_nil
976    >S >L' %
977  ]
978]
979qed.
Note: See TracBrowser for help on using the repository browser.