Changeset 3099


Ignore:
Timestamp:
Apr 6, 2013, 4:02:09 PM (4 years ago)
Author:
mckinna
Message:

Simplified preliminaries:

inefficient_address_of_word_labels, and hence create_cost_label_map,

make redundant appeal to bivector_of_nat to change return type,
when only address_of_word_labels need return a Word.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r3039 r3099  
    1 (*include "ASM/BitVectorTrie.ma".*)
     1include "basics/russell.ma".
     2
    23include "ASM/Arithmetic.ma".
    34include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma". *)
    4 include "basics/russell.ma".
    55
    66(***** Pseudo-code ******)
    77
    8 definition inefficient_address_of_word_labels_code_mem ≝
    9   λcode_mem : list labelled_instruction.
     8definition inefficient_address_of_label :
     9 list labelled_instruction → Identifier →  ℕ ≝
     10  λinstr_list : list labelled_instruction.
    1011  λid: Identifier.
    11     bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
    12 
    13 lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list.
     12    index_of ? (instruction_matches_identifier ?? id) instr_list.
     13
     14lemma inefficient_address_of_label_None: ∀i,id,instr_list.
    1415 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
    15   inefficient_address_of_word_labels_code_mem instr_list id =
    16   inefficient_address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    17  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    18  >(index_of_internal_None ?????? H) %
    19 qed.
    20 
    21 lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
     16  inefficient_address_of_label instr_list id =
     17  inefficient_address_of_label (instr_list@[〈None …,i〉]) id.
     18 #i #id #instr_list #H whd in ⊢ (??%%);
     19 >(index_of_internal_None ?????? H) // (*%*)
     20qed.
     21
     22lemma inefficient_address_of_label_Some_miss: ∀i,id,id',instr_list.
    2223 eq_identifier ? id' id = false →
    2324  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
    24    inefficient_address_of_word_labels_code_mem instr_list id =
    25    inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
    26  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
    27  >(index_of_internal_Some_miss ???????? H) [ @refl | // ]
    28 qed.
    29 
    30 lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list.
     25   inefficient_address_of_label instr_list id =
     26   inefficient_address_of_label (instr_list@[〈Some … id',i〉]) id.
     27 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%);
     28 >(index_of_internal_Some_miss ???????? H) // (*[ @refl | // ]*)
     29qed.
     30
     31lemma inefficient_address_of_label_Some_hit: ∀i,id,instr_list.
    3132  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
    32    inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
    33    = bitvector_of_nat … (|instr_list|).
    34  #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
    35  >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl
     33   inefficient_address_of_label (instr_list@[〈Some … id,i〉]) id
     34   = |instr_list|.
     35 #i #id #instr_list #H whd in ⊢ (??%%);
     36 >(index_of_internal_Some_hit ?????? H) <plus_n_O // (*@refl*)
    3637qed.
    3738
     
    4142(* The function that creates the label-to-address map *)
    4243definition create_label_cost_map0: ∀program:list labelled_instruction.
    43   (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     44  (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
    4445    let labels ≝ \fst labels_costs in
     46    let address_of_label ≝ λl. lookup_def ?? labels l 0 in
    4547    (∀l.occurs_exactly_once ?? l program →
    46       bitvector_of_nat ? (lookup_def ?? labels l 0) =
    47        inefficient_address_of_word_labels_code_mem program l) ∧
    48     (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|)
     48      address_of_label l =
     49       inefficient_address_of_label program l) ∧
     50    (∀l.occurs_exactly_once ?? l program → address_of_label l < |program|)
    4951  ) ≝
    5052  λprogram.
    5153  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    52   (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
     54  (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
    5355    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    54     ppc = |prefix| ∧
     56    let address_of_label ≝ λl. lookup_def ?? labels l 0 in
     57      ppc = |prefix| ∧
    5558    ((∀l.occurs_exactly_once ?? l prefix →
    56       bitvector_of_nat ? (lookup_def ?? labels l 0) =
    57        inefficient_address_of_word_labels_code_mem prefix l) ∧
    58     (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|)))
     59      address_of_label l =
     60       inefficient_address_of_label prefix l) ∧
     61    (∀l.occurs_exactly_once ?? l prefix → address_of_label l < |program|)))
    5962  program
    6063  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     
    7376   ) 〈(empty_map …),(Stub ??),0〉)).
    7477[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
    75   #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
    76  inversion label [#EQ | #l #EQ]
    77  [ % #lbl
    78    [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta
    79      >occurs_exactly_once_None in Hocc; @IH2
    80    | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ]
    81  | %
    82    #lbl normalize nodelta inversion (eq_identifier ? lbl l)
    83     [1,3: #Heq #Hocc >(eq_identifier_eq … Heq)
    84      [ >inefficient_address_of_word_labels_Some_hit
    85        [ >IH1 >lookup_def_add_hit %
    86        | <(eq_identifier_eq … Heq) in Hocc; //
    87        ]
    88      | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     78  #IH1 >IH1 -IH1 * #IH2 #IH3 -labels_costs_ppc % [>length_append <plus_n_Sm <plus_n_O %]
     79 inversion label [#EQ | #l #EQ] 
     80 [ % #lbl >occurs_exactly_once_None #Hocc
     81   [ <inefficient_address_of_label_None [2: >occurs_exactly_once_None //]
     82     @IH2
     83   | @IH3
     84   ] //
     85 | % #lbl inversion (eq_identifier ? l lbl)
     86    [1,3: #Heq >(eq_identifier_eq … Heq) #Hocc
     87     [ >inefficient_address_of_label_Some_hit
     88       [ >lookup_def_add_hit
     89       |
     90       ] //
     91     | >lookup_def_add_hit >prf >length_append <plus_n_Sm @le_S_S @le_plus_n_r
    8992     ]
    90     |*: #Hneq #Hocc
    91      cut (occurs_exactly_once … lbl prefix)
    92      [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ]
    93      #Hocc' lapply (IH2 lbl ?) try assumption
    94      [ <inefficient_address_of_word_labels_Some_miss //
    95        >lookup_def_add_miss // % @neq_identifier_neq @Hneq
    96      | >lookup_def_add_miss /2/
    97      ]
     93    |*: #Hneq cut (lbl ≠ l) [1,3: % @neq_identifier_neq >eq_identifier_sym //]
     94     #lbl_neq >(lookup_def_add_miss ??????? lbl_neq) >occurs_exactly_once_Some_eq >Hneq
     95     [ #Hocc lapply (IH2 ? Hocc)
     96       <inefficient_address_of_label_Some_miss [2: >occurs_exactly_once_Some_eq >Hneq]
     97     | @IH3
     98     ] //
    9899   ]
    99100 ]
    100 | @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
     101| @pair_elim * #labels #costs #ppc #EQ destruct % // %
    101102  #l #abs cases (abs)
    102 | cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
     103| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc *
    103104  #_ #H @H
    104105]
     
    107108(* The function that creates the label-to-address map *)
    108109definition create_label_cost_map: ∀program:list labelled_instruction.
    109   label_map × (BitVectorTrie costlabel 16)
     110  label_map × costlabel_map
    110111    λprogram.
    111112      pi1 … (create_label_cost_map0 program).
     
    114115 ∀instr_list.
    115116   let labels ≝ \fst (create_label_cost_map instr_list) in
     117   let address_of_label ≝ λl. lookup_def ?? labels l 0 in
    116118    ((∀id. occurs_exactly_once ??  id instr_list →
    117      (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id))
     119     (address_of_label id = inefficient_address_of_label instr_list id))
    118120    ∧
    119      (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
     121     (∀id. occurs_exactly_once ?? id instr_list → address_of_label id < |instr_list|)).
    120122 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
    121123 @pi2
    122124qed.
    123125
     126(* the defn we care about, and export elsewhere *)
    124127definition address_of_word_labels :
    125128 list labelled_instruction → Identifier → Word
    126129
    127   λcode_mem : list labelled_instruction.
     130  λprogram : list labelled_instruction.
    128131  λid: Identifier.
    129    let labels ≝ \fst (create_label_cost_map code_mem) in
    130     bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
     132   let labels ≝ \fst (create_label_cost_map program) in
     133   let address_of_label ≝ λl. lookup_def ?? labels l 0 in
     134    bitvector_of_nat ? (address_of_label id).
    131135
    132136lemma address_of_word_labels_None: ∀i,id,instr_list.
     
    138142 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
    139143 lapply (create_label_cost_map_ok instr_list) * #K #_
    140  >K' // >K // <inefficient_address_of_word_labels_None //
     144 >K' // >K // <inefficient_address_of_label_None //
    141145qed.
    142146
     
    150154 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
    151155 lapply (create_label_cost_map_ok instr_list) * #K #_
    152  >K' // >K
     156 >K' // >K 
    153157 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
    154  @inefficient_address_of_word_labels_Some_miss //
     158 <inefficient_address_of_label_Some_miss //
    155159qed.
    156160
     
    162166 whd in match address_of_word_labels; normalize nodelta
    163167 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
    164  >K // @inefficient_address_of_word_labels_Some_hit //
     168 >K // <inefficient_address_of_label_Some_hit //
    165169qed.
    166170
    167171(***** Object-code *******)
    168 
     172(*
    169173definition bitvector_max_nat ≝
    170174  λlength: nat.
     
    172176
    173177definition code_memory_size ≝ bitvector_max_nat 16.
     178*)
    174179
    175180lemma Prod_inv_rect_Type0:
Note: See TracChangeset for help on using the changeset viewer.