Changeset 1943 for src/ASM/Assembly.ma
 Timestamp:
 May 14, 2012, 6:45:01 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1942 r1943 1087 1087 tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *) 1088 1088 1089 (*axiom eq_identifier_eq:1089 axiom eq_identifier_eq: 1090 1090 ∀tag: String. 1091 1091 ∀l. … … 1097 1097 ∀l, r: identifier tag. 1098 1098 eq_identifier tag l r = false → (l = r → False). 1099 *)1100 1099 1101 1100 (* label_map: identifier ↦ pseudo program counter *) … … 1140 1139 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *) 1141 1140 let 〈labels,costs〉 ≝ labels_costs in 1142 ∀i:ℕ.lt i (program) →1141 (*∀i:ℕ.lt i (program) → *) 1143 1142 ∀l.occurs_exactly_once ?? l program → 1144 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 1145 lookup ?? labels l = Some ? i 1143 (*is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 1144 lookup ?? labels l = Some ? i*) 1145 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1146 address_of_word_labels_code_mem program l 1146 1147 ) ≝ 1147 1148 λprogram. … … 1150 1151 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in 1151 1152 ppc = prefix ∧ 1153 ∀l.occurs_exactly_once ?? l prefix → 1154 bitvector_of_nat ? (lookup_def ?? labels l 0) = 1155 address_of_word_labels_code_mem prefix l 1156 (* 1152 1157 ∀i:ℕ.lt i (prefix) → 1153 1158 ∀l.occurs_exactly_once ?? l prefix → 1154 1159 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 1155 lookup … labels l = Some ? i 1160 lookup … labels l = Some ? i *) 1156 1161 ) 1157 1162 program … … 1173 1178 labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %] 1174 1179 inversion label [#EQ  #l #EQ] 1180 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta 1181 >occurs_exactly_once_None in Hocc; @(IH2 lbl) 1182  #lbl normalize nodelta inversion (eq_identifier ? lbl l) 1183 [ #Heq #Hocc >(eq_identifier_eq … Heq) 1184 >address_of_word_labels_code_mem_Some_hit 1185 [ >IH1 >lookup_def_add_hit % 1186  <(eq_identifier_eq … Heq) in Hocc; // 1187 ] 1188  #Hneq #Hocc 1189 <address_of_word_labels_code_mem_Some_miss 1190 [ >lookup_def_add_miss 1191 [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq // 1192  % @neq_identifier_neq @Hneq 1193 ] 1194  @Hocc 1195  >eq_identifier_sym @Hneq 1196 ] 1197 ] 1198 ] 1199 (*  1200 [ @Hocc 1201  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by / 1202 ] 1175 1203 [1,2: normalize nodelta 1176 #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi;1177 [3: #Hi #lbl #Hocc #Hlbllapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc1204 (* #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 1205 [3: #Hi *) #lbl #Hocc (*#Hlbl*) lapply (occurs_exactly_once_Some_stronger ?????? Hocc) Hocc 1178 1206 @eq_identifier_elim 1179 1207 [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl … … 1201 1229 ] 1202 1230 ] 1203 ] 1231 ] *) 1204 1232  @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try % 1205 # i #Hi normalize in Hi; cases (not_le_Sn_O i) #abs cases (abs Hi)1233 #l #abs cases (abs) 1206 1234  cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta * 1207 1235 #_ #H @H … … 1214 1242 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 1215 1243 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 1253 qed. 1254 1244 #p @pi2 1245 qed. 1246 1255 1247 definition assembly: 1256 1248 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝
Note: See TracChangeset
for help on using the changeset viewer.