Changeset 2516 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Dec 2, 2012, 5:45:36 PM (7 years ago)
Author:
mckinna
Message:

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2498 r2516  
    1010let rec compute_max_trace_label_label_cost
    1111  (cm: ?)
    12   (cost_labels: costlabel_map)
     12  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     23  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     51  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     67  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     75  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     83  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     166  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     178  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     199  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     213  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     222  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     232  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     273  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     290  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     311  (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     388 ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     449 ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map)
     503 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     517 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map)
     532 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
    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: costlabel_map.
     651  ∀cost_labels: BitVectorTrie costlabel 16.
    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: costlabel_map.
     671  ∀cost_labels: BitVectorTrie costlabel 16.
    672672  ∀cost_labels_injective:
    673673   (∀pc,pc',l.
     
    697697 
    698698include "utilities/permutations.ma".
    699 (*
    700 lemma 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 ]
    720 qed.
    721 *)
     699
    722700lemma tech_cost_sum_eq_as_cost :
    723701  ∀code_memory: BitVectorTrie Byte 16.
    724   ∀cost_labels: costlabel_map.
     702  ∀cost_labels: BitVectorTrie costlabel 16.
    725703  ∀cost_map: identifier_map CostTag nat.
    726704  ∀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.