Changeset 1935 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 10, 2012, 5:13:34 PM (8 years ago)
Author:
mulligan
Message:

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1929 r1935  
    268268include alias "ASM/BitVectorTrie.ma".
    269269
     270(*
    270271let rec compute_cost_trace_label_label
    271272  (cm: BitVectorTrie Byte 16)
     
    327328 | cases abs #absurd @absurd % ]
    328329qed.
     330*)
    329331
    330332include alias "arithmetics/nat.ma".
     
    384386
    385387definition tech_cost_of_label0:
     388 ∀code_memory: BitVectorTrie Byte 16.
    386389 ∀cost_labels: BitVectorTrie costlabel 16.
    387390 ∀cost_map: identifier_map CostTag nat.
    388391 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    389  ∀ctrace:list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k).
     392 ∀ctrace:list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k).
    390393 ∀i,p. present … cost_map (nth_safe ? i ctrace p).
    391  #cost_labels #cost_map #codom_dom #ctrace #i #p
     394 #code_memory #cost_labels #cost_map #codom_dom #ctrace #i #p
    392395 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K
    393396 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres)
     
    445448
    446449definition tech_cost_of_label:
     450 ∀code_memory: BitVectorTrie Byte 16.
    447451 ∀cost_labels: BitVectorTrie costlabel 16.
    448452 ∀cost_map: identifier_map CostTag nat.
    449453 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    450  list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k) →
     454 list (Σk:costlabel.∃s: ASM_abstract_status code_memory cost_labels. as_label … s = Some ? k) →
    451455 nat → nat
    452 ≝ λcost_labels,cost_map,codom_dom,ctrace,i.
     456≝ λcode_memory,cost_labels,cost_map,codom_dom,ctrace,i.
    453457 ltb_rect ? i (|ctrace|)
    454458 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?)
     
    485489
    486490lemma tech_cost_of_label_shift:
    487  ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     491 ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
    488492  i < |l2| →
    489    tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    490    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
    491  #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
     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
    492496 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    493497 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
     
    500504   |3: @⊥ @(absurd ?? K2) >length_append in K1; #K1 /2 by lt_plus_to_lt_l/ ]
    501505 | #H1 #H2
    502    generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     506   generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
    503507   <(shift_nth_safe … H1) #p %
    504508 | // ]
     
    506510
    507511lemma tech_cost_of_label_prefix:
    508  ∀cost_labels,cost_map,codom_dom,l1,l2,i.
     512 ∀code_memory,cost_labels,cost_map,codom_dom,l1,l2,i.
    509513  i < |l1| →
    510    tech_cost_of_label cost_labels cost_map codom_dom l1 i =
    511    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) i.
    512  #cost_labels #cost_map #codom_dom #l1 #l2 #i #H
     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
    513517 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    514518 [1:
     
    518522 |2:
    519523   #K1 #K2
    520    generalize in match (tech_cost_of_label0 ??? (l1@l2) ??);
     524   generalize in match (tech_cost_of_label0 ???? (l1@l2) ??);
    521525   <(shift_nth_prefix … l1 i l2 K1 K2) //
    522526 |3:
     
    535539 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    536540   pi1 … (block_cost cm pc cost_labels) = lookup_present … k_pres).
    537   let ctrace ≝ compute_cost_trace_label_return cm … trace in
     541  let ctrace ≝ as_compute_cost_trace_label_return (ASM_abstract_status cm cost_labels) … trace in
    538542  compute_trace_label_return_cost_using_paid cm … trace =
    539    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     543   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    540544    ≝ ?
    541545and compute_trace_any_label_using_paid_ok_with_trace
     
    550554 on trace:
    551555  ∀unrepeating_witness: tal_unrepeating … trace.
    552   let ctrace ≝ compute_cost_trace_any_label … trace in
     556  let ctrace ≝ as_compute_cost_trace_any_label (ASM_abstract_status cm cost_labels) … trace_ends_flag … trace in
    553557  compute_trace_any_label_cost_using_paid … trace =
    554    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     558   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    555559    ≝ ?
    556560and compute_trace_label_label_using_paid_ok_with_trace
     
    566570 on trace:
    567571 ∀unrepeating_witness: tll_unrepeating … trace.
    568   let ctrace ≝ compute_cost_trace_label_label … trace in
     572  let ctrace ≝ as_compute_cost_trace_label_label (ASM_abstract_status cm cost_labels) … trace in
    569573  compute_trace_label_label_cost_using_paid … trace =
    570    (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     574   (Σ_{i < |ctrace|} (tech_cost_of_label cm cost_labels cost_map codom_dom ctrace i))
    571575    ≝ ?.
    572576  cases trace normalize nodelta
    573577  [ #sb #sa #tr #unrepeating_witness #dom_codom whd in ⊢ (??%?);
    574     whd in match (compute_cost_trace_label_return ?????);
     578    whd in match (as_compute_cost_trace_label_return ????);
    575579    @compute_trace_label_label_using_paid_ok_with_trace
    576580    assumption
    577581  | #si #sl #sf #tr1 #tr2 #unrepeating_witness #dom_codom
    578582    whd in ⊢ (??%?);
    579     whd in match (compute_cost_trace_label_return ?????);
     583    whd in match (as_compute_cost_trace_label_return ????);
    580584    >append_length >bigop_sum_rev >commutative_plus @eq_f2
    581585    [ >(compute_trace_label_return_using_paid_ok_with_trace … cost_map … codom_dom ? dom_codom)
     
    602606    >(compute_trace_any_label_using_paid_ok_with_trace … cost_map … codom_dom … dom_codom)
    603607    [1:
     608      whd in match (as_compute_cost_trace_label_label ?????);
    604609      >bigop_0 in ⊢ (???%); >commutative_plus @eq_f2
    605610      [1:
    606611        @same_bigop [//] #i #H #_ -dom_codom >(plus_n_O i) >plus_n_Sm
    607         <(tech_cost_of_label_shift ??? [?] ? i) //
     612        <(tech_cost_of_label_shift ???? [?] ? i) try assumption <(plus_n_O i) %
    608613      |2:
    609614        change with (? = lookup_present ? ? ? ? ?)
    610         generalize in match (tech_cost_of_label0 ? ? ? ? ? ?);
     615        generalize in match (tech_cost_of_label0 ? ? ? ? ? ? ?);
    611616        normalize in match (nth_safe ? ? ? ?);
    612617        whd in costed_assm; lapply costed_assm whd in match (as_label ??);
     
    682687  ∀dom_codom: (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
    683688      pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres).
    684         let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
     689        let ctrace ≝ as_compute_cost_trace_label_return … trace in
    685690          clock … code_memory … final =
    686             clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i)).
     691            clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label code_memory cost_labels cost_map codom_dom ctrace i)).
    687692  #code_memory #cost_labels #cost_map
    688693  #initial #final #trace #unrepeating_witness #codom_dom #dom_codom normalize nodelta
     
    703708  ∀unrepeating_witness: tlr_unrepeating … trace.
    704709    let cost_map ≝ traverse_code code_memory cost_labels cost_labels_injective in
    705     let ctrace ≝ compute_cost_trace_label_return code_memory … trace in
    706       clock … code_memory … final = clock … code_memory … initial + (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map ? ctrace i)).
     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)).
    707712  [1:
    708713    #code_memory #cost_labels #cost_labels_injective #initial #final #trace #unrepeating_witness
Note: See TracChangeset for help on using the changeset viewer.