include "ASM/Assembly.ma".
include "ASM/Interpret.ma".

(* RUSSEL **)

include "basics/jmeq.ma".

notation > "hvbox(a break ≃ b)"
  non associative with precedence 45
for @{ 'jmeq ? $a ? $b }.

notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
  non associative with precedence 45
for @{ 'jmeq $t $a $u $b }.

interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).

lemma eq_to_jmeq:
  ∀A: Type[0].
  ∀x, y: A.
    x = y → x ≃ y.
  //
qed.

definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].

coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.

axiom VOID: Type[0].
axiom assert_false: VOID.
definition bigbang: ∀A:Type[0].False → VOID → A.
 #A #abs cases abs
qed.

coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.

lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
 #A #P #p cases p #w #q @q
qed.

lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
qed.

coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.

(* END RUSSELL **)

let rec foldl_strong_internal
  (A: Type[0]) (P: list A → Type[0]) (l: list A)
  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
    l = prefix @ suffix → P(prefix @ suffix) ≝
  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
  [ nil ⇒ λprf. ?
  | cons hd tl ⇒ λprf. ?
  ].
  [ > (append_nil ?)
    @ acc
  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
    [ @ (H prefix hd tl prf acc)
    | applyS prf
    ]
  ]
qed.

definition foldl_strong ≝
  λA: Type[0].
  λP: list A → Type[0].
  λl: list A.
  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
  λacc: P [ ].
    foldl_strong_internal A P l H [ ] l acc (refl …).

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' ? ?)
  ].
  [ applyS prefix
  | letin res ≝ (bit ::: prefix)
    < (minus_S_S ? ?)
    > (minus_Sn_m ? ?)
    [ @ res
    | @ prf2
    ]
  | /2/
  ].
qed.

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

axiom 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)).
        
lemma vector_cons_append:
  ∀A: Type[0].
  ∀n: nat.
  ∀e: A.
  ∀v: Vector A n.
    e ::: v = [[ e ]] @@ v.
  # A # N # E # V
  elim V
  [ normalize %
  | # NN # AA # VV # IH
    normalize
    % 
  ]
qed.

lemma super_rewrite2:
 ∀A:Type[0].∀n,m.∀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 <EQ in v2; #V #JMEQ >JMEQ //
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
  [ normalize
    > (REFLEX A)
    normalize
    # H
    %
  | # NN # AA # PP # IH
    normalize
    cases (EQ A AA) //
     @ IH
  ]
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
  [ #R #H @H
  | #NN #AA # PP # IH #R #H
    normalize
    cases (EQ A AA)
    [ normalize %
    | @ IH @ H
    ]
  ]
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
  [ normalize
    # M # V %
  | # NN # AA # VV # IH # MM # QQ
    change with (bool_to_Prop (andb ??))
    cut ((mem A EQ (O + (MM + S NN)) (H@@QQ@@AA:::VV) AA) = true)
    [ 
    | # HH > HH
      > (vector_cons_append ? ? AA VV)
      change with (bool_to_Prop (subvector_with ??????))
      @(super_rewrite2 A ((MM + 1)+ NN) (MM+S NN) ??
        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
        ?
        (vector_associative_append A ? ? ? QQ [[AA]] VV))
      [ >associative_plus //
      | @IH ]
    ]
    @(mem_monotonic_wrt_append)
    [ @ REFLEX
    | @(mem_monotonic_wrt_append)
      [ @ REFLEX
      | normalize
        > REFLEX
        normalize
        %
      ]
    ]
qed.

lemma vector_cons_empty:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
    [[ ]] @@ v = v.
  # A # N # V
  elim V
  [ normalize %
  | # NN # HH # VV #H %
  ]
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 A ? H V)
  < (vector_cons_empty A ? ([[H]] @@ V))
  @ (subvector_multiple_append A ? ? 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
  # H
  elim Q
  [ normalize
    @ H
  | # NN # PP # QQ # IH
    normalize
    cases (is_a PP TO_SEARCH)
    [ normalize
      %
    | normalize
      normalize in IH
      @ IH
    ]
  ]
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
  [ # H
    normalize in H;
    cases H
  | # NN # HHD # VV # IH # HH
    > vector_cons_append
    > (vector_cons_append ? ? HHD VV)
    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
    @ HH
  ]
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); @tl
  | cases prf in tl H; #tl
    normalize in ⊢ (∀_: %. ?)
    # H
    whd
    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
qed.

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

axiom union_elim:
  ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool.

(*
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. P (DJNZ ? ? addr)) ∧
    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 ?) ∧
    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))).
    
    
    
    
    
    list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)).

    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧
    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧
    P (RET ?) ∧
    P (RETI ?) ∧
    P (NOP ?).
  

axiom instruction_elim: ∀P: instruction → bool. bool.
  
 
lemma instruction_elim_correct:
  ∀i: instruction.
  ∀P: instruction → bool.
    instruction_elim P = true → ∀j. P j = true.
  
lemma test:
  ∀i: instruction.
  ∃pc.
  let assembled ≝ assembly1 i in
  let code_memory ≝ load_code_memory assembled in
  let fetched ≝ fetch code_memory pc in
  let 〈instr_pc, ticks〉 ≝ fetched in
    \fst instr_pc = i.
  # INSTR
  @ (ex_intro ?)
  [ @ (zero 16)
  | @ (instruction_elim INSTR)
  ].
*)
 
(* This establishes the correspondence between pseudo program counters and
   program counters. It is at the heart of the proof. *)
(*CSC: code taken from build_maps *)
definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16))) ≝
 λinstr_list.
  foldl ??
    (λt. λi.
       match t with
       [ None ⇒ None ?
       | Some ppc_pc_map ⇒
         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
         let 〈program_counter, sigma_map〉 ≝ pc_map in
         let 〈label, i〉 ≝ i in
          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
           [ None ⇒ None ?
           | Some pc_ignore ⇒
              let 〈pc,ignore〉 ≝ pc_ignore in
              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (\snd instr_list).
       
definition tech_pc_sigma0: pseudo_assembly_program → option (nat × (BitVectorTrie Word 16)) ≝
 λinstr_list.
  match sigma0 instr_list with
   [ None ⇒ None …
   | Some result ⇒
      let 〈ppc,pc_sigma_map〉 ≝ result in
       Some … pc_sigma_map ].

definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝       
 λinstr_list.
  match sigma0 instr_list with
  [ None ⇒ None ?
  | Some result ⇒
    let 〈ppc,pc_sigma_map〉 ≝ result in
    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
      if gtb pc (2^16) then
        None ?
      else
        Some ? (λx.lookup ?? x sigma_map (zero …)) ].

axiom policy_ok: ∀p. sigma_safe p ≠ None ….

definition sigma: pseudo_assembly_program → Word → Word ≝
 λp.
  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
   [ None ⇒ λabs. ⊥
   | Some r ⇒ λ_.r] (policy_ok p).
 cases abs //
qed.

lemma length_append:
 ∀A.∀l1,l2:list A.
  |l1 @ l2| = |l1| + |l2|.
 #A #l1 elim l1
  [ //
  | #hd #tl #IH #l2 normalize <IH //]
qed.

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

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

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

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

coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 

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

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

axiom tech_pc_sigma0_append:
 ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.

axiom tech_pc_sigma0_append_None:
 ∀preamble,instr_list,prefix,i,pc,costs.
  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
    → False.

lemma BitVectorTrie_O:
 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
  [ #w #_ %1 %[@w] %
  | #n #l #r #abs @⊥ //
  | #n #EQ %2 >EQ %]
qed.

lemma BitVectorTrie_Sn:
 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
  [ #m #abs @⊥ //
  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
  | #m #EQ %2 // ]
qed.

lemma lookup_prepare_trie_for_insertion_hit:
 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
  lookup … b (prepare_trie_for_insertion … b v) a = v. 
 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
qed.
 
lemma lookup_insert_hit:
 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
  lookup … b (insert … b v t) a = v.
 #A #a #v #n #b elim b -b -n //
 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
qed.

lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
 #n #hd #tl #abs @⊥ //
qed.

lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
 ∃hd.∃tl.v ≃ VCons bool n hd tl.
 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
 [ #abs @⊥ //
 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
qed.

lemma lookup_prepare_trie_for_insertion_miss:
 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
 #A #a #v #n #c elim c
  [ #b >(BitVector_O … b) normalize #abs @⊥ //
  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    cases hd cases hd' normalize
    [2,3: #_ cases tl' //
    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
qed.
  
lemma lookup_insert_miss:
 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
 #A #a #v #n #c elim c -c -n
  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    #t cases(BitVectorTrie_Sn … t)
    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
qed.

definition build_maps' ≝
  λpseudo_program.
  let 〈preamble,instr_list〉 ≝ pseudo_program in
  let result ≝
   foldl_strong
    (option Identifier × pseudo_instruction)
    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
      let pre' ≝ 〈preamble,pre〉 in
      let 〈labels,pc_costs〉 ≝ res in
       tech_pc_sigma0 pre' = Some … pc_costs ∧
       ∀id. occurs_exactly_once id pre →
        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
    instr_list
    (λprefix,i,tl,prf,t.
      let 〈labels, pc_costs〉 ≝ t in
      let 〈program_counter, costs〉 ≝ pc_costs in
       let 〈label, i'〉 ≝ i in
       let labels ≝
         match label with
         [ None ⇒ labels
         | Some label ⇒
           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
             insert ? ? label program_counter_bv labels
         ]
       in
         match construct_costs 〈preamble,instr_list〉 program_counter (λx. zero ?) (λx. zero ?) costs i' with
         [ None ⇒
            let dummy ≝ 〈labels,pc_costs〉 in
             dummy
         | Some construct ⇒ 〈labels, construct〉
         ]
    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉
  in
   let 〈labels, pc_costs〉 ≝ result in
   let 〈pc, costs〉 ≝ pc_costs in
    〈labels, costs〉.
 [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
 | whd cases construct in p3 #PC #CODE #JMEQ %
    [ @(tech_pc_sigma0_append ??????????? (jmeq_to_eq ??? JMEQ)) | #id #Hid ]
 | (* dummy case *) @⊥
   @(tech_pc_sigma0_append_None ?? prefix ???? (jmeq_to_eq ??? p3)) ]
 [*: generalize in match (sig2 … t) whd in ⊢ (% → ?)
     >p whd in ⊢ (% → ?) >p1 * #IH0 #IH1 >IH0 // ]
 whd in ⊢ (??(????%?)?) -labels1;
 cases label in Hid
  [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
     [ >(address_of_word_labels_code_mem_None … Hid)
       (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
     | whd in Hid >occurs_exactly_once_None in Hid // ]
  | -label #label #Hid whd in ⊢ (??(????%?)?)
   
  ]
qed.

(*
(*
notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
 with precedence 10
for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
*)

lemma build_maps_ok:
 ∀p:pseudo_assembly_program.
  let 〈labels,costs〉 ≝ build_maps' p in
   ∀pc.
    (nat_of_bitvector … pc) < length … (\snd p) →
     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
 #p cases p #preamble #instr_list
  elim instr_list
   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
   | #hd #tl #IH 
    whd in ⊢ (match % with [ _ ⇒ ?])
   ]
qed.
*)

(*
lemma list_elim_rev:
 ∀A:Type[0].∀P:list A → Prop.
  P [ ] → (∀n,l. length l = n → P l →  
  P [ ] → (∀l,a. P l → P (l@[a])) →
   ∀l. P l.
 #A #P
qed.*)

lemma rev_preserves_length:
 ∀A.∀l. length … (rev A l) = length … l.
  #A #l elim l
   [ %
   | #hd #tl #IH normalize >length_append normalize /2/ ]
qed.

lemma rev_append:
 ∀A.∀l1,l2.
  rev A (l1@l2) = rev A l2 @ rev A l1.
 #A #l1 elim l1 normalize //
qed.
  
lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
 #A #l elim l
  [ //
  | #hd #tl #IH normalize >rev_append normalize // ]
qed.

lemma split_len_Sn:
 ∀A:Type[0].∀l:list A.∀len.
  length … l = S len →
   Σl'.Σa. l = l'@[a] ∧ length … l' = len.
 #A #l elim l
  [ normalize #len #abs destruct
  | #hd #tl #IH #len
    generalize in match (rev_rev … tl)
    cases (rev A tl) in ⊢ (??%? → ?)
     [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/  
     | #a #l' #H <H normalize #EQ 
      %[@(hd::rev … l')] %[@a] % //
      >length_append in EQ #EQ normalize in EQ; normalize;
      generalize in match (injective_S … EQ) #EQ2 /2/ ]]
qed.

lemma list_elim_rev:
 ∀A:Type[0].∀P:list A → Type[0].
  P [ ] → (∀l,a. P l → P (l@[a])) →
   ∀l. P l.
 #A #P #H1 #H2 #l
 generalize in match (refl … (length … l))
 generalize in ⊢ (???% → ?) #n generalize in match l
 elim n
  [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
  | #m #IH #L #EQ
    cases (split_len_Sn … EQ) #l' * #a * /3/ ]
qed.

axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
axiom prefix_of_append:
 ∀A:Type[0].∀l,l1,l2:list A.
  is_prefix … l l1 → is_prefix … l (l1@l2).
axiom prefix_reflexive: ∀A,l. is_prefix A l l.
axiom nil_prefix: ∀A,l. is_prefix A [ ] l.

record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.

definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].

definition app ≝
 λA:Type[0].λl1:Propify (list A).λl2:list A.
  match l1 with
   [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].

lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
 #A * /3/
qed.

lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
 #A * #l1 normalize //
qed. 

let rec foldli (A: Type[0]) (B: Propify (list A) → Type[0])
 (f: ∀prefix. B prefix → ∀x.B (app … prefix [x]))
 (prefix: Propify (list A)) (b: B prefix) (l: list A) on l :
 B (app … prefix l) ≝
  match l with
  [ nil ⇒ ? (* b *)
  | cons hd tl ⇒ ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
  ].
 [ applyS b
 | <(app_assoc ?? [hd]) @(foldli A B f (app … prefix [hd]) (f prefix b hd) tl) ]
qed.

(*
let rec foldli (A: Type[0]) (B: list A → Type[0]) (f: ∀prefix. B prefix → ∀x. B (prefix@[x]))
 (prefix: list A) (b: B prefix) (l: list A) on l : B (prefix@l) ≝
  match l with
  [ nil ⇒ ? (* b *)
  | cons hd tl ⇒
     ? (*foldli A B f (prefix@[hd]) (f prefix b hd) tl*)
  ].
 [ applyS b
 | applyS (foldli A B f (prefix@[hd]) (f prefix b hd) tl) ]
qed.
*)

definition foldll:
 ∀A:Type[0].∀B: Propify (list A) → Type[0].
  (∀prefix. B prefix → ∀x. B (app … prefix [x])) →
   B (mk_Propify … []) → ∀l: list A. B (mk_Propify … l)
 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).

axiom is_pprefix: ∀A:Type[0]. Propify (list A) → list A → Prop.
axiom pprefix_of_append:
 ∀A:Type[0].∀l,l1,l2.
  is_pprefix A l l1 → is_pprefix A l (l1@l2).
axiom pprefix_reflexive: ∀A,l. is_pprefix A (mk_Propify … l) l.
axiom nil_pprefix: ∀A,l. is_pprefix A (mk_Propify … [ ]) l.


axiom foldll':
 ∀A:Type[0].∀l: list A.
  ∀B: ∀prefix:Propify (list A). is_pprefix ? prefix l → Type[0].
  (∀prefix,proof. B prefix proof → ∀x,proof'. B (app … prefix [x]) proof') →
   B (mk_Propify … [ ]) (nil_pprefix …) → B (mk_Propify … l) (pprefix_reflexive … l).
 #A #l #B
 generalize in match (foldll A (λprefix. is_pprefix ? prefix l)) #HH
 
 
  #H #acc
 @foldll
  [
  |
  ]
 
 ≝ λA,B,f. foldli A B f (mk_Propify … [ ]).


(*
record subset (A:Type[0]) (P: A → Prop): Type[0] ≝
 { subset_wit:> A;
   subset_proof: P subset_wit
 }.
*)

definition build_maps' ≝
  λpseudo_program.
  let 〈preamble,instr_list〉 ≝ pseudo_program in
  let result ≝
   foldll
    (option Identifier × pseudo_instruction)
    (λprefix.
      Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
       match prefix return λ_.Prop with [mk_Propify prefix ⇒ tech_pc_sigma0 〈preamble,prefix〉 ≠ None ?])
    (λprefix,t,i.
      let 〈labels, pc_costs〉 ≝ t in
      let 〈program_counter, costs〉 ≝ pc_costs in
       let 〈label, i'〉 ≝ i in
       let labels ≝
         match label with
         [ None ⇒ labels
         | Some label ⇒
           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
             insert ? ? label program_counter_bv labels
         ]
       in
         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
         [ None ⇒
            let dummy ≝ 〈labels,pc_costs〉 in
              dummy
         | Some construct ⇒ 〈labels, construct〉
         ]
    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list
  in
   let 〈labels, pc_costs〉 ≝ result in
   let 〈pc, costs〉 ≝ pc_costs in
    〈labels, costs〉.
 [
 | @⊥ 
 | normalize % // 
 ]
qed.

definition build_maps' ≝
  λpseudo_program.
  let 〈preamble,instr_list〉 ≝ pseudo_program in
  let result ≝
   foldl
    (Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)))
    (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
           is_prefix ? instr_list_prefix' instr_list →
           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)
    (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))).
          ∃instr_list_prefix. is_prefix ? instr_list_prefix instr_list ∧
           tech_pc_sigma0 〈preamble,instr_list_prefix〉 = Some ? (\fst (\snd t)).
     λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
           is_prefix ? instr_list_prefix' instr_list →
           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? .
      let 〈labels, pc_costs〉 ≝ t in
      let 〈program_counter, costs〉 ≝ pc_costs in
       let 〈label, i'〉 ≝ i in
       let labels ≝
         match label with
         [ None ⇒ labels
         | Some label ⇒
           let program_counter_bv ≝ bitvector_of_nat ? program_counter in
             insert ? ? label program_counter_bv labels
         ]
       in
         match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with
         [ None ⇒
            let dummy ≝ 〈labels,pc_costs〉 in
              dummy
         | Some construct ⇒ 〈labels, construct〉
         ]
    ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*)
  in
   let 〈labels, pc_costs〉 ≝ result in
   let 〈pc, costs〉 ≝ pc_costs in
    〈labels, costs〉.
 [4: @(list_elim_rev ?
       (λinstr_list. list (
        (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix.
          let instr_list_prefix' ≝ instr_list_prefix @ [i] in
           is_prefix ? instr_list_prefix' instr_list →
           tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?)))
       ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *)
      [ @[ ]
      | #l' #a #limage %2
        [ %[@a] #PREFIX #PREFIX_OK 
        | (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN
             THE INDUCTION HYPOTHESIS INSTEAD *)
          elim limage
           [ %1
           | #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3
             @K1 @(prefix_of_append ???? K3)
           ]  
        ] 
        
       
     
 
  cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt'
     % [@ (LIST_PREFIX @ [i])] %
      [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1
      | (* DOABLE IN PRINCIPLE *)
      ]
 | (* assert false case *)
 |3: % [@ ([ ])] % [2: % | (* DOABLE *)]
 |   

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

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 status_of_pseudo_status: PseudoStatus → option Status ≝
 λps.
  let pap ≝ code_memory … ps in
   match assembly pap with
    [ None ⇒ None …
    | Some p ⇒
       let cm ≝ load_code_memory (\fst p) in
       let pc ≝ sigma' pap (program_counter ? ps) in
        Some …
         (mk_PreStatus (BitVectorTrie Byte 16)
           cm
           (low_internal_ram … ps)
           (high_internal_ram … ps)
           (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.
*)

lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
 ∀ps,ps': PseudoStatus.
  code_memory … ps = code_memory … ps' →
   match status_of_pseudo_status ps with
    [ None ⇒ status_of_pseudo_status ps' = None …
    | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
    ].
 #ps #ps' #H whd in ⊢ (mat
 ch % with [ _ ⇒ ? | _ ⇒ ? ])
 generalize in match (refl … (assembly (code_memory … ps)))
 cases (assembly ?) in ⊢ (???% → %)
  [ #K whd whd in ⊢ (??%?) <H >K %
  | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
qed.*)

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

(* prove later *)
axiom test:
  ∀pc: Word.
  ∀code_memory: BitVectorTrie Byte 16.
  ∀i: instruction.
    let assembled ≝ assembly1 i in
      encoding_check' code_memory pc assembled →
        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
        let 〈instr, pc〉 ≝ instr_pc in
          instr = i.
 
lemma main_thm:
 ∀ticks_of.
 ∀ps: PseudoStatus.
  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
  let s' ≝ execute_1 s in
   s = s'']].
 #ticks_of #ps
 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
 
 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd