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
  | medium_jump: jump_length
  | long_jump: jump_length.

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.

definition expand_relative_jump_internal_safe:
 Word → jump_length → Word → ([[relative]] → preinstruction [[relative]]) →
 option (list instruction)
 ≝
  λlookup_address,jmp_len.λpc,i.
  match jmp_len with
  [ short_jump ⇒
     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_address)
    ]
  ].
  @ I
qed.

definition rel_jump_length_ok ≝
 λlookup_address:Word.
 λpc:Word.
 Σjump_len:jump_length.
  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
  ∀(*x,*)y. expand_relative_jump_internal_safe lookup_address jump_len (*x*) pc y ≠ None ?.

lemma eject_rel_jump_length: ∀x,y. rel_jump_length_ok x y → jump_length.
 #x #y #p @(pi1 … p)
qed.

coercion eject_rel_jump_length nocomposites:
 ∀x,y.∀pol:rel_jump_length_ok x y. jump_length ≝
 eject_rel_jump_length on _pol:(rel_jump_length_ok ??) to jump_length.

definition expand_relative_jump_internal:
 ∀lookup_address:Word. ∀pc:Word. rel_jump_length_ok lookup_address pc →
  ([[relative]] → preinstruction [[relative]]) →
 list instruction
≝ λlookup_address,pc,jump_len,i.
   match expand_relative_jump_internal_safe lookup_address jump_len pc i
   return λres. res ≠ None ? → ?
   with
   [ None ⇒ λabs.⊥
   | Some res ⇒ λ_.res ] (pi2 … jump_len i).
 cases abs /2/
qed.

definition expand_relative_jump_safe: ∀lookup_labels:Identifier → Word.Word → jump_length → preinstruction Identifier → option (list instruction) ≝
  λlookup_labels.
  λpc: 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_safe (lookup_labels jmp) jmp_len pc (JC ?)
  | JNC jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNC ?)
  | JB baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JB ? baddr)
  | JZ jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JZ ?)
  | JNZ jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNZ ?)
  | JBC baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JBC ? baddr)
  | JNB baddr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (JNB ? baddr)
  | CJNE addr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len pc (CJNE ? addr)
  | DJNZ addr jmp ⇒ expand_relative_jump_internal_safe (lookup_labels jmp) jmp_len 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:
 ∀lookup_labels,pc. jump_length → ? → pseudo_instruction → option (list instruction) ≝
  λlookup_labels.
  λpc.
  λjmp_len.
  λlookup_datalabels.
  λ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_safe lookup_labels pc jmp_len instr
  | Jmp jmp ⇒
    match jmp_len with
    [ short_jump ⇒ 
      let 〈result, flags〉 ≝ sub_16_with_carry pc (lookup_labels jmp) 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 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) 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.

definition jump_length_ok ≝
 λlookup_labels:Identifier → Word.
 λpc:Word.
 Σjump_len:jump_length.
  (* CSC,JPB: Cheating here, use Jaap's better definition select_reljump_length *)
  ∀x,y.expand_pseudo_instruction_safe lookup_labels pc jump_len x y ≠ None ?.

lemma eject_jump_length: ∀x,y. jump_length_ok x y → jump_length.
 #x #y #p @(pi1 … p)
qed.

coercion eject_jump_length nocomposites:
 ∀x,y.∀pol:jump_length_ok x y. jump_length ≝
 eject_jump_length on _pol:(jump_length_ok ??) to jump_length.

definition expand_pseudo_instruction:
 ∀lookup_labels:Identifier → Word. ∀pc:Word. jump_length_ok lookup_labels pc →
 ? → pseudo_instruction → list instruction ≝
 λlookup_labels,pc,jump_len,lookup_datalabels,i.
   match expand_pseudo_instruction_safe lookup_labels pc jump_len lookup_datalabels i
   return λres. res ≠ None ? → ?
   with
   [ None ⇒ λabs.⊥
   | Some res ⇒ λ_.res ] (pi2 … jump_len lookup_datalabels i).
 cases abs /2/
qed.

definition policy_type ≝
 λlookup_labels:Identifier → Word.
 ∀pc:Word. jump_length_ok lookup_labels pc.

definition policy_type2 ≝
 ∀lookup_labels.policy_type lookup_labels.
 
definition assembly_1_pseudoinstruction ≝
  λlookup_labels.
  λjump_expansion: policy_type lookup_labels.
  (*λppc: Word.*)
  λpc: Word.
  λlookup_datalabels.
  λi.
  let expansion ≝ jump_expansion pc in
  let pseudos ≝ expand_pseudo_instruction lookup_labels pc expansion 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 construct_costs ≝
  λprogram_counter: nat.
  λjump_expansion: policy_type (λx.bitvector_of_nat ? program_counter).
  λpseudo_program_counter: nat.
  λcosts: BitVectorTrie costlabel 16.
  λi.
  match i with
  [ Cost cost ⇒
    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
     〈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_datalabels ≝ λx.zero ? in
    let pc_delta_assembled ≝
      assembly_1_pseudoinstruction (λx.pc_bv)
       jump_expansion (*ppc_bv*) pc_bv lookup_datalabels i in
    let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
     〈pc_delta + program_counter, costs〉
  ].
  
axiom nat_of_bitvector_bitvector_of_nat:
  ∀n,v.n < 2^v → nat_of_bitvector v (bitvector_of_nat v n) = n.
  
axiom bitvector_of_nat_nat_of_bitvector:
  ∀n,v.bitvector_of_nat n (nat_of_bitvector n v) = v.

lemma nth_cons:
  ∀n,A,h,t,y.
  nth (S n) A (h::t) y = nth n A t y.
 #n #A #h #t #y /2 by refl/
qed.
  
lemma fetch_pseudo_instruction_prefix:
  ∀prefix.∀x.∀ppc.ppc < (|prefix|) → 
  fetch_pseudo_instruction prefix (bitvector_of_nat ? ppc) =
  fetch_pseudo_instruction (prefix@x) (bitvector_of_nat ? ppc).
 #prefix #x #ppc elim prefix
 [ #Hppc @⊥ @(absurd … Hppc) @le_to_not_lt @le_O_n
 | #h #t #Hind #Hppc whd in match (fetch_pseudo_instruction ??);
   whd in match (fetch_pseudo_instruction ((h::t)@x) ?);
   >nth_append_first
   [ //
   | >nat_of_bitvector_bitvector_of_nat
     [ @Hppc
     | cases daemon (* XXX invariant *)
     ]
   ]
 ]
qed.

(* 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: ∀jump_expansion:policy_type2.∀l:list labelled_instruction.? →
 (Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
  let 〈ppc,pc_map〉 ≝ ppc_pc_map in
  let 〈program_counter, sigma_map〉 ≝ pc_map in
  ppc = |l| ∧
  (ppc = |l| →
   (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
   (∀x.x < |l| →
    ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
   let pc_x ≝ bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
   bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 
   bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
   (\fst
    (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi)))))
 ) ≝ 
 λjump_expansion: policy_type2.
 λl:list labelled_instruction.
 λacc.
  foldl_strong ?
   (λprefix.(Σppc_pc_map:ℕ×(ℕ×(BitVectorTrie Word 16)).
     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     let 〈program_counter, sigma_map〉 ≝ pc_map in
     (ppc = |prefix|) ∧
     (ppc = |prefix| → 
      (bvt_lookup ?? (bitvector_of_nat ? ppc) sigma_map (zero ?) = (bitvector_of_nat ? program_counter)) ∧
      (∀x.x < |prefix| →
       ∀pi.\fst (fetch_pseudo_instruction l (bitvector_of_nat ? x)) = pi →
       let pc_x ≝  bvt_lookup ?? (bitvector_of_nat 16 x) sigma_map (zero ?) in
       bvt_lookup ?? (bitvector_of_nat 16 (S x)) sigma_map (zero ?) = 
       bitvector_of_nat 16 ((nat_of_bitvector ? pc_x) +
       (\fst (assembly_1_pseudoinstruction (λx.pc_x) (jump_expansion (λx.pc_x)) pc_x (λx.zero ?) pi))))))
    )
   l
   (λhd.λi.λtl.λp.λppc_pc_map.
     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     let 〈program_counter, sigma_map〉 ≝ pc_map in
     let 〈label, i〉 ≝ i in
      let 〈pc,ignore〉 ≝ construct_costs program_counter (jump_expansion (λx.bitvector_of_nat ? program_counter)) ppc (Stub …) i in
         〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 (S ppc)) (bitvector_of_nat 16 pc) sigma_map〉〉
   ) acc.
cases i in p; #label #ins #p @pair_elim #new_ppc #x normalize nodelta cases x -x #old_pc #old_map
@pair_elim #new_pc #ignore #Hc #Heq normalize nodelta @conj
[ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
  <(pair_eq1 ?????? Heq) >(proj1 ?? Hind) >append_length <commutative_plus normalize @refl
| #Hnew <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) @conj
  [ >lookup_insert_hit >(pair_eq1 ?????? (pair_eq2 ?????? Heq)) @refl
  | #x <(pair_eq1 ?????? Heq) >append_length <commutative_plus #Hx normalize in Hx;
    #pi #Hpi <(pair_eq2 ?????? (pair_eq2 ?????? Heq)) <(pair_eq1 ?????? Heq) in Hnew;
    >append_length <commutative_plus #Hnew normalize in Hnew; >(injective_S … Hnew)
    elim (le_to_or_lt_eq … Hx) -Hx #Hx
    [ lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta #Hind
      lapply (proj2 ?? ((proj2 ?? Hind) (proj1 ?? Hind)) x (le_S_S_to_le … Hx) pi Hpi)
      -Hind #Hind >lookup_insert_miss
      [2: @bitvector_of_nat_abs
        [3: @lt_to_not_eq @Hx
        |1: @(transitive_le … Hx)
        ]
        cases daemon (* XXX invariant *)
      ]
      >lookup_insert_miss
      [2: @bitvector_of_nat_abs
        [3: @lt_to_not_eq @(transitive_le … (le_S_S_to_le … Hx)) @le_S @le_n
        |1: @(transitive_le … (le_S_S_to_le … Hx))
        ]
        cases daemon (* XXX invariant *)
      ]
      @Hind
    | lapply (pi2 ?? ppc_pc_map) >p1 >p2 normalize nodelta
      #Hind lapply (proj1 ?? ((proj2 ?? Hind) (proj1 ?? Hind))) -Hind
      >(injective_S … Hnew) #Hind <(injective_S … Hx) >lookup_insert_hit >lookup_insert_miss
      [2: @bitvector_of_nat_abs 
        [3: @lt_to_not_eq @le_n
        |1: @(transitive_le ??? (le_n (S x)))
        ]
        cases daemon (* XXX invariant *)
      ]
      >p in Hpi; whd in match (fetch_pseudo_instruction ??); >nth_append_second
      >nat_of_bitvector_bitvector_of_nat >(injective_S … Hx)
      [3: @le_n]
      [2,3: cases daemon (* XXX invariant *)]
      <minus_n_n cases (half_add ???) #x #y normalize nodelta -x -y #Heq <Heq
      whd in match (construct_costs ?????) in Hc; whd in match (assembly_1_pseudoinstruction ?????);
      cases ins in p Hc; normalize nodelta
      [1,2,4,5: #x #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
        [1,3,5,7: @refl
        |2,4,6,8: cases daemon (* XXX invariant *)
        ]
      |3: #c #p >Hind #H <(pair_eq1 ?????? H) >nat_of_bitvector_bitvector_of_nat 
        [2: cases daemon (* XXX invariant *) ]
        whd in match (expand_pseudo_instruction ?????); normalize <plus_n_O @refl
      |6: #x #y #p >Hind #H <(pair_eq1 ?????? H) >commutative_plus >nat_of_bitvector_bitvector_of_nat
        [ @refl
        | cases daemon (* XXX invariant *)
        ]
      ]
    ]
  ]
]
qed.

definition sigma0: pseudo_assembly_program → policy_type2 → (nat × (nat × (BitVectorTrie Word 16))) ≝
  λprog.
  λjump_expansion.
    sigma00 jump_expansion (\snd prog)
    〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub …))〉〉.
 normalize nodelta @conj
 [ / by refl/
 | #H @conj
   [ >lookup_insert_hit @refl
   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
   ]
 ]
qed. 

definition tech_pc_sigma00: pseudo_assembly_program → policy_type2 →
 list labelled_instruction → (nat × nat) ≝
 λprogram,jump_expansion,instr_list.
   let 〈ppc,pc_sigma_map〉 ≝ sigma00 jump_expansion instr_list
   〈0, 〈0, (insert … (bitvector_of_nat ? 0) (bitvector_of_nat ? 0) (Stub ? ?))〉〉 in
   (* acc copied from sigma0 *)
   let 〈pc,map〉 ≝ pc_sigma_map in
     〈ppc,pc〉.
 normalize nodelta @conj
 [ / by refl/
 | #H @conj
   [ >lookup_insert_hit @refl
   | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
   ]
 ]
qed.

definition sigma_safe: pseudo_assembly_program → policy_type2 →
 option (Word → Word) ≝
 λinstr_list,jump_expansion.
  let 〈ppc,pc_sigma_map〉 ≝ sigma0 instr_list jump_expansion 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_type2. policy_ok jump_expansion p.

lemma eject_policy: ∀p. policy p → policy_type2.
 #p #pol @(pi1 … pol)
qed.

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

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

(*CSC: Main axiom here, needs to be proved soon! *)
lemma snd_assembly_1_pseudoinstruction_ok:
 ∀program:pseudo_assembly_program.∀pol: policy program.
 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
  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 →
   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
 #program #pol #ppc #pi #lookup_labels #lookup_datalabels #Hll #Hldl
 whd in match (sigma ???); whd in match (sigma program pol (\snd (half_add ???)));
 whd in match (sigma_safe program pol); whd in match (sigma0 program pol);
 lapply (refl ? (pi1 ?? (sigma00 pol (\snd program)
  «〈0, 〈0, (insert (BitVector 16) 16 (bitvector_of_nat 16 0) (bitvector_of_nat 16 0) (Stub (BitVector 16) 16))〉〉,?»)))
 [ @conj
   [ / by refl/
   | #H >lookup_insert_hit @conj
     [ @refl
     | #x #Hx @⊥ @(absurd … Hx) @le_to_not_lt @le_O_n
     ]
   ]
 | (* here we go *) cases daemon
 ] 
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:
 ∀jump_expansion,l1,l2.
 ∀acc:ℕ×ℕ×(BitVectorTrie Word 16).
  sigma00 jump_expansion (l1@l2) acc =
  sigma00 jump_expansion
    l2 (pi1 ?? (sigma00 jump_expansion l1 acc)).*)

(* lemma sigma00_strict:
 ∀jump_expansion,l,acc. acc = None ? →
  sigma00 jump_expansion l acc = None ….
 #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 (pi2 ?? 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. *)

(* JPB,CSC: this definition is now replaced by the expand_pseudo_instruction higher up
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 pc (lookup_labels pi) lookup_datalabels (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 (pi2 ?? 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)).
   res = assembly_1_pseudoinstruction 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.
   assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
 [ @⊥ 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 (pi2 … (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. pi1 … (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 (pi2 … 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)〉. *)

axiom eq_identifier_eq:
  ∀tag: String.
  ∀l.
  ∀r.
    eq_identifier tag l r = true → l = r.

axiom neq_identifier_neq:
  ∀tag: String.
  ∀l, r: identifier tag.
    eq_identifier tag l r = false → (l = r → False).

definition build_maps0:
 ∀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 (pi1 … pol) pre = 〈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 pc (pol (λx.bitvector_of_nat ? pc)) ppc 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 (pi2 … 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) >lookup_def_add_hit >address_of_word_labels_code_mem_Some_hit
          <IH0 [@IHn1 | <(eq_identifier_eq … EQ) in H; #H @H]
        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_def_add_miss [2: -IHn1;
          (*Andrea:XXXX used to work /2/*)@nmk #IDL lapply (sym_eq ? ? ? IDL)
          lapply (neq_identifier_neq ? ? ? EQ) #ASSM assumption ]
          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ] 
 | generalize in match (pi2 … result) in ⊢ ?;
   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H] *)
 cases daemon
qed.

definition build_maps:
 ∀pseudo_program. policy pseudo_program →
  (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)
 ≝ λpseudo_program,pol. build_maps0 pseudo_program pol.

theorem build_maps_ok:
 ∀pseudo_program.∀pol:policy pseudo_program.
   let 〈labels, costs〉 ≝ build_maps pseudo_program pol 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 @(pi2 … (build_maps0 … pol))
qed.

definition assembly:
 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 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_def … labels x (zero ?) in
    let lookup_datalabels ≝ λx. lookup_def … datalabels x (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 lookup_labels (pol lookup_labels) ppc' 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 lookup_labels (pol lookup_labels) ppc 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〉.
 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 …〉).