source: src/common/StructuredTraces.ma @ 1935

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

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

File size: 20.0 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4include "common/CostLabel.ma".
5include "utilities/option.ma".
6include "ASM/Util.ma".
7include "ASM/Interpret.ma".
8
9record abstract_status : Type[1] ≝
10{
11    as_status :> Type[0]
12  ; as_execute : as_status → as_status → Prop
13  ; as_pc : DeqSet
14  ; as_pc_of : as_status → as_pc
15  ; as_classifier : as_status → status_class → Prop
16  ; as_label : as_status → option costlabel
17  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
18  ; as_final: as_status → Prop
19}.
20
21definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
22  λcode_memory.
23  λcost_labels.
24    mk_abstract_status
25      (Status code_memory)
26      (λs,s'. (execute_1 … s) = s')
27      word_deqset
28      (program_counter …)
29      (λs,class. ASM_classify … s = class)
30      (current_instruction_label code_memory cost_labels)
31      (next_instruction_properly_relates_program_counters code_memory)
32      ?.
33  cases daemon (* XXX: is final predicate *)
34qed.
35
36(* temporary alias for backward compatibility *)
37definition final_abstract_status ≝ abstract_status.
38
39definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
40  λa_s,st.as_label ? st ≠ None ?.
41
42definition as_label_safe : ∀a_s : abstract_status.
43  (Σs : a_s.as_costed ? s) → costlabel ≝
44  λa_s,st_sig.opt_safe … (pi2 … st_sig).
45
46inductive trace_ends_with_ret: Type[0] ≝
47  | ends_with_ret: trace_ends_with_ret
48  | doesnt_end_with_ret: trace_ends_with_ret.
49
50inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
51  | tlr_base:
52      ∀status_before: S.
53      ∀status_after: S.
54        trace_label_label S ends_with_ret status_before status_after →
55        trace_label_return S status_before status_after
56  | tlr_step:
57      ∀status_initial: S.
58      ∀status_labelled: S.
59      ∀status_final: S.
60        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
61        trace_label_return S status_labelled status_final →
62          trace_label_return S status_initial status_final
63with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
64  | tll_base:
65      ∀ends_flag: trace_ends_with_ret.
66      ∀start_status: S.
67      ∀end_status: S.
68        trace_any_label S ends_flag start_status end_status →
69        as_costed S start_status →
70          trace_label_label S ends_flag start_status end_status
71with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
72  (* Single steps within a function which reach a label.
73     Note that this is the only case applicable for a jump. *)
74  | tal_base_not_return:
75      ∀start_status: S.
76      ∀final_status: S.
77        as_execute S start_status final_status →
78        (as_classifier S start_status cl_jump ∨
79         as_classifier S start_status cl_other) →
80        as_costed S final_status →
81          trace_any_label S doesnt_end_with_ret start_status final_status
82  | tal_base_return:
83      ∀start_status: S.
84      ∀final_status: S.
85        as_execute S start_status final_status →
86        as_classifier S start_status cl_return →
87          trace_any_label S ends_with_ret start_status final_status
88  (* A call followed by a label on return. *)
89  | tal_base_call:
90      ∀status_pre_fun_call: S.
91      ∀status_start_fun_call: S.
92      ∀status_final: S.
93        as_execute S status_pre_fun_call status_start_fun_call →
94        ∀H:as_classifier S status_pre_fun_call cl_call.
95          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
96          trace_label_return S status_start_fun_call status_final →
97          as_costed S status_final →
98            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
99  (* A call followed by a non-empty trace. *)
100  | tal_step_call:
101      ∀end_flag: trace_ends_with_ret.
102      ∀status_pre_fun_call: S.
103      ∀status_start_fun_call: S.
104      ∀status_after_fun_call: S.
105      ∀status_final: S.
106        as_execute S status_pre_fun_call status_start_fun_call →
107        ∀H:as_classifier S status_pre_fun_call cl_call.
108          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
109          trace_label_return S status_start_fun_call status_after_fun_call →
110          ¬ as_costed S status_after_fun_call →
111          trace_any_label S end_flag status_after_fun_call status_final →
112            trace_any_label S end_flag status_pre_fun_call status_final
113  | tal_step_default:
114      ∀end_flag: trace_ends_with_ret.
115      ∀status_pre: S.
116      ∀status_init: S.
117      ∀status_end: S.
118        as_execute S status_pre status_init →
119        trace_any_label S end_flag status_init status_end →
120        as_classifier S status_pre cl_other →
121        ¬ (as_costed S status_init) →
122          trace_any_label S end_flag status_pre status_end.
123
124let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
125  on tal : list (as_pc S) ≝
126 match tal with
127 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
128 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
129 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
130 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
131 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
132 ].
133
134definition as_trace_any_label_length':
135    ∀S: abstract_status.
136    ∀trace_ends_flag: trace_ends_with_ret.
137    ∀start_status: S.
138    ∀final_status: S.
139    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
140      nat ≝
141  λS: abstract_status.
142  λtrace_ends_flag: trace_ends_with_ret.
143  λstart_status: S.
144  λfinal_status: S.
145  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
146    |tal_pc_list … the_trace|.
147
148let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
149  match tlr with
150  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
151  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
152  ]
153and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
154  match tll with
155  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
156  ]
157and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
158  match tal with
159  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
160    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
161    tal_unrepeating … tl ∧
162    tlr_unrepeating … tlr
163  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
164    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
165    tal_unrepeating … tl
166  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
167  | _ ⇒ True
168  ].
169
170definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
171  trace_label_label S fl st1 st2 → costlabel ≝
172  λS,fl,st1,st2,tr.match tr with
173  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
174
175definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
176  trace_label_return S st1 st2 → costlabel ≝
177  λS,st1,st2,tr.match tr with
178  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
179  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
180  ].
181
182let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
183  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
184cases tal //
185#fl' #st1' [#st_fun] #st2' #st3' #H
186[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
187#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
188qed.
189
190inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
191  | tac_base:
192      ∀status: S.
193        as_classifier S status cl_call →
194          trace_any_call S status status
195  | tac_step_call:
196      ∀status_pre_fun_call: S.
197      ∀status_after_fun_call: S.
198      ∀status_final: S.
199      ∀status_start_fun_call: S.
200        as_execute S status_pre_fun_call status_start_fun_call →
201        ∀H:as_classifier S status_pre_fun_call cl_call.
202          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
203          trace_label_return S status_start_fun_call status_after_fun_call →
204          ¬ as_costed S status_after_fun_call →
205          trace_any_call S status_after_fun_call status_final →
206            trace_any_call S status_pre_fun_call status_final
207  | tac_step_default:
208      ∀status_pre: S.
209      ∀status_end: S.
210      ∀status_init: S.
211        as_execute S status_pre status_init →
212        trace_any_call S status_init status_end →
213        as_classifier S status_pre cl_other →
214        ¬ (as_costed S status_init) →
215          trace_any_call S status_pre status_end.
216
217             
218inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
219  | tlc_base:
220      ∀start_status: S.
221      ∀end_status: S.
222        trace_any_call S start_status end_status →
223        as_costed S start_status →
224        trace_label_call S start_status end_status
225.
226
227definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
228  trace_label_call S st1 st2 → costlabel ≝
229  λS,st1,st2,tr.match tr with
230  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
231  ].
232   
233coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
234  | tld_step:
235      ∀status_initial: S.
236      ∀status_labelled: S.
237          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
238          trace_label_diverges S status_labelled →
239            trace_label_diverges S status_initial
240  | tld_base:
241      ∀status_initial: S.
242      ∀status_pre_fun_call: S.
243      ∀status_start_fun_call: S.
244        trace_label_call S status_initial status_pre_fun_call →
245        as_execute S status_pre_fun_call status_start_fun_call →
246        ∀H:as_classifier S status_pre_fun_call cl_call.
247          trace_label_diverges S status_start_fun_call →
248            trace_label_diverges S status_initial.
249
250definition tld_hd_label : ∀S : abstract_status.∀st.
251  trace_label_diverges S st → costlabel ≝
252  λS,st,tr.match tr with
253  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
254  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
255  ].       
256
257(* Version in Prop for showing existence. *)
258coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
259  | tld_step:
260      ∀status_initial: S.
261      ∀status_labelled: S.
262          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
263          trace_label_diverges_exists S status_labelled →
264            trace_label_diverges_exists S status_initial
265  | tld_base:
266      ∀status_initial: S.
267      ∀status_pre_fun_call: S.
268      ∀status_start_fun_call: S.
269        trace_label_call S status_initial status_pre_fun_call →
270        as_execute S status_pre_fun_call status_start_fun_call →
271        ∀H:as_classifier S status_pre_fun_call cl_call.
272          trace_label_diverges_exists S status_start_fun_call →
273            trace_label_diverges_exists S status_initial.
274
275inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
276  | twp_terminating:
277      ∀status_initial: S.
278      ∀status_start_fun: S.
279      ∀status_final: S.
280        as_classifier S status_initial cl_call →
281        as_execute S status_initial status_start_fun →
282        trace_label_return S status_start_fun status_final →
283        as_final S status_final →
284        trace_whole_program S status_initial
285  | twp_diverges:
286      ∀status_initial: S.
287      ∀status_start_fun: S.
288        as_classifier S status_initial cl_call →
289        as_execute S status_initial status_start_fun →
290        trace_label_diverges S status_start_fun →
291        trace_whole_program S status_initial.
292
293(* Again, an identical version in Prop for existence proofs. *)
294inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
295  | twp_terminating:
296      ∀status_initial: S.
297      ∀status_start_fun: S.
298      ∀status_final: S.
299        as_classifier S status_initial cl_call →
300        as_execute S status_initial status_start_fun →
301        trace_label_return S status_start_fun status_final →
302        as_final S status_final →
303        trace_whole_program_exists S status_initial
304  | twp_diverges:
305      ∀status_initial: S.
306      ∀status_start_fun: S.
307        as_classifier S status_initial cl_call →
308        as_execute S status_initial status_start_fun →
309        trace_label_diverges_exists S status_start_fun →
310        trace_whole_program_exists S status_initial.
311
312
313let rec trace_any_label_label S s s' f
314  (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 ] ≝
315match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
316[ tal_base_not_return start final _ _ C ⇒ C
317| tal_base_return _ _  _ _ ⇒ I
318| tal_base_call _ _ _ _ _ _ _ C ⇒ C
319| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
320| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
321].
322
323definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
324  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
325  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
326
327lemma trace_label_label_label : ∀S,s,s',f.
328  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
329#S #s #s' #f #tr
330cases tr
331#f #start #end #tr' #C @(trace_any_label_label … tr')
332qed.
333
334definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
335  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
336  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
337
338lemma trace_any_call_call : ∀S,s,s'.
339  trace_any_call S s s' → as_classifier S s' cl_call.
340#S #s #s' #T elim T //
341qed.
342
343(* an uncalling, unreturning and *unjumping*,
344  as well as unlabelled (but possibly for the first and last statuses)
345  possibly empty trace segment *)
346inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
347  | taa_base :
348      ∀start_status: S.
349        trace_any_any S start_status start_status
350  | taa_step :
351      ∀status_pre: S.
352      ∀status_init: S.
353      ∀status_end: S.
354        as_execute S status_pre status_init →
355        trace_any_any S status_init status_end →
356        as_classifier S status_pre cl_other →
357        ¬as_costed … status_init →
358          trace_any_any S status_pre status_end.
359
360let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
361  match taa with
362  [ taa_base st1' ⇒ [st1']
363  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
364  ].
365
366let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
367  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
368  match taa1
369  return λst1,st2.λx : trace_any_any S st1 st2.
370    trace_any_any S st2 st3 → trace_any_any S st1 st3
371  with
372  [ taa_base _ ⇒ λtaa2.taa2
373  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
374      taa_step … H (taa_append_taa … tl taa2) G K
375  ].
376
377let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
378  on taa :
379  trace_any_label S fl st2 st3 →
380  trace_any_label S fl st1 st3 ≝
381  match taa
382  return λst1,st2.λx : trace_any_any S st1 st2.
383    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
384  with
385  [ taa_base _ ⇒ λtaa2.taa2
386  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
387      tal_step_default … H (taa_append_tal … tl taa2) G K
388  ].
389
390let rec tlr_rel S1 st1 st1' S2 st2 st2'
391  (tlr1 : trace_label_return S1 st1 st1')
392  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
393match tlr1 with
394  [ tlr_base st1 st1' tll1 ⇒
395    match tlr2 with
396    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
397    | _ ⇒ False
398    ]
399  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
400    match tlr2 with
401    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
402      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
403    | _ ⇒ False
404    ]
405  ]
406and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
407 (tll1 : trace_label_label S1 fl1 st1 st1')
408 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
409  match tll1 with
410  [ tll_base fl1 st1 st1' tal1 H ⇒
411    match tll2 with
412    [ tll_base fl2 st2 st2 tal2 G ⇒
413      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
414      tal_rel … tal1 tal2
415    ]
416  ]
417and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
418 (tal1 : trace_any_label S1 fl1 st1 st1')
419 (tal2 : trace_any_label S2 fl2 st2 st2')
420   on tal1 : Prop ≝
421  match tal1 with
422  [ tal_base_not_return st1 st1' _ _ _ ⇒
423    ∃st2mid,taa,H,G,K.
424    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
425      (tal_base_not_return ? st2mid st2' H G K)
426  | tal_base_return st1 st1' _ _ ⇒
427    ∃st2mid,taa,H,G.
428    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
429      (tal_base_return ? st2mid st2' H G)
430  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
431    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
432    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
433      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
434      tlr_rel … tlr1 tlr2
435  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
436    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
437    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
438      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
439      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
440  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
441    tal_rel … tl1 tal2 (* <- this makes it many to many *)
442  ].
443
444include "ASM/BitVectorTrie.ma".
445include "ASM/Status.ma".
446include "ASM/Fetch.ma".
447
448let rec as_compute_cost_trace_label_label
449  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
450    (start_status: S) (final_status: S)
451      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
452        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
453  match the_trace with
454  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
455      let label ≝
456        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
457        [ None ⇒ λabs. ⊥
458        | Some l ⇒ λ_. l
459        ] labelled_proof
460      in
461        (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
462  ]
463and as_compute_cost_trace_any_label
464  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
465    (start_status: S) (final_status: S)
466      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
467        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
468  match the_trace with
469  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
470  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
471      as_compute_cost_trace_label_return … call_trace
472  | tal_base_return the_status _ _ _ ⇒ [ ]
473  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
474    _ _ _ call_trace _ final_trace ⇒
475    let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
476    let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
477        call_cost_trace @ final_cost_trace
478  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
479      as_compute_cost_trace_any_label … tail_trace
480  ]
481and as_compute_cost_trace_label_return
482  (S: abstract_status)
483    (start_status: S) (final_status: S)
484      (the_trace: trace_label_return S start_status final_status)
485        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
486  match the_trace with
487  [ tlr_base before after trace_to_lift ⇒
488      as_compute_cost_trace_label_label … trace_to_lift
489  | tlr_step initial labelled final labelled_trace ret_trace ⇒
490    let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
491    let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
492        labelled_cost @ return_cost
493  ].
494  [2:
495    cases abs -abs #abs @abs %
496  |1:
497    %{initial} whd in match label;
498    generalize in match labelled_proof; whd in ⊢ (% → ?);
499    cases (as_label S initial)
500    [1:
501      #absurd @⊥ cases absurd -absurd #absurd @absurd %
502    |2:
503      #costlabel normalize nodelta #_ %
504    ]
505  ]
506qed.
Note: See TracBrowser for help on using the repository browser.