Changeset 2999 for src/ASM/CostsProof.ma
- Timestamp:
- Mar 28, 2013, 12:47:55 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r2907 r2999 11 11 (prog: labelled_object_code) 12 12 (trace_ends_flag: trace_ends_with_ret) 13 (start_status: Status ( load_code_memory (oc prog)))14 (final_status: Status ( load_code_memory (oc prog)))13 (start_status: Status (cm prog)) 14 (final_status: Status (cm prog)) 15 15 (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag 16 16 start_status final_status) on the_trace: nat ≝ … … 22 22 (prog: labelled_object_code) 23 23 (trace_ends_flag: trace_ends_with_ret) 24 (start_status: Status ( load_code_memory (oc prog)))25 (final_status: Status ( load_code_memory (oc prog)))24 (start_status: Status (cm prog)) 25 (final_status: Status (cm prog)) 26 26 (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status) 27 27 on the_trace: nat ≝ … … 53 53 and compute_max_trace_label_return_cost 54 54 (prog: labelled_object_code) 55 (start_status: Status ( load_code_memory (oc prog)))56 (final_status: Status ( load_code_memory (oc prog)))55 (start_status: Status (cm prog)) 56 (final_status: Status (cm prog)) 57 57 (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status) 58 58 on the_trace: nat ≝ … … 70 70 (prog: labelled_object_code) 71 71 (trace_ends_flag: trace_ends_with_ret) 72 (start_status: Status ( load_code_memory (oc prog)))73 (final_status: Status ( load_code_memory (oc prog)))72 (start_status: Status (cm prog)) 73 (final_status: Status (cm prog)) 74 74 (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag 75 75 start_status final_status) on the_trace: 76 clock … ( load_code_memory (oc prog)) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?76 clock … (cm prog) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ? 77 77 and compute_max_trace_any_label_cost_is_ok 78 78 (prog: labelled_object_code) 79 79 (trace_ends_flag: trace_ends_with_ret) 80 (start_status: Status ( load_code_memory (oc prog)))81 (final_status: Status ( load_code_memory (oc prog)))80 (start_status: Status (cm prog)) 81 (final_status: Status (cm prog)) 82 82 (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status) 83 83 on the_trace: 84 clock … ( load_code_memory (oc prog)) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?84 clock … (cm prog) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ? 85 85 and compute_max_trace_label_return_cost_is_ok 86 86 (prog: labelled_object_code) 87 (start_status: Status ( load_code_memory (oc prog)))88 (final_status: Status ( load_code_memory (oc prog)))87 (start_status: Status (cm prog)) 88 (final_status: Status (cm prog)) 89 89 (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status) 90 90 on the_trace: 91 clock … ( load_code_memory (oc prog)) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (load_code_memory (oc prog)) … start_status ≝ ?.91 clock … (cm prog) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (cm prog) … start_status ≝ ?. 92 92 [1: 93 93 cases the_trace … … 127 127 >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call 128 128 status_after_fun_call call_trace) 129 cases(is_next) in match (clock … ( load_code_memory (oc prog)) status_start_fun_call);129 cases(is_next) in match (clock … (cm prog) status_start_fun_call); 130 130 >(execute_1_ok_clock … status_pre_fun_call) 131 131 <associative_plus in ⊢ (??%?); … … 149 149 >(compute_max_trace_any_label_cost_is_ok prog end_flag 150 150 status_init status_end trace_any_label) 151 cases(is_next) in match (clock … ( load_code_memory (oc prog)) status_init);151 cases(is_next) in match (clock … (cm prog) status_init); 152 152 >(execute_1_ok_clock … status_pre) 153 153 >commutative_plus >associative_plus >associative_plus @eq_f … … 175 175 (prog:labelled_object_code) 176 176 (trace_ends_flag: trace_ends_with_ret) 177 (start_status: Status ( load_code_memory (oc prog)))178 (final_status: Status ( load_code_memory (oc prog)))177 (start_status: Status (cm prog)) 178 (final_status: Status (cm prog)) 179 179 (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag 180 180 start_status final_status) on the_trace: nat ≝ … … 187 187 (prog:labelled_object_code) 188 188 (trace_ends_flag: trace_ends_with_ret) 189 (start_status: Status ( load_code_memory (oc prog)))190 (final_status: Status ( load_code_memory (oc prog)))189 (start_status: Status (cm prog)) 190 (final_status: Status (cm prog)) 191 191 (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status) 192 192 on the_trace: nat ≝ … … 209 209 and compute_trace_label_return_cost_using_paid 210 210 (prog:labelled_object_code) 211 (start_status: Status ( load_code_memory (oc prog)))212 (final_status: Status ( load_code_memory (oc prog)))211 (start_status: Status (cm prog)) 212 (final_status: Status (cm prog)) 213 213 (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status) 214 214 on the_trace: nat ≝ … … 224 224 (prog:labelled_object_code) 225 225 (trace_ends_flag: trace_ends_with_ret) 226 (start_status: Status ( load_code_memory (oc prog)))227 (final_status: Status ( load_code_memory (oc prog)))226 (start_status: Status (cm prog)) 227 (final_status: Status (cm prog)) 228 228 (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag 229 229 start_status final_status) on the_trace: … … 233 233 (prog:labelled_object_code) 234 234 (trace_ends_flag: trace_ends_with_ret) 235 (start_status: Status ( load_code_memory (oc prog)))236 (final_status: Status ( load_code_memory (oc prog)))235 (start_status: Status (cm prog)) 236 (final_status: Status (cm prog)) 237 237 (the_trace: trace_any_label (OC_abstract_status prog) 238 238 trace_ends_flag start_status final_status) on the_trace: … … 242 242 and compute_trace_label_return_cost_using_paid_ok 243 243 (prog:labelled_object_code) 244 (start_status: Status ( load_code_memory (oc prog)))245 (final_status: Status ( load_code_memory (oc prog)))244 (start_status: Status (cm prog)) 245 (final_status: Status (cm prog)) 246 246 (the_trace: trace_label_return (OC_abstract_status prog) 247 247 start_status final_status) on the_trace: … … 454 454 (prog: labelled_object_code) 455 455 (cost_map: identifier_map CostTag nat) 456 (initial: Status ( load_code_memory (oc prog)))457 (final: Status ( load_code_memory (oc prog)))456 (initial: Status (cm prog)) 457 (final: Status (cm prog)) 458 458 (trace: trace_label_return (OC_abstract_status prog) initial final) 459 459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k)) … … 470 470 (trace_ends_flag: trace_ends_with_ret) 471 471 (cost_map: identifier_map CostTag nat) 472 (initial: Status ( load_code_memory (oc prog)))473 (final: Status ( load_code_memory (oc prog)))472 (initial: Status (cm prog)) 473 (final: Status (cm prog)) 474 474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final) 475 475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k)) … … 486 486 (trace_ends_flag: trace_ends_with_ret) 487 487 (cost_map: identifier_map CostTag nat) 488 (initial: Status ( load_code_memory (oc prog)))489 (final: Status ( load_code_memory (oc prog)))488 (initial: Status (cm prog)) 489 (final: Status (cm prog)) 490 490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final) 491 491 (unrepeating_witness: tll_unrepeating … trace) … … 630 630 ∀prog: labelled_object_code. 631 631 ∀cost_map: identifier_map CostTag nat. 632 ∀initial: Status ( load_code_memory (oc prog)).633 ∀final: Status ( load_code_memory (oc prog)).632 ∀initial: Status (cm prog). 633 ∀final: Status (cm prog). 634 634 ∀trace: trace_label_return (OC_abstract_status prog) initial final. 635 635 ∀unrepeating_witness: tlr_unrepeating … trace. … … 638 638 pi1 … (block_cost prog pc) = lookup_present … k_pres). 639 639 let ctrace ≝ flatten_trace_label_return … trace in 640 clock … ( load_code_memory (oc prog)) … final =641 clock … ( load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).640 clock … (cm prog) … final = 641 clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)). 642 642 #prog #cost_map 643 643 #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta … … 648 648 theorem compute_max_trace_label_return_cost_ok_with_trace: 649 649 ∀prog: labelled_object_code. 650 ∀initial: Status ( load_code_memory (oc prog)).651 ∀final: Status ( load_code_memory (oc prog)).650 ∀initial: Status (cm prog). 651 ∀final: Status (cm prog). 652 652 ∀trace: trace_label_return (OC_abstract_status prog) initial final. 653 653 ∀unrepeating_witness: tlr_unrepeating … trace. 654 654 let cost_map ≝ traverse_code prog in 655 655 let ctrace ≝ flatten_trace_label_return … trace in 656 clock … ( load_code_memory (oc prog)) … final = clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).656 clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)). 657 657 [1: 658 658 #prog #initial #final #trace #unrepeating_witness
Note: See TracChangeset
for help on using the changeset viewer.