Changeset 867
 Timestamp:
 May 31, 2011, 5:01:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r866 r867 106 106 qed. 107 107 108 axiom vector_associativ ity_of_append:108 axiom vector_associative_append: 109 109 ∀A: Type[0]. 110 110 ∀n, m, o: nat. … … 116 116 (v @@ (q @@ r)). 117 117 118 axiomvector_cons_append:118 lemma vector_cons_append: 119 119 ∀A: Type[0]. 120 120 ∀n: nat. 121 ∀ a: A.121 ∀e: A. 122 122 ∀v: Vector A n. 123 a ::: v = [[ a ]] @@ v. 123 e ::: v = [[ e ]] @@ v. 124 # A # N # E # V 125 elim V 126 [ normalize % 127  # NN # AA # VV # IH 128 normalize 129 % 130 ] 131 qed. 124 132 125 133 lemma super_rewrite2: … … 198 206 (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS))) 199 207 ? 200 (vector_associativ ity_of_append A ? ? ? QQ [[AA]] VV))208 (vector_associative_append A ? ? ? QQ [[AA]] VV)) 201 209 [ >associative_plus // 202 210  @IH ] … … 214 222 qed. 215 223 216 (* 217 lemma subvector_hd_tl: 224 lemma vector_cons_empty: 225 ∀A: Type[0]. 226 ∀n: nat. 227 ∀v: Vector A n. 228 [[ ]] @@ v = v. 229 # A # N # V 230 elim V 231 [ normalize % 232  # NN # HH # VV #H % 233 ] 234 qed. 235 236 corollary subvector_hd_tl: 218 237 ∀A: Type[0]. 219 238 ∀o: nat. … … 223 242 ∀v: Vector A o. 224 243 bool_to_Prop (subvector_with A ? ? eq v (h ::: v)). 225 226 axiom eq_a_reflexive: 244 # A # O # EQ # REFLEX # H # V 245 > (vector_cons_append A ? H V) 246 < (vector_cons_empty A ? ([[H]] @@ V)) 247 @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]]) 248 qed. 249 250 lemma eq_a_reflexive: 227 251 ∀a. eq_a a a = true. 228 252 # A 253 cases A 254 % 255 qed. 256 257 lemma is_in_monotonic_wrt_append: 258 ∀m, n: nat. 259 ∀p: Vector addressing_mode_tag m. 260 ∀q: Vector addressing_mode_tag n. 261 ∀to_search: addressing_mode. 262 bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). 263 # M # N # P # Q # TO_SEARCH 264 # H 265 elim Q 266 [ normalize 267 @ H 268  # NN # PP # QQ # IH 269 normalize 270 cases (is_a PP TO_SEARCH) 271 [ normalize 272 % 273  normalize 274 normalize in IH 275 @ IH 276 ] 277 ] 278 qed. 279 280 corollary is_in_hd_tl: 281 ∀to_search: addressing_mode. 282 ∀hd: addressing_mode_tag. 283 ∀n: nat. 284 ∀v: Vector addressing_mode_tag n. 285 bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). 286 # TO_SEARCH # HD # N # V 287 elim V 288 [ # H 289 normalize in H; 290 cases H 291  # NN # HHD # VV # IH # HH 292 > vector_cons_append 293 > (vector_cons_append ? ? HHD VV) 294 @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH) 295 @ HH 296 ] 297 qed. 298 229 299 let rec list_addressing_mode_tags_elim 230 300 (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ … … 257 327 in 258 328 andb (process_hd P) 259 (match len return λ len. Vector addressing_mode_taglen → bool with260 [ O ⇒ λ _.true261  S y ⇒ λ tl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl)329 (match len return λx. x = len → bool with 330 [ O ⇒ λprf. true 331  S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) 262 332 ]. 263 [1: @ (execute_1_technical ? ? tl) 264 [ // 265  @ (subvector_hd_tl addressing_mode_tag (S y) (S len) eq_a eq_a_reflexive) 266 ] 267 ]. 333 try % 334 [ 2: cases (sym_eq ??? prf); @tl 335  cases prf in tl H; #tl 336 normalize in ⊢ (∀_: %. ?) 337 # H 338 whd 339 normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]) 340 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 341 qed. 342 343 definition product_elim ≝ 344 λm, n: nat. 345 λv: Vector addressing_mode_tag (S m). 346 λq: Vector addressing_mode_tag (S n). 347 λP: (Vector addressing_mode_tag (S m) × (Vector addressing_mode_tag (S n))) → bool. 348 P 〈v, q〉. 349 350 axiom union_elim: 351 ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool. 268 352 269 353 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ 270 λP. 271 P (ADD … ACC_A 272 P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. 273 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % 274 qed. 275 % 276 qed. 354 λP. 355 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧ 356 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧ 357 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧ 358 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧ 359 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧ 360 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧ 361 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧ 362 list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. P (DJNZ ? ? addr)) ∧ 363 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧ 364 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧ 365 P (DA ? ACC_A) ∧ 366 P (JC ? ?) ∧ 367 P (JNC ? ?) ∧ 368 P (JZ ? ?) ∧ 369 P (JNZ ? ?) ∧ 370 P (JB ? (BIT_ADDR ?) ?) ∧ 371 P (JNB ? [[ bit_addr ]] ?) ∧ 372 P (JBC ? [[ bit_addr ]] ?) ∧ 373 P (RL ? ACC_A). 374 375 376 377 378 379 380 list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)). 381 382 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧ 383 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧ 384 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧ 385 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RL ? addr)) ∧ 386 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RLC ? addr)) ∧ 387 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RR ? addr)) ∧ 388 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RRC ? addr)) ∧ 389 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧ 390 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧ 391 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧ 392 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧ 393 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧ 394 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧ 395 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧ 396 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧ 397 P (RET ?) ∧ 398 P (RETI ?) ∧ 399 P (NOP ?). 277 400 278 401 … … 298 421  @ (instruction_elim INSTR) 299 422 ]. 300 *)301 423 302 424 (* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset
for help on using the changeset viewer.