Changeset 2498 for src/ASM/ASMCostsSplit.ma

Timestamp:

Nov 27, 2012, 6:01:50 PM (8 years ago)

Author:

mckinna

Message:

Refactor:
Typedefs object_code and costlabel_map lifted out from ASMCostsSplit.ma
Dependencies simplified.

File:

• src/ASM/ASMCostsSplit.ma (modified) (5 diffs)

src/ASM/ASMCostsSplit.ma

@@ -5 +5 @@
 
 let rec traverse_code_internal
-  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
+  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
     (program_counter: Word) (program_size: nat)
       (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
@@ -279 +279 @@
 definition traverse_code:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀cost_labels_injective:
     ∀pc, pc',l.
@@ -289 +289 @@
           pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
   λcode_memory: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_labels: costlabel_map.
   λcost_labels_injective.
     pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
@@ -318 +318 @@
 definition compute_costs ≝
   λprogram: list Byte.
-  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_labels: costlabel_map.
   λcost_labels_injective:
     ∀pc, pc',l.
@@ -327 +327 @@
       traverse_code code_memory cost_labels cost_labels_injective.
 
-definition object_code ≝ list Byte.
-definition costlabel_map ≝ BitVectorTrie costlabel 16.      
+(* definition object_code ≝ list Byte. *)
 
+(* use of this defn in ASM/CostsProof.ma is ill-typed *)
 definition ASM_cost_map :
   ∀p.let code_memory ≝ load_code_memory (\fst p) in