Changeset 2907 for src/ASM/ASMCostsSplit.ma

Timestamp:

Mar 19, 2013, 7:48:19 PM (7 years ago)

Author:

sacerdot

Message:

1. a few bugs fixed
2. as_return implemented for ASM & OC

File:

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

src/ASM/ASMCostsSplit.ma

@@ -6 +6 @@
 
 let rec traverse_code_internal
-  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
+  (prog: labelled_object_code)
     (program_counter: Word) (program_size: nat)
       (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
         on program_size:
           Σcost_map: identifier_map CostTag nat.
-            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
-            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
-               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
+            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k) ∧
+            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc (costlabels prog) = Some … k ∧
+               pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
   match program_size return λx. x = program_size → Σcost_map: ?. ? with
   [ O ⇒ λprogram_size_refl. empty_map CostTag nat
   | S program_size' ⇒ λprogram_size_refl.
     let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
-    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
-    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
+    let cost_mapping ≝ traverse_code_internal prog new_program_counter' program_size' ? in
+    match lookup_opt … program_counter (costlabels prog)
+    return λx. x = lookup_opt … program_counter (costlabels prog) → Σcost_map: ?. ? with
     [ None ⇒ λlookup_refl. pi1 … cost_mapping
     | Some lbl ⇒ λlookup_refl.
-      let cost ≝ block_cost code_memory program_counter cost_labels in
+      let cost ≝ block_cost prog program_counter in
         cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
-    ] (refl … (lookup_opt … program_counter cost_labels))
+    ] (refl … (lookup_opt … program_counter (costlabels prog)))
   ] (refl … program_size).
   [3:
@@ -279 +280 @@
  *)
 definition traverse_code:
-  ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
-  ∀cost_labels_injective:
-    ∀pc, pc',l.
-      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
-        pc = pc'.
+  ∀prog: labelled_object_code.
+   let cost_labels ≝ costlabels prog in
     Σcost_map: identifier_map CostTag nat.
       (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
       (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
-          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
-  λcode_memory: BitVectorTrie Byte 16.
-  λcost_labels: BitVectorTrie costlabel 16.
-  λcost_labels_injective.
-    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
+          pi1 … (block_cost prog pc) = lookup_present … k_pres) ≝
+  λprog.
+    pi1 ? ? (traverse_code_internal prog (zero …) (2^16) ?).
   [1:
     @or_intror %
   |2:
-    cases (traverse_code_internal ?????)
+    cases (traverse_code_internal ???)
     #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
     [1:
@@ -311 +306 @@
       cases (inductive_hypothesis2 ? k_pres)
       #program_counter' * #lookup_opt_assm' #block_cost_assm
-      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
+      >(oc_injective_costlabels … lookup_opt_assm lookup_opt_assm')
       assumption
     ]
@@ -317 +312 @@
 qed.
     
-definition compute_costs ≝
-  λprogram: object_code.
-  λcost_labels: BitVectorTrie costlabel 16.
-  λcost_labels_injective:
-    ∀pc, pc',l.
-      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
-        pc = pc'.
-    (* let program_size ≝ |program| in *)
-    let code_memory ≝ load_code_memory program in
-      traverse_code code_memory cost_labels cost_labels_injective.
+definition compute_costs ≝ traverse_code.
 
 definition ASM_cost_map :
   ∀p: labelled_object_code.
   let code_memory ≝ load_code_memory (oc p) in
-  let a_s ≝ OC_abstract_status code_memory (costlabels p) in 
+  let a_s ≝ OC_abstract_status p in 
   as_cost_map a_s ≝
   λp.
-  let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p) in
+  let cost_map ≝ compute_costs p in
   λl_sig.
   lookup_present … cost_map (as_cost_get_label ? l_sig) ?.