Changeset 2498 for src/ASM/CostsProof.ma
- Timestamp:
- Nov 27, 2012, 6:01:50 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r2057 r2498 10 10 let rec compute_max_trace_label_label_cost 11 11 (cm: ?) 12 (cost_labels: BitVectorTrie costlabel 16)12 (cost_labels: costlabel_map) 13 13 (trace_ends_flag: trace_ends_with_ret) 14 14 (start_status: Status cm) (final_status: Status cm) … … 21 21 and compute_max_trace_any_label_cost 22 22 (cm: ?) 23 (cost_labels: BitVectorTrie costlabel 16)23 (cost_labels: costlabel_map) 24 24 (trace_ends_flag: trace_ends_with_ret) 25 25 (start_status: Status cm) (final_status: Status cm) … … 49 49 and compute_max_trace_label_return_cost 50 50 (cm: ?) 51 (cost_labels: BitVectorTrie costlabel 16)51 (cost_labels: costlabel_map) 52 52 (start_status: Status cm) (final_status: Status cm) 53 53 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) … … 65 65 let rec compute_max_trace_label_label_cost_is_ok 66 66 (cm: ?) 67 (cost_labels: BitVectorTrie costlabel 16)67 (cost_labels: costlabel_map) 68 68 (trace_ends_flag: trace_ends_with_ret) 69 69 (start_status: Status cm) (final_status: Status cm) … … 73 73 and compute_max_trace_any_label_cost_is_ok 74 74 (cm: ?) 75 (cost_labels: BitVectorTrie costlabel 16)75 (cost_labels: costlabel_map) 76 76 (trace_ends_flag: trace_ends_with_ret) 77 77 (start_status: Status cm) (final_status: Status cm) … … 81 81 and compute_max_trace_label_return_cost_is_ok 82 82 (cm: ?) 83 (cost_labels: BitVectorTrie costlabel 16)83 (cost_labels: costlabel_map) 84 84 (start_status: Status cm) (final_status: Status cm) 85 85 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) … … 164 164 let rec compute_trace_label_label_cost_using_paid 165 165 (cm: ?) 166 (cost_labels: BitVectorTrie costlabel 16)166 (cost_labels: costlabel_map) 167 167 (trace_ends_flag: trace_ends_with_ret) 168 168 (start_status: Status cm) (final_status: Status cm) … … 176 176 and compute_trace_any_label_cost_using_paid 177 177 (cm: ?) 178 (cost_labels: BitVectorTrie costlabel 16)178 (cost_labels: costlabel_map) 179 179 (trace_ends_flag: trace_ends_with_ret) 180 180 (start_status: Status cm) (final_status: Status cm) … … 197 197 and compute_trace_label_return_cost_using_paid 198 198 (cm: ?) 199 (cost_labels: BitVectorTrie costlabel 16)199 (cost_labels: costlabel_map) 200 200 (start_status: Status cm) (final_status: Status cm) 201 201 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) … … 211 211 let rec compute_trace_label_label_cost_using_paid_ok 212 212 (cm: ?) 213 (cost_labels: BitVectorTrie costlabel 16)213 (cost_labels: costlabel_map) 214 214 (trace_ends_flag: trace_ends_with_ret) 215 215 (start_status: Status cm) (final_status: Status cm) … … 220 220 and compute_trace_any_label_cost_using_paid_ok 221 221 (cm: ?) 222 (cost_labels: BitVectorTrie costlabel 16)222 (cost_labels: costlabel_map) 223 223 (trace_ends_flag: trace_ends_with_ret) 224 224 (start_status: Status cm) (final_status: Status cm) … … 230 230 and compute_trace_label_return_cost_using_paid_ok 231 231 (cm: ?) 232 (cost_labels: BitVectorTrie costlabel 16)232 (cost_labels: costlabel_map) 233 233 (start_status: Status cm) (final_status: Status cm) 234 234 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) … … 271 271 let rec compute_cost_trace_label_label 272 272 (cm: BitVectorTrie Byte 16) 273 (cost_labels: BitVectorTrie costlabel 16)273 (cost_labels: costlabel_map) 274 274 (trace_ends_flag: trace_ends_with_ret) 275 275 (start_status: Status cm) (final_status: Status cm) … … 288 288 and compute_cost_trace_any_label 289 289 (cm: BitVectorTrie Byte 16) 290 (cost_labels: BitVectorTrie costlabel 16)290 (cost_labels: costlabel_map) 291 291 (trace_ends_flag: trace_ends_with_ret) 292 292 (start_status: Status cm) (final_status: Status cm) … … 309 309 and compute_cost_trace_label_return 310 310 (cm: BitVectorTrie Byte 16) 311 (cost_labels: BitVectorTrie costlabel 16)311 (cost_labels: costlabel_map) 312 312 (start_status: Status cm) (final_status: Status cm) 313 313 (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status) … … 386 386 387 387 definition tech_cost_of_label0: 388 ∀cost_labels: BitVectorTrie costlabel 16.388 ∀cost_labels: costlabel_map. 389 389 ∀cost_map: identifier_map CostTag nat. 390 390 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). … … 447 447 448 448 definition tech_cost_of_label: 449 ∀cost_labels: BitVectorTrie costlabel 16.449 ∀cost_labels: costlabel_map. 450 450 ∀cost_map: identifier_map CostTag nat. 451 451 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). … … 501 501 502 502 let rec compute_trace_label_return_using_paid_ok_with_trace 503 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)503 (cm: ?) (cost_labels: costlabel_map) 504 504 (cost_map: identifier_map CostTag nat) 505 505 (initial: Status cm) (final: Status cm) … … 515 515 ≝ ? 516 516 and compute_trace_any_label_using_paid_ok_with_trace 517 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)517 (cm: ?) (cost_labels: costlabel_map) 518 518 (trace_ends_flag: trace_ends_with_ret) 519 519 (cost_map: identifier_map CostTag nat) … … 530 530 ≝ ? 531 531 and compute_trace_label_label_using_paid_ok_with_trace 532 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)532 (cm: ?) (cost_labels: costlabel_map) 533 533 (trace_ends_flag: trace_ends_with_ret) 534 534 (cost_map: identifier_map CostTag nat) … … 649 649 lemma compute_max_trace_label_return_cost_ok_with_trace_aux: 650 650 ∀code_memory: BitVectorTrie Byte 16. 651 ∀cost_labels: BitVectorTrie costlabel 16.651 ∀cost_labels: costlabel_map. 652 652 ∀cost_map: identifier_map CostTag nat. 653 653 ∀initial: Status code_memory. … … 669 669 theorem compute_max_trace_label_return_cost_ok_with_trace: 670 670 ∀code_memory: BitVectorTrie Byte 16. 671 ∀cost_labels: BitVectorTrie costlabel 16.671 ∀cost_labels: costlabel_map. 672 672 ∀cost_labels_injective: 673 673 (∀pc,pc',l. … … 697 697 698 698 include "utilities/permutations.ma". 699 699 (* 700 lemma tech_cost_sum_eq_as_cost : 701 ∀code_memory: object_code. 702 ∀cost_labels: costlabel_map. 703 ∀cost_map: identifier_map CostTag nat. 704 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 705 ∀trace. 706 (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) = 707 (Σ_{l ∈ trace}(ASM_cost_map 〈code_memory, cost_labels〉 … codom_dom l)). 708 #cmem #clab #cmap #codom_dom #trace 709 @(list_elim_left … trace) 710 [ % 711 | #tl #hd #IH >append_length >commutative_plus 712 >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ] 713 whd in ⊢ (??%%); <IH 714 <tech_cost_of_label_shift [2: %] 715 cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP 716 [ % 717 | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/ 718 ] 719 ] 720 qed. 721 *) 700 722 lemma tech_cost_sum_eq_as_cost : 701 723 ∀code_memory: BitVectorTrie Byte 16. 702 ∀cost_labels: BitVectorTrie costlabel 16.724 ∀cost_labels: costlabel_map. 703 725 ∀cost_map: identifier_map CostTag nat. 704 726 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
Note: See TracChangeset
for help on using the changeset viewer.