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

include "basics/russell.ma".

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

definition Time ≝ nat.

inductive SerialBufferType: Type[0] ≝
  Eight: Byte → SerialBufferType
| Nine: Bit → Byte → SerialBufferType.

inductive LineType: Type[0] ≝
  P1: Byte → LineType
| P3: Byte → LineType
| SerialBuffer: SerialBufferType → LineType.

(* What is a continuation, now? *)

inductive 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.

definition sfr_8051_index ≝
  λs: SFR8051.
    match s with
      [ SFR_SP ⇒ O
      | SFR_DPL ⇒ 1
      | SFR_DPH ⇒ 2
      | SFR_PCON ⇒ 3
      | SFR_TCON ⇒ 4
      | SFR_TMOD ⇒ 5
      | SFR_TL0 ⇒ 6
      | SFR_TL1 ⇒ 7
      | SFR_TH0 ⇒ 8
      | SFR_TH1 ⇒ 9
      | SFR_P1 ⇒ 10
      | SFR_SCON ⇒ 11
      | SFR_SBUF ⇒ 12
      | SFR_IE ⇒ 13
      | SFR_P3 ⇒ 14
      | SFR_IP ⇒ 15
      | SFR_PSW ⇒ 16
      | SFR_ACC_A ⇒ 17
      | SFR_ACC_B ⇒ 18
      ].
      
inductive SFR8052: Type[0] ≝
   SFR_T2CON: SFR8052
|  SFR_RCAP2L: SFR8052
|  SFR_RCAP2H: SFR8052
|  SFR_TL2: SFR8052
|  SFR_TH2: SFR8052.

definition sfr_8052_index ≝
  λs: SFR8052.
    match s with
      [ SFR_T2CON ⇒ O
      | SFR_RCAP2L ⇒ 1
      | SFR_RCAP2H ⇒ 2
      | SFR_TL2 ⇒ 3
      | SFR_TH2 ⇒ 4
      ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Processor status.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝
{
  low_internal_ram: BitVectorTrie Byte 7;
  high_internal_ram: BitVectorTrie Byte 7;
  external_ram: BitVectorTrie Byte 16;
 
  program_counter: Word;
  
  special_function_registers_8051: Vector Byte 19;
  special_function_registers_8052: Vector Byte 5;
  
  p1_latch: Byte;
  p3_latch: Byte;
  
  clock: Time
}.

definition Status ≝ PreStatus (BitVectorTrie Byte 16).
definition PseudoStatus ≝ PreStatus (pseudo_assembly_program).

lemma sfr8051_index_19:
  ∀i: SFR8051.
    sfr_8051_index i < 19.
 # i
 cases i
 normalize
 repeat (@ le_S_S)
 @ le_O_n
qed.
    
lemma sfr8052_index_5:
  ∀i: SFR8052.
    sfr_8052_index i < 5.
 # i
 cases i
 normalize
 repeat (@ le_S_S)
 @ le_O_n
qed.
    
definition set_clock ≝ 
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λt: Time.
    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 old_p1_latch ≝ p1_latch ?? s in    
    let old_p3_latch ≝ p3_latch ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                old_p3_latch
                t.
    
definition set_p1_latch ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
    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 old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                b
                old_p3_latch
                old_clock.

definition set_p3_latch ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
    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 old_p1_latch ≝ p1_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                b
                old_clock.

definition get_8051_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λi: SFR8051.
    let sfr ≝ special_function_registers_8051 ?? s in
    let index ≝ sfr_8051_index i in
      get_index_v … sfr index ?.
    @ sfr8051_index_19
qed.

definition get_8052_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λi: SFR8052.
    let sfr ≝ special_function_registers_8052 ?? s in
    let index ≝ sfr_8052_index i in
      get_index_v … sfr index ?.
    @ sfr8052_index_5
qed.

definition set_8051_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λi: SFR8051.
  λb: Byte.
    let index ≝ sfr_8051_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
    let new_special_function_registers_8051 ≝
      set_index Byte 19 old_special_function_registers_8051 index b ? in
    let old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M 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
                old_p1_latch
                old_p3_latch
                old_clock.
    @ (sfr8051_index_19 i)
qed.

lemma clock_set_8051_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
        clock … code_memory s = clock … code_memory (set_8051_sfr M code_memory s i b).
  #M #code_memory #s #i #b // 
qed.

definition set_8052_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λi: SFR8052.
  λb: Byte.
    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
    let new_special_function_registers_8052 ≝
      set_index Byte 5 old_special_function_registers_8052 index b ? in
    let old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M 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
                old_p1_latch
                old_p3_latch
                old_clock.
    @ (sfr8052_index_5 i)
qed.

lemma clock_set_8052_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀i,b.
        clock … code_memory s = clock … code_memory (set_8052_sfr M code_memory s i b).
  #M #code_memory #s #i #b //
qed.

definition set_program_counter ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λw: Word.
    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
    let old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                old_high_internal_ram
                old_external_ram
                w
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                old_p3_latch
                old_clock.
                
definition set_code_memory ≝
  λM,M': Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: M'.
    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 old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M' 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
                old_p1_latch
                old_p3_latch
                old_clock.
                
definition set_low_internal_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVectorTrie Byte 7.
    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 old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                r
                old_high_internal_ram
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                old_p3_latch
                old_clock.
                
definition update_low_internal_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λaddr,v.
  let old_low_internal_ram ≝ low_internal_ram ?? s in
  let new_low_internal_ram ≝ insert ?? addr v old_low_internal_ram in
      set_low_internal_ram … s new_low_internal_ram.
            
lemma clock_set_low_internal_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r.
        clock … code_memory s = clock … code_memory (set_low_internal_ram M code_memory s r).
  #M #code_memory #s #r //
qed.

lemma clock_update_low_internal_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
        clock … code_memory s = clock … code_memory (update_low_internal_ram M code_memory s addr v).
  #M #code_memory #s #addr #v // 
qed.

definition set_high_internal_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVectorTrie Byte 7.
    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 old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                r
                old_external_ram
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                old_p3_latch
                old_clock.
                
definition update_high_internal_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λaddr,v.
  let old_high_internal_ram ≝ high_internal_ram ?? s in
  let new_high_internal_ram ≝ insert ?? addr v old_high_internal_ram in
      set_high_internal_ram … s new_high_internal_ram.

lemma clock_set_high_internal_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 7.
        clock … code_memory s = clock … code_memory (set_high_internal_ram M code_memory s r).
  #M #code_memory #s #r //
qed.

lemma clock_update_high_internal_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr,v.
        clock … code_memory s = clock … code_memory (update_high_internal_ram M code_memory s addr v).
  #M #code_memory #s #addr #v //
qed.

definition set_external_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVectorTrie Byte 16.
    let old_low_internal_ram ≝ low_internal_ram ?? s in
    let old_high_internal_ram ≝ high_internal_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 old_p1_latch ≝ p1_latch ?? s in
    let old_p3_latch ≝ p3_latch ?? s in
    let old_clock ≝ clock ?? s in
      mk_PreStatus M code_memory
                old_low_internal_ram
                old_high_internal_ram
                r
                old_program_counter
                old_special_function_registers_8051
                old_special_function_registers_8052
                old_p1_latch
                old_p3_latch
                old_clock.
                
definition update_external_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λaddr,v.
  let old_external_ram ≝ external_ram ?? s in
  let new_external_ram ≝ insert ?? addr v old_external_ram in
      set_external_ram … s new_external_ram.

lemma clock_set_external_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀r: BitVectorTrie Byte 16. 
        clock … code_memory s = clock … code_memory (set_external_ram M code_memory s r).
  #M #code_memory #s #r //
qed.

lemma clock_update_external_ram:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀addr: Word. ∀v: Byte. 
        clock … code_memory s = clock … code_memory (update_external_ram M code_memory s addr v).
  #M #code_memory #s #addr #v //
qed.

definition get_psw_flags ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory. 
  λflag. 
  λflag_ok: flag < ?.        
    let psw ≝ get_8051_sfr … s SFR_PSW in
      get_index_v bool ? psw flag flag_ok.
                
definition get_cy_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 0 ?. //
qed.

definition get_ac_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 1 ?. //
qed.

definition get_fo_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 2 ?. //
qed.

definition get_rs1_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 3 ?. //
qed.

definition get_rs0_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 4 ?. //
qed.

definition get_ov_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 5 ?. //
qed.

definition get_ud_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 6 ?. //
qed.

definition get_p_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    get_psw_flags … s 7 ?. //
qed.

definition set_flags ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λcy: Bit.
  λac: option Bit.
  λov: Bit.
    (*let sfr_psw ≝ get_8051_sfr ?? s SFR_PSW in *)
    let old_cy ≝ get_cy_flag ?? s (* get_index_v ?? sfr_psw O ?*) in
    let old_ac ≝ get_ac_flag ?? s (* get_index_v ?? sfr_psw 1 ?*) in
    let old_fo ≝ get_fo_flag ?? s (* get_index_v ?? sfr_psw 2 ?*) in
    let old_rs1 ≝ get_rs1_flag ?? s (* get_index_v ?? sfr_psw 3 ?*) in
    let old_rs0 ≝ get_rs0_flag ?? s (* get_index_v ?? sfr_psw 4 ?*) in
    let old_ov ≝ get_ov_flag ?? s (* get_index_v ?? sfr_psw 5 ?*) in
    let old_ud ≝ get_ud_flag ?? s (* get_index_v ?? sfr_psw 6 ?*) in
    let old_p ≝ get_p_flag ?? s (* get_index_v ?? sfr_psw 7 ?*) in
    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
      set_8051_sfr ?? s SFR_PSW
      [[ cy ; new_ac ; old_fo ; old_rs1 ;
         old_rs0 ; ov ; old_ud ; old_p ]].

definition initialise_status ≝
  λM: Type[0].
  λcode_mem: M.
  let status ≝ mk_PreStatus M code_mem                 (* Code mem. *)
                         (Stub …)                      (* Low mem.  *)
                         (Stub …)                      (* High mem. *)
                         (Stub …)                      (* Ext mem.  *)
                         (zero ?)                      (* PC.       *)
                         (replicate … (zero ?))        (* 8051 SFR. *)
                         (replicate … (zero ?))        (* 8052 SFR. *)
                         (zero ?)                      (* P1 latch. *)
                         (zero ?)                      (* P3 latch. *)
                         O                             (* Clock.    *)
  in
    set_8051_sfr ?? status SFR_SP (bitvector_of_nat ? 7).
  
definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝
  λb: Byte.
    let address ≝ nat_of_bitvector … b in
      if (eqb address 128) then None ?
      else if (eqb address 144) then Some … (inl … SFR_P1)
      else if (eqb address 160) then None ?
      else if (eqb address 176) then Some … (inl … SFR_P3)
      else if (eqb address 153) then Some … (inl … SFR_SBUF)
      else if (eqb address 138) then Some … (inl … SFR_TL0)
      else if (eqb address 139) then Some … (inl … SFR_TL1)
      else if (eqb address 140) then Some … (inl … SFR_TH0)
      else if (eqb address 141) then Some … (inl … SFR_TH1)
      else if (eqb address 200) then Some … (inr … SFR_T2CON)
      else if (eqb address 202) then Some … (inr … SFR_RCAP2L)
      else if (eqb address 203) then Some … (inr … SFR_RCAP2H)
      else if (eqb address 204) then Some … (inr … SFR_TL2)
      else if (eqb address 205) then Some … (inr … SFR_TH2)
      else if (eqb address 135) then Some … (inl … SFR_PCON)
      else if (eqb address 136) then Some … (inl … SFR_TCON)
      else if (eqb address 137) then Some … (inl … SFR_TMOD)
      else if (eqb address 152) then Some … (inl … SFR_SCON)
      else if (eqb address 168) then Some … (inl … SFR_IE)
      else if (eqb address 184) then Some … (inl … SFR_IP)
      else if (eqb address 129) then Some … (inl … SFR_SP)
      else if (eqb address 130) then Some … (inl … SFR_DPL)
      else if (eqb address 131) then Some … (inl … SFR_DPH)
      else if (eqb address 208) then Some … (inl … SFR_PSW)
      else if (eqb address 224) then Some … (inl … SFR_ACC_A)
      else if (eqb address 240) then Some … (inl … SFR_ACC_B)
      else None ?.

definition get_bit_addressable_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
  λl: bool.
  match sfr_of_Byte b with
  [ None ⇒ match not_implemented in False with [ ]
  | Some sfr8051_8052 ⇒
    match sfr8051_8052 with
    [ inl sfr ⇒
      match sfr with
      [ SFR_P1 ⇒
        if l then
          p1_latch … s
        else
          get_8051_sfr … s SFR_P1
      | SFR_P3 ⇒
        if l then
          p3_latch … s
        else
          get_8051_sfr … s SFR_P3
      | _ ⇒ get_8051_sfr … s sfr
      ]
    | inr sfr ⇒ get_8052_sfr M code_memory s sfr
    ]
  ].

definition set_bit_addressable_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
  λv: Byte.
   match sfr_of_Byte b with
   [ None ⇒ match not_implemented in False with [ ]
   | Some sfr8051_8052 ⇒
      match sfr8051_8052 with
      [ inl sfr ⇒
         match sfr with
         [ SFR_P1 ⇒
           let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
           set_p1_latch ?? s v
         | SFR_P3 ⇒
           let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
           set_p3_latch ?? s v
         | _ ⇒ set_8051_sfr ?? s sfr v ]
      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]].

lemma clock_set_bit_addressable_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
        clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v).
  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
  cases (sfr_of_Byte ?)
  [1: 
    normalize nodelta cases not_implemented
  |2: 
    * * %
  ]
qed.

lemma program_counter_set_bit_addressable_sfr:
    ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. ∀b: Byte. ∀v: Byte.
        program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v).
  #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????);
  cases (sfr_of_Byte ?)
  [1:
    normalize nodelta cases not_implemented
  |2:
    * * %
  ]
qed.

definition bit_address_of_register ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVector 3.
    let b ≝ get_index_v … r O ? in
    let c ≝ get_index_v … r 1 ? in
    let d ≝ get_index_v … r 2 ? in
(* JHM: redundant bit-twiddling, once you have get_*_flag helpers 
    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 
*)
    let r1 ≝ get_rs1_flag ?? s in 
    let r0 ≝ get_rs0_flag ?? s in 
    let offset ≝
      if ¬r1 ∧ ¬r0 then
        O
      else if ¬r1 ∧ r0 then
        8
      else if r1 ∧ r0 then
        24
      else
        16
    in
      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
  //
qed.

definition get_register ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVector 3.
    let address ≝ bit_address_of_register … s r in
      lookup ?? address (low_internal_ram … s) (zero ?).

definition set_register ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λr: BitVector 3.
  λv: Byte.
    let address ≝ bit_address_of_register … s r in
    (*      
    let old_low_internal_ram ≝ low_internal_ram ?? s in
    let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
      set_low_internal_ram … s new_low_internal_ram.
    *)
    update_low_internal_ram … s address v.
      
definition read_from_external_ram ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λaddr: Word.
    lookup ?? addr (external_ram … s) (zero ?).

definition read_from_internal_ram ≝ (* JHM: lots of 7bits+HI/Lo vs. 8bit redundancy throughout *)
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λaddr: Byte.
    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    let memory ≝
      if head' … bit_one then
        (high_internal_ram ?? s)
      else
        (low_internal_ram ?? s)
    in
      lookup … seven_bits memory (zero ?).

definition read_at_stack_pointer ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    read_from_internal_ram … s (get_8051_sfr ?? s SFR_SP).

definition write_at_stack_pointer ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λv: Byte.
    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
      if head' … bit_one then
      (*
        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
          set_high_internal_ram ?? s memory
      *)
        update_high_internal_ram … s seven_bits v
      else
      (*
        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
          set_low_internal_ram ?? s memory.
      *)
        update_low_internal_ram … s seven_bits v.

definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝
  λM,code_memory,s,v,a.
   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
     [ DPTR ⇒ λ_:True.
       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
       let status ≝ set_8051_sfr … s SFR_DPH bu in
       let status ≝ set_8051_sfr … status SFR_DPL bl in
         status
     | _ ⇒ λK.
       match K in False with
       [
       ]
     ] (subaddressing_modein … a).
 //
qed.

definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝
 set_arg_16'.

lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x).
 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2
qed.

definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory →
  [[ data16 ; acc_dptr ]] → Word ≝
  λm, cm, s, a.
    match a return λx. bool_to_Prop (is_in ? [[ data16 ; acc_dptr ]] x) → ? with
      [ DATA16 d ⇒ λ_:True. d
      | ACC_DPTR ⇒ λ_:True.
        let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
        let big_acc ≝ (zero ?) @@ (get_8051_sfr … s SFR_ACC_A) in
        add … big_acc dptr
      | _ ⇒ Ⓧ
      ] (subaddressing_modein … a).
      
definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;
                                          acc_a ; acc_b ; data ; acc_dptr ;
                                          acc_pc ; ext_indirect ;
                                          ext_indirect_dptr ]] → Byte ≝
  λm, cm, s, l, a.
    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
                                                acc_a ; acc_b ; data ; acc_dptr ;
                                                acc_pc ; ext_indirect ;
                                                ext_indirect_dptr ]] x) → ? with
      [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A
      | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B
      | DATA d ⇒ λdata: True. d
      | REGISTER r ⇒ λregister: True. get_register ?? s r
      | EXT_INDIRECT_DPTR ⇒
        λext_indirect_dptr: True.
          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
            read_from_external_ram … s address
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]]  in
          let padded_address ≝ pad 8 ? address in
            read_from_external_ram … s padded_address
      | ACC_DPTR ⇒
        λacc_dptr: True.
          let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in
            read_from_external_ram … s address
      | ACC_PC ⇒
        λacc_pc: True.
          let padded_acc ≝ pad 8 ? (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
            read_from_external_ram … s address
      | DIRECT d ⇒ (* JHM: simplify false branch with read_from_internal_ram *)
        λdirect: True.
          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
            match head' … hd with
            [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l
             (* XXX: get_bit_addressable_sfr m cm s d l *)
            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
             (* XXX: read_from_internal_ram … s d *)
            ]
      | INDIRECT i ⇒ (* JHM: simplify completely with read_from_internal_ram *)
        λindirect: True.
          let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in
            match head' … hd with
            [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero ?)
            | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero ?)
            ]
          (* XXX: read_from_internal_ram … s (get_register … s [[false;false;i]]) *)
      | _ ⇒ λother.
        match other in False with [ ]
      ] (subaddressing_modein … a).

definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;
                                   acc_a ; acc_b ; ext_indirect ;
                                   ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝
  λm, cm, s, a, v.
    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
                                                acc_a ; acc_b ; ext_indirect ;
                                                ext_indirect_dptr ]] x) →
                   PreStatus m cm
            with
      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
        λdirect: True.
          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
            match head' … bit_one with
              [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v
              | false ⇒ update_low_internal_ram … s seven_bits v
                (*let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory*)
              ]
      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
        λindirect: True.
          let register ≝ get_register ?? s [[ false; false; i ]] in
          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
            match head' … bit_one with
              [ false ⇒ update_low_internal_ram … s seven_bits v
                (*let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory*)
              | true ⇒ update_high_internal_ram … s seven_bits v
                (*let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
                  set_high_internal_ram ?? s memory*)
              ]
      | REGISTER r ⇒ λregister: True. set_register ?? s r v
      | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v
      | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]] in
          let padded_address ≝ pad 8 8 address in
          (*
          let memory ≝ insert ?? padded_address v (external_ram ?? s) in
            set_external_ram ?? s memory
          *)
          update_external_ram … s padded_address v
      | EXT_INDIRECT_DPTR ⇒
        λext_indirect_dptr: True.
          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
          (*
          let memory ≝ insert ?? address v (external_ram ?? s) in
            set_external_ram ?? s memory
          *)
          update_external_ram … s address v
      | _ ⇒ 
        λother: False.
          match other in False with [ ]
      ] (subaddressing_modein … a).

lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v) ≝ 
  λm, cm, s, a, v.
    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
                                                acc_a ; acc_b ; ext_indirect ;
                                                ext_indirect_dptr ]] x) →
                   clock … cm s = clock … cm (set_arg_8 … s x v)
            with
      [ DIRECT d ⇒ (* JHM: should simplify false branch with update_internal_ram *)
        λdirect: True.
          let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in
            match head' … bit_one with
              [ true ⇒ ?
              | false ⇒ ?
              ]
      | INDIRECT i ⇒ (* JHM: should simplify completely with update_internal_ram *)
        λindirect: True.
          let register ≝ get_register ?? s [[ false; false; i ]] in
          let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in
            match head' … bit_one with
              [ false ⇒ ?
              | true ⇒ ?
              ]
      | REGISTER r ⇒ λregister: True. ?
      | ACC_A ⇒ λacc_a: True. ?
      | ACC_B ⇒ λacc_b: True. ?
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]] in
          let padded_address ≝ pad 8 8 address in
            ?
      | EXT_INDIRECT_DPTR ⇒
        λext_indirect_dptr: True.
          let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in
            ?
      | _ ⇒ 
        λother: False.
          match other in False with [ ]
      ] (subaddressing_modein … a). 
  //
  whd in match set_arg_8; normalize nodelta
(* XXX: non-Russell way
  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
    cases x * normalize nodelta 
  [1: #d #ok cases (vsplit ? 1 7 d) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
    [1: @clock_set_bit_addressable_sfr
    |2: @clock_update_low_internal_ram
    ]
  |2: #i #ok cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta
    [1: @clock_update_high_internal_ram
    |2: @clock_update_low_internal_ram
    ]
  |3: #b1 #ok @clock_update_external_ram
  |4: #b3 #ok @clock_update_low_internal_ram
  |5,6: #ok @clock_set_8051_sfr
  |12: #ok @clock_update_external_ram
  ]
  cases not_implemented (* JHM: there has to be a better way to deal with the absurd branches *)
*)
  [1: (* case DIRECT d *)
    cases (vsplit ? 1 7 d) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
  |2: (* case DIRECT d; why the repetition? *)
    cases (vsplit ? 1 7 d) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
  |3: (* case INDIRECT i *)
    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
   |4: (* case INDIRECT i; why the repetition? *)
    cases (vsplit ? 1 7 (get_register ?? s [[ false; false; i ]])) normalize nodelta
    #bit_one #seven_bits cases (head' … bit_one) normalize nodelta //
  ]
qed.

(* XXX: these --- like those above --- belong in StatusProofs*.ma ??? *)
lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v).
  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
  cases daemon
qed.

lemma p1_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p1_latch M cm s = p1_latch … (set_arg_8 M cm s x v).
  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
  cases daemon
qed.

lemma p3_latch_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. p3_latch M cm s = p3_latch … (set_arg_8 M cm s x v).
  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
  cases daemon
qed.

lemma special_function_registers_8052_set_arg_8: ∀M.∀cm.∀s.∀x: [[indirect; registr; acc_a; acc_b; ext_indirect; ext_indirect_dptr]]. ∀v. special_function_registers_8052 M cm s = special_function_registers_8052 … (set_arg_8 M cm s x v).
  [2: /2 by subaddressing_modein, orb_Prop_r/ ]
  #M #cm #s #x #v whd in match set_arg_8; normalize nodelta
  cases daemon
qed.

theorem modulus_less_than:
  ∀m,n: nat. (m mod (S n)) < S n.
  #n #m
  normalize
  @ le_S_S
  lapply (le_n n)
  generalize in ⊢ (?%? → ?(??%?)?);
  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
  [ normalize
    #n
    @ (less_than_or_equal_b_elim n m)
    normalize
    [ //
    | #H #K
      @(le_inv_ind ?? K …)
      [ # H1
        < H1
        //
      | #x #H1 #H2 #H3
        destruct
      ]
    ]
  | normalize
    # y # H1 # n # H2
    @ (less_than_or_equal_b_elim n m)
    normalize
    [ //
    | # K
      @ H1
      cut (n ≤ S y → n - S m ≤ y)
      /2 by/
      cases n
      normalize
      //
      # x # K1
      lapply (le_S_S_to_le … K1)
      generalize in match m;
      elim x
      normalize
      //
      # w1 # H # m
      cases m
      normalize
      //
      # q # K2
      @H
      /3/
    ]
  ]
qed.

definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →
                       bool → bool ≝
  λm, cm, s, a, l.
    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
                                                 n_bit_addr ;
                                                 carry ]] x) → ? with
      [ BIT_ADDR b ⇒
        λbit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in
        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
        match head' … bit_1 with
        [ true ⇒
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
            get_index_v … sfr (nat_of_bitvector … three_bits) ?
        | false ⇒
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup ?? address' (low_internal_ram ?? s) (zero ?) in
            get_index_v … t (nat_of_bitvector … three_bits) ? 
        ]
      | N_BIT_ADDR n ⇒
        λn_bit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in
        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 
        match head' … bit_1 with
        [ true ⇒
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
        | false ⇒
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?) 
        ]
      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
      | _ ⇒ λother.
        match other in False with [ ]
      ] (subaddressing_modein … a).
  //
qed.
      
definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝
  λm: Type[0].
  λcm.
  λs: PreStatus m cm.
  λa: [[bit_addr; carry]].
  λv: Bit.
    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with
      [ BIT_ADDR b ⇒ λbit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
        match head' … bit_1 with
        [ true ⇒
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr … s trans true in
          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
            set_bit_addressable_sfr … s new_sfr trans
        | false ⇒
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero ?) in
          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
          (*
          let memory ≝ insert ?? address' n_bit (low_internal_ram ?? s) in
            set_low_internal_ram … s memory
          *)
            update_low_internal_ram … s address' n_bit 
        ]
      | CARRY ⇒
        λcarry: True.
        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
        let new_psw ≝ v:::seven_bits in
          set_8051_sfr ?? s SFR_PSW new_psw
      | _ ⇒
        λother: False.
          match other in False with
            [ ]
      ] (subaddressing_modein … a).
  //
qed.

(* JHM: Russell-style works, modulo some oddities...??? *)
lemma clock_set_arg_1: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v) 
  ≝ 
  λm: Type[0].
  λcm.
  λs: PreStatus m cm.
  λa: [[bit_addr; carry]].
  λv: Bit.      
    match a 
    return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → 
     clock m cm s = clock … (set_arg_1 m cm s x v)
    with
      [ BIT_ADDR b ⇒ λbit_addr: True.
        let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 b in
        let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
        match head' … bit_1 with
        [ true ⇒
          let trans ≝ true:::four_bits @@ [[false; false; false]] in
          let sfr ≝ get_bit_addressable_sfr … s trans true in
          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
            ?
        | false ⇒
          let address' ≝ [[true; false; false]]@@four_bits in
          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
            ?
        ]
      | CARRY ⇒
        λcarry: True.
        let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in
        let new_psw ≝ v:::seven_bits in
          ?
      | _ ⇒
        λother: False.
          match other in False with
            [ ]
      ] (subaddressing_modein … a). //
      whd in match set_arg_1; normalize nodelta      
  [1: (* case: CARRY *)
    cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
    #ignore #seven_bits normalize nodelta @clock_set_8051_sfr
  |2: (* case: BIT_ADDR *)
    cases (vsplit bool 1 7 b)
    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
    [1: @clock_set_bit_addressable_sfr
    |2: @clock_update_low_internal_ram
    ]
  |3: (* case: BIT_ADDR, again; why? *)
    cases (vsplit bool 1 7 b)
    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
    [1: @clock_set_bit_addressable_sfr
    |2: @clock_update_low_internal_ram
    ]
  ]
qed.

lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 
(* JHM: boring, non-Russell way 
  #m #cm #s #x #v whd in match set_arg_1;
  cases x * normalize nodelta 
  [14: #ok cases (vsplit bool 1 7 (get_8051_sfr … s SFR_PSW))
    #ignore #seven_bits @clock_set_8051_sfr
  |15: #b #ok cases (vsplit bool 1 7 b)
    #bit_1 #seven_bits normalize nodelta cases (vsplit bool 4 3 seven_bits)
    #four_bits #three_bits normalize nodelta cases (head' … bit_1)
    [1: @clock_set_bit_addressable_sfr
    |2: @clock_set_low_internal_ram
    ]
  ] cases not_implemented (* XXX: there has to be a better way to deal with the absurd branches *)
*)
  @clock_set_arg_1
qed. 


definition construct_datalabels: list (Identifier × Word) →
  identifier_map ASMTag Word ≝
  λthe_preamble.
  \fst (foldl ?? (λt,preamble.
      let 〈datalabels, addr〉 ≝ t in
      let 〈name, size〉 ≝ preamble in
      let 〈addr, carry〉 ≝ sub_16_with_carry addr size false in
      〈add ?? datalabels name addr, addr〉)
    (* mcu8051ide disallows XDATA access at -1, bug or feature? *)
    〈empty_map …, maximum …〉 the_preamble).