include "basics/lists/listb.ma".
include "ASM/StatusProofs.ma".
include "ASM/Fetch.ma".
include "ASM/AbstractStatus.ma". 
    
lemma execute_1_technical:
  ∀n, m: nat.
  ∀v: Vector addressing_mode_tag (S n).
  ∀q: Vector addressing_mode_tag (S m).
  ∀a: addressing_mode.
    bool_to_Prop (is_in ? v a) →
    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    bool_to_Prop (is_in ? q a).
 # n
 # m
 # v
 # q
 # a
 elim v
 [ normalize
   # K
   cases K
 | # n'
   # he
   # tl
   # II
   whd in ⊢ (% → ? → ?);
   lapply (refl … (is_in … (he:::tl) a))
   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
   [ # K
     # _
     normalize in K;
     whd in ⊢ (% → ?);
     lapply (refl … (subvector_with … eq_a (he:::tl) q));
     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
     [ # K1
       # _
       change with ((andb ? (subvector_with …)) = true) in K1;
       cases (conjunction_true … K1)
       # K3
       # K4
       cases (inclusive_disjunction_true … K)
       # K2
       [ > (is_a_to_mem_to_is_in … K2 K3)
         %
       | @ II
         [ > K2
           %
         | > K4
           %
         ]
       ] 
     | # K1
       # K2
       normalize in K2;
       cases K2;
     ]
   | # K1
     # K2
     normalize in K2;
     cases K2
   ]
 ]
qed.

include alias "arithmetics/nat.ma".
include alias "ASM/BitVectorTrie.ma".

definition execute_1_preinstruction:
  ∀ticks: nat × nat.
  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
  ∀s: PreStatus m cm. PreStatus m cm ≝
  λticks: nat × nat.
  λa, m: Type[0]. λcm.
  λaddr_of: a → PreStatus m cm → Word.
  λinstr: preinstruction a.
  λs: PreStatus m cm.
  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
  match instr in preinstruction return λx. x = instr → PreStatus m cm with
        [ ADD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) false in
            let cy_flag ≝ get_index' ? O  ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ADDC addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | SUBB addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ANL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
               set_flags … s and_val (None ?) (get_ov_flag ?? s)
            ]
        | ORL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
               set_flags … s or_val (None ?) (get_ov_flag … s)
            ]
        | XRL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l' ⇒
              let 〈addr1, addr2〉 ≝ l' in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            ]
        | INC addr ⇒ λinstr_refl.
            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with
              [ ACC_A ⇒ λacc_a: True.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' ACC_A result
              | REGISTER r ⇒ λregister: True.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (REGISTER r) result
              | DIRECT d ⇒ λdirect: True.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (DIRECT d) result
              | INDIRECT i ⇒ λindirect: True.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (INDIRECT i) result
              | DPTR ⇒ λdptr: True.
                let s' ≝ add_ticks1 s in
                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
                let s ≝ set_8051_sfr … s' SFR_DPL bl in
                 set_8051_sfr … s' SFR_DPH bu
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr)
        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
          let s ≝ add_ticks1 s in
          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
          let jmp_addr ≝ add … big_acc dptr in
          let new_pc ≝ add … (program_counter … s) jmp_addr in
            set_program_counter … s new_pc
        | NOP ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
            s
        | DEC addr ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
             set_arg_8 … s addr result
        | MUL addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
           let product ≝ acc_a_nat * acc_b_nat in
           let ov_flag ≝ product ≥ 256 in
           let low ≝ bitvector_of_nat 8 (product mod 256) in
           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
           let s ≝ set_8051_sfr … s SFR_ACC_A low in
             set_8051_sfr … s SFR_ACC_B high
        | DIV addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
             match acc_b_nat with
               [ O ⇒ set_flags … s false (None Bit) true
               | S o ⇒
                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
                   set_flags … s false (None Bit) false
               ]
        | DA addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
                let cy_flag ≝ get_index' ? O ? flags in
                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
                    let new_acc ≝ nu @@ acc_nl' in
                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
                  else
                    s
              else
                s
        | CLR addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
            [ ACC_A ⇒ λacc_a: True.
              let s ≝ add_ticks1 s in
               set_arg_8 … s ACC_A (zero 8)
            | CARRY ⇒ λcarry: True.
              let s ≝ add_ticks1 s in
               set_arg_1 … s CARRY false
            | BIT_ADDR b ⇒ λbit_addr: True.
              let s ≝ add_ticks1 s in
               set_arg_1 … s (BIT_ADDR b) false
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        | CPL addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
            [ ACC_A ⇒ λacc_a: True.
                let s ≝ add_ticks1 s in
                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
                let new_acc ≝ negation_bv ? old_acc in
                 set_8051_sfr … s SFR_ACC_A new_acc
            | CARRY ⇒ λcarry: True.
                let s ≝ add_ticks1 s in
                let old_cy_flag ≝ get_arg_1 … s CARRY true in
                let new_cy_flag ≝ ¬old_cy_flag in
                 set_arg_1 … s CARRY new_cy_flag
            | BIT_ADDR b ⇒ λbit_addr: True.
                let s ≝ add_ticks1 s in
                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
                let new_bit ≝ ¬old_bit in
                 set_arg_1 … s (BIT_ADDR b) new_bit
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr)
        | SETB b ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            set_arg_1 … s b false
        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_left … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_right … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? O ? old_acc in
            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
            let new_acc ≝ nl @@ nu in
              set_8051_sfr … s SFR_ACC_A new_acc
        | PUSH addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
             write_at_stack_pointer … s (get_arg_8 … s false addr)
        | POP addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let contents ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
              set_arg_8 … s addr contents
        | XCH addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_addr ≝ get_arg_8 … s false addr2 in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
              set_arg_8 … s addr2 old_acc
        | XCHD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
            let new_acc ≝ acc_nu @@ arg_nl in
            let new_arg ≝ arg_nu @@ acc_nl in
            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
              set_arg_8 … s addr2 new_arg
        | RET ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | RETI ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | MOVX addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          (* DPM: only copies --- doesn't affect I/O *)
          match addr with
            [ inl l ⇒
              let 〈addr1, addr2〉 ≝ l in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            ]
        | MOV addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  match l' with
                    [ inl l'' ⇒
                      match l'' with
                        [ inl l''' ⇒
                          match l''' with
                            [ inl l'''' ⇒
                              let 〈addr1, addr2〉 ≝ l'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            | inr r'''' ⇒
                              let 〈addr1, addr2〉 ≝ r'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            ]
                        | inr r''' ⇒
                          let 〈addr1, addr2〉 ≝ r''' in
                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                        ]
                    | inr r'' ⇒
                      let 〈addr1, addr2〉 ≝ r'' in
                       set_arg_16 … s (get_arg_16 … s addr2) addr1
                    ]
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
                ]
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
            ]
          | JC addr ⇒ λinstr_refl.
                  if get_cy_flag ?? s then
                    let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                  else
                    let s ≝ add_ticks2 s in
                      s
            | JNC addr ⇒ λinstr_refl.
                  if ¬(get_cy_flag ?? s) then
                   let s ≝ add_ticks1 s in
                     set_program_counter … s (addr_of addr s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JB addr1 addr2 ⇒ λinstr_refl.
                  if get_arg_1 … s addr1 false then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JNB addr1 addr2 ⇒ λinstr_refl.
                  if ¬(get_arg_1 … s addr1 false) then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JBC addr1 addr2 ⇒ λinstr_refl.
                  let s ≝ set_arg_1 … s addr1 false in
                    if get_arg_1 … s addr1 false then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr2 s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JZ addr ⇒ λinstr_refl.
                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JNZ addr ⇒ λinstr_refl.
                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | CJNE addr1 addr2 ⇒ λinstr_refl.
                  match addr1 with
                    [ inl l ⇒
                        let 〈addr1, addr2'〉 ≝ l in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    | inr r' ⇒
                        let 〈addr1, addr2'〉 ≝ r' in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    ]
            | DJNZ addr1 addr2 ⇒ λinstr_refl.
              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
              let s ≝ set_arg_8 … s addr1 result in
                if ¬(eq_bv ? result (zero 8)) then
                 let s ≝ add_ticks1 s in
                  set_program_counter … s (addr_of addr2 s)
                else
                 let s ≝ add_ticks2 s in
                  s
            ] (refl … instr).
    try (cases(other))
    try assumption (*20s*)
    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    try (
      @(execute_1_technical … (subaddressing_modein …))
      @I
    ) (*66s*)
qed.

definition execute_1_preinstruction_ok':
  ∀ticks: nat × nat.
  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
  ∀s: PreStatus m cm.
    Σs': PreStatus m cm.
      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
  λticks: nat × nat.
  λa, m: Type[0]. λcm.
  λaddr_of: a → PreStatus m cm → Word.
  λinstr: preinstruction a.
  λs: PreStatus m cm.
  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
        [ ADD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) false in
            let cy_flag ≝ get_index' ? O  ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ADDC addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | SUBB addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ANL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
               set_flags … s and_val (None ?) (get_ov_flag ?? s)
            ]
        | ORL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
               set_flags … s or_val (None ?) (get_ov_flag … s)
            ]
        | XRL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l' ⇒
              let 〈addr1, addr2〉 ≝ l' in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            ]
        | INC addr ⇒ λinstr_refl.
            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
              [ ACC_A ⇒ λacc_a: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' ACC_A result
              | REGISTER r ⇒ λregister: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (REGISTER r) result
              | DIRECT d ⇒ λdirect: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (DIRECT d) result
              | INDIRECT i ⇒ λindirect: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (INDIRECT i) result
              | DPTR ⇒ λdptr: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
                let s ≝ set_8051_sfr … s' SFR_DPL bl in
                 set_8051_sfr … s' SFR_DPH bu
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
        | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
          let s ≝ add_ticks1 s in
          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
          let jmp_addr ≝ add … big_acc dptr in
          let new_pc ≝ add … (program_counter … s) jmp_addr in
            set_program_counter … s new_pc
        | NOP ⇒ λinstr_refl.
           let s ≝ add_ticks2 s in
            s
        | DEC addr ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
             set_arg_8 … s addr result
        | MUL addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
           let product ≝ acc_a_nat * acc_b_nat in
           let ov_flag ≝ product ≥ 256 in
           let low ≝ bitvector_of_nat 8 (product mod 256) in
           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
           let s ≝ set_8051_sfr … s SFR_ACC_A low in
             set_8051_sfr … s SFR_ACC_B high
        | DIV addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
             match acc_b_nat with
               [ O ⇒ set_flags … s false (None Bit) true
               | S o ⇒
                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
                   set_flags … s false (None Bit) false
               ]
        | DA addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
                let cy_flag ≝ get_index' ? O ? flags in
                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
                    let new_acc ≝ nu @@ acc_nl' in
                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
                  else
                    s
              else
                s
        | CLR addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
            [ ACC_A ⇒ λacc_a: True. λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_8 … s ACC_A (zero 8)
            | CARRY ⇒ λcarry: True. λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_1 … s CARRY false
            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_1 … s (BIT_ADDR b) false
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | CPL addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
            [ ACC_A ⇒ λacc_a: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
                let new_acc ≝ negation_bv ? old_acc in
                 set_8051_sfr … s SFR_ACC_A new_acc
            | CARRY ⇒ λcarry: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let old_cy_flag ≝ get_arg_1 … s CARRY true in
                let new_cy_flag ≝ ¬old_cy_flag in
                 set_arg_1 … s CARRY new_cy_flag
            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
                let new_bit ≝ ¬old_bit in
                 set_arg_1 … s (BIT_ADDR b) new_bit
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 
        | SETB b ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            set_arg_1 … s b false
        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_left … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_right … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? O ? old_acc in
            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
            let new_acc ≝ nl @@ nu in
              set_8051_sfr … s SFR_ACC_A new_acc
        | PUSH addr ⇒ λinstr_refl.
            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
              [ DIRECT d ⇒ λdirect: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
                let s ≝ set_8051_sfr … s SFR_SP new_sp in
                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | POP addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let contents ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
              set_arg_8 … s addr contents
        | XCH addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_addr ≝ get_arg_8 … s false addr2 in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
              set_arg_8 … s addr2 old_acc
        | XCHD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
            let new_acc ≝ acc_nu @@ arg_nl in
            let new_arg ≝ arg_nu @@ acc_nl in
            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
              set_arg_8 … s addr2 new_arg
        | RET ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | RETI ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | MOVX addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          (* DPM: only copies --- doesn't affect I/O *)
          match addr with
            [ inl l ⇒
              let 〈addr1, addr2〉 ≝ l in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            ]
        | MOV addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  match l' with
                    [ inl l'' ⇒
                      match l'' with
                        [ inl l''' ⇒
                          match l''' with
                            [ inl l'''' ⇒
                              let 〈addr1, addr2〉 ≝ l'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            | inr r'''' ⇒
                              let 〈addr1, addr2〉 ≝ r'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            ]
                        | inr r''' ⇒
                          let 〈addr1, addr2〉 ≝ r''' in
                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                        ]
                    | inr r'' ⇒
                      let 〈addr1, addr2〉 ≝ r'' in
                       set_arg_16 … s (get_arg_16 … s addr2) addr1
                    ]
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
                ]
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
            ]
          | JC addr ⇒ λinstr_refl.
                  if get_cy_flag ?? s then
                    let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                  else
                    let s ≝ add_ticks2 s in
                      s
            | JNC addr ⇒ λinstr_refl.
                  if ¬(get_cy_flag ?? s) then
                   let s ≝ add_ticks1 s in
                     set_program_counter … s (addr_of addr s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JB addr1 addr2 ⇒ λinstr_refl.
                  if get_arg_1 … s addr1 false then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JNB addr1 addr2 ⇒ λinstr_refl.
                  if ¬(get_arg_1 … s addr1 false) then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JBC addr1 addr2 ⇒ λinstr_refl.
                  let s ≝ set_arg_1 … s addr1 false in
                    if get_arg_1 … s addr1 false then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr2 s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JZ addr ⇒ λinstr_refl.
                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JNZ addr ⇒ λinstr_refl.
                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | CJNE addr1 addr2 ⇒ λinstr_refl.
                  match addr1 with
                    [ inl l ⇒
                        let 〈addr1, addr2'〉 ≝ l in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    | inr r' ⇒
                        let 〈addr1, addr2'〉 ≝ r' in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    ]
            | DJNZ addr1 addr2 ⇒ λinstr_refl.
              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
              let s ≝ set_arg_8 … s addr1 result in
                if ¬(eq_bv ? result (zero 8)) then
                 let s ≝ add_ticks1 s in
                  set_program_counter … s (addr_of addr2 s)
                else
                 let s ≝ add_ticks2 s in
                  s
            ] (refl … instr).
    try (cases(other))
    try assumption (*20s*)
    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    try (
      @(execute_1_technical … (subaddressing_modein …))
      @I
    ) (*66s*)
    whd in match execute_1_preinstruction;
    normalize nodelta %
    [21,22,23,24: (* DIV *)
     normalize nodelta in p;
    |7,8,9,10,11,12,13,14,15,16, (* INC *)
     71,72,73,74,75,76, (* CLR *)
     77,78,79,80,81,82: (* CPL *)
      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
    |99,100: (* PUSH *)
      whd in match add; normalize nodelta [>clock_write_at_stack_pointer]
    |93,94: (* MOV *)
      cases addr * normalize nodelta
       [1,2,4,5: * normalize nodelta
        [1,2,4,5: * normalize nodelta
         [1,2,4,5: * normalize nodelta
          [1,2,4,5: * normalize nodelta ]]]]
       #arg1 #arg2
    |65,66, (* ANL *)
     67,68, (* ORL *)
     95,96: (* MOVX*)
      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
    |59,60: (* CJNE *)
      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
      cases (¬(eq_bv ???)) normalize nodelta
    |69,70: (* XRL *)
      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
    ]
    try (>p normalize nodelta 
         try (>p1 normalize nodelta
              try (>p2 normalize nodelta
                   try (>p3 normalize nodelta
                        try (>p4 normalize nodelta
                             try (>p5 normalize nodelta))))))
    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
    try (change with (cl_call = cl_other → ?) #absurd destruct(absurd))
    try (@or_introl //)
    try (@or_intror //)
    try #_
    try /demod nohyps by clock_set_clock,clock_set_8051_sfr,clock_set_arg_8,set_arg_1_ok,
                         program_counter_set_8051_sfr,program_counter_set_arg_1/
    try (% @I) try (@or_introl % @I) try (@or_intror % @I) //
qed.

lemma execute_1_preinstruction_ok:
 ∀ticks,a,m,cm,f,i,s.
  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
qed.

definition compute_target_of_unconditional_jump:
    ∀program_counter: Word.
    ∀i: instruction.
      Word ≝
  λprogram_counter.
  λi.
    match i with
    [ LJMP addr ⇒
        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
        [ ADDR16 a ⇒ λaddr16: True. a
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … addr)
    | SJMP addr ⇒
        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
        [ RELATIVE r ⇒ λrelative: True.
            add … program_counter (sign_extension r)
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … addr)
    | AJMP addr ⇒
        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
        [ ADDR11 a ⇒ λaddr11: True.
          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 5 11 program_counter in
          let new_addr ≝ pc_bu @@ a in
            new_addr
        | _ ⇒ λother: False. ⊥
        ] (subaddressing_modein … addr)
    | _ ⇒ zero ?
    ].
  //
qed.

definition is_unconditional_jump:
    instruction → bool ≝
  λi: instruction.
    match i with
    [ LJMP _ ⇒ true
    | SJMP _ ⇒ true
    | AJMP _ ⇒ true
    | _ ⇒ false
    ].

definition program_counter_after_other ≝
  λprogram_counter. (* XXX: program counter after fetching *)
  λinstruction.
    if is_unconditional_jump instruction then
      compute_target_of_unconditional_jump program_counter instruction
    else
      program_counter.

definition addr_of_relative ≝
 λM,cm. λx:[[relative]]. λs: PreStatus M cm.
  match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
   [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
   | _ ⇒ λabsd. ⊥
   ] (subaddressing_modein … x).
 @absd
qed.

include alias "arithmetics/nat.ma".
include alias "ASM/BitVectorTrie.ma".
include alias "ASM/Vector.ma".

definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
  Σs': Status cm.
    And (clock ?? s' = \snd current + clock … s)
      (ASM_classify0 (\fst (\fst current)) = cl_other →
        program_counter ? ? s' =
          program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
  λcm,s0,instr_pc_ticks.
    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    let s ≝ set_program_counter … s0 pc in
      match instr return λx. x = instr → Σs:?.? with
      [ MOVC addr1 addr2 ⇒ λinstr_refl.
          let s ≝ set_clock ?? s (ticks + clock … s) in
          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
            [ ACC_DPTR ⇒ λacc_dptr: True.
              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
              let new_addr ≝ add … dptr big_acc in
              let result ≝ lookup ? ? new_addr cm (zero ?) in
                set_8051_sfr … s SFR_ACC_A result
            | ACC_PC ⇒ λacc_pc: True.
              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
              (* DPM: Under specified: does the carry from PC incrementation affect the *)
              (*      addition of the PC with the DPTR? At the moment, no.              *)
              let new_addr ≝ add … (program_counter … s) big_acc in
              let result ≝ lookup ? ? new_addr cm (zero ?) in
                set_8051_sfr … s SFR_ACC_A result
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr2)
      | LJMP addr ⇒ λinstr_refl.
          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
          let s ≝ set_clock ?? s (ticks + clock … s) in
            set_program_counter … s new_pc
      | SJMP addr ⇒ λinstr_refl.
          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
          let s ≝ set_clock ?? s (ticks + clock … s) in
            set_program_counter … s new_pc
      | AJMP addr ⇒ λinstr_refl.
          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
          let s ≝ set_clock ?? s (ticks + clock … s) in
            set_program_counter … s new_pc
      | ACALL addr ⇒ λinstr_refl.
          let s ≝ set_clock ?? s (ticks + clock … s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
            [ ADDR11 a ⇒ λaddr11: True.
              «let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
              let s ≝ set_8051_sfr … s SFR_SP new_sp in
              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
              let s ≝ write_at_stack_pointer … s pc_bl in
              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
              let s ≝ set_8051_sfr … s SFR_SP new_sp in
              let s ≝ write_at_stack_pointer … s pc_bu in
              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
              let new_addr ≝ fiv @@ a in
                set_program_counter … s new_addr, ?»
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
      | LCALL addr ⇒ λinstr_refl.
          let s ≝ set_clock ?? s (ticks + clock … s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
            [ ADDR16 a ⇒ λaddr16: True.
              «
              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
              let s ≝ set_8051_sfr … s SFR_SP new_sp in
              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
              let s ≝ write_at_stack_pointer … s pc_bl in
              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
              let s ≝ set_8051_sfr … s SFR_SP new_sp in
              let s ≝ write_at_stack_pointer … s pc_bu in
                set_program_counter … s a, ?»
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        ] (refl … instr). (*10s*)
  try assumption
  [1,2,3,4,5,6,7:
    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
    try //
    -s destruct(INSTR_PC) <instr_refl whd
    try (#absurd normalize in absurd; try destruct(absurd) try %)
    @pair_elim #carry #new_sp #carry_new_sp_refl
    [2:
      /demod nohyps/ %
    |1:
      cases (vsplit ????) #fiv #thr' normalize nodelta
      /demod by clock_set_program_counter/ /demod nohyps/ %
    ]
  |8:
    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
        (λx. λs.
        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
        | _ ⇒ λabsd. ⊥
        ] (subaddressing_modein … x)) instr' s) try @absd
    #clock_proof #classify_proof %
    [1:
      cases clock_proof #clock_proof' >clock_proof'
      destruct(INSTR_PC_TICKS) %
    |2:
      -clock_proof <INSTR_PC_TICKS normalize nodelta
      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
      [1:
        destruct(INSTR_PC) /2/
      |2:
        * #hyp1 #hyp2 >hyp1 normalize nodelta
      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
      try assumption >hyp2 %
    ]
  ]
qed.

definition current_instruction_cost ≝
  λcm.λs: Status cm.
    \snd (fetch cm (program_counter … s)).

definition execute_1': ∀cm.∀s:Status cm.
  Σs':Status cm.
    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
      And (clock ?? s' = current_instruction_cost cm s + clock … s)
        (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
          program_counter ? ? s' =
            program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
  λcm. λs: Status cm.
  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
  %
  [1:
    cases(execute_1_0 cm s instr_pc_ticks)
    #the_status * #clock_assm #_ @clock_assm
  |2:
    cases(execute_1_0 cm s instr_pc_ticks)
    #the_status * #_ #classify_assm
    assumption
  ]
qed.

definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.

lemma execute_1_ok: ∀cm.∀s.
  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
        program_counter ? cm (execute_1 cm s) =
          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
  #cm #s normalize nodelta
  whd in match execute_1; normalize nodelta @pi2
qed.

lemma execute_1_ok_clock:
  ∀cm.
  ∀s.
    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
qed-.

definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
  λticks,cm,s,instr,pc.
  let s ≝ set_program_counter ?? s pc in
  let s ≝
    match instr with
    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
    | Cost cst ⇒ s
    | Jmp jmp ⇒
       let s ≝ set_clock … s (\fst ticks + clock … s) in
        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
    | Jnz acc dst1 dst2 ⇒
       if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
        let s ≝ set_clock ?? s (\fst ticks + clock … s) in
         set_program_counter … s (address_of_word_labels (\snd cm) dst1)
       else
        let s ≝ set_clock ?? s (\snd ticks + clock … s) in
         set_program_counter … s (address_of_word_labels (\snd cm) dst2)
    | MovSuccessor dst ws lbl ⇒
      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
      let addr ≝ address_of_word_labels (\snd cm) lbl in
      let 〈high, low〉 ≝ vsplit ? 8 8 addr in
      let v ≝ match ws with [ HIGH ⇒ high | LOW ⇒ low ] in
       set_arg_8 … s dst v      
    | Call call ⇒
      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
      let a ≝ address_of_word_labels (\snd cm) call in
      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr … s SFR_SP new_sp in
      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
      let s ≝ write_at_stack_pointer … s pc_bl in
      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr … s SFR_SP new_sp in
      let s ≝ write_at_stack_pointer … s pc_bu in
        set_program_counter … s a
    | Mov dptr ident ⇒
      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
      let the_preamble ≝ \fst cm in
      let data_labels ≝ construct_datalabels the_preamble in
        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
    ]
  in
    s.
  [2: % | @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
qed.

definition execute_1_pseudo_instruction:
 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
    PseudoStatus cm
≝
  λcm,ticks_of,s,pc_ok.
  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
  let ticks ≝ ticks_of (program_counter … s) pc_ok in
   execute_1_pseudo_instruction0 ticks cm s instr pc.

let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
  match n with
    [ O ⇒ s
    | S o ⇒ execute o … (execute_1 … s)
    ].

(* CSC: No way to have a total function because of function pointers call!
   The new pc after the execution can fall outside the program length.
   Luckily, this function is never actually used because we are only
   interested in structured traces.
let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
  match n with
    [ O ⇒ s
    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
    ].
*)