Changeset 2657


Ignore:
Timestamp:
Feb 12, 2013, 2:41:22 AM (6 years ago)
Author:
sacerdot
Message:

Cost proof fully repaired. It was broken by the definitions used in compiler.ma.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2516 r2657  
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
    329 (* use of this defn in ASM/CostsProof.ma is ill-typed *)
    330329definition ASM_cost_map :
    331330  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
  • src/ASM/CostsProof.ma

    r2656 r2657  
    720720include "utilities/permutations.ma".
    721721
     722definition map_of_sigma_map:
     723 ∀P.
     724  (Σmap:identifier_map CostTag ℕ.P map) → identifier_map CostTag ℕ
     725 ≝ λP,x.x.
     726
     727definition costlabel_of_as_cost_labels:
     728 ∀code,cost_labels.
     729  as_cost_label (ASM_abstract_status (load_code_memory code) cost_labels)
     730  →Σk:costlabel
     731   .(∃b:BitVector 16.lookup_opt costlabel 16 b cost_labels = Some costlabel k).
     732 #code #cost_labels * #l #Hl %{l} cases Hl #pc #Hl' %{pc} @Hl'
     733qed.
     734
     735lemma costlabel_map_of_as_cost_labels_map_ok:
     736 ∀ccode1,ccode2,cost_labels_injective,tl,Htl,PRF,PRF2.
     737  lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective) tl
     738  PRF
     739  =
     740   lookup_present CostTag ℕ (compute_costs ccode1 ccode2 cost_labels_injective)
     741   (as_cost_get_label (ASM_abstract_status (load_code_memory ccode1) ccode2)
     742    «tl,Htl») PRF2.
     743//
     744qed.
     745
    722746lemma tech_cost_sum_eq_as_cost :
    723   ∀code_memory: BitVectorTrie Byte 16.
    724   ∀cost_labels: BitVectorTrie costlabel 16.
    725   ∀cost_map: identifier_map CostTag nat.
    726   ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     747  ∀compiled_code: (list Byte) × (BitVectorTrie costlabel 16).
     748  let cost_labels ≝ \snd compiled_code in
     749  ∀cost_labels_injective:
     750   (∀pc,pc',l.
     751     lookup_opt … pc (\snd  compiled_code) = Some … l
     752     → lookup_opt … pc' (\snd  compiled_code) = Some … l → pc = pc').
     753  let cost_map ≝ compute_costs (\fst compiled_code) (\snd compiled_code) cost_labels_injective in
     754  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    727755  ∀trace.
    728   (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
    729   (Σ_{l ∈ trace}(ASM_cost_map code_memory … codom_dom l)).
    730 #cmem #clab #cmap #codom_dom #trace
     756  (Σ_{i < |trace|}(tech_cost_of_label cost_labels (map_of_sigma_map … cost_map) codom_dom (map ?? (costlabel_of_as_cost_labels …) trace) i)) =
     757  (Σ_{l ∈ trace}(ASM_cost_map compiled_code cost_labels_injective l)).
     758* #ccode1 #ccode2 #cost_labels_injective #codom_dom #trace
    731759@(list_elim_left … trace)
    732760[ %
    733761| #tl #hd #IH >append_length >commutative_plus
    734762  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
    735   whd in ⊢ (??%%); <IH
    736   <tech_cost_of_label_shift [2: %]
     763  whd in ⊢ (??%%); <IH <map_append
     764  <(? : | map … hd | = | hd |) [1: <tech_cost_of_label_shift] [2: % | 5: // |3,4: skip]
    737765  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
    738   [ %
     766  [ cases tl -tl #tl #Htl
     767    change with (lookup_present ????? = ?)
     768    whd in ⊢ (???(%???)); normalize nodelta
     769    generalize in ⊢ (???(?????%)); #p
     770    @costlabel_map_of_as_cost_labels_map_ok
    739771  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
    740772  ]
Note: See TracChangeset for help on using the changeset viewer.