(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Interpret.ma: Operational semantics for the 8051/8052 processor.           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* include "ASM.ma". *)
include "Arithmetic.ma".
include "BitVectorTrie.ma".

ninductive SFR8051: Type[0] ≝
  SFR_SP: SFR8051
| SFR_DPL: SFR8051
| SFR_DPH: SFR8051
| SFR_PCON: SFR8051
| SFR_TCON: SFR8051
| SFR_TMOD: SFR8051
| SFR_TL0: SFR8051
| SFR_TL1: SFR8051
| SFR_TH0: SFR8051
| SFR_TH1: SFR8051
| SFR_P1: SFR8051
| SFR_SCON: SFR8051
| SFR_SBUF: SFR8051
| SFR_IE: SFR8051
| SFR_P3: SFR8051
| SFR_IP: SFR8051
| SFR_PSW: SFR8051
| SFR_ACC_A: SFR8051
| SFR_ACC_B: SFR8051.

ndefinition sfr_8051_index ≝
  λs: SFR8051.
    match s with
      [ SFR_SP ⇒ Z
      | SFR_DPL ⇒ S Z
      | SFR_DPH ⇒ two
      | SFR_PCON ⇒ three
      | SFR_TCON ⇒ four
      | SFR_TMOD ⇒ five
      | SFR_TL0 ⇒ six
      | SFR_TL1 ⇒ seven
      | SFR_TH0 ⇒ eight
      | SFR_TH1 ⇒ nine
      | SFR_P1 ⇒ ten
      | SFR_SCON ⇒ eleven
      | SFR_SBUF ⇒ twelve
      | SFR_IE ⇒ thirteen
      | SFR_P3 ⇒ fourteen
      | SFR_IP ⇒ fifteen
      | SFR_PSW ⇒ sixteen
      | SFR_ACC_A ⇒ seventeen
      | SFR_ACC_B ⇒ eighteen
      ].
      
ninductive SFR8052: Type[0] ≝
   SFR_T2CON: SFR8052
|  SFR_RCAP2L: SFR8052
|  SFR_RCAP2H: SFR8052
|  SFR_TL2: SFR8052
|  SFR_TH2: SFR8052.

ndefinition sfr_8052_index ≝
  λs: SFR8052.
    match s with
      [ SFR_T2CON ⇒ Z
      | SFR_RCAP2L ⇒ S Z
      | SFR_RCAP2H ⇒ two
      | SFR_TL2 ⇒ three
      | SFR_TH2 ⇒ four 
      ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Processor status.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
nrecord Status: Type[0] ≝
{
  code_memory: BitVectorTrie Byte sixteen;
  low_internal_ram: BitVectorTrie Byte seven;
  high_internal_ram: BitVectorTrie Byte seven;
  external_ram: BitVectorTrie Byte sixteen;
 
  program_counter: Word;
  
  special_function_registers_8051: Vector Byte nineteen;
  special_function_registers_8052: Vector Byte five
}.

ncheck special_function_registers_8051.

naxiom sfr8051_index_nineteen:
  ∀i: SFR8051.
    sfr_8051_index i < nineteen.
    
naxiom sfr8052_index_five:
  ∀i: SFR8052.
    sfr_8052_index i < five.

ndefinition get_8051_sfr ≝
  λs: Status.
  λi: SFR8051.
    let sfr ≝ special_function_registers_8051 s in
    let index ≝ sfr_8051_index i in
      get_index … sfr index ?.
    napply (sfr8051_index_nineteen i).
nqed.

ndefinition get_8052_sfr ≝
  λs: Status.
  λi: SFR8052.
    let sfr ≝ special_function_registers_8052 s in
    let index ≝ sfr_8052_index i in
      get_index … sfr index ?.
    napply (sfr8052_index_five i).
nqed.

ndefinition set_8051_sfr ≝
  λs: Status.
  λi: SFR8051.
  λb: Byte.
    let index ≝ sfr_8051_index i in
    let old_code_memory ≝ code_memory s in
    let old_low_internal_ram ≝ low_internal_ram s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_program_counter ≝ program_counter s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    let new_special_function_registers_8051 ≝
      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
      mk_Status old_code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                new_special_function_registers_8051
                old_special_function_registers_8052.
    napply (sfr8051_index_nineteen i).
nqed.

ndefinition set_8052_sfr ≝
  λs: Status.
  λi: SFR8052.
  λb: Byte.
    let index ≝ sfr_8052_index i in
    let old_code_memory ≝ code_memory s in
    let old_low_internal_ram ≝ low_internal_ram s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_program_counter ≝ program_counter s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    let new_special_function_registers_8052 ≝
      cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
      mk_Status old_code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                new_special_function_registers_8052.
    napply (sfr8052_index_five i).
nqed.

ndefinition set_program_counter ≝
  λs: Status.
  λi: SFR8052.
  λw: Word.
    let index ≝ sfr_8052_index i in
    let old_code_memory ≝ code_memory s in
    let old_low_internal_ram ≝ low_internal_ram s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
      mk_Status old_code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                w
                old_special_function_registers_8051
                old_special_function_registers_8052.
                
ndefinition set_code_memory ≝
  λs: Status.
  λi: SFR8052.
  λr: BitVectorTrie Byte sixteen.
    let index ≝ sfr_8052_index i in
    let old_low_internal_ram ≝ low_internal_ram s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_program_counter ≝ program_counter s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
      mk_Status r
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052.
                
ndefinition set_low_internal_ram ≝
  λs: Status.
  λi: SFR8052.
  λr: BitVectorTrie Byte seven.
    let index ≝ sfr_8052_index i in
    let old_code_memory ≝ code_memory s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_program_counter ≝ program_counter s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
      mk_Status old_code_memory
                r
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052.
                
ndefinition get_cy_flag ≝
  λs: Status.
    let sfr ≝ special_function_registers_8051 s in
    let psw ≝ get_index … (get_8051_index SFR_PSW) s ? in
      get_index … Z psw ?.
                
ndefinition set_high_internal_ram ≝
  λs: Status.
  λi: SFR8052.
  λr: BitVectorTrie Byte seven.
    let index ≝ sfr_8052_index i in
    let old_code_memory ≝ code_memory s in
    let old_low_internal_ram ≝ low_internal_ram s in
    let old_high_internal_ram ≝ high_internal_ram s in
    let old_external_ram ≝ external_ram s in
    let old_program_counter ≝ program_counter s in
    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
      mk_Status old_code_memory
                old_low_internal_ram
                r
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052.

ndefinition initialise_status ≝
  let status ≝ mk_Status (Stub Byte sixteen)
                         (Stub Byte seven)
                         (Stub Byte seven)
                         (Stub Byte sixteen)
                         (zero sixteen)
                         (replicate Byte nineteen (zero eight))
                         (replicate Byte five (zero eight)) in
  status.