Changeset 1614
 Timestamp:
 Dec 14, 2011, 5:00:45 PM (9 years ago)
 Location:
 src/ASM
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1613 r1614 6 6 include alias "arithmetics/nat.ma". 7 7 include "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 ]. 8 include "ASM/Policy.ma". 1624 9 1625 10 (**************************************** START OF POLICY ABSTRACTION ********************) … … 2010 395 eq_identifier tag l r = false → (l = r → False). 2011 396 2012 include "basics/russell.ma".2013 2014 lemma weird: ∀A,B,P. (Σx:A × B. P x) → True.2015 #A #B #P #c2016 letin H ≝ (let 〈a,b〉 ≝ c in b)2017 check H2018 2019 397 definition build_maps: 2020 398 ∀pseudo_program.∀pol:policy pseudo_program. … … 2039 417 lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))) 2040 418 (\snd pseudo_program) 2041 (λprefix,i,tl,prf,t. ?(*419 (λprefix,i,tl,prf,t. 2042 420 let 〈labels, ppc_pc_costs〉 ≝ t in 2043 421 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in … … 2053 431 in 2054 432 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 ? ?〉〉〉 2056 434 in 2057 435 let 〈labels, ppc_pc_costs〉 ≝ result in 2058 436 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 2059 437 let 〈pc, costs〉 ≝ pc_costs in 2060 〈labels, ?(*costs*)〉. 2061 [2: check result 438 〈labels, costs〉. 2062 439 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 2063 440 generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
Note: See TracChangeset
for help on using the changeset viewer.