source: src/common/StatusSimulation.ma @ 2991

Last change on this file since 2991 was 2991, checked in by piccolo, 7 years ago

Fixed cond and seq case in StatusSimulationHelper?

Added cost case in StatusSimulationHelper?

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