source: src/common/StatusSimulation.ma @ 3367

Last change on this file since 3367 was 3154, checked in by piccolo, 7 years ago

1) changed block_of_call in order to prevent pre-main calls
2) StatusSimulationHelper? in place

File size: 30.0 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/StructuredTraces.ma".
16include "common/FlatTraces.ma".
17
18(* We work with two relations on states in parallel, as well as two derived ones.
19   sem_rel is the classic semantic relation between states, keeping track of
20   memory and how program counters are mapped between languages.
21   call_rel keeps track of what pcs corresponding calls have and just that:
22   this is different than corresponance between program counters in sem_rel when
23   CALL f ↦ instr* CALL f instr* *)
24
25record status_rel
26  (S1 : abstract_status)
27  (S2 : abstract_status)
28  : Type[1] ≝
29  { sem_rel :2> S1 → S2 → Prop
30  (* this is kept separate, as not necessarily carrier will
31     synchronise on calls. It should state the minimal properties
32     necessary for as_after_return (typically just the program counter)
33     maybe what function is called too? *)
34  ; call_rel : (Σs.as_classifier S1 s cl_call) →
35               (Σs.as_classifier S2 s cl_call) → Prop
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 ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
50  λs1_ret,s2_ret.
51  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
52                 call_rel ?? R s1_pre s2_pre →
53                 as_after_return S2 s2_pre s2_ret.
54
55(* the base property we ask for simulation to work depends on the status_class
56   S will mark semantic relation, C call relation, L label relation, R return relation *)
57
58record status_simulation
59  (S1, S2 : abstract_status)
60  (sim_status_rel : status_rel S1 S2) : Prop ≝
61{ one_step_sim :5>
62    ∀st1,st1',st2.as_execute S1 st1 st1' →
63    sim_status_rel st1 st2 →
64      match as_classify … st1 with
65      [ cl_call ⇒ ∀prf.
66        (*
67             st1' ------------S----------\
68              ↑ \                         \
69             st1 \--L--\                   \
70              | \       \                   \
71              S  \-C-\  st2_after_call →taa→ st2'
72              |       \     ↑
73             st2 →taa→ st2_pre_call
74        *)
75        ∃st2_pre_call.
76        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
77        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
78        ∃st2_after_call,st2'.
79        ∃taa2 : trace_any_any … st2 st2_pre_call.
80        ∃taa2' : trace_any_any … st2_after_call st2'.
81        as_execute … st2_pre_call st2_after_call ∧
82        sim_status_rel st1' st2' ∧
83        label_rel … st1' st2_after_call
84      | cl_tailcall ⇒ ∀prf.
85        (*
86             st1' ------------S----------\
87              ↑ \                         \
88             st1 \--L--\                   \
89              |         \                   \
90              S         st2_after_call →taa→ st2'
91              |             ↑
92             st2 →taa→ st2_pre_call
93        *)
94        ∃st2_pre_call.
95        as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧
96        ∃st2_after_call,st2'.
97        ∃taa2 : trace_any_any … st2 st2_pre_call.
98        ∃taa2' : trace_any_any … st2_after_call st2'.
99        as_execute … st2_pre_call st2_after_call ∧
100        sim_status_rel st1' st2' ∧
101        label_rel … st1' st2_after_call
102      | cl_return ⇒
103        (*
104             st1
105            / ↓
106           | st1'----------S,L------------\
107           S   \                           \
108            \   \-----R-------\            |     
109             \                 |           |
110             st2 →taa→ st2_ret |           |
111                          ↓   /            |
112                     st2_after_ret →taaf→ st2'
113
114           we also ask that st2_after_ret be not labelled if the taaf tail is
115           not empty
116        *)
117        ∃st2_ret,st2_after_ret,st2'.
118        ∃taa2 : trace_any_any … st2 st2_ret.
119        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
120        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
121        as_classifier … st2_ret cl_return ∧
122        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
123        ret_rel … sim_status_rel st1' st2_after_ret ∧
124        label_rel … st1' st2'
125      | cl_other ⇒
126          (*         
127          st1 → st1'
128            |      \
129            S      S,L
130            |        \
131           st2 →taaf→ st2'
132           
133           the taaf can be empty (e.g. tunneling) but we ask it must not be the
134           case when both st1 and st1' are labelled (we would be able to collapse
135           labels otherwise)
136         *)
137        ∃st2'.
138        ∃taa2 : trace_any_any_free … st2 st2'.
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      | cl_jump ⇒
143        (* just like cl_other, but with a hypothesis more *)
144        as_costed … st1' →
145        ∃st2'.
146        ∃taa2 : trace_any_any_free … st2 st2'.
147        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
148        sim_status_rel st1' st2' ∧
149        label_rel … st1' st2'
150    ]
151; sim_final :
152  ∀st1,st2.sim_status_rel st1 st2 → as_result S1 st1 = as_result S2 st2
153}.
154
155record status_simulation_with_init (S1,S2 : abstract_status)
156  (R : status_rel S1 S2)
157  (init1 : S1) (init2 : S2) : Prop ≝
158{ sim_init : R init1 init2
159; sim_init_labels : label_rel … init1 init2
160; sim_step_final :> status_simulation S1 S2 R
161}.
162
163(*
164check trace_any_label_label
165let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
166  on tal : as_costed … st2 ≝
167  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
168  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
169  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
170  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
171  | tal_base_return _ _ _ _ ⇒ λprf.⊥
172  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
173  ] (refl …).
174[ destruct
175|*: >prf %
176]
177qed.
178*)
179
180
181(* little helpers *)
182lemma if_else_True : ∀b,P.P → if b then P else True.
183* // qed-.
184lemma if_then_True : ∀b,P.P → if b then True else P.
185* // qed-.
186
187include alias "basics/logic.ma".
188
189let rec status_simulation_produce_tlr S1 S2 R
190(* NB: the axiomatized part about unrepeatingness is imprecise, as further
191  hypotheses are surely needed for the taa prefix. Left for when it is
192  rendered more precise. *)
193(* we start from this situation
194     st1 →→→→tlr→→→→ st1'
195      | \
196      L  \---S--\
197      |          \
198   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
199                        by the preceding call)
200   
201   and we produce
202     st1 →→→→tlr→→→→ st1'
203             \\      /  \
204             //     R    \-L,S-\
205             \\     |           \
206   st2_lab →tlr→ st2_mid →taaf→ st2'
207*)
208  st1 st1' st2_lab st2
209  (tlr1 : trace_label_return S1 st1 st1')
210  (taa2_pre : trace_any_any S2 st2_lab st2)
211  (sim_execute : status_simulation S1 S2 R)
212  on tlr1 : tlr_unrepeating … tlr1 → R st1 st2 → label_rel … st1 st2_lab →
213  ∃st2_mid.∃st2'.
214  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
215  ∃taa2 : trace_any_any_free … st2_mid st2'.
216  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
217  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
218  tlr_rel … tlr1 tlr2 ∧ tlr_unrepeating … tlr2 ≝
219 match tlr1 with
220 [ tlr_base st1 st1' tll1 ⇒ ?
221 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
222 ]
223and status_simulation_produce_tll S1 S2 R
224(* we start from this situation
225     st1 →→→→tll→→→ st1'
226      | \
227      L  \---S--\
228      |          \
229   st2_lab →taa→ st2
230   
231   and if the tll is a returning one we produce a diagram like the one for tlr,
232   otherwise a simpler:
233     st1 →→→→tll→→→→ st1'
234             \\       |
235             //      L,S
236             \\       |
237   st2_lab →→→tll→→→ st2'
238*)
239  fl st1 st1' st2_lab st2
240  (tll1 : trace_label_label S1 fl st1 st1')
241  (taa2_pre : trace_any_any S2 st2_lab st2)
242  (sim_execute : status_simulation S1 S2 R)
243   on tll1 : tll_unrepeating … tll1 → R st1 st2 → label_rel … st1 st2_lab →
244    match fl with
245    [ ends_with_ret ⇒
246      ∃st2_mid.∃st2'.
247      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
248      ∃taa2 : trace_any_any_free … st2_mid st2'.
249      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
250      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
251      tll_rel … tll1 tll2 ∧ tll_unrepeating … tll2
252    | doesnt_end_with_ret ⇒
253      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
254      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2 ∧
255      tll_unrepeating … tll2
256    ] ≝
257  match tll1 with
258  [ tll_base fl1' rst1 rst1' tal1 H ⇒ ?
259  ]
260and status_simulation_produce_tal S1 S2 R
261(* we start from this situation
262     st1 →→tal→→ st1'
263      |
264      S
265      |
266     st2
267   
268   and if the tal is a returning one we produce a diagram like the one for tlr,
269   otherwise we allow for two possibilities:
270   either
271
272     st1 →→tal→→ st1'
273            \\    |
274            //   L,S
275            \\    |
276     st2 →→tal→→ st2'
277
278   or we do not advance from st2:
279
280     st1 →→tal→→ st1'  collapsable, and st1 uncosted
281                /
282         /-L,S-/
283        /
284     st2
285*)
286  fl st1 st1' st2
287  (tal1 : trace_any_label S1 fl st1 st1')
288  (sim_execute : status_simulation S1 S2 R)
289   on tal1 : tal_unrepeating … tal1 → R st1 st2 →
290    match fl with
291    [ ends_with_ret ⇒
292      ∃st2_mid.∃st2'.
293      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
294      ∃taa2 : trace_any_any_free … st2_mid st2'.
295      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
296      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
297      tal_rel … tal1 tal2 ∧ tal_unrepeating … tal2
298    | doesnt_end_with_ret ⇒
299      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
300       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2 ∧
301       tal_unrepeating … tal2) ∨
302      (* empty *)
303      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
304    ] ≝
305  match tal1 with
306  [ tal_base_not_return st1' st1'' H G K ⇒ ?
307  | tal_base_return st1' st1'' H G ⇒ ?
308  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
309  | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ?
310  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
311  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
312  ].
313#unrpt #st1_R_st2
314[1,2,3: #st1_L_st2_lab]
315[ (* tlr_base *)
316  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute unrpt st1_R_st2 st1_L_st2_lab)
317  #st2_mid * #st2' * #tll2 #H
318  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
319| (* tlr_step *)
320  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute (proj1 … unrpt) st1_R_st2 st1_L_st2_lab)
321  #st2_mid * #tll2 *** #H1 #H2 #H3 #H4
322  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute (proj2 … unrpt) H1 H2)
323  #st2_mid' * #st2' * #tl2 * #taa2 ** #H5 #H6 #H7
324  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
325  % [ %{H5} %{H3 H6} | %{H4 H7} ]
326| (* tll_base *)
327  lapply (status_simulation_produce_tal … st2 tal1 sim_execute unrpt st1_R_st2)
328  cases fl1' in tal1; normalize nodelta #tal1 *
329  [3: * #_ #ABS elim (absurd … H ABS) ]
330  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] ** #H1 #H2 #unrpt'
331  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
332  [1,3: whd <st1_L_st2_lab assumption
333  |*: [%{taa2} ] %
334    [1,3: %{H1} %
335      [1,3: change with (opt_safe ??? = opt_safe ???)
336        @opt_safe_elim #a #EQ1
337        @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
338      |*: @taa_append_tal_rel assumption
339      ]
340    |*: whd (* unrepeatingness... *) cases daemon
341    ]
342  ]
343| (* tal_base_non_return *) whd
344  cases G -G #G
345  lapply (sim_execute … H st1_R_st2)
346  (* without try it fails... why? *)
347  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
348  [ #H lapply (H K) -H ] *
349  #st2' ** -st2 -st2'
350  [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *)
351    ** whd in ⊢ (%→?); *
352    [1,3: #ncost #R' #L' %2 /4 by conj/
353    |*: * #ABS elim (ABS K)
354    ]
355  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ]
356    *** #st1_R_st2' #st1_L_st2' %1
357    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))}
358    [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ]
359    %
360    [1,3,5,7:
361      % /2 by conj/
362      % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]]
363    |*: (* unrepeatingness... *) cases daemon
364    ]
365  ]
366| (* tal_base_return *) whd
367  lapply (sim_execute … H st1_R_st2)
368  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
369  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
370  ***** #ncost #J2 #K2
371  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
372  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
373  %
374  [ % [ /4 by conj/ ]
375    %[ % | %[|%[|%[|%[| % ]]]]]
376  |*: (* unrepeatingness... *) cases daemon
377  ]]]
378| (* tal_base_call *) whd
379  lapply (sim_execute … H st1_R_st2)
380  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
381  #H elim (H G) -H
382  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
383  #st1_R_st2_mid #st1_L_st2_after_call
384  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
385  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
386  [ #st2' #tlr2 ******
387  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
388    #I2 #J2 [2: #K2 ] #tlr2 ***** #ncost
389  ]
390  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt' %1
391  %{st2'}
392  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
393    [3: %
394      [ % [ % assumption ]
395        % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
396      |  (* unrepeatingness... *) cases daemon
397      ]
398    ]
399  |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))}
400    [2: %1{J2} |6: %2{J2}
401    |4,8: %
402      [1,3: % try (% assumption)
403        % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
404          % [1,3: %{S} % ] /2 by taa_append_collapsable, I/
405        ]]]]]]]]]]
406      |*: (* unrepeatingness... *) cases daemon
407      ]
408    ]
409  ]
410  [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption
411  |*: whd <st1_L_st2' assumption
412  ]
413| (* tal_base_tailcall *) whd
414  lapply (sim_execute … H st1_R_st2)
415  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
416  #H elim (H G) -H
417  * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
418  #st1_R_st2_mid #st1_L_st2_after_call
419  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute unrpt st1_R_st2_mid st1_L_st2_after_call)
420  #st2_after_ret * #st2' * #tlr2 * #taa2''
421  ** #props #S #unrpt'
422  %{st2_after_ret} %{st2'}
423  %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)}
424  %{taa2''}
425  %
426  [ %{props}
427    % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]]
428  | (* unrepeatingness... *) cases daemon
429  ]
430| (* tal_step_call *)
431  lapply (sim_execute … H st1_R_st2)
432  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?);
433  #H elim (H G) -H
434  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
435  #st1_R_st2_mid #st1_L_st2_after_call
436  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute (proj2 … unrpt) st1_R_st2_mid st1_L_st2_after_call)
437  #st2_after_ret * #st2' * #tlr2 * #taa2''
438  *****
439  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S #unrpt'
440  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … (proj1 … unrpt)) st1_R_st2')
441  cases fl1' in tl1; #tl1 *
442  [ #st2'' * #st2''' * #tl2 * #taa2''' ***** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' #unrpt''
443    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
444    [4: %{taa2'''} %
445      [ % [ /4 by conj/ ]
446        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
447      | (* unrepeatingness... *) cases daemon
448      ]
449    ]]]
450  | *#st2'' *#tl2 *** #st1_R_st2'' #st1_L_st2'' #S' #unrpt'' %1
451    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
452    [4: %
453      [ % [ /2 by conj/ ]
454        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
455      | (* unrepeatingness... *) cases daemon
456      ]
457    ]]
458  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
459    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
460    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
461      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
462      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
463      [3: %
464        [ % [ /2 by conj/ ]
465          %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]
466        | (* unrepeatingness... *) cases daemon
467      ]]]
468    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
469      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
470      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
471      %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))}
472      [2: %1{J2'} |6: %2{J2'}
473      |4,8: %
474        [ % [1,3: /2 by conj/]
475          %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4:
476            %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
477          ]]]]]]]]]]
478        |*: (* unrepeatingness... *) cases daemon
479        ]
480      ]]
481    ]
482  ]
483  [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption
484  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
485    [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
486    |*: normalize nodelta //
487    ]
488  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
489  |*: whd <st1_L_st2'' @(trace_any_label_label … tl1)
490  ]
491| (* step_default *)
492  lapply (sim_execute … H st1_R_st2)
493  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
494  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
495  lapply (status_simulation_produce_tal … tl1 sim_execute (proj2 … unrpt) st1_R_st2_mid)
496  cases fl1' in tl1; #tl1 *
497  [ #st2_mid' *#st2' *#tal2 *#taa2' ** #H #G #unrpt'
498    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
499      [2: %{taa2'} %
500        [ % [/4 by conj/ ] @taaf_append_tal_rel @G
501        |  (* unrepeatingness... *) cases daemon
502        ]
503      ]
504    ]]
505  | *#st2' *#tal2 ** #H #G #unrpt' %1
506    %[| %{(taaf_append_tal … taa2 ? tal2)}
507      [2: %
508        [ % [/2 by conj/] @taaf_append_tal_rel @G
509        | (* unrepeatingness... *) cases daemon
510        ]
511      ]
512    ]
513  | (* can't happen *)
514    *** #_ #L' elim (absurd ?? K)
515    whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1)
516  ]
517  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
518]
519qed.
520
521(* little helper to avoid splitting equal cases *)
522lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
523
524lemma enforce_costedness_ok : ∀S,s1,s2.enforce_costedness S s1 s2 →
525as_classifier S s1 cl_jump → as_costed … s2.
526#S #s1 #s2 whd in ⊢ (%→%→?); whd in match (is_cl_jump ??); #H #G >G in H; #K @K qed.
527
528let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa :
529  trace_any_any_free S st1 st2 ≝
530match taa return λst1,st2,taa.trace_any_any_free S st1 st2 with
531[ taa_base s ⇒ taaf_base … s
532| taa_step s1 s2 s3 ex cl ncost tl ⇒
533  taaf_cons … ex cl (taa_to_taaf … tl) ?
534]. @if_else_True assumption qed.
535
536definition taa_append_taaf : ∀S,st1,st2,st3.
537  trace_any_any S st1 st2 → trace_any_any_free S st2 st3 →
538  trace_any_any_free S st1 st3 ≝
539λS,st1,st2,st3,taa,taaf.
540match taaf return λst2,st3,taaf.trace_any_any S st1 st2 → trace_any_any_free S st1 st3 with
541[ taaf_base s ⇒ taa_to_taaf …
542| taaf_step s1 s2 s3 taa' ex cl ⇒
543  λtaa.taaf_step … (taa_append_taa … taa taa') ex cl
544| taaf_step_jump s1 s2 s3 taa' ex cl K ⇒
545  λtaa.taaf_step_jump … (taa_append_taa … taa taa') ex cl K
546] taa.
547
548lemma taa_to_taaf_non_empty : ∀S,st1,st2,taa.
549taaf_non_empty … (taa_to_taaf S st1 st2 taa) = taa_non_empty … taa.
550#S #st1 #st2 #taa elim taa -st1 -st2
551[ #s % | #s1 #s2 #s3 #ex #cl #ncost #tl #IH
552  change with (taaf_cons ????????) in match (taa_to_taaf ????);
553  >taaf_cons_non_empty %
554qed.
555
556lemma taa_append_taaf_non_empty : ∀S,st1,st2,st3,taa,taaf.
557taaf_non_empty … (taa_append_taaf S st1 st2 st3 taa taaf) =
558(taa_non_empty … taa ∨ taaf_non_empty … taaf).
559#S #st1 #st2 #st3 #taa #taaf lapply taa cases taaf -st2 -st3
560[ #s #taa whd in match (taa_append_taaf ??????); >taa_to_taaf_non_empty
561  >commutative_orb %
562|*: #s1 #s2 #s3 #taa' #ex #cl [2: #K] #taa >commutative_orb %
563]
564qed.
565
566lemma taa_empty_to_eq : ∀S,st1,st2,taa.
567¬(bool_to_Prop (taa_non_empty S st1 st2 taa)) → st1 = st2.
568#S #st1 #st2 * // #s1 #s2 #s3 #ex #cl #K #tl * #ABS cases (ABS ?) % qed.
569
570lemma taaf_empty_to_eq : ∀S,st1,st2,taaf.
571¬(bool_to_Prop (taaf_non_empty S st1 st2 taaf)) → st1 = st2.
572#S #st1 #st2 * // #s1 #s2 #s3 #pre #ex #cl [2: #K ] * #ABS cases (ABS ?) % qed.
573
574theorem status_simulation_produce_ft :
575(* from
576
577  st1 →→→ft→→→ st1'
578   |
579  R,L
580   |
581  st2
582
583  we produce
584 
585  st1 →→→ft→→→ st1'-------\
586         //      \         \
587         \\       L         S
588         //       |          \
589  st2 →→→ft→→→ st2_lab →taa→ st2'
590 
591  so that from any tlr or tll following st1' we can produce the corresponding
592  structured trace from st2_lab using the previous result
593*)
594  ∀S1,S2.
595  ∀R.
596  ∀st1,st1',st2.∀ft1 : flat_trace S1 st1 st1'.
597  status_simulation S1 S2 R → R st1 st2 → label_rel … st1 st2 →
598  ∃st2_lab,st2'.
599  ∃ft2 : flat_trace S2 st2 st2_lab.
600  ∃taa : trace_any_any S2 st2_lab st2'.
601  R st1' st2' ∧ label_rel … st1' st2_lab ∧ ft_stack_observables … ft1 = ft_stack_observables … ft2.
602#S1 #S2 #R #st1 #st1' #st2 #ft1 #sim_execute #H #G elim ft1 -st1'
603[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % ]
604#st1_mid #st1' #ft1 #ex #ncost_st1'
605(* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #G' #L' #S
606inversion (as_classify … st1_mid) #cl
607[2,5: (* other/jump *)
608  lapply (sim_execute … ex G')
609  try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta
610  [ #H lapply (H (enforce_costedness_ok ??? ncost_st1' (jmeq_to_eq … cl))) -H ] *
611  #st2' *#taaf ** #ncost #H'' #G''
612  %{st2'} %{st2'}
613  %[1,3:
614    @(ft_extend_taaf … (taa_append_taaf … taa taaf))
615    assumption]
616  %{(taa_base …)}
617  % [1,3: %{H'' G''} ]
618  >ft_extend_taaf_obs >taa_append_taaf_non_empty
619  whd in match ft_observables; whd in match ft_stack; normalize nodelta
620  <S whd in ⊢ (??%?); @pair_elim' normalize nodelta
621  >(status_class_dep_match_rewrite … cl) normalize nodelta @eq_f @eq_f
622  cases (true_or_false_Prop taa) #Htaa >Htaa
623  [2,4: lapply (taa_empty_to_eq … Htaa) #EQ destruct
624    cases (true_or_false_Prop (taaf_non_empty … taaf)) #Htaaf
625    >Htaaf in ncost ⊢ %;
626    [1,3: #_ |*: * #ncost lapply (taaf_empty_to_eq … Htaaf) #EQ destruct ]
627  ]
628  normalize nodelta in ncost ⊢ %; // >not_costed_no_label //
629  whd in ⊢ (?%); >L' <G'' assumption
630|4: (* tailcall *)
631  lapply (sim_execute … ex G')
632  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
633  * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2'
634  * #taa2 * #taa2' ** #ex' #H'' #G''
635  %{st2_after_call} %{st2'}
636  %[@(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
637    @(ft_extend_taa … (taa_append_taa … taa taa2))
638    assumption]
639  %{taa2'}
640  % [ %{H'' G''} ]
641  >ft_extend_taa_advance_obs
642  whd in ⊢ (??%?); @pair_elim' @pair_elim'
643  >(status_class_dep_match_rewrite … cl)
644  >(status_class_dep_match_rewrite … cl') normalize nodelta
645  >S <EQcall >L' %
646|1: (* ret *)
647  lapply (sim_execute … ex G')
648  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); *
649  #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
650  ***** #ncost #cl' #ex' #H'' #_ #G'' %{st2'} %{st2'}
651  %[@(ft_extend_taaf … taa2')
652    @(ft_advance … ex' ?) [2: @hide_prf normalize >cl' % ]
653    @(ft_extend_taa … (taa_append_taa … taa taa2))
654    assumption]
655  %{(taa_base …)}
656  % [ %{H'' G''} ]
657  >ft_extend_taaf_obs whd in match ft_observables; whd in match ft_stack; normalize nodelta
658  >ft_extend_taa_advance_obs
659  whd in ⊢ (??%?); @pair_elim' @pair_elim' normalize nodelta
660  >(status_class_dep_match_rewrite … cl)
661  >(status_class_dep_match_rewrite … cl') normalize nodelta
662  >S cases (\fst (ft_stack_observables … ft2)) [2: #f #stack']
663  normalize nodelta @eq_f >L' >associative_append @eq_f
664  cases (true_or_false_Prop (taaf_non_empty … taa2')) #H
665  >H in ncost ⊢ %; normalize nodelta [1,3: #ncost |*: lapply (taaf_empty_to_eq … H) #EQ destruct #_ ]
666  // >(not_costed_no_label … st2_after_ret) // >append_nil %
667|3: (* call *)
668  lapply (sim_execute … ex G')
669  >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H
670  * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
671  * #taa2 * #taa2' ** #ex' #H'' #G''
672  %{st2_after_call} %{st2'}
673  %[@(ft_advance … ex' ?) [2: @hide_prf  normalize >cl' % ]
674    @(ft_extend_taa … (taa_append_taa … taa taa2))
675    assumption]
676  %{taa2'}
677  % [ %{H'' G''} ]
678  >ft_extend_taa_advance_obs @pair_elim' >(status_class_dep_match_rewrite … cl') normalize nodelta
679  whd in ⊢ (??%?); @pair_elim' >(status_class_dep_match_rewrite … cl) normalize nodelta
680  >S <EQcall >L' %
681]
682qed.
683
684definition call_stack_from_obs : list intensional_event → list ident ≝
685let f ≝ λacc,ev.match ev with
686  [ IEVcall id ⇒ id :: acc
687  | IEVret _ ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ tl ]
688  | IEVtailcall _ id ⇒ match acc with [ nil ⇒ [ ] | cons _ tl ⇒ id :: tl ]
689  | _ ⇒ acc
690  ] in
691foldl ?? f [ ].
692
693lemma ft_stack_from_observables :
694∀S1,st1,st1'.∀ft : flat_trace S1 st1 st1'.
695  ft_stack … ft = call_stack_from_obs … (ft_observables … ft).
696#S1 #st1 #st1' #ft elim ft -st1'
697[ % ] #st1' #st1'' #pre #ex #ncost #IH whd in match ft_stack; whd in match ft_observables; normalize nodelta
698whd in match (ft_stack_observables ????); @pair_elim' normalize nodelta
699@status_class_dep_match_elim #cl [2,3: inversion (\fst (ft_stack_observables ????))
700  [2,4: #f #stak' #_ ] #EQ_stack normalize nodelta ] whd in match call_stack_from_obs; normalize nodelta
701[1,2,5: <associative_append >foldl_append whd in ⊢ (???%); ]
702>foldl_append cases (as_label ??) [2,4,6,8,10,12,14: #lbl]
703whd in match option_to_list; normalize nodelta
704whd in match (foldl ?????);
705change with (call_stack_from_obs ?) in match (foldl ?????);
706whd in match ft_stack in IH; whd in match ft_observables; normalize nodelta in IH; <IH
707try >EQ_stack %
708qed.
709 
710lemma ft_stack_observables_eq : ∀S1,S2,st1,st1',st2,st2'.
711∀ft1 : flat_trace S1 st1 st1'.∀ft2 : flat_trace S2 st2 st2'.
712ft_observables … ft1 = ft_observables … ft2 →
713ft_stack_observables … ft1 = ft_stack_observables … ft2.
714#S1 #S2 #st1 #st1' #st2 #st2' #ft1 #ft2 #EQ
715>(eq_pair_fst_snd … (ft_stack_observables … ft1))
716>(eq_pair_fst_snd … (ft_stack_observables … ft2))
717change with (〈ft_stack … ft1, ft_observables … ft1〉 = 〈ft_stack … ft2, ft_observables … ft2〉)
718>ft_stack_from_observables >ft_stack_from_observables >EQ %
719qed.
720
721record ft_and_tlr (S : abstract_status) (prefix, subtrace : list intensional_event)
722(fn : ident) (st1 : S) : Prop ≝
723{ st2 : S
724; st3 : S
725; ft : flat_trace S st1 st2
726; tlr : trace_label_return S st2 st3
727; tlr_unrpt : tlr_unrepeating … tlr
728; ft_is_prefix : ft_observables … ft = prefix
729; fn_is_current : ft_current_function … ft = Some ? fn
730; tlr_is_subtrace : observables_trace_label_return … tlr fn = subtrace
731}.
732
733theorem status_simulation_produce_ft_and_tlr :
734∀S1,S2.
735∀R.
736∀prefix,subtrace,fn.
737∀st1,st2.
738status_simulation_with_init S1 S2 R st1 st2 →
739ft_and_tlr S1 prefix subtrace fn st1 →
740ft_and_tlr S2 prefix subtrace fn st2.
741#S1 #S2 #R #pref #subtr #fn #st1 #st2
742* #S #L #simul *
743#st1' #st1'' #ft1 #tlr1 #unrpt #EQ1 #EQ2 #EQ3
744cases (status_simulation_produce_ft … ft1 simul S L)
745#st2' * #st2_mid * #ft2 * #taa2 ** #S' #L' #EQ4
746cases (status_simulation_produce_tlr … tlr1 taa2 simul unrpt S' L')
747#st2'' * #st2''' * #tlr2 * #taa2' ***** #_ #S'' #_ #_ #EQ5 #unrpt'
748%{st2' st2'' ft2 tlr2 unrpt' ???}
749[ whd in ⊢ (??%?); <EQ4 assumption
750| whd in ⊢ (??%?); whd in match ft_stack; normalize nodelta <EQ4 assumption
751| <(tlr_rel_to_traces_same_observables … EQ5) assumption
752]
753qed.
Note: See TracBrowser for help on using the repository browser.