Changeset 2999 for src/ASM/CostsProof.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2907 r2999  
    1111  (prog: labelled_object_code)
    1212   (trace_ends_flag: trace_ends_with_ret)
    13     (start_status: Status (load_code_memory (oc prog)))
    14     (final_status: Status (load_code_memory (oc prog)))
     13    (start_status: Status (cm prog))
     14    (final_status: Status (cm prog))
    1515      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
     
    2222  (prog: labelled_object_code)
    2323  (trace_ends_flag: trace_ends_with_ret)
    24    (start_status: Status (load_code_memory (oc prog)))
    25    (final_status: Status (load_code_memory (oc prog)))
     24   (start_status: Status (cm prog))
     25   (final_status: Status (cm prog))
    2626     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
     
    5353and compute_max_trace_label_return_cost
    5454  (prog: labelled_object_code)
    55   (start_status: Status (load_code_memory (oc prog)))
    56   (final_status: Status (load_code_memory (oc prog)))
     55  (start_status: Status (cm prog))
     56  (final_status: Status (cm prog))
    5757    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    5858      on the_trace: nat ≝
     
    7070  (prog: labelled_object_code)
    7171   (trace_ends_flag: trace_ends_with_ret)
    72     (start_status: Status (load_code_memory (oc prog)))
    73     (final_status: Status (load_code_memory (oc prog)))
     72    (start_status: Status (cm prog))
     73    (final_status: Status (cm prog))
    7474      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    7575        start_status final_status) on the_trace:
    76           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) ≝ ?
     76          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) ≝ ?
    7777and compute_max_trace_any_label_cost_is_ok
    7878  (prog: labelled_object_code)
    7979  (trace_ends_flag: trace_ends_with_ret)
    80     (start_status: Status (load_code_memory (oc prog)))
    81     (final_status: Status (load_code_memory (oc prog)))
     80    (start_status: Status (cm prog))
     81    (final_status: Status (cm prog))
    8282     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    8383       on the_trace:
    84          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) ≝ ?
     84         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) ≝ ?
    8585and compute_max_trace_label_return_cost_is_ok
    8686  (prog: labelled_object_code)
    87     (start_status: Status (load_code_memory (oc prog)))
    88     (final_status: Status (load_code_memory (oc prog)))
     87    (start_status: Status (cm prog))
     88    (final_status: Status (cm prog))
    8989    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    9090      on the_trace:
    91         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 ≝ ?.
     91        clock … (cm prog) … final_status = (compute_max_trace_label_return_cost prog start_status final_status the_trace) + clock … (cm prog) … start_status ≝ ?.
    9292  [1:
    9393    cases the_trace
     
    127127      >(compute_max_trace_label_return_cost_is_ok prog status_start_fun_call
    128128        status_after_fun_call call_trace)
    129       cases(is_next) in match (clock … (load_code_memory (oc prog)) status_start_fun_call);
     129      cases(is_next) in match (clock … (cm prog) status_start_fun_call);
    130130      >(execute_1_ok_clock … status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
     
    149149      >(compute_max_trace_any_label_cost_is_ok prog end_flag
    150150         status_init status_end trace_any_label)
    151       cases(is_next) in match (clock … (load_code_memory (oc prog)) status_init);
     151      cases(is_next) in match (clock … (cm prog) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    175175  (prog:labelled_object_code)
    176176   (trace_ends_flag: trace_ends_with_ret)
    177     (start_status: Status (load_code_memory (oc prog)))
    178     (final_status: Status (load_code_memory (oc prog)))
     177    (start_status: Status (cm prog))
     178    (final_status: Status (cm prog))
    179179      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    180180        start_status final_status) on the_trace: nat ≝
     
    187187  (prog:labelled_object_code)
    188188  (trace_ends_flag: trace_ends_with_ret)
    189     (start_status: Status (load_code_memory (oc prog)))
    190     (final_status: Status (load_code_memory (oc prog)))
     189    (start_status: Status (cm prog))
     190    (final_status: Status (cm prog))
    191191     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    192192       on the_trace: nat ≝
     
    209209and compute_trace_label_return_cost_using_paid
    210210  (prog:labelled_object_code)
    211     (start_status: Status (load_code_memory (oc prog)))
    212     (final_status: Status (load_code_memory (oc prog)))
     211    (start_status: Status (cm prog))
     212    (final_status: Status (cm prog))
    213213    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    214214      on the_trace: nat ≝
     
    224224  (prog:labelled_object_code)
    225225   (trace_ends_flag: trace_ends_with_ret)
    226     (start_status: Status (load_code_memory (oc prog)))
    227     (final_status: Status (load_code_memory (oc prog)))
     226    (start_status: Status (cm prog))
     227    (final_status: Status (cm prog))
    228228      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    229229        start_status final_status) on the_trace:
     
    233233  (prog:labelled_object_code)
    234234  (trace_ends_flag: trace_ends_with_ret)
    235     (start_status: Status (load_code_memory (oc prog)))
    236     (final_status: Status (load_code_memory (oc prog)))
     235    (start_status: Status (cm prog))
     236    (final_status: Status (cm prog))
    237237     (the_trace: trace_any_label (OC_abstract_status prog)
    238238      trace_ends_flag start_status final_status) on the_trace:     
     
    242242and compute_trace_label_return_cost_using_paid_ok
    243243  (prog:labelled_object_code)
    244     (start_status: Status (load_code_memory (oc prog)))
    245     (final_status: Status (load_code_memory (oc prog)))
     244    (start_status: Status (cm prog))
     245    (final_status: Status (cm prog))
    246246    (the_trace: trace_label_return (OC_abstract_status prog)
    247247     start_status final_status) on the_trace:
     
    454454 (prog: labelled_object_code)
    455455 (cost_map: identifier_map CostTag nat)
    456  (initial: Status (load_code_memory (oc prog)))
    457  (final: Status (load_code_memory (oc prog)))
     456 (initial: Status (cm prog))
     457 (final: Status (cm prog))
    458458 (trace: trace_label_return (OC_abstract_status prog) initial final)
    459459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    470470 (trace_ends_flag: trace_ends_with_ret)
    471471 (cost_map: identifier_map CostTag nat)
    472  (initial: Status (load_code_memory (oc prog)))
    473  (final: Status (load_code_memory (oc prog)))
     472 (initial: Status (cm prog))
     473 (final: Status (cm prog))
    474474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
    475475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     
    486486 (trace_ends_flag: trace_ends_with_ret)
    487487 (cost_map: identifier_map CostTag nat)
    488  (initial: Status (load_code_memory (oc prog)))
    489  (final: Status (load_code_memory (oc prog)))
     488 (initial: Status (cm prog))
     489 (final: Status (cm prog))
    490490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    491491 (unrepeating_witness: tll_unrepeating … trace)
     
    630630  ∀prog: labelled_object_code.
    631631  ∀cost_map: identifier_map CostTag nat.
    632   ∀initial: Status (load_code_memory (oc prog)).
    633   ∀final: Status (load_code_memory (oc prog)).
     632  ∀initial: Status (cm prog).
     633  ∀final: Status (cm prog).
    634634  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    635635  ∀unrepeating_witness: tlr_unrepeating … trace.
     
    638638      pi1 … (block_cost prog pc) = lookup_present … k_pres).
    639639        let ctrace ≝ flatten_trace_label_return … trace in
    640           clock … (load_code_memory (oc prog)) … final =
    641             clock … (load_code_memory (oc prog)) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
     640          clock … (cm prog) … final =
     641            clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i)).
    642642  #prog #cost_map
    643643  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
     
    648648theorem compute_max_trace_label_return_cost_ok_with_trace:
    649649  ∀prog: labelled_object_code.
    650   ∀initial: Status (load_code_memory (oc prog)).
    651   ∀final: Status (load_code_memory (oc prog)).
     650  ∀initial: Status (cm prog).
     651  ∀final: Status (cm prog).
    652652  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    653653  ∀unrepeating_witness: tlr_unrepeating … trace.
    654654    let cost_map ≝ traverse_code prog in
    655655    let ctrace ≝ flatten_trace_label_return … trace in
    656       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)).
     656      clock … (cm prog) … final = clock … (cm prog) … initial + (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map ? ctrace i)).
    657657  [1:
    658658    #prog #initial #final #trace #unrepeating_witness
Note: See TracChangeset for help on using the changeset viewer.