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.