source: src/common/StatusSimulation.ma @ 2428

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

added simulation of flat prefix, and comments to explain the code

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