Changeset 2498 for src/ASM/CostsProof.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/CostsProof.ma (modified) (23 diffs)

src/ASM/CostsProof.ma

@@ -10 +10 @@
 let rec compute_max_trace_label_label_cost
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
    (trace_ends_flag: trace_ends_with_ret)
     (start_status: Status cm) (final_status: Status cm)
@@ -21 +21 @@
 and compute_max_trace_any_label_cost
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status cm) (final_status: Status cm)
@@ -49 +49 @@
 and compute_max_trace_label_return_cost
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (start_status: Status cm) (final_status: Status cm)
     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
@@ -65 +65 @@
 let rec compute_max_trace_label_label_cost_is_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
    (trace_ends_flag: trace_ends_with_ret)
     (start_status: Status cm) (final_status: Status cm)
@@ -73 +73 @@
 and compute_max_trace_any_label_cost_is_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status cm) (final_status: Status cm)
@@ -81 +81 @@
 and compute_max_trace_label_return_cost_is_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (start_status: Status cm) (final_status: Status cm)
     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
@@ -164 +164 @@
 let rec compute_trace_label_label_cost_using_paid
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
    (trace_ends_flag: trace_ends_with_ret)
     (start_status: Status cm) (final_status: Status cm)
@@ -176 +176 @@
 and compute_trace_any_label_cost_using_paid
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status cm) (final_status: Status cm)
@@ -197 +197 @@
 and compute_trace_label_return_cost_using_paid
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (start_status: Status cm) (final_status: Status cm)
     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
@@ -211 +211 @@
 let rec compute_trace_label_label_cost_using_paid_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
    (trace_ends_flag: trace_ends_with_ret)
     (start_status: Status cm) (final_status: Status cm)
@@ -220 +220 @@
 and compute_trace_any_label_cost_using_paid_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status cm) (final_status: Status cm)
@@ -230 +230 @@
 and compute_trace_label_return_cost_using_paid_ok
   (cm: ?)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (start_status: Status cm) (final_status: Status cm)
     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
@@ -271 +271 @@
 let rec compute_cost_trace_label_label
   (cm: BitVectorTrie Byte 16)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
    (trace_ends_flag: trace_ends_with_ret)
     (start_status: Status cm) (final_status: Status cm)
@@ -288 +288 @@
 and compute_cost_trace_any_label
   (cm: BitVectorTrie Byte 16)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (trace_ends_flag: trace_ends_with_ret)
    (start_status: Status cm) (final_status: Status cm)
@@ -309 +309 @@
 and compute_cost_trace_label_return
   (cm: BitVectorTrie Byte 16)
-  (cost_labels: BitVectorTrie costlabel 16)
+  (cost_labels: costlabel_map)
   (start_status: Status cm) (final_status: Status cm)
     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
@@ -386 +386 @@
 
 definition tech_cost_of_label0:
- ∀cost_labels: BitVectorTrie costlabel 16.
+ ∀cost_labels: costlabel_map.
  ∀cost_map: identifier_map CostTag nat.
  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
@@ -447 +447 @@
 
 definition tech_cost_of_label:
- ∀cost_labels: BitVectorTrie costlabel 16.
+ ∀cost_labels: costlabel_map.
  ∀cost_map: identifier_map CostTag nat.
  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
@@ -501 +501 @@
     
 let rec compute_trace_label_return_using_paid_ok_with_trace
- (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
+ (cm: ?) (cost_labels: costlabel_map)
  (cost_map: identifier_map CostTag nat)
  (initial: Status cm) (final: Status cm)
@@ -515 +515 @@
     ≝ ?
 and compute_trace_any_label_using_paid_ok_with_trace
- (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
+ (cm: ?) (cost_labels: costlabel_map)
  (trace_ends_flag: trace_ends_with_ret)
  (cost_map: identifier_map CostTag nat)
@@ -530 +530 @@
     ≝ ?
 and compute_trace_label_label_using_paid_ok_with_trace
- (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
+ (cm: ?) (cost_labels: costlabel_map)
  (trace_ends_flag: trace_ends_with_ret)
  (cost_map: identifier_map CostTag nat)
@@ -649 +649 @@
 lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀cost_map: identifier_map CostTag nat.
   ∀initial: Status code_memory.
@@ -669 +669 @@
 theorem compute_max_trace_label_return_cost_ok_with_trace:
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀cost_labels_injective:
    (∀pc,pc',l.
@@ -697 +697 @@
   
 include "utilities/permutations.ma".
-
+(*
+lemma tech_cost_sum_eq_as_cost :
+  ∀code_memory: object_code.
+  ∀cost_labels: costlabel_map.
+  ∀cost_map: identifier_map CostTag nat.
+  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
+  ∀trace.
+  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
+  (Σ_{l ∈ trace}(ASM_cost_map 〈code_memory, cost_labels〉 … codom_dom l)).
+#cmem #clab #cmap #codom_dom #trace
+@(list_elim_left … trace)
+[ %
+| #tl #hd #IH >append_length >commutative_plus
+  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
+  whd in ⊢ (??%%); <IH
+  <tech_cost_of_label_shift [2: %]
+  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
+  [ %
+  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
+  ]
+]
+qed.
+*)
 lemma tech_cost_sum_eq_as_cost :
   ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
+  ∀cost_labels: costlabel_map.
   ∀cost_map: identifier_map CostTag nat.
   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).