source: src/common/StatusSimulation.ma @ 2457

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

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

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