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".
include "utilities/extralib.ma".

(**************************************** START OF POLICY ABSTRACTION ********************)

(* definition of & operations on jump length *)
inductive jump_length: Type[0] ≝
  | short_jump: jump_length
  | absolute_jump: jump_length
  | long_jump: jump_length.
  
(* Functions that define the conditions under which jumps are possible *)
definition short_jump_cond: Word → Word → (*pseudo_instruction →*) 
  bool × (BitVector 8) ≝
  λpc_plus_jmp_length.λaddr.(*λinstr.*)
  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
  let 〈upper, lower〉 ≝ vsplit ? 9 7 result in
    if get_index' ? 2 0 flags then
      〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉
    else
      〈eq_bv 9 upper (zero …), false:::lower〉.
 
definition absolute_jump_cond: Word → Word → (*pseudo_instruction →*)
  bool × (BitVector 11) ≝ 
  λpc_plus_jmp_length.λaddr.(*λinstr.*)
  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
  〈eq_bv 5 fst_5_addr fst_5_pc, rest_addr〉.

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 ≝ vsplit ? 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 ≝ vsplit ? 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 ≝ vsplit ? 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 ≝ vsplit ? 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 ≝ vsplit ? 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.

(* XXX: pc_plus_sjmp_length used to be just sigma of ppc.  This is incorrect
        as relative lengths are computed from the *end* of the SJMP, not from
        the beginning.
*)
definition expand_relative_jump_internal:
 ∀lookup_labels:Identifier → Word.∀sigma:Word → Word.
 Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
 list instruction
 ≝
  λlookup_labels.λsigma.λlbl.λppc,i.
   let lookup_address ≝ sigma (lookup_labels lbl) in
   let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
   let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
   if sj_possible
   then
     let address ≝ RELATIVE disp in
       [ RealInstruction (i address) ]
   else
    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
      LJMP (ADDR16 lookup_address)
    ].
  %
qed.

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

definition expand_pseudo_instruction:
    ∀lookup_labels.
    ∀sigma: Word → Word.
    ∀policy: Word → bool.
      Word → ? → pseudo_instruction → list instruction ≝
  λlookup_labels: Identifier → Word.
  λsigma: Word → Word.
  λpolicy: Word → bool.
  λppc.
  λlookup_datalabels:Identifier → Word.
  λi.
  match i with
  [ Cost cost ⇒ [ ]
  | Comment comment ⇒ [ ]
  | Call call ⇒
    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    let lookup_address ≝ sigma (lookup_labels call) in
    let 〈mj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
    let do_a_long ≝ policy ppc in
    if mj_possible ∧ ¬ do_a_long then
      let address ≝ ADDR11 disp in
        [ ACALL address ]
    else
      let address ≝ ADDR16 lookup_address in
        [ LCALL address ]
  | Mov d trgt ⇒ 
    let address ≝ DATA16 (lookup_datalabels trgt) in
      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
  | Instruction instr ⇒ expand_relative_jump lookup_labels sigma ppc instr
  | Jmp jmp ⇒
    let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in
    let do_a_long ≝ policy ppc in
    let lookup_address ≝ sigma (lookup_labels jmp) in
    let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length lookup_address in
    if sj_possible ∧ ¬ do_a_long then
      let address ≝ RELATIVE disp in
        [ SJMP address ]
    else
      let 〈mj_possible, disp2〉 ≝ absolute_jump_cond pc_plus_jmp_length lookup_address in
      if mj_possible ∧ ¬ do_a_long then
        let address ≝ ADDR11 disp2 in
          [ AJMP address ]
      else    
        let address ≝ ADDR16 lookup_address in
        [ LJMP address ]
  ].
  %
qed.
 
definition assembly_1_pseudoinstruction ≝
  λlookup_labels.
  λsigma: Word → Word.
  λpolicy: Word → bool.
  λppc: Word.
  λlookup_datalabels.
  λi.
  let pseudos ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in
  let mapped ≝ map ? ? assembly1 pseudos in
  let flattened ≝ flatten ? mapped in
  let pc_len ≝ length ? flattened in
   〈pc_len, flattened〉.

definition instruction_size ≝
  λlookup_labels.
  λsigma: Word → Word.
  λpolicy: Word → bool.
  λppc.
  λi.
    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).

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

(* Labels *) 
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:list labelled_instruction.∀l:Identifier.
  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 cases H 
 | #h #t #IH #i cases i -i 
   [ cases h #hi #hp cases hi
     [ normalize #H cases H
     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
       whd in Heq; >Heq
       >eq_identifier_refl / by 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 / by /
       | normalize #_ @(IH i) @H
       ]
     ]
   ]
 ]
qed.

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

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

theorem create_label_cost_map_ok:
 ∀pseudo_program: pseudo_assembly_program.
   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
qed.

definition sigma_policy_specification ≝
  λprogram: pseudo_assembly_program.
  λsigma: Word → Word.
  λpolicy: Word → bool.
  sigma (zero …) = zero … ∧
  let instr_list ≝ \snd program in
  ∀ppc: Word. ∀ppc_ok: nat_of_bitvector … ppc < |instr_list|.
    let pc ≝ sigma ppc in
    let labels ≝ \fst (create_label_cost_map instr_list) in
    let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in
    let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in
     next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))
     ∧
     (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16
     ∨
     S (nat_of_bitvector … ppc) = |instr_list| ∧
     nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).


lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
 ∀lookup_labels,sigma,policy,ppc,pi.
  ∀lookup_datalabels1,lookup_datalabels2.
   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels1 pi) =
   \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels2 pi).
#lookup_labels #sigma #policy #ppc #pi #lookup_datalabels1 #lookup_datalabels2
cases pi //
qed.

lemma fst_snd_assembly_1_pseudoinstruction:
 ∀lookup_labels,sigma,policy,ppc,pi,lookup_datalabels,len,assembled.
   assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi
   = 〈len,assembled〉 →
    len = |assembled|.
#lookup #sigma #policy #ppc #pi #lookup_datalabels #len #assembled
inversion (assembly_1_pseudoinstruction ??????) #len' #assembled'
whd in ⊢ (??%? → ?); #EQ1 #EQ2 destruct %
qed.

(* XXX: easy but tedious *)
lemma assembly1_lt_128:
  ∀i: instruction.
    |(assembly1 i)| < 128.
  cases daemon
(* XXX: commented out as takes ages to type check 
  #i cases i
  try (#assm1 #assm2) try #assm1
  [8:
    cases assm1
    try (#assm1 #assm2) try #assm1
    whd in match assembly1; normalize nodelta
    whd in match assembly_preinstruction; normalize nodelta
    try @(subaddressing_mode_elim … assm2)
    try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta
    [32:
      cases assm1 -assm1 #assm1 normalize nodelta
      cases assm1 #addr1 #addr2 normalize nodelta
      [1:
        @(subaddressing_mode_elim … addr2)
      |2:
        @(subaddressing_mode_elim … addr1)
      ]
      #w
    |35,36,37:
      cases assm1 -assm1 #assm1 normalize nodelta
      [1,3:
        cases assm1 -assm1 #assm1 normalize nodelta
      ]
      cases assm1 #addr1 #addr2 normalize nodelta
      @(subaddressing_mode_elim … addr2) try #w
    |49:
      cases assm1 -assm1 #assm1 normalize nodelta
      [1:
        cases assm1 -assm1 #assm1 normalize nodelta
        [1:
          cases assm1 -assm1 #assm1 normalize nodelta
          [1:
            cases assm1 -assm1 #assm1 normalize nodelta
            [1:
              cases assm1 -assm1 #assm1 normalize nodelta
            ]
          ]
        ]
      ]
      cases assm1 #addr1 #addr2 normalize nodelta
      [1,3,4,5:
        @(subaddressing_mode_elim … addr2) try #w
      |*:
        @(subaddressing_mode_elim … addr1) try #w
        normalize nodelta
        [1,2:
          @(subaddressing_mode_elim … addr2) try #w
        ]
      ]
    |50:
      cases assm1 -assm1 #assm1 normalize nodelta
      cases assm1 #addr1 #addr2 normalize nodelta
      [1:
        @(subaddressing_mode_elim … addr2) try #w
      |2:
        @(subaddressing_mode_elim … addr1) try #w
      ]
    ]
    normalize repeat @le_S_S @le_O_n
  ]
  whd in match assembly1; normalize nodelta
  [6:
    normalize repeat @le_S_S @le_O_n
  |7:
    @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n
  |*:
    @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n
  ]
  *)
qed.

lemma assembly1_pseudoinstruction_lt_2_to_16:
  ∀lookup_labels,sigma,policy,ppc,lookup_datalabels,pi.
  |\snd (assembly_1_pseudoinstruction
    lookup_labels sigma policy ppc lookup_datalabels pi)|
   < 2^16.
 #lookup_labels #sigma #policy #ppc #lookup_datalabels *
[ cut (128 < 2^16) [@leb_true_to_le %] #LT
  * whd in match (assembly_1_pseudoinstruction ??????);
  whd in match (expand_pseudo_instruction ??????);
  whd in match assembly_1_pseudoinstruction; normalize nodelta
  try (#arg1 #arg2 #arg3) try (#arg1 #arg2) try #arg1
  whd in match (expand_pseudo_instruction ??????);
  try
   (change with (|flatten ? [assembly1 ?]| < ?)
    >flatten_singleton
    @(transitive_lt … (assembly1_lt_128 ?))
    @LT)
  @pair_elim #x #y #_ cases x normalize nodelta
  try
   (change with (|flatten ? [assembly1 ?]| < ?)
    >flatten_singleton
    @(transitive_lt … (assembly1_lt_128 ?))
    @LT)
  change with (|flatten ? [assembly1 ?; assembly1 ?; assembly1 ?]| < ?)
  >length_flatten_cons >length_flatten_cons >length_flatten_cons <plus_n_O
  <associative_plus @(transitive_lt … (tech_transitive_lt_3 … (2^7) ???))
  try @assembly1_lt_128 @leb_true_to_le %
|2,3: #msg normalize in ⊢ (?%?); //
| #label whd in match (assembly_1_pseudoinstruction ??????);
  whd in match (expand_pseudo_instruction ??????);
  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
  [2: @pair_elim #x #y #_ cases (?∧?)]
  normalize in ⊢ (?%?); //
| #label whd in match (assembly_1_pseudoinstruction ??????);
  whd in match (expand_pseudo_instruction ??????);
  @pair_elim #sj_poss #disp cases (?∧?) normalize nodelta #_
  normalize in ⊢ (?%?); //
| #dptr #id normalize in ⊢ (?%?); //
]
qed.

definition assembly:
    ∀p: pseudo_assembly_program.
    ∀sigma: Word → Word.
    ∀policy: Word → bool.
      Σres:list Byte × (BitVectorTrie costlabel 16).
       sigma_policy_specification p sigma policy →
       let 〈preamble,instr_list〉 ≝ p in
       |instr_list| ≤ 2^16 →
       let 〈assembled,costs〉 ≝ res in
       |assembled| ≤ 2^16 ∧
       (nat_of_bitvector … (sigma (bitvector_of_nat … (|instr_list|))) = |assembled| ∨
        sigma (bitvector_of_nat … (|instr_list|)) = zero … ∧ |assembled| = 2^16) ∧
       let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in
       let datalabels ≝ construct_datalabels preamble in
       let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
       let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
       ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|.
         let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc ppc_ok in
         let 〈len,assembledi〉 ≝
          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
         |assembledi| ≤ |assembled| ∧
         ∀j:nat. ∀H: j < |assembledi|. ∀K.
          nth_safe ? j assembledi H =
           nth_safe ? (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat ? j)))
            assembled K
≝
  λp.
  λsigma.
  λpolicy.
  deplet 〈preamble, instr_list〉 as p_refl ≝ p in
  deplet 〈labels_to_ppc,ppc_to_costs〉 as eq_create_label_cost_map ≝ create_label_cost_map instr_list in
  let datalabels ≝ construct_datalabels preamble in
  let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in
  let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in
  let 〈next_pc,revcode〉 ≝ pi1 … (
     foldl_strong
      (option Identifier × pseudo_instruction)
      (λpre. Σppc_code:(Word × (list Byte)).
       sigma_policy_specification 〈preamble,instr_list〉 sigma policy →
        |instr_list| ≤ 2^16 →
        let 〈ppc,code〉 ≝ ppc_code in
         ppc = bitvector_of_nat … (|pre|) ∧
         |code| ≤ 2^16 ∧
         (|code| = 2^16 → |pre| = |instr_list|) ∧
         (nat_of_bitvector … (sigma ppc) = |code| ∨
          sigma ppc = zero … ∧ |code| = 2^16) ∧
         ∀ppc'.∀ppc_ok'.
          (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) →
           let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in
           let 〈len,assembledi〉 ≝
            assembly_1_pseudoinstruction lookup_labels sigma policy ppc' lookup_datalabels pi in
           |assembledi| ≤ |reverse … code| ∧
           ∀j:nat. ∀H: j < |assembledi|. ∀K.
            nth_safe ? j assembledi H =
             nth_safe ? (nat_of_bitvector … (add … (sigma ppc') (bitvector_of_nat ? j))) (reverse … code) K)
      instr_list
      (λprefix,hd,tl,prf,ppc_code.
        let 〈ppc, code〉 ≝ pi1 … ppc_code in
        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels (\snd hd) in
        let new_ppc ≝ add ? ppc (bitvector_of_nat ? 1) in
         〈new_ppc, (reverse … program @ code)〉)
      〈(zero ?), [ ]〉)
    in
     〈reverse … revcode,
      fold … (λppc.λcost.λpc_to_costs. insert … (sigma ppc) cost pc_to_costs) ppc_to_costs (Stub ??)〉.
  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
    cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 #Hfold2 whd
    <eq_create_label_cost_map whd %
    [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16)
      [ #limit %2 @limit
      | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
        @not_eq_to_le_to_lt assumption ]
    | >length_reverse % try assumption cases Hfold3 -Hfold3
      [ #Hfold3 <Hfold3 % >Hfold1 %
      | #Hfold5 %2 <Hfold1 assumption ]]
  | * #sigma_pol_ok1 #_ #instr_list_ok %
    [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]]
    #ppc' #ppc_ok' #abs @⊥ cases abs
     [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip]
     |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ]
  | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code
    #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH
    * * * #IH1 #IH2 #IH4 *
    [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append
        >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X
        lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')]
    #IH3 #IH5
    cut (|prefix| < |instr_list|)
    [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list
    cut (|prefix| < 2^16)
    [ @(lt_to_le_to_lt … (|instr_list|)) assumption ] #prefix_ok
    cut (nat_of_bitvector … ppc < |instr_list|)
    [ >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ] #ppc_ok
    cut (\snd hd = \fst (fetch_pseudo_instruction instr_list ppc ppc_ok))
    [ >prf in ppc_ok; >IH1 >(add_zero … (bitvector_of_nat … (|prefix|)))
      >fetch_pseudo_instruction_append
      [ #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
        whd in match (nth_safe ????); [ cases hd // | normalize // ]
      | <add_zero >nat_of_bitvector_bitvector_of_nat_inverse
        [ <prf assumption | assumption ]
      | skip
      | <prf assumption
      ]] #eq_fetch_pseudo_instruction
    lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
    cut (pc_delta < 2^16)
    [ >EQpc_delta
      @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2)
      @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok
    cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
    [ whd in match instruction_size; normalize nodelta
      >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ]
    #EQpc_delta2
    cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2
    <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2
    #sigma_pol3 #sigma_pol4
    % [ % [% [% ] ] ]
    [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat
    | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus
      cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ]
    | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
       #abs >abs in sigma_pol4; *
       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
         >nat_of_bitvector_bitvector_of_nat_inverse // ]
    | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4
      [ #LT %1 >sigma_pol3 >nat_of_bitvector_add
        [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption]
        >nat_of_bitvector_bitvector_of_nat_inverse try assumption //
      | * #EQ1 #EQ2 %2 %
        [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus
          >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
        | >commutative_plus assumption ]]
  | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
    #EQpc_delta2 #eq_fetch_pseudo_instruction *
    [2: #eq_S_prefix_bound (*@(IH5 ? LTppc')
      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
      @pair_elim*) cases daemon
    | #LTppc_ppc
      cases (le_to_or_lt_eq … LTppc_ppc)
      [2: #S_S_eq normalize nodelta in S_S_eq;
          (*CSC: TRUE, NEEDS SOME WORK *)
          cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf
          >IH1 #LTppc lapply LTppc
          >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
          >fetch_pseudo_instruction_append
          [3: @le_S_S @le_O_n
          |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
          |4: <prf <p_refl in instr_list_ok; #H @H ]
          #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
          [ >length_reverse >length_append >length_reverse // ]
          #j #LTj >nat_of_bitvector_add
          >nat_of_bitvector_bitvector_of_nat_inverse
          [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
          >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
          @nth_safe_prepend
      | #LTppc''
        cut (nat_of_bitvector … ppc' < |instr_list|)
        [ normalize nodelta in LTppc'';
          @(transitive_le … (nat_of_bitvector … ppc))
          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse //
          | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
            [ >commutative_plus #H @H
            | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
              @(transitive_le … instr_list_ok)
              >IH1 >nat_of_bitvector_bitvector_of_nat_inverse [2: assumption ]
              >prf >length_append >length_append <plus_n_Sm @le_S_S normalize
              cases daemon (*CSC: ????
              
               >prf >length_append @le_S_S >(commutative_plus (|prefix|))
              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
              [2: <p_refl in instr_list_ok; >prf >length_append #H
                  @(transitive_le … H) //
              | @le_S_S //*) ]]]]
      #X lapply (IH5 ppc' X)
      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
      cases (IH ?)
      [2: cases daemon (*CSC: new proof obligation*) ] #IH6 #IH
      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?)
      >eq_assembly_1_pseudoinstruction %
      [ cases daemon (*CSC: new proof obligation*)
      | #j #LTj >reverse_append >reverse_reverse #K
        >IH
        [2: >length_reverse <IH3 (*CSC: USE MONOTONICITY *) cases daemon
        | @shift_nth_prefix ]]]]]
(*        |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
           [ >commutative_plus %
           | >commutative_plus >IH1 whd in ⊢ (?%?);
             @(transitive_le … (S (|instr_list|)))
             [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
             | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
               [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
*)
qed.

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