Changeset 2999 for src/ASM/CostsProof.ma

Timestamp:

Mar 28, 2013, 12:47:55 PM (7 years ago)

Author:

sacerdot

Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:

• src/ASM/CostsProof.ma (modified) (18 diffs)

src/ASM/CostsProof.ma

@@ -11 +11 @@
   (prog: labelled_object_code)
    (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
       (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
         start_status final_status) on the_trace: nat ≝
@@ -22 +22 @@
   (prog: labelled_object_code)
   (trace_ends_flag: trace_ends_with_ret)
-   (start_status: Status (load_code_memory (oc prog)))
-   (final_status: Status (load_code_memory (oc prog)))
+   (start_status: Status (cm prog))
+   (final_status: Status (cm prog))
      (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
        on the_trace: nat ≝
@@ -53 +53 @@
 and compute_max_trace_label_return_cost
   (prog: labelled_object_code)
-  (start_status: Status (load_code_memory (oc prog)))
-  (final_status: Status (load_code_memory (oc prog)))
+  (start_status: Status (cm prog))
+  (final_status: Status (cm prog))
     (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
       on the_trace: nat ≝
@@ -70 +70 @@
   (prog: labelled_object_code)
    (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
       (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
         start_status final_status) on the_trace:
-          clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
+          clock … (cm prog) … final_status = (compute_max_trace_label_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
 and compute_max_trace_any_label_cost_is_ok
   (prog: labelled_object_code)
   (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
      (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
        on the_trace:
-         clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (load_code_memory (oc prog)) … start_status) ≝ ?
+         clock … (cm prog) … final_status = (compute_max_trace_any_label_cost prog trace_ends_flag start_status final_status the_trace) + (clock … (cm prog) … start_status) ≝ ?
 and compute_max_trace_label_return_cost_is_ok
   (prog: labelled_object_code)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
     (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
       on the_trace:
-        clock … (load_code_memory (oc prog)) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (load_code_memory (oc prog)) … start_status ≝ ?.
+        clock … (cm prog) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (cm prog) … start_status ≝ ?.
   [1:
     cases the_trace
@@ -127 +127 @@
       >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call
         status_after_fun_call call_trace)
-      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_start_fun_call);
+      cases(is_next) in match (clock … (cm prog) status_start_fun_call);
       >(execute_1_ok_clock … status_pre_fun_call)
       <associative_plus in ⊢ (??%?);
@@ -149 +149 @@
       >(compute_max_trace_any_label_cost_is_ok prog end_flag
          status_init status_end trace_any_label)
-      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_init);
+      cases(is_next) in match (clock … (cm prog) status_init);
       >(execute_1_ok_clock … status_pre)
       >commutative_plus >associative_plus >associative_plus @eq_f
@@ -175 +175 @@
   (prog:labelled_object_code)
    (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
       (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
         start_status final_status) on the_trace: nat ≝
@@ -187 +187 @@
   (prog:labelled_object_code)
   (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
      (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
        on the_trace: nat ≝
@@ -209 +209 @@
 and compute_trace_label_return_cost_using_paid
   (prog:labelled_object_code)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
     (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
       on the_trace: nat ≝
@@ -224 +224 @@
   (prog:labelled_object_code)
    (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
       (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
         start_status final_status) on the_trace:
@@ -233 +233 @@
   (prog:labelled_object_code)
   (trace_ends_flag: trace_ends_with_ret)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
      (the_trace: trace_any_label (OC_abstract_status prog)
       trace_ends_flag start_status final_status) on the_trace:      
@@ -242 +242 @@
 and compute_trace_label_return_cost_using_paid_ok
   (prog:labelled_object_code)
-    (start_status: Status (load_code_memory (oc prog)))
-    (final_status: Status (load_code_memory (oc prog)))
+    (start_status: Status (cm prog))
+    (final_status: Status (cm prog))
     (the_trace: trace_label_return (OC_abstract_status prog)
      start_status final_status) on the_trace:
@@ -454 +454 @@
  (prog: labelled_object_code)
  (cost_map: identifier_map CostTag nat)
- (initial: Status (load_code_memory (oc prog)))
- (final: Status (load_code_memory (oc prog)))
+ (initial: Status (cm prog))
+ (final: Status (cm prog))
  (trace: trace_label_return (OC_abstract_status prog) initial final)
  (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
@@ -470 +470 @@
  (trace_ends_flag: trace_ends_with_ret)
  (cost_map: identifier_map CostTag nat)
- (initial: Status (load_code_memory (oc prog)))
- (final: Status (load_code_memory (oc prog)))
+ (initial: Status (cm prog))
+ (final: Status (cm prog))
  (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
  (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
@@ -486 +486 @@
  (trace_ends_flag: trace_ends_with_ret)
  (cost_map: identifier_map CostTag nat)
- (initial: Status (load_code_memory (oc prog)))
- (final: Status (load_code_memory (oc prog)))
+ (initial: Status (cm prog))
+ (final: Status (cm prog))
  (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
  (unrepeating_witness: tll_unrepeating … trace)
@@ -630 +630 @@
   ∀prog: labelled_object_code.
   ∀cost_map: identifier_map CostTag nat.
-  ∀initial: Status (load_code_memory (oc prog)).
-  ∀final: Status (load_code_memory (oc prog)).
+  ∀initial: Status (cm prog).
+  ∀final: Status (cm prog).
   ∀trace: trace_label_return (OC_abstract_status prog) initial final.
   ∀unrepeating_witness: tlr_unrepeating … trace.
@@ -638 +638 @@
       pi1 … (block_cost prog pc) = lookup_present … k_pres).
         let ctrace ≝ flatten_trace_label_return … trace in
-          clock … (load_code_memory (oc prog)) … final =
-            clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
+          clock … (cm prog) … final =
+            clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
   #prog #cost_map
   #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
@@ -648 +648 @@
 theorem compute_max_trace_label_return_cost_ok_with_trace:
   ∀prog: labelled_object_code.
-  ∀initial: Status (load_code_memory (oc prog)).
-  ∀final: Status (load_code_memory (oc prog)).
+  ∀initial: Status (cm prog).
+  ∀final: Status (cm prog).
   ∀trace: trace_label_return (OC_abstract_status prog) initial final.
   ∀unrepeating_witness: tlr_unrepeating … trace.
     let cost_map ≝ traverse_code prog in
     let ctrace ≝ flatten_trace_label_return … trace in
-      clock … (load_code_memory (oc prog)) … final = clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
+      clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
   [1:
     #prog #initial #final #trace #unrepeating_witness