Changeset 1942 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 14, 2012, 6:02:20 PM (9 years ago)
Author:
mulligan
Message:

Work on showing the equivalence of two methods of looking up from the maps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1934 r1942  
    12091209qed.
    12101210
    1211 (*theorem build_maps_ok:
    1212  ∀pseudo_program.∀sigma:Word → Word.
    1213    let 〈labels, costs〉 ≝ build_maps pseudo_program sigma in
     1211theorem create_label_cost_map_ok:
     1212 ∀pseudo_program: pseudo_assembly_program.
     1213   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
    12141214    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    1215      lookup_def … labels id (zero ?) = sigma (address_of_word_labels_code_mem (\snd pseudo_program) id).
    1216  #pseudo_program #sigma @(pi2 … (build_maps0 … sigma))
    1217 qed.*)
     1215     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
     1216 #pseudo_program
     1217 cases (create_label_cost_map (\snd pseudo_program)) * #label_map #cost_map
     1218 normalize nodelta elim (\snd pseudo_program)
     1219 [1:
     1220   #_ #id #absurd normalize in absurd; cases absurd
     1221 |2:
     1222   #hd #tl #inductive_hypothesis #H #id
     1223   whd in match (occurs_exactly_once ????);
     1224   whd in ⊢ (? → ???%);
     1225   whd in match (index_of ???);
     1226   inversion (instruction_matches_identifier ????) normalize nodelta
     1227   [1:
     1228     whd in ⊢ (??%? → ?); #G
     1229     lapply (H 0 ? id ??)
     1230     [1:
     1231       normalize cases hd in G; #lbl #instr normalize
     1232       cases lbl normalize try (#absurd destruct(absurd) @I)
     1233       #id' change with (eq_identifier ??? = true → ?)
     1234       @(eq_identifier_elim ? ? id id') #assm
     1235       [1:
     1236         //
     1237       |2:
     1238         lapply (eq_identifier_false … assm)
     1239         check eq_identifier
     1240         #absurd1 >eq_identifier_sym >absurd1 #absurd2 destruct(absurd2)
     1241       ]
     1242     |2:
     1243     |3:
     1244       normalize @le_S_S //
     1245     |4:
     1246       #H whd in match (lookup_def ?????);
     1247       >H normalize nodelta #_ %
     1248     ]
     1249   |2:
     1250     
     1251   ]
     1252   cases daemon
     1253qed.
    12181254
    12191255definition assembly:
Note: See TracChangeset for help on using the changeset viewer.