Changeset 2264 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (7 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r2124 r2264  
    33include "ASM/ASM.ma".
    44include "basics/russell.ma".
     5
     6(***** Pseudo-code ******)
     7
     8definition inefficient_address_of_word_labels_code_mem ≝
     9  λcode_mem : list labelled_instruction.
     10  λid: Identifier.
     11    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).
     12
     13lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list.
     14 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) %
     19qed.
     20
     21lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
     22 eq_identifier ? id' id = false →
     23  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 | // ]
     28qed.
     29
     30lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list.
     31  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
     36qed.
     37
     38(* label_map: identifier ↦ pseudo program counter *)
     39definition label_map ≝ identifier_map ASMTag ℕ.
     40
     41(* The function that creates the label-to-address map *)
     42definition create_label_cost_map0: ∀program:list labelled_instruction.
     43  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
     44    let labels ≝ \fst labels_costs in
     45    (∀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|)
     49  ) ≝
     50  λprogram.
     51  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
     52  (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.
     53    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
     54    ppc = |prefix| ∧
     55    ((∀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  program
     60  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     61   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
     62   let 〈label,instr〉 ≝ x in
     63   let labels ≝
     64     match label with
     65     [ None   ⇒ labels
     66     | Some l ⇒ add … labels l ppc
     67     ] in
     68   let costs ≝
     69     match instr with
     70     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
     71     | _ ⇒ costs ] in
     72      〈labels,costs,S ppc〉
     73   ) 〈(empty_map …),(Stub ??),0〉)).
     74[ 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
     89     ]
     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     ]
     98   ]
     99 ]
     100| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
     101  #l #abs cases (abs)
     102| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
     103  #_ #H @H
     104]
     105qed.
     106
     107(* The function that creates the label-to-address map *)
     108definition create_label_cost_map: ∀program:list labelled_instruction.
     109  label_map × (BitVectorTrie costlabel 16) ≝
     110    λprogram.
     111      pi1 … (create_label_cost_map0 program).
     112
     113theorem create_label_cost_map_ok:
     114 ∀instr_list.
     115   let labels ≝ \fst (create_label_cost_map instr_list) in
     116    ((∀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))
     118    ∧
     119     (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)).
     120 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
     121 @pi2
     122qed.
     123
     124definition address_of_word_labels :
     125 list labelled_instruction → Identifier → Word
     126
     127  λcode_mem : list labelled_instruction.
     128  λid: Identifier.
     129   let labels ≝ \fst (create_label_cost_map code_mem) in
     130    bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O).
     131
     132lemma address_of_word_labels_None: ∀i,id,instr_list.
     133 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
     134  address_of_word_labels instr_list id =
     135  address_of_word_labels (instr_list@[〈None …,i〉]) id.
     136 #i #id #instr_list #H
     137 whd in match address_of_word_labels; normalize nodelta
     138 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
     139 lapply (create_label_cost_map_ok instr_list) * #K #_
     140 >K' // >K // <inefficient_address_of_word_labels_None //
     141qed.
     142
     143lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
     144 eq_identifier ? id' id = false →
     145  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
     146   address_of_word_labels instr_list id =
     147   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
     148 #i #id #id' #instr_list #H1 #H2
     149 whd in match address_of_word_labels; normalize nodelta
     150 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
     151 lapply (create_label_cost_map_ok instr_list) * #K #_
     152 >K' // >K
     153 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
     154 @inefficient_address_of_word_labels_Some_miss //
     155qed.
     156
     157lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
     158  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
     159   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
     160   = bitvector_of_nat … (|instr_list|).
     161 #i #id #instr_list #H
     162 whd in match address_of_word_labels; normalize nodelta
     163 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
     164 >K // @inefficient_address_of_word_labels_Some_hit //
     165qed.
     166
     167(***** Object-code *******)
    5168
    6169definition bitvector_max_nat ≝
Note: See TracChangeset for help on using the changeset viewer.