source: src/common/StatusSimulation.ma @ 3096

Last change on this file since 3096 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

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