include "ASM/ASM.ma".
include "ASM/BitVectorTrie.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Status.ma".

definition assembly_preinstruction ≝
  λA: Type[0].
  λaddr_of: A → Byte. (* relative *)
  λpre: preinstruction A.
  match pre with
  [ ADD addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | ADDC addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | ANL addrs ⇒
     match addrs with
      [ inl addrs ⇒ match addrs with
         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
            let b1 ≝
             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
              [ DIRECT b1 ⇒ λ_.b1
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
         ]
      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
  | CLR addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[true; true; true; false; false; true; false; false]]) ]
      | CARRY ⇒ λ_.
         [ ([[true; true; false; false; false; false; true; true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | CPL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[true; true; true; true; false; true; false; false]]) ]
      | CARRY ⇒ λ_.
         [ ([[true; false; true; true; false; false; true; true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | DA addr ⇒
     [ ([[true; true; false; true; false; true; false; false]]) ]
  | DEC addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[false; false; false; true; false; true; false; false]]) ]
      | REGISTER r ⇒ λ_.
         [ ([[false; false; false; true; true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
      | INDIRECT i1 ⇒ λ_.
         [ ([[false; false; false; true; false; true; true; i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | DJNZ addr1 addr2 ⇒
         let b2 ≝ addr_of addr2 in
         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
          [ REGISTER r ⇒ λ_.
             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
          | DIRECT b1 ⇒ λ_.
             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JC addr ⇒
        let b1 ≝ addr_of addr in
          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
      | JNC addr ⇒
         let b1 ≝ addr_of addr in
           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
      | JZ addr ⇒
         let b1 ≝ addr_of addr in
           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
      | JNZ addr ⇒
         let b1 ≝ addr_of addr in
           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
      | JB addr1 addr2 ⇒
         let b2 ≝ addr_of addr2 in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JNB addr1 addr2 ⇒
         let b2 ≝ addr_of addr2 in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JBC addr1 addr2 ⇒
         let b2 ≝ addr_of addr2 in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | CJNE addrs addr3 ⇒
         let b3 ≝ addr_of addr3 in
         match addrs with
          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
              [ DIRECT b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
              | DATA b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             let b2 ≝
              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
               [ DATA b2 ⇒ λ_. b2
               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
              [ REGISTER r ⇒ λ_.
                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
              | INDIRECT i1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
         ]
  | DIV addr1 addr2 ⇒
     [ ([[true;false;false;false;false;true;false;false]]) ]
  | INC addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[false;false;false;false;false;true;false;false]]) ]         
      | REGISTER r ⇒ λ_.
         [ ([[false;false;false;false;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
      | INDIRECT i1 ⇒ λ_.
        [ ([[false; false; false; false; false; true; true; i1]]) ]
      | DPTR ⇒ λ_.
        [ ([[true;false;true;false;false;false;true;true]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | MOV addrs ⇒
     match addrs with
      [ inl addrs ⇒
         match addrs with
          [ inl addrs ⇒
             match addrs with
              [ inl addrs ⇒
                 match addrs with
                  [ inl addrs ⇒
                     match addrs with
                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
                          [ REGISTER r ⇒ λ_.
                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                          | INDIRECT i1 ⇒ λ_.
                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
                     let b1 ≝
                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
                       [ DIRECT b1 ⇒ λ_. b1
                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
                  [ DATA16 w ⇒ λ_.
                     let 〈b1,b2〉 ≝ split ? 8 8 w in
                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
              [ BIT_ADDR b1 ⇒ λ_.
                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
  | MOVX addrs ⇒
     match addrs with
      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
          [ EXT_INDIRECT i1 ⇒ λ_.
             [ ([[true;true;true;false;false;false;true;i1]]) ]
          | EXT_INDIRECT_DPTR ⇒ λ_.
             [ ([[true;true;true;false;false;false;false;false]]) ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
          [ EXT_INDIRECT i1 ⇒ λ_.
             [ ([[true;true;true;true;false;false;true;i1]]) ]
          | EXT_INDIRECT_DPTR ⇒ λ_.
             [ ([[true;true;true;true;false;false;false;false]]) ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
  | MUL addr1 addr2 ⇒
     [ ([[true;false;true;false;false;true;false;false]]) ]
  | NOP ⇒
     [ ([[false;false;false;false;false;false;false;false]]) ]
  | ORL addrs ⇒
     match addrs with
      [ inl addrs ⇒
         match addrs with
          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
            let b1 ≝
              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
               [ DIRECT b1 ⇒ λ_. b1
               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
              [ ACC_A ⇒ λ_.
                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
              | DATA b2 ⇒ λ_.
                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in      
         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
          | N_BIT_ADDR b1 ⇒ λ_.
             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
  | POP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
      [ DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | PUSH addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
      [ DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | RET ⇒
     [ ([[false;false;true;false;false;false;true;false]]) ]
  | RETI ⇒
     [ ([[false;false;true;true;false;false;true;false]]) ]
  | RL addr ⇒
     [ ([[false;false;true;false;false;false;true;true]]) ]
  | RLC addr ⇒
     [ ([[false;false;true;true;false;false;true;true]]) ]
  | RR addr ⇒
     [ ([[false;false;false;false;false;false;true;true]]) ]
  | RRC addr ⇒
     [ ([[false;false;false;true;false;false;true;true]]) ]
  | SETB addr ⇒     
     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
      [ CARRY ⇒ λ_.
         [ ([[true;true;false;true;false;false;true;true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | SUBB addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
      [ REGISTER r ⇒ λ_.
         [ ([[true;false;false;true;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;false;true]]); b1]
      | INDIRECT i1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;false;false]]); b1]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | SWAP addr ⇒
     [ ([[true;true;false;false;false;true;false;false]]) ]
  | XCH addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
      [ REGISTER r ⇒ λ_.
         [ ([[true;true;false;false;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;false;false;true;false;true]]); b1]
      | INDIRECT i1 ⇒ λ_.
         [ ([[true;true;false;false;false;true;true;i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | XCHD addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
      [ INDIRECT i1 ⇒ λ_.
         [ ([[true;true;false;true;false;true;true;i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | XRL addrs ⇒
     match addrs with
      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
          [ REGISTER r ⇒ λ_.
             [ ([[false;true;true;false;true]]) @@ r ]
          | DIRECT b1 ⇒ λ_.
             [ ([[false;true;true;false;false;true;false;true]]); b1]
          | INDIRECT i1 ⇒ λ_.
             [ ([[false;true;true;false;false;true;true;i1]]) ]
          | DATA b1 ⇒ λ_.
             [ ([[false;true;true;false;false;true;false;false]]); b1]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         let b1 ≝
          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
           [ DIRECT b1 ⇒ λ_. b1
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
          [ ACC_A ⇒ λ_.
             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
          | DATA b2 ⇒ λ_.
             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
       ].

definition assembly1 ≝
 λi: instruction.
 match i with
  [ ACALL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
      [ ADDR11 w ⇒ λ_.
         let 〈v1,v2〉 ≝ split ? 3 8 w in
          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | AJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
      [ ADDR11 w ⇒ λ_.
         let 〈v1,v2〉 ≝ split ?  3 8 w in
          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | JMP adptr ⇒
     [ ([[false;true;true;true;false;false;true;true]]) ]
  | LCALL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
      [ ADDR16 w ⇒ λ_.
         let 〈b1,b2〉 ≝ split ? 8 8 w in
          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | LJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
      [ ADDR16 w ⇒ λ_.
         let 〈b1,b2〉 ≝ split ? 8 8 w in
          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | MOVC addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
      [ ACC_DPTR ⇒ λ_.
         [ ([[true;false;false;true;false;false;true;true]]) ]
      | ACC_PC ⇒ λ_.
         [ ([[true;false;false;false;false;false;true;true]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | SJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
      [ RELATIVE b1 ⇒ λ_.
         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | RealInstruction instr ⇒
    assembly_preinstruction [[ relative ]]
      (λx.
        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
        [ RELATIVE r ⇒ λ_. r
        | _ ⇒ λabsd. ⊥
        ] (subaddressing_modein … x)) instr
  ].
  cases absd
qed.

definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝
    λmap.
    λid: Identifier.
      let address ≝ lookup … id map (zero ?) in
      let 〈high, low〉 ≝ split ? 8 8 address in
      if eq_bv ? high (zero ?) then
        low
      else
        ?.
      elim not_implemented.
qed.

definition assembly_expansion ≝
  λi.
  λcosts: BitVectorTrie Identifier 16.
  λprogram_counter: nat.
            match i with
              [ Instruction instr ⇒
                let code_memory ≝ load_code_memory (assembly_preinstruction Identifier (λx. zero 8) instr) in
                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
                let 〈instr', program_counter'〉 ≝ instr_pc' in
                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
                  〈program_counter + program_counter_n', costs〉 
              | Comment comment ⇒ 〈program_counter, costs〉
              | Cost cost ⇒
                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
                  〈program_counter, (insert ? ? program_counter_bv cost costs)〉
              | Jmp jmp ⇒
                  〈program_counter + 3, costs〉
              | Call call ⇒
                  〈program_counter + 3, costs〉
              | Mov dptr trgt ⇒ 〈program_counter, costs〉
              ].

definition assembly_1_pseudoinstruction ≝
  λlookup_labels.
  λlookup_datalabels.
  λaddress_of.
  λi: labelled_instruction.
                match \snd i with
                  [ Cost cost ⇒ [ ]
                  | Comment comment ⇒ [ ]
                  | Call call ⇒
                    let address ≝ ADDR16 (lookup_labels call) in
                      assembly1 (LCALL address)
                  | Mov d trgt ⇒
                    let address ≝ DATA16 (lookup_datalabels trgt) in
                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
                  | Instruction instr ⇒ assembly_preinstruction ? address_of instr
                  | Jmp jmp ⇒ 
                    let address ≝ ADDR16 (lookup_labels jmp) in
                      assembly1 (LJMP address)
(*                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
*)
                  ].
  @ I
qed.

definition construct_datalabels ≝
  λpreamble.
    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
    λt. λpreamble.
      let 〈datalabels, addr〉 ≝ t in
      let 〈name, size〉 ≝ preamble in
      let addr_16 ≝ bitvector_of_nat 16 addr in
        〈insert ? ? name addr_16 datalabels, addr + size〉)
          〈(Stub ? ?), 0〉 preamble).

definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  λp.
    let 〈preamble, instr_list〉 ≝ p in
    let datalabels ≝ construct_datalabels preamble in
    let 〈labels,pc_costs〉 ≝
      foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
        λt. λi.
          let 〈label, i〉 ≝ i in
          let 〈labels, pc_costs〉 ≝ t in
          let 〈program_counter, costs〉 ≝ pc_costs 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
          〈labels, assembly_expansion i costs program_counter〉
          ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
    let 〈program_counter, costs〉 ≝ pc_costs in
      if gtb program_counter (2^16) then (* 65536 *)
        None ?
      else
        let flat_list ≝ flatten ? (
          map ? ? (
            assembly_1_pseudoinstruction (
              λx. lookup ? ? x labels (zero ?))
                (λx. lookup ? ? x datalabels (zero ?))
                (address_of labels)) instr_list) in
        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
(*
  [2,3,4,5,6:
    normalize; %;
  | whd in ⊢ (? (? ? ? %));
      cases (split bool 8 8 (lookup Word 16 trgt labels (zero 16)))
      # high
      # low
      whd in ⊢ (? (? ? ? %))
      cases (eq_bv 8 high (zero 8))
      [ normalize
        %
      | elim not_implemented;
      ]
  ]
qed. *)

definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).