Changeset 465 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Jan 20, 2011, 6:10:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r439 r465 7 7 include "BitVectorTrie.ma". 8 8 9 ndefinition Time ≝ Nat.9 ndefinition Time ≝ nat. 10 10 11 11 ninductive SerialBufferType: Type[0] ≝ … … 44 44 λs: SFR8051. 45 45 match s with 46 [ SFR_SP ⇒ Z47  SFR_DPL ⇒ S Z48  SFR_DPH ⇒ two49  SFR_PCON ⇒ three50  SFR_TCON ⇒ four51  SFR_TMOD ⇒ five52  SFR_TL0 ⇒ six53  SFR_TL1 ⇒ seven54  SFR_TH0 ⇒ eight55  SFR_TH1 ⇒ nine56  SFR_P1 ⇒ ten57  SFR_SCON ⇒ eleven58  SFR_SBUF ⇒ twelve59  SFR_IE ⇒ thirteen60  SFR_P3 ⇒ fourteen61  SFR_IP ⇒ fifteen62  SFR_PSW ⇒ sixteen63  SFR_ACC_A ⇒ seventeen64  SFR_ACC_B ⇒ eighteen46 [ SFR_SP ⇒ O 47  SFR_DPL ⇒ 1 48  SFR_DPH ⇒ 2 49  SFR_PCON ⇒ 3 50  SFR_TCON ⇒ 4 51  SFR_TMOD ⇒ 5 52  SFR_TL0 ⇒ 6 53  SFR_TL1 ⇒ 7 54  SFR_TH0 ⇒ 8 55  SFR_TH1 ⇒ 9 56  SFR_P1 ⇒ 10 57  SFR_SCON ⇒ 11 58  SFR_SBUF ⇒ 12 59  SFR_IE ⇒ 13 60  SFR_P3 ⇒ 14 61  SFR_IP ⇒ 15 62  SFR_PSW ⇒ 16 63  SFR_ACC_A ⇒ 17 64  SFR_ACC_B ⇒ 18 65 65 ]. 66 66 … … 75 75 λs: SFR8052. 76 76 match s with 77 [ SFR_T2CON ⇒ Z78  SFR_RCAP2L ⇒ S Z79  SFR_RCAP2H ⇒ two80  SFR_TL2 ⇒ three81  SFR_TH2 ⇒ four77 [ SFR_T2CON ⇒ O 78  SFR_RCAP2L ⇒ 1 79  SFR_RCAP2H ⇒ 2 80  SFR_TL2 ⇒ 3 81  SFR_TH2 ⇒ 4 82 82 ]. 83 83 … … 87 87 nrecord Status: Type[0] ≝ 88 88 { 89 code_memory: BitVectorTrie Byte sixteen;90 low_internal_ram: BitVectorTrie Byte seven;91 high_internal_ram: BitVectorTrie Byte seven;92 external_ram: BitVectorTrie Byte sixteen;89 code_memory: BitVectorTrie Byte 16; 90 low_internal_ram: BitVectorTrie Byte 7; 91 high_internal_ram: BitVectorTrie Byte 7; 92 external_ram: BitVectorTrie Byte 16; 93 93 94 94 program_counter: Word; 95 95 96 special_function_registers_8051: Vector Byte nineteen;97 special_function_registers_8052: Vector Byte five;96 special_function_registers_8051: Vector Byte 19; 97 special_function_registers_8052: Vector Byte 5; 98 98 99 99 p1_latch: Byte; … … 103 103 }. 104 104 105 nlemma sfr8051_index_ nineteen:105 nlemma sfr8051_index_19: 106 106 ∀i: SFR8051. 107 sfr_8051_index i < nineteen.108 #i; ncases i; nnormalize; nrepeat (napply le ss_than_or_equal_monotone);109 napply le ss_than_or_equal_zero.107 sfr_8051_index i < 19. 108 #i; ncases i; nnormalize; nrepeat (napply le_S_S); 109 napply le_O_n. 110 110 nqed. 111 111 112 nlemma sfr8052_index_ five:112 nlemma sfr8052_index_5: 113 113 ∀i: SFR8052. 114 sfr_8052_index i < five.115 #i; ncases i; nnormalize; nrepeat (napply le ss_than_or_equal_monotone);116 napply le ss_than_or_equal_zero.114 sfr_8052_index i < 5. 115 #i; ncases i; nnormalize; nrepeat (napply le_S_S); 116 napply le_O_n. 117 117 nqed. 118 118 … … 192 192 let index ≝ sfr_8051_index i in 193 193 get_index_v … sfr index ?. 194 napply sfr8051_index_ nineteen.194 napply sfr8051_index_19. 195 195 nqed. 196 196 … … 201 201 let index ≝ sfr_8052_index i in 202 202 get_index_v … sfr index ?. 203 napply sfr8052_index_ five.203 napply sfr8052_index_5. 204 204 nqed. 205 205 … … 217 217 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 218 218 let new_special_function_registers_8051 ≝ 219 set_index Byte nineteenold_special_function_registers_8051 index b ? in219 set_index Byte 19 old_special_function_registers_8051 index b ? in 220 220 let old_p1_latch ≝ p1_latch s in 221 221 let old_p3_latch ≝ p3_latch s in … … 231 231 old_p3_latch 232 232 old_clock. 233 napply (sfr8051_index_ nineteeni).233 napply (sfr8051_index_19 i). 234 234 nqed. 235 235 … … 247 247 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 248 248 let new_special_function_registers_8052 ≝ 249 set_index Byte fiveold_special_function_registers_8052 index b ? in249 set_index Byte 5 old_special_function_registers_8052 index b ? in 250 250 let old_p1_latch ≝ p1_latch s in 251 251 let old_p3_latch ≝ p3_latch s in … … 261 261 old_p3_latch 262 262 old_clock. 263 napply (sfr8052_index_ fivei).263 napply (sfr8052_index_5 i). 264 264 nqed. 265 265 … … 289 289 ndefinition set_code_memory ≝ 290 290 λs: Status. 291 λr: BitVectorTrie Byte sixteen.291 λr: BitVectorTrie Byte 16. 292 292 let old_low_internal_ram ≝ low_internal_ram s in 293 293 let old_high_internal_ram ≝ high_internal_ram s in … … 312 312 ndefinition set_low_internal_ram ≝ 313 313 λs: Status. 314 λr: BitVectorTrie Byte seven.314 λr: BitVectorTrie Byte 7. 315 315 let old_code_memory ≝ code_memory s in 316 316 let old_high_internal_ram ≝ high_internal_ram s in … … 335 335 ndefinition set_high_internal_ram ≝ 336 336 λs: Status. 337 λr: BitVectorTrie Byte seven.337 λr: BitVectorTrie Byte 7. 338 338 let old_code_memory ≝ code_memory s in 339 339 let old_low_internal_ram ≝ low_internal_ram s in … … 359 359 ndefinition set_external_ram ≝ 360 360 λs: Status. 361 λr: BitVectorTrie Byte sixteen.361 λr: BitVectorTrie Byte 16. 362 362 let old_code_memory ≝ code_memory s in 363 363 let old_low_internal_ram ≝ low_internal_ram s in … … 383 383 λs: Status. 384 384 let sfr ≝ special_function_registers_8051 s in 385 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v Bool eight psw Z ?. 387 nnormalize. 388 napply (less_than_or_equal_monotone ? ?). 389 napply (less_than_or_equal_zero). 390 nrepeat (napply (less_than_or_equal_monotone ? ?)). 391 napply (less_than_or_equal_zero). 385 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v bool 8 psw O ?. 387 nnormalize; 388 napply (le_S_S ? ?); 389 ##[ napply le_O_n; 390 ## nrepeat (napply (le_S_S)); 391 //; 392 ##] 392 393 nqed. 393 394 … … 395 396 λs: Status. 396 397 let sfr ≝ special_function_registers_8051 s in 397 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 398 get_index_v Bool eight psw (S Z) ?. 399 nnormalize. 400 nrepeat (napply (less_than_or_equal_monotone ? ?)). 401 napply (less_than_or_equal_zero). 402 nrepeat (napply (less_than_or_equal_monotone ? ?)). 403 napply (less_than_or_equal_zero). 398 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 399 get_index_v bool 8 psw (S O) ?. 400 nnormalize; 401 nrepeat (napply (le_S_S ? ?)); 402 napply le_O_n; 404 403 nqed. 405 404 … … 407 406 λs: Status. 408 407 let sfr ≝ special_function_registers_8051 s in 409 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 410 get_index_v Bool eight psw two ?. 411 nnormalize. 412 nrepeat (napply (less_than_or_equal_monotone ? ?)). 413 napply (less_than_or_equal_zero). 414 nrepeat (napply (less_than_or_equal_monotone ? ?)). 415 napply (less_than_or_equal_zero). 408 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 409 get_index_v bool 8 psw 2 ?. 410 nnormalize; 411 nrepeat (napply (le_S_S ? ?)); 412 napply le_O_n; 416 413 nqed. 417 414 … … 419 416 λs: Status. 420 417 let sfr ≝ special_function_registers_8051 s in 421 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 422 get_index_v Bool eight psw three ?. 423 nnormalize. 424 nrepeat (napply (less_than_or_equal_monotone ? ?)). 425 napply (less_than_or_equal_zero). 426 nrepeat (napply (less_than_or_equal_monotone ? ?)). 427 napply (less_than_or_equal_zero). 418 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 419 get_index_v bool 8 psw 3 ?. 420 nnormalize; 421 nrepeat (napply (le_S_S ? ?)); 422 napply le_O_n; 428 423 nqed. 429 424 … … 431 426 λs: Status. 432 427 let sfr ≝ special_function_registers_8051 s in 433 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 434 get_index_v Bool eight psw four ?. 435 nnormalize. 436 nrepeat (napply (less_than_or_equal_monotone ? ?)). 437 napply (less_than_or_equal_zero). 438 nrepeat (napply (less_than_or_equal_monotone ? ?)). 439 napply (less_than_or_equal_zero). 428 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 429 get_index_v bool 8 psw 4 ?. 430 nnormalize; 431 nrepeat (napply (le_S_S ? ?)); 432 napply le_O_n; 440 433 nqed. 441 434 … … 443 436 λs: Status. 444 437 let sfr ≝ special_function_registers_8051 s in 445 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 446 get_index_v Bool eight psw five ?. 447 nnormalize. 448 nrepeat (napply (less_than_or_equal_monotone ? ?)). 449 napply (less_than_or_equal_zero). 450 nrepeat (napply (less_than_or_equal_monotone ? ?)). 451 napply (less_than_or_equal_zero). 438 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 439 get_index_v bool 8 psw 5 ?. 440 nnormalize; 441 nrepeat (napply (le_S_S ? ?)); 442 napply le_O_n; 452 443 nqed. 453 444 … … 455 446 λs: Status. 456 447 let sfr ≝ special_function_registers_8051 s in 457 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 458 get_index_v Bool eight psw six ?. 459 nnormalize. 460 nrepeat (napply (less_than_or_equal_monotone ? ?)). 461 napply (less_than_or_equal_zero). 462 nrepeat (napply (less_than_or_equal_monotone ? ?)). 463 napply (less_than_or_equal_zero). 448 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 449 get_index_v bool 8 psw 6 ?. 450 nnormalize; 451 nrepeat (napply (le_S_S ? ?)); 452 napply le_O_n; 464 453 nqed. 465 454 … … 467 456 λs: Status. 468 457 let sfr ≝ special_function_registers_8051 s in 469 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 470 get_index_v Bool eight psw seven ?. 471 nnormalize. 472 nrepeat (napply (less_than_or_equal_monotone ? ?)). 473 napply (less_than_or_equal_zero). 474 nrepeat (napply (less_than_or_equal_monotone ? ?)). 475 napply (less_than_or_equal_zero). 458 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 459 get_index_v bool 8 psw 7 ?. 460 nnormalize; 461 nrepeat (napply (le_S_S ? ?)); 462 napply le_O_n; 476 463 nqed. 477 464 … … 479 466 λs: Status. 480 467 λcy: Bit. 481 λac: MaybeBit.468 λac: option Bit. 482 469 λov: Bit. 483 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_PSW) in484 let old_cy ≝ get_index_v… nu Z? in485 let old_ac ≝ get_index_v… nu one? in486 let old_fo ≝ get_index_v… nu two? in487 let old_rs1 ≝ get_index_v… nu three? in488 let old_rs0 ≝ get_index_v… nl Z? in489 let old_ov ≝ get_index_v… nl one? in490 let old_ud ≝ get_index_v… nl two? in491 let old_p ≝ get_index_v… nl three? in492 let new_ac ≝ match ac with [ No thing ⇒ old_ac  Justj ⇒ j ] in470 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in 471 let old_cy ≝ get_index_v… nu O ? in 472 let old_ac ≝ get_index_v… nu 1 ? in 473 let old_fo ≝ get_index_v… nu 2 ? in 474 let old_rs1 ≝ get_index_v… nu 3 ? in 475 let old_rs0 ≝ get_index_v… nl O ? in 476 let old_ov ≝ get_index_v… nl 1 ? in 477 let old_ud ≝ get_index_v… nl 2 ? in 478 let old_p ≝ get_index_v… nl 3 ? in 479 let new_ac ≝ match ac with [ None ⇒ old_ac  Some j ⇒ j ] in 493 480 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 494 481 old_rs0 ; old_ov ; old_ud ; old_p ]] in … … 496 483 ##[##1,2,3,4,5,6,7,8: 497 484 nnormalize; 498 nrepeat (napply le ss_than_or_equal_monotone);499 napply (le ss_than_or_equal_zero);485 nrepeat (napply le_S_S); 486 napply (le_O_n); 500 487 ##] 501 488 nqed. 502 489 503 490 ndefinition initialise_status ≝ 504 let status ≝ mk_Status (Stub Byte sixteen) (* Code mem. *)505 (Stub Byte seven) (* Low mem. *)506 (Stub Byte seven) (* High mem. *)507 (Stub Byte sixteen) (* Ext mem. *)508 (zero sixteen) (* PC. *)509 (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)510 (replicate Byte five (zero eight)) (* 8052 SFR. *)511 (zero eight) (* P1 latch. *)512 (zero eight) (* P3 latch. *)513 Z(* Clock. *)491 let status ≝ mk_Status (Stub Byte 16) (* Code mem. *) 492 (Stub Byte 7) (* Low mem. *) 493 (Stub Byte 7) (* High mem. *) 494 (Stub Byte 16) (* Ext mem. *) 495 (zero 16) (* PC. *) 496 (replicate Byte 19 (zero 8)) (* 8051 SFR. *) 497 (replicate Byte 5 (zero 8)) (* 8052 SFR. *) 498 (zero 8) (* P1 latch. *) 499 (zero 8) (* P3 latch. *) 500 O (* Clock. *) 514 501 in 515 set_8051_sfr status SFR_SP (bitvector_of_nat eight seven).502 set_8051_sfr status SFR_SP (bitvector_of_nat 8 7). 516 503 517 504 naxiom not_implemented: False. … … 519 506 ndefinition get_bit_addressable_sfr ≝ 520 507 λs: Status. 521 λn: Nat.508 λn: nat. 522 509 λb: BitVector n. 523 λl: Bool.510 λl: bool. 524 511 let address ≝ nat_of_bitvector … b in 525 if (eq _n address one_hundred_and_twenty_eight) then512 if (eqb address 128) then 526 513 ? 527 else if (eq _n address one_hundred_and_forty_four) then514 else if (eqb address 144) then 528 515 if l then 529 516 (p1_latch s) 530 517 else 531 518 (get_8051_sfr s SFR_P1) 532 else if (eq _n address one_hundred_and_sixty) then519 else if (eqb address 160) then 533 520 ? 534 else if (eq _n address one_hundred_and_seventy_six) then521 else if (eqb address 176) then 535 522 if l then 536 523 (p3_latch s) 537 524 else 538 525 (get_8051_sfr s SFR_P3) 539 else if (eq _n address one_hundred_and_fifty_three) then526 else if (eqb address 153) then 540 527 get_8051_sfr s SFR_SBUF 541 else if (eq _n address one_hundred_and_thirty_eight) then528 else if (eqb address 138) then 542 529 get_8051_sfr s SFR_TL0 543 else if (eq _n address one_hundred_and_thirty_nine) then530 else if (eqb address 139) then 544 531 get_8051_sfr s SFR_TL1 545 else if (eq _n address one_hundred_and_forty) then532 else if (eqb address 140) then 546 533 get_8051_sfr s SFR_TH0 547 else if (eq _n address one_hundred_and_forty_one) then534 else if (eqb address 141) then 548 535 get_8051_sfr s SFR_TH1 549 else if (eq _n address two_hundred) then536 else if (eqb address 200) then 550 537 get_8052_sfr s SFR_T2CON 551 else if (eq _n address two_hundred_and_two) then538 else if (eqb address 202) then 552 539 get_8052_sfr s SFR_RCAP2L 553 else if (eq _n address two_hundred_and_three) then540 else if (eqb address 203) then 554 541 get_8052_sfr s SFR_RCAP2H 555 else if (eq _n address two_hundred_and_four) then542 else if (eqb address 204) then 556 543 get_8052_sfr s SFR_TL2 557 else if (eq _n address two_hundred_and_five) then544 else if (eqb address 205) then 558 545 get_8052_sfr s SFR_TH2 559 else if (eq _n address one_hundred_and_thirty_five) then546 else if (eqb address 135) then 560 547 get_8051_sfr s SFR_PCON 561 else if (eq _n address one_hundred_and_thirty_six) then548 else if (eqb address 136) then 562 549 get_8051_sfr s SFR_TCON 563 else if (eq _n address one_hundred_and_thirty_seven) then550 else if (eqb address 137) then 564 551 get_8051_sfr s SFR_TMOD 565 else if (eq _n address one_hundred_and_fifty_two) then552 else if (eqb address 152) then 566 553 get_8051_sfr s SFR_SCON 567 else if (eq _n address one_hundred_and_sixty_eight) then554 else if (eqb address 168) then 568 555 get_8051_sfr s SFR_IE 569 else if (eq _n address one_hundred_and_eighty_four) then556 else if (eqb address 184) then 570 557 get_8051_sfr s SFR_IP 571 else if (eq _n address one_hundred_and_twenty_nine) then558 else if (eqb address 129) then 572 559 get_8051_sfr s SFR_SP 573 else if (eq _n address one_hundred_and_thirty) then560 else if (eqb address 130) then 574 561 get_8051_sfr s SFR_DPL 575 else if (eq _n address one_hundred_and_thirty_one) then562 else if (eqb address 131) then 576 563 get_8051_sfr s SFR_DPH 577 else if (eq _n address two_hundred_and_eight) then564 else if (eqb address 208) then 578 565 get_8051_sfr s SFR_PSW 579 else if (eq _n address two_hundred_and_twenty_four) then566 else if (eqb address 224) then 580 567 get_8051_sfr s SFR_ACC_A 581 else if (eq _n address two_hundred_and_forty) then568 else if (eqb address 240) then 582 569 get_8051_sfr s SFR_ACC_B 583 570 else … … 591 578 λv: Byte. 592 579 let address ≝ nat_of_bitvector … b in 593 if (eq _n address one_hundred_and_twenty_eight) then580 if (eqb address 128) then 594 581 ? 595 else if (eq _n address one_hundred_and_forty_four) then582 else if (eqb address 144) then 596 583 let status_1 ≝ set_8051_sfr s SFR_P1 v in 597 584 let status_2 ≝ set_p1_latch s v in 598 585 status_2 599 else if (eq _n address one_hundred_and_sixty) then586 else if (eqb address 160) then 600 587 ? 601 else if (eq _n address one_hundred_and_seventy_six) then588 else if (eqb address 176) then 602 589 let status_1 ≝ set_8051_sfr s SFR_P3 v in 603 590 let status_2 ≝ set_p3_latch s v in 604 591 status_2 605 else if (eq _n address one_hundred_and_fifty_three) then592 else if (eqb address 153) then 606 593 set_8051_sfr s SFR_SBUF v 607 else if (eq _n address one_hundred_and_thirty_eight) then594 else if (eqb address 138) then 608 595 set_8051_sfr s SFR_TL0 v 609 else if (eq _n address one_hundred_and_thirty_nine) then596 else if (eqb address 139) then 610 597 set_8051_sfr s SFR_TL1 v 611 else if (eq _n address one_hundred_and_forty) then598 else if (eqb address 140) then 612 599 set_8051_sfr s SFR_TH0 v 613 else if (eq _n address one_hundred_and_forty_one) then600 else if (eqb address 141) then 614 601 set_8051_sfr s SFR_TH1 v 615 else if (eq _n address two_hundred) then602 else if (eqb address 200) then 616 603 set_8052_sfr s SFR_T2CON v 617 else if (eq _n address two_hundred_and_two) then604 else if (eqb address 202) then 618 605 set_8052_sfr s SFR_RCAP2L v 619 else if (eq _n address two_hundred_and_three) then606 else if (eqb address 203) then 620 607 set_8052_sfr s SFR_RCAP2H v 621 else if (eq _n address two_hundred_and_four) then608 else if (eqb address 204) then 622 609 set_8052_sfr s SFR_TL2 v 623 else if (eq _n address two_hundred_and_five) then610 else if (eqb address 205) then 624 611 set_8052_sfr s SFR_TH2 v 625 else if (eq _n address one_hundred_and_thirty_five) then612 else if (eqb address 135) then 626 613 set_8051_sfr s SFR_PCON v 627 else if (eq _n address one_hundred_and_thirty_six) then614 else if (eqb address 136) then 628 615 set_8051_sfr s SFR_TCON v 629 else if (eq _n address one_hundred_and_thirty_seven) then616 else if (eqb address 137) then 630 617 set_8051_sfr s SFR_TMOD v 631 else if (eq _n address one_hundred_and_fifty_two) then618 else if (eqb address 152) then 632 619 set_8051_sfr s SFR_SCON v 633 else if (eq _n address one_hundred_and_sixty_eight) then620 else if (eqb address 168) then 634 621 set_8051_sfr s SFR_IE v 635 else if (eq _n address one_hundred_and_eighty_four) then622 else if (eqb address 184) then 636 623 set_8051_sfr s SFR_IP v 637 else if (eq _n address one_hundred_and_twenty_nine) then624 else if (eqb address 129) then 638 625 set_8051_sfr s SFR_SP v 639 else if (eq _n address one_hundred_and_thirty) then626 else if (eqb address 130) then 640 627 set_8051_sfr s SFR_DPL v 641 else if (eq _n address one_hundred_and_thirty_one) then628 else if (eqb address 131) then 642 629 set_8051_sfr s SFR_DPH v 643 else if (eq _n address two_hundred_and_eight) then630 else if (eqb address 208) then 644 631 set_8051_sfr s SFR_PSW v 645 else if (eq _n address two_hundred_and_twenty_four) then632 else if (eqb address 224) then 646 633 set_8051_sfr s SFR_ACC_A v 647 else if (eq _n address two_hundred_and_forty) then634 else if (eqb address 240) then 648 635 set_8051_sfr s SFR_ACC_B v 649 636 else … … 654 641 ndefinition bit_address_of_register ≝ 655 642 λs: Status. 656 λr: BitVector three.657 let b ≝ get_index_v … r Z? in658 let c ≝ get_index_v … r one? in659 let d ≝ get_index_v … r two? in660 let 〈 un, ln 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in661 let 〈 r1, r0 〉 ≝ mk_ Cartesian … (get_index_v … four un two ?) (get_index_v … four un three?) in643 λr: BitVector 3. 644 let b ≝ get_index_v … r O ? in 645 let c ≝ get_index_v … r 1 ? in 646 let d ≝ get_index_v … r 2 ? in 647 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 648 let 〈 r1, r0 〉 ≝ mk_pair … (get_index_v … 4 un 2 ?) (get_index_v … 4 un 3 ?) in 662 649 let offset ≝ 663 if conjunction (negation r1) (negation r0)then664 Z665 else if conjunction (negation r1)r0 then666 eight667 else if conjunction r1r0 then668 twenty_four650 if ¬r1 ∧ ¬r0 then 651 O 652 else if ¬r1 ∧ r0 then 653 8 654 else if r1 ∧ r0 then 655 24 669 656 else 670 sixteen657 16 671 658 in 672 bitvector_of_nat seven(offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).659 bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). 673 660 ##[##1,2,3,4,5: 674 661 nnormalize; 675 nrepeat (napply le ss_than_or_equal_monotone);676 napply le ss_than_or_equal_zero;662 nrepeat (napply le_S_S); 663 napply le_O_n; 677 664 ##] 678 665 nqed. … … 680 667 ndefinition get_register ≝ 681 668 λs: Status. 682 λr: BitVector three.669 λr: BitVector 3. 683 670 let address ≝ bit_address_of_register s r in 684 lookup … address (low_internal_ram s) (zero eight).671 lookup … address (low_internal_ram s) (zero 8). 685 672 686 673 ndefinition set_register ≝ 687 674 λs: Status. 688 λr: BitVector three.675 λr: BitVector 3. 689 676 λv: Byte. 690 677 let address ≝ bit_address_of_register s r in … … 695 682 ndefinition read_at_stack_pointer ≝ 696 683 λs: Status. 697 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_SP) in698 let m ≝ get_index_v … nu Z? in699 let r1 ≝ get_index_v … nu one? in700 let r2 ≝ get_index_v … nu two? in701 let r3 ≝ get_index_v … nu three? in684 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in 685 let m ≝ get_index_v … nu O ? in 686 let r1 ≝ get_index_v … nu 1 ? in 687 let r2 ≝ get_index_v … nu 2 ? in 688 let r3 ≝ get_index_v … nu 3 ? in 702 689 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 703 690 let memory ≝ … … 707 694 (high_internal_ram s) 708 695 in 709 lookup … address memory (zero eight).710 711 712 nrepeat (napply less_than_or_equal_monotone);713 napply less_than_or_equal_zero;714 696 lookup … address memory (zero 8). 697 ##[##1,2,3,4: 698 nnormalize; 699 nrepeat (napply le_S_S); 700 napply le_O_n; 701 ##] 715 702 nqed. 716 703 … … 718 705 λs: Status. 719 706 λv: Byte. 720 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_SP) in721 let bit_zero ≝ get_index_v… nu Z? in722 let bit_ one ≝ get_index_v… nu one? in723 let bit_ two ≝ get_index_v… nu two? in724 let bit_ three ≝ get_index_v… nu three? in707 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in 708 let bit_zero ≝ get_index_v… nu O ? in 709 let bit_1 ≝ get_index_v… nu 1 ? in 710 let bit_2 ≝ get_index_v… nu 2 ? in 711 let bit_3 ≝ get_index_v… nu 3 ? in 725 712 if bit_zero then 726 let memory ≝ insert … ([[ bit_ one ; bit_two ; bit_three]] @@ nl)713 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 727 714 v (low_internal_ram s) in 728 715 set_low_internal_ram s memory 729 716 else 730 let memory ≝ insert … ([[ bit_ one ; bit_two ; bit_three]] @@ nl)717 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 731 718 v (high_internal_ram s) in 732 719 set_high_internal_ram s memory. 733 734 735 nrepeat (napply less_than_or_equal_monotone);736 napply less_than_or_equal_zero;737 720 ##[##1,2,3,4: 721 nnormalize; 722 nrepeat (napply le_S_S); 723 napply le_O_n; 724 ##] 738 725 nqed. 739 726 … … 742 729 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with 743 730 [ DPTR ⇒ λ_:True. 744 let 〈 bu, bl 〉 ≝ split … eight eightv in731 let 〈 bu, bl 〉 ≝ split … 8 8 v in 745 732 let status ≝ set_8051_sfr s SFR_DPH bu in 746 733 let status ≝ set_8051_sfr status SFR_DPL bl in … … 762 749 ] (subaddressing_modein … a). 763 750 764 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;751 ndefinition get_arg_8: Status → bool → [[ direct ; indirect ; register ; 765 752 acc_a ; acc_b ; data ; acc_dptr ; 766 753 acc_pc ; ext_indirect ; … … 778 765 λext_indirect_dptr: True. 779 766 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 780 lookup … sixteen address (external_ram s) (zero eight)767 lookup … 16 address (external_ram s) (zero 8) 781 768  EXT_INDIRECT e ⇒ 782 769 λext_indirect: True. 783 770 let address ≝ get_register s [[ false; false; e ]] in 784 let padded_address ≝ pad eight eightaddress in785 lookup … sixteen padded_address (external_ram s) (zero eight)771 let padded_address ≝ pad 8 8 address in 772 lookup … 16 padded_address (external_ram s) (zero 8) 786 773  ACC_DPTR ⇒ 787 774 λacc_dptr: True. 788 775 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 789 let padded_acc ≝ pad eight eight(get_8051_sfr s SFR_ACC_A) in790 let 〈 carry, address 〉 ≝ half_add sixteendptr padded_acc in791 lookup … sixteen address (external_ram s) (zero eight)776 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in 777 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 778 lookup … 16 address (external_ram s) (zero 8) 792 779  ACC_PC ⇒ 793 780 λacc_pc: True. 794 let padded_acc ≝ pad eight eight(get_8051_sfr s SFR_ACC_A) in795 let 〈 carry, address 〉 ≝ half_add sixteen(program_counter s) padded_acc in796 lookup … sixteen address (external_ram s) (zero eight)781 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in 782 let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in 783 lookup … 16 address (external_ram s) (zero 8) 797 784  DIRECT d ⇒ 798 785 λdirect: True. 799 let 〈 nu, nl 〉 ≝ split … four fourd in800 let bit_ one ≝ get_index_v … nu one? in801 match bit_ onewith786 let 〈 nu, nl 〉 ≝ split … 4 4 d in 787 let bit_1 ≝ get_index_v … nu 1 ? in 788 match bit_1 with 802 789 [ true ⇒ 803 let 〈 bit_one, three_bits 〉 ≝ split ? one threenu in790 let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in 804 791 let address ≝ three_bits @@ nl in 805 lookup ? seven address (low_internal_ram s) (zero eight)806  false ⇒ get_bit_addressable_sfr s eightd l792 lookup ? 7 address (low_internal_ram s) (zero 8) 793  false ⇒ get_bit_addressable_sfr s 8 d l 807 794 ] 808 795  INDIRECT i ⇒ 809 796 λindirect: True. 810 let 〈 nu, nl 〉 ≝ split ? four four(get_register s [[ false; false; i]]) in811 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in812 let bit_ one ≝ get_index_v … bit_one_v Z? in813 match bit_ onewith797 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in 798 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 799 let bit_1 ≝ get_index_v … bit_one_v O ? in 800 match bit_1 with 814 801 [ true ⇒ 815 lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)802 lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8) 816 803  false ⇒ 817 lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)804 lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8) 818 805 ] 819 806  _ ⇒ λother. … … 822 809 ##[##1,2: 823 810 nnormalize; 824 nrepeat (napply le ss_than_or_equal_monotone);825 napply le ss_than_or_equal_zero;811 nrepeat (napply le_S_S); 812 napply le_O_n; 826 813 ##] 827 814 nqed. … … 836 823 [ DIRECT d ⇒ 837 824 λdirect: True. 838 let 〈 nu, nl 〉 ≝ split … four fourd in839 let bit_ one ≝ get_index_v … nu one? in840 let 〈 ignore, three_bits 〉 ≝ split ? one threenu in841 match bit_ onewith825 let 〈 nu, nl 〉 ≝ split … 4 4 d in 826 let bit_1 ≝ get_index_v … nu 1 ? in 827 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 828 match bit_1 with 842 829 [ true ⇒ set_bit_addressable_sfr s d v 843 830  false ⇒ 844 let memory ≝ insert ? seven(three_bits @@ nl) v (low_internal_ram s) in831 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in 845 832 set_low_internal_ram s memory 846 833 ] … … 848 835 λindirect: True. 849 836 let register ≝ get_register s [[ false; false; i ]] in 850 let 〈nu, nl〉 ≝ split ? four fourregister in851 let bit_ one ≝ get_index_v … nu one? in852 let 〈ignore, three_bits〉 ≝ split ? one threenu in853 match bit_ onewith837 let 〈nu, nl〉 ≝ split ? 4 4 register in 838 let bit_1 ≝ get_index_v … nu 1 ? in 839 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in 840 match bit_1 with 854 841 [ true ⇒ 855 842 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in … … 865 852 λext_indirect: True. 866 853 let address ≝ get_register s [[ false; false; e ]] in 867 let padded_address ≝ pad eight eightaddress in868 let memory ≝ insert ? sixteenpadded_address v (external_ram s) in854 let padded_address ≝ pad 8 8 address in 855 let memory ≝ insert ? 16 padded_address v (external_ram s) in 869 856 set_external_ram s memory 870 857  EXT_INDIRECT_DPTR ⇒ 871 858 λext_indirect_dptr: True. 872 859 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 873 let memory ≝ insert ? sixteenaddress v (external_ram s) in860 let memory ≝ insert ? 16 address v (external_ram s) in 874 861 set_external_ram s memory 875 862  _ ⇒ … … 879 866 ##[##1,2: 880 867 nnormalize; 881 nrepeat (napply le ss_than_or_equal_monotone);882 napply le ss_than_or_equal_zero868 nrepeat (napply le_S_S); 869 napply le_O_n 883 870 ##] 884 871 nqed. 885 872 886 873 ntheorem modulus_less_than: 887 ∀m,n: Nat. (m mod (S n)) < S n.888 #n m; nnormalize; napply le ss_than_or_equal_monotone;889 nlapply (l toe_refln);874 ∀m,n: nat. (m mod (S n)) < S n. 875 #n m; nnormalize; napply le_S_S; 876 nlapply (le_n n); 890 877 ngeneralize in ⊢ (?%? → ?(??%?)?); 891 878 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?) … … 895 882 [ //  #K; napply H1; ncut (n ≤ S y → n  S m ≤ y); /2/; 896 883 ncases n; nnormalize; //; 897 #x K1; nlapply (le ss_than_or_equal_injective … K1); ngeneralize in match m;884 #x K1; nlapply (le_S_S_to_le … K1); ngeneralize in match m; 898 885 nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //; 899 886 #q K2; napply H; /3/] … … 901 888 902 889 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → 903 Bool → Bool ≝890 bool → bool ≝ 904 891 λs, a, l. 905 892 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; … … 908 895 [ BIT_ADDR b ⇒ 909 896 λbit_addr: True. 910 let 〈 nu, nl 〉 ≝ split … four fourb in911 let bit_ one ≝ get_index_v … nu one? in912 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in913 match bit_ onewith897 let 〈 nu, nl 〉 ≝ split … 4 4 b in 898 let bit_1 ≝ get_index_v … nu 1 ? in 899 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 900 match bit_1 with 914 901 [ true ⇒ 915 902 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 916 let d ≝ address ÷ eightin917 let m ≝ address mod eightin918 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in903 let d ≝ address ÷ 8 in 904 let m ≝ address mod 8 in 905 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 919 906 let sfr ≝ get_bit_addressable_sfr s ? trans l in 920 907 get_index_v … sfr m ? 921 908  false ⇒ 922 909 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 923 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in924 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in925 get_index_v … t (modulus address eight) ?910 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 911 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 912 get_index_v … t (modulus address 8) ? 926 913 ] 927 914  N_BIT_ADDR n ⇒ 928 915 λn_bit_addr: True. 929 let 〈 nu, nl 〉 ≝ split … four fourn in930 let bit_ one ≝ get_index_v … nu one? in931 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in932 match bit_ onewith916 let 〈 nu, nl 〉 ≝ split … 4 4 n in 917 let bit_1 ≝ get_index_v … nu 1 ? in 918 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 919 match bit_1 with 933 920 [ true ⇒ 934 921 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 935 let d ≝ address ÷ eightin936 let m ≝ address mod eightin937 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in922 let d ≝ address ÷ 8 in 923 let m ≝ address mod 8 in 924 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 938 925 let sfr ≝ get_bit_addressable_sfr s ? trans l in 939 negation(get_index_v … sfr m ?)926 ¬(get_index_v … sfr m ?) 940 927  false ⇒ 941 928 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 942 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in943 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in944 negation (get_index_v … trans (modulus address eight) ?)929 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 930 let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 931 ¬(get_index_v … trans (modulus address 8) ?) 945 932 ] 946 933  CARRY ⇒ λcarry: True. get_cy_flag s … … 950 937 ##[##3,6: 951 938 nnormalize; 952 nrepeat (napply le ss_than_or_equal_monotone);953 napply le ss_than_or_equal_zero;939 nrepeat (napply le_S_S); 940 napply le_O_n; 954 941 ####1,2,4,5: 955 942 napply modulus_less_than; … … 962 949 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with 963 950 [ BIT_ADDR b ⇒ λbit_addr: True. 964 let 〈 nu, nl 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in965 let bit_ one ≝ get_index_v … nu one? in966 let 〈 ignore, three_bits 〉 ≝ split ? one threenu in967 match bit_ onewith951 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 952 let bit_1 ≝ get_index_v … nu 1 ? in 953 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 954 match bit_1 with 968 955 [ true ⇒ 969 956 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 970 let d ≝ address ÷ eightin971 let m ≝ address mod eightin972 let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in957 let d ≝ address ÷ 8 in 958 let m ≝ address mod 8 in 959 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 973 960 let sfr ≝ get_bit_addressable_sfr s ? t true in 974 961 let new_sfr ≝ set_index … sfr m v ? in … … 976 963  false ⇒ 977 964 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 978 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in979 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in980 let n_bit ≝ set_index … t (modulus address eight) v ? in981 let memory ≝ insert ? sevenaddress' n_bit (low_internal_ram s) in965 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 966 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 967 let n_bit ≝ set_index … t (modulus address 8) v ? in 968 let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in 982 969 set_low_internal_ram s memory 983 970 ] 984 971  CARRY ⇒ 985 972 λcarry: True. 986 let 〈 nu, nl 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in987 let bit_ one ≝ get_index_v… nu one? in988 let bit_ two ≝ get_index_v… nu two? in989 let bit_ three ≝ get_index_v… nu three? in990 let new_psw ≝ [[ v; bit_ one ; bit_two; bit_three]] @@ nl in973 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 974 let bit_1 ≝ get_index_v… nu 1 ? in 975 let bit_2 ≝ get_index_v… nu 2 ? in 976 let bit_3 ≝ get_index_v… nu 3 ? in 977 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 991 978 set_8051_sfr s SFR_PSW new_psw 992 979  _ ⇒ … … 997 984 ##[##1,2,3,6: 998 985 nnormalize; 999 nrepeat (napply le ss_than_or_equal_monotone);1000 napply le ss_than_or_equal_zero;986 nrepeat (napply le_S_S); 987 napply le_O_n; 1001 988 ####4,5: 1002 989 napply modulus_less_than; … … 1005 992 1006 993 ndefinition load_code_memory ≝ 1007 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).994 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). 1008 995 1009 996 ndefinition load ≝
Note: See TracChangeset
for help on using the changeset viewer.