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

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)
  | ADD addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;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 ? [[register;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)
  | 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)
  | 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 ? [[register;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;register;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)
  | DIV addr1 addr2 ⇒
     [ ([[true;false;false;false;false;true;false;false]]) ]
  | Jump j ⇒
     match j with
      [ DJNZ addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
         match addr1 return λx. bool_to_Prop (is_in ? [[register;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 ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JNC addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JZ addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JNZ addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JB addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … 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 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … 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 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … 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 ≝
          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b3 ⇒ λ_. b3
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … 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 ? [[register;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) ]]
  | INC addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;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)
  | JMP addr ⇒
     [ ([[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)
  | 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 ? [[register;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 ? [[register;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;register;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)]
  | 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)
  | 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 ? [[register;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)
  | 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)
  | SUBB addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;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 ? [[register;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;register;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 assembly_jump: (jump Identifier) → (Identifier → [[relative]]) → instruction ≝
  λj: jump Identifier.
  λaddr_of: Identifier → [[relative]].
    match j with
      [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp))
      | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp))
      | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp))
      | JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp))
      | JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp'))
      | JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp'))
      | JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp'))
      | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
      | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
      ].

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

definition assembly: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
  λp.
    let 〈preamble, instr_list〉 ≝ p in
    let 〈datalabels, ignore〉 ≝
      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 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,
            match i with
              [ Instruction instr ⇒
                let code_memory ≝ load_code_memory (assembly1 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 ⇒ pc_costs
              | WithLabel jmp ⇒
                let fake_addr ≝ RELATIVE (zero 8) in
                let fake_jump ≝ assembly_jump jmp (λx: Identifier. fake_addr) in
                let code_memory ≝ load_code_memory (assembly1 fake_jump) 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 16 program_counter' in
                  〈program_counter + program_counter_n', costs〉
              ]〉
          ) 〈(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 ? ? (
              λi: labelled_instruction.
                match \snd i with
                  [ Cost cost ⇒ [ ]
                  | Comment comment ⇒ [ ]
                  | Call call ⇒
                    let pc_offset ≝ lookup ? ? call labels (zero ?) in
                    let address ≝ ADDR16 pc_offset in
                      assembly1 (LCALL ? address)
                  | Mov d trgt ⇒
                    let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in
                    let address ≝ DATA16 pc_offset in
                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
                  | Instruction instr ⇒ assembly1 instr
                  | Jmp jmp ⇒ 
                    let pc_offset ≝ lookup ? ? jmp labels (zero ?) in
                    let address ≝ ADDR16 pc_offset in
                      assembly1 (LJMP ? address)
                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (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 c0 labels (zero 16)))
      # high
      # low
      whd in ⊢ (? (? ? ? %))
      cases (eq_bv 8 high (zero 8))
      [ normalize
        %
      | elim not_implemented;
      ]
  ]
qed.

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