 Timestamp:
 Jun 1, 2011, 5:32:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r871 r872 345 345 λv: Vector addressing_mode_tag (S m). 346 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. 352 353 (* 347 λP: (v × q) → bool. 348 list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)). 349 350 definition union_elim ≝ 351 λA, B: Type[0]. 352 λelimA: (A → bool) → bool. 353 λelimB: (B → bool) → bool. 354 λelimU: A ⊎ B → bool. 355 elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))). 356 354 357 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ 355 358 λP. … … 361 364 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧ 362 365 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧ 363 list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. P (DJNZ ? ? addr)) ∧366 list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ 364 367 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧ 365 368 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧ … … 381 384 P (RETI ?) ∧ 382 385 P (NOP ?) ∧ 386 bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧ 383 387 list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧ 384 388 bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧ 385 bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))). 386 387 388 389 390 391 list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)). 392 393 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧ 394 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧ 395 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧ 396 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧ 397 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧ 398 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧ 399 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧ 400 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧ 401 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧ 402 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧ 403 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧ 404 P (RET ?) ∧ 405 P (RETI ?) ∧ 406 P (NOP ?). 389 bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧ 390 union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]]) 391 (product_elim ? ? [[ registr; indirect ]] [[ data ]]) 392 (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧ 393 list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧ 394 union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]]) 395 (product_elim ? ? [[direct]] [[ acc_a ; data ]]) 396 (λd. P (XRL ? d)) ∧ 397 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) 398 (product_elim ? ? [[direct]] [[ acc_a ; data ]])) 399 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) 400 (λd. P (ANL ? d)) ∧ 401 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) 402 (product_elim ? ? [[direct]] [[ acc_a ; data ]])) 403 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) 404 (λd. P (ORL ? d)) ∧ 405 union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]]) 406 (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]]) 407 (λd. P (MOVX ? d)) ∧ 408 union_elim ? ? ( 409 union_elim ? ? ( 410 union_elim ? ? ( 411 union_elim ? ? ( 412 union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) 413 (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]])) 414 (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]])) 415 (product_elim ? ? [[dptr]] [[data16]])) 416 (product_elim ? ? [[carry]] [[bit_addr]])) 417 (product_elim ? ? [[bit_addr]] [[carry]]) 418 (λd. P (MOV ? d)). 419 % 420 qed. 407 421 408 409 axiom instruction_elim: ∀P: instruction → bool. bool. 410 411 412 lemma instruction_elim_correct: 413 ∀i: instruction. 414 ∀P: instruction → bool. 415 instruction_elim P = true → ∀j. P j = true. 416 422 definition instruction_elim: ∀P: instruction → bool. bool ≝ 423 λP. (* 424 bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧ 425 bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧ 426 bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧ 427 bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *) 428 bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (* ∧ 429 P (JMP INDIRECT_DPTR) ∧ 430 list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧ 431 preinstruction_elim (λp. P (RealInstruction p)). *) 432 % 433 qed. 434 435 436 axiom instruction_elim_complete: 437 ∀P. instruction_elim P = true → ∀i. P i = true. 438 439 definition eq_instruction ≝ 440 λi, j: instruction. 441 true. 442 (* 417 443 lemma test: 418 ∀i: instruction. 419 ∃pc. 420 let assembled ≝ assembly1 i in 421 let code_memory ≝ load_code_memory assembled in 422 let fetched ≝ fetch code_memory pc in 423 let 〈instr_pc, ticks〉 ≝ fetched in 424 \fst instr_pc = i. 425 # INSTR 426 @ (ex_intro ?) 427 [ @ (zero 16) 428  @ (instruction_elim INSTR) 429 ]. 430 *) 444 let i ≝ SJMP (RELATIVE (bitvector_of_nat 8 255)) in 445 (let assembled ≝ assembly1 i in 446 let code_memory ≝ load_code_memory assembled in 447 let fetched ≝ fetch code_memory ? in 448 let 〈instr_pc, ticks〉 ≝ fetched in 449 eq_instruction (\fst instr_pc)) i = true. 450 [2: @ zero 451  normalize 452 ]*) 453 454 lemma test: 455 ∀i. 456 (let assembled ≝ assembly1 i in 457 let code_memory ≝ load_code_memory assembled in 458 let fetched ≝ fetch code_memory ? in 459 let 〈instr_pc, ticks〉 ≝ fetched in 460 eq_instruction (\fst instr_pc)) i = true. 461 [ @ (instruction_elim_complete ) 462  @ zero 463 ] 464 normalize 465 431 466 432 467 (* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset
for help on using the changeset viewer.