Changeset 313


Ignore:
Timestamp:
Nov 26, 2010, 3:33:32 PM (9 years ago)
Author:
mulligan
Message:

Added axioms for addition for claudio.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

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

    r286 r313  
    2828ndefinition nineteen ≝ ten + nine.
    2929ndefinition twenty_four ≝ sixteen + eight.
     30ndefinition thirty_two ≝ sixteen + sixteen.
    3031ndefinition one_hundred ≝ ten * ten.
    3132ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
  • Deliverables/D4.1/Matita/BitVector.ma

    r275 r313  
    217217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218218    ].
     219   
     220naxiom half_add:
     221  ∀n: Nat.
     222  ∀b, c: BitVector n.
     223    Bool × (BitVector n).
     224   
     225naxiom full_add:
     226  ∀n: Nat.
     227  ∀b, c: BitVector n.
     228  ∀d: Bit.
     229    Bool × (BitVector n).
  • Deliverables/D4.1/Matita/Status.ma

    r311 r313  
    304304                r
    305305                old_external_ram
     306                old_program_counter
     307                old_special_function_registers_8051
     308                old_special_function_registers_8052
     309                old_p1_latch
     310                old_p3_latch.
     311               
     312ndefinition set_external_ram ≝
     313  λs: Status.
     314  λr: BitVectorTrie Byte sixteen.
     315    let old_code_memory ≝ code_memory s in
     316    let old_low_internal_ram ≝ low_internal_ram s in
     317    let old_high_internal_ram ≝ high_internal_ram s in
     318    let old_program_counter ≝ program_counter s in
     319    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     320    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     321    let old_p1_latch ≝ p1_latch s in
     322    let old_p3_latch ≝ p3_latch s in
     323      mk_Status old_code_memory
     324                old_low_internal_ram
     325                old_high_internal_ram
     326                r
    306327                old_program_counter
    307328                old_special_function_registers_8051
     
    525546  λs: Status.
    526547  λb: Byte.
     548  λv: Byte.
    527549    let address ≝ nat_of_bitvector … b in
    528550      if (decidable_equality address one_hundred_and_twenty_eight) then
    529551        ?
    530552      else if (decidable_equality address one_hundred_and_forty_four) then
    531         let status_1 ≝ set_8051_sfr s SFR_P1 b in
    532         let status_2 ≝ set_p1_latch s b in
     553        let status_1 ≝ set_8051_sfr s SFR_P1 v in
     554        let status_2 ≝ set_p1_latch s v in
    533555          status_2
    534556      else if (decidable_equality address one_hundred_and_sixty) then
    535557        ?
    536558      else if (decidable_equality address one_hundred_and_seventy_six) then
    537         let status_1 ≝ set_8051_sfr s SFR_P3 b in
    538         let status_2 ≝ set_p3_latch s b in
     559        let status_1 ≝ set_8051_sfr s SFR_P3 v in
     560        let status_2 ≝ set_p3_latch s v in
    539561          status_2
    540562      else if (decidable_equality address one_hundred_and_fifty_three) then
    541         set_8051_sfr s SFR_SBUF b
     563        set_8051_sfr s SFR_SBUF v
    542564      else if (decidable_equality address one_hundred_and_thirty_eight) then
    543         set_8051_sfr s SFR_TL0 b
     565        set_8051_sfr s SFR_TL0 v
    544566      else if (decidable_equality address one_hundred_and_thirty_nine) then
    545         set_8051_sfr s SFR_TL1 b
     567        set_8051_sfr s SFR_TL1 v
    546568      else if (decidable_equality address one_hundred_and_forty) then
    547         set_8051_sfr s SFR_TH0 b
     569        set_8051_sfr s SFR_TH0 v
    548570      else if (decidable_equality address one_hundred_and_forty_one) then
    549         set_8051_sfr s SFR_TH1 b
     571        set_8051_sfr s SFR_TH1 v
    550572      else if (decidable_equality address two_hundred) then
    551         set_8052_sfr s SFR_T2CON b
     573        set_8052_sfr s SFR_T2CON v
    552574      else if (decidable_equality address two_hundred_and_two) then
    553         set_8052_sfr s SFR_RCAP2L b
     575        set_8052_sfr s SFR_RCAP2L v
    554576      else if (decidable_equality address two_hundred_and_three) then
    555         set_8052_sfr s SFR_RCAP2H b
     577        set_8052_sfr s SFR_RCAP2H v
    556578      else if (decidable_equality address two_hundred_and_four) then
    557         set_8052_sfr s SFR_TL2 b
     579        set_8052_sfr s SFR_TL2 v
    558580      else if (decidable_equality address two_hundred_and_five) then
    559         set_8052_sfr s SFR_TH2 b
     581        set_8052_sfr s SFR_TH2 v
    560582      else if (decidable_equality address one_hundred_and_thirty_five) then
    561         set_8051_sfr s SFR_PCON b
     583        set_8051_sfr s SFR_PCON v
    562584      else if (decidable_equality address one_hundred_and_thirty_six) then
    563         set_8051_sfr s SFR_TCON b
     585        set_8051_sfr s SFR_TCON v
    564586      else if (decidable_equality address one_hundred_and_thirty_seven) then
    565         set_8051_sfr s SFR_TMOD b
     587        set_8051_sfr s SFR_TMOD v
    566588      else if (decidable_equality address one_hundred_and_fifty_two) then
    567         set_8051_sfr s SFR_SCON b
     589        set_8051_sfr s SFR_SCON v
    568590      else if (decidable_equality address one_hundred_and_sixty_eight) then
    569         set_8051_sfr s SFR_IE b
     591        set_8051_sfr s SFR_IE v
    570592      else if (decidable_equality address one_hundred_and_eighty_four) then
    571         set_8051_sfr s SFR_IP b
     593        set_8051_sfr s SFR_IP v
    572594      else if (decidable_equality address one_hundred_and_twenty_nine) then
    573         set_8051_sfr s SFR_SP b
     595        set_8051_sfr s SFR_SP v
    574596      else if (decidable_equality address one_hundred_and_thirty) then
    575         set_8051_sfr s SFR_DPL b
     597        set_8051_sfr s SFR_DPL v
    576598      else if (decidable_equality address one_hundred_and_thirty_one) then
    577         set_8051_sfr s SFR_DPH b
     599        set_8051_sfr s SFR_DPH v
    578600      else if (decidable_equality address two_hundred_and_eight) then
    579         set_8051_sfr s SFR_PSW b
     601        set_8051_sfr s SFR_PSW v
    580602      else if (decidable_equality address two_hundred_and_twenty_four) then
    581         set_8051_sfr s SFR_ACC_A b
     603        set_8051_sfr s SFR_ACC_A v
    582604      else if (decidable_equality address two_hundred_and_forty) then
    583         set_8051_sfr s SFR_ACC_B b
     605        set_8051_sfr s SFR_ACC_B v
    584606      else
    585607        ?.
     
    695717        ]
    696718      ] (subaddressing_modein … a).
    697      
    698 naxiom half_add:
    699   ∀n: Nat.
    700   ∀b, c: BitVector n.
    701     BitVector n × Bool.
    702719     
    703720ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
     
    727744          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    728745          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    729           let 〈 address, carry 〉 ≝ half_add sixteen dptr padded_acc in
     746          let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
    730747            lookup … sixteen address (external_ram s) (zero eight)
    731748      | ACC_PC ⇒
    732749        λacc_pc: True.
    733750          let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    734           let 〈 address, carry 〉 ≝ half_add sixteen (program_counter s) padded_acc in
     751          let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
    735752            lookup … sixteen address (external_ram s) (zero eight)
    736753      | DIRECT d ⇒
     
    765782      ##]
    766783nqed.
    767 nqed.
     784
     785(*
     786ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
     787                       Bool → Bool ≝
     788  λs, a, l.
     789    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
     790                                                 n_bit_addr ;
     791                                                 carry ]] x) → ? with
     792      [ BIT_ADDR b ⇒
     793        λbit_addr: True.
     794          let 〈 nu, nl 〉 ≝ split … four four b in
     795          let bit_one ≝ get_index … nu one ? in
     796          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
     797            match bit_one with
     798              [ true ⇒
     799                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     800                let d ≝ address ÷ eight in
     801                let m ≝ address mod eight in
     802                let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in
     803                let sfr ≝ get_bit_addressable_sfr s ? trans l in
     804                  get_index ? sfr m ?
     805              | false ⇒
     806                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     807                let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in
     808                let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
     809                  get_index ? t (modulus address eight) ?
     810              ]
     811      | N_BIT_ADDR n ⇒
     812        λn_bit_addr: True.
     813          let 〈 nu, nl 〉 ≝ split … four four n in
     814          let bit_one ≝ get_index … nu one ? in
     815          let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
     816            match bit_one with
     817              [ true ⇒
     818                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     819                let d ≝ address ÷ eight in
     820                let m ≝ address mod eight in
     821                let trans ≝ bitvector_of_nat ((d * eight) + one_hundred_and_twenty_eight) eight in
     822                let sfr ≝ get_bit_addressable_sfr s ? trans l in
     823                  negation (get_index ? sfr m ?)
     824              | false ⇒
     825                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
     826                let address' ≝ bitvector_of_nat ((address ÷ eight) + thirty_two) seven in
     827                let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
     828                  negation (get_index ? trans (modulus address eight) ?)
     829              ]
     830      | CARRY ⇒ λcarry: True. get_cy_flag s
     831      | _ ⇒ λother.
     832        match other in False with [ ]
     833      ] (subaddressing_modein … a). *)
     834
     835ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
     836                                   acc_a ; acc_b ; ext_indirect ;
     837                                   ext_indirect_dptr ]] → Byte → Status ≝
     838  λs, a, v.
     839    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     840                                                acc_a ; acc_b ; ext_indirect ;
     841                                                ext_indirect_dptr ]] x) → ? with
     842      [ DIRECT d ⇒
     843        λdirect: True.
     844          let 〈 nu, nl 〉 ≝ split … four four d in
     845          let bit_one ≝ get_index … nu one ? in
     846          let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
     847            match bit_one with
     848              [ true ⇒ set_bit_addressable_sfr s d v
     849              | false ⇒
     850                let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
     851                  set_low_internal_ram s memory
     852              ]
     853      | INDIRECT i ⇒
     854        λindirect: True. ?
     855      | REGISTER r1 r2 r3 ⇒ λregister: True. set_register s r1 r2 r3 v
     856      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
     857      | ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
     858      | EXT_INDIRECT e ⇒
     859        λext_indirect: True.
     860          let address ≝ get_register s false false e in
     861          let padded_address ≝ pad eight eight address in
     862          let memory ≝ insert ? sixteen padded_address v (external_ram s) in
     863            set_external_ram s memory
     864      | EXT_INDIRECT_DPTR ⇒
     865        λext_indirect_dptr: True.
     866          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
     867          let memory ≝ insert ? sixteen address v (external_ram s) in
     868            set_external_ram s memory
     869      | _ ⇒
     870        λother: False.
     871          match other in False with [ ]
     872      ] (subaddressing_modein … a).
Note: See TracChangeset for help on using the changeset viewer.