Changeset 1614


Ignore:
Timestamp:
Dec 14, 2011, 5:00:45 PM (8 years ago)
Author:
boender
Message:
  • split policy from assembly
Location:
src/ASM
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1613 r1614  
    66include alias "arithmetics/nat.ma".
    77include "utilities/extralib.ma".
    8 
    9 definition assembly_preinstruction ≝
    10   λA: Type[0].
    11   λaddr_of: A → Byte. (* relative *)
    12   λpre: preinstruction A.
    13   match pre with
    14   [ ADD addr1 addr2 ⇒
    15      match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    16       [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
    17       | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
    18       | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
    19       | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
    20       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    21   | ADDC addr1 addr2 ⇒
    22      match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    23       [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
    24       | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
    25       | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
    26       | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
    27       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    28   | ANL addrs ⇒
    29      match addrs with
    30       [ inl addrs ⇒ match addrs with
    31          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    32            match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    33             [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    34             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
    35             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
    36             | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
    37             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    38          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    39             let b1 ≝
    40              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    41               [ DIRECT b1 ⇒ λ_.b1
    42               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    43             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
    44              [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
    45              | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
    46              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    47          ]
    48       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    49          match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    50           [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
    51           | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
    52           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    53   | CLR addr ⇒
    54      match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
    55       [ ACC_A ⇒ λ_.
    56          [ ([[true; true; true; false; false; true; false; false]]) ]
    57       | CARRY ⇒ λ_.
    58          [ ([[true; true; false; false; false; false; true; true]]) ]
    59       | BIT_ADDR b1 ⇒ λ_.
    60          [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
    61       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    62   | CPL addr ⇒
    63      match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
    64       [ ACC_A ⇒ λ_.
    65          [ ([[true; true; true; true; false; true; false; false]]) ]
    66       | CARRY ⇒ λ_.
    67          [ ([[true; false; true; true; false; false; true; true]]) ]
    68       | BIT_ADDR b1 ⇒ λ_.
    69          [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
    70       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    71   | DA addr ⇒
    72      [ ([[true; true; false; true; false; true; false; false]]) ]
    73   | DEC addr ⇒
    74      match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
    75       [ ACC_A ⇒ λ_.
    76          [ ([[false; false; false; true; false; true; false; false]]) ]
    77       | REGISTER r ⇒ λ_.
    78          [ ([[false; false; false; true; true]]) @@ r ]
    79       | DIRECT b1 ⇒ λ_.
    80          [ ([[false; false; false; true; false; true; false; true]]); b1 ]
    81       | INDIRECT i1 ⇒ λ_.
    82          [ ([[false; false; false; true; false; true; true; i1]]) ]
    83       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    84       | DJNZ addr1 addr2 ⇒
    85          let b2 ≝ addr_of addr2 in
    86          match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
    87           [ REGISTER r ⇒ λ_.
    88              [ ([[true; true; false; true; true]]) @@ r ; b2 ]
    89           | DIRECT b1 ⇒ λ_.
    90              [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
    91           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    92       | JC addr ⇒
    93         let b1 ≝ addr_of addr in
    94           [ ([[false; true; false; false; false; false; false; false]]); b1 ]
    95       | JNC addr ⇒
    96          let b1 ≝ addr_of addr in
    97            [ ([[false; true; false; true; false; false; false; false]]); b1 ]
    98       | JZ addr ⇒
    99          let b1 ≝ addr_of addr in
    100            [ ([[false; true; true; false; false; false; false; false]]); b1 ]
    101       | JNZ addr ⇒
    102          let b1 ≝ addr_of addr in
    103            [ ([[false; true; true; true; false; false; false; false]]); b1 ]
    104       | JB addr1 addr2 ⇒
    105          let b2 ≝ addr_of addr2 in
    106          match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    107           [ BIT_ADDR b1 ⇒ λ_.
    108              [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
    109           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    110       | JNB addr1 addr2 ⇒
    111          let b2 ≝ addr_of addr2 in
    112          match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    113           [ BIT_ADDR b1 ⇒ λ_.
    114              [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
    115           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    116       | JBC addr1 addr2 ⇒
    117          let b2 ≝ addr_of addr2 in
    118          match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    119           [ BIT_ADDR b1 ⇒ λ_.
    120              [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
    121           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    122       | CJNE addrs addr3 ⇒
    123          let b3 ≝ addr_of addr3 in
    124          match addrs with
    125           [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    126              match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
    127               [ DIRECT b1 ⇒ λ_.
    128                  [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
    129               | DATA b1 ⇒ λ_.
    130                  [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
    131               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    132           | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    133              let b2 ≝
    134               match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
    135                [ DATA b2 ⇒ λ_. b2
    136                | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    137              match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
    138               [ REGISTER r ⇒ λ_.
    139                  [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
    140               | INDIRECT i1 ⇒ λ_.
    141                  [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
    142               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
    143          ]
    144   | DIV addr1 addr2 ⇒
    145      [ ([[true;false;false;false;false;true;false;false]]) ]
    146   | INC addr ⇒
    147      match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
    148       [ ACC_A ⇒ λ_.
    149          [ ([[false;false;false;false;false;true;false;false]]) ]         
    150       | REGISTER r ⇒ λ_.
    151          [ ([[false;false;false;false;true]]) @@ r ]
    152       | DIRECT b1 ⇒ λ_.
    153          [ ([[false; false; false; false; false; true; false; true]]); b1 ]
    154       | INDIRECT i1 ⇒ λ_.
    155         [ ([[false; false; false; false; false; true; true; i1]]) ]
    156       | DPTR ⇒ λ_.
    157         [ ([[true;false;true;false;false;false;true;true]]) ]
    158       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    159   | MOV addrs ⇒
    160      match addrs with
    161       [ inl addrs ⇒
    162          match addrs with
    163           [ inl addrs ⇒
    164              match addrs with
    165               [ inl addrs ⇒
    166                  match addrs with
    167                   [ inl addrs ⇒
    168                      match addrs with
    169                       [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    170                          match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    171                           [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    172                           | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
    173                           | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
    174                           | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
    175                           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    176                       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    177                          match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
    178                           [ REGISTER r ⇒ λ_.
    179                              match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
    180                               [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
    181                               | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
    182                               | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
    183                               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    184                           | INDIRECT i1 ⇒ λ_.
    185                              match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
    186                               [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
    187                               | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
    188                               | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
    189                               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    190                           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    191                   | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    192                      let b1 ≝
    193                       match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    194                        [ DIRECT b1 ⇒ λ_. b1
    195                        | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    196                      match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
    197                       [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    198                       | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
    199                       | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
    200                       | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
    201                       | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
    202                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    203               | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    204                  match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    205                   [ DATA16 w ⇒ λ_.
    206                      let b1_b2 ≝ split ? 8 8 w in
    207                      let b1 ≝ \fst b1_b2 in
    208                      let b2 ≝ \snd b1_b2 in
    209                       [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
    210                   | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    211           | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    212              match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    213               [ BIT_ADDR b1 ⇒ λ_.
    214                  [ ([[true;false;true;false;false;false;true;false]]); b1 ]
    215               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    216       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    217          match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    218           [ BIT_ADDR b1 ⇒ λ_.
    219              [ ([[true;false;false;true;false;false;true;false]]); b1 ]
    220           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    221   | MOVX addrs ⇒
    222      match addrs with
    223       [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    224          match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    225           [ EXT_INDIRECT i1 ⇒ λ_.
    226              [ ([[true;true;true;false;false;false;true;i1]]) ]
    227           | EXT_INDIRECT_DPTR ⇒ λ_.
    228              [ ([[true;true;true;false;false;false;false;false]]) ]
    229           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    230       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    231          match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    232           [ EXT_INDIRECT i1 ⇒ λ_.
    233              [ ([[true;true;true;true;false;false;true;i1]]) ]
    234           | EXT_INDIRECT_DPTR ⇒ λ_.
    235              [ ([[true;true;true;true;false;false;false;false]]) ]
    236           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    237   | MUL addr1 addr2 ⇒
    238      [ ([[true;false;true;false;false;true;false;false]]) ]
    239   | NOP ⇒
    240      [ ([[false;false;false;false;false;false;false;false]]) ]
    241   | ORL addrs ⇒
    242      match addrs with
    243       [ inl addrs ⇒
    244          match addrs with
    245           [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    246              match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
    247              [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    248              | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
    249              | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
    250              | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
    251              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    252           | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    253             let b1 ≝
    254               match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    255                [ DIRECT b1 ⇒ λ_. b1
    256                | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    257              match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
    258               [ ACC_A ⇒ λ_.
    259                  [ ([[false;true;false;false;false;false;true;false]]); b1 ]
    260               | DATA b2 ⇒ λ_.
    261                  [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
    262               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    263       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
    264          match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    265           [ BIT_ADDR b1 ⇒ λ_.
    266              [ ([[false;true;true;true;false;false;true;false]]); b1 ]
    267           | N_BIT_ADDR b1 ⇒ λ_.
    268              [ ([[true;false;true;false;false;false;false;false]]); b1 ]
    269           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    270   | POP addr ⇒
    271      match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    272       [ DIRECT b1 ⇒ λ_.
    273          [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
    274       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    275   | PUSH addr ⇒
    276      match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    277       [ DIRECT b1 ⇒ λ_.
    278          [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
    279       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    280   | RET ⇒
    281      [ ([[false;false;true;false;false;false;true;false]]) ]
    282   | RETI ⇒
    283      [ ([[false;false;true;true;false;false;true;false]]) ]
    284   | RL addr ⇒
    285      [ ([[false;false;true;false;false;false;true;true]]) ]
    286   | RLC addr ⇒
    287      [ ([[false;false;true;true;false;false;true;true]]) ]
    288   | RR addr ⇒
    289      [ ([[false;false;false;false;false;false;true;true]]) ]
    290   | RRC addr ⇒
    291      [ ([[false;false;false;true;false;false;true;true]]) ]
    292   | SETB addr ⇒     
    293      match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
    294       [ CARRY ⇒ λ_.
    295          [ ([[true;true;false;true;false;false;true;true]]) ]
    296       | BIT_ADDR b1 ⇒ λ_.
    297          [ ([[true;true;false;true;false;false;true;false]]); b1 ]
    298       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    299   | SUBB addr1 addr2 ⇒
    300      match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    301       [ REGISTER r ⇒ λ_.
    302          [ ([[true;false;false;true;true]]) @@ r ]
    303       | DIRECT b1 ⇒ λ_.
    304          [ ([[true;false;false;true;false;true;false;true]]); b1]
    305       | INDIRECT i1 ⇒ λ_.
    306          [ ([[true;false;false;true;false;true;true;i1]]) ]
    307       | DATA b1 ⇒ λ_.
    308          [ ([[true;false;false;true;false;true;false;false]]); b1]
    309       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    310   | SWAP addr ⇒
    311      [ ([[true;true;false;false;false;true;false;false]]) ]
    312   | XCH addr1 addr2 ⇒
    313      match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
    314       [ REGISTER r ⇒ λ_.
    315          [ ([[true;true;false;false;true]]) @@ r ]
    316       | DIRECT b1 ⇒ λ_.
    317          [ ([[true;true;false;false;false;true;false;true]]); b1]
    318       | INDIRECT i1 ⇒ λ_.
    319          [ ([[true;true;false;false;false;true;true;i1]]) ]
    320       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    321   | XCHD addr1 addr2 ⇒
    322      match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
    323       [ INDIRECT i1 ⇒ λ_.
    324          [ ([[true;true;false;true;false;true;true;i1]]) ]
    325       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    326   | XRL addrs ⇒
    327      match addrs with
    328       [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    329          match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
    330           [ REGISTER r ⇒ λ_.
    331              [ ([[false;true;true;false;true]]) @@ r ]
    332           | DIRECT b1 ⇒ λ_.
    333              [ ([[false;true;true;false;false;true;false;true]]); b1]
    334           | INDIRECT i1 ⇒ λ_.
    335              [ ([[false;true;true;false;false;true;true;i1]]) ]
    336           | DATA b1 ⇒ λ_.
    337              [ ([[false;true;true;false;false;true;false;false]]); b1]
    338           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    339       | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    340          let b1 ≝
    341           match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    342            [ DIRECT b1 ⇒ λ_. b1
    343            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    344          match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
    345           [ ACC_A ⇒ λ_.
    346              [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
    347           | DATA b2 ⇒ λ_.
    348              [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
    349           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    350        ].
    351 
    352 definition assembly1 ≝
    353  λi: instruction.
    354  match i with
    355   [ ACALL addr ⇒
    356      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    357       [ ADDR11 w ⇒ λ_.
    358          let v1_v2 ≝ split ? 3 8 w in
    359          let v1 ≝ \fst v1_v2 in
    360          let v2 ≝ \snd v1_v2 in
    361           [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    362       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    363   | AJMP addr ⇒
    364      match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    365       [ ADDR11 w ⇒ λ_.
    366          let v1_v2 ≝ split ? 3 8 w in
    367          let v1 ≝ \fst v1_v2 in
    368          let v2 ≝ \snd v1_v2 in
    369           [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    370       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    371   | JMP adptr ⇒
    372      [ ([[false;true;true;true;false;false;true;true]]) ]
    373   | LCALL addr ⇒
    374      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    375       [ ADDR16 w ⇒ λ_.
    376          let b1_b2 ≝ split ? 8 8 w in
    377          let b1 ≝ \fst b1_b2 in
    378          let b2 ≝ \snd b1_b2 in
    379           [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    380       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    381   | LJMP addr ⇒
    382      match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    383       [ ADDR16 w ⇒ λ_.
    384          let b1_b2 ≝ split ? 8 8 w in
    385          let b1 ≝ \fst b1_b2 in
    386          let b2 ≝ \snd b1_b2 in
    387           [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    388       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    389   | MOVC addr1 addr2 ⇒
    390      match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
    391       [ ACC_DPTR ⇒ λ_.
    392          [ ([[true;false;false;true;false;false;true;true]]) ]
    393       | ACC_PC ⇒ λ_.
    394          [ ([[true;false;false;false;false;false;true;true]]) ]
    395       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    396   | SJMP addr ⇒
    397      match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
    398       [ RELATIVE b1 ⇒ λ_.
    399          [ ([[true;false;false;false;false;false;false;false]]); b1 ]
    400       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    401   | RealInstruction instr ⇒
    402     assembly_preinstruction [[ relative ]]
    403       (λx.
    404         match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
    405         [ RELATIVE r ⇒ λ_. r
    406         | _ ⇒ λabsd. ⊥
    407         ] (subaddressing_modein … x)) instr
    408   ].
    409   cases absd
    410 qed.
    411 
    412 (* definition of & operations on jump length *)
    413 inductive jump_length: Type[0] ≝
    414   | short_jump: jump_length
    415   | medium_jump: jump_length
    416   | long_jump: jump_length.
    417 
    418 definition max_length: jump_length → jump_length → jump_length ≝
    419   λj1.λj2.
    420   match j1 with
    421   [ long_jump   ⇒ long_jump
    422   | medium_jump ⇒
    423     match j2 with
    424     [ long_jump ⇒ long_jump
    425     | _         ⇒ medium_jump
    426     ]
    427   | short_jump  ⇒ j2
    428   ].
    429 
    430 definition jmple: jump_length → jump_length → Prop ≝
    431   λj1.λj2.
    432   match j1 with
    433   [ short_jump  ⇒
    434     match j2 with
    435     [ short_jump ⇒ False
    436     | _          ⇒ True
    437     ]
    438   | medium_jump ⇒
    439     match j2 with
    440     [ long_jump ⇒ True
    441     | _         ⇒ False
    442     ]
    443   | long_jump   ⇒ False
    444   ].
    445 
    446 definition jmpleq: jump_length → jump_length → Prop ≝
    447   λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    448  
    449 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
    450  #x #y cases x cases y /3 by inl, inr, nmk, I/
    451 qed.
    452  
    453 lemma jmpleq_max_length: ∀ol,nl.
    454   jmpleq ol (max_length ol nl).
    455  #ol #nl cases ol cases nl
    456  /2 by or_introl, or_intror, I/
    457 qed.
    458 
    459 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
    460   #a #b cases a cases b /2/
    461   %2 @nmk #H destruct (H)
    462 qed.
    463 
    464  
    465 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
    466 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
    467 
    468 definition expand_relative_jump_internal:
    469  (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
    470  option (list instruction)
    471  ≝
    472   λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
    473   match jmp_len with
    474   [ short_jump ⇒
    475      let lookup_address ≝ lookup_labels jmp in
    476      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    477      let 〈upper, lower〉 ≝ split ? 8 8 result in
    478      if eq_bv ? upper (zero 8) then
    479       let address ≝ RELATIVE lower in
    480        Some ? [ RealInstruction (i address) ]
    481      else
    482        None ?
    483   | medium_jump ⇒ None …
    484   | long_jump ⇒
    485     Some ?
    486     [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
    487       SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
    488       LJMP (ADDR16 (lookup_labels jmp))
    489     ]
    490   ].
    491   @ I
    492 qed.
    493 
    494 definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
    495   λlookup_labels.
    496   λjmp_len: jump_length.
    497   λpc.
    498   λi: preinstruction Identifier.
    499   let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
    500   match i with
    501   [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
    502   | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
    503   | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
    504   | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
    505   | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
    506   | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
    507   | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
    508   | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
    509   | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
    510   | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
    511   | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
    512   | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
    513   | INC arg ⇒ Some ? [ INC ? arg ]
    514   | DEC arg ⇒ Some ? [ DEC ? arg ]
    515   | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
    516   | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
    517   | DA arg ⇒ Some ? [ DA ? arg ]
    518   | ANL arg ⇒ Some ? [ ANL ? arg ]
    519   | ORL arg ⇒ Some ? [ ORL ? arg ]
    520   | XRL arg ⇒ Some ? [ XRL ? arg ]
    521   | CLR arg ⇒ Some ? [ CLR ? arg ]
    522   | CPL arg ⇒ Some ? [ CPL ? arg ]
    523   | RL arg ⇒ Some ? [ RL ? arg ]
    524   | RR arg ⇒ Some ? [ RR ? arg ]
    525   | RLC arg ⇒ Some ? [ RLC ? arg ]
    526   | RRC arg ⇒ Some ? [ RRC ? arg ]
    527   | SWAP arg ⇒ Some ? [ SWAP ? arg ]
    528   | MOV arg ⇒ Some ? [ MOV ? arg ]
    529   | MOVX arg ⇒ Some ? [ MOVX ? arg ]
    530   | SETB arg ⇒ Some ? [ SETB ? arg ]
    531   | PUSH arg ⇒ Some ? [ PUSH ? arg ]
    532   | POP arg ⇒ Some ? [ POP ? arg ]
    533   | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
    534   | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
    535   | RET ⇒ Some ? [ RET ? ]
    536   | RETI ⇒ Some ? [ RETI ? ]
    537   | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
    538   ].
    539 
    540 definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
    541   λlookup_labels.
    542   λlookup_datalabels.
    543   λpc.
    544   λjmp_len.
    545   λi.
    546   match i with
    547   [ Cost cost ⇒ Some ? [ ]
    548   | Comment comment ⇒ Some ? [ ]
    549   | Call call ⇒
    550     match jmp_len with
    551     [ short_jump ⇒ None ?
    552     | medium_jump ⇒
    553       let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
    554       let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
    555       if eq_bv ? ignore fst_5 then
    556         let address ≝ ADDR11 address in
    557           Some ? ([ ACALL address ])
    558       else
    559         None ?
    560     | long_jump ⇒
    561       let address ≝ ADDR16 (lookup_labels call) in
    562         Some ? [ LCALL address ]
    563     ]
    564   | Mov d trgt ⇒
    565     let address ≝ DATA16 (lookup_datalabels trgt) in
    566       Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
    567   | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
    568   | Jmp jmp ⇒
    569     match jmp_len with
    570     [ short_jump ⇒
    571       let lookup_address ≝ lookup_labels jmp in
    572       let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
    573       let 〈upper, lower〉 ≝ split ? 8 8 result in
    574       if eq_bv ? upper (zero 8) then
    575         let address ≝ RELATIVE lower in
    576           Some ? [ SJMP address ]
    577       else
    578         None ?
    579     | medium_jump ⇒
    580       let address ≝ lookup_labels jmp in
    581       let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
    582       let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    583       if eq_bv ? fst_5_addr fst_5_pc then
    584         let address ≝ ADDR11 rest_addr in
    585           Some ? ([ AJMP address ])
    586       else
    587         None ?
    588     | long_jump ⇒
    589       let address ≝ ADDR16 (lookup_labels jmp) in
    590         Some ? [ LJMP address ]
    591     ]
    592   ].
    593   @ I
    594 qed.
    595 
    596 (* label_map: identifier ↦ 〈instruction number, address〉 *)
    597 definition label_map ≝ identifier_map ASMTag (nat × nat).
    598 
    599 definition is_label ≝
    600   λx:labelled_instruction.λl:Identifier.
    601   let 〈lbl,instr〉 ≝ x in
    602   match lbl with
    603   [ Some l' ⇒ l' = l
    604   | _       ⇒ False
    605   ].
    606 
    607 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
    608   λpc.λjmp_len.λinstr.
    609   let bv_pc ≝ bitvector_of_nat 16 pc in
    610   let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
    611   let bv: list (BitVector 8) ≝ match ilist with
    612     [ None   ⇒ (* this shouldn't happen *) [ ]
    613     | Some l ⇒ flatten … (map … assembly1 l)
    614     ] in
    615   pc + (|bv|).
    616 
    617 lemma label_does_not_occur:
    618   ∀i,p,l.
    619   is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
    620  #i #p #l generalize in match i; elim p
    621  [ #i >nth_nil #H @⊥ @H
    622  | #h #t #IH #i cases i -i
    623    [ cases h #hi #hp cases hi
    624      [ normalize #H @⊥ @H
    625      | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
    626        whd in Heq; >Heq
    627        >eq_identifier_refl //
    628      ]
    629    | #i #H whd in match (does_not_occur ??);
    630      whd in match (instruction_matches_identifier ??);
    631      cases h #hi #hp cases hi normalize nodelta
    632      [ @(IH i) @H
    633      | #l' @eq_identifier_elim
    634        [ normalize //
    635        | normalize #_ @(IH i) @H
    636        ]
    637      ]
    638    ]
    639  ]
    640 qed. 
    641 
    642 definition create_label_map: ∀program:list labelled_instruction.
    643   ∀policy:jump_expansion_policy.
    644   (Σlabels:label_map.
    645     ∀i:ℕ.lt i (|program|) →
    646     ∀l.occurs_exactly_once l program →
    647     is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    648     ∃a.lookup … labels l = Some ? 〈i,a〉
    649   ) ≝
    650   λprogram.λpolicy.
    651   let 〈final_pc, final_labels〉 ≝
    652     foldl_strong (option Identifier × pseudo_instruction)
    653     (λprefix.ℕ × (Σlabels.
    654       ∀i:ℕ.lt i (|prefix|) →
    655       ∀l.occurs_exactly_once l prefix →
    656       is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    657       ∃a.lookup … labels l = Some ? 〈i,a〉)
    658     )
    659     program
    660     (λprefix.λx.λtl.λprf.λacc.
    661      let 〈pc,labels〉 ≝ acc in
    662      let 〈label,instr〉 ≝ x in
    663        let new_labels ≝
    664        match label with
    665        [ None   ⇒ labels
    666        | Some l ⇒ add … labels l 〈|prefix|, pc〉
    667        ] in
    668      let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
    669        〈add_instruction_size pc jmp_len instr, new_labels〉
    670     ) 〈0, empty_map …〉 in
    671     final_labels.
    672 [ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    673   [ #Hi #l normalize nodelta; cases label normalize nodelta
    674     [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    675       lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    676       % [ @addr | @Haddr ]
    677     | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
    678       @eq_identifier_elim #Heq #Hocc
    679       [ normalize in Hocc;
    680         >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    681         @⊥ @(absurd … Hocc)
    682       | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    683         [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    684         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
    685         ]
    686       ]
    687       >(label_does_not_occur i … Hl) normalize nodelta @nmk //
    688     ]
    689   | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
    690     [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
    691       [ normalize nodelta #H @⊥ @H
    692       | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
    693       ]
    694     | @le_n
    695     ]
    696   ]
    697 | #i #Hi #l #Hl @⊥ @Hl
    698 ]
    699 qed.
    700 
    701 definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
    702   λlabels.λpc.λlbl.
    703   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    704   if leb pc addr (* forward jump *)
    705   then if leb (addr - pc) 126
    706        then 〈addr, short_jump〉
    707        else 〈addr, long_jump〉
    708   else if leb (pc - addr) 129
    709        then 〈addr, short_jump〉
    710        else 〈addr, long_jump〉.
    711 
    712 definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    713   λlabels.λpc_nat.λlbl.
    714   let pc ≝ bitvector_of_nat 16 pc_nat in
    715   let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
    716   let addr ≝ bitvector_of_nat 16 addr_nat in
    717   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    718   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    719   if eq_bv ? fst_5_addr fst_5_pc
    720   then 〈addr_nat, medium_jump〉
    721   else 〈addr_nat, long_jump〉.
    722  
    723 definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    724   λlabels.λpc.λlbl.
    725   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    726   if leb pc addr
    727   then if leb (addr - pc) 126
    728        then 〈addr, short_jump〉
    729        else select_call_length labels pc lbl
    730   else if leb (pc - addr) 129
    731        then 〈addr, short_jump〉
    732        else select_call_length labels pc lbl.
    733  
    734 definition jump_expansion_step_instruction: label_map → ℕ →
    735   preinstruction Identifier → option (ℕ × jump_length) ≝
    736   λlabels.λpc.λi.
    737   match i with
    738   [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
    739   | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
    740   | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
    741   | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
    742   | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
    743   | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
    744   | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
    745   | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
    746   | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
    747   | _        ⇒ None ?
    748   ].
    749 
    750 definition is_jump' ≝
    751   λx:preinstruction Identifier.
    752   match x with
    753   [ JC _ ⇒ True
    754   | JNC _ ⇒ True
    755   | JZ _ ⇒ True
    756   | JNZ _ ⇒ True
    757   | JB _ _ ⇒ True
    758   | JNB _ _ ⇒ True
    759   | JBC _ _ ⇒ True
    760   | CJNE _ _ ⇒ True
    761   | DJNZ _ _ ⇒ True
    762   | _ ⇒ False
    763   ].
    764  
    765 definition is_jump ≝
    766   λx:labelled_instruction.
    767   let 〈label,instr〉 ≝ x in
    768   match instr with
    769   [ Instruction i   ⇒ is_jump' i
    770   | Call _ ⇒ True
    771   | Jmp _ ⇒ True
    772   | _ ⇒ False
    773   ].
    774 
    775 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
    776 #x cases x #l #i cases i
    777 [#id cases id
    778  [1,2,3,6,7,33,34:
    779   #x #y %2 whd in match (is_jump ?); /2 by nmk/
    780  |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    781   #x %2 whd in match (is_jump ?); /2 by nmk/
    782  |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    783  |9,10,14,15: #x %1 //
    784  |11,12,13,16,17: #x #y %1 //
    785  ]
    786 |2,3: #x %2 /2 by nmk/
    787 |4,5: #x %1 //
    788 |6: #x #y %2 /2 by nmk/
    789 ]
    790 qed.
    791  
    792 
    793 definition jump_in_policy ≝
    794   λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
    795   ∀i:ℕ.i < |prefix| →
    796   (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    797    ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
    798 
    799 (* these should be moved to BitVector at some point *) 
    800 lemma bitvector_of_nat_ok:
    801   ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
    802  #n elim n -n
    803  [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
    804  | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
    805  ]
    806 qed.
    807 
    808 lemma bitvector_of_nat_abs:
    809   ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
    810  #n #x #y #Hx #Hy #Heq @notb_elim
    811  lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
    812  cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
    813  [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
    814  | #H //
    815  ]
    816 qed.
    817 
    818 lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    819  ∀policy:(Σp:jump_expansion_policy.
    820  (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    821  jump_in_policy prefix p).
    822   ∀i:ℕ.i < |prefix| →
    823   iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
    824   (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
    825  #prefix #policy #i #Hi @conj
    826  [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
    827    cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    828    [ #H @H
    829    | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    830      @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
    831    ]
    832  | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    833    #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
    834  ] 
    835 qed.
    836 
    837 definition jump_expansion_start:
    838   ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    839   Σpolicy:jump_expansion_policy.
    840     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    841     jump_in_policy program policy ∧
    842     ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
    843      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
    844   λprogram.
    845   foldl_strong (option Identifier × pseudo_instruction)
    846   (λprefix.Σpolicy:jump_expansion_policy.
    847     (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    848     jump_in_policy prefix policy ∧
    849     ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    850       lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
    851   program
    852   (λprefix.λx.λtl.λprf.λpolicy.
    853    let 〈label,instr〉 ≝ x in
    854    match instr with
    855    [ Instruction i ⇒ match i with
    856      [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    857      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    858      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    859      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    860      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    861      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    862      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    863      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    864      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    865      | _ ⇒ (pi1 … policy)
    866      ]
    867    | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    868    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    869    | _      ⇒ (pi1 ?? policy)
    870    ]
    871   ) (Stub ? ?).
    872 [1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
    873  @conj
    874  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    875   @conj
    876   #i >append_length <commutative_plus #Hi normalize in Hi;
    877   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    878    #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
    879    [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
    880      @le_S_to_le @le_S_to_le @Hi
    881    |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
    882      @Hi2
    883    |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
    884      <Hi @le_n_Sn
    885    |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
    886      @Hi2
    887    ]
    888   ]
    889   cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    890   [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    891     >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    892     @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    893   ]
    894   @conj >(injective_S … Hi)
    895    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    896     >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
    897    ]
    898    #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
    899    >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    900    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    901      #H destruct (H)
    902    ]
    903    @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    904    @le_plus_n_r
    905  ]
    906  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    907  -Hi; #Hi
    908  [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
    909   #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
    910   >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
    911  ]
    912  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
    913  #H @⊥ @H
    914 |2,3,26,27,28,29,30,31,32,33,34: @conj
    915  [1,3,5,7,9,11,13,15,17,19,21: @conj
    916   [1,3,5,7,9,11,13,15,17,19,21:
    917     #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
    918    [1,3,5,7,9,11,13,15,17,19,21:
    919      @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    920    ]
    921    >eq_bv_sym @bitvector_of_nat_abs
    922    [1,4,7,10,13,16,19,22,25,28,31:
    923      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    924      @le_plus_n_r
    925    |2,5,8,11,14,17,20,23,26,29,32: @Hi2
    926    |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
    927    ]
    928   ]
    929   #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    930   -Hi #Hi
    931   [1,3,5,7,9,11,13,15,17,19,21:
    932    >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
    933    [1,3,5,7,9,11,13,15,17,19,21:
    934     @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    935    ]
    936    @bitvector_of_nat_abs
    937    [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
    938    |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    939    ]
    940    @(transitive_lt … (pi2 ?? program))
    941    >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    942   ]
    943   @conj >(injective_S … Hi) #H
    944   [2,4,6,8,10,12,14,16,18,20,22:
    945    >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
    946   ]
    947   @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
    948  ]
    949  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    950   -Hi #Hi
    951  [1,3,5,7,9,11,13,15,17,19,21:
    952   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
    953   [1,3,5,7,9,11,13,15,17,19,21:
    954    @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
    955   ]
    956   @bitvector_of_nat_abs
    957   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
    958   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    959   ]
    960   @(transitive_lt … (pi2 ?? program))
    961   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    962  ]
    963  #_ >(injective_S … Hi) @lookup_opt_insert_hit
    964 |@conj
    965  [@conj
    966   [ #i #Hi //
    967   | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
    968   ]
    969  | #i #Hi >nth_nil #Hj @⊥ @Hj
    970 ]
    971 qed.
    972 
    973 definition policy_increase: list labelled_instruction → jump_expansion_policy →
    974   jump_expansion_policy → Prop ≝
    975  λprogram.λop.λp.
    976   (∀i:ℕ.i < |program| →
    977     let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
    978     let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
    979     jmpleq oj j).
    980 
    981 definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
    982  (*λlabels.*)λpolicy.
    983  bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
    984     match jmp_len with
    985     [ short_jump  ⇒ if leb pc_nat addr_nat
    986        then le (addr_nat - pc_nat) 126
    987        else le (pc_nat - addr_nat) 129
    988     | medium_jump ⇒
    989        let addr ≝ bitvector_of_nat 16 addr_nat in
    990        let pc ≝ bitvector_of_nat 16 pc_nat in
    991        let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
    992        let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
    993        eq_bv 5 fst_5_addr fst_5_pc = true
    994     | long_jump   ⇒ True
    995     ]
    996   ).
    997  
    998 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    999   ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
    1000     ∀l.occurs_exactly_once l program →
    1001     is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    1002     ∃a.lookup … lm l = Some ? 〈i,a〉).
    1003   ∀old_policy:(Σpolicy.
    1004     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    1005     jump_in_policy program policy).
    1006   (Σpolicy.
    1007     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    1008     jump_in_policy program policy ∧
    1009     policy_increase program old_policy policy)
    1010     ≝
    1011   λprogram.λlabels.λold_policy.
    1012   let 〈final_pc, final_policy〉 ≝
    1013     foldl_strong (option Identifier × pseudo_instruction)
    1014     (λprefix.ℕ × Σpolicy.
    1015       (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    1016       jump_in_policy prefix policy ∧
    1017       policy_increase prefix old_policy policy
    1018     )
    1019     program
    1020     (λprefix.λx.λtl.λprf.λacc.
    1021       let 〈pc, policy〉 ≝ acc in
    1022       let 〈label,instr〉 ≝ x in
    1023       let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
    1024       let add_instr ≝
    1025         match instr with
    1026         [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
    1027         | Call c        ⇒ Some ? (select_call_length labels pc c)
    1028         | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
    1029         | _             ⇒ None ?
    1030         ] in
    1031       let 〈new_pc, new_policy〉 ≝
    1032         let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
    1033         match add_instr with
    1034         [ None    ⇒ (* i.e. it's not a jump *)
    1035           〈add_instruction_size pc long_jump instr, policy〉
    1036         | Some z ⇒ let 〈addr,ai〉 ≝ z in
    1037           let new_length ≝ max_length old_length ai in
    1038           〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
    1039         ] in
    1040       〈new_pc, new_policy〉
    1041     ) 〈0, Stub ? ?〉 in
    1042     final_policy.
    1043 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    1044 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
    1045   [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    1046   | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
    1047     [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    1048     | >eq_bv_sym @bitvector_of_nat_abs
    1049       [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1050         @le_S_S @le_plus_n_r
    1051       | @Hi2
    1052       | @lt_to_not_eq @Hi
    1053       ]
    1054     ]
    1055   ]
    1056 | cases (le_to_or_lt_eq … Hi) -Hi;
    1057   [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    1058     [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    1059       cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
    1060       [ @(proj1 ?? Hacc Hj)
    1061       | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
    1062         @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
    1063         >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
    1064         [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    1065         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    1066         ]
    1067         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1068         @le_S_S @le_plus_n_r
    1069       ]
    1070     | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    1071       #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
    1072       normalize nodelta #x #y [2: #z]
    1073       #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
    1074       [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
    1075         [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    1076         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    1077         ]
    1078         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1079         @le_S_S @le_plus_n_r
    1080       | @Hl
    1081       ]
    1082     ]
    1083   | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
    1084      <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
    1085      [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
    1086      [3,5,11: #H @⊥ @H (* instr is not a jump *)
    1087      |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    1088        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    1089        [1,3,5: #H destruct (H)]
    1090        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1091        @le_S_S @le_plus_n_r
    1092      |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    1093        whd in match (snd ???); @(ex_intro ?? pc)
    1094        [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
    1095          @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
    1096          cases (select_jump_length labels pc id)
    1097        | @(ex_intro ?? (\fst (select_call_length labels pc id)))
    1098          @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
    1099          cases (select_call_length labels pc id)
    1100        ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
    1101      |8,10: #_ //
    1102      |1,2: cases pi
    1103        [35,36,37: #H @⊥ @H
    1104        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
    1105        |1,2,3,6,7,33,34: #x #y #H @⊥ @H
    1106        |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    1107          whd in match (snd ???); @(ex_intro ?? pc)
    1108          @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
    1109          @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
    1110          normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
    1111          @lookup_opt_insert_hit
    1112        |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    1113          whd in match (snd ???); @(ex_intro ?? pc)
    1114          @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
    1115          @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
    1116          normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
    1117          @lookup_opt_insert_hit
    1118        |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    1119         #z cases z -z #x #y #z normalize nodelta
    1120         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    1121         [1,3,5: #H destruct (H)]
    1122         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1123         @le_S_S @le_plus_n_r     
    1124        |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    1125         #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    1126         #z cases z -z #x #y #z normalize nodelta
    1127         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    1128         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
    1129         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1130         @le_S_S @le_plus_n_r
    1131        |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
    1132         cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
    1133         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    1134         [1,3,5,7,9,11,13: #H destruct (H)]
    1135         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1136         @le_S_S @le_plus_n_r             
    1137        |46,47,51,52: #id #_ //
    1138        |48,49,50,53,54: #x #id #_ //
    1139        ]
    1140      ]
    1141    ]
    1142   ]
    1143 | lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
    1144   [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    1145     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    1146     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    1147       #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    1148     | normalize nodelta >(injective_S … Hi)
    1149       >lookup_opt_lookup_miss
    1150       [ >lookup_opt_lookup_miss
    1151         [ //
    1152         | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    1153           #x #y normalize nodelta
    1154           >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    1155           [ //
    1156           | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1157             @le_S_S @le_plus_n_r
    1158           ]
    1159         ]
    1160       | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
    1161         [ //
    1162         | >prf >p1 >nth_append_second [ <minus_n_n
    1163         generalize in match Ha; normalize nodelta cases instr normalize nodelta
    1164         [1: #pi cases pi
    1165          [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
    1166          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
    1167          |35,36,37: #H normalize /2 by nmk/
    1168          |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
    1169            #H destruct (H)
    1170          |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
    1171            #H destruct (H)
    1172          ]
    1173         |2,3: #x #H normalize /2 by nmk/
    1174         |6: #x #y #H normalize /2 by nmk/
    1175         |4,5: #id #H destruct (H)
    1176         ] | @le_n ]
    1177         | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
    1178         ]
    1179       ]
    1180     ]
    1181   | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    1182     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    1183     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    1184       #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
    1185       [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    1186       | @bitvector_of_nat_abs
    1187         [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    1188         |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
    1189         ]
    1190         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1191         @le_S_S @le_plus_n_r
    1192       ]
    1193     | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
    1194       [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
    1195         normalize nodelta >lookup_insert_hit @jmpleq_max_length
    1196       | >prf >p1 >nth_append_second
    1197         [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
    1198           [1: #pi cases pi
    1199            [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
    1200            |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
    1201            |35,36,37: #H normalize in H; destruct (H)
    1202            |9,10,14,15: #id #H //
    1203            |11,12,13,16,17: #x #id #H //
    1204            ]
    1205           |2,3: #x #H normalize in H; destruct (H)
    1206           |6: #x #y #H normalize in H; destruct (H)
    1207           |4,5: #id #H //
    1208           ]
    1209         | @le_n ]
    1210       | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
    1211       ]
    1212     ]
    1213   ] ]
    1214 | @conj [ @conj
    1215   [ #i #Hi //
    1216   | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
    1217                    normalize in H3; destruct (H3) ]
    1218   ]                 
    1219   | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    1220 ]
    1221 qed.
    1222  
    1223 let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
    1224   (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
    1225     And
    1226     (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
    1227     (jump_in_policy program policy)) ≝
    1228   match n with
    1229   [ O   ⇒ jump_expansion_start program
    1230   | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
    1231     jump_expansion_step program (create_label_map program old_policy) old_policy
    1232   ].
    1233 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
    1234 | @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
    1235 ]
    1236 qed.
    1237 
    1238 definition policy_equal ≝
    1239   λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
    1240   ∀n:ℕ.n < |program| →
    1241     let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
    1242     let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
    1243     j1 = j2.
    1244 
    1245 lemma pe_refl:
    1246   ∀program.reflexive ? (policy_equal program).
    1247  #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
    1248  #y cases y -y #y #z normalize nodelta @refl
    1249 qed.
    1250 
    1251 lemma pe_sym:
    1252   ∀program.symmetric ? (policy_equal program).
    1253  #program whd #x #y #Hxy whd #n #Hn
    1254  lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
    1255  #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
    1256  #z cases z -z #y1 #y2 #y3 normalize nodelta //
    1257 qed.
    1258 
    1259 lemma pe_trans:
    1260   ∀program.transitive ? (policy_equal program).
    1261  #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
    1262  whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
    1263  lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
    1264  cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
    1265  cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
    1266  cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
    1267  normalize nodelta //
    1268 qed.
    1269 
    1270 lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1271  ∀p1,p2:Σpolicy.
    1272  (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
    1273  ∧jump_in_policy program policy.
    1274   policy_equal program p1 p2 →
    1275   policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
    1276     (jump_expansion_step program (create_label_map program p2) p2).
    1277  #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
    1278  lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
    1279  cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
    1280  [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
    1281    #Hnotjmp >lookup_opt_lookup_miss
    1282    [ >lookup_opt_lookup_miss
    1283      [ @refl
    1284      | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
    1285        [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
    1286        | @Hnotjmp
    1287        ]
    1288      ]
    1289    | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
    1290      [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
    1291      | @Hnotjmp
    1292      ]
    1293    ]
    1294  | #x #Hl cases daemon (* XXX *)
    1295  ]
    1296 qed.
    1297 
    1298 (* this is in the stdlib, but commented out, why? *)
    1299 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
    1300   #n (elim n) normalize /2 by S_pred/ qed.
    1301 
    1302 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
    1303   policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
    1304   ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
    1305  #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
    1306  lapply Heq -Heq; lapply n -n; elim z -z;
    1307  [ #n #Heq <plus_n_O @pe_refl 
    1308  | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
    1309    [ @Heq
    1310    | @pe_step @Hind @Heq
    1311    ]
    1312  ]
    1313 qed.
    1314 
    1315 lemma thingie:
    1316   ∀A:Prop.(A + ¬A) → (¬¬A) → A.
    1317  #A #Adec #nnA cases Adec
    1318  [ //
    1319  | #H @⊥ @(absurd (¬A) H nnA)
    1320  ]
    1321 qed.
    1322  
    1323 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
    1324  ∀policy:(Σp:jump_expansion_policy.
    1325     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    1326     jump_in_policy program p).
    1327   ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
    1328   ∃n:ℕ.n < (|program|) ∧ jmple
    1329     (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    1330     (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
    1331  #program #policy #Hp
    1332  cases (dec_bounded_exists (λn.jmple
    1333    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    1334    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
    1335  [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
    1336  | #abs @⊥ @(absurd ?? Hp) #n #Hn
    1337    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
    1338    lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    1339    cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
    1340    #z cases z -z #x1 #x2 #x3 #Hx
    1341    lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
    1342    cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
    1343    #z cases z -z #y1 #y2 #y3 #Hy
    1344    normalize nodelta #Hj cases Hj
    1345    [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
    1346    | //
    1347    ]
    1348  | #n @dec_jmple
    1349  ]
    1350 qed.
    1351 
    1352 lemma stupid:
    1353   ∀program,n.
    1354   pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
    1355   pi1 … (jump_expansion_internal program (S n)).
    1356  //
    1357 qed.
    1358 
    1359 let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
    1360  on program: ℕ ≝
    1361  match program with
    1362  [ nil      ⇒ acc
    1363  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
    1364    [ long_jump   ⇒ measure_int t policy (acc + 2)
    1365    | medium_jump ⇒ measure_int t policy (acc + 1)
    1366    | _           ⇒ measure_int t policy acc
    1367    ]
    1368  ].
    1369 
    1370 (* definition measure ≝
    1371   λprogram.λpolicy.measure_int program policy 0. *)
    1372  
    1373 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
    1374   measure_int program policy (x+d) = measure_int program policy x + d.
    1375  #program #policy #x #d generalize in match x; -x elim d
    1376  [ //
    1377  | -d; #d #Hind elim program
    1378    [ //
    1379    | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1380      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    1381      [ normalize nodelta @Hd
    1382      |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
    1383        @Hd
    1384      ]
    1385    ]
    1386  ]
    1387 qed.
    1388    
    1389 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    1390   ∀policy:Σp:jump_expansion_policy.
    1391     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    1392     jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
    1393   measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
    1394 #program #policy #l elim l -l;
    1395   [ #Hp #acc normalize @le_n
    1396   | #h #t #Hind #Hp #acc
    1397     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
    1398     whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
    1399     cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
    1400     cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
    1401     normalize nodelta #Hj cases Hj
    1402     [ cases x3 cases y3
    1403       [1,4,5,7,8,9: #H @⊥ @H
    1404       |2,3,6: #_ normalize nodelta
    1405         [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
    1406         |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
    1407         ]
    1408         [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
    1409         |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //]
    1410         ]
    1411       ]
    1412     | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    1413     ]
    1414   ]
    1415 qed.
    1416 
    1417 lemma measure_le: ∀program.∀policy.
    1418   measure_int program policy 0 ≤ 2*|program|.
    1419  #program #policy elim program
    1420  [ normalize @le_n
    1421  | #h #t #Hind whd in match (measure_int ???);
    1422    cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    1423    [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    1424    |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    1425      @le_plus [1,3: @Hind |2,4: // ]
    1426    ]
    1427  ]
    1428 qed.
    1429 
    1430 (* these lemmas seem superfluous, but not sure how *)
    1431 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
    1432  #a elim a
    1433  [ normalize #b //
    1434  | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
    1435    <plus_n_Sm <plus_n_Sm #H
    1436    >(Hind b (injective_S ?? (injective_S ?? H))) // ]
    1437  ]
    1438 qed.
    1439 
    1440 lemma sth_not_s: ∀x.x ≠ S x.
    1441  #x cases x
    1442  [ // | #y // ]
    1443 qed.
    1444 
    1445 lemma measure_full: ∀program.∀policy.
    1446   measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1447   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
    1448  #program #policy elim program
    1449  [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1450  | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    1451    [ whd in match (measure_int ???) in Hm;
    1452      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    1453      normalize nodelta
    1454      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    1455      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    1456        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
    1457        >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
    1458        >plus_n_Sm @le_n
    1459      | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
    1460      ]
    1461    | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
    1462    [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    1463    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1464      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    1465      normalize nodelta
    1466      [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
    1467        >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
    1468      | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
    1469        #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
    1470      | #_ //
    1471      ]
    1472    ]]
    1473  ]
    1474 qed.
    1475 
    1476 lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1477   ∀policy:Σp:jump_expansion_policy.
    1478     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    1479     jump_in_policy program p.
    1480   measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
    1481   policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
    1482 #program #policy lapply (le_n (|program|)) @(list_ind ?
    1483   (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
    1484       policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
    1485    ?? program)
    1486  [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
    1487  | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    1488    [ #Hi @Hind
    1489      [ @(transitive_le … Hp) //
    1490      | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
    1491        lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    1492        [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    1493        | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    1494          #x cases x -x #x1 #x2 #x3
    1495          cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    1496          #y cases y -y #y1 #y2 #y3
    1497          normalize nodelta cases x3 cases y3 normalize nodelta
    1498          [1: #H #_ @H
    1499          |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    1500            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    1501          |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    1502          |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
    1503            #H #_ @(injective_plus_r … H)
    1504          |6: >measure_plus >measure_plus
    1505             change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    1506             #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    1507             @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    1508          |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
    1509            #H #_ @(injective_plus_r … H)
    1510          ]
    1511        ]
    1512      | @(le_S_S_to_le … Hi)
    1513      ]
    1514    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
    1515      whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
    1516      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    1517      [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    1518      | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    1519        #x cases x -x #x1 #x2 #x3
    1520        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    1521        #y cases y -y #y1 #y2 #y3
    1522        normalize nodelta cases x3 cases y3 normalize nodelta
    1523        [1,5,9: #_ #_ //
    1524        |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    1525        |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    1526          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    1527        |6: >measure_plus >measure_plus
    1528           change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    1529           #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    1530           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    1531        ]
    1532      ]
    1533    ]
    1534  ] 
    1535 qed.
    1536 
    1537 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    1538   |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
    1539  #l #program elim l
    1540  [ //
    1541  | #h #t #Hind #Hp whd in match (measure_int ???);
    1542    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1543    [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
    1544      [ normalize nodelta @Hind @le_S_to_le ]
    1545      @Hp
    1546    | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
    1547      [ normalize nodelta @Hind @le_S_to_le ]
    1548      @Hp
    1549    ]
    1550  ]
    1551 qed.
    1552  
    1553 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1554   Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
    1555  #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
    1556  @(ex_intro … (2*|program|)) #k #Hk
    1557  cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
    1558    (jump_expansion_internal program (S k))) ? (2*|program|))
    1559  [ #H elim H -H #x #Hx @pe_trans
    1560    [ @(jump_expansion_internal program x)
    1561    | @pe_sym @equal_remains_equal
    1562      [ @(proj2 ?? Hx)
    1563      | @(transitive_le ? (2*|program|))
    1564        [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
    1565        | @le_S_S_to_le @le_S @Hk
    1566        ]
    1567      ]
    1568    | @equal_remains_equal
    1569      [ @(proj2 ?? Hx)
    1570      | @le_S_S_to_le @le_S @(proj1 ?? Hx)
    1571      ]
    1572    ]
    1573  | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
    1574    [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
    1575      #Hfull #i #Hi
    1576      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
    1577      lapply (Hfull ? i Hi)
    1578      [ -i @le_to_le_to_eq
    1579        [ @measure_le
    1580        | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
    1581          [ #_ >measure_zero @le_n
    1582          | #x #Hind #Hx
    1583            cut (measure_int program (jump_expansion_internal program x) 0 <
    1584                 measure_int program (jump_expansion_internal program (S x)) 0)
    1585            [ elim (le_to_or_lt_eq …
    1586                (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
    1587              [ //
    1588              | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
    1589              ]
    1590            | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
    1591            ]
    1592          ]
    1593        ]
    1594      | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
    1595        #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
    1596        >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
    1597        #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
    1598        [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
    1599        | #_ //
    1600        ]
    1601      ]
    1602    | @le_S_to_le @Hk
    1603    ]
    1604  | #n @dec_bounded_forall #m
    1605    cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
    1606    #x cases x -x #x1 #x2 #x3
    1607    cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
    1608    #y cases y -y #y1 #y2 #y3 normalize nodelta
    1609    @dec_eq_jump_length
    1610  ]
    1611 qed.
    1612 
    1613 let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
    1614   BitVectorTrie jump_length 16 ≝
    1615   match n with
    1616   [ O    ⇒ acc
    1617   | S n' ⇒
    1618     match lookup_opt … (bitvector_of_nat 16 n') policy with
    1619     [ None   ⇒ transform_policy n' policy acc
    1620     | Some x ⇒ let 〈pc,length〉 ≝ x in
    1621       transform_policy n' policy (insert … pc length acc)
    1622     ]
    1623   ].
     8include "ASM/Policy.ma".
    16249
    162510(**************************************** START OF POLICY ABSTRACTION ********************)
     
    2010395    eq_identifier tag l r = false → (l = r → False).
    2011396
    2012 include "basics/russell.ma".
    2013 
    2014 lemma weird: ∀A,B,P. (Σx:A × B. P x) → True.
    2015  #A #B #P #c
    2016  letin H ≝ (let 〈a,b〉 ≝ c in b)
    2017  check H
    2018 
    2019397definition build_maps:
    2020398 ∀pseudo_program.∀pol:policy pseudo_program.
     
    2039417                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
    2040418                (\snd pseudo_program)
    2041         (λprefix,i,tl,prf,t. ?(*
     419        (λprefix,i,tl,prf,t.
    2042420          let 〈labels, ppc_pc_costs〉 ≝ t in
    2043421          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     
    2053431          in
    2054432            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
    2055               〈labels, 〈S ppc,construct〉〉*)) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
     433              〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
    2056434    in
    2057435      let 〈labels, ppc_pc_costs〉 ≝ result in
    2058436      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    2059437      let 〈pc, costs〉 ≝ pc_costs in
    2060         〈labels, ?(*costs*)〉.
    2061  [2: check result
     438        〈labels, costs〉.
    2062439 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    2063440   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
Note: See TracChangeset for help on using the changeset viewer.