source: src/common/StatusSimulation.ma @ 2540

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

cl_jump case now provides a proof of costedness of the following state

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