include "ASM/Status.ma".
include "ASM/Fetch.ma".
include "ASM/JMCoercions.ma".

definition sign_extension: Byte → Word ≝
  λc.
    let b ≝ get_index_v ? 8 c 1 ? in
      [[ b; b; b; b; b; b; b; b ]] @@ c.
  normalize;
  repeat (@ (le_S_S ?));
  @ (le_O_n);
qed.
    
lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
 # a
 # b
 cases a
 cases b
 normalize
 //
 # K
 cases (eq_true_false K)
qed.

lemma is_a_to_mem_to_is_in:
 ∀he,a,m,q. is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
 # he
 # a
 # m
 # q
 elim q
 [ normalize
   # _
   # K
   assumption
 | # m'
   # t
   # q'
   # II
   # H1
   # H2
   normalize
   change with (orb ??) in H2: (??%?);
   cases (inclusive_disjunction_true … H2)
   [ # K
     < (eq_a_to_eq … K)
     > H1
     %
   | # K
     > II
     try assumption
     cases (is_a t a)
     normalize
     %
   ]
 ]
qed.

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


lemma set_flags_ignores_clock:
 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).
//
qed.

lemma set_arg_8_ignores_clock:
 ∀M,s,f1,f2. clock M s = clock … (set_arg_8 … s f1 f2).
#M #s #f1 #f2 cases (set_arg_8 M s f1 f2)
#a #E >E //
qed.

lemma set_program_counter_ignores_clock:
  ∀M: Type[0].
  ∀s: PreStatus M.
  ∀pc: Word.
    clock M (set_program_counter … s pc) = clock … s.
  #M #s #pc %
qed.

lemma set_low_internal_ram_ignores_clock:
  ∀M: Type[0].
  ∀s: PreStatus M.
  ∀ram: BitVectorTrie Byte 7.
    clock … (set_low_internal_ram … s ram) = clock … s.
  #M #s #ram %
qed.

lemma set_8051_sfr_ignores_clock:
  ∀M: Type[0].
  ∀s: PreStatus M.
  ∀sfr: SFR8051.
  ∀v: Byte.
    clock … (set_8051_sfr ? s sfr v) = clock … s.
  #M #s #sfr #v %
qed.
  
lemma clock_set_clock:
  ∀M: Type[0].
  ∀s: PreStatus M.
  ∀v.
    clock … (set_clock … s v) = v.
  #M #s #v %
qed.

definition execute_1_preinstruction:
 ∀ticks: nat × nat.
 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A →
 ∀s:PreStatus M.
  Σs': PreStatus M.
   Or (clock … s' - clock … s = \fst ticks)
      (clock … s' - clock … s = \snd ticks)
 ≝
  λticks.
  λA, M: Type[0].
  λaddr_of: A → (PreStatus M) → Word.
  λinstr: preinstruction A.
  λs: PreStatus M.
  let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in
  let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in
  match instr return λx. Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks)
   (clock … s' - clock … s = \snd ticks) with
        [ ADD addr1 addr2 ⇒
            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 ⇒
            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 ⇒
            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 ⇒
          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 ⇒
          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 ⇒
          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
                eject … (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
                eject … (set_arg_8 ? s addr1 xor_val)
            ]
        | INC addr ⇒
            match addr
            return
             λx. bool_to_Prop
              (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) →
               Σs': PreStatus M.
                Or (clock … s' - clock … s = \fst ticks)
                   (clock … s' - clock … s = \snd ticks)
             with
              [ ACC_A ⇒ λacc_a: True.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in
                 eject … (set_arg_8 ? s' ACC_A result)
              | REGISTER r ⇒ λregister: True.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in
                 eject … (set_arg_8 ? s' (REGISTER r) result)
              | DIRECT d ⇒ λdirect: True.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in
                 eject … (set_arg_8 ? s' (DIRECT d) result)
              | INDIRECT i ⇒ λindirect: True.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
                 eject … (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
                  eject … (set_8051_sfr ? s' SFR_DPH bu)
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr)
        | NOP ⇒
           let s ≝ add_ticks2 s in
            s
        | DEC addr ⇒
           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
             eject … (set_arg_8 ? s addr result)
        | MUL addr1 addr2 ⇒
           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
             eject … (set_8051_sfr ? s SFR_ACC_B high)
        | DIV addr1 addr2 ⇒
           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
                   eject … (set_flags ? s false (None Bit) false)
               ]
        | DA addr ⇒
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ split ? 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'〉 ≝ split ? 4 4 result in
                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
                    let 〈 carry, nu 〉 ≝ half_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 ⇒ 
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) with
            [ ACC_A ⇒ λacc_a: True.
              let s ≝ add_ticks1 s in
                eject … (set_arg_8 ? s ACC_A (zero 8))
            | CARRY ⇒ λcarry: True.
              let s ≝ add_ticks1 s in
                eject … (set_arg_1 ? s CARRY false)
            | BIT_ADDR b ⇒ λbit_addr: True.
              let s ≝ add_ticks1 s in
                eject … (set_arg_1 ? s (BIT_ADDR b) false)
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        | CPL addr ⇒
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) 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
                  eject … (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
                  eject … (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
                  eject … (set_arg_1 ? s (BIT_ADDR b) new_bit)
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr)
        | SETB b ⇒
            let s ≝ add_ticks1 s in
            set_arg_1 ? s b false
        | RL _ ⇒ (* 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 _ ⇒ (* 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 _ ⇒ (* 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 _ ⇒ (* 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 _ ⇒ (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in
            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
            let new_acc ≝ nl @@ nu in
              set_8051_sfr ? s SFR_ACC_A new_acc
        | PUSH addr ⇒
            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. Or (clock … s' - clock … s = \fst ticks) (clock … s' - clock … s = \snd ticks) with
              [ DIRECT d ⇒ λdirect: True.
                let s ≝ add_ticks1 s in
                let 〈carry, new_sp〉 ≝ half_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 d
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr)
        | POP addr ⇒
            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 ⇒
            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
              eject … (set_arg_8 ? s addr2 old_acc)
        | XCHD addr1 addr2 ⇒
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_ACC_A) in
            let 〈arg_nu, arg_nl〉 ≝ split … 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 ⇒
            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 ⇒
            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 ⇒
          let s ≝ add_ticks1 s in
          (* DPM: only copies --- doesn't affect I/O *)
          match addr with
            [ inl l ⇒
              let 〈addr1, addr2〉 ≝ l in
                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
            ]
        | MOV addr ⇒
          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
                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
                            | inr r'''' ⇒
                              let 〈addr1, addr2〉 ≝ r'''' in
                                eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
                            ]
                        | inr r''' ⇒
                          let 〈addr1, addr2〉 ≝ r''' in
                            eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))
                        ]
                    | inr r'' ⇒
                      let 〈addr1, addr2〉 ≝ r'' in
                        eject … (set_arg_16 ? s (get_arg_16 ? s addr2) addr1)
                    ]
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                    eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
                ]
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
                eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))
            ]
          | JC addr ⇒
                  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 ⇒
                  if ¬(get_cy_flag ? s) then
                   let s ≝ add_ticks1 s in
                     eject … (set_program_counter ? s (addr_of addr s))
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JB addr1 addr2 ⇒
                  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 ⇒
                  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 ⇒
                  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 ⇒
                    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 ⇒
                    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 ⇒
                  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
                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
                          else
                            let s ≝ add_ticks2 s in
                              eject … (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
                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
                          else
                            let s ≝ add_ticks2 s in
                              eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))
                    ]
            | DJNZ addr1 addr2 ⇒
              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
        ]. (*15s*)
    try assumption (*20s*)
    try % (*6s*)
    try (
      @ (execute_1_technical … (subaddressing_modein …))
      @ I
    ) (*66s*)
 try @le_n
 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ //
 |*: cases daemon ]
(* 
 [2,6,10: normalize @I
 |1,5: /by/ (* 81 seconds *)
 |9:
   normalize nodelta <set_flags_ignores_clock >set_arg_8_ignores_clock
   >clock_set_clock //
 |23:
   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
   >set_8051_sfr_ignores_clock >clock_set_clock //
 |21,24:
   normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock
   >clock_set_clock //
 |25,26,28:
   normalize nodelta //
 |30,32,35:
   normalize nodelta //
 |13,14,15,16,18:
   normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
 |17:
   normalize nodelta >set_8051_sfr_ignores_clock >clock_set_clock //
 |3,4,7,8,11,12,19,20,33,36: cases daemon
 |27,29,31,34,37:
   normalize nodelta >set_program_counter_ignores_clock >clock_set_clock //
 |22:
   normalize nodelta <set_flags_ignores_clock >clock_set_clock //
 [9: (* normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock
     >clock_set_clock // *) (* segfault now *)
 |32,34: cases l #either normalize nodelta cases either
      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
      >clock_set_clock //
 |36,48: cases addr #either normalize nodelta cases either
      #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
      >clock_set_clock // (* XXX: change addr to l *)
 |44: cases l2 #either normalize nodelta
      [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock
          >clock_set_clock //
      |1: cases either #addr cases addr #addr1 #addr2 normalize nodelta
          >set_arg_8_ignores_clock >clock_set_clock //
      ] (* XXX: change l2 to l *)
 |5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false)
     #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock //
 |37: cases addr
 |20,21,30,31: (* XXX: segfault here *)
 |1,2,3: /by/ (*41s*)
 |4,6,7,8,10,11,12,13,14,15: /by/ (*6s*)
 |16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*)
 |33,35,39,41,43,54,55,56: /by/ (*6s*)
 |57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*)
 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *)
 |*:cases daemon] *)
qed.

lemma write_at_stack_pointer_ignores_clock:
  ∀M.∀s: PreStatus M.
  ∀sp: Byte.
    clock … (write_at_stack_pointer … s sp) = clock … s.
  #M #s #sp
  change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
   in match (write_at_stack_pointer ???);
  normalize nodelta
  cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
  #nu #nl normalize nodelta;
  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
  [ normalize nodelta; %
  | normalize nodelta; %
  ]
qed.

definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. Σs': Status. clock … s' - clock … s = \snd current ≝
  λs0,instr_pc_ticks.
    let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in
    let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in
    let s ≝ set_program_counter ? s0 pc in
      match instr return λ_.Status with
      [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks,ticks〉 [[ relative ]] ?
        (λx. λs.
        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
        [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ? s) (sign_extension r))
        | _ ⇒ λabsd. ⊥
        ] (subaddressing_modein … x)) instr s)
     | ACALL addr ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 = ticks with
            [ ADDR11 a ⇒ λaddr11: True.
              let 〈carry, new_sp〉 ≝ half_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〉 ≝ split ? 8 8 (program_counter ? s) in
              let s ≝ write_at_stack_pointer ? s pc_bl in
              let 〈carry, new_sp〉 ≝ half_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 〈thr, eig〉 ≝ split ? 3 8 a in
              let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
                set_program_counter ? s new_addr
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        | LCALL addr ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
            [ ADDR16 a ⇒ λaddr16: True.
              let 〈carry, new_sp〉 ≝ half_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〉 ≝ split ? 8 8 (program_counter ? s) in
              let s ≝ write_at_stack_pointer ? s pc_bl in
              let 〈carry, new_sp〉 ≝ half_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)
        | MOVC addr1 addr2 ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks 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 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in
              let result ≝ lookup ? ? new_addr (code_memory ? s) (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
              let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in
              (* DPM: Under specified: does the carry from PC incrementation affect the *)
              (*      addition of the PC with the DPTR? At the moment, no.              *)
              let s ≝ set_program_counter ? s inc_pc in
              let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in
              let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in
                set_8051_sfr ? s SFR_ACC_A result
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr2)
        | JMP _ ⇒ (* DPM: always indirect_dptr *)
          let s ≝ set_clock ? s (ticks + clock ? 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 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
          let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
            set_program_counter ? s new_pc
        | LJMP addr ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
            [ ADDR16 a ⇒ λaddr16: True.
                set_program_counter ? s a
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        | SJMP addr ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
            [ RELATIVE r ⇒ λrelative: True.
                let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
                  set_program_counter ? s new_pc
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
        | AJMP addr ⇒
          let s ≝ set_clock ? s (ticks + clock ? s) in
          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s' - clock … s0 =  ticks with
            [ ADDR11 a ⇒ λaddr11: True.
              let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
              let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
              let bit ≝ get_index' ? O ? nl in
              let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
              let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
                set_program_counter ? s new_pc
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr)
      ]. (*10s*)
    [||||||||*:try assumption]
    [1,2,3,4,5,7: @sig2 (*7s*)
    |8: cases (execute_1_preinstruction ??????) #a * #H @H]
    [2,3: >set_program_counter_ignores_clock normalize nodelta
      >write_at_stack_pointer_ignores_clock
      >set_8051_sfr_ignores_clock
      >write_at_stack_pointer_ignores_clock
      >set_8051_sfr_ignores_clock >clock_set_clock
      >set_program_counter_ignores_clock
      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H] (*Andrea: ???*)
    |1,4,5,6: >set_program_counter_ignores_clock normalize nodelta
     >clock_set_clock >set_program_counter_ignores_clock
     cut (∀n,m. n+m-m = n) [1,3,5,7:#n #m /by/ |*: #H @H] (*Andrea: ???*)
    |7: >set_8051_sfr_ignores_clock normalize nodelta
      >clock_set_clock >set_program_counter_ignores_clock
      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]
    |8: >set_8051_sfr_ignores_clock normalize nodelta
      >set_program_counter_ignores_clock >clock_set_clock
      >set_program_counter_ignores_clock
      cut (∀n,m. n+m-m = n) [1,3:#n #m /by/ |*: #H @H]]
qed.

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

definition execute_1: ∀s:Status. Σs':Status. clock … s' - clock … s = current_instruction_cost s ≝
  λs: Status.
    let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in
     execute_1_0 s instr_pc_ticks.

definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus ≝
  λticks,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 y x) instr s
    | Comment cmt ⇒
       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
        s
    | Cost cst ⇒ s
    | Jmp jmp ⇒
       let s ≝ set_clock ? s (\fst ticks + clock ? s) in
        set_program_counter ? s (address_of_word_labels s jmp)
    | Call call ⇒
      let s ≝ set_clock ? s (\fst ticks + clock ? s) in
      let a ≝ address_of_word_labels s call in
      let 〈carry, new_sp〉 ≝ half_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〉 ≝ split ? 8 8 (program_counter ? s) in
      let s ≝ write_at_stack_pointer ? s pc_bl in
      let 〈carry, new_sp〉 ≝ half_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 (code_memory ? s) 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.
  normalize
  @ I
qed.

definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
  λticks_of,s.
  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
  let ticks ≝ ticks_of (program_counter ? s) in
   execute_1_pseudo_instruction0 ticks s instr pc.

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

let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (s: PseudoStatus) on n: PseudoStatus ≝
  match n with
    [ O ⇒ s
    | S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_of s)
    ].