source: src/common/StructuredTraces.ma @ 1921

Last change on this file since 1921 was 1921, checked in by mulligan, 8 years ago

Horror proof mostly finished (compiles all way until end of CostsProof?.ma).

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