Changeset 2498 for src/ASM/CostsProof.ma


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

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2057 r2498  
    1010let rec compute_max_trace_label_label_cost
    1111  (cm: ?)
    12   (cost_labels: BitVectorTrie costlabel 16)
     12  (cost_labels: costlabel_map)
    1313   (trace_ends_flag: trace_ends_with_ret)
    1414    (start_status: Status cm) (final_status: Status cm)
     
    2121and compute_max_trace_any_label_cost
    2222  (cm: ?)
    23   (cost_labels: BitVectorTrie costlabel 16)
     23  (cost_labels: costlabel_map)
    2424  (trace_ends_flag: trace_ends_with_ret)
    2525   (start_status: Status cm) (final_status: Status cm)
     
    4949and compute_max_trace_label_return_cost
    5050  (cm: ?)
    51   (cost_labels: BitVectorTrie costlabel 16)
     51  (cost_labels: costlabel_map)
    5252  (start_status: Status cm) (final_status: Status cm)
    5353    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    6565let rec compute_max_trace_label_label_cost_is_ok
    6666  (cm: ?)
    67   (cost_labels: BitVectorTrie costlabel 16)
     67  (cost_labels: costlabel_map)
    6868   (trace_ends_flag: trace_ends_with_ret)
    6969    (start_status: Status cm) (final_status: Status cm)
     
    7373and compute_max_trace_any_label_cost_is_ok
    7474  (cm: ?)
    75   (cost_labels: BitVectorTrie costlabel 16)
     75  (cost_labels: costlabel_map)
    7676  (trace_ends_flag: trace_ends_with_ret)
    7777   (start_status: Status cm) (final_status: Status cm)
     
    8181and compute_max_trace_label_return_cost_is_ok
    8282  (cm: ?)
    83   (cost_labels: BitVectorTrie costlabel 16)
     83  (cost_labels: costlabel_map)
    8484  (start_status: Status cm) (final_status: Status cm)
    8585    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    164164let rec compute_trace_label_label_cost_using_paid
    165165  (cm: ?)
    166   (cost_labels: BitVectorTrie costlabel 16)
     166  (cost_labels: costlabel_map)
    167167   (trace_ends_flag: trace_ends_with_ret)
    168168    (start_status: Status cm) (final_status: Status cm)
     
    176176and compute_trace_any_label_cost_using_paid
    177177  (cm: ?)
    178   (cost_labels: BitVectorTrie costlabel 16)
     178  (cost_labels: costlabel_map)
    179179  (trace_ends_flag: trace_ends_with_ret)
    180180   (start_status: Status cm) (final_status: Status cm)
     
    197197and compute_trace_label_return_cost_using_paid
    198198  (cm: ?)
    199   (cost_labels: BitVectorTrie costlabel 16)
     199  (cost_labels: costlabel_map)
    200200  (start_status: Status cm) (final_status: Status cm)
    201201    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    211211let rec compute_trace_label_label_cost_using_paid_ok
    212212  (cm: ?)
    213   (cost_labels: BitVectorTrie costlabel 16)
     213  (cost_labels: costlabel_map)
    214214   (trace_ends_flag: trace_ends_with_ret)
    215215    (start_status: Status cm) (final_status: Status cm)
     
    220220and compute_trace_any_label_cost_using_paid_ok
    221221  (cm: ?)
    222   (cost_labels: BitVectorTrie costlabel 16)
     222  (cost_labels: costlabel_map)
    223223  (trace_ends_flag: trace_ends_with_ret)
    224224   (start_status: Status cm) (final_status: Status cm)
     
    230230and compute_trace_label_return_cost_using_paid_ok
    231231  (cm: ?)
    232   (cost_labels: BitVectorTrie costlabel 16)
     232  (cost_labels: costlabel_map)
    233233  (start_status: Status cm) (final_status: Status cm)
    234234    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels)
     
    271271let rec compute_cost_trace_label_label
    272272  (cm: BitVectorTrie Byte 16)
    273   (cost_labels: BitVectorTrie costlabel 16)
     273  (cost_labels: costlabel_map)
    274274   (trace_ends_flag: trace_ends_with_ret)
    275275    (start_status: Status cm) (final_status: Status cm)
     
    288288and compute_cost_trace_any_label
    289289  (cm: BitVectorTrie Byte 16)
    290   (cost_labels: BitVectorTrie costlabel 16)
     290  (cost_labels: costlabel_map)
    291291  (trace_ends_flag: trace_ends_with_ret)
    292292   (start_status: Status cm) (final_status: Status cm)
     
    309309and compute_cost_trace_label_return
    310310  (cm: BitVectorTrie Byte 16)
    311   (cost_labels: BitVectorTrie costlabel 16)
     311  (cost_labels: costlabel_map)
    312312  (start_status: Status cm) (final_status: Status cm)
    313313    (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
     
    386386
    387387definition tech_cost_of_label0:
    388  ∀cost_labels: BitVectorTrie costlabel 16.
     388 ∀cost_labels: costlabel_map.
    389389 ∀cost_map: identifier_map CostTag nat.
    390390 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    447447
    448448definition tech_cost_of_label:
    449  ∀cost_labels: BitVectorTrie costlabel 16.
     449 ∀cost_labels: costlabel_map.
    450450 ∀cost_map: identifier_map CostTag nat.
    451451 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     
    501501   
    502502let rec compute_trace_label_return_using_paid_ok_with_trace
    503  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     503 (cm: ?) (cost_labels: costlabel_map)
    504504 (cost_map: identifier_map CostTag nat)
    505505 (initial: Status cm) (final: Status cm)
     
    515515    ≝ ?
    516516and compute_trace_any_label_using_paid_ok_with_trace
    517  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     517 (cm: ?) (cost_labels: costlabel_map)
    518518 (trace_ends_flag: trace_ends_with_ret)
    519519 (cost_map: identifier_map CostTag nat)
     
    530530    ≝ ?
    531531and compute_trace_label_label_using_paid_ok_with_trace
    532  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     532 (cm: ?) (cost_labels: costlabel_map)
    533533 (trace_ends_flag: trace_ends_with_ret)
    534534 (cost_map: identifier_map CostTag nat)
     
    649649lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    650650  ∀code_memory: BitVectorTrie Byte 16.
    651   ∀cost_labels: BitVectorTrie costlabel 16.
     651  ∀cost_labels: costlabel_map.
    652652  ∀cost_map: identifier_map CostTag nat.
    653653  ∀initial: Status code_memory.
     
    669669theorem compute_max_trace_label_return_cost_ok_with_trace:
    670670  ∀code_memory: BitVectorTrie Byte 16.
    671   ∀cost_labels: BitVectorTrie costlabel 16.
     671  ∀cost_labels: costlabel_map.
    672672  ∀cost_labels_injective:
    673673   (∀pc,pc',l.
     
    697697 
    698698include "utilities/permutations.ma".
    699 
     699(*
     700lemma tech_cost_sum_eq_as_cost :
     701  ∀code_memory: object_code.
     702  ∀cost_labels: costlabel_map.
     703  ∀cost_map: identifier_map CostTag nat.
     704  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     705  ∀trace.
     706  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
     707  (Σ_{l ∈ trace}(ASM_cost_map 〈code_memory, cost_labels〉 … codom_dom l)).
     708#cmem #clab #cmap #codom_dom #trace
     709@(list_elim_left … trace)
     710[ %
     711| #tl #hd #IH >append_length >commutative_plus
     712  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
     713  whd in ⊢ (??%%); <IH
     714  <tech_cost_of_label_shift [2: %]
     715  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
     716  [ %
     717  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
     718  ]
     719]
     720qed.
     721*)
    700722lemma tech_cost_sum_eq_as_cost :
    701723  ∀code_memory: BitVectorTrie Byte 16.
    702   ∀cost_labels: BitVectorTrie costlabel 16.
     724  ∀cost_labels: costlabel_map.
    703725  ∀cost_map: identifier_map CostTag nat.
    704726  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
Note: See TracChangeset for help on using the changeset viewer.