source: src/common/StructuredTraces.ma @ 1918

Last change on this file since 1918 was 1918, checked in by tranquil, 8 years ago

using listb.ma now

File size: 14.7 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4include "basics/lists/listb.ma".
5include "ASM/Util.ma".
6
7inductive status_class : Type[0] ≝
8| cl_return : status_class
9| cl_jump   : status_class
10| cl_call   : status_class
11| cl_other : status_class.
12
13record abstract_status : Type[1] ≝
14  { as_status :> Type[0]
15  ; as_execute : as_status → as_status → Prop
16  ; as_pc : DeqSet
17  ; as_pc_of : as_status → as_pc
18  ; as_classifier : as_status → status_class → Prop
19  ; as_costed : as_status → Prop
20  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
21  ; as_final: as_status → Prop
22}.
23
24(* temporary alias for backward compatibility *)
25definition final_abstract_status ≝ abstract_status.
26
27inductive trace_ends_with_ret: Type[0] ≝
28  | ends_with_ret: trace_ends_with_ret
29  | doesnt_end_with_ret: trace_ends_with_ret.
30
31inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
32  | tlr_base:
33      ∀status_before: S.
34      ∀status_after: S.
35        trace_label_label S ends_with_ret status_before status_after →
36        trace_label_return S status_before status_after
37  | tlr_step:
38      ∀status_initial: S.
39      ∀status_labelled: S.
40      ∀status_final: S.
41        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
42        trace_label_return S status_labelled status_final →
43          trace_label_return S status_initial status_final
44with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
45  | tll_base:
46      ∀ends_flag: trace_ends_with_ret.
47      ∀start_status: S.
48      ∀end_status: S.
49        trace_any_label S ends_flag start_status end_status →
50        as_costed S start_status →
51          trace_label_label S ends_flag start_status end_status
52with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
53  (* Single steps within a function which reach a label.
54     Note that this is the only case applicable for a jump. *)
55  | tal_base_not_return:
56      ∀start_status: S.
57      ∀final_status: S.
58        as_execute S start_status final_status →
59        (as_classifier S start_status cl_jump ∨
60         as_classifier S start_status cl_other) →
61        as_costed S final_status →
62          trace_any_label S doesnt_end_with_ret start_status final_status
63  | tal_base_return:
64      ∀start_status: S.
65      ∀final_status: S.
66        as_execute S start_status final_status →
67        as_classifier S start_status cl_return →
68          trace_any_label S ends_with_ret start_status final_status
69  (* A call followed by a label on return. *)
70  | tal_base_call:
71      ∀status_pre_fun_call: S.
72      ∀status_start_fun_call: S.
73      ∀status_final: S.
74        as_execute S status_pre_fun_call status_start_fun_call →
75        ∀H:as_classifier S status_pre_fun_call cl_call.
76          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
77          trace_label_return S status_start_fun_call status_final →
78          as_costed S status_final →
79            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
80  (* A call followed by a non-empty trace. *)
81  | tal_step_call:
82      ∀end_flag: trace_ends_with_ret.
83      ∀status_pre_fun_call: S.
84      ∀status_start_fun_call: S.
85      ∀status_after_fun_call: S.
86      ∀status_final: S.
87        as_execute S status_pre_fun_call status_start_fun_call →
88        ∀H:as_classifier S status_pre_fun_call cl_call.
89          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
90          trace_label_return S status_start_fun_call status_after_fun_call →
91          ¬ as_costed S status_after_fun_call →
92          trace_any_label S end_flag status_after_fun_call status_final →
93            trace_any_label S end_flag status_pre_fun_call status_final
94  | tal_step_default:
95      ∀end_flag: trace_ends_with_ret.
96      ∀status_pre: S.
97      ∀status_init: S.
98      ∀status_end: S.
99        as_execute S status_pre status_init →
100        trace_any_label S end_flag status_init status_end →
101        as_classifier S status_pre cl_other →
102        ¬ (as_costed S status_init) →
103          trace_any_label S end_flag status_pre status_end.
104
105let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
106  on tal : list (as_pc S) ≝
107 match tal with
108 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
109 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
110 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
111 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
112 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
113 ].
114
115let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
116  match tlr with
117  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
118  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
119  ]
120and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
121  match tll with
122  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
123  ]
124and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
125  match tal with
126  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
127    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
128    tal_unrepeating … tl ∧
129    tlr_unrepeating … tlr
130  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
131    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
132    tal_unrepeating … tl
133  | _ ⇒ True
134  ].
135
136let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
137  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
138cases tal //
139#fl' #st1' [#st_fun] #st2' #st3' #H
140[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
141#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
142qed.
143
144inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
145  | tac_base:
146      ∀status: S.
147        as_classifier S status cl_call →
148          trace_any_call S status status
149  | tac_step_call:
150      ∀status_pre_fun_call: S.
151      ∀status_after_fun_call: S.
152      ∀status_final: S.
153      ∀status_start_fun_call: S.
154        as_execute S status_pre_fun_call status_start_fun_call →
155        ∀H:as_classifier S status_pre_fun_call cl_call.
156          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
157          trace_label_return S status_start_fun_call status_after_fun_call →
158          ¬ as_costed S status_after_fun_call →
159          trace_any_call S status_after_fun_call status_final →
160            trace_any_call S status_pre_fun_call status_final
161  | tac_step_default:
162      ∀status_pre: S.
163      ∀status_end: S.
164      ∀status_init: S.
165        as_execute S status_pre status_init →
166        trace_any_call S status_init status_end →
167        as_classifier S status_pre cl_other →
168        ¬ (as_costed S status_init) →
169          trace_any_call S status_pre status_end.
170
171             
172inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
173  | tlc_base:
174      ∀start_status: S.
175      ∀end_status: S.
176        trace_any_call S start_status end_status →
177        as_costed S start_status →
178        trace_label_call S start_status end_status
179.
180
181coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
182  | tld_step:
183      ∀status_initial: S.
184      ∀status_labelled: S.
185          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
186          trace_label_diverges S status_labelled →
187            trace_label_diverges S status_initial
188  | tld_base:
189      ∀status_initial: S.
190      ∀status_pre_fun_call: S.
191      ∀status_start_fun_call: S.
192        trace_label_call S status_initial status_pre_fun_call →
193        as_execute S status_pre_fun_call status_start_fun_call →
194        ∀H:as_classifier S status_pre_fun_call cl_call.
195          trace_label_diverges S status_start_fun_call →
196            trace_label_diverges S status_initial.
197
198(* Version in Prop for showing existence. *)
199coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
200  | tld_step:
201      ∀status_initial: S.
202      ∀status_labelled: S.
203          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
204          trace_label_diverges_exists S status_labelled →
205            trace_label_diverges_exists S status_initial
206  | tld_base:
207      ∀status_initial: S.
208      ∀status_pre_fun_call: S.
209      ∀status_start_fun_call: S.
210        trace_label_call S status_initial status_pre_fun_call →
211        as_execute S status_pre_fun_call status_start_fun_call →
212        ∀H:as_classifier S status_pre_fun_call cl_call.
213          trace_label_diverges_exists S status_start_fun_call →
214            trace_label_diverges_exists S status_initial.
215
216inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
217  | twp_terminating:
218      ∀status_initial: S.
219      ∀status_start_fun: S.
220      ∀status_final: S.
221        as_classifier S status_initial cl_call →
222        as_execute S status_initial status_start_fun →
223        trace_label_return S status_start_fun status_final →
224        as_final S status_final →
225        trace_whole_program S status_initial
226  | twp_diverges:
227      ∀status_initial: S.
228      ∀status_start_fun: S.
229        as_classifier S status_initial cl_call →
230        as_execute S status_initial status_start_fun →
231        trace_label_diverges S status_start_fun →
232        trace_whole_program S status_initial.
233
234(* Again, an identical version in Prop for existence proofs. *)
235inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
236  | twp_terminating:
237      ∀status_initial: S.
238      ∀status_start_fun: S.
239      ∀status_final: S.
240        as_classifier S status_initial cl_call →
241        as_execute S status_initial status_start_fun →
242        trace_label_return S status_start_fun status_final →
243        as_final S status_final →
244        trace_whole_program_exists S status_initial
245  | twp_diverges:
246      ∀status_initial: S.
247      ∀status_start_fun: S.
248        as_classifier S status_initial cl_call →
249        as_execute S status_initial status_start_fun →
250        trace_label_diverges_exists S status_start_fun →
251        trace_whole_program_exists S status_initial.
252
253
254let rec trace_any_label_label S s s' f
255  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
256match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
257[ tal_base_not_return start final _ _ C ⇒ C
258| tal_base_return _ _  _ _ ⇒ I
259| tal_base_call _ _ _ _ _ _ _ C ⇒ C
260| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
261| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
262].
263
264lemma trace_label_label_label : ∀S,s,s',f.
265  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
266#S #s #s' #f #tr
267cases tr
268#f #start #end #tr' #C @(trace_any_label_label … tr')
269qed.
270
271lemma trace_any_call_call : ∀S,s,s'.
272  trace_any_call S s s' → as_classifier S s' cl_call.
273#S #s #s' #T elim T //
274qed.
275
276(* an uncalling, unreturning and *unjumping*,
277  as well as unlabelled (but possibly for the first and last statuses)
278  possibly empty trace segment *)
279inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
280  | taa_base :
281      ∀start_status: S.
282        trace_any_any S start_status start_status
283  | taa_step :
284      ∀status_pre: S.
285      ∀status_init: S.
286      ∀status_end: S.
287        as_execute S status_pre status_init →
288        trace_any_any S status_init status_end →
289        as_classifier S status_pre cl_other →
290        ¬as_costed … status_init →
291          trace_any_any S status_pre status_end.
292
293let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
294  match taa with
295  [ taa_base st1' ⇒ [st1']
296  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
297  ].
298
299let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
300  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
301  match taa1
302  return λst1,st2.λx : trace_any_any S st1 st2.
303    trace_any_any S st2 st3 → trace_any_any S st1 st3
304  with
305  [ taa_base _ ⇒ λtaa2.taa2
306  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
307      taa_step … H (taa_append_taa … tl taa2) G K
308  ].
309
310let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
311  on taa :
312  trace_any_label S fl st2 st3 →
313  trace_any_label S fl st1 st3 ≝
314  match taa
315  return λst1,st2.λx : trace_any_any S st1 st2.
316    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
317  with
318  [ taa_base _ ⇒ λtaa2.taa2
319  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
320      tal_step_default … H (taa_append_tal … tl taa2) G K
321  ].
322
323(* TODO: use as_label for forcing same labels *)
324let rec tlr_rel S1 st1 st1' S2 st2 st2'
325  (tlr1 : trace_label_return S1 st1 st1')
326  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
327match tlr1 with
328  [ tlr_base st1 st1' tll1 ⇒
329    match tlr2 with
330    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
331    | _ ⇒ False
332    ]
333  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
334    match tlr2 with
335    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
336      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
337    | _ ⇒ False
338    ]
339  ]
340and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
341 (tll1 : trace_label_label S1 fl1 st1 st1')
342 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
343  match tll1 with
344  [ tll_base fl1 st1 st1' tal1 _ ⇒
345    match tll2 with
346    [ tll_base fl2 st2 st2 tal2 _ ⇒ tal_rel … tal1 tal2
347    ]
348  ]
349and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
350 (tal1 : trace_any_label S1 fl1 st1 st1')
351 (tal2 : trace_any_label S2 fl2 st2 st2')
352   on tal1 : Prop ≝
353  match tal1 with
354  [ tal_base_not_return st1 st1' _ _ _ ⇒
355    ∃st2mid,taa,H,G,K.
356    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
357      (tal_base_not_return ? st2mid st2' H G K)
358  | tal_base_return st1 st1' _ _ ⇒
359    ∃st2mid,taa,H,G.
360    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
361      (tal_base_return ? st2mid st2' H G)
362  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
363    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
364    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
365      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
366      tlr_rel … tlr1 tlr2
367  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
368    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
369    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
370      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
371      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
372  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
373    tal_rel … tl1 tal2 (* <- this makes it many to many *)
374  ].
Note: See TracBrowser for help on using the repository browser.