Changeset 2498 for src/ASM/ASMCostsSplit.ma
- Timestamp:
- Nov 27, 2012, 6:01:50 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCostsSplit.ma
r2475 r2498 5 5 6 6 let rec traverse_code_internal 7 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)7 (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map) 8 8 (program_counter: Word) (program_size: nat) 9 9 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16) … … 279 279 definition traverse_code: 280 280 ∀code_memory: BitVectorTrie Byte 16. 281 ∀cost_labels: BitVectorTrie costlabel 16.281 ∀cost_labels: costlabel_map. 282 282 ∀cost_labels_injective: 283 283 ∀pc, pc',l. … … 289 289 pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝ 290 290 λcode_memory: BitVectorTrie Byte 16. 291 λcost_labels: BitVectorTrie costlabel 16.291 λcost_labels: costlabel_map. 292 292 λcost_labels_injective. 293 293 pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?). … … 318 318 definition compute_costs ≝ 319 319 λprogram: list Byte. 320 λcost_labels: BitVectorTrie costlabel 16.320 λcost_labels: costlabel_map. 321 321 λcost_labels_injective: 322 322 ∀pc, pc',l. … … 327 327 traverse_code code_memory cost_labels cost_labels_injective. 328 328 329 definition object_code ≝ list Byte. 330 definition costlabel_map ≝ BitVectorTrie costlabel 16. 329 (* definition object_code ≝ list Byte. *) 331 330 331 (* use of this defn in ASM/CostsProof.ma is ill-typed *) 332 332 definition ASM_cost_map : 333 333 ∀p.let code_memory ≝ load_code_memory (\fst p) in
Note: See TracChangeset
for help on using the changeset viewer.