Changeset 2498 for src/ASM/ASMCosts.ma
- Timestamp:
- Nov 27, 2012, 6:01:50 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r2475 r2498 5 5 include "common/StructuredTraces.ma". 6 6 7 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝ 7 (* moved to Fetch.ma *) 8 (* definition costlabel_map ≝ BitVectorTrie costlabel 16. *) 9 10 definition ASM_abstract_status: ∀code_memory. costlabel_map → abstract_status ≝ 8 11 λcode_memory. 9 12 λcost_labels. … … 23 26 definition trace_any_label_length ≝ 24 27 λcode_memory: BitVectorTrie Byte 16. 25 λcost_labels: BitVectorTrie costlabel 16.28 λcost_labels: costlabel_map. 26 29 λtrace_ends_flag: trace_ends_with_ret. 27 30 λstart_status: Status code_memory. … … 139 142 lemma sublist_tal_pc_list_all_program_counter_list: 140 143 ∀code_memory: BitVectorTrie Byte 16. 141 ∀cost_labels: BitVectorTrie costlabel 16.144 ∀cost_labels: costlabel_map. 142 145 ∀start, final: Status code_memory. 143 146 ∀trace_ends_flag. … … 152 155 corollary tal_pc_list_length_leq_total_program_size: 153 156 ∀code_memory: BitVectorTrie Byte 16. 154 ∀cost_labels: BitVectorTrie costlabel 16.157 ∀cost_labels: costlabel_map. 155 158 ∀start, final: Status code_memory. 156 159 ∀trace_ends_flag. … … 171 174 172 175 let rec compute_paid_trace_any_label 173 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)176 (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map) 174 177 (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory) 175 178 (final_status: Status code_memory) … … 196 199 definition compute_paid_trace_label_label ≝ 197 200 λcode_memory: BitVectorTrie Byte 16. 198 λcost_labels: BitVectorTrie costlabel 16.201 λcost_labels: costlabel_map. 199 202 λtrace_ends_flag: trace_ends_with_ret. 200 203 λstart_status: Status code_memory. … … 209 212 ∀code_memory' : (BitVectorTrie Byte 16). 210 213 ∀program_counter' : Word. 211 ∀cost_labels : (BitVectorTrie costlabel 16).214 ∀cost_labels : costlabel_map. 212 215 ∀program_size' : ℕ. 213 216 ∀ticks : ℕ. … … 363 366 ∀code_memory': BitVectorTrie Byte 16. 364 367 ∀program_counter': Word. 365 ∀cost_labels: BitVectorTrie costlabel 16.368 ∀cost_labels: costlabel_map. 366 369 ∀first_time_around: bool. 367 370 ∀program_size': ℕ. … … 418 421 ∀code_memory' : (BitVectorTrie Byte 16). 419 422 ∀program_counter' : Word. 420 ∀cost_labels : (BitVectorTrie costlabel 16).423 ∀cost_labels : costlabel_map. 421 424 ∀program_size' : ℕ. 422 425 ∀ticks : ℕ. … … 555 558 ∀code_memory' : (BitVectorTrie Byte 16). 556 559 ∀program_counter' : Word. 557 ∀cost_labels : (BitVectorTrie costlabel 16).560 ∀cost_labels : costlabel_map. 558 561 ∀program_size' : ℕ. 559 562 ∀ticks : ℕ. … … 613 616 lemma trace_any_label_length_leq_0_to_False: 614 617 ∀code_memory: BitVectorTrie Byte 16. 615 ∀cost_labels: BitVectorTrie costlabel 16.618 ∀cost_labels: costlabel_map. 616 619 ∀trace_ends_flag: trace_ends_with_ret. 617 620 ∀start_status: Status code_memory. … … 627 630 let rec block_cost' 628 631 (code_memory': BitVectorTrie Byte 16) (program_counter': Word) 629 (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)632 (program_size: nat) (cost_labels: costlabel_map) 630 633 (first_time_around: bool) 631 634 on program_size: … … 760 763 ∀code_memory': BitVectorTrie Byte 16. 761 764 ∀program_counter': Word. 762 ∀cost_labels: BitVectorTrie costlabel 16.765 ∀cost_labels: costlabel_map. 763 766 Σcost_of_block: nat. 764 767 ∀start_status: Status code_memory'. … … 771 774 λcode_memory: BitVectorTrie Byte 16. 772 775 λprogram_counter: Word. 773 λcost_labels: BitVectorTrie costlabel 16. ?.776 λcost_labels: costlabel_map. ?. 774 777 cases(block_cost' code_memory program_counter (2^16) cost_labels true) 775 778 #cost_of_block #block_cost_hyp
Note: See TracChangeset
for help on using the changeset viewer.