Changeset 466


Ignore:
Timestamp:
Jan 20, 2011, 6:46:21 PM (7 years ago)
Author:
mulligan
Message:

Most of execute_1 checked. Need to fix negations, though, in rest in order to get it to typecheck.

File:
1 edited

Legend:

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

    r465 r466  
    44ndefinition sign_extension: Byte → Word ≝
    55  λc.
    6     let b ≝ get_index_v ? eight c one ? in
     6    let b ≝ get_index_v ? 8 c 1 ? in
    77      [[ b; b; b; b; b; b; b; b ]] @@ c.
    88  nnormalize;
    9   nrepeat (napply (less_than_or_equal_monotone ?));
    10   napply (less_than_or_equal_zero);
     9  nrepeat (napply (le_S_S ?));
     10  napply (le_O_n);
    1111nqed.
    1212   
    1313nlemma inclusive_disjunction_true:
    14   ∀b, c: Bool.
    15     inclusive_disjunction b c = true → b = true ∨ c = true.
     14  ∀b, c: bool.
     15    (orb b c) = true → b = true ∨ c = true.
    1616  #b c;
    1717  nelim b
     
    2222
    2323nlemma conjunction_true:
    24   ∀b, c: Bool.
    25     conjunction b c = true → b = true ∧ c = true.
     24  ∀b, c: bool.
     25    andb b c = true → b = true ∧ c = true.
    2626  #b c;
    2727  nelim b; nnormalize
     
    3737nqed.
    3838
    39 nlemma inclusive_disjunction_b_true: ∀b. inclusive_disjunction b true = true.
     39nlemma inclusive_disjunction_b_true: ∀b. orb b true = true.
    4040 #b; ncases b; @.
    4141nqed.
     
    4646  [ nnormalize; #_; #K; nassumption
    4747  | #m' t q' II H1 H2; nnormalize;
    48     nchange in H2:(??%?) with (inclusive_disjunction ??);
     48    nchange in H2:(??%?) with (orb ??);
    4949    ncases (inclusive_disjunction_true … H2)
    5050     [ #K; nrewrite < (eq_a_to_eq … K); nrewrite > H1; @
    51      | #K; nrewrite > II; ntry nassumption; // ]
     51     | #K; nrewrite > II; ntry nassumption; ncases (is_a t a); nnormalize; @ ]
    5252nqed.
    5353
     
    7070       ncases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
    7171       [ #K1; #_;
    72         nchange in K1 with ((conjunction ? (subvector_with …)) = true);
     72        nchange in K1 with ((andb ? (subvector_with …)) = true);
    7373        ncases (conjunction_true … K1); #K3; #K4;
    7474        ncases (inclusive_disjunction_true … K); #K2
     
    8282  λs.
    8383    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
    84     let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
     84    let 〈 instr, pc 〉 ≝ 〈 fst … instr_pc, snd … instr_pc 〉 in
    8585    let s ≝ set_clock s (clock s + ticks) in
    8686    let s ≝ set_program_counter s pc in
     
    9090            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    9191                                                   (get_arg_8 s false addr2) false in
    92             let cy_flag ≝ get_index' ? Z  ? flags in
    93             let ac_flag ≝ get_index' ? one ? flags in
    94             let ov_flag ≝ get_index' ? two ? flags in
     92            let cy_flag ≝ get_index' ? O  ? flags in
     93            let ac_flag ≝ get_index' ? 1 ? flags in
     94            let ov_flag ≝ get_index' ? 2 ? flags in
    9595            let s ≝ set_arg_8 s ACC_A result in
    9696              set_flags s cy_flag (Some Bit ac_flag) ov_flag
     
    9999            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    100100                                                   (get_arg_8 s false addr2) old_cy_flag in
    101             let cy_flag ≝ get_index' ? Z ? flags in
    102             let ac_flag ≝ get_index' ? one ? flags in
    103             let ov_flag ≝ get_index' ? two ? flags in
     101            let cy_flag ≝ get_index' ? O ? flags in
     102            let ac_flag ≝ get_index' ? 1 ? flags in
     103            let ov_flag ≝ get_index' ? 2 ? flags in
    104104            let s ≝ set_arg_8 s ACC_A result in
    105105              set_flags s cy_flag (Some Bit ac_flag) ov_flag
     
    108108            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
    109109                                                   (get_arg_8 s false addr2) old_cy_flag in
    110             let cy_flag ≝ get_index' ? Z ? flags in
    111             let ac_flag ≝ get_index' ? one ? flags in
    112             let ov_flag ≝ get_index' ? two ? flags in
     110            let cy_flag ≝ get_index' ? O ? flags in
     111            let ac_flag ≝ get_index' ? 1 ? flags in
     112            let ov_flag ≝ get_index' ? 2 ? flags in
    113113            let s ≝ set_arg_8 s ACC_A result in
    114114              set_flags s cy_flag (Some Bit ac_flag) ov_flag
     
    121121                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    122122                    set_arg_8 s addr1 and_val
    123                 | right r ⇒
     123                | inr r ⇒
    124124                  let 〈addr1, addr2〉 ≝ r in
    125125                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    126126                    set_arg_8 s addr1 and_val
    127127                ]
    128             | right r ⇒
     128            | inr r ⇒
    129129              let 〈addr1, addr2〉 ≝ r in
    130               let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
     130              let and_val ≝ (get_cy_flag s) ∧ (get_arg_1 s addr2 true) in
    131131                set_flags s and_val (None ?) (get_ov_flag s)
    132132            ]
     
    139139                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    140140                    set_arg_8 s addr1 or_val
    141                 | right r ⇒
     141                | inr r ⇒
    142142                  let 〈addr1, addr2〉 ≝ r in
    143143                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    144144                    set_arg_8 s addr1 or_val
    145145                ]
    146             | right r ⇒
     146            | inr r ⇒
    147147              let 〈addr1, addr2〉 ≝ r in
    148               let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
     148              let or_val ≝ (get_cy_flag s) ∨ (get_arg_1 s addr2 true) in
    149149                set_flags s or_val (None ?) (get_ov_flag s)
    150150            ]
     
    155155              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    156156                set_arg_8 s addr1 xor_val
    157             | right r ⇒
     157            | inr r ⇒
    158158              let 〈addr1, addr2〉 ≝ r in
    159159              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
     
    167167                                                           dptr ]] x) → ? with
    168168              [ ACC_A ⇒ λacc_a: True.
    169                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
     169                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat 8 1) in
    170170                  set_arg_8 s ACC_A result
    171171              | REGISTER r ⇒ λregister: True.
    172                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
     172                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat 8 1) in
    173173                  set_arg_8 s (REGISTER r) result
    174174              | DIRECT d ⇒ λdirect: True.
    175                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
     175                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat 8 1) in
    176176                  set_arg_8 s (DIRECT d) result
    177177              | INDIRECT i ⇒ λindirect: True.
    178                 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
     178                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat 8 1) in
    179179                  set_arg_8 s (INDIRECT i) result
    180180              | DPTR ⇒ λdptr: True.
    181                 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
    182                 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
     181                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat 8 1) in
     182                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero 8) carry in
    183183                let s ≝ set_8051_sfr s SFR_DPL bl in
    184184                  set_8051_sfr s SFR_DPH bu
    185185              | _ ⇒ λother: False. ⊥
    186186              ] (subaddressing_modein … addr)
    187        | DEC addr ⇒
    188            let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
     187        | DEC addr ⇒
     188           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat 8 1) false in
    189189             set_arg_8 s addr result
    190190        | MUL addr1 addr2 ⇒
    191            let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
    192            let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
     191           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     192           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    193193           let product ≝ acc_a_nat * acc_b_nat in
    194            let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
    195            let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
    196            let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
     194           let ov_flag ≝ product ≥ 256 in
     195           let low ≝ bitvector_of_nat 8 (product mod 256) in
     196           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
    197197           let s ≝ set_8051_sfr s SFR_ACC_A low in
    198198             set_8051_sfr s SFR_ACC_B high
    199199        | DIV addr1 addr2 ⇒
    200            let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
    201            let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
     200           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_A) in
     201           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr s SFR_ACC_B) in
    202202             match acc_b_nat with
    203                [ Z ⇒ set_flags s false (None Bit) true
     203               [ O ⇒ set_flags s false (None Bit) true
    204204               | S o ⇒
    205                  let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
    206                  let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
     205                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
     206                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
    207207                 let s ≝ set_8051_sfr s SFR_ACC_A q in
    208208                 let s ≝ set_8051_sfr s SFR_ACC_B r in
     
    210210               ]
    211211        | DA addr ⇒
    212             let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
    213               if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
    214                 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
    215                 let cy_flag ≝ get_index' ? Z ? flags in
    216                 let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
    217                   if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
    218                     let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
     212            let 〈 acc_nu, acc_nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_ACC_A) in
     213              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag s) then
     214                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat 8 6) false in
     215                let cy_flag ≝ get_index' ? O ? flags in
     216                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
     217                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
     218                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
    219219                    let new_acc ≝ nu @@ acc_nl' in
    220220                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
     
    226226        | CLR addr ⇒
    227227          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
    228             [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
     228            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero 8)
    229229            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
    230230            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
     
    239239            | CARRY ⇒ λcarry: True.
    240240                let old_cy_flag ≝ get_arg_1 s CARRY true in
    241                 let new_cy_flag ≝ negation old_cy_flag in
     241                let new_cy_flag ≝ ¬old_cy_flag in
    242242                  set_arg_1 s CARRY new_cy_flag
    243243            | BIT_ADDR b ⇒ λbit_addr: True.
    244244                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
    245                 let new_bit ≝ negation old_bit in
     245                let new_bit ≝ ¬old_bit in
    246246                  set_arg_1 s (BIT_ADDR b) new_bit
    247247            | _ ⇒ λother: False. ?
     
    250250        | RL _ ⇒ (* DPM: always ACC_A *)
    251251            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    252             let new_acc ≝ rotate_left … one old_acc in
     252            let new_acc ≝ rotate_left … 1 old_acc in
    253253              set_8051_sfr s SFR_ACC_A new_acc
    254254        | RR _ ⇒ (* DPM: always ACC_A *)
    255255            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    256             let new_acc ≝ rotate_right … one old_acc in
     256            let new_acc ≝ rotate_right … 1 old_acc in
    257257              set_8051_sfr s SFR_ACC_A new_acc
    258258        | RLC _ ⇒ (* DPM: always ACC_A *)
    259259            let old_cy_flag ≝ get_cy_flag s in
    260260            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    261             let new_cy_flag ≝ get_index' ? Z ? old_acc in
    262             let new_acc ≝ shift_left … one old_acc old_cy_flag in
     261            let new_cy_flag ≝ get_index' ? O ? old_acc in
     262            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
    263263            let s ≝ set_arg_1 s CARRY new_cy_flag in
    264264              set_8051_sfr s SFR_ACC_A new_acc
     
    266266            let old_cy_flag ≝ get_cy_flag s in
    267267            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    268             let new_cy_flag ≝ get_index' ? seven ? old_acc in
    269             let new_acc ≝ shift_right … one old_acc old_cy_flag in
     268            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
     269            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
    270270            let s ≝ set_arg_1 s CARRY new_cy_flag in
    271271              set_8051_sfr s SFR_ACC_A new_acc
    272272        | SWAP _ ⇒ (* DPM: always ACC_A *)
    273273            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    274             let 〈nu,nl〉 ≝ split ? four four old_acc in
     274            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
    275275            let new_acc ≝ nl @@ nu in
    276276              set_8051_sfr s SFR_ACC_A new_acc
     
    278278            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    279279              [ DIRECT d ⇒ λdirect: True.
    280                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     280                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    281281                let s ≝ set_8051_sfr s SFR_SP new_sp in
    282282                  write_at_stack_pointer s d
     
    285285        | POP addr ⇒
    286286            let contents ≝ read_at_stack_pointer s in
    287             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     287            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    288288            let s ≝ set_8051_sfr s SFR_SP new_sp in
    289289              set_arg_8 s addr contents
     
    294294              set_arg_8 s addr2 old_acc
    295295        | XCHD addr1 addr2 ⇒
    296             let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
    297             let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
     296            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr s SFR_ACC_A) in
     297            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 s false addr2) in
    298298            let new_acc ≝ acc_nu @@ arg_nl in
    299299            let new_arg ≝ arg_nu @@ acc_nl in
     
    302302        | RET ⇒
    303303            let high_bits ≝ read_at_stack_pointer s in
    304             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     304            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    305305            let s ≝ set_8051_sfr s SFR_SP new_sp in
    306306            let low_bits ≝ read_at_stack_pointer s in
    307             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     307            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    308308            let s ≝ set_8051_sfr s SFR_SP new_sp in
    309309            let new_pc ≝ high_bits @@ low_bits in
     
    311311        | RETI ⇒
    312312            let high_bits ≝ read_at_stack_pointer s in
    313             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     313            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    314314            let s ≝ set_8051_sfr s SFR_SP new_sp in
    315315            let low_bits ≝ read_at_stack_pointer s in
    316             let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
     316            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) false in
    317317            let s ≝ set_8051_sfr s SFR_SP new_sp in
    318318            let new_pc ≝ high_bits @@ low_bits in
     
    374374              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    375375                [ RELATIVE r ⇒ λrel: True.
    376                     if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
     376                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8) then
    377377                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    378378                        set_program_counter s new_pc
     
    384384              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    385385                [ RELATIVE r ⇒ λrel: True.
    386                     if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
     386                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero 8)) then
    387387                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    388388                        set_program_counter s new_pc
     
    405405                          else
    406406                            (set_flags s new_cy (None ?) (get_ov_flag s))
    407                     | right r' ⇒
     407                    | inr r' ⇒
    408408                        let 〈addr1, addr2〉 ≝ r' in
    409409                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
     
    421421              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    422422                [ RELATIVE r ⇒ λrel: True.
    423                     let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
     423                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat 8 1) false in
    424424                    let s ≝ set_arg_8 s addr1 result in
    425                       if negation (eq_bv ? result (zero eight)) then
     425                      if negation (eq_bv ? result (zero 8)) then
    426426                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    427427                          set_program_counter s new_pc
     
    433433        | JMP _ ⇒ (* DPM: always indirect_dptr *)
    434434          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    435           let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
     435          let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    436436          let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    437437          let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) jmp_addr in
     
    453453          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    454454            [ ADDR11 a ⇒ λaddr11: True.
    455               let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    456               let 〈nu, nl〉 ≝ split ? four four pc_bu in
    457               let bit ≝ get_index' ? Z ? nl in
    458               let 〈relevant1, relevant2〉 ≝ split ? three eight a in
     455              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
     456              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     457              let bit ≝ get_index' ? O ? nl in
     458              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
    459459              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    460460              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
     
    465465          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with
    466466            [ ACC_DPTR ⇒ λacc_dptr: True.
    467               let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
     467              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
    468468              let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    469469              let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
     
    471471                set_8051_sfr s SFR_ACC_A result
    472472            | ACC_PC ⇒ λacc_pc: True.
    473               let big_acc ≝ (zero eight) @@ (get_8051_sfr s SFR_ACC_A) in
    474               let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat sixteen one) in
     473              let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in
     474              let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in
    475475              (* DPM: Under specified: does the carry from PC incrementation affect the *)
    476476              (*      addition of the PC with the DPTR? At the moment, no.              *)
     
    487487              let 〈addr1, addr2〉 ≝ l in
    488488                set_arg_8 s addr1 (get_arg_8 s false addr2)
    489             | right r ⇒
     489            | inr r ⇒
    490490              let 〈addr1, addr2〉 ≝ r in
    491491                set_arg_8 s addr1 (get_arg_8 s false addr2)
     
    504504                              let 〈addr1, addr2〉 ≝ l'''' in
    505505                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    506                             | right r'''' ⇒
     506                            | inr r'''' ⇒
    507507                              let 〈addr1, addr2〉 ≝ r'''' in
    508508                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    509509                            ]
    510                         | right r''' ⇒
     510                        | inr r''' ⇒
    511511                          let 〈addr1, addr2〉 ≝ r''' in
    512512                            set_arg_8 s addr1 (get_arg_8 s false addr2)
    513513                        ]
    514                     | right r'' ⇒
     514                    | inr r'' ⇒
    515515                      let 〈addr1, addr2〉 ≝ r'' in
    516516                        set_arg_16 s (get_arg_16 s addr2) addr1
    517517                    ]
    518                 | right r ⇒
     518                | inr r ⇒
    519519                  let 〈addr1, addr2〉 ≝ r in
    520520                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
    521521                ]
    522             | right r ⇒
     522            | inr r ⇒
    523523              let 〈addr1, addr2〉 ≝ r in
    524524                set_arg_1 s addr1 (get_arg_1 s addr2 false)
     
    527527          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    528528            [ ADDR16 a ⇒ λaddr16: True.
    529               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     529              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    530530              let s ≝ set_8051_sfr s SFR_SP new_sp in
    531               let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
     531              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    532532              let s ≝ write_at_stack_pointer s pc_bl in
    533               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     533              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    534534              let s ≝ set_8051_sfr s SFR_SP new_sp in
    535535              let s ≝ write_at_stack_pointer s pc_bu in
     
    540540          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    541541            [ ADDR11 a ⇒ λaddr11: True.
    542               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     542              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    543543              let s ≝ set_8051_sfr s SFR_SP new_sp in
    544               let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
     544              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter s) in
    545545              let s ≝ write_at_stack_pointer s pc_bl in
    546               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
     546              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat 8 1) in
    547547              let s ≝ set_8051_sfr s SFR_SP new_sp in
    548548              let s ≝ write_at_stack_pointer s pc_bu in
    549               let 〈thr, eig〉 ≝ split ? three eight a in
    550               let 〈fiv, thr'〉 ≝ split ? five three pc_bu in
     549              let 〈thr, eig〉 ≝ split ? 3 8 a in
     550              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
    551551              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    552552                set_program_counter s new_addr
     
    560560    ntry (
    561561      nnormalize
    562       nrepeat (napply (less_than_or_equal_monotone))
    563       napply (less_than_or_equal_zero)
     562      nrepeat (napply (le_S_S))
     563      napply (le_O_n)
    564564    );
    565565    ntry (
     
    575575nlet rec execute (n: nat) (s: Status) on n: Status ≝
    576576  match n with
    577     [ Z ⇒ s
     577    [ O ⇒ s
    578578    | S o ⇒ execute o (execute_1 s)
    579579    ].
Note: See TracChangeset for help on using the changeset viewer.