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

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


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


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

(* This establishes the correspondence between pseudo program counters and
   program counters. It is at the heart of the proof. *)
(*CSC: code taken from build_maps *)
definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
 λinstr_list.
 λjump_expansion: policy_type.
 λl:list labelled_instruction.
 λacc.
  foldl …
   (λt,i.
       match t with
       [ None ⇒ None …
       | Some ppc_pc_map ⇒
         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
         let 〈program_counter, sigma_map〉 ≝ pc_map in
         let 〈label, i〉 ≝ i in
          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
           [ None ⇒ None ?
           | Some pc_ignore ⇒
              let 〈pc,ignore〉 ≝ pc_ignore in
                Some … 〈S ppc, 〈pc, insert ?? (bitvector_of_nat 16 ppc) (bitvector_of_nat 16 pc) sigma_map〉〉 ]
       ]) acc l.

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

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

definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
 λinstr_list,jump_expansion.
  match sigma0 instr_list jump_expansion with
  [ None ⇒ None ?
  | Some result ⇒
    let 〈ppc,pc_sigma_map〉 ≝ result in
    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
      if gtb pc (2^16) then
        None ?
      else
        Some ? (λx. lookup … x sigma_map (zero …)) ].

(* stuff about policy *)

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

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

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

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

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

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

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

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

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

lemma policy_ok_prefix_ok:
 ∀program.∀pol:policy program.∀suffix,prefix.
  prefix@suffix = \snd program →
   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
 generalize in match (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.

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

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

lemma assembly_1_pseudoinstruction_ok1:
 ∀program:pseudo_assembly_program.∀pol: policy program.
  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
  ∀prf2:lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)).
  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
 cases (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_maps:
 ∀pseudo_program.∀pol:policy pseudo_program.
  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
   let 〈labels, costs〉 ≝ res in
    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
  λpseudo_program.
  λpol:policy pseudo_program.
    let result ≝
      foldl_strong
        (option Identifier × pseudo_instruction)
          (λpre. Σres:((identifier_map ASMTag Word) × (nat × (nat × (BitVectorTrie costlabel 16)))).
            let 〈labels,ppc_pc_costs〉 ≝ res in
            let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
            let 〈pc',costs〉 ≝ pc_costs in
              And ( And (
              And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
                (ppc' = length … pre)) (*∧ *)
                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
                (∀id. occurs_exactly_once id pre →
                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
                (\snd pseudo_program)
        (λprefix,i,tl,prf,t. 
          let 〈labels, ppc_pc_costs〉 ≝ t in
          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
          let 〈pc,costs〉 ≝ pc_costs in
          let 〈label, i'〉 ≝ i in
          let labels ≝
            match label with
            [ None ⇒ labels
            | Some label ⇒
                let program_counter_bv ≝ bitvector_of_nat ? pc in
                  add ? ? labels label program_counter_bv
            ]
          in
            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
    in
      let 〈labels, ppc_pc_costs〉 ≝ result in
      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
      let 〈pc, costs〉 ≝ pc_costs in
        〈labels, costs〉.
 [2: whd generalize in match (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]
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 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
           True)
      instr_list
      (λprefix,hd,tl,prf,pc_ppc_code.
        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
        let 〈ppc, code〉 ≝ ppc_code in
        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
         〈new_pc, 〈new_ppc, (code @ program)〉〉)
      〈(zero ?), 〈(zero ?), [ ]〉〉
    in
     〈\snd (\snd result), costs〉.
 [2,5: %
 |*: cases daemon ]
qed.

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