Changeset 1964 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 17, 2012, 12:06:34 PM (8 years ago)
Author:
tranquil
Message:

introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/CostsProof.ma

    r1935 r1964  
    386386
    387387definition tech_cost_of_label0:
    388  ∀code_memory: BitVectorTrie Byte 16.
    389388 ∀cost_labels: BitVectorTrie costlabel 16.
    390389 ∀cost_map: identifier_map CostTag nat.
    391390 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    392  ∀ctrace:list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k).
     391 ∀ctrace:list (Σk:costlabel.∃b.lookup_opt … b cost_labels = Some ? k).
    393392 ∀i,p. present … cost_map (nth_safe ? i ctrace p).
    394  #code_memory #cost_labels #cost_map #codom_dom #ctrace #i #p
     393 #cost_labels #cost_map #codom_dom #ctrace #i #p
    395394 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K
    396395 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres)
    … …  
    448447
    449448definition tech_cost_of_label:
    450  ∀code_memory: BitVectorTrie Byte 16.
    451449 ∀cost_labels: BitVectorTrie costlabel 16.
    452450 ∀cost_map: identifier_map CostTag nat.
    453451 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    454  list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k) →
     452 list (Σk:costlabel.∃b.lookup_opt … b cost_labels = Some ? k) →
    455453 nat → nat
    456 ≝ λcode_memory,cost_labels,cost_map,codom_dom,ctrace,i.
     454≝ λcost_labels,cost_map,codom_dom,ctrace,i.
    457455 ltb_rect ? i (|ctrace|)
    458456 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?)
    … …  
    489487
    490488lemma tech_cost_of_label_shift:
    491  ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
     489 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
    492490  i < |l2| →
    493    tech_cost_of_label code_memory cost_labels cost_map codom_dom l2 i =
    494    tech_cost_of_label code_memory cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
    495  #code_memory #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
     491   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
     492   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
     493 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    496494 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    497495 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
    498496   whd in match ltb; normalize nodelta
    499    [1: >le_to_leb_true try assumption applyS le_to_leb_true //
     497   [1: >le_to_leb_true try assumption applyS le_to_leb_true / by /
    500498   |4: >not_le_to_leb_false try assumption applyS not_le_to_leb_false
    501499       change with (¬ ? ≤ ?) in K1; applyS K1
    502    |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) // >length_append
    503        applyS (monotonic_lt_plus_r … (|l1|)) //
     500   |2: @⊥ @(absurd (i+|l1| < |l1@l2|)) / by / >length_append
     501       applyS (monotonic_lt_plus_r … (|l1|)) / by /
    504502   |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ]
    505503 | #H1 #H2
    506    generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
     504   generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
    507505   <(shift_nth_safe … H1) #p %
    508  | // ]
     506 | / by / ]
    509507qed.
    510508
    511509lemma tech_cost_of_label_prefix:
    512  ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
     510 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
    513511  i < |l1| →
    514    tech_cost_of_label code_memory cost_labels cost_map codom_dom l1 i =
    515    tech_cost_of_label code_memory cost_labels cost_map codom_dom (l1@l2) i.
    516  #code_memory #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
     512   tech_cost_of_label cost_labels cost_map codom_dom l1 i =
     513   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) i.
     514 #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
    517515 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    518516 [1:
    … …  
    522520 |2:
    523521   #K1 #K2
    524    generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
     522   generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
    525523   <(shift_nth_prefix … l1 i l2 K1 K2) //
    526524 |3:
    … …  
    539537 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    540538   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    541   let ctrace ≝ as_compute_cost_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
     539  let ctrace ≝ flatten_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
    542540  compute_trace_label_return_cost_using_paid cm … trace =
    543    (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
     541   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    544542    ≝ ?
    545543and compute_trace_any_label_using_paid_ok_with_trace
    … …  
    554552 on trace:
    555553  ∀unrepeating_witness: tal_unrepeating … trace.
    556   let ctrace ≝ as_compute_cost_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
     554  let ctrace ≝ flatten_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
    557555  compute_trace_any_label_cost_using_paid … trace =
    558    (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
     556   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    559557    ≝ ?
    560558and compute_trace_label_label_using_paid_ok_with_trace
    … …  
    570568 on trace:
    571569 ∀unrepeating_witness: tll_unrepeating … trace.
    572   let ctrace ≝ as_compute_cost_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
     570  let ctrace ≝ flatten_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
    573571  compute_trace_label_label_cost_using_paid … trace =
    574    (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
     572   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    575573    ≝ ?.
    576574  cases trace normalize nodelta
    577575  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    578     whd in match (as_compute_cost_trace_label_return ????);
     576    whd in match (flatten_trace_label_return ????);
    579577    @compute_trace_label_label_using_paid_ok_with_trace
    580578    assumption
    581579  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    582580    whd in ⊢ (??%?);
    583     whd in match (as_compute_cost_trace_label_return ????);
     581    whd in match (flatten_trace_label_return ????);
    584582    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    585583    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
    … …  
    606604    >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    607605    [1:
    608       whd in match (as_compute_cost_trace_label_label ?????);
     606      whd in match (flatten_trace_label_label ?????);
    609607      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    610608      [1:
    611609        @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    612         <(tech_cost_of_label_shift ???? [?] ? i) try assumption <(plus_n_O i) %
     610        <(tech_cost_of_label_shift ??? [?] ? i) try assumption <(plus_n_O i) %
    613611      |2:
    614612        change with (? = lookup_present ? ? ? ? ?)
    615         generalize in match (tech_cost_of_label0 ? ? ? ? ? ? ?);
     613        generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
    616614        normalize in match (nth_safe ? ? ? ?);
    617615        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
    … …  
    687685  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    688686      pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
    689         let ctrace ≝ as_compute_cost_trace_label_return … trace in
     687        let ctrace ≝ flatten_trace_label_return … trace in
    690688          clock … code_memory … final =
    691             clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label code_memory cost_labels cost_map codom_dom ctrace i)).
     689            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
    692690  #code_memory #cost_labels #cost_map
    693691  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
    … …  
    708706  ∀unrepeating_witness: tlr_unrepeating … trace.
    709707    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
    710     let ctrace ≝ as_compute_cost_trace_label_return … trace in
    711       clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label code_memory cost_labels cost_map ? ctrace i)).
     708    let ctrace ≝ flatten_trace_label_return … trace in
     709      clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
    712710  [1:
    713711    #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
Note: See TracChangeset for help on using the changeset viewer.