Changeset 2516 for src/ASM/ASMCostsSplit.ma
- Timestamp:
- Dec 2, 2012, 5:45:36 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCostsSplit.ma
r2508 r2516 5 5 6 6 let rec traverse_code_internal 7 (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)7 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 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: costlabel_map.281 ∀cost_labels: BitVectorTrie costlabel 16. 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: costlabel_map.291 λcost_labels: BitVectorTrie costlabel 16. 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: costlabel_map.320 λcost_labels: BitVectorTrie costlabel 16. 321 321 λcost_labels_injective: 322 322 ∀pc, pc',l. … … 327 327 traverse_code code_memory cost_labels cost_labels_injective. 328 328 329 (* JHM: moved to Fetch.ma *)330 (* definition object_code ≝ list Byte. *)331 (* definition costlabel_map ≝ BitVectorTrie costlabel 16. *)332 333 329 (* use of this defn in ASM/CostsProof.ma is ill-typed *) 334 330 definition ASM_cost_map : 335 ∀p: object_code × costlabel_map.331 ∀p: (list Byte) × (BitVectorTrie costlabel 16). 336 332 let code_memory ≝ load_code_memory (\fst p) in 337 333 let a_s ≝ ASM_abstract_status code_memory (\snd p) in
Note: See TracChangeset
for help on using the changeset viewer.