include "basics/russell.ma".

include "ASM/Arithmetic.ma".
include "ASM/ASM.ma". (* includes "ASM/BitVectorTrie.ma". *)

(***** Pseudo-code ******)

definition inefficient_address_of_label :
 list labelled_instruction → Identifier →  ℕ ≝
  λinstr_list : list labelled_instruction.
  λid: Identifier.
    index_of ? (instruction_matches_identifier ?? id) instr_list.

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

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

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

(* label_map: identifier ↦ pseudo program counter *)
definition label_map ≝ identifier_map ASMTag ℕ.

(* The function that creates the label-to-address map *)
definition create_label_cost_map0: ∀program:list labelled_instruction.
  (Σlabels_costs:label_map × costlabel_map. (* Both on ppcs *)
    let labels ≝ \fst labels_costs in
    let address_of_label ≝ λl. lookup_def ?? labels l 0 in 
    (∀l.occurs_exactly_once ?? l program →
      address_of_label l =
       inefficient_address_of_label program l) ∧
    (∀l.occurs_exactly_once ?? l program → address_of_label l < |program|)
  ) ≝
  λprogram.
  \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
  (λprefix.Σlabels_costs_ppc:label_map × costlabel_map × ℕ.
    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    let address_of_label ≝ λl. lookup_def ?? labels l 0 in 
      ppc = |prefix| ∧
    ((∀l.occurs_exactly_once ?? l prefix →
      address_of_label l =
       inefficient_address_of_label prefix l) ∧
    (∀l.occurs_exactly_once ?? l prefix → address_of_label l < |program|)))
  program
  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
   let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in
   let 〈label,instr〉 ≝ x in
   let labels ≝
     match label with
     [ None   ⇒ labels
     | Some l ⇒ add … labels l ppc
     ] in
   let costs ≝
     match instr with
     [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs
     | _ ⇒ costs ] in
      〈labels,costs,S ppc〉
   ) 〈(empty_map …),(Stub ??),0〉)).
[ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta *
  #IH1 >IH1 -IH1 * #IH2 #IH3 -labels_costs_ppc % [>length_append <plus_n_Sm <plus_n_O %]
 inversion label [#EQ | #l #EQ] 
 [ % #lbl >occurs_exactly_once_None #Hocc 
   [ <inefficient_address_of_label_None [2: >occurs_exactly_once_None //]
     @IH2
   | @IH3
   ] //
 | % #lbl inversion (eq_identifier ? l lbl) 
    [1,3: #Heq >(eq_identifier_eq … Heq) #Hocc 
     [ >inefficient_address_of_label_Some_hit 
       [ >lookup_def_add_hit 
       | 
       ] //
     | >lookup_def_add_hit >prf >length_append <plus_n_Sm @le_S_S @le_plus_n_r
     ]
    |*: #Hneq cut (lbl ≠ l) [1,3: % @neq_identifier_neq >eq_identifier_sym //]
     #lbl_neq >(lookup_def_add_miss ??????? lbl_neq) >occurs_exactly_once_Some_eq >Hneq
     [ #Hocc lapply (IH2 ? Hocc)
       <inefficient_address_of_label_Some_miss [2: >occurs_exactly_once_Some_eq >Hneq] 
     | @IH3 
     ] //
   ]
 ]
| @pair_elim * #labels #costs #ppc #EQ destruct % // % 
  #l #abs cases (abs)
| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc * 
  #_ #H @H
]
qed.

(* The function that creates the label-to-address map *)
definition create_label_cost_map: ∀program:list labelled_instruction.
  label_map × costlabel_map ≝
    λprogram.
      pi1 … (create_label_cost_map0 program).

theorem create_label_cost_map_ok:
 ∀instr_list.
   let labels ≝ \fst (create_label_cost_map instr_list) in
   let address_of_label ≝ λl. lookup_def ?? labels l 0 in 
    ((∀id. occurs_exactly_once ??  id instr_list →
     (address_of_label id = inefficient_address_of_label instr_list id))
    ∧
     (∀id. occurs_exactly_once ?? id instr_list → address_of_label id < |instr_list|)).
 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?);
 @pi2
qed.

(* the defn we care about, and export elsewhere *)
definition address_of_word_labels :
 list labelled_instruction → Identifier → Word
≝
  λprogram : list labelled_instruction.
  λid: Identifier.
   let labels ≝ \fst (create_label_cost_map program) in
   let address_of_label ≝ λl. lookup_def ?? labels l 0 in 
    bitvector_of_nat ? (address_of_label id).

lemma address_of_word_labels_None: ∀i,id,instr_list.
 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →
  address_of_word_labels instr_list id =
  address_of_word_labels (instr_list@[〈None …,i〉]) id.
 #i #id #instr_list #H
 whd in match address_of_word_labels; normalize nodelta
 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_
 lapply (create_label_cost_map_ok instr_list) * #K #_
 >K' // >K // <inefficient_address_of_label_None //
qed.

lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list.
 eq_identifier ? id' id = false →
  occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →
   address_of_word_labels instr_list id =
   address_of_word_labels (instr_list@[〈Some … id',i〉]) id.
 #i #id #id' #instr_list #H1 #H2
 whd in match address_of_word_labels; normalize nodelta
 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_
 lapply (create_label_cost_map_ok instr_list) * #K #_
 >K' // >K 
 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ]
 <inefficient_address_of_label_Some_miss //
qed.

lemma address_of_word_labels_Some_hit: ∀i,id,instr_list.
  occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →
   address_of_word_labels (instr_list@[〈Some … id,i〉]) id
   = bitvector_of_nat … (|instr_list|).
 #i #id #instr_list #H
 whd in match address_of_word_labels; normalize nodelta
 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_
 >K // <inefficient_address_of_label_Some_hit //
qed.

(***** Object-code *******)
(*
definition bitvector_max_nat ≝
  λlength: nat.
    2^length.

definition code_memory_size ≝ bitvector_max_nat 16.
*)

lemma Prod_inv_rect_Type0:
 ∀A,B. ∀P: A × B → Type[0].∀ab.
  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
 #A #B #P * /2/
qed.

notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
 with precedence 10
for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.

notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
 with precedence 10
for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.

lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
[2: // ]
#A #B #C *; normalize /2/
qed.

(* timings taken from SIEMENS *)

definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
    ∀program_counter: Word. Byte → instruction × Word × nat ≝
  λpmem.
  λpc.
  λv.
   let 〈b,v〉 ≝ head … v in if b then
    let 〈b,v〉 ≝ head … v in if b then
     let 〈b,v〉 ≝ head … v in if b then
      let 〈b,v〉 ≝ head … v in if b then
       let 〈b,v〉 ≝ head … v in if b then
        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
          else
           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
          else
           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
          else
           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    else
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
         else
          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
          else
           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
   else
    let 〈b,v〉≝  head … v in if b then
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈JMP … ACC_DPTR, pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    else
     let 〈b,v〉≝  head … v in if b then
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
          else
           〈〈RealInstruction (RETI …), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
          else
           〈〈RealInstruction (RET …), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     else
      let 〈b,v〉≝  head … v in if b then
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
      else
       let 〈b,v〉≝  head … v in if b then
        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
       else
        let 〈b,v〉≝  head … v in if b then
         let 〈b,v〉≝  head … v in if b then
          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
          else
           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
        else
         let 〈b,v〉≝  head … v in if b then
          let 〈b,v〉≝  head … v in if b then
           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
          else
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
         else
          let 〈b,v〉≝  head … v in if b then
           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
          else
           〈〈RealInstruction (NOP …), pc〉, 1〉.
  %
qed.

definition fetch: ∀code_memory: BitVectorTrie Byte 16.
    ∀program_counter: Word. instruction × Word × nat ≝
  λpmem: BitVectorTrie Byte 16.
  λpc: Word.
  let 〈word, byte〉 ≝ next pmem pc in
    fetch0 pmem word byte.