include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Status.ma".
include alias "basics/logic.ma".
include alias "arithmetics/nat.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 (ℕ × 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_map: identifier ↦ 〈instruction number, address〉 *)
definition label_map ≝ identifier_map ASMTag (nat × nat).

definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
  λpc.λjmp_len.λinstr.
  let bv_pc ≝ bitvector_of_nat 16 pc in
  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_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 
  pc + (|bv|).
  
definition is_label ≝ 
  λx:labelled_instruction.λl:Identifier. 
  let 〈lbl,instr〉 ≝ x in
  match lbl with
  [ Some l' ⇒ l' = l
  | _       ⇒ False
  ].
  
lemma label_does_not_occur:
  ∀i,p,l.
  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
 #i #p #l generalize in match i; elim p
 [ #i >nth_nil #H @⊥ @H
 | #h #t #IH #i cases i -i 
   [ cases h #hi #hp cases hi
     [ normalize #H @⊥ @H
     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
       whd in Heq; >Heq
       >eq_identifier_refl //
     ]
   | #i #H whd in match (does_not_occur ??);
     whd in match (instruction_matches_identifier ??);
     cases h #hi #hp cases hi normalize nodelta
     [ @(IH i) @H
     | #l' @eq_identifier_elim
       [ normalize //
       | normalize #_ @(IH i) @H
       ]
     ]
   ]
 ]
qed.  

lemma coerc_pair_sigma:
 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
#A #B #P * #a #b #p % [@a | /2/]
qed.
coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). 

definition create_label_map: ∀program:list labelled_instruction.
  ∀policy:jump_expansion_policy.
  (Σlabels:label_map.
    ∀i:ℕ.lt i (|program|) →
    ∀l.occurs_exactly_once l program →
    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    ∃a.lookup … labels l = Some ? 〈i,a〉 
  ) ≝
  λprogram.λpolicy.
  let 〈final_pc, final_labels〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.ℕ × (Σlabels.
      ∀i:ℕ.lt i (|prefix|) →
      ∀l.occurs_exactly_once l prefix →
      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
      ∃a.lookup … labels l = Some ? 〈i,a〉)
    )
    program
    (λprefix.λx.λtl.λprf.λacc.
     let 〈pc,labels〉 ≝ acc in
     let 〈label,instr〉 ≝ x in
          let new_labels ≝ 
          match label with
          [ None   ⇒ labels
          | Some l ⇒ add … labels l 〈|prefix|, pc〉
          ] in
          let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
          〈add_instruction_size pc jmp_len instr, new_labels〉
    ) 〈0, empty_map …〉 in
    final_labels.
[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
  [ #Hi #l normalize nodelta; cases label normalize nodelta
    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
      lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr  
      % [ @addr | @Haddr ]
    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
      @eq_identifier_elim #Heq #Hocc
      [ normalize in Hocc;
        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl  
        @⊥ @(absurd … Hocc) 
      | normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
        ]
      ]
      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
    ]
  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 
    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
      [ normalize nodelta #H @⊥ @H
      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
      ]
    | @le_n
    ]
  ]
| #i #Hi #l #Hl @⊥ @Hl
]
qed.

definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
  if leb pc addr (* forward jump *)
  then if leb (addr - pc) 126
       then short_jump
       else long_jump
  else if leb (pc - addr) 129
       then short_jump
       else long_jump.

definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
  λlabels.λpc_nat.λlbl.
  let pc ≝ bitvector_of_nat 16 pc_nat in
  let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) 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_map → ℕ → Identifier → jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
  if leb pc addr
  then if leb (addr - pc) 126
       then short_jump
       else select_call_length labels pc lbl
  else if leb (pc - addr) 129
       then short_jump
       else select_call_length labels pc lbl.
 
definition jump_expansion_step_instruction: label_map → ℕ →
  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 jmple: jump_length → jump_length → Prop ≝
  λj1.λj2.
  match j1 with
  [ short_jump  ⇒ 
    match j2 with
    [ short_jump ⇒ False
    | _          ⇒ True
    ]
  | medium_jump ⇒
    match j2 with
    [ long_jump ⇒ True
    | _         ⇒ False
    ]
  | long_jump   ⇒ False
  ].

definition jmpleq: jump_length → jump_length → Prop ≝
  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
  
lemma jmpleq_max_length: ∀ol,nl.
  jmpleq ol (max_length ol nl).
 #ol #nl cases ol cases nl
 /2 by or_introl, or_intror, I/
qed.
 
definition is_jump' ≝
  λx:preinstruction Identifier.
  match x with
  [ JC _ ⇒ True
  | JNC _ ⇒ True
  | JZ _ ⇒ True
  | JNZ _ ⇒ True
  | JB _ _ ⇒ True
  | JNB _ _ ⇒ True
  | JBC _ _ ⇒ True
  | CJNE _ _ ⇒ True
  | DJNZ _ _ ⇒ True
  | _ ⇒ False
  ].
  
definition is_jump ≝
  λx:labelled_instruction.
  let 〈label,instr〉 ≝ x in
  match instr with
  [ Instruction i   ⇒ is_jump' i
  | Call _ ⇒ True
  | Jmp _ ⇒ True
  | _ ⇒ False
  ].

definition jump_in_policy ≝
  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
  ∀i:ℕ.i < |prefix| →
  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
   ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
  
axiom bitvector_of_nat_abs:
  ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).

lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
 /2/ qed.

lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
 ∀policy:(Σp:jump_expansion_policy.
 (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
 jump_in_policy prefix p).
  ∀i:ℕ.i < |prefix| →
  ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
  lookup_opt … (bitvector_of_nat 16 i) policy = None ?.
 #prefix #policy #i #Hi @conj
 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
   [ #H @H
   | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi))
     @(ex_intro … y (ex_intro … z H))
   ]
 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj)
   #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
 ]  
qed.
 
definition jump_expansion_start: ∀program:list labelled_instruction.
  Σpolicy:jump_expansion_policy.(∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy program policy ≝
  λprogram.
  foldl_strong (option Identifier × pseudo_instruction)
  (λprefix.Σpolicy:jump_expansion_policy.(∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy prefix policy)
  program
  (λprefix.λx.λtl.λprf.λpolicy.
   let 〈label,instr〉 ≝ x in
   match instr with
   [ Instruction i ⇒ match i with
     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     | _ ⇒ (eject … policy)
     ]
   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
   | _      ⇒ (eject … policy)
   ]
  ) (Stub ? ?).
@conj
(* non-jumps, lookup_opt = None *)
[1,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,69,71,73,75,77,79,81,83:
  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
  -Hi; #Hi @((proj1 ?? (sig2 ?? policy)) i) 
  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65:
    @le_S_to_le @le_S_to_le @Hi
  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66:
    <Hi @le_n_Sn
  ]
(* non-jumps, lookup_opt = Some *)
|2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84:
  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
  -Hi; #Hi
  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65:
    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
  |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66:
    @conj >(injective_S … Hi)
    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65:
      >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
      <minus_n_n #H @⊥ @H
    |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66:
      #H elim H; -H; #t1 #H elim H; -H #t2 #H
      lapply (proj1 ?? (sig2 ?? policy) (|prefix|) (le_n (|prefix|)))
      #H2 >H2 in H; #H destruct (H)
    ]
  ]
(* jumps, lookup_opt = None *)
|3,5,51,53,55,57,59,61,63,65,67: #i >append_length <commutative_plus #Hi normalize in Hi;
  >lookup_opt_insert_miss
  [1,3,5,7,9,11,13,15,17,19,21,23: @((proj1 ?? (sig2 ?? policy)) i) @(le_S_to_le … Hi)
  |2,4,6,8,10,12,14,16,18,20,22,24: >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
  ]
(* non-jumps, lookup_opt = Some *)
|4,6,52,54,56,58,60,62,64,66,68: #i >append_length <commutative_plus #Hi normalize in Hi;
  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
  [1,3,5,7,9,11,13,15,17,19,21,23: >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    >lookup_opt_insert_miss
    [1,3,5,7,9,11,13,15,17,19,21,23: @((proj2 ?? (sig2 ?? policy)) i) @(le_S_S_to_le … Hi)
    |2,4,6,8,10,12,14,16,18,20,22,24: @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi))
    ]
  |2,4,6,8,10,12,14,16,18,20,22,24: @conj >(injective_S … Hi) #H
    [2,4,6,8,10,12,14,16,18,20,22,24: >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
       <minus_n_n // ]
    @(ex_intro ? ? 0 (ex_intro ? ? short_jump (lookup_opt_insert_hit ? ? 16 ? policy)))
  ]
(* cases for the empty program *)
|85: #i #Hi //
|86: whd #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
]
qed.

definition policy_increase: list labelled_instruction → jump_expansion_policy →
  jump_expansion_policy → Prop ≝
 λprogram.λop.λp.
  (* (∀i:ℕ.i < |program| →
    lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *)
  (∀i:ℕ.i < |program| →
    jmpleq 
      (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉))
      (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
    
definition jump_expansion_step: ∀program:list labelled_instruction.
  ∀old_policy:(Σpolicy.
    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    jump_in_policy program policy).
  (Σpolicy.
    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    jump_in_policy program policy ∧
    policy_increase program old_policy policy)
    ≝ 
  λprogram.λold_policy.
  let labels ≝ create_label_map program old_policy in
  let 〈final_pc, final_policy〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.ℕ × Σpolicy.
      (∀i.i ≥ |prefix| → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
      jump_in_policy prefix policy ∧
      policy_increase prefix old_policy policy
    )
    program
    (λprefix.λx.λtl.λprf.λacc.
      let 〈pc, policy〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_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 (|prefix|)) old_policy 〈0, 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 (|prefix|)) 〈pc, new_length〉 policy〉 
        ] in
      〈new_pc, new_policy〉
    ) 〈0, Stub ? ?〉 in
    final_policy.
[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
[ cases (lookup ??? old_policy ?) #h #n cases add_instr
  [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
  | #z normalize nodelta >lookup_opt_insert_miss 
    [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi))
    | >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi
    ]
  ]
| cases (le_to_or_lt_eq … Hi) -Hi;
  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    [ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
      [ @(proj1 ?? Hacc Hj)
      | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
        % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
            @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) ] ]
      ]
    | lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
      #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
      normalize nodelta #x #y [2: #z]
      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
      [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
      | @Hl
      ] 
    ]
  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
     [3,5,11: #H @⊥ @H (* instr is not a jump *)
     |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)))
       #H destruct (H)
     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n 
       whd in match (snd ???); @(ex_intro ?? pc) 
       [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id)))
       | @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id)))
       ] @lookup_opt_insert_hit
     |8,10: #_ //
     |1,2: cases pi
       [35,36,37: #H @⊥ @H
       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n
         whd in match (snd ???);
         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
         @lookup_opt_insert_hit
       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n
         whd in match (snd ???);
         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
         @lookup_opt_insert_hit
       |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
        #x #y normalize nodelta
        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 
        #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
        #x #y normalize nodelta
        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
        cases (lookup ??? old_policy ?) #x #y normalize nodelta
        >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) #H destruct (H)
       |46,47,51,52: #id #_ //
       |48,49,50,53,54: #x #id #_ //
       ]
     ]
   ]
  ]
| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %); 
  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
      #x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
    | normalize nodelta >(injective_S … Hi)
      >lookup_opt_lookup_miss
      [ >lookup_opt_lookup_miss
        [ //
        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
          #x #y normalize nodelta
          >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|))) //
        ]
      | >(proj1 ?? (jump_not_in_policy program old_policy (|prefix|) ?))
        [ //
        | >prf >p1 >nth_append_second [ <minus_n_n
        generalize in match Ha; normalize nodelta cases instr normalize nodelta 
        [1: #pi cases pi
         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
         |35,36,37: #H normalize /2 by nmk/
         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
           #H destruct (H)
         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
           #H destruct (H)
         ]
        |2,3: #x #H normalize /2 by nmk/
        |6: #x #y #H normalize /2 by nmk/
        |4,5: #id #H destruct (H)
        ] | @le_n ] 
        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
        ] 
      ]
    ]
  | #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    cases (le_to_or_lt_eq … Hi) -Hi; #Hi 
    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
      #y #z normalize nodelta normalize nodelta >lookup_insert_miss 
      [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
      | @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi)
      ]
    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (|prefix|) ?) ?)
      [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
        normalize nodelta >lookup_insert_hit @jmpleq_max_length
      | >prf >p1 >nth_append_second
        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta 
          [1: #pi cases pi
           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H) 
           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
           |35,36,37: #H normalize in H; destruct (H)
           |9,10,14,15: #id #H //
           |11,12,13,16,17: #x #id #H //
           ]
          |2,3: #x #H normalize in H; destruct (H) 
          |6: #x #y #H normalize in H; destruct (H)
          |4,5: #id #H //
          ]
        | @le_n ] 
      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
      ]
    ] 
  ] ]
| @conj [ @conj
  [ #i #Hi //
  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2
                   normalize in H2; destruct (H2) ]
  ]                 
  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
]
qed.
 
let rec jump_expansion_internal (program: list labelled_instruction)
  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
    And
    (∀i:ℕ.i ≥ |program| → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
    (jump_in_policy program policy)) ≝
  match n with
  [ O   ⇒ jump_expansion_start program
  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
  ].
[ @(sig2 … (jump_expansion_start program))
| @(proj1 … (sig2 … (jump_expansion_step program (jump_expansion_internal program m))))
]
qed.

definition policy_equal ≝
  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
  ∀n:ℕ.n < |program| →
    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) =
    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)).

lemma pe_refl:
  ∀program.reflexive ? (policy_equal program).
 #program whd #x whd #n #Hn @refl
qed.

lemma pe_sym:
  ∀program.symmetric ? (policy_equal program).
 #program whd #x #y #Hxy whd #n #Hn
 >(Hxy n Hn) @refl
qed.

lemma pe_trans:
  ∀program.transitive ? (policy_equal program).
 #program whd #x #y #z #Hxy #Hyz whd #n #Hn
 >(Hxy n Hn) @(Hyz n Hn)
qed.

lemma le_plus:
  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
 #n #m elim m -m;
 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
   | % [ @O | <Hn // ]
   ]
 ]
qed.

theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
#n (elim n) normalize /2 by S_pred/ qed.

lemma pe_step: ∀program:list labelled_instruction.
 ∀p1,p2:Σpolicy.
 (∀i:ℕ.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
 ∧jump_in_policy program policy.
  policy_equal program p1 p2 →
  policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2).
 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
   #Hnotjmp >lookup_opt_lookup_miss
   [ >lookup_opt_lookup_miss
     [ @refl
     | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
       [ @(proj1 ?? (sig2 … (jump_expansion_step program p2)))
       | @Hnotjmp
       ]
     ]
   | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
     [ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1)))
     | @Hnotjmp
     ]
   ]
 | #x #Hl cases daemon
 ]
qed.
    
lemma equal_remains_equal: ∀program:list labelled_instruction.∀n:ℕ.
  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
 #program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H -H -Hk -k;
 lapply Heq -Heq; lapply n -n; elim z -z;
 [ #n #Heq <plus_n_O @pe_refl  
 | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
   [ @Heq
   | @pe_step @Hind @Heq
   ]
 ]
qed.

lemma dec_bounded_forall:
  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
 #P #HP_dec #k elim k -k
 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
 | #k #Hind cases Hind
   [ #Hk cases (HP_dec k)
     [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
       [ #H @(Hk … (le_S_S_to_le … H))
       | #H >(injective_S … H) @HPk
       ]
     | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
     ]
   | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
   ]
 ]
qed.

lemma dec_bounded_exists:
  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
 #P #HP_dec #k elim k -k
 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
 | #k #Hind cases Hind
   [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
   | #Hk cases (HP_dec k)
     [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
     | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
       | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
       ]  
     ]
   ]
 ]
qed.

lemma not_exists_forall:
  ∀A:Type[0].∀P:A → Prop.¬(∃x.P x) → ∀x.¬P x.
 #A #P #Hex #x @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) @Habs
qed.

lemma de_morgan1:
 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.
 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA | @H ] | @Hnot ]
qed.

lemma thingie:
  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
 #A #Adec #nnA cases Adec
 [ //
 | #H @⊥ @(absurd (¬A) H nnA)
 ]
qed.
 
lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
  #a #b cases a cases b /2/
  %2 @nmk #H destruct (H)
qed.

lemma incr_or_equal: ∀program:list labelled_instruction.
  ∀policy:(Σp:jump_expansion_policy.
    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    jump_in_policy program p).
  policy_equal program policy (jump_expansion_step program policy) ∨
  ∃n:ℕ.jmple
    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
 #program #policy cases (dec_bounded_exists
   (λk.
     \snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠
     \snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉))
   ? (|program|))
   [ #H %2 elim H -H; #i #Hi
     cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi))
     [ #H @(ex_intro … i H)
     | #H @⊥ @(absurd ? H (proj2 ?? Hi))
     ]
   | #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H -H #H; @nmk #H2 @H
     @(ex_intro … i) @conj [ @Hi | @H2 ]
   | #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
     (\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)))
     [ #H %2 @nmk #H1 elim H1 #H2 @H2 @H
     | #H %1 @H
     ]
   ]
qed.  

(**************************************** 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) (|\snd program|) in
  let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, 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 costlabel 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 16 ppc) (bitvector_of_nat 16 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.

axiom fetch_pseudo_instruction_split:
 ∀instr_list,ppc.
  ∃pre,suff,lbl.
   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.

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

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_def … (construct_datalabels (\fst program)) x (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 ].
 [ @⊥ whd in p:(??%??);
   generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
   cases (sigma00 ????) in ⊢ (??%? → %); normalize nodelta [#_ * #abs @abs %]
   #res #K
   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?;
   cases daemon (* CSC: XXXXXXXX Ero qui
   
    [3: @policy_ok_prefix_ok ]
    | sigma00 program pol pre



   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
   per concludere construct_costs_safe ≠ None *)
 | >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_def … (construct_datalabels (\fst program)) x (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_def … (construct_datalabels (\fst program)) x (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_def … (construct_datalabels (\fst program)) x (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 costlabel 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 costlabel 16〉 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).

(*
axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.

axiom foldl_strong_step:
 ∀A:Type[0].
  ∀P: list A → Type[0].
   ∀l: list A.
    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
     ∀acc: P [ ].
      ∀Q: ∀prefix. P prefix → Prop.
       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
       Q [ ] acc →
        Q l (foldl_strong A P l H acc).
(*
 #A #P #l #H #acc #Q #HQ #Hacc normalize;
 generalize in match
  (foldl_strong ?
   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
   l ? Hacc)
 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%) 
 #K 

 generalize in match
  (foldl_strong ?
   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
 [2: @H
*)

axiom foldl_elim:
 ∀A:Type[0].
  ∀B: Type[0].
   ∀H: A → B → A.
    ∀acc: A.
     ∀l: list B.
      ∀Q: A → Prop.
       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
         Q acc →
          Q (foldl A B H acc l).
*)

lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
 #A #a #b #EQ destruct //
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)〉.

lemma eq_identifier_eq:
  ∀tag: String.
  ∀l.
  ∀r.
    eq_identifier tag l r = true → l = r.
  #tag #l #r cases l cases r #posl #posr
  cases daemon
qed.

definition build_maps:
 ∀pseudo_program.∀pol:policy pseudo_program.
  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
   let 〈labels, costs〉 ≝ res in
    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     lookup_def … labels id (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:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 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_def … labels id (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
                  add ? ? labels label program_counter_bv
            ]
          in
            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈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 %
   | >append_length <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_identifier ? l id)); cases (eq_identifier … l id) in ⊢ (???% → %);
        [ #EQ #_ <(eq_identifier_eq … EQ) check lookup_add_hit. >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; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
          <(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 build_maps:
 ∀pseudo_program.∀pol:policy pseudo_program.
  Σres:((BitVectorTrie Identifier 16) × (BitVectorTrie costlabel 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 costlabel 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 %
   | >append_length <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; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
          <(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 …〉).