Changeset 2899 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (7 years ago)
Author:
sacerdot
Message:
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2760 r2899  
    1313   (trace_ends_flag: trace_ends_with_ret)
    1414    (start_status: Status cm) (final_status: Status cm)
    15       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     15      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
    1717  match the_trace with
     
    2424  (trace_ends_flag: trace_ends_with_ret)
    2525   (start_status: Status cm) (final_status: Status cm)
    26      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     26     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
    2828  match the_trace with
     
    5555  (cost_labels: BitVectorTrie costlabel 16)
    5656  (start_status: Status cm) (final_status: Status cm)
    57     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     57    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    5858      on the_trace: nat ≝
    5959  match the_trace with
     
    7272   (trace_ends_flag: trace_ends_with_ret)
    7373    (start_status: Status cm) (final_status: Status cm)
    74       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     74      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    7575        start_status final_status) on the_trace:
    7676          clock … cm … final_status = (compute_max_trace_label_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     
    8080  (trace_ends_flag: trace_ends_with_ret)
    8181   (start_status: Status cm) (final_status: Status cm)
    82      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     82     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    8383       on the_trace:
    8484         clock … cm … final_status = (compute_max_trace_any_label_cost cm cost_labels trace_ends_flag start_status final_status the_trace) + (clock … cm … start_status) ≝ ?
     
    8787  (cost_labels: BitVectorTrie costlabel 16)
    8888  (start_status: Status cm) (final_status: Status cm)
    89     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     89    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    9090      on the_trace:
    9191        clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?.
     
    178178   (trace_ends_flag: trace_ends_with_ret)
    179179    (start_status: Status cm) (final_status: Status cm)
    180       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     180      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    181181        start_status final_status) on the_trace: nat ≝
    182182  match the_trace with
     
    190190  (trace_ends_flag: trace_ends_with_ret)
    191191   (start_status: Status cm) (final_status: Status cm)
    192      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     192     (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    193193       on the_trace: nat ≝
    194194  match the_trace with
     
    212212  (cost_labels: BitVectorTrie costlabel 16)
    213213  (start_status: Status cm) (final_status: Status cm)
    214     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     214    (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
    215215      on the_trace: nat ≝
    216216  match the_trace with
     
    227227   (trace_ends_flag: trace_ends_with_ret)
    228228    (start_status: Status cm) (final_status: Status cm)
    229       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
     229      (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
    230230        start_status final_status) on the_trace:
    231231 compute_trace_label_label_cost_using_paid cm cost_labels … the_trace =
     
    236236  (trace_ends_flag: trace_ends_with_ret)
    237237   (start_status: Status cm) (final_status: Status cm)
    238      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels)
     238     (the_trace: trace_any_label (OC_abstract_status cm cost_labels)
    239239      trace_ends_flag start_status final_status) on the_trace:     
    240240  compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace
     
    245245  (cost_labels: BitVectorTrie costlabel 16)
    246246  (start_status: Status cm) (final_status: Status cm)
    247     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
     247    (the_trace: trace_label_return (OC_abstract_status cm cost_labels)
    248248     start_status final_status) on the_trace:
    249249 compute_trace_label_return_cost_using_paid cm cost_labels … the_trace =
     
    456456 (cost_map: identifier_map CostTag nat)
    457457 (initial: Status cm) (final: Status cm)
    458  (trace: trace_label_return (ASM_abstract_status cm cost_labels) initial final)
     458 (trace: trace_label_return (OC_abstract_status cm cost_labels) initial final)
    459459 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    460460 on trace:
     
    462462 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    463463   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    464   let ctrace ≝ flatten_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
     464  let ctrace ≝ flatten_trace_label_return (OC_abstract_status cm cost_labels) … trace in
    465465  compute_trace_label_return_cost_using_paid cm … trace =
    466466   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    471471 (cost_map: identifier_map CostTag nat)
    472472 (initial: Status cm) (final: Status cm)
    473  (trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     473 (trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    474474 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    475475 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
     
    477477 on trace:
    478478  ∀unrepeating_witness: tal_unrepeating … trace.
    479   let ctrace ≝ flatten_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
     479  let ctrace ≝ flatten_trace_any_label (OC_abstract_status cm cost_labels) … trace_ends_flag … trace in
    480480  compute_trace_any_label_cost_using_paid … trace =
    481481   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    486486 (cost_map: identifier_map CostTag nat)
    487487 (initial: Status cm) (final: Status cm)
    488  (trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag initial final)
     488 (trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    489489 (unrepeating_witness: tll_unrepeating … trace)
    490490 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     
    493493 on trace:
    494494 ∀unrepeating_witness: tll_unrepeating … trace.
    495   let ctrace ≝ flatten_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
     495  let ctrace ≝ flatten_trace_label_label (OC_abstract_status cm cost_labels) … trace in
    496496  compute_trace_label_label_cost_using_paid … trace =
    497497   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     
    631631  ∀initial: Status code_memory.
    632632  ∀final: Status code_memory.
    633   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     633  ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
    634634  ∀unrepeating_witness: tlr_unrepeating … trace.
    635635  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    654654  ∀initial: Status code_memory.
    655655  ∀final: Status code_memory.
    656   ∀trace: trace_label_return (ASM_abstract_status code_memory cost_labels) initial final.
     656  ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
    657657  ∀unrepeating_witness: tlr_unrepeating … trace.
    658658    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
     
    687687  =
    688688   lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective)
    689    (as_cost_get_label (ASM_abstract_status (load_code_memory ccode1) ccode2)
     689   (as_cost_get_label (OC_abstract_status (load_code_memory ccode1) ccode2)
    690690    «tl,Htl») PRF2.
    691691//
Note: See TracChangeset for help on using the changeset viewer.