source: src/common/StatusSimulation.ma @ 2476

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

swapped back call_rel and ret_rel...

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