Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (10 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Status.ma

    r439 r465  
    77include "BitVectorTrie.ma".
    88
    9 ndefinition Time ≝ Nat.
     9ndefinition Time ≝ nat.
    1010
    1111ninductive SerialBufferType: Type[0] ≝
     
    4444  λs: SFR8051.
    4545    match s with
    46       [ SFR_SP ⇒ Z
    47       | SFR_DPL ⇒ S Z
    48       | SFR_DPH ⇒ two
    49       | SFR_PCON ⇒ three
    50       | SFR_TCON ⇒ four
    51       | SFR_TMOD ⇒ five
    52       | SFR_TL0 ⇒ six
    53       | SFR_TL1 ⇒ seven
    54       | SFR_TH0 ⇒ eight
    55       | SFR_TH1 ⇒ nine
    56       | SFR_P1 ⇒ ten
    57       | SFR_SCON ⇒ eleven
    58       | SFR_SBUF ⇒ twelve
    59       | SFR_IE ⇒ thirteen
    60       | SFR_P3 ⇒ fourteen
    61       | SFR_IP ⇒ fifteen
    62       | SFR_PSW ⇒ sixteen
    63       | SFR_ACC_A ⇒ seventeen
    64       | SFR_ACC_B ⇒ eighteen
     46      [ 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
    6565      ].
    6666     
     
    7575  λs: SFR8052.
    7676    match s with
    77       [ SFR_T2CON ⇒ Z
    78       | SFR_RCAP2L ⇒ S Z
    79       | SFR_RCAP2H ⇒ two
    80       | SFR_TL2 ⇒ three
    81       | SFR_TH2 ⇒ four
     77      [ SFR_T2CON ⇒ O
     78      | SFR_RCAP2L ⇒ 1
     79      | SFR_RCAP2H ⇒ 2
     80      | SFR_TL2 ⇒ 3
     81      | SFR_TH2 ⇒ 4
    8282      ].
    8383
     
    8787nrecord Status: Type[0] ≝
    8888{
    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;
    9393 
    9494  program_counter: Word;
    9595 
    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;
    9898 
    9999  p1_latch: Byte;
     
    103103}.
    104104
    105 nlemma sfr8051_index_nineteen:
     105nlemma sfr8051_index_19:
    106106  ∀i: SFR8051.
    107     sfr_8051_index i < nineteen.
    108  #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
    109  napply less_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.
    110110nqed.
    111111   
    112 nlemma sfr8052_index_five:
     112nlemma sfr8052_index_5:
    113113  ∀i: SFR8052.
    114     sfr_8052_index i < five.
    115  #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
    116  napply less_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.
    117117nqed.
    118118   
     
    192192    let index ≝ sfr_8051_index i in
    193193      get_index_v … sfr index ?.
    194     napply sfr8051_index_nineteen.
     194    napply sfr8051_index_19.
    195195nqed.
    196196
     
    201201    let index ≝ sfr_8052_index i in
    202202      get_index_v … sfr index ?.
    203     napply sfr8052_index_five.
     203    napply sfr8052_index_5.
    204204nqed.
    205205
     
    217217    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    218218    let new_special_function_registers_8051 ≝
    219       set_index Byte nineteen old_special_function_registers_8051 index b ? in
     219      set_index Byte 19 old_special_function_registers_8051 index b ? in
    220220    let old_p1_latch ≝ p1_latch s in
    221221    let old_p3_latch ≝ p3_latch s in
     
    231231                old_p3_latch
    232232                old_clock.
    233     napply (sfr8051_index_nineteen i).
     233    napply (sfr8051_index_19 i).
    234234nqed.
    235235
     
    247247    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    248248    let new_special_function_registers_8052 ≝
    249       set_index Byte five old_special_function_registers_8052 index b ? in
     249      set_index Byte 5 old_special_function_registers_8052 index b ? in
    250250    let old_p1_latch ≝ p1_latch s in
    251251    let old_p3_latch ≝ p3_latch s in
     
    261261                old_p3_latch
    262262                old_clock.
    263     napply (sfr8052_index_five i).
     263    napply (sfr8052_index_5 i).
    264264nqed.
    265265
     
    289289ndefinition set_code_memory ≝
    290290  λs: Status.
    291   λr: BitVectorTrie Byte sixteen.
     291  λr: BitVectorTrie Byte 16.
    292292    let old_low_internal_ram ≝ low_internal_ram s in
    293293    let old_high_internal_ram ≝ high_internal_ram s in
     
    312312ndefinition set_low_internal_ram ≝
    313313  λs: Status.
    314   λr: BitVectorTrie Byte seven.
     314  λr: BitVectorTrie Byte 7.
    315315    let old_code_memory ≝ code_memory s in
    316316    let old_high_internal_ram ≝ high_internal_ram s in
     
    335335ndefinition set_high_internal_ram ≝
    336336  λs: Status.
    337   λr: BitVectorTrie Byte seven.
     337  λr: BitVectorTrie Byte 7.
    338338    let old_code_memory ≝ code_memory s in
    339339    let old_low_internal_ram ≝ low_internal_ram s in
     
    359359ndefinition set_external_ram ≝
    360360  λs: Status.
    361   λr: BitVectorTrie Byte sixteen.
     361  λr: BitVectorTrie Byte 16.
    362362    let old_code_memory ≝ code_memory s in
    363363    let old_low_internal_ram ≝ low_internal_ram s in
     
    383383  λs: Status.
    384384    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    ##]
    392393nqed.
    393394
     
    395396  λs: Status.
    396397    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;
    404403nqed.
    405404
     
    407406  λs: Status.
    408407    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;
    416413nqed.
    417414
     
    419416  λs: Status.
    420417    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;
    428423nqed.
    429424
     
    431426  λs: Status.
    432427    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;
    440433nqed.
    441434
     
    443436  λs: Status.
    444437    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;
    452443nqed.
    453444
     
    455446  λs: Status.
    456447    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;
    464453nqed.
    465454
     
    467456  λs: Status.
    468457    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;
    476463nqed.
    477464
     
    479466  λs: Status.
    480467  λcy: Bit.
    481   λac: Maybe Bit.
     468  λac: option Bit.
    482469  λov: Bit.
    483     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
    484     let old_cy ≝ get_index_v… nu Z ? in
    485     let old_ac ≝ get_index_v… nu one ? in
    486     let old_fo ≝ get_index_v… nu two ? in
    487     let old_rs1 ≝ get_index_v… nu three ? in
    488     let old_rs0 ≝ get_index_v… nl Z ? in
    489     let old_ov ≝ get_index_v… nl one ? in
    490     let old_ud ≝ get_index_v… nl two ? in
    491     let old_p ≝ get_index_v… nl three ? in
    492     let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
     470    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
    493480    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
    494481                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
     
    496483    ##[##1,2,3,4,5,6,7,8:
    497484        nnormalize;
    498         nrepeat (napply less_than_or_equal_monotone);
    499         napply (less_than_or_equal_zero);
     485        nrepeat (napply le_S_S);
     486        napply (le_O_n);
    500487    ##]
    501488nqed.
    502489
    503490ndefinition 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.    *)
    514501  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).
    516503 
    517504naxiom not_implemented: False.
     
    519506ndefinition get_bit_addressable_sfr ≝
    520507  λs: Status.
    521   λn: Nat.
     508  λn: nat.
    522509  λb: BitVector n.
    523   λl: Bool.
     510  λl: bool.
    524511    let address ≝ nat_of_bitvector … b in
    525       if (eq_n address one_hundred_and_twenty_eight) then
     512      if (eqb address 128) then
    526513        ?
    527       else if (eq_n address one_hundred_and_forty_four) then
     514      else if (eqb address 144) then
    528515        if l then
    529516          (p1_latch s)
    530517        else
    531518          (get_8051_sfr s SFR_P1)
    532       else if (eq_n address one_hundred_and_sixty) then
     519      else if (eqb address 160) then
    533520        ?
    534       else if (eq_n address one_hundred_and_seventy_six) then
     521      else if (eqb address 176) then
    535522        if l then
    536523          (p3_latch s)
    537524        else
    538525          (get_8051_sfr s SFR_P3)
    539       else if (eq_n address one_hundred_and_fifty_three) then
     526      else if (eqb address 153) then
    540527        get_8051_sfr s SFR_SBUF
    541       else if (eq_n address one_hundred_and_thirty_eight) then
     528      else if (eqb address 138) then
    542529        get_8051_sfr s SFR_TL0
    543       else if (eq_n address one_hundred_and_thirty_nine) then
     530      else if (eqb address 139) then
    544531        get_8051_sfr s SFR_TL1
    545       else if (eq_n address one_hundred_and_forty) then
     532      else if (eqb address 140) then
    546533        get_8051_sfr s SFR_TH0
    547       else if (eq_n address one_hundred_and_forty_one) then
     534      else if (eqb address 141) then
    548535        get_8051_sfr s SFR_TH1
    549       else if (eq_n address two_hundred) then
     536      else if (eqb address 200) then
    550537        get_8052_sfr s SFR_T2CON
    551       else if (eq_n address two_hundred_and_two) then
     538      else if (eqb address 202) then
    552539        get_8052_sfr s SFR_RCAP2L
    553       else if (eq_n address two_hundred_and_three) then
     540      else if (eqb address 203) then
    554541        get_8052_sfr s SFR_RCAP2H
    555       else if (eq_n address two_hundred_and_four) then
     542      else if (eqb address 204) then
    556543        get_8052_sfr s SFR_TL2
    557       else if (eq_n address two_hundred_and_five) then
     544      else if (eqb address 205) then
    558545        get_8052_sfr s SFR_TH2
    559       else if (eq_n address one_hundred_and_thirty_five) then
     546      else if (eqb address 135) then
    560547        get_8051_sfr s SFR_PCON
    561       else if (eq_n address one_hundred_and_thirty_six) then
     548      else if (eqb address 136) then
    562549        get_8051_sfr s SFR_TCON
    563       else if (eq_n address one_hundred_and_thirty_seven) then
     550      else if (eqb address 137) then
    564551        get_8051_sfr s SFR_TMOD
    565       else if (eq_n address one_hundred_and_fifty_two) then
     552      else if (eqb address 152) then
    566553        get_8051_sfr s SFR_SCON
    567       else if (eq_n address one_hundred_and_sixty_eight) then
     554      else if (eqb address 168) then
    568555        get_8051_sfr s SFR_IE
    569       else if (eq_n address one_hundred_and_eighty_four) then
     556      else if (eqb address 184) then
    570557        get_8051_sfr s SFR_IP
    571       else if (eq_n address one_hundred_and_twenty_nine) then
     558      else if (eqb address 129) then
    572559        get_8051_sfr s SFR_SP
    573       else if (eq_n address one_hundred_and_thirty) then
     560      else if (eqb address 130) then
    574561        get_8051_sfr s SFR_DPL
    575       else if (eq_n address one_hundred_and_thirty_one) then
     562      else if (eqb address 131) then
    576563        get_8051_sfr s SFR_DPH
    577       else if (eq_n address two_hundred_and_eight) then
     564      else if (eqb address 208) then
    578565        get_8051_sfr s SFR_PSW
    579       else if (eq_n address two_hundred_and_twenty_four) then
     566      else if (eqb address 224) then
    580567        get_8051_sfr s SFR_ACC_A
    581       else if (eq_n address two_hundred_and_forty) then
     568      else if (eqb address 240) then
    582569        get_8051_sfr s SFR_ACC_B
    583570      else
     
    591578  λv: Byte.
    592579    let address ≝ nat_of_bitvector … b in
    593       if (eq_n address one_hundred_and_twenty_eight) then
     580      if (eqb address 128) then
    594581        ?
    595       else if (eq_n address one_hundred_and_forty_four) then
     582      else if (eqb address 144) then
    596583        let status_1 ≝ set_8051_sfr s SFR_P1 v in
    597584        let status_2 ≝ set_p1_latch s v in
    598585          status_2
    599       else if (eq_n address one_hundred_and_sixty) then
     586      else if (eqb address 160) then
    600587        ?
    601       else if (eq_n address one_hundred_and_seventy_six) then
     588      else if (eqb address 176) then
    602589        let status_1 ≝ set_8051_sfr s SFR_P3 v in
    603590        let status_2 ≝ set_p3_latch s v in
    604591          status_2
    605       else if (eq_n address one_hundred_and_fifty_three) then
     592      else if (eqb address 153) then
    606593        set_8051_sfr s SFR_SBUF v
    607       else if (eq_n address one_hundred_and_thirty_eight) then
     594      else if (eqb address 138) then
    608595        set_8051_sfr s SFR_TL0 v
    609       else if (eq_n address one_hundred_and_thirty_nine) then
     596      else if (eqb address 139) then
    610597        set_8051_sfr s SFR_TL1 v
    611       else if (eq_n address one_hundred_and_forty) then
     598      else if (eqb address 140) then
    612599        set_8051_sfr s SFR_TH0 v
    613       else if (eq_n address one_hundred_and_forty_one) then
     600      else if (eqb address 141) then
    614601        set_8051_sfr s SFR_TH1 v
    615       else if (eq_n address two_hundred) then
     602      else if (eqb address 200) then
    616603        set_8052_sfr s SFR_T2CON v
    617       else if (eq_n address two_hundred_and_two) then
     604      else if (eqb address 202) then
    618605        set_8052_sfr s SFR_RCAP2L v
    619       else if (eq_n address two_hundred_and_three) then
     606      else if (eqb address 203) then
    620607        set_8052_sfr s SFR_RCAP2H v
    621       else if (eq_n address two_hundred_and_four) then
     608      else if (eqb address 204) then
    622609        set_8052_sfr s SFR_TL2 v
    623       else if (eq_n address two_hundred_and_five) then
     610      else if (eqb address 205) then
    624611        set_8052_sfr s SFR_TH2 v
    625       else if (eq_n address one_hundred_and_thirty_five) then
     612      else if (eqb address 135) then
    626613        set_8051_sfr s SFR_PCON v
    627       else if (eq_n address one_hundred_and_thirty_six) then
     614      else if (eqb address 136) then
    628615        set_8051_sfr s SFR_TCON v
    629       else if (eq_n address one_hundred_and_thirty_seven) then
     616      else if (eqb address 137) then
    630617        set_8051_sfr s SFR_TMOD v
    631       else if (eq_n address one_hundred_and_fifty_two) then
     618      else if (eqb address 152) then
    632619        set_8051_sfr s SFR_SCON v
    633       else if (eq_n address one_hundred_and_sixty_eight) then
     620      else if (eqb address 168) then
    634621        set_8051_sfr s SFR_IE v
    635       else if (eq_n address one_hundred_and_eighty_four) then
     622      else if (eqb address 184) then
    636623        set_8051_sfr s SFR_IP v
    637       else if (eq_n address one_hundred_and_twenty_nine) then
     624      else if (eqb address 129) then
    638625        set_8051_sfr s SFR_SP v
    639       else if (eq_n address one_hundred_and_thirty) then
     626      else if (eqb address 130) then
    640627        set_8051_sfr s SFR_DPL v
    641       else if (eq_n address one_hundred_and_thirty_one) then
     628      else if (eqb address 131) then
    642629        set_8051_sfr s SFR_DPH v
    643       else if (eq_n address two_hundred_and_eight) then
     630      else if (eqb address 208) then
    644631        set_8051_sfr s SFR_PSW v
    645       else if (eq_n address two_hundred_and_twenty_four) then
     632      else if (eqb address 224) then
    646633        set_8051_sfr s SFR_ACC_A v
    647       else if (eq_n address two_hundred_and_forty) then
     634      else if (eqb address 240) then
    648635        set_8051_sfr s SFR_ACC_B v
    649636      else
     
    654641ndefinition bit_address_of_register ≝
    655642  λs: Status.
    656   λr: BitVector three.
    657     let b ≝ get_index_v … r Z ? in
    658     let c ≝ get_index_v … r one ? in
    659     let d ≝ get_index_v … r two ? in
    660     let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    661     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in
     643  λ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
    662649    let offset ≝
    663       if conjunction (negation r1) (negation r0) then
    664         Z
    665       else if conjunction (negation r1) r0 then
    666         eight
    667       else if conjunction r1 r0 then
    668         twenty_four
     650      if ¬r1 ∧ ¬r0 then
     651        O
     652      else if ¬r1 ∧ r0 then
     653        8
     654      else if r1 ∧ r0 then
     655        24
    669656      else
    670         sixteen
     657        16
    671658    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 ]])).
    673660  ##[##1,2,3,4,5:
    674661      nnormalize;
    675       nrepeat (napply less_than_or_equal_monotone);
    676       napply less_than_or_equal_zero;
     662      nrepeat (napply le_S_S);
     663      napply le_O_n;
    677664  ##]
    678665nqed.
     
    680667ndefinition get_register ≝
    681668  λs: Status.
    682   λr: BitVector three.
     669  λr: BitVector 3.
    683670    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).
    685672     
    686673ndefinition set_register ≝
    687674  λs: Status.
    688   λr: BitVector three.
     675  λr: BitVector 3.
    689676  λv: Byte.
    690677    let address ≝ bit_address_of_register s r in
     
    695682ndefinition read_at_stack_pointer ≝
    696683  λs: Status.
    697     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    698     let m ≝ get_index_v … nu Z ? in
    699     let r1 ≝ get_index_v … nu one ? in
    700     let r2 ≝ get_index_v … nu two ? in
    701     let r3 ≝ get_index_v … nu three ? in
     684    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
    702689    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    703690    let memory ≝
     
    707694        (high_internal_ram s)
    708695    in
    709       lookup … address memory (zero eight).
    710     ##[##1,2,3,4:
    711         nnormalize;
    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  ##]
    715702nqed.
    716703
     
    718705  λs: Status.
    719706  λv: Byte.
    720     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    721     let bit_zero ≝ get_index_v… nu Z ? in
    722     let bit_one ≝ get_index_v… nu one ? in
    723     let bit_two ≝ get_index_v… nu two ? in
    724     let bit_three ≝ get_index_v… nu three ? in
     707    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
    725712      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)
    727714                              v (low_internal_ram s) in
    728715          set_low_internal_ram s memory
    729716      else
    730         let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     717        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    731718                              v (high_internal_ram s) in
    732719          set_high_internal_ram s memory.
    733     ##[##1,2,3,4:
    734         nnormalize;
    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  ##]
    738725nqed.
    739726
     
    742729   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
    743730     [ DPTR ⇒ λ_:True.
    744        let 〈 bu, bl 〉 ≝ split … eight eight v in
     731       let 〈 bu, bl 〉 ≝ split … 8 8 v in
    745732       let status ≝ set_8051_sfr s SFR_DPH bu in
    746733       let status ≝ set_8051_sfr status SFR_DPL bl in
     
    762749      ] (subaddressing_modein … a).
    763750     
    764 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
     751ndefinition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
    765752                                          acc_a ; acc_b ; data ; acc_dptr ;
    766753                                          acc_pc ; ext_indirect ;
     
    778765        λext_indirect_dptr: True.
    779766          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)
    781768      | EXT_INDIRECT e ⇒
    782769        λext_indirect: True.
    783770          let address ≝ get_register s [[ false; false; e ]]  in
    784           let padded_address ≝ pad eight eight address in
    785             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)
    786773      | ACC_DPTR ⇒
    787774        λacc_dptr: True.
    788775          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) in
    790           let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
    791             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)
    792779      | ACC_PC ⇒
    793780        λacc_pc: True.
    794           let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    795           let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
    796             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)
    797784      | DIRECT d ⇒
    798785        λdirect: True.
    799           let 〈 nu, nl 〉 ≝ split … four four d in
    800           let bit_one ≝ get_index_v … nu one ? in
    801             match bit_one with
     786          let 〈 nu, nl 〉 ≝ split … 4 4 d in
     787          let bit_1 ≝ get_index_v … nu 1 ? in
     788            match bit_1 with
    802789              [ true ⇒
    803                   let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
     790                  let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
    804791                  let address ≝ three_bits @@ nl in
    805                     lookup ? seven address (low_internal_ram s) (zero eight)
    806               | false ⇒ get_bit_addressable_sfr s eight d l
     792                    lookup ? 7 address (low_internal_ram s) (zero 8)
     793              | false ⇒ get_bit_addressable_sfr s 8 d l
    807794              ]
    808795      | INDIRECT i ⇒
    809796        λindirect: True.
    810           let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    811           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    812           let bit_one ≝ get_index_v … bit_one_v Z ? in
    813           match bit_one with
     797          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
    814801            [ 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)
    816803            | 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)
    818805            ]
    819806      | _ ⇒ λother.
     
    822809      ##[##1,2:
    823810          nnormalize;
    824           nrepeat (napply less_than_or_equal_monotone);
    825           napply less_than_or_equal_zero;
     811          nrepeat (napply le_S_S);
     812          napply le_O_n;
    826813      ##]
    827814nqed.
     
    836823      [ DIRECT d ⇒
    837824        λdirect: True.
    838           let 〈 nu, nl 〉 ≝ split … four four d in
    839           let bit_one ≝ get_index_v … nu one ? in
    840           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    841             match bit_one with
     825          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
    842829              [ true ⇒ set_bit_addressable_sfr s d v
    843830              | false ⇒
    844                 let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
     831                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in
    845832                  set_low_internal_ram s memory
    846833              ]
     
    848835        λindirect: True.
    849836          let register ≝ get_register s [[ false; false; i ]] in
    850           let 〈nu, nl〉 ≝ split ? four four register in
    851           let bit_one ≝ get_index_v … nu one ? in
    852           let 〈ignore, three_bits〉 ≝ split ? one three nu in
    853             match bit_one with
     837          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
    854841              [ true ⇒
    855842                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
     
    865852        λext_indirect: True.
    866853          let address ≝ get_register s [[ false; false; e ]] in
    867           let padded_address ≝ pad eight eight address in
    868           let memory ≝ insert ? sixteen padded_address v (external_ram s) in
     854          let padded_address ≝ pad 8 8 address in
     855          let memory ≝ insert ? 16 padded_address v (external_ram s) in
    869856            set_external_ram s memory
    870857      | EXT_INDIRECT_DPTR ⇒
    871858        λext_indirect_dptr: True.
    872859          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    873           let memory ≝ insert ? sixteen address v (external_ram s) in
     860          let memory ≝ insert ? 16 address v (external_ram s) in
    874861            set_external_ram s memory
    875862      | _ ⇒
     
    879866      ##[##1,2:
    880867          nnormalize;
    881           nrepeat (napply less_than_or_equal_monotone);
    882           napply less_than_or_equal_zero
     868          nrepeat (napply le_S_S);
     869          napply le_O_n
    883870      ##]
    884871nqed.
    885872
    886873ntheorem modulus_less_than:
    887   ∀m,n: Nat. (m mod (S n)) < S n.
    888  #n m; nnormalize; napply less_than_or_equal_monotone;
    889  nlapply (ltoe_refl n);
     874  ∀m,n: nat. (m mod (S n)) < S n.
     875 #n m; nnormalize; napply le_S_S;
     876 nlapply (le_n n);
    890877 ngeneralize in ⊢ (?%? → ?(??%?)?);
    891878 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
     
    895882     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
    896883       ncases n; nnormalize; //;
    897        #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m;
     884       #x K1; nlapply (le_S_S_to_le … K1); ngeneralize in match m;
    898885       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
    899886       #q K2; napply H; /3/]
     
    901888
    902889ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
    903                        Bool → Bool ≝
     890                       bool → bool ≝
    904891  λs, a, l.
    905892    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
     
    908895      [ BIT_ADDR b ⇒
    909896        λbit_addr: True.
    910           let 〈 nu, nl 〉 ≝ split … four four b in
    911           let bit_one ≝ get_index_v … nu one ? in
    912           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    913             match bit_one with
     897          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
    914901              [ true ⇒
    915902                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    916                 let d ≝ address ÷ eight in
    917                 let m ≝ address mod eight in
    918                 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     903                let d ≝ address ÷ 8 in
     904                let m ≝ address mod 8 in
     905                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    919906                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    920907                  get_index_v … sfr m ?
    921908              | false ⇒
    922909                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    923                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    924                 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    925                   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) ?
    926913              ]
    927914      | N_BIT_ADDR n ⇒
    928915        λn_bit_addr: True.
    929           let 〈 nu, nl 〉 ≝ split … four four n in
    930           let bit_one ≝ get_index_v … nu one ? in
    931           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    932             match bit_one with
     916          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
    933920              [ true ⇒
    934921                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    935                 let d ≝ address ÷ eight in
    936                 let m ≝ address mod eight in
    937                 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     922                let d ≝ address ÷ 8 in
     923                let m ≝ address mod 8 in
     924                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    938925                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    939                   negation (get_index_v … sfr m ?)
     926                  ¬(get_index_v … sfr m ?)
    940927              | false ⇒
    941928                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    942                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    943                 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    944                   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) ?)
    945932              ]
    946933      | CARRY ⇒ λcarry: True. get_cy_flag s
     
    950937      ##[##3,6:
    951938          nnormalize;
    952           nrepeat (napply less_than_or_equal_monotone);
    953           napply less_than_or_equal_zero;
     939          nrepeat (napply le_S_S);
     940          napply le_O_n;
    954941      ##|##1,2,4,5:
    955942          napply modulus_less_than;
     
    962949    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
    963950      [ BIT_ADDR b ⇒ λbit_addr: True.
    964           let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    965           let bit_one ≝ get_index_v … nu one ? in
    966           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    967           match bit_one with
     951          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
    968955            [ true ⇒
    969956                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    970                 let d ≝ address ÷ eight in
    971                 let m ≝ address mod eight in
    972                 let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     957                let d ≝ address ÷ 8 in
     958                let m ≝ address mod 8 in
     959                let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    973960                let sfr ≝ get_bit_addressable_sfr s ? t true in
    974961                let new_sfr ≝ set_index … sfr m v ? in
     
    976963            | false ⇒
    977964                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    978                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    979                 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    980                 let n_bit ≝ set_index … t (modulus address eight) v ? in
    981                 let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
     965                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
    982969                  set_low_internal_ram s memory
    983970            ]
    984971      | CARRY ⇒
    985972        λcarry: True.
    986           let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    987           let bit_one ≝ get_index_v… nu one ? in
    988           let bit_two ≝ get_index_v… nu two ? in
    989           let bit_three ≝ get_index_v… nu three ? in
    990           let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
     973          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
    991978            set_8051_sfr s SFR_PSW new_psw
    992979      | _ ⇒
     
    997984      ##[##1,2,3,6:
    998985          nnormalize;
    999           nrepeat (napply less_than_or_equal_monotone);
    1000           napply less_than_or_equal_zero;
     986          nrepeat (napply le_S_S);
     987          napply le_O_n;
    1001988      ##|##4,5:
    1002989          napply modulus_less_than;
     
    1005992
    1006993ndefinition 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).
    1008995
    1009996ndefinition load ≝
Note: See TracChangeset for help on using the changeset viewer.