Changeset 2498 for src/ASM/ASMCosts.ma

Timestamp:

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

Author:

mckinna

Message:

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

File:

• src/ASM/ASMCosts.ma (modified) (14 diffs)

src/ASM/ASMCosts.ma

@@ -5 +5 @@
 include "common/StructuredTraces.ma".
 
-definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
+(* moved to Fetch.ma *)
+(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
+
+definition ASM_abstract_status: ∀code_memory. costlabel_map → abstract_status ≝
   λcode_memory.
   λcost_labels.
@@ -23 +26 @@
 definition trace_any_label_length ≝
   λcode_memory: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_labels: costlabel_map.
   λtrace_ends_flag: trace_ends_with_ret.
   λstart_status: Status code_memory.
@@ -139 +142 @@
 lemma sublist_tal_pc_list_all_program_counter_list:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀start, final: Status code_memory.
   ∀trace_ends_flag.
@@ -152 +155 @@
 corollary tal_pc_list_length_leq_total_program_size:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀start, final: Status code_memory.
   ∀trace_ends_flag.
@@ -171 +174 @@
 
 let rec compute_paid_trace_any_label
-  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
+  (code_memory: BitVectorTrie Byte 16) (cost_labels: costlabel_map)
     (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
       (final_status: Status code_memory)
@@ -196 +199 @@
 definition compute_paid_trace_label_label ≝
   λcode_memory: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie costlabel 16.
+  λcost_labels: costlabel_map.
   λtrace_ends_flag: trace_ends_with_ret.
   λstart_status: Status code_memory.
@@ -209 +212 @@
   ∀code_memory' : (BitVectorTrie Byte 16).
   ∀program_counter' : Word.
-  ∀cost_labels : (BitVectorTrie costlabel 16).
+  ∀cost_labels : costlabel_map.
   ∀program_size' : ℕ.
   ∀ticks : ℕ.
@@ -363 +366 @@
   ∀code_memory': BitVectorTrie Byte 16.
   ∀program_counter': Word.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀first_time_around: bool.
   ∀program_size': ℕ.
@@ -418 +421 @@
   ∀code_memory' : (BitVectorTrie Byte 16).
   ∀program_counter' : Word.
-  ∀cost_labels : (BitVectorTrie costlabel 16).
+  ∀cost_labels : costlabel_map.
   ∀program_size' : ℕ.
   ∀ticks : ℕ.
@@ -555 +558 @@
   ∀code_memory' : (BitVectorTrie Byte 16).
   ∀program_counter' : Word.
-  ∀cost_labels : (BitVectorTrie costlabel 16).
+  ∀cost_labels : costlabel_map.
   ∀program_size' : ℕ.
   ∀ticks : ℕ.
@@ -613 +616 @@
 lemma trace_any_label_length_leq_0_to_False:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀trace_ends_flag: trace_ends_with_ret.
   ∀start_status: Status code_memory.
@@ -627 +630 @@
 let rec block_cost'
   (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
-    (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
+    (program_size: nat) (cost_labels: costlabel_map)
       (first_time_around: bool)
         on program_size:
@@ -760 +763 @@
     ∀code_memory': BitVectorTrie Byte 16.
     ∀program_counter': Word.
-    ∀cost_labels: BitVectorTrie costlabel 16.
+    ∀cost_labels: costlabel_map.
       Σcost_of_block: nat.
         ∀start_status: Status code_memory'.
@@ -771 +774 @@
   λcode_memory: BitVectorTrie Byte 16.
   λprogram_counter: Word.
-  λcost_labels: BitVectorTrie costlabel 16. ?.
+  λcost_labels: costlabel_map. ?.
   cases(block_cost' code_memory program_counter (2^16) cost_labels true)
   #cost_of_block #block_cost_hyp