source: src/common/StatusSimulation.ma @ 2769

Last change on this file since 2769 was 2756, checked in by sacerdot, 7 years ago

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

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