include "Status.ma". 
(* include "Fetch.ma". *)
include "Cartesian.ma".
include "Arithmetic.ma".
include "List.ma".

naxiom fetch: BitVectorTrie Byte sixteen → Word → (preinstruction [[relative]]) × Word × Nat.

alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)".

ndefinition sign_extension: Byte → Word ≝
  λb.
    zero eight @@ b.

ndefinition execute_1: Status → Status ≝
  λs.
    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
    let s ≝ set_clock s (clock s + ticks) in
    let s ≝ set_program_counter s pc in
    let s ≝
      match instr with
        [ ADD addr1 addr2 ⇒
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
                                                   (get_arg_8 s false addr2) false in
            let cy_flag ≝ get_index … flags Z ? in
            let ac_flag ≝ get_index … flags one ? in
            let ov_flag ≝ get_index … flags two ? in
            let s ≝ set_arg_8 s ACC_A result in
              set_flags s cy_flag (Just Bit ac_flag) ov_flag
        | ADDC addr1 addr2 ⇒
            let old_cy_flag ≝ get_cy_flag s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
                                                   (get_arg_8 s false addr2) old_cy_flag in
            let cy_flag ≝ get_index … flags Z ? in
            let ac_flag ≝ get_index … flags one ? in
            let ov_flag ≝ get_index … flags two ? in
            let s ≝ set_arg_8 s ACC_A result in
              set_flags s cy_flag (Just Bit ac_flag) ov_flag
        | SUBB addr1 addr2 ⇒
            let old_cy_flag ≝ get_cy_flag s in
            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
                                                   (get_arg_8 s false addr2) old_cy_flag in
            let cy_flag ≝ get_index … flags Z ? in
            let ac_flag ≝ get_index … flags one ? in
            let ov_flag ≝ get_index … flags two ? in
            let s ≝ set_arg_8 s ACC_A result in
              set_flags s cy_flag (Just Bit ac_flag) ov_flag
        | INC addr ⇒
            match addr return λx. bool_to_Prop (is_in … [[ acc_a;
                                                           register;
                                                           direct;
                                                           indirect;
                                                           dptr ]] x) → ? with
              [ ACC_A ⇒ λacc_a: True.
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in
                  set_arg_8 s ACC_A result
              | REGISTER r ⇒ λregister: True.
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in
                  set_arg_8 s (REGISTER r) result
              | DIRECT d ⇒ λdirect: True.
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in
                  set_arg_8 s (DIRECT d) result
              | INDIRECT i ⇒ λindirect: True.
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in
                  set_arg_8 s (INDIRECT i) result
              | DPTR ⇒ λdptr: True.
                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in
                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in
                let s ≝ set_8051_sfr s SFR_DPL bl in
                  set_8051_sfr s SFR_DPH bu
              | _ ⇒ λother: False. ?
              ] (subaddressing_modein … addr)
       | DEC addr ⇒
           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in
             set_arg_8 s addr result
        | MUL addr1 addr2 ⇒
           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
           let product ≝ acc_a_nat * acc_b_nat in
           let ov_flag ≝ product ≥ two_hundred_and_fifty_six in
           let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in
           let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in
           let s ≝ set_8051_sfr s SFR_ACC_A low in
             set_8051_sfr s SFR_ACC_B high
        | DIV addr1 addr2 ⇒
           let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
             match acc_b_nat with
               [ Z ⇒ set_flags s false (Nothing Bit) true
               | S o ⇒
                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
                 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in
                 let s ≝ set_8051_sfr s SFR_ACC_A q in
                 let s ≝ set_8051_sfr s SFR_ACC_B r in
                   set_flags s false (Nothing Bit) false
               ]
        | DA addr ⇒
            let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in
              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
                let cy_flag ≝ get_index ? flags Z ? in
                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in
                    let new_acc ≝ nu @@ acc_nl' in
                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
                      set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
                  else
                    s
              else
                s
        | CLR addr ⇒ 
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
            [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight)
            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr)
        | CPL addr ⇒
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
            [ ACC_A ⇒ λacc_a: True.
                let old_acc ≝ get_8051_sfr s SFR_ACC_A in
                let new_acc ≝ negation_bv ? old_acc in
                  set_8051_sfr s SFR_ACC_A new_acc
            | CARRY ⇒ λcarry: True.
                let old_cy_flag ≝ get_arg_1 s CARRY true in
                let new_cy_flag ≝ negation old_cy_flag in
                  set_arg_1 s CARRY new_cy_flag
            | BIT_ADDR b ⇒ λbit_addr: True.
                let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in
                let new_bit ≝ negation old_bit in
                  set_arg_1 s (BIT_ADDR b) new_bit
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr)
        | SETB b ⇒ set_arg_1 s b false
        | RL _ ⇒ (* DPM: always ACC_A *)
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let new_acc ≝ rotate_left_bv ? one old_acc in
              set_8051_sfr s SFR_ACC_A new_acc
        | RR _ ⇒ (* DPM: always ACC_A *)
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let new_acc ≝ rotate_right_bv ? one old_acc in
              set_8051_sfr s SFR_ACC_A new_acc
        | RLC _ ⇒ (* DPM: always ACC_A *)
            let old_cy_flag ≝ get_cy_flag s in
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
            let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
            let s ≝ set_arg_1 s CARRY new_cy_flag in
              set_8051_sfr s SFR_ACC_A new_acc
        | RRC _ ⇒ (* DPM: always ACC_A *)
            let old_cy_flag ≝ get_cy_flag s in
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
            let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
            let s ≝ set_arg_1 s CARRY new_cy_flag in
              set_8051_sfr s SFR_ACC_A new_acc
        | SWAP _ ⇒ (* DPM: always ACC_A *)
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let 〈nu,nl〉 ≝ split ? four four old_acc in
            let new_acc ≝ nl @@ nu in
              set_8051_sfr s SFR_ACC_A new_acc
        | PUSH addr ⇒
            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
              [ DIRECT d ⇒ λdirect: True.
                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in
                let s ≝ set_8051_sfr s SFR_SP new_sp in
                  write_at_stack_pointer s d
              | _ ⇒ λother: False. ?
              ] (subaddressing_modein … addr)
        | POP addr ⇒
            let contents ≝ read_at_stack_pointer s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in
            let s ≝ set_8051_sfr s SFR_SP new_sp in
              set_arg_8 s addr contents
        | XCH addr1 addr2 ⇒
            let old_addr ≝ get_arg_8 s false addr2 in
            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
            let s ≝ set_8051_sfr s SFR_ACC_A old_addr in
              set_arg_8 s addr2 old_acc
        | XCHD addr1 addr2 ⇒
            let 〈acc_nu, acc_nl〉 ≝ split … four four (get_8051_sfr s SFR_ACC_A) in
            let 〈arg_nu, arg_nl〉 ≝ split … four four (get_arg_8 s false addr2) in
            let new_acc ≝ acc_nu @@ arg_nl in
            let new_arg ≝ arg_nu @@ acc_nl in
            let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
              set_arg_8 s addr2 new_arg
        | Jump j ⇒
          match j with
            [ JC addr ⇒
              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                  if get_cy_flag s then
                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                      set_program_counter s new_pc
                  else
                    s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr)
            | JNC addr ⇒
              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                  if negation (get_cy_flag s) then
                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                      set_program_counter s new_pc
                  else
                    s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr)
            | JB addr1 addr2 ⇒
              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                  if get_arg_1 s addr1 false then
                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                      set_program_counter s new_pc
                  else
                    s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr2)
            | JNB addr1 addr2 ⇒
              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                  if negation (get_arg_1 s addr1 false) then
                    let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                      set_program_counter s new_pc
                  else
                    s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr2)
            | JBC addr1 addr2 ⇒
              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                  let s ≝ set_arg_1 s addr1 false in
                    if get_arg_1 s addr1 false then
                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                        set_program_counter s new_pc
                    else
                      s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr2)
            | JZ addr ⇒
              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                    if eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight) then
                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                        set_program_counter s new_pc
                    else
                      s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr)
            | JNZ addr ⇒
              match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                    if negation (eq_bv ? (get_8051_sfr s SFR_ACC_A) (zero eight)) then
                      let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                        set_program_counter s new_pc
                    else
                      s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr)
            | CJNE addr1 addr2 ⇒ ?
              match addr1 with
                [ Left l ⇒ ?
                | Right r ⇒ ?
                ]
            | DJNZ addr1 addr2 ⇒
              match addr2 return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
                [ RELATIVE r ⇒ λrel: True.
                    let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s true addr1) (bitvector_of_nat eight one) false in
                    let s ≝ set_arg_8 s addr1 result in
                      if negation (eq_bv ? result (zero eight)) then
                        let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
                          set_program_counter s new_pc
                      else
                        s
                | _ ⇒ λother: False. ?
                ] (subaddressing_modein … addr2)
            ]
        | NOP ⇒ s
        | _ ⇒ s
        ]
    in
      s.