Changeset 1964


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

introduced as_label_of_cost and adapted accordingly. Equality of cost mapping sums

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1962 r1964  
    1414      (program_counter …)
    1515      (λs,class. ASM_classify … s = class)
    16       (current_instruction_label code_memory cost_labels)
     16      (λpc.lookup_opt ?? pc cost_labels)
    1717      (next_instruction_properly_relates_program_counters code_memory)
    1818      ?.
  • 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
  • src/ASM/Interpret.ma

    r1962 r1964  
    1818 #a #b
    1919 cases a cases b
    20  normalize
    2120 #K
    22  try %
    23  cases (eq_true_false K)
     21 try cases (eq_true_false K)
     22 %
    2423qed.
    2524
  • src/ASM/Util.ma

    r1937 r1964  
    10641064  |2:
    10651065    #n' #inductive_hypothesis normalize
    1066     #absurd @inductive_hypothesis /2/
     1066    #absurd @inductive_hypothesis /2 by injective_S/
    10671067  ]
    10681068qed.
     
    14331433 #T #x #y #H @option_destruct_Some @H
    14341434qed.
     1435
     1436lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?.
     1437#A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS')
     1438qed.
     1439
     1440coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝
     1441  not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?.
  • src/common/StructuredTraces.ma

    r1949 r1964  
    2020  ; as_pc_of : as_status → as_pc
    2121  ; as_classifier : as_status → status_class → Prop
    22   ; as_label : as_status → option costlabel
     22  ; as_label_of_pc : as_pc → option costlabel
    2323  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    2424  ; as_final: as_status → Prop
    2525}.
     26
     27definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc … (as_pc_of … s).
    2628
    2729(* temporary alias for backward compatibility *)
     
    435437    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    436438  ].
     439 
     440interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
     441interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
     442interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
     443
    437444
    438445let rec flatten_trace_label_label
     
    440447    (start_status: S) (final_status: S)
    441448      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    442         on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     449        on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝
    443450  match the_trace with
    444451  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    455462    (start_status: S) (final_status: S)
    456463      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    457         on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     464        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
    458465  match the_trace with
    459466  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     
    473480    (start_status: S) (final_status: S)
    474481      (the_trace: trace_label_return S start_status final_status)
    475         on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     482        on the_trace: list (Σl: costlabel.  ∃pc. as_label_of_pc S pc = Some … l) ≝
    476483  match the_trace with
    477484  [ tlr_base before after trace_to_lift ⇒
     
    485492    cases abs -abs #abs @abs %
    486493  |1:
    487     %{initial} whd in match label;
     494    %{(as_pc_of … initial)} whd in match label;
     495    change with (as_label ?? = ?)
    488496    generalize in match labelled_proof; whd in ⊢ (% → ?);
    489497    cases (as_label S initial)
     
    595603qed.
    596604
     605definition as_cost_map ≝
     606  λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
     607
     608definition lift_cost_map_id :
     609  ∀S_in, S_out: abstract_status.
     610   (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
     611       ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
     612  (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
     613   match dec l_sig with
     614   [ inl prf ⇒ m «l_sig, prf»
     615   | inr _ ⇒ 0 (* labels not present in out code get 0 *)
     616   ].
     617
     618lemma lift_cost_map_id_eq :
     619  ∀S_in, S_out, dec, m, l_in, l_out.
     620  pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
     621#S_in #S_out #dec #m #l_in * #l_out #prf #EQ
     622whd in match lift_cost_map_id; normalize nodelta
     623cases (dec l_in) normalize nodelta >EQ
     624[2: #H @⊥] /2 by refl, absurd/
     625qed.
     626
     627notation > "Σ_{ ident i ∈ l } f"
     628  with precedence 20
     629  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
     630notation < "Σ_{ ident i ∈ l } f"
     631  with precedence 20
     632for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     633
     634definition as_cost_of_trace_any_label :
     635  ∀S : abstract_status.
     636  ∀fl, start, end.
     637  as_cost_map S →
     638  trace_any_label S fl start end → ℕ ≝
     639  λS,fl,start,end,m,the_trace.
     640  Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig).
     641
     642definition as_cost_of_trace_label_label :
     643  ∀S : abstract_status.
     644  ∀fl, start, end.
     645  as_cost_map S →
     646  trace_label_label S fl start end → ℕ ≝
     647  λS,fl,start,end,m,the_trace.
     648  Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig).
     649
     650definition as_cost_of_trace_label_return :
     651  ∀S : abstract_status.
     652  ∀start, end.
     653  as_cost_map S →
     654  trace_label_return S start end → ℕ ≝
     655  λS,start,end,m,the_trace.
     656  Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig).
     657
     658lemma lift_cost_map_same_cost :
     659  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     660  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
     661  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
     662  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
     663#S_in #S_out #dec #m_out #trace_in elim trace_in
     664[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
     665normalize in ⊢ (%→?);
     666[2,3: #ABS destruct(ABS)
     667|4: #_ %
     668|1:
     669  #EQ destruct
     670  whd in ⊢(??%%);
     671  >(lift_cost_map_id_eq … e0)
     672  >e0 in e1; normalize in ⊢(%→?); #EQ
     673  >(IH … EQ) %
     674]
     675qed.
     676
     677lemma lift_cost_map_same_cost_tal :
     678  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
     679  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
     680  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
     681  tal_rel … the_trace_in the_trace_out →
     682  as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     683    as_cost_of_trace_any_label … m_out the_trace_out.
     684#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
     685#tal_in #tal_out #H_tal
     686@(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal))
     687qed.
     688
     689lemma lift_cost_map_same_cost_tll :
     690  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
     691  ∀the_trace_in : trace_label_label S_in f_in start_in end_in.
     692  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
     693  tll_rel … the_trace_in the_trace_out →
     694  as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     695    as_cost_of_trace_label_label … m_out the_trace_out.
     696#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
     697#tll_in #tll_out #H_tll
     698@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
     699qed.
     700
     701lemma lift_cost_map_same_cost_tlr :
     702  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
     703  ∀the_trace_in : trace_label_return S_in start_in end_in.
     704  ∀the_trace_out : trace_label_return S_out start_out end_out.
     705  tlr_rel … the_trace_in the_trace_out →
     706  as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
     707    as_cost_of_trace_label_return … m_out the_trace_out.
     708#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
     709#tlr_in #tlr_out #H_tlr
     710@(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
     711qed.
Note: See TracChangeset for help on using the changeset viewer.