Changeset 2760 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2754 r2760  
    451451 ]
    452452qed.
    453    
     453
    454454let rec compute_trace_label_return_using_paid_ok_with_trace
    455455 (cm: ?) (cost_labels: BitVectorTrie costlabel 16)
     
    504504  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    505505    whd in ⊢ (??%?);
    506     whd in match (flatten_trace_label_return ????);
     506    whd in match flatten_trace_label_return; normalize nodelta
     507    whd in match (observables_trace_label_return ?????);
     508    >costlabels_of_observables_append
    507509    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    508510    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     
    565567    #classifier_assm #after_return_assm #trace_label_return #costed_assm #unrepeating_witness
    566568    whd in ⊢ (??%?);
    567     @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    568     assumption
     569    >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     570    //
     571    whd in match flatten_trace_any_label; normalize nodelta
     572    whd in match (observables_trace_any_label ??????);
     573    >(costlabels_of_observables_append … [?]) [2: normalize /2/]
     574    >length_append whd in match (? + ?);
     575    whd in match flatten_trace_label_return; normalize nodelta
     576    >costlabels_of_observables_trace_label_return_id_irrelevant //
    569577  |6:
    570578    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    571579    #classifier_assm #trace_label_return #unrepeating_witness
    572580    whd in ⊢ (??%?);
    573     @(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    574     assumption
     581    >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     582    //
     583    whd in match flatten_trace_any_label; normalize nodelta
     584    whd in match (observables_trace_any_label ??????);
     585    >(costlabels_of_observables_append … [?]) [2: normalize /2/]
     586    >length_append whd in match (? + ?);
     587    whd in match flatten_trace_label_return; normalize nodelta
     588    >costlabels_of_observables_trace_label_return_id_irrelevant //
    575589  |7:
    576590    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    582596      >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    583597      [1:
     598        whd in match flatten_trace_any_label in ⊢ (???%); normalize nodelta
     599        whd in match (observables_trace_any_label ??????);
     600        >costlabels_of_observables_append
     601        >(costlabels_of_observables_append … [?]) [2: normalize /2/]
    584602        >length_append >bigop_sum_rev >commutative_plus @eq_f2
    585603        [ @same_bigop [2: #i #H #_ -dom_codom @tech_cost_of_label_shift assumption
    586604                      |1: #i #H % ]
    587         | @same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H)
     605        | >length_append whd in match (|?|+?);
     606          >costlabels_of_observables_trace_label_return_id_irrelevant
     607          [@same_bigop [#i #H %] #i #H #_ @(tech_cost_of_label_prefix … H) | skip]
    588608        ]
    589609      |2:
     
    674694lemma tech_cost_sum_eq_as_cost :
    675695  ∀compiled_code: labelled_object_code.
    676   let cost_labels ≝ \fst (\snd compiled_code) in
    677   ∀cost_labels_injective:
    678    (∀pc,pc',l.
    679      lookup_opt … pc cost_labels = Some … l
    680      → lookup_opt … pc' cost_labels = Some … l → pc = pc').
    681   let cost_map ≝ compute_costs (\fst compiled_code) (\fst (\snd compiled_code)) cost_labels_injective in
     696  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
    682698  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    683699  ∀trace.
    684700  (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom trace i)) =
    685   (Σ_{l ∈ trace}(ASM_cost_map compiled_code cost_labels_injective l)).
    686 * #ccode1 #ccode2 #cost_labels_injective #codom_dom #trace
     701  (Σ_{l ∈ trace}(ASM_cost_map compiled_code l)).
     702#ccode #codom_dom #trace
    687703@(list_elim_left … trace)
    688704[ %
     
    692708  <tech_cost_of_label_shift [2: //]
    693709  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
    694   [ cases tl -tl #tl #Htl
    695     change with (lookup_present ????? = ?)
    696     whd in ⊢ (???(%???)); normalize nodelta
    697     generalize in ⊢ (???(?????%)); #p
    698     @costlabel_map_of_as_cost_labels_map_ok
     710  [ cases tl -tl #tl #Htl @costlabel_map_of_as_cost_labels_map_ok
    699711  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
    700712  ]
Note: See TracChangeset for help on using the changeset viewer.