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
                     let b1 ≝ \fst b1_b2 in
                     let b2 ≝ \snd b1_b2 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
         let v1 ≝ \fst v1_v2 in
         let v2 ≝ \snd v1_v2 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
         let v1 ≝ \fst v1_v2 in
         let v2 ≝ \snd v1_v2 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
         let b1 ≝ \fst b1_b2 in
         let b2 ≝ \snd b1_b2 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
         let b1 ≝ \fst b1_b2 in
         let b2 ≝ \snd b1_b2 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.

inductive jump_length: Type[0] ≝
  | short_jump: jump_length
  | medium_jump: jump_length
  | long_jump: jump_length.

(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
definition jump_expansion_policy ≝ BitVectorTrie (Word × jump_length) 16.

definition expand_relative_jump_internal:
 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
 option (list instruction)
 ≝
  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
  match jmp_len with
  [ short_jump ⇒
     let lookup_address ≝ lookup_labels jmp in
     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
     let 〈upper, lower〉 ≝ split ? 8 8 result in
     if eq_bv ? upper (zero 8) then
      let address ≝ RELATIVE lower in
       Some ? [ RealInstruction (i address) ]
     else
       None ?
  | medium_jump ⇒ None …
  | long_jump ⇒
    Some ?
    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
      LJMP (ADDR16 (lookup_labels jmp))
    ]
  ].
  @ I
qed.

definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
  λlookup_labels.
  λjmp_len: jump_length.
  λpc.
  λi: preinstruction Identifier.
  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
  match i with
  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
  | INC arg ⇒ Some ? [ INC ? arg ]
  | DEC arg ⇒ Some ? [ DEC ? arg ]
  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
  | DA arg ⇒ Some ? [ DA ? arg ]
  | ANL arg ⇒ Some ? [ ANL ? arg ]
  | ORL arg ⇒ Some ? [ ORL ? arg ]
  | XRL arg ⇒ Some ? [ XRL ? arg ]
  | CLR arg ⇒ Some ? [ CLR ? arg ]
  | CPL arg ⇒ Some ? [ CPL ? arg ]
  | RL arg ⇒ Some ? [ RL ? arg ]
  | RR arg ⇒ Some ? [ RR ? arg ]
  | RLC arg ⇒ Some ? [ RLC ? arg ]
  | RRC arg ⇒ Some ? [ RRC ? arg ]
  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
  | MOV arg ⇒ Some ? [ MOV ? arg ]
  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
  | SETB arg ⇒ Some ? [ SETB ? arg ] 
  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
  | POP arg ⇒ Some ? [ POP ? arg ]
  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
  | RET ⇒ Some ? [ RET ? ]
  | RETI ⇒ Some ? [ RETI ? ]
  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
  ].

definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
  λlookup_labels.
  λlookup_datalabels.
  λpc.
  λjmp_len.
  λi.
  match i with
  [ Cost cost ⇒ Some ? [ ]
  | Comment comment ⇒ Some ? [ ]
  | Call call ⇒
    match jmp_len with
    [ short_jump ⇒ None ?
    | medium_jump ⇒
      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
      if eq_bv ? ignore fst_5 then
        let address ≝ ADDR11 address in
          Some ? ([ ACALL address ])
      else
        None ?
    | long_jump ⇒
      let address ≝ ADDR16 (lookup_labels call) in
        Some ? [ LCALL address ]
    ]
  | Mov d trgt ⇒ 
    let address ≝ DATA16 (lookup_datalabels trgt) in
      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
  | Jmp jmp ⇒
    match jmp_len with
    [ short_jump ⇒ 
      let lookup_address ≝ lookup_labels jmp in
      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
      let 〈upper, lower〉 ≝ split ? 8 8 result in
      if eq_bv ? upper (zero 8) then
        let address ≝ RELATIVE lower in
          Some ? [ SJMP address ]
      else
        None ?
    | medium_jump ⇒
      let address ≝ lookup_labels jmp in
      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
      if eq_bv ? fst_5_addr fst_5_pc then
        let address ≝ ADDR11 rest_addr in
          Some ? ([ AJMP address ])
      else
        None ?
    | long_jump ⇒
      let address ≝ ADDR16 (lookup_labels jmp) in
        Some ? [ LJMP address ]
    ]
  ].
  @ I
qed.

(* label_trie: identifier ↦ 〈instruction number, address〉 *)
definition label_trie ≝ BitVectorTrie (nat × Word) 16.

definition add_instruction_size: Word → jump_length → pseudo_instruction → Word ≝
  λpc.λjmp_len.λinstr.
  let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in
  let bv: list (BitVector 8) ≝ match ilist with
    [ None   ⇒ (* hmm, this shouldn't happen *) [ ]
    | Some l ⇒ flatten … (map … assembly1 l)
    ] in 
  let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in
  new_pc.
  
definition create_label_trie: list labelled_instruction → jump_expansion_policy → 
  label_trie ≝
  λprogram.λpolicy.
  let 〈final_n, final_pc, final_labels〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.Σres.True)
    program
    (λprefix.λx.λtl.λprf.λacc.
     let 〈n,pc,labels〉 ≝ acc in
     let 〈label,instr〉 ≝ x in
     let new_labels ≝ 
       match label with
       [ None   ⇒ labels
       | Some l ⇒ insert … l 〈n, pc〉 labels
       ] in
     let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in
     let new_pc ≝ add_instruction_size pc jmp_len instr in
     〈S n, new_pc, new_labels〉
    ) 〈0, zero ?, Stub ? ?〉 in
    final_labels.
 @I
qed.

definition select_reljump_length: label_trie → Word → Identifier → jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *)
  then short_jump
  else long_jump.

definition select_call_length: label_trie → Word → Identifier → jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
  if eq_bv ? fst_5_addr fst_5_pc
  then medium_jump
  else long_jump.
  
definition select_jump_length: label_trie → Word → Identifier → jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
  if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *)
  then short_jump
  else
    let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in
    let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    if eq_bv ? fst_5_addr fst_5_pc
    then medium_jump
    else long_jump.
 
definition jump_expansion_step_instruction: label_trie → Word →
  preinstruction Identifier → option jump_length ≝
  λlabels.λpc.λi.
  match i with
  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
  | _        ⇒ None ?
  ].

definition max_length: jump_length → jump_length → jump_length ≝
  λj1.λj2.
  match j1 with
  [ long_jump   ⇒ long_jump
  | medium_jump ⇒
    match j2 with
    [ long_jump ⇒ long_jump
    | _         ⇒ medium_jump
    ]
  | short_jump  ⇒ j2
  ].
      
definition jump_expansion_step: list labelled_instruction →
  jump_expansion_policy → jump_expansion_policy ≝ 
  λprogram.λpolicy.
  let labels ≝ create_label_trie program policy in
  let 〈final_n, final_pc, final_policy〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.Σres.True)
    program
    (λprefix.λx.λtl.λprf.λacc.
      let 〈n, pc, policy〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
      let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in
      let add_instr ≝
        match instr with
        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i 
        | Call c        ⇒ Some ? (select_call_length labels pc c)
        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
        | _             ⇒ None ?
        ] in
      let 〈new_pc, new_policy〉 ≝
        let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in
        match add_instr with
        [ None    ⇒ (* i.e. it's not a jump *)
          〈add_instruction_size pc long_jump instr, policy〉
        | Some ai ⇒
          let new_length ≝ max_length old_length ai in
          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉 
        ] in
      〈S n, new_pc, new_policy〉
    ) 〈0, zero ?, Stub ? ?〉 in
    final_policy.
 @I
qed.
 
definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝
  λprogram.
    Stub ? ?.
    
(**************************************** START OF POLICY ABSTRACTION ********************)

definition policy_type ≝ Word → jump_length.

definition jump_expansion': pseudo_assembly_program → policy_type ≝
 λprogram.λpc.
  let policy ≝ jump_expansion_internal (\snd program) in
  let 〈n,j〉 ≝ lookup ? ? pc policy 〈zero ?, long_jump〉 in
    j.
  
definition assembly_1_pseudoinstruction_safe ≝
  λprogram: pseudo_assembly_program.
  λjump_expansion: policy_type.
  λppc: Word.
  λpc: Word.
  λlookup_labels.
  λlookup_datalabels.
  λi.
  let expansion ≝ jump_expansion ppc in
    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
    [ None ⇒ None ?
    | Some pseudos ⇒
      let mapped ≝ map ? ? assembly1 pseudos in
      let flattened ≝ flatten ? mapped in
      let pc_len ≝ length ? flattened in
        Some ? (〈pc_len, flattened〉)
    ].
 
definition construct_costs_safe ≝
  λprogram.
  λjump_expansion: policy_type.
  λpseudo_program_counter: nat.
  λprogram_counter: nat.
  λcosts: BitVectorTrie Word 16.
  λi.
  match i with
  [ Cost cost ⇒
    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
  | _ ⇒
    let pc_bv ≝ bitvector_of_nat ? program_counter in
    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
    let lookup_labels ≝ λx.pc_bv in
    let lookup_datalabels ≝ λx.zero ? in
    let pc_delta_assembled ≝
      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
        lookup_labels lookup_datalabels i
    in
    match pc_delta_assembled with
    [ None ⇒ None ?
    | Some pc_delta_assembled ⇒
      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
        Some ? 〈pc_delta + program_counter, costs〉        
    ]
  ].

(* 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 sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
 λinstr_list.
 λjump_expansion: policy_type.
 λl:list labelled_instruction.
 λacc.
  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_safe instr_list jump_expansion ppc program_counter (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〉〉 ]
       ]) acc l.

definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).

definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
 λprogram,jump_expansion,instr_list.
  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
   [ None ⇒ None …
   | Some result ⇒
      let 〈ppc,pc_sigma_map〉 ≝ result in
      let 〈pc,map〉 ≝ pc_sigma_map in
       Some … 〈ppc,pc〉 ].

definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
 λinstr_list,jump_expansion.
  match sigma0 instr_list jump_expansion 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 …)) ].

(* stuff about policy *)

definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….

definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.

lemma eject_policy: ∀p. policy p → policy_type.
 #p #pol @(eject … pol)
qed.

coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.

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

example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
 cases daemon.
qed.

definition expand_pseudo_instruction:
 ∀program:pseudo_assembly_program.∀pol: policy program.
  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc.
  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
  let pi ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
  pc = sigma program pol ppc →
  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,prf1,prf2,prf3.
   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) (\fst (fetch_pseudo_instruction (\snd program) ppc)) with
    [ None ⇒ let dummy ≝ [ ] in dummy
    | Some res ⇒ res ].
 [ cases daemon
 | >p %]
qed.

(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
definition assembly_1_pseudoinstruction':
 ∀program:pseudo_assembly_program.∀pol: policy program.
  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
  Σres:(nat × (list Byte)).
   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
   let 〈len,code〉 ≝ res in
    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
≝ λprogram: pseudo_assembly_program.
  λpol: policy program.
  λppc: Word.
  λlookup_labels.
  λlookup_datalabels.
  λpi.
  λprf1,prf2,prf3.
   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy 
    | Some res ⇒ res ].
 [ @⊥ elim pi in p [*]
   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
   cases daemon
 | % [ >p %]
   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
   (* THIS SHOULD BE TRUE INSTEAD *)
   cases daemon]
qed.

definition assembly_1_pseudoinstruction:
 ∀program:pseudo_assembly_program.∀pol: policy program.
  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
   nat × (list Byte)
≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
    prf2 prf3.

lemma assembly_1_pseudoinstruction_ok1:
 ∀program:pseudo_assembly_program.∀pol: policy program.
  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
 #H1 #_ @H1
qed.

(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
definition construct_costs':
 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
≝
  λprogram.λpol: policy program.λppc,pc,costs,i.
   match construct_costs_safe program pol ppc pc costs i with
    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
    | Some res ⇒ res ].
 [ cases daemon
 | >p %]
qed.

definition construct_costs ≝
 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).

lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
 #A #a #b #EQ destruct //
qed.

lemma sigma00_strict:
 ∀instr_list,jump_expansion,l,acc. acc = None ? →
  sigma00 instr_list jump_expansion l acc = None ….
 #instr_list #jump_expansion #l elim l
  [ #acc #H >H %
  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
qed.

lemma sigma00_append:
 ∀instr_list,jump_expansion,l1,l2,acc.
  sigma00 instr_list jump_expansion (l1@l2) acc =
   sigma00 instr_list jump_expansion
    l2 (sigma00 instr_list jump_expansion l1 acc).
 whd in match sigma00; normalize nodelta;
 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
qed.

lemma policy_ok_prefix_ok:
 ∀program.∀pol:policy program.∀suffix,prefix.
  prefix@suffix = \snd program →
   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
 normalize nodelta >sigma00_append
 cases (sigma00 ?? prefix ?)
  [2: #x #_ % #abs destruct(abs)
  | * #abs @⊥ @abs >sigma00_strict % ]
qed.

lemma policy_ok_prefix_hd_ok:
 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
  (prefix@[hd])@suffix = \snd program →
   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    let 〈program_counter, sigma_map〉 ≝ pc_map in
    let 〈label, i〉 ≝ hd in
     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
 @pair_elim' #pc #map #EQ4 normalize nodelta
 @pair_elim' #l' #i' #EQ5 normalize nodelta
 cases (construct_costs_safe ??????) normalize
  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
qed.

(*
lemma tech_pc_sigma00_append_Some:
 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
 #program #pol #prefix #costs #label #i #ppc #pc #H
  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
  whd in match sigma0; normalize nodelta;
  >foldl_step
  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
  cases (sigma00 program pol prefix) in H ⊢ %
   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
     
     normalize nodelta; -H;
     
  
   generalize in match H; -H;
  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
   [2: whd in ⊢ (??%%)
XXX
*)

axiom construct_costs_sigma:
 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).

axiom tech_pc_sigma00_append_Some:
 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.

definition build_maps:
 ∀pseudo_program.∀pol:policy pseudo_program.
  Σres:((BitVectorTrie Word 16) × (BitVectorTrie Word 16)).
   let 〈labels,costs〉 ≝ res in
    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
≝
  λpseudo_program.λpol:policy pseudo_program.
  let result ≝
   foldl_strong
    (option Identifier × pseudo_instruction)
    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
      let 〈labels,ppc_pc_costs〉 ≝ res in
      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
      let 〈pc',costs〉 ≝ pc_costs in
       And ( And (
       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
       (ppc' = length … pre)) (*∧ *)
       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
       (∀id. occurs_exactly_once id pre →
        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
    (\snd pseudo_program)
    (λprefix,i,tl,prf,t.
      let 〈labels, ppc_pc_costs〉 ≝ t in
      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
      let 〈pc,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 ? pc in
             insert ? ? label program_counter_bv labels]
       in
         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
          〈labels, 〈S ppc,construct〉〉
    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
  in
   let 〈labels, ppc_pc_costs〉 ≝ result in
   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
   let 〈pc, costs〉 ≝ pc_costs in
    〈labels, costs〉.
 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
   | #id normalize nodelta; -labels1; cases label; normalize nodelta
     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
 | generalize in match (sig2 … result) in ⊢ ?;
   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
qed.

definition assembly:
 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
  λp.let 〈preamble, instr_list〉 ≝ p in
   λpol.
    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
    let datalabels ≝ construct_datalabels preamble in
    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    let result ≝
     foldl_strong
      (option Identifier × pseudo_instruction)
      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
        let 〈ppc,code〉 ≝ ppc_code in
         ∀ppc'.
          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
          let 〈len,assembledi〉 ≝
           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
           True)
      instr_list
      (λprefix,hd,tl,prf,pc_ppc_code.
        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
        let 〈ppc, code〉 ≝ ppc_code in
        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
         〈new_pc, 〈new_ppc, (code @ program)〉〉)
      〈(zero ?), 〈(zero ?), [ ]〉〉
    in
     〈\snd (\snd result), costs〉.
 [2,5: %
 |*: cases daemon ]
qed.

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