source: src/ASM/AssemblyProof.ma @ 1945

include "ASM/Assembly.ma".
include "ASM/Interpret.ma".
include "ASM/StatusProofs.ma".
include alias "arithmetics/nat.ma".

definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
  λP.
    P true ∧ P false.
 
let rec bitvector_elim_prop_internal
  (n: nat) (P: BitVector n → Prop) (m: nat)
    on m:
      m ≤ n → BitVector (n - m) → Prop ≝
  match m return λm. m ≤ n → BitVector (n - m) → Prop with
  [ O    ⇒ λprf1. λprefix. P ?
  | S n' ⇒ λprf2. λprefix.
      bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
  ].
  [1:
    applyS prefix
  |2:
    letin res ≝ (bit ::: prefix)
    <minus_S_S >minus_Sn_m
    try assumption @res
  |3:
    @le_S_to_le
    assumption
  ]
qed.

definition bitvector_elim_prop ≝
  λn: nat.
  λP: BitVector n → Prop.
    bitvector_elim_prop_internal n P n ? ?.
  [ @(le_n ?)
  | <(minus_n_n ?)
    @[[ ]]
  ]
qed.

lemma bool_eq_internal_eq:
  ∀b, c.
    (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
  #b #c
  cases b
  [1:
    normalize //
  |2:
    normalize
    cases c normalize //
  ]
qed.

definition bit_elim: ∀P: bool → bool. bool ≝
  λP.
    P true ∧ P false.

let rec bitvector_elim_internal
  (n: nat) (P: BitVector n → bool) (m: nat)
    on m:
      m ≤ n → BitVector (n - m) → bool ≝
  match m return λm. m ≤ n → BitVector (n - m) → bool with
  [ O    ⇒ λprf1. λprefix. P ?
  | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
  ].
  [1:
    applyS prefix
  |2:
    letin res ≝ (bit ::: prefix)
    <(minus_S_S ? ?) >(minus_Sn_m ? ?)
    try @prf2 @res
  |3:
    /2/
  ].
qed.

definition bitvector_elim ≝
  λn: nat.
  λP: BitVector n → bool.
    bitvector_elim_internal n P n ? ?.
  try @le_n
  <minus_n_n @[[]]
qed.

lemma super_rewrite2:
  ∀A:Type[0].
  ∀n, m: nat.
  ∀v1: Vector A n.
  ∀v2: Vector A m.
  ∀P: ∀m. Vector A m → Prop.
    n = m → v1 ≃ v2 → P n v1 → P m v2.
  #A #n #m #v1 #v2 #P #eq #jmeq
  destruct #assm assumption
qed.

lemma vector_cons_append:
  ∀A: Type[0].
  ∀n: nat.
  ∀e: A.
  ∀v: Vector A n.
    e ::: v = [[ e ]] @@ v.
  #A #n #e #v
  cases v try %
  #n' #hd #tl %
qed.

lemma vector_cons_append2:
  ∀A: Type[0].
  ∀n, m: nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀hd: A.
    hd:::(v@@q) = (hd:::v)@@q.
  #A #n #m #v #q
  elim v try (#hd %)
  #n' #hd' #tl' #ih #hd'
  <ih %
qed.

lemma jmeq_cons_vector_monotone:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v: Vector A m.
  ∀q: Vector A n.
  ∀prf: m = n.
  ∀hd: A.
    v ≃ q → hd:::v ≃ hd:::q.
  #A #m #n #v #q #prf #hd #E
  @(super_rewrite2 A … E)
  try assumption %
qed.

lemma vector_associative_append:
  ∀A: Type[0].
  ∀n, m, o:  nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀r: Vector A o.
    (v @@ q) @@ r ≃ v @@ (q @@ r).
  #A #n #m #o #v #q #r
  elim v try %
  #n' #hd #tl #ih
  <(vector_cons_append2 A … hd)
  @jmeq_cons_vector_monotone
  try assumption
  @associative_plus
qed.

lemma mem_middle_vector:
  ∀A: Type[0].
  ∀m, o: nat.
  ∀eq: A → A → bool.
  ∀reflex: ∀a. eq a a = true.
  ∀p: Vector A m.
  ∀a: A.
  ∀r: Vector A o.
    mem A eq ? (p@@(a:::r)) a = true.
  #A #m #o #eq #reflex #p #a
  elim p try (normalize >reflex #H %)
  #m' #hd #tl #inductive_hypothesis
  normalize
  cases (eq ??) normalize nodelta
  try (#irrelevant %)
  @inductive_hypothesis
qed.

lemma mem_monotonic_wrt_append:
  ∀A: Type[0].
  ∀m, o: nat.
  ∀eq: A → A → bool.
  ∀reflex: ∀a. eq a a = true.
  ∀p: Vector A m.
  ∀a: A.
  ∀r: Vector A o.
    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
  #A #m #o #eq #reflex #p #a
  elim p try (#r #assm assumption)
  #m' #hd #tl #inductive_hypothesis #r #assm
  normalize
  cases (eq ??) try %
  @inductive_hypothesis assumption
qed.

lemma subvector_multiple_append:
  ∀A: Type[0].
  ∀o, n: nat.
  ∀eq: A → A → bool.
  ∀refl: ∀a. eq a a = true.
  ∀h: Vector A o.
  ∀v: Vector A n.
  ∀m: nat.
  ∀q: Vector A m.
    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
  #A #o #n #eq #reflex #h #v
  elim v try (normalize #m #irrelevant @I)
  #m' #hd #tl #inductive_hypothesis #m #q
  change with (bool_to_Prop (andb ??))
  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
  [1:
    @mem_monotonic_wrt_append try assumption
    @mem_monotonic_wrt_append try assumption
    normalize >reflex %
  |2:
    #assm >assm
    >vector_cons_append
    change with (bool_to_Prop (subvector_with ??????))
    @(super_rewrite2 … (vector_associative_append … q [[hd]] tl))
    try @associative_plus
    @inductive_hypothesis
  ]
qed.

lemma vector_cons_empty:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
    [[ ]] @@ v = v.
  #A #n #v
  cases v try %
  #n' #hd #tl %
qed.

corollary subvector_hd_tl:
  ∀A: Type[0].
  ∀o: nat.
  ∀eq: A → A → bool.
  ∀refl: ∀a. eq a a = true.
  ∀h: A.
  ∀v: Vector A o.
    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
  #A #o #eq #reflex #h #v
  >(vector_cons_append … h v)
  <(vector_cons_empty … ([[h]] @@ v))
  @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
qed.

lemma eq_a_reflexive:
  ∀a. eq_a a a = true.
  #a cases a %
qed.

lemma is_in_monotonic_wrt_append:
  ∀m, n: nat.
  ∀p: Vector addressing_mode_tag m.
  ∀q: Vector addressing_mode_tag n.
  ∀to_search: addressing_mode.
    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
  #m #n #p #q #to_search #assm
  elim q try assumption
  #n' #hd #tl #inductive_hypothesis
  normalize
  cases (is_a ??) try @I
  >inductive_hypothesis @I
qed.

corollary is_in_hd_tl:
  ∀to_search: addressing_mode.
  ∀hd: addressing_mode_tag.
  ∀n: nat.
  ∀v: Vector addressing_mode_tag n.
    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
  #to_search #hd #n #v
  elim v
  [1:
    #absurd
    normalize in absurd; cases absurd
  |2:
    #n' #hd' #tl #inductive_hypothesis #assm
    >vector_cons_append >(vector_cons_append … hd' tl)
    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
    assumption
  ]
qed.
  
let rec list_addressing_mode_tags_elim
  (n: nat) (l: Vector addressing_mode_tag (S n))
    on l: (l → bool) → bool ≝
  match l return λx.
    match x with
    [ O ⇒ λl: Vector … O. bool
    | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool
    ] with
  [ VEmpty      ⇒  true  
  | VCons len hd tl ⇒ λP.
    let process_hd ≝
      match hd return λhd. ∀P: hd:::tl → bool. bool with
      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
      | acc_a ⇒ λP.P ACC_A
      | acc_b ⇒ λP.P ACC_B
      | dptr ⇒ λP.P DPTR
      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
      | acc_dptr ⇒ λP.P ACC_DPTR
      | acc_pc ⇒ λP.P ACC_PC
      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
      | carry ⇒ λP.P CARRY
      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
      ]
    in
      andb (process_hd P)
       (match len return λx. x = len → bool with
         [ O ⇒ λprf. true
         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
  ].
  try %
  [2:
    cases (sym_eq ??? prf); assumption
  |1:
    generalize in match H; generalize in match tl;
    destruct #tl
    normalize in ⊢ (∀_: %. ?);
    #H
    whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
    cases (is_a hd (subaddressing_modeel y tl H))
    whd try @I normalize nodelta //
  ]
qed.

definition product_elim ≝
  λm, n: nat.
  λv: Vector addressing_mode_tag (S m).
  λq: Vector addressing_mode_tag (S n).
  λP: (v × q) → bool.
    list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).

definition union_elim ≝ 
  λA, B: Type[0].
  λelimA: (A → bool) → bool.
  λelimB: (B → bool) → bool.
  λelimU: A ⊎ B → bool.
    elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).

(*                           
definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
  λP.
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
    P (DA ? ACC_A) ∧
    bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
    list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    P (RL ? ACC_A) ∧
    P (RLC ? ACC_A) ∧
    P (RR ? ACC_A) ∧
    P (RRC ? ACC_A) ∧
    P (SWAP ? ACC_A) ∧
    P (RET ?) ∧
    P (RETI ?) ∧
    P (NOP ?) ∧
    bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
    list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
    bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
    bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
    union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
                   (product_elim ? ? [[ registr; indirect ]] [[ data ]])
                   (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
    list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
    union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
                   (product_elim ? ? [[direct]] [[ acc_a ; data ]])
                   (λd. P (XRL ? d)) ∧
    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) 
                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
                   (λd. P (ANL ? d)) ∧
    union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) 
                                   (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
                   (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
                   (λd. P (ORL ? d)) ∧
    union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
                   (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
                   (λd. P (MOVX ? d)) ∧
    union_elim ? ? (
      union_elim ? ? (
        union_elim ? ? (
          union_elim ? ? (
            union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
                            (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
                            (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
                            (product_elim ? ? [[dptr]] [[data16]]))
                            (product_elim ? ? [[carry]] [[bit_addr]]))
                            (product_elim ? ? [[bit_addr]] [[carry]])
                            (λd. P (MOV ? d)).
  %
qed.
  
definition instruction_elim: ∀P: instruction → bool. bool ≝
  λP. (*
    bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
    bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
    bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
    bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
    bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
    P (JMP INDIRECT_DPTR) ∧
    list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
    preinstruction_elim (λp. P (RealInstruction p)). *)
  %
qed.


axiom instruction_elim_complete:
 ∀P. instruction_elim P = true → ∀i. P i = true.
*)
(*definition eq_instruction ≝
  λi, j: instruction.
    true.*)

definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
  λa, b: addressing_mode.
  match a with
  [ DIRECT d ⇒
    match b with
    [ DIRECT e ⇒ eq_bv ? d e
    | _ ⇒ false
    ]
  | INDIRECT b' ⇒
    match b with
    [ INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | EXT_INDIRECT b' ⇒
    match b with
    [ EXT_INDIRECT e ⇒ eq_b b' e
    | _ ⇒ false
    ]
  | REGISTER bv ⇒
    match b with
    [ REGISTER bv' ⇒ eq_bv ? bv bv'
    | _ ⇒ false
    ]
  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
  | DATA b' ⇒
    match b with
    [ DATA e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | DATA16 w ⇒ 
    match b with
    [ DATA16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
  | BIT_ADDR b' ⇒
    match b with
    [ BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | N_BIT_ADDR b' ⇒ 
    match b with
    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
    | _ ⇒ false
    ]
  | RELATIVE n ⇒
    match b with
    [ RELATIVE e ⇒ eq_bv ? n e
    | _ ⇒ false
    ]
  | ADDR11 w ⇒
    match b with
    [ ADDR11 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  | ADDR16 w ⇒
    match b with
    [ ADDR16 e ⇒ eq_bv ? w e
    | _ ⇒ false
    ]
  ].

lemma eq_bv_refl:
  ∀n, b.
    eq_bv n b b = true.
  #n #b cases b //
qed.

lemma eq_b_refl:
  ∀b.
    eq_b b b = true.
  #b cases b //
qed.

lemma eq_addressing_mode_refl:
  ∀a. eq_addressing_mode a a = true.
  #a
  cases a try #arg1 try #arg2
  try @eq_bv_refl try @eq_b_refl
  try normalize %
qed.
  
definition eq_sum:
    ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
  λlt, rt, leq, req, left, right.
    match left with
    [ inl l ⇒
      match right with
      [ inl l' ⇒ leq l l'
      | _ ⇒ false
      ]
    | inr r ⇒
      match right with
      [ inr r' ⇒ req r r'
      | _ ⇒ false
      ]
    ].

definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
  λlt, rt, leq, req, left, right.
    let 〈l, r〉 ≝ left in
    let 〈l', r'〉 ≝ right in
      leq l l' ∧ req r r'.

definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
  λi, j.
  match i with
  [ ADD arg1 arg2 ⇒
    match j with
    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | ADDC arg1 arg2 ⇒
    match j with
    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | SUBB arg1 arg2 ⇒
    match j with
    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | INC arg ⇒
    match j with
    [ INC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | DEC arg ⇒
    match j with
    [ DEC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MUL arg1 arg2 ⇒
    match j with
    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DIV arg1 arg2 ⇒
    match j with
    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DA arg ⇒
    match j with
    [ DA arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JC arg ⇒
    match j with
    [ JC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNC arg ⇒
    match j with
    [ JNC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JB arg1 arg2 ⇒
    match j with
    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JNB arg1 arg2 ⇒
    match j with
    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JBC arg1 arg2 ⇒
    match j with
    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | JZ arg ⇒
    match j with
    [ JZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JNZ arg ⇒
    match j with
    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CJNE arg1 arg2 ⇒
    match j with
    [ CJNE arg1' arg2' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | DJNZ arg1 arg2 ⇒
    match j with
    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | CLR arg ⇒
    match j with
    [ CLR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | CPL arg ⇒
    match j with
    [ CPL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RL arg ⇒
    match j with
    [ RL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RLC arg ⇒
    match j with
    [ RLC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RR arg ⇒
    match j with
    [ RR arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | RRC arg ⇒
    match j with
    [ RRC arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SWAP arg ⇒
    match j with
    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SETB arg ⇒
    match j with
    [ SETB arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | PUSH arg ⇒
    match j with
    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | POP arg ⇒
    match j with
    [ POP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | XCH arg1 arg2 ⇒
    match j with
    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | XCHD arg1 arg2 ⇒
    match j with
    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
  | MOVX arg ⇒
    match j with
    [ MOVX arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | XRL arg ⇒
    match j with
    [ XRL arg' ⇒
      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ORL arg ⇒
    match j with
    [ ORL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | ANL arg ⇒
    match j with
    [ ANL arg' ⇒
      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
        sum_eq arg arg'
    | _ ⇒ false
    ]
  | MOV arg ⇒
    match j with
    [ MOV arg' ⇒
      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
        sum_eq_5 arg arg'
    | _ ⇒ false
    ]
  ].

lemma eq_sum_refl:
  ∀A, B: Type[0].
  ∀leq, req.
  ∀s.
  ∀leq_refl: (∀t. leq t t = true).
  ∀req_refl: (∀u. req u u = true).
    eq_sum A B leq req s s = true.
  #A #B #leq #req #s #leq_refl #req_refl
  cases s assumption
qed.

lemma eq_prod_refl:
  ∀A, B: Type[0].
  ∀leq, req.
  ∀s.
  ∀leq_refl: (∀t. leq t t = true).
  ∀req_refl: (∀u. req u u = true).
    eq_prod A B leq req s s = true.
  #A #B #leq #req #s #leq_refl #req_refl
  cases s
  whd in ⊢ (? → ? → ??%?);
  #l #r
  >leq_refl @req_refl
qed.

lemma eq_preinstruction_refl:
  ∀i.
    eq_preinstruction i i = true.
  #i cases i try #arg1 try #arg2
  try @eq_addressing_mode_refl
  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    whd in ⊢ (??%?); try %
    >eq_addressing_mode_refl
    >eq_addressing_mode_refl %
  |13,15:
    whd in ⊢ (??%?);
    cases arg1
    [*:
      #arg1_left normalize nodelta
      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
    ]
  |11,12:
    whd in ⊢ (??%?);
    cases arg1
    [1:
      #arg1_left normalize nodelta 
      >(eq_sum_refl …)
      [1: % | 2,3: #arg @eq_prod_refl ]
      @eq_addressing_mode_refl
    |2:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: @eq_addressing_mode_refl ]
    |3:
      #arg1_left normalize nodelta
      >(eq_sum_refl …)
      [1:
        %
      |2,3:
        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
      ]
    |4:
      #arg1_left normalize nodelta
      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
    ]
  |14:
    whd in ⊢ (??%?);
    cases arg1
    [1:
      #arg1_left normalize nodelta
      @eq_sum_refl
      [1:
        #arg @eq_sum_refl
        [1:
          #arg @eq_sum_refl
          [1:
            #arg @eq_sum_refl
            [1:
              #arg @eq_prod_refl
              [*:
                @eq_addressing_mode_refl
              ]
            |2:
              #arg @eq_prod_refl
              [*:
                #arg @eq_addressing_mode_refl
              ]
            ]
          |2:
            #arg @eq_prod_refl
            [*:
              #arg @eq_addressing_mode_refl
            ]
          ]
        |2:
          #arg @eq_prod_refl
          [*:
            #arg @eq_addressing_mode_refl
          ]
        ]
      |2:
        #arg @eq_prod_refl
        [*:
          #arg @eq_addressing_mode_refl
        ]
      ]
    |2:
      #arg1_right normalize nodelta
      @eq_prod_refl
      [*:
        #arg @eq_addressing_mode_refl
      ]
    ]
  |*:
    whd in ⊢ (??%?);
    cases arg1
    [*:
      #arg1 >eq_sum_refl
      [1,4:
        @eq_addressing_mode_refl
      |2,3,5,6:
        #arg @eq_prod_refl
        [*:
          #arg @eq_addressing_mode_refl
        ]
      ]
    ]
  ]
qed.

definition eq_instruction: instruction → instruction → bool ≝
  λi, j.
  match i with
  [ ACALL arg ⇒
    match j with
    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LCALL arg ⇒
    match j with
    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | AJMP arg ⇒ 
    match j with
    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | LJMP arg ⇒
    match j with
    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | SJMP arg ⇒ 
    match j with
    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | JMP arg ⇒
    match j with
    [ JMP arg' ⇒ eq_addressing_mode arg arg'
    | _ ⇒ false
    ]
  | MOVC arg1 arg2 ⇒
    match j with
    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
    | _ ⇒ false
    ]
  | RealInstruction instr ⇒
    match j with
    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
    | _ ⇒ false
    ]
  ].
  
lemma eq_instruction_refl:
  ∀i. eq_instruction i i = true.
  #i cases i [*: #arg1 ]
  try @eq_addressing_mode_refl
  try @eq_preinstruction_refl
  #arg2 whd in ⊢ (??%?);
  >eq_addressing_mode_refl >eq_addressing_mode_refl %
qed.

let rec vect_member
  (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A)
    on v: bool ≝
  match v with
  [ VEmpty          ⇒ false
  | VCons len hd tl ⇒
      eq hd a ∨ (vect_member A ? eq tl a)
  ].

let rec list_addressing_mode_tags_elim_prop
  (n: nat)
  (l: Vector addressing_mode_tag (S n))
  on l:
  ∀P: l → Prop.
  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
  ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
  ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
  ∀x: l. P x ≝
  match l return
    λy.
      match y with
      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
               ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
               ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
               ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
               ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
               ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
               ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
               ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
               ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
               ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
               ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
               ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
               ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
               ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
               ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
               ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
               ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
               ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
               ∀x:l. P x
      ] with
  [ VEmpty          ⇒ λAbsurd. ⊥
  | VCons len hd tl ⇒ λProof. ?
  ] (refl ? (S n)). cases daemon. qed. (*
  [ destruct(Absurd)
  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
    # A8 # A9 # A10 # A11 # A12 # A13 # A14
    # A15 # A16 # A17 # A18 # A19 # X
    cases X
    # SUB cases daemon ] qed.
    cases SUB
    [ # BYTE
    normalize
  ].
  
  
(*    let prepare_hd ≝
      match hd with
      [ direct ⇒ λdirect_prf. ?
      | indirect ⇒ λindirect_prf. ?
      | ext_indirect ⇒ λext_indirect_prf. ?
      | registr ⇒ λregistr_prf. ?
      | acc_a ⇒ λacc_a_prf. ?
      | acc_b ⇒ λacc_b_prf. ?
      | dptr ⇒ λdptr_prf. ?
      | data ⇒ λdata_prf. ?
      | data16 ⇒ λdata16_prf. ?
      | acc_dptr ⇒ λacc_dptr_prf. ?
      | acc_pc ⇒ λacc_pc_prf. ?
      | ext_indirect_dptr ⇒ λext_indirect_prf. ?
      | indirect_dptr ⇒ λindirect_prf. ?
      | carry ⇒ λcarry_prf. ?
      | bit_addr ⇒ λbit_addr_prf. ?
      | n_bit_addr ⇒ λn_bit_addr_prf. ?
      | relative ⇒ λrelative_prf. ?
      | addr11 ⇒ λaddr11_prf. ?
      | addr16 ⇒ λaddr16_prf. ?
      ]
    in ? *)
  ].
  [ 1: destruct(absd)
  | 2: # A1 # A2 # A3 # A4 # A5 # A6
       # A7 # A8 # A9 # A10 # A11 # A12
       # A13 # A14 # A15 # A16 # A17 # A18
       # A19 * 
  ].


  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
   (l → bool) → bool ] with
  [ VEmpty      ⇒  true  
  | VCons len hd tl ⇒ λP.
    let process_hd ≝
      match hd return λhd. ∀P: hd:::tl → bool. bool with
      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
      | acc_a ⇒ λP.P ACC_A
      | acc_b ⇒ λP.P ACC_B
      | dptr ⇒ λP.P DPTR
      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
      | acc_dptr ⇒ λP.P ACC_DPTR
      | acc_pc ⇒ λP.P ACC_PC
      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
      | carry ⇒ λP.P CARRY
      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
      ]
    in
      andb (process_hd P)
       (match len return λx. x = len → bool with
         [ O ⇒ λprf. true
         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
  ].
  try %
  [ 2: cases (sym_eq ??? prf); @tl
  | generalize in match H; generalize in match tl; cases prf;
    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    #tl
    normalize in ⊢ (∀_: %. ?)
    # H
    whd
    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
qed.
*)

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

lemma split_zero:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = split A 0 m v.
  #A #m #v
  cases v try %
  #n #hd #tl %
qed.

lemma Vector_O:
  ∀A: Type[0].
  ∀v: Vector A 0.
    v ≃ VEmpty A.
 #A #v
 generalize in match (refl … 0);
 cases v in ⊢ (??%? → ?%%??); //
 #n #hd #tl #absurd
 destruct(absurd)
qed.

lemma Vector_Sn:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A (S n).
    ∃hd: A. ∃tl: Vector A n.
      v ≃ VCons A n hd tl.
  #A #n #v
  generalize in match (refl … (S n));
  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
  [1:
    #absurd destruct(absurd)
  |2:
    #m #hd #tl #eq
    <(injective_S … eq)
    %{hd} %{tl} %
  ]
qed.

lemma vector_append_zero:
  ∀A,m.
  ∀v: Vector A m.
  ∀q: Vector A 0.
    v = q@@v.
  #A #m #v #q
  >(Vector_O A q) %
qed.

lemma prod_eq_left:
  ∀A: Type[0].
  ∀p, q, r: A.
    p = q → 〈p, r〉 = 〈q, r〉.
  #A #p #q #r #hyp
  destruct %
qed.

lemma prod_eq_right:
  ∀A: Type[0].
  ∀p, q, r: A.
    p = q → 〈r, p〉 = 〈r, q〉.
  #A #p #q #r #hyp
  destruct %
qed.

corollary prod_vector_zero_eq_left:
  ∀A, n.
  ∀q: Vector A O.
  ∀r: Vector A n.
    〈q, r〉 = 〈[[ ]], r〉.
  #A #n #q #r
  generalize in match (Vector_O A q …);
  #hyp destruct %
qed.

lemma tail_head:
  ∀a: Type[0].
  ∀m, n: nat.
  ∀hd: a.
  ∀l: Vector a m.
  ∀r: Vector a n.
    tail a ? (hd:::(l@@r)) = l@@r.
  #a #m #n #hd #l #r
  cases l try %
  #m' #hd' #tl' %
qed.

lemma head_head':
  ∀a: Type[0].
  ∀m: nat.
  ∀hd: a.
  ∀l: Vector a m.
    hd = head' … (hd:::l).
  #a #m #hd #l cases l try %
  #m' #hd' #tl %
qed.

lemma split_succ:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd: A.
    v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)).
  #A #m
  elim m
  [1:
    #n #l #r #v #hd #eq #hyp
    destruct >(Vector_O … l) %
  |2:
    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
    destruct
    cases (Vector_Sn … l) #hd' #tl'
    whd in ⊢ (???%);
    >tail_head
    <(? : split A (S m') n (l@@r) = split' A (S m') n (l@@r))
    try (<hyp <head_head' %)
    elim l normalize //
  ]
qed.

lemma split_prod:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = split A m n p.
  #A #m elim m
  [1:
    #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @split_zero
  |2:
    #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v) #hd #exists
    cases exists #tl #jmeq
    >jmeq @split_succ try %
    @ih %
  ]
qed.

(*
lemma split_prod_exists:
  ∀A, m, n.
  ∀p: Vector A (m + n).
  ∃v: Vector A m.
  ∃q: Vector A n.
    〈v, q〉 = split A m n p.
  #A #m #n #p
  elim m
  @ex_intro
  [1:
  |2: @ex_intro
      [1: 
      |2:
      ]
  ]
*)

definition split_elim:
  ∀A: Type[0].
  ∀l, m: nat.
  ∀v: Vector A (l + m).
  ∀P: (Vector A l) × (Vector A m) → Prop.
    (∀vl: Vector A l.
     ∀vm: Vector A m.
      v = vl@@vm → P 〈vl,vm〉) → P (split A l m v) ≝
  λa: Type[0].
  λl, m: nat.
  λv: Vector a (l + m).
  λP. ?.
  cases daemon
qed.

(* XXX: this looks almost certainly wrong *)
example half_add_SO:
 ∀pc.
 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
 cases daemon.
qed.

(*
axiom not_eqvb_S:
 ∀pc.
 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).

axiom not_eqvb_SS:
 ∀pc.
 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
 
axiom bitvector_elim_complete:
 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.

lemma bitvector_elim_complete':
 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
qed.
*)

(*
lemma andb_elim':
 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
qed.
*)

let rec encoding_check
  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    (encoding: list Byte)
      on encoding: Prop ≝
  match encoding with
  [ nil ⇒ final_pc = pc
  | cons hd tl ⇒
    let 〈new_pc, byte〉 ≝ next code_memory pc in
      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
  ].

axiom add_bitvector_of_nat_Sm:
  ∀n, m: nat.
    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
      bitvector_of_nat n (S m).

lemma encoding_check_append:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀final_pc: Word.
  ∀l1: list Byte.
  ∀pc: Word.
  ∀l2: list Byte.
    encoding_check code_memory pc final_pc (l1@l2) →
      let pc_plus_len ≝ add … pc (bitvector_of_nat … (length … l1)) in
        encoding_check code_memory pc pc_plus_len l1 ∧
          encoding_check code_memory pc_plus_len final_pc l2.
  #code_memory #final_pc #l1 elim l1
  [1:
    #pc #l2
    whd in ⊢ (????% → ?); #H
    <add_zero
    whd whd in ⊢ (?%?); /2/
  |2:
    #hd #tl #IH #pc #l2 * #H1 #H2
(*    >half_add_SO in H2; #H2 *)
    cases (IH … H2) #E1 #E2 %
    [1:
      % try @H1
      <(add_bitvector_of_nat_Sm 16 (|tl|)) in E1;
      <add_associative #assm assumption
    |2:
      <add_associative in E2;
      <(add_bitvector_of_nat_Sm 16 (|tl|)) #assm
      assumption
    ]
  ]
qed.

axiom bitvector_3_cases:
  ∀b: BitVector 3.
  ∃l, c, r: bool.
    b = [[l; c; r]].

lemma bitvector_3_elim_prop:
  ∀P: BitVector 3 → Prop.
    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
  cases (bitvector_3_cases … H9) #l #assm cases assm
  -assm #c #assm cases assm
  -assm #r #assm cases assm destruct
  cases l cases c cases r //
qed.

definition ticks_of_instruction ≝
  λi.
    let trivial_code_memory ≝ assembly1 i in
    let trivial_status ≝ load_code_memory trivial_code_memory in
      \snd (fetch trivial_status (zero ?)).

lemma fetch_assembly:
  ∀pc: Word.
  ∀i: instruction.
  ∀code_memory: BitVectorTrie Byte 16.
  ∀assembled: list Byte.
    assembled = assembly1 i →
      let len ≝ length … assembled in
      let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
        encoding_check code_memory pc pc_plus_len assembled →
          let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in
           (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true.
  #pc #i #code_memory #assembled cases i [8: *]
 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
 [47,48,49:
 |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
   59,60,63,64,65,66,67: #ARG]]
 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
  56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
  [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
   68,69,70,71: #ARG2]]
 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
 normalize in ⊢ (???% → ?);
 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
  normalize in ⊢ (???% → ?);]
 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
(*
 whd in ⊢ (let ? ≝ ??% in ?); <H1 whd in ⊢ (let fetched ≝ % in ?)
 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
 [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,
  30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
 whd >eq_instruction_refl >H4 @eq_bv_refl
*) (* XXX: not working! *)
qed.

let rec fetch_many
  (code_memory: BitVectorTrie Byte 16) (final_pc: Word) (pc: Word)
    (expected: list instruction)
      on expected: Prop ≝
  match expected with
  [ nil ⇒ eq_bv … pc final_pc = true
  | cons i tl ⇒
    let fetched ≝ fetch code_memory pc in
    let 〈instr_pc, ticks〉 ≝ fetched in
    let 〈instr,pc'〉 ≝ instr_pc in
      eq_instruction instr i = true ∧
        ticks = (ticks_of_instruction i) ∧
        fetch_many code_memory final_pc pc' tl
  ].

lemma option_destruct_Some:
  ∀A: Type[0].
  ∀a, b: A.
    Some A a = Some A b → a = b.
  #A #a #b #EQ
  destruct %
qed.

axiom eq_instruction_to_eq:
  ∀i1, i2: instruction.
    eq_instruction i1 i2 = true → i1 ≃ i2.
          
lemma fetch_assembly_pseudo':
  ∀lookup_labels.
  ∀sigma: Word → Word × bool.
  ∀ppc.
  ∀lookup_datalabels.
  ∀pi.
  ∀code_memory.
  ∀len.
  ∀assembled.
  ∀instructions.
    let 〈pc, force_long_jump〉 ≝ sigma ppc in
      instructions = expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi →
        〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi →
          let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
            encoding_check code_memory pc pc_plus_len assembled →
              fetch_many code_memory pc_plus_len pc instructions.
  #lookup_labels #sigma #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions
  generalize in match (refl … (sigma ppc));
  cases (sigma ?) in ⊢ (??%? → %); #pc #force_long_jump #sigma_refl normalize nodelta
  #instructions_refl whd in ⊢ (???% → ?); <instructions_refl whd in ⊢ (???% → ?); #assembled_refl
  cases (pair_destruct ?????? assembled_refl) -assembled_refl #len_refl #assembled_refl
  >len_refl >assembled_refl -len_refl
  generalize in match (add 16 pc
    (bitvector_of_nat 16
     (|flatten (Vector bool 8)
       (map instruction (list (Vector bool 8)) assembly1 instructions)|)));
  #final_pc
  generalize in match pc; elim instructions
  [1:
    #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
  |2:
    #i #tl #IH #pc #H whd
    cases (encoding_check_append ????? H) -H #H1 #H2
    @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta
    @pair_elim #instr #pc' #instr_pc_refl normalize nodelta
    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
    #H3 lapply (H3 H1) -H3 >fetch_refl >instr_pc_refl normalize nodelta
    #H3 lapply (conjunction_true ?? H3) * #H4 #H5 %
    [1:
      lapply (conjunction_true … H4) * #B1 #B2
      % try assumption @eqb_true_to_eq
      <(eq_instruction_to_eq … B1) assumption
    |2:
      >(eq_bv_eq … H5) @IH @H2
    ]
  ]
qed.

lemma fetch_assembly_pseudo:
  ∀program: pseudo_assembly_program.
  ∀sigma: Word → Word × bool.
  let lookup_labels ≝ λx:Identifier.\fst (sigma (address_of_word_labels_code_mem (\snd  program) x)) in
  ∀ppc.∀code_memory.
  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
  let pc ≝ \fst (sigma ppc) in
  let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    encoding_check code_memory pc pc_plus_len assembled →
      fetch_many code_memory pc_plus_len pc instructions.
 #program #sigma letin lookup_labels ≝ (λx.?) #ppc #code_memory
 letin lookup_datalabels ≝ (λx.?) 
 letin pi ≝ (fst ???)
 letin pc ≝ (fst ???)
 letin instructions ≝ (expand_pseudo_instruction ?????)
 @pair_elim #len #assembled #assembled_refl normalize nodelta
 #H
 generalize in match
  (fetch_assembly_pseudo' lookup_labels sigma ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?;
 #X destruct
 cases (sigma ppc) in H X; #pc #force_long_jump normalize nodelta
 #H #X @X try % <assembled_refl try % assumption
qed.

(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
   function that load the code in memory is correct. The latter is based
   on missing properties from the standard library on the BitVectorTrie
   data structrure.
   
   Wrong at the moment, requires Jaap's precondition to ensure that the program
   does not overflow when put into code memory (i.e. shorter than 2^16 bytes).
*)
axiom assembly_ok:
 ∀program,sigma,assembled,costs'.
  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
  〈assembled,costs'〉 = assembly program sigma →
  costs = costs' ∧
  let code_memory ≝ load_code_memory assembled in
  let datalabels ≝ construct_datalabels (\fst program) in
  let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in  
  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
  ∀ppc.
  let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi in
  let pc ≝ \fst (sigma ppc) in
  let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
   encoding_check code_memory pc pc_plus_len assembled ∧
       \fst (sigma newppc) = add … pc (bitvector_of_nat … len).

(* XXX: should we add that costs = costs'? *)
lemma fetch_assembly_pseudo2:
 ∀program,sigma,ppc.
  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
  let 〈assembled, costs'〉 ≝ assembly program sigma in
  let code_memory ≝ load_code_memory assembled in
  let data_labels ≝ construct_datalabels (\fst program) in
  let lookup_labels ≝ λx.\fst (sigma (address_of_word_labels_code_mem (\snd program) x)) in  
  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
  let instructions ≝ expand_pseudo_instruction lookup_labels sigma ppc lookup_datalabels pi in
    fetch_many code_memory (\fst (sigma newppc)) (\fst (sigma ppc)) instructions.
  * #preamble #instr_list #sigma #ppc
  @pair_elim #labels #costs #create_label_map_refl
  @pair_elim #assembled #costs' #assembled_refl
  letin code_memory ≝ (load_code_memory ?)
  letin data_labels ≝ (construct_datalabels ?)
  letin lookup_labels ≝ (λx. ?)
  letin lookup_datalabels ≝ (λx. ?)
  @pair_elim #pi #newppc #fetch_pseudo_refl
  lapply (assembly_ok 〈preamble, instr_list〉 sigma assembled costs')
  @pair_elim #labels' #costs' #create_label_map_refl' #H
  cases (H (sym_eq … assembled_refl))
  #_
  lapply (refl … (assembly_1_pseudoinstruction lookup_labels sigma ppc lookup_datalabels pi))
  cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?);
  #len #assembledi #EQ4 #H
  lapply (H ppc) >fetch_pseudo_refl #H
  lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma ppc (load_code_memory assembled))
  >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta
  >fetch_pseudo_refl in H1; #assm @assm assumption
qed.

(* OLD?
definition assembly_specification:
  ∀assembly_program: pseudo_assembly_program.
  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
  λpseudo_assembly_program.
  λcode_mem.
    ∀pc: Word.
      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
      let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
      match pre_assembled with
       [ None ⇒ True
       | Some pc_code ⇒
          let 〈new_pc,code〉 ≝ pc_code in
           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].

axiom assembly_meets_specification:
  ∀pseudo_assembly_program.
    match assembly pseudo_assembly_program with
    [ None ⇒ True
    | Some code_mem_cost ⇒
      let 〈code_mem, cost〉 ≝ code_mem_cost in
        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
    ].
(*
  # PROGRAM
  [ cases PROGRAM
    # PREAMBLE
    # INSTR_LIST
    elim INSTR_LIST
    [ whd
      whd in ⊢ (∀_. %)
      # PC
      whd
    | # INSTR
      # INSTR_LIST_TL
      # H
      whd
      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    ]
  | cases not_implemented
  ] *)
*)

definition internal_pseudo_address_map ≝ list (BitVector 8).

axiom low_internal_ram_of_pseudo_low_internal_ram:
 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.

axiom high_internal_ram_of_pseudo_high_internal_ram:
 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.

axiom low_internal_ram_of_pseudo_internal_ram_hit:
 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀addr:BitVector 7.
  member ? (eq_bv 8) (false:::addr) M = true →
   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram … s) (zero 8) in
   let bl ≝ lookup ? 7 addr ram (zero 8) in
   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
    bu@@bl = \fst (sigma (pbu@@pbl)).

(* changed from add to sub *)
axiom low_internal_ram_of_pseudo_internal_ram_miss:
 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
  let carr ≝ get_index_v ? ? flags 1 ? in
  carr = false →
  member ? (eq_bv 8) (false:::Saddr) M = false →
   member ? (eq_bv 8) (false:::addr) M = false →
    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
  //
qed.

definition addressing_mode_ok ≝
 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm.
  λaddr:addressing_mode.
   match addr with
    [ DIRECT d ⇒
       ¬(member ? (eq_bv 8) d M) ∧
       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
    | INDIRECT i ⇒
       let d ≝ get_register … s [[false;false;i]] in
       ¬(member ? (eq_bv 8) d M) ∧
       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
    | EXT_INDIRECT _ ⇒ true
    | REGISTER _ ⇒ true
    | ACC_A ⇒ true
    | ACC_B ⇒ true
    | DPTR ⇒ true
    | DATA _ ⇒ true
    | DATA16 _ ⇒ true
    | ACC_DPTR ⇒ true
    | ACC_PC ⇒ true
    | EXT_INDIRECT_DPTR ⇒ true
    | INDIRECT_DPTR ⇒ true
    | CARRY ⇒ true
    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
    | RELATIVE _ ⇒ true
    | ADDR11 _ ⇒ true
    | ADDR16 _ ⇒ true ].
    
definition next_internal_pseudo_address_map0 ≝
  λT.
  λfetched.
  λM: internal_pseudo_address_map.
  λcm:T.
  λs: PreStatus T cm.
   match fetched with
    [ Comment _ ⇒ Some ? M
    | Cost _ ⇒ Some … M
    | Jmp _ ⇒ Some … M
    | Call _ ⇒
       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
    | Mov _ _ ⇒ Some … M
    | Instruction instr ⇒
       match instr with
        [ ADD addr1 addr2 ⇒
           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
            Some ? M
           else
            None ?
        | ADDC addr1 addr2 ⇒ 
           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
            Some ? M
           else
            None ?
        | SUBB addr1 addr2 ⇒
           if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
            Some ? M
           else
            None ?        
        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
  

definition next_internal_pseudo_address_map ≝
 λM:internal_pseudo_address_map.
 λcm.
  λs:PseudoStatus cm.
    next_internal_pseudo_address_map0 ?
     (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s))) M cm s.

definition code_memory_of_pseudo_assembly_program:
 ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16
≝ λpap,sigma.
   let p ≝ assembly pap sigma in
    load_code_memory (\fst p).

definition status_of_pseudo_status:
 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool.
  Status (code_memory_of_pseudo_assembly_program pap sigma) ≝
 λM,pap,ps,sigma.
  let cm ≝ code_memory_of_pseudo_assembly_program … sigma in
  let pc ≝ \fst (sigma (program_counter … ps)) in
  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     mk_PreStatus (BitVectorTrie Byte 16)
      cm
      lir
      hir
      (external_ram … ps)
      pc
      (special_function_registers_8051 … ps)
      (special_function_registers_8052 … ps)
      (p1_latch … ps)
      (p3_latch … ps)
      (clock … ps).

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

definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
≝
  λ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
  let s ≝ set_clock ? s (clock ? s + ticks) in
  let s ≝ set_program_counter ? s pc in
    match instr with
    [ Instruction instr ⇒
       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    | Comment cmt ⇒ s
    | Cost cst ⇒ s
    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    | Call call ⇒
      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 ⇒
       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    ].
 [
 |2,3,4: %
 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
 |
 | %
 ]
 cases not_implemented
qed.
*)

(*
lemma execute_code_memory_unchanged:
 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
 #ticks #ps whd in ⊢ (??? (??%))
 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
  (program_counter pseudo_assembly_program ps)) #instr #pc
 whd in ⊢ (??? (??%)) cases instr
  [ #pre cases pre
     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
       [ #x1 whd in ⊢ (??? (??%)) 
     | *: cases not_implemented
     ]
  | #comment %
  | #cost %
  | #label %
  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    (* CSC: ??? *)
  | #dptr #label (* CSC: ??? *)
  ]
  cases not_implemented
qed.
*)

(* DEAD CODE?
lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
 ∀M:internal_pseudo_address_map.
 ∀ps,ps': PseudoStatus.
 ∀pol.
  ∀prf:code_memory … ps = code_memory … ps'.
   let pol' ≝ ? in
   match status_of_pseudo_status M ps pol with
    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
    ].
 [2: <prf @pol]
 #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 generalize in match (refl … (assembly (code_memory … ps) pol))
 cases (assembly ??) in ⊢ (???% → %)
  [ #K whd whd in ⊢ (??%?) <H >K %
  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
qed.
*)

definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝
  λprogram: pseudo_assembly_program.λsigma.
  λppc: Word.
  λfetched. ?.
cases daemon(*
    match fetched with
    [ Instruction instr ⇒
      match instr with
      [ JC lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNC lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JB bit lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNB bit lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JBC bit lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JZ lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | JNZ lbl ⇒
        match pol lookup_labels  ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | CJNE arg lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | DJNZ arg lbl ⇒
        match pol lookup_labels ppc with
        [ short_jump ⇒ 〈2, 2〉
        | medium_jump ⇒ ?
        | long_jump ⇒ 〈4, 4〉
        ]
      | ADD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in
         〈ticks, ticks〉
      | ADDC arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (ADDC ? arg1 arg2) in
         〈ticks, ticks〉
      | SUBB arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (SUBB ? arg1 arg2) in
         〈ticks, ticks〉
      | INC arg ⇒ 
        let ticks ≝ ticks_of_instruction (INC ? arg) in
         〈ticks, ticks〉
      | DEC arg ⇒ 
        let ticks ≝ ticks_of_instruction (DEC ? arg) in
         〈ticks, ticks〉
      | MUL arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (MUL ? arg1 arg2) in
         〈ticks, ticks〉
      | DIV arg1 arg2 ⇒ 
        let ticks ≝ ticks_of_instruction (DIV ? arg1 arg2) in
         〈ticks, ticks〉
      | DA arg ⇒ 
        let ticks ≝ ticks_of_instruction (DA ? arg) in
         〈ticks, ticks〉
      | ANL arg ⇒
        let ticks ≝ ticks_of_instruction (ANL ? arg) in
         〈ticks, ticks〉
      | ORL arg ⇒
        let ticks ≝ ticks_of_instruction (ORL ? arg) in
         〈ticks, ticks〉
      | XRL arg ⇒
        let ticks ≝ ticks_of_instruction (XRL ? arg) in
         〈ticks, ticks〉
      | CLR arg ⇒
        let ticks ≝ ticks_of_instruction (CLR ? arg) in
         〈ticks, ticks〉
      | CPL arg ⇒
        let ticks ≝ ticks_of_instruction (CPL ? arg) in
         〈ticks, ticks〉
      | RL arg ⇒
        let ticks ≝ ticks_of_instruction (RL ? arg) in
         〈ticks, ticks〉
      | RLC arg ⇒
        let ticks ≝ ticks_of_instruction (RLC ? arg) in
         〈ticks, ticks〉
      | RR arg ⇒
        let ticks ≝ ticks_of_instruction (RR ? arg) in
         〈ticks, ticks〉
      | RRC arg ⇒
        let ticks ≝ ticks_of_instruction (RRC ? arg) in
         〈ticks, ticks〉
      | SWAP arg ⇒
        let ticks ≝ ticks_of_instruction (SWAP ? arg) in
         〈ticks, ticks〉
      | MOV arg ⇒
        let ticks ≝ ticks_of_instruction (MOV ? arg) in
         〈ticks, ticks〉
      | MOVX arg ⇒
        let ticks ≝ ticks_of_instruction (MOVX ? arg) in
         〈ticks, ticks〉
      | SETB arg ⇒
        let ticks ≝ ticks_of_instruction (SETB ? arg) in
         〈ticks, ticks〉
      | PUSH arg ⇒
        let ticks ≝ ticks_of_instruction (PUSH ? arg) in
         〈ticks, ticks〉
      | POP arg ⇒
        let ticks ≝ ticks_of_instruction (POP ? arg) in
         〈ticks, ticks〉
      | XCH arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCH ? arg1 arg2) in
         〈ticks, ticks〉
      | XCHD arg1 arg2 ⇒
        let ticks ≝ ticks_of_instruction (XCHD ? arg1 arg2) in
         〈ticks, ticks〉
      | RET ⇒
        let ticks ≝ ticks_of_instruction (RET ?) in
         〈ticks, ticks〉
      | RETI ⇒
        let ticks ≝ ticks_of_instruction (RETI ?) in
         〈ticks, ticks〉
      | NOP ⇒
        let ticks ≝ ticks_of_instruction (NOP ?) in
         〈ticks, ticks〉
      ]
    | Comment comment ⇒ 〈0, 0〉
    | Cost cost ⇒ 〈0, 0〉
    | Jmp jmp ⇒ 〈2, 2〉
    | Call call ⇒ 〈2, 2〉
    | Mov dptr tgt ⇒ 〈2, 2〉
    ].
  cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *)
*)qed.

definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝
  λprogram: pseudo_assembly_program.λsigma.
  λppc: Word.
    let 〈preamble, pseudo〉 ≝ program in
    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
     ticks_of0 program sigma ppc fetched.

lemma eq_rect_Type1_r:
  ∀A: Type[1].
  ∀a:A.
  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
  #A #a #P #H #x #p
  generalize in match H;
  generalize in match P;
  cases p
  //
qed.

axiom split_append:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v, v': Vector A m.
  ∀q, q': Vector A n.
    let 〈v', q'〉 ≝ split A m n (v@@q) in
      v = v' ∧ q = q'.

axiom split_vector_singleton:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A (S n).
  ∀rest: Vector A n.
  ∀s: Vector A 1.
  ∀prf.
    v = s @@ rest →
    ((get_index_v A ? v 0 prf) ::: rest) = v.

example sub_minus_one_seven_eight:
  ∀v: BitVector 7.
  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
 cases daemon.
qed.

(*
lemma blah:
  ∀m: internal_pseudo_address_map.
  ∀s: PseudoStatus.
  ∀arg: Byte.
  ∀b: bool.
    addressing_mode_ok m s (DIRECT arg) = true →
      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
      get_arg_8 ? s b (DIRECT arg).
  [2, 3: normalize % ]
  #m #s #arg #b #hyp
  whd in ⊢ (??%%)
  @split_elim''
  #nu' #nl' #arg_nu_nl_eq
  normalize nodelta
  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
  #get_index_v_eq
  normalize nodelta
  [2:
    normalize nodelta
    @split_elim''
    #bit_one' #three_bits' #bit_one_three_bit_eq
    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
    normalize nodelta
    generalize in match (refl ? (sub_7_with_carry ? ? ?))
    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
    #Saddr #carr' #Saddr_carr_eq
    normalize nodelta
    #carr_hyp'
    @carr_hyp'
    [1:
    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
        generalize in match (refl ? (¬(member (BitVector 8) ? arg m))) 
        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
        #member_eq
        normalize nodelta
        [2: #destr destruct(destr)
        |1: -carr_hyp';
            >arg_nu_nl_eq
            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
            [1: >get_index_v_eq in ⊢ (??%? → ?)
            |2: @le_S @le_S @le_S @le_n
            ]
            cases (member (BitVector 8) ? (\fst ?) ?)
            [1: #destr normalize in destr; destruct(destr)
            |2:
            ]
        ]
    |3: >get_index_v_eq in ⊢ (??%?)
        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
        >(split_vector_singleton … bit_one_three_bit_eq)
        <arg_nu_nl_eq
        whd in hyp:(??%?)
        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
        normalize nodelta [*: #ignore @sym_eq ]
    ]
  |
  ].
*)
(*
map_address0 ... (DIRECT arg) = Some .. →
  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
  get_arg_8 (internal_ram ...) (DIRECT arg)

((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
                     then Some internal_pseudo_address_map M 
                     else None internal_pseudo_address_map )
                    =Some internal_pseudo_address_map M')
*)

axiom low_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
  sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
  bu@@bl = \fst (sigma (pbu@@pbl)) →
   low_internal_ram T1 cm1
     (write_at_stack_pointer …
       (set_8051_sfr …
         (write_at_stack_pointer …
           (set_8051_sfr …
             (set_low_internal_ram … s1
               (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = low_internal_ram_of_pseudo_low_internal_ram (sp1::M)
      (low_internal_ram …
       (write_at_stack_pointer …
         (set_8051_sfr …
           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).

axiom high_internal_ram_write_at_stack_pointer:
 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.
  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
  sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
  sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
  bu@@bl = \fst (sigma (pbu@@pbl)) →
   high_internal_ram T1 cm1
     (write_at_stack_pointer …
       (set_8051_sfr …
         (write_at_stack_pointer …
           (set_8051_sfr …
             (set_high_internal_ram … s1
               (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2)))
             SFR_SP sp1)
          bl)
        SFR_SP sp2)
      bu)
   = high_internal_ram_of_pseudo_high_internal_ram (sp1::M)
      (high_internal_ram …
       (write_at_stack_pointer …
         (set_8051_sfr …
           (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl)
          SFR_SP sp2)
        pbu)).

lemma Some_Some_elim:
 ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P.
 #T #x #y #P #H #K @H @option_destruct_Some // 
qed.

(*CSC: ???*)
axiom snd_assembly_1_pseudoinstruction_ok:
 ∀program:pseudo_assembly_program.∀sigma.
 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
  lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) →
  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels  pi) in
    \fst (sigma (add … ppc (bitvector_of_nat ? 1))) =
     add … (\fst (sigma ppc)) (bitvector_of_nat ? len).

lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
 /2/
qed.

(* To be moved in ProofStatus *)
lemma program_counter_set_program_counter:
 ∀T,cm,s,x. program_counter T cm (set_program_counter T cm s x) = x.
 //
qed.

theorem main_thm:
 ∀M,M',cm,ps,sigma.
  next_internal_pseudo_address_map M cm ps = Some … M' →
   ∃n.
      execute n … (status_of_pseudo_status M … ps sigma)
    = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma.
 #M #M' * #preamble #instr_list #ps #sigma
 change with (next_internal_pseudo_address_map0 ????? = ? → ?)
 @(pose … (program_counter ?? ps)) #ppc #EQppc
 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?;
 @pair_elim #labels #costs #H0 normalize nodelta
 @pair_elim #assembled #costs' #EQ1 normalize nodelta
 @pair_elim #pi #newppc #EQ2 normalize nodelta
 @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels
 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
 whd in match execute_1_pseudo_instruction; normalize nodelta
 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?)
 [>EQ2 %]
 inversion pi
  [2,3: (* Comment, Cost *) #ARG #EQ
   #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ?????) in H3;
   whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
   whd in match (execute_1_pseudo_instruction0 ?????);
   %{0} @split_eq_status CSC:STOP HERE //
  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
         @pair_elim' * #instr #newppc' #ticks #EQ4       
         * * #H2a #H2b whd in ⊢ (% → ?) #H2
         >H2b >(eq_instruction_to_eq … H2a)
         #EQ %[@1]
         <MAP >(eq_bv_eq … H2) >EQ
         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
         whd in ⊢ (??%?)
         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
  |6: (* Mov *) #arg1 #arg2
       #H1 #H2 #EQ %[@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
       normalize nodelta;
       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
       #result #flags
       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
  |5: (* Call *) #label #MAP
      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
       [ (* short *) #abs @⊥ destruct (abs)
       |3: (* long *) #H1 #H2 #EQ %[@1]
           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ??%?);
           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
           >(eq_bv_eq … H2c)
           change with
            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           @split_eq_status;
            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
              >code_memory_write_at_stack_pointer %
            | >set_program_counter_set_low_internal_ram
              >set_clock_set_low_internal_ram
              @low_internal_ram_write_at_stack_pointer
               [ >EQ0 @pol | % | %
               | @(pair_destruct_2 … EQ1)
               | @(pair_destruct_2 … EQ2)
               | >(pair_destruct_1 ????? EQpc)
                 >(pair_destruct_2 ????? EQpc)
                 @split_elim #x #y #H <H -x y H;
                 >(pair_destruct_1 ????? EQppc)
                 >(pair_destruct_2 ????? EQppc)
                 @split_elim #x #y #H <H -x y H;
                 >EQ0 % ]
            | >set_low_internal_ram_set_high_internal_ram
              >set_program_counter_set_high_internal_ram
              >set_clock_set_high_internal_ram
              @high_internal_ram_write_at_stack_pointer
               [ >EQ0 @pol | % | %
               | @(pair_destruct_2 … EQ1)
               | @(pair_destruct_2 … EQ2)
               | >(pair_destruct_1 ????? EQpc)
                 >(pair_destruct_2 ????? EQpc)
                 @split_elim #x #y #H <H -x y H;
                 >(pair_destruct_1 ????? EQppc)
                 >(pair_destruct_2 ????? EQppc)
                 @split_elim #x #y #H <H -x y H;
                 >EQ0 % ]            
            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
              >external_ram_write_at_stack_pointer %
            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
              >EQ0 % 
            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8051_write_at_stack_pointer %
            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
              >special_function_registers_8052_write_at_stack_pointer %
            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p1_latch_write_at_stack_pointer %
            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
              >p3_latch_write_at_stack_pointer %
            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
              >clock_write_at_stack_pointer whd in ⊢ (???%)
              >clock_write_at_stack_pointer whd in ⊢ (???%)
              >clock_write_at_stack_pointer %]
       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
         @pair_elim' #fst_5_addr #rest_addr #EQ1
         @pair_elim' #fst_5_pc #rest_pc #EQ2
         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
         change in ⊢ (? →??%?) with (execute_1_0 ??)
         @pair_elim' * #instr #newppc' #ticks #EQn
          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
          >get_8051_sfr_set_8051_sfr
          
          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
           generalize in match (refl … (split bool 4 4 pc_bu))
           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
           generalize in match (refl … (split bool 3 8 rest_addr))
           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
           generalize in match
            (refl …
             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
           @split_eq_status try %
            [ change with (? = sigma ? (address_of_word_labels ps label))
              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
  |4: (* Jmp *) #label #MAP
      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
       [3: (* long *) #H1 #H2 #EQ %[@1]
           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
           generalize in match
            (refl ?
             (sub_16_with_carry
              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
              false))
           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
           change in ⊢ (? → ??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ?);
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
         generalize in match
          (refl …
            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
         generalize in match
          (refl …
            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
         change in ⊢ (? →??%?) with (execute_1_0 ??)
           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
           >H2b >(eq_instruction_to_eq … H2a)
           generalize in match EQ; -EQ;
           whd in ⊢ (???% → ?);
           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
           generalize in match (refl … (split bool 4 4 pc_bu))
           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
           generalize in match (refl … (split bool 3 8 rest_addr))
           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
           generalize in match
            (refl …
             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7    
           @split_eq_status try %
            [ change with (? = sigma ?? (address_of_word_labels ps label))
              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
       normalize nodelta; #MAP;
       [1: change in ⊢ (? → %) with
        ((let 〈result,flags〉 ≝
          add_8_with_carry
           (get_arg_8 ? ps false ACC_A)
           (get_arg_8 ?
             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
             false (DIRECT ARG2))
           ? in ?) = ?)
        [2,3: %]
        change in ⊢ (???% → ?) with
         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
        >get_arg_8_set_clock
       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
         [2,4: #abs @⊥ normalize in abs; destruct (abs)
         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
       [ change in ⊢ (? → %) with
        ((let 〈result,flags〉 ≝
          add_8_with_carry
           (get_arg_8 ? ps false ACC_A)
           (get_arg_8 ?
             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
             false (DIRECT ARG2))
           ? in ?) = ?)
          >get_arg_8_set_low_internal_ram
       
        cases (add_8_with_carry ???)
         
        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
       #result #flags
       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
       change in ⊢ (? → ??%?) with (execute_1_0 ??)
       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
       >H2b >(eq_instruction_to_eq … H2a)
       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
       [1,2,3,4: cases (half_add ???) #carry #result
       | cases (half_add ???) #carry #bl normalize nodelta;
         cases (full_add ????) #carry' #bu normalize nodelta ]
        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
        [5: %
        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
      (set_program_counter pseudo_assembly_program ps newppc)
      (\fst  (ticks_of0 〈preamble,instr_list〉
                   (program_counter pseudo_assembly_program ps)
                   (Instruction (INC Identifier (DIRECT ARG))))
       +clock pseudo_assembly_program
        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
        [2,3: // ]
            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
            whd in ⊢ (??%%)
            cases (split bool 4 4 ARG)
            #nu' #nl'
            normalize nodelta
            cases (split bool 1 3 nu')
            #bit_1' #ignore'
            normalize nodelta
            cases (get_index_v bool 4 nu' ? ?)
            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
            |
            ]
cases daemon (* EASY CASES TO BE COMPLETED *)
qed.