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

include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/BitVectorTrie.ma".
include "basics/russell.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.

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.

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 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 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 get_cy_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw O ?.
    normalize
    @ (le_S_S ? ?)
    [ @ le_O_n
    | repeat (@ (le_S_S));
      //
    ]
qed.

definition get_ac_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 1 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_fo_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 2 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_rs1_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 3 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_rs0_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 4 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_ov_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 5 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_ud_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 6 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition get_p_flag ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let sfr ≝ special_function_registers_8051 ?? s in
    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
      get_index_v bool 8 psw 7 ?.
    normalize
    repeat (@ (le_S_S ? ?))
    @ le_O_n
qed.

definition set_flags ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λcy: Bit.
  λac: option Bit.
  λov: Bit.
    let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in
    let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in
    let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in
    let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in
    let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in
    let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in
    let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in
    let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in
    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
      set_8051_sfr ?? s SFR_PSW
      [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
         old_rs0 ; old_ov ; old_ud ; old_p ]].
    [1,2,3,4,5,6,7,8:
       normalize
       repeat (@ le_S_S)
       @ le_O_n
    ]
qed.

definition initialise_status ≝
  λM: Type[0].
  λcode_mem: M.
  let status ≝ mk_PreStatus M code_mem                    (* Code mem. *)
                         (Stub Byte 7)                      (* Low mem.  *)
                         (Stub Byte 7)                      (* High mem. *)
                         (Stub Byte 16)                    (* Ext mem.  *)
                         (zero 16)                         (* PC.       *)
                         (replicate Byte 19 (zero 8)) (* 8051 SFR. *)
                         (replicate Byte 5 (zero 8))     (* 8052 SFR. *)
                         (zero 8)                           (* P1 latch. *)
                         (zero 8)                           (* P3 latch. *)
                         O                                      (* Clock.    *)
  in
    set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7).
  
definition get_bit_addressable_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λn: nat.
  λb: BitVector n.
  λl: bool.
    let address ≝ nat_of_bitvector … b in
      if (eqb address 128) then
        ?
      else if (eqb address 144) then
        if l then
          (p1_latch ?? s)
        else
          (get_8051_sfr ?? s SFR_P1)
      else if (eqb address 160) then
        ?
      else if (eqb address 176) then
        if l then
          (p3_latch ?? s)
        else
          (get_8051_sfr ?? s SFR_P3)
      else if (eqb address 153) then
        get_8051_sfr ?? s SFR_SBUF
      else if (eqb address 138) then
        get_8051_sfr ?? s SFR_TL0
      else if (eqb address 139) then
        get_8051_sfr ?? s SFR_TL1
      else if (eqb address 140) then
        get_8051_sfr ?? s SFR_TH0
      else if (eqb address 141) then
        get_8051_sfr ?? s SFR_TH1
      else if (eqb address 200) then
        get_8052_sfr ?? s SFR_T2CON
      else if (eqb address 202) then
        get_8052_sfr ?? s SFR_RCAP2L
      else if (eqb address 203) then
        get_8052_sfr ?? s SFR_RCAP2H
      else if (eqb address 204) then
        get_8052_sfr ?? s SFR_TL2
      else if (eqb address 205) then
        get_8052_sfr ?? s SFR_TH2
      else if (eqb address 135) then
        get_8051_sfr ?? s SFR_PCON
      else if (eqb address 136) then
        get_8051_sfr ?? s SFR_TCON
      else if (eqb address 137) then
        get_8051_sfr ?? s SFR_TMOD
      else if (eqb address 152) then
        get_8051_sfr ?? s SFR_SCON
      else if (eqb address 168) then
        get_8051_sfr ?? s SFR_IE
      else if (eqb address 184) then
        get_8051_sfr ?? s SFR_IP
      else if (eqb address 129) then
        get_8051_sfr ?? s SFR_SP
      else if (eqb address 130) then
        get_8051_sfr ?? s SFR_DPL
      else if (eqb address 131) then
        get_8051_sfr ?? s SFR_DPH
      else if (eqb address 208) then
        get_8051_sfr ?? s SFR_PSW
      else if (eqb address 224) then
        get_8051_sfr ?? s SFR_ACC_A
      else if (eqb address 240) then
        get_8051_sfr ?? s SFR_ACC_B
      else
        ?.
      cases not_implemented
qed.

definition set_bit_addressable_sfr ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λb: Byte.
  λv: Byte.
    let address ≝ nat_of_bitvector … b in
      if (eqb address 128) then
        ?
      else if (eqb address 144) then
        let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in
        let status_2 ≝ set_p1_latch ?? s v in
          status_2
      else if (eqb address 160) then
        ?
      else if (eqb address 176) then
        let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in
        let status_2 ≝ set_p3_latch ?? s v in
          status_2
      else if (eqb address 153) then
        set_8051_sfr ?? s SFR_SBUF v
      else if (eqb address 138) then
        set_8051_sfr ?? s SFR_TL0 v
      else if (eqb address 139) then
        set_8051_sfr ?? s SFR_TL1 v
      else if (eqb address 140) then
        set_8051_sfr ?? s SFR_TH0 v
      else if (eqb address 141) then
        set_8051_sfr ?? s SFR_TH1 v
      else if (eqb address 200) then
        set_8052_sfr ?? s SFR_T2CON v
      else if (eqb address 202) then
        set_8052_sfr ?? s SFR_RCAP2L v
      else if (eqb address 203) then
        set_8052_sfr ?? s SFR_RCAP2H v
      else if (eqb address 204) then
        set_8052_sfr ?? s SFR_TL2 v
      else if (eqb address 205) then
        set_8052_sfr ?? s SFR_TH2 v
      else if (eqb address 135) then
        set_8051_sfr ?? s SFR_PCON v
      else if (eqb address 136) then
        set_8051_sfr ?? s SFR_TCON v
      else if (eqb address 137) then
        set_8051_sfr ?? s SFR_TMOD v
      else if (eqb address 152) then
        set_8051_sfr ?? s SFR_SCON v
      else if (eqb address 168) then
        set_8051_sfr ?? s SFR_IE v
      else if (eqb address 184) then
        set_8051_sfr ?? s SFR_IP v
      else if (eqb address 129) then
        set_8051_sfr ?? s SFR_SP v
      else if (eqb address 130) then
        set_8051_sfr ?? s SFR_DPL v
      else if (eqb address 131) then
        set_8051_sfr ?? s SFR_DPH v
      else if (eqb address 208) then
        set_8051_sfr ?? s SFR_PSW v
      else if (eqb address 224) then
        set_8051_sfr ?? s SFR_ACC_A v
      else if (eqb address 240) then
        set_8051_sfr ?? s SFR_ACC_B v
      else
        ?.
      cases not_implemented
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
    let 〈 un, ln 〉 ≝ split ? 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 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 ]])).
  [1,2,3,4,5:
    normalize
    repeat (@ le_S_S)
    @ le_O_n;
  ]
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 8).
      
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.
      
definition read_at_stack_pointer ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
    let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
    let m ≝ get_index_v ?? nu O ? in
    let r1 ≝ get_index_v ?? nu 1 ? in
    let r2 ≝ get_index_v ?? nu 2 ? in
    let r3 ≝ get_index_v ?? nu 3 ? in
    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    let memory ≝
      if m then
        (low_internal_ram ?? s)
      else
        (high_internal_ram ?? s)
    in
      lookup … address memory (zero 8).
  [1,2,3,4:
     normalize
     repeat (@ le_S_S)
     @ le_O_n
  ]
qed.

definition write_at_stack_pointer ≝
  λM: Type[0].
  λcode_memory:M.
  λs: PreStatus M code_memory.
  λv: Byte.
    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
    let bit_zero ≝ get_index_v ?? nu O ? in
    let bit_1 ≝ get_index_v ?? nu 1 ? in
    let bit_2 ≝ get_index_v ?? nu 2 ? in
    let bit_3 ≝ get_index_v ?? nu 3 ? in
      if bit_zero then
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (low_internal_ram ?? s) in
          set_low_internal_ram ?? s memory
      else
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (high_internal_ram ?? s) in
          set_high_internal_ram ?? s memory.
  [1,2,3,4:
     normalize
     repeat (@ le_S_S)
     @ le_O_n
  ]
qed.

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 〉 ≝ split … 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 ]] → Word ≝
  λm, cm, s, a.
    match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
      [ DATA16 d ⇒ λ_:True. d
      | _ ⇒ λK.
        match K in False with
        [
        ]
      ] (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
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | EXT_INDIRECT e ⇒
        λext_indirect: True.
          let address ≝ get_register ?? s [[ false; false; e ]]  in
          let padded_address ≝ pad 8 8 address in
            lookup ? 16 padded_address (external_ram ?? s) (zero 8)
      | 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 8 (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | ACC_PC ⇒
        λacc_pc: True.
          let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in
          let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in
            lookup ? 16 address (external_ram ?? s) (zero 8)
      | DIRECT d ⇒
        λdirect: True.
          let 〈 nu, nl 〉 ≝ split ? 4 4 d in
          let bit_one ≝ get_index_v ? ? nu 0 ? in
          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
            match bit_one with
              [ false ⇒
                  let address ≝ three_bits @@ nl in
                    lookup ? 7 address (low_internal_ram ?? s) (zero 8)
              | true ⇒ get_bit_addressable_sfr ?? s 8 d l
              ]
      | INDIRECT i ⇒
        λindirect: True.
          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
          match  bit_1 with
            [ false ⇒
                lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8)
            | true ⇒ 
                lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8)
            ]
      | _ ⇒ λother.
        match other in False with [ ]
      ] (subaddressing_modein … a).
  [1,2:
     normalize
     repeat (@ le_S_S)
     @ le_O_n
  ]
qed.

axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v).

definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ;
                                   acc_a ; acc_b ; ext_indirect ;
                                   ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory.
                                   clock … code_memory s = clock … code_memory s' ≝
  λ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) →
                   Σs':PreStatus m cm. clock m cm s = clock m cm s'
                   (*CSC: bug here if one specified the two clock above*)
            with
      [ DIRECT d ⇒
        λdirect: True.
          let 〈 nu, nl 〉 ≝ split … 4 4 d in
          let bit_one ≝ get_index_v ? ? nu 0 ? in
          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
            match bit_one with
              [ true ⇒ set_bit_addressable_sfr ?? s d v
              | false ⇒
                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory
              ]
      | INDIRECT i ⇒
        λindirect: True.
          let register ≝ get_register ?? s [[ false; false; i ]] in
          let 〈nu, nl〉 ≝ split ? 4 4 register in
          let bit_1 ≝ get_index_v … nu 0 ? in
          let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
            match bit_1 with
              [ false ⇒
                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in
                  set_low_internal_ram ?? s memory
              | true ⇒ 
                let memory ≝ insert … (three_bits @@ nl) 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 ? 16 padded_address v (external_ram ?? s) in
            set_external_ram ?? s memory
      | 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 ? 16 address v (external_ram ?? s) in
            set_external_ram ?? s memory
      | _ ⇒ 
        λother: False.
          match other in False with [ ]
      ] (subaddressing_modein … a).
// qed.

definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝
 set_arg_8'.

lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v).
 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2
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 〈 nu, nl 〉 ≝ split … 4 4 b in
          let bit_1 ≝ get_index_v ? ? nu 0 ? in
          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
            match bit_1 with
              [ true ⇒
                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
                let d ≝ address ÷ 8 in
                let m ≝ address mod 8 in
                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
                  get_index_v … sfr m ?
              | false ⇒
                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
                let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
                  get_index_v … t (modulus address 8) ? 
              ]
      | N_BIT_ADDR n ⇒
        λn_bit_addr: True.
          let 〈 nu, nl 〉 ≝ split … 4 4 n in
          let bit_1 ≝ get_index_v ? ? nu 0 ? in
          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
            match bit_1 with
              [ true ⇒
                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
                let d ≝ address ÷ 8 in
                let m ≝ address mod 8 in
                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
                let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in
                  ¬(get_index_v … sfr m ?)
              | false ⇒
                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
                let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
                  ¬(get_index_v … trans (modulus address 8) ?)
              ]
      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
      | _ ⇒ λother.
        match other in False with [ ]
      ] (subaddressing_modein … a).
      [3,6:
         normalize
         repeat (@ le_S_S)
         @ le_O_n
      |1,2,4,5:
         @modulus_less_than
      ]
qed.
      
definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝
  λ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) → Σs'. clock m cm s = clock m cm s' with
      [ BIT_ADDR b ⇒ λbit_addr: True.
        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
        let bit_1 ≝ get_index_v ?? nu 0 ? in
        let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
        match bit_1 return λ_. ? with
          [ true ⇒
            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
            let d ≝ address ÷ 8 in
            let m ≝ address mod 8 in
            let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
            let sfr ≝ get_bit_addressable_sfr ?? s ? t true in
            let new_sfr ≝ set_index … sfr m v ? in
              set_bit_addressable_sfr ?? s new_sfr t
          | false ⇒
            let address ≝ nat_of_bitvector … (three_bits @@ nl) in
            let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
            let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
            let n_bit ≝ set_index … t (modulus address 8) v ? in
            let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
              set_low_internal_ram ?? s memory
          ]
      | CARRY ⇒
        λcarry: True.
        let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
        let bit_1 ≝ get_index_v… nu 1 ? in
        let bit_2 ≝ get_index_v… nu 2 ? in
        let bit_3 ≝ get_index_v… nu 3 ? in
        let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
          set_8051_sfr ?? s SFR_PSW new_psw
      | _ ⇒
        λother: False.
          match other in False with
            [ ]
      ] (subaddressing_modein … a).
try (repeat @le_S_S @le_O_n)
/by/
qed.

definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'.

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

definition load_code_memory ≝
 fold_left_i … (
   λi, mem, v.
     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).

definition load ≝
 λl,cm.
 λstatus.
   set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).

definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝
  λcode_mem.
  λpc: Word.
    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
      〈instr, new_pc〉.
    cases not_implemented.
qed.

lemma snd_fetch_pseudo_instruction:
 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
 #lft #rgt @pair_elim #x #y #_ #_ %
qed.

definition instruction_matches_identifier ≝
  λy: Identifier.
  λx: labelled_instruction.
    match \fst x with
    [ None ⇒ false
    | Some x ⇒ eq_identifier ? x y
    ].

let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
 match l with
  [ nil ⇒ true
  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].

lemma does_not_occur_None:
 ∀id,i,list_instr.
  does_not_occur id (list_instr@[〈None …,i〉]) =
  does_not_occur id list_instr.
 #id #i #list_instr elim list_instr
  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH %]
qed.

lemma does_not_occur_Some:
 ∀id,id',i,list_instr.
  eq_identifier ? id' id = false →
   does_not_occur id (list_instr@[〈Some ? id',i〉]) =
    does_not_occur id list_instr.
 #id #id' #i #list_instr elim list_instr
  [ #H normalize in H ⊢ %; >H %
  | * #x #i' #tl #IH #H whd in ⊢ (??%%); >(IH H) %]
qed.

lemma does_not_occur_absurd:
 ∀id,i,list_instr.
  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
 #id #i #list_instr elim list_instr
  [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?)
    >eq_identifier_refl %
  | * #x #i' #tl #IH whd in ⊢ (??%%); >IH cases (notb ?) %]
qed.


let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
 match l with
  [ nil ⇒ false
  | cons hd tl ⇒
     if instruction_matches_identifier id hd then
      does_not_occur id tl
     else
      occurs_exactly_once id tl ].

lemma occurs_exactly_once_None:
 ∀id,i,list_instr.
  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
  occurs_exactly_once id list_instr.
 #id #i #list_instr elim list_instr
  [ % | #hd #tl #IH whd in ⊢ (??%%); >IH >does_not_occur_None %]
qed.

lemma occurs_exactly_once_Some:
 ∀id,id',i,prefix.
  occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix.
 #id #id' #i #prefix elim prefix
  [ whd in ⊢ (?% → ?);
    change with (eq_identifier ? id' id) in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    @eq_identifier_elim normalize nodelta; /2/
  | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
    cases he; normalize nodelta
     [ #H @ (IH H)
     | #x whd in ⊢ (? → ?(??%)); change with (eq_identifier ? x id) in match (instruction_matches_identifier ??);
       @eq_identifier_elim #E normalize nodelta
       [ destruct @eq_identifier_elim normalize nodelta;
        /2/ #H >does_not_occur_Some /2/
       | #H @IH @H]]]
qed.

lemma occurs_exactly_once_Some_stronger:
  ∀id,id',i,prefix.
    occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 
    (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨
    (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix).
 #id #id' #i #prefix elim prefix
 [ whd in ⊢ (?% → ?); change with (eq_identifier ???) in ⊢ (?(match % with [_ ⇒ ?| _ ⇒ ?]) → ?);
   @eq_identifier_elim #E
  [ normalize //
  | normalize #H @⊥ @H  
  ]
 | *; #he #i' #tl #IH whd in ⊢ (?% → ?); whd in ⊢ (?(match % with [_ ⇒ ? | _ ⇒ ?]) → ?);
   cases he; normalize nodelta
   [ #H @ (IH H)
   | #x @eq_identifier_elim #Heq
     [ @eq_identifier_elim normalize nodelta
       [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf
       | #H >(does_not_occur_Some)
         [ #H2 whd in match (does_not_occur ??);
           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
           >Heq >eq_identifier_refl normalize nodelta
           @orb_elim normalize nodelta whd in match (occurs_exactly_once ??);
           change with (eq_identifier ???) in match (instruction_matches_identifier ??);
           >eq_identifier_refl
           normalize nodelta @H2  
         | /2/
         ]
       ]
     | normalize nodelta #H lapply (IH H) -IH -H;
       @eq_identifier_elim #Heq2
       #Hor @orb_elim
       [ <Heq2 in Hor; #Hor normalize in Hor;
         whd in match (does_not_occur ??); change with (eq_identifier ???) in match (instruction_matches_identifier ??);
         >eq_identifier_false // normalize nodelta
         cases (does_not_occur id' tl) in Hor; normalize nodelta //
       | normalize nodelta whd in match (occurs_exactly_once ??);
         change with (eq_identifier ???) in match (instruction_matches_identifier ??);
         >eq_identifier_false //
       ] 
     ]  
   ]
 ]
qed.   

let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
  match l with
  [ nil ⇒ ?
  | cons hd tl ⇒
    if pred hd then
      acc
    else
      index_of_internal A pred tl (S acc)
  ].
  cases not_implemented.
qed.


definition index_of ≝
  λA.
  λeq.
  λl.
    index_of_internal A eq l 0.

lemma index_of_internal_None: ∀i,id,instr_list,n.
 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
  index_of_internal ? (instruction_matches_identifier id) instr_list n =
   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
 #i #id #instr_list elim instr_list
  [ #n #abs whd in abs; cases abs
  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?);
    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%);
    [ #H %
    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %;
      [ #_ % | #abs cases abs ]]]
qed.

lemma index_of_internal_Some_miss: ∀i,id,id'.
 eq_identifier ? id' id = false →
 ∀instr_list,n.
 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
  index_of_internal ? (instruction_matches_identifier id) instr_list n =
   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
 change with (occurs_exactly_once ?? → ?) generalize in match n; -n -H; elim instr_list
  [ #n #abs cases abs
  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    [ // | #K @IH //]]
qed.

lemma index_of_internal_Some_hit: ∀i,id.
 ∀instr_list,n.
  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
  = |instr_list| + n.
 #i #id #instr_list elim instr_list
  [ #n #_ whd in ⊢ (??%%); change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl %
  | #hd #tl #IH #n whd in ⊢ (?% → ??%%); cases (instruction_matches_identifier id hd) normalize nodelta;
    [ >does_not_occur_absurd #abs cases abs | #H >plus_n_Sm applyS (IH (S n)) //]]
qed.

definition address_of_word_labels_code_mem ≝
  λcode_mem.
  λid: Identifier.
    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).

lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
  address_of_word_labels_code_mem instr_list id =
  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
 >(index_of_internal_None … H) %
qed.

lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
 eq_identifier ? id' id = false →
  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
   address_of_word_labels_code_mem instr_list id =
   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));
 >(index_of_internal_Some_miss … H) [ @refl | // ]
qed.

lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
   = bitvector_of_nat … (|instr_list|).
 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);
 >(index_of_internal_Some_hit … H) <plus_n_O @refl
qed.

definition address_of_word_labels ≝
  λpr: pseudo_assembly_program.
  λid: Identifier.
    address_of_word_labels_code_mem (\snd pr) id.

definition construct_datalabels: preamble → ? ≝
  λthe_preamble: preamble.
    \fst (foldl ((identifier_map ASMTag Word) × Word) ? (
    λt. λpreamble.
      let 〈datalabels, addr〉 ≝ t in
      let 〈name, size〉 ≝ preamble in
      let 〈carry, sum〉 ≝ half_add … addr size in
        〈add ? ? datalabels name addr, sum〉)
          〈empty_map …, zero 16〉 (\snd the_preamble)).