Changeset 2907 for src/ASM/CostsProof.ma


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

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2899 r2907  
    99
    1010let rec compute_max_trace_label_label_cost
    11   (cm: ?)
    12   (cost_labels: BitVectorTrie costlabel 16)
     11  (prog: labelled_object_code)
    1312   (trace_ends_flag: trace_ends_with_ret)
    14     (start_status: Status cm) (final_status: Status cm)
    15       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     13    (start_status: Status (load_code_memory (oc prog)))
     14    (final_status: Status (load_code_memory (oc prog)))
     15      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    1616        start_status final_status) on the_trace: nat ≝
    1717  match the_trace with
     
    2020  ]
    2121and compute_max_trace_any_label_cost
    22   (cm: ?)
    23   (cost_labels: BitVectorTrie costlabel 16)
     22  (prog: labelled_object_code)
    2423  (trace_ends_flag: trace_ends_with_ret)
    25    (start_status: Status cm) (final_status: Status cm)
    26      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     24   (start_status: Status (load_code_memory (oc prog)))
     25   (final_status: Status (load_code_memory (oc prog)))
     26     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    2727       on the_trace: nat ≝
    2828  match the_trace with
    29   [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost cm the_status
    30   | tal_base_return the_status _ _ _ ⇒ current_instruction_cost cm the_status
     29  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost the_status
     30  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost the_status
    3131  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    32       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     32      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    3333      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    3434        call_trace_cost + current_instruction_cost
    3535  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    36       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     36      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    3737      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    3838        call_trace_cost + current_instruction_cost
    3939  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    4040     _ _ _ call_trace _ final_trace ⇒
    41       let current_instruction_cost ≝ current_instruction_cost cm pre_fun_call in
     41      let current_instruction_cost ≝ current_instruction_cost pre_fun_call in
    4242      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
    43       let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
     43      let final_trace_cost ≝ compute_max_trace_any_label_cost prog end_flag … final_trace in
    4444        call_trace_cost + current_instruction_cost + final_trace_cost
    4545  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    46       let current_instruction_cost ≝ current_instruction_cost cm status_pre in
     46      let current_instruction_cost ≝ current_instruction_cost status_pre in
    4747      let tail_trace_cost ≝
    48        compute_max_trace_any_label_cost cm cost_labels end_flag
     48       compute_max_trace_any_label_cost prog end_flag
    4949        status_init status_end tail_trace
    5050      in
     
    5252  ]
    5353and compute_max_trace_label_return_cost
    54   (cm: ?)
    55   (cost_labels: BitVectorTrie costlabel 16)
    56   (start_status: Status cm) (final_status: Status cm)
    57     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     54  (prog: labelled_object_code)
     55  (start_status: Status (load_code_memory (oc prog)))
     56  (final_status: Status (load_code_memory (oc prog)))
     57    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    5858      on the_trace: nat ≝
    5959  match the_trace with
     
    6868
    6969let rec compute_max_trace_label_label_cost_is_ok
    70   (cm: ?)
    71   (cost_labels: BitVectorTrie costlabel 16)
     70  (prog: labelled_object_code)
    7271   (trace_ends_flag: trace_ends_with_ret)
    73     (start_status: Status cm) (final_status: Status cm)
    74       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     72    (start_status: Status (load_code_memory (oc prog)))
     73    (final_status: Status (load_code_memory (oc prog)))
     74      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    7575        start_status final_status) on the_trace:
    76           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) ≝ ?
     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) ≝ ?
    7777and compute_max_trace_any_label_cost_is_ok
    78   (cm: ?)
    79   (cost_labels: BitVectorTrie costlabel 16)
     78  (prog: labelled_object_code)
    8079  (trace_ends_flag: trace_ends_with_ret)
    81    (start_status: Status cm) (final_status: Status cm)
    82      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     80    (start_status: Status (load_code_memory (oc prog)))
     81    (final_status: Status (load_code_memory (oc prog)))
     82     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    8383       on the_trace:
    84          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) ≝ ?
     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) ≝ ?
    8585and compute_max_trace_label_return_cost_is_ok
    86   (cm: ?)
    87   (cost_labels: BitVectorTrie costlabel 16)
    88   (start_status: Status cm) (final_status: Status cm)
    89     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     86  (prog: labelled_object_code)
     87    (start_status: Status (load_code_memory (oc prog)))
     88    (final_status: Status (load_code_memory (oc prog)))
     89    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    9090      on the_trace:
    91         clock … cm … final_status = (compute_max_trace_label_return_cost cm cost_labels start_status final_status the_trace) + clock … cm … start_status ≝ ?.
     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 ≝ ?.
    9292  [1:
    9393    cases the_trace
    9494    #ends_flag #start_status #end_status #any_label_trace #is_costed
    95     normalize @compute_max_trace_any_label_cost_is_ok
     95    @compute_max_trace_any_label_cost_is_ok
    9696  |2:
    9797    cases the_trace
    9898    [1,2:
    9999      #start_status #final_status #is_next #is_not_return try (#is_costed)
    100       change with (current_instruction_cost cm start_status) in ⊢ (???(?%?));
     100      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
    101101      cases(is_next) @execute_1_ok_clock
    102102    |3:
     
    104104      #classifier_assm #after_return_assm #call_trace #costed_assm
    105105      whd in match (compute_max_trace_any_label_cost … (tal_base_call …));
    106       >(compute_max_trace_label_return_cost_is_ok … call_trace)
     106      >(compute_max_trace_label_return_cost_is_ok prog … call_trace)
    107107      >associative_plus @eq_f cases(is_next)
    108108      @execute_1_ok_clock
     
    118118      #status_final #is_next #is_call #is_after_return #call_trace #not_costed #final_trace
    119119      change with (
    120       let current_instruction_cost ≝ current_instruction_cost cm status_pre_fun_call in
    121       let call_trace_cost ≝ compute_max_trace_label_return_cost cm … call_trace in
    122       let final_trace_cost ≝ compute_max_trace_any_label_cost cm cost_labels end_flag … final_trace in
     120      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
     121      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
     122      let final_trace_cost ≝ compute_max_trace_any_label_cost prog end_flag … final_trace in
    123123        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
    124124      normalize nodelta;
    125       >(compute_max_trace_any_label_cost_is_ok … cost_labels end_flag status_after_fun_call
     125      >(compute_max_trace_any_label_cost_is_ok prog end_flag status_after_fun_call
    126126          status_final final_trace)
    127       >(compute_max_trace_label_return_cost_is_ok … cost_labels status_start_fun_call
     127      >(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 … cm status_start_fun_call);
    130       >(execute_1_ok_clock cm status_pre_fun_call)
     129      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_start_fun_call);
     130      >(execute_1_ok_clock status_pre_fun_call)
    131131      <associative_plus in ⊢ (??%?);
    132132      <commutative_plus in match (
    133         compute_max_trace_any_label_cost cm cost_labels end_flag status_after_fun_call status_final final_trace
    134           + compute_max_trace_label_return_cost cm cost_labels status_start_fun_call status_after_fun_call call_trace);
     133        compute_max_trace_any_label_cost prog end_flag status_after_fun_call status_final final_trace
     134          + compute_max_trace_label_return_cost prog status_start_fun_call status_after_fun_call call_trace);
    135135      >associative_plus in ⊢ (??%?); >associative_plus in ⊢ (???%); >associative_plus in ⊢ (???%);
    136136      @eq_f >commutative_plus in ⊢ (??%?); >associative_plus in ⊢ (??%?);
    137       @eq_f @commutative_plus 
     137      @eq_f @commutative_plus
    138138    |6:
    139139      #end_flag #status_pre #status_init #status_end #is_next
    140140      #trace_any_label #is_other #is_not_costed
    141141      change with (
    142       let current_instruction_cost ≝ current_instruction_cost cm status_pre in
     142      let current_instruction_cost ≝ current_instruction_cost status_pre in
    143143      let tail_trace_cost ≝
    144        compute_max_trace_any_label_cost cm cost_labels end_flag
     144       compute_max_trace_any_label_cost prog end_flag
    145145        status_init status_end trace_any_label
    146146      in
    147147        current_instruction_cost + tail_trace_cost) in ⊢ (???(?%?));
    148148      normalize nodelta;
    149       >(compute_max_trace_any_label_cost_is_ok cm cost_labels end_flag
     149      >(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 … cm status_init);
     151      cases(is_next) in match (clock … (load_code_memory (oc prog)) status_init);
    152152      >(execute_1_ok_clock … status_pre)
    153153      >commutative_plus >associative_plus >associative_plus @eq_f
     
    158158    [1:
    159159      #status_before #status_after #trace_to_lift
    160       normalize @compute_max_trace_label_label_cost_is_ok
     160      @compute_max_trace_label_label_cost_is_ok
    161161    |2:
    162162      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
    163       normalize
    164       >(compute_max_trace_label_return_cost_is_ok cm cost_labels status_labelled status_final ret_trace);
    165       >(compute_max_trace_label_label_cost_is_ok cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     163      >(compute_max_trace_label_return_cost_is_ok prog status_labelled status_final ret_trace);
     164      >(compute_max_trace_label_label_cost_is_ok prog doesnt_end_with_ret status_initial status_labelled labelled_trace);
    166165      <associative_plus in ⊢ (??%?);
    167166      >commutative_plus in match (
    168         compute_max_trace_label_return_cost cm cost_labels status_labelled status_final ret_trace
    169           + compute_max_trace_label_label_cost cm cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
     167        compute_max_trace_label_return_cost prog status_labelled status_final ret_trace
     168          + compute_max_trace_label_label_cost prog doesnt_end_with_ret status_initial status_labelled labelled_trace);
    170169      %
    171170    ]
     
    174173
    175174let rec compute_trace_label_label_cost_using_paid
    176   (cm: ?)
    177   (cost_labels: BitVectorTrie costlabel 16)
     175  (prog:labelled_object_code)
    178176   (trace_ends_flag: trace_ends_with_ret)
    179     (start_status: Status cm) (final_status: Status cm)
    180       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     177    (start_status: Status (load_code_memory (oc prog)))
     178    (final_status: Status (load_code_memory (oc prog)))
     179      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    181180        start_status final_status) on the_trace: nat ≝
    182181  match the_trace with
    183182  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    184       compute_paid_trace_label_label cm cost_labels … the_trace +
     183      compute_paid_trace_label_label prog … the_trace +
    185184      compute_trace_any_label_cost_using_paid … given_trace
    186185  ]
    187186and compute_trace_any_label_cost_using_paid
    188   (cm: ?)
    189   (cost_labels: BitVectorTrie costlabel 16)
     187  (prog:labelled_object_code)
    190188  (trace_ends_flag: trace_ends_with_ret)
    191    (start_status: Status cm) (final_status: Status cm)
    192      (the_trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
     189    (start_status: Status (load_code_memory (oc prog)))
     190    (final_status: Status (load_code_memory (oc prog)))
     191     (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    193192       on the_trace: nat ≝
    194193  match the_trace with
     
    202201     _ _ _ call_trace _ final_trace ⇒
    203202      let call_trace_cost ≝ compute_trace_label_return_cost_using_paid … call_trace in
    204       let final_trace_cost ≝ compute_trace_any_label_cost_using_paid cm cost_labels end_flag … final_trace in
     203      let final_trace_cost ≝ compute_trace_any_label_cost_using_paid prog end_flag … final_trace in
    205204        call_trace_cost + final_trace_cost
    206205  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    207      compute_trace_any_label_cost_using_paid cm cost_labels end_flag
     206     compute_trace_any_label_cost_using_paid prog end_flag
    208207      status_init status_end tail_trace
    209208  ]
    210209and compute_trace_label_return_cost_using_paid
    211   (cm: ?)
    212   (cost_labels: BitVectorTrie costlabel 16)
    213   (start_status: Status cm) (final_status: Status cm)
    214     (the_trace: trace_label_return (OC_abstract_status cm cost_labels) start_status final_status)
     210  (prog:labelled_object_code)
     211    (start_status: Status (load_code_memory (oc prog)))
     212    (final_status: Status (load_code_memory (oc prog)))
     213    (the_trace: trace_label_return (OC_abstract_status prog) start_status final_status)
    215214      on the_trace: nat ≝
    216215  match the_trace with
     
    223222
    224223let rec compute_trace_label_label_cost_using_paid_ok
    225   (cm: ?)
    226   (cost_labels: BitVectorTrie costlabel 16)
     224  (prog:labelled_object_code)
    227225   (trace_ends_flag: trace_ends_with_ret)
    228     (start_status: Status cm) (final_status: Status cm)
    229       (the_trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag
     226    (start_status: Status (load_code_memory (oc prog)))
     227    (final_status: Status (load_code_memory (oc prog)))
     228      (the_trace: trace_label_label (OC_abstract_status prog) trace_ends_flag
    230229        start_status final_status) on the_trace:
    231  compute_trace_label_label_cost_using_paid cm cost_labels … the_trace =
     230 compute_trace_label_label_cost_using_paid prog … the_trace =
    232231 compute_max_trace_label_label_cost … the_trace ≝ ?
    233232and compute_trace_any_label_cost_using_paid_ok
    234   (cm: ?)
    235   (cost_labels: BitVectorTrie costlabel 16)
     233  (prog:labelled_object_code)
    236234  (trace_ends_flag: trace_ends_with_ret)
    237    (start_status: Status cm) (final_status: Status cm)
    238      (the_trace: trace_any_label (OC_abstract_status cm cost_labels)
     235    (start_status: Status (load_code_memory (oc prog)))
     236    (final_status: Status (load_code_memory (oc prog)))
     237     (the_trace: trace_any_label (OC_abstract_status prog)
    239238      trace_ends_flag start_status final_status) on the_trace:     
    240   compute_paid_trace_any_label cm cost_labels trace_ends_flag … the_trace
    241   +compute_trace_any_label_cost_using_paid cm cost_labels trace_ends_flag … the_trace
    242   =compute_max_trace_any_label_cost cm cost_labels trace_ends_flag … the_trace ≝ ?
     239  compute_paid_trace_any_label prog trace_ends_flag … the_trace
     240  +compute_trace_any_label_cost_using_paid prog trace_ends_flag … the_trace
     241  =compute_max_trace_any_label_cost prog trace_ends_flag … the_trace ≝ ?
    243242and compute_trace_label_return_cost_using_paid_ok
    244   (cm: ?)
    245   (cost_labels: BitVectorTrie costlabel 16)
    246   (start_status: Status cm) (final_status: Status cm)
    247     (the_trace: trace_label_return (OC_abstract_status cm cost_labels)
     243  (prog:labelled_object_code)
     244    (start_status: Status (load_code_memory (oc prog)))
     245    (final_status: Status (load_code_memory (oc prog)))
     246    (the_trace: trace_label_return (OC_abstract_status prog)
    248247     start_status final_status) on the_trace:
    249  compute_trace_label_return_cost_using_paid cm cost_labels … the_trace =
    250  compute_max_trace_label_return_cost cm cost_labels … the_trace ≝ ?.
     248 compute_trace_label_return_cost_using_paid prog … the_trace =
     249 compute_max_trace_label_return_cost prog … the_trace ≝ ?.
    251250[ cases the_trace #endsf #ss #es #tr #H normalize
    252251  @compute_trace_any_label_cost_using_paid_ok
     
    453452
    454453let rec compute_trace_label_return_using_paid_ok_with_trace
    455  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     454 (prog: labelled_object_code)
    456455 (cost_map: identifier_map CostTag nat)
    457  (initial: Status cm) (final: Status cm)
    458  (trace: trace_label_return (OC_abstract_status cm cost_labels) initial final)
    459  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     456 (initial: Status (load_code_memory (oc prog)))
     457 (final: Status (load_code_memory (oc prog)))
     458 (trace: trace_label_return (OC_abstract_status prog) initial final)
     459 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
    460460 on trace:
    461461 ∀unrepeating_witness: tlr_unrepeating … trace.
    462  ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    463    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    464   let ctrace ≝ flatten_trace_label_return (OC_abstract_status cm cost_labels) … trace in
    465   compute_trace_label_return_cost_using_paid cm … trace =
    466    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     462 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     463   pi1 … (block_cost prog pc) = lookup_present … k_pres).
     464  let ctrace ≝ flatten_trace_label_return (OC_abstract_status prog) … trace in
     465  compute_trace_label_return_cost_using_paid prog … trace =
     466   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    467467    ≝ ?
    468468and compute_trace_any_label_using_paid_ok_with_trace
    469  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     469 (prog: labelled_object_code)
    470470 (trace_ends_flag: trace_ends_with_ret)
    471471 (cost_map: identifier_map CostTag nat)
    472  (initial: Status cm) (final: Status cm)
    473  (trace: trace_any_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
    474  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    475  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    476    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
     472 (initial: Status (load_code_memory (oc prog)))
     473 (final: Status (load_code_memory (oc prog)))
     474 (trace: trace_any_label (OC_abstract_status prog) trace_ends_flag initial final)
     475 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     476 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     477   pi1 … (block_cost prog pc) = lookup_present … k_pres))
    477478 on trace:
    478479  ∀unrepeating_witness: tal_unrepeating … trace.
    479   let ctrace ≝ flatten_trace_any_label (OC_abstract_status cm cost_labels) … trace_ends_flag … trace in
     480  let ctrace ≝ flatten_trace_any_label (OC_abstract_status prog) … trace_ends_flag … trace in
    480481  compute_trace_any_label_cost_using_paid … trace =
    481    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     482   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    482483    ≝ ?
    483484and compute_trace_label_label_using_paid_ok_with_trace
    484  (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     485 (prog: labelled_object_code)
    485486 (trace_ends_flag: trace_ends_with_ret)
    486487 (cost_map: identifier_map CostTag nat)
    487  (initial: Status cm) (final: Status cm)
    488  (trace: trace_label_label (OC_abstract_status cm cost_labels) trace_ends_flag initial final)
     488 (initial: Status (load_code_memory (oc prog)))
     489 (final: Status (load_code_memory (oc prog)))
     490 (trace: trace_label_label (OC_abstract_status prog) trace_ends_flag initial final)
    489491 (unrepeating_witness: tll_unrepeating … trace)
    490  (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    491  (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    492    pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres))
     492 (codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k))
     493 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     494   pi1 … (block_cost prog pc) = lookup_present … k_pres))
    493495 on trace:
    494496 ∀unrepeating_witness: tll_unrepeating … trace.
    495   let ctrace ≝ flatten_trace_label_label (OC_abstract_status cm cost_labels) … trace in
     497  let ctrace ≝ flatten_trace_label_label (OC_abstract_status prog) … trace in
    496498  compute_trace_label_label_cost_using_paid … trace =
    497    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     499   (Σ_{i < |ctrace|} (tech_cost_of_label (costlabels prog) cost_map codom_dom ctrace i))
    498500    ≝ ?.
    499501  cases trace normalize nodelta
     
    541543        whd in ⊢ (∀p:????%.???(????%?));
    542544        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
    543         inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels)
     545        inversion (lookup_opt ? ? (program_counter … start_status) (costlabels prog))
    544546        [1:
    545547          #_ #absurd @⊥ cases absurd #absurd @absurd %
     
    547549          normalize nodelta #cost_label #Some_assm #_ #p
    548550          cases (dom_codom ? p ? Some_assm)
    549           cases (block_cost ???)
     551          cases (block_cost ??)
    550552          #cost #block_cost_assm
    551553          cases (block_cost_assm ??? trace_any_label ??)
     
    626628 
    627629lemma compute_max_trace_label_return_cost_ok_with_trace_aux:
    628   ∀code_memory: BitVectorTrie Byte 16.
    629   ∀cost_labels: BitVectorTrie costlabel 16.
     630  ∀prog: labelled_object_code.
    630631  ∀cost_map: identifier_map CostTag nat.
    631   ∀initial: Status code_memory.
    632   ∀final: Status code_memory.
    633   ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
     632  ∀initial: Status (load_code_memory (oc prog)).
     633  ∀final: Status (load_code_memory (oc prog)).
     634  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    634635  ∀unrepeating_witness: tlr_unrepeating … trace.
    635   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    636   ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    637       pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
     636  ∀codom_dom: (∀pc,k. lookup_opt … pc (costlabels prog) = Some … k → present … cost_map k).
     637  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc (costlabels prog) = Some … k →
     638      pi1 … (block_cost prog pc) = lookup_present … k_pres).
    638639        let ctrace ≝ flatten_trace_label_return … trace in
    639           clock … code_memory … final =
    640             clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    641   #code_memory #cost_labels #cost_map
     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)).
     642  #prog #cost_map
    642643  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    643644  <compute_trace_label_return_using_paid_ok_with_trace try assumption
     
    646647
    647648theorem compute_max_trace_label_return_cost_ok_with_trace:
    648   ∀code_memory: BitVectorTrie Byte 16.
    649   ∀cost_labels: BitVectorTrie costlabel 16.
    650   ∀cost_labels_injective:
    651    (∀pc,pc',l.
    652      lookup_opt costlabel 16 pc cost_labels=Some costlabel l
    653       →lookup_opt costlabel 16 pc' cost_labels=Some costlabel l→pc=pc').
    654   ∀initial: Status code_memory.
    655   ∀final: Status code_memory.
    656   ∀trace: trace_label_return (OC_abstract_status code_memory cost_labels) initial final.
     649  ∀prog: labelled_object_code.
     650  ∀initial: Status (load_code_memory (oc prog)).
     651  ∀final: Status (load_code_memory (oc prog)).
     652  ∀trace: trace_label_return (OC_abstract_status prog) initial final.
    657653  ∀unrepeating_witness: tlr_unrepeating … trace.
    658     let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
     654    let cost_map ≝ traverse_code prog in
    659655    let ctrace ≝ flatten_trace_label_return … trace in
    660       clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
     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)).
    661657  [1:
    662     #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
     658    #prog #initial #final #trace #unrepeating_witness
    663659    @compute_max_trace_label_return_cost_ok_with_trace_aux try assumption
    664660  |2:
     
    666662  ]
    667663  normalize nodelta
    668   cases (traverse_code ???)
     664  cases (traverse_code ?)
    669665  #cost_map * #dom_codom #codom_dom try assumption
    670666  #pc #k #lookup_opt_assm @(dom_codom … lookup_opt_assm)
     
    682678
    683679lemma costlabel_map_of_as_cost_labels_map_ok:
    684  ∀ccode1,ccode2,cost_labels_injective,tl,Htl,PRF,PRF2.
    685   lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective) tl
     680 ∀prog,tl,Htl,PRF,PRF2.
     681  lookup_present CostTag ℕ (compute_costs prog) tl
    686682  PRF
    687683  =
    688    lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective)
    689    (as_cost_get_label (OC_abstract_status (load_code_memory ccode1) ccode2)
     684   lookup_present CostTag ℕ (compute_costs prog)
     685   (as_cost_get_label (OC_abstract_status prog)
    690686    «tl,Htl») PRF2.
    691687//
     
    695691  ∀compiled_code: labelled_object_code.
    696692  let cost_labels ≝ costlabels compiled_code in
    697   let cost_map ≝ compute_costs (oc compiled_code) (costlabels compiled_code) (oc_injective_costlabels compiled_code) in
     693  let cost_map ≝ compute_costs compiled_code in
    698694  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    699695  ∀trace.
Note: See TracChangeset for help on using the changeset viewer.