 Timestamp:
 Jul 20, 2012, 2:05:56 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2215 r2220 266 266 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 267 267 ] 268  (* jump_increase *) cases daemon269 (*#i >append_length >commutative_plus #Hi normalize in Hi;268  (* jump_increase *) (* cases daemon *) 269 #i >append_length >commutative_plus #Hi normalize in Hi; 270 270 cases (le_to_or_lt_eq … Hi) Hi; #Hi 271 271 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 275 275 @pair_elim #opc #oj #EQ1 >lookup_insert_miss 276 276 [ >lookup_insert_miss 277 [ @pair_elim #pc #j #EQ2 / by /277 [ @pair_elim #pc #j #EQ2 #X @X 278 278  @bitvector_of_nat_abs 279 279 [ @(transitive_lt ??? Hi) ] … … 290 290 ] 291 291 ] 292  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) @pair_elim #opc #oj #EQ1292  >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta 293 293 >lookup_insert_miss 294 294 [ >lookup_insert_hit cases (dec_is_jump instr) … … 300 300 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 301 301 whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; normalize nodelta303 #H42 >(proj2 ?? (pair_destruct ?????? H42))@jmpleq_max_length302 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) 303 @jmpleq_max_length 304 304 ] 305 305 2,3,6: #x [3: #y] #_ #Hj cases Hj 306 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1; 307 normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length 306 4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 308 307 ] 309 308  lapply Heq1 Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta … … 326 325 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 327 326 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 328 cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1; 329 #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 330 %2 @refl 327 >Holdeq #EQ2 >EQ2 %2 @refl 331 328 ] 332 329 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 333 #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/330 #_ #_ #abs @⊥ @(absurd ? I abs) 334 331 ] 335 332 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) … … 341 338 ] 342 339 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 343 3,6,9: 344 cases (lookup ?? (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1; 345 #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl 346 ] 347 4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ 340 3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl 341 ] 342 4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs) 348 343 ] 349 344 ] … … 357 352 ] 358 353  <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit 359 normalize nodelta 354 normalize nodelta 360 355 cases (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) 361 356 #a #b normalize nodelta %2 @refl 362 ] *)363 ] 364  (* sigma_compact_unsafe *) cases daemon365 (*#i >append_length <commutative_plus #Hi normalize in Hi;357 ] 358 ] 359  (* sigma_compact_unsafe *) 360 #i >append_length <commutative_plus #Hi normalize in Hi; 366 361 <(proj2 ?? (pair_destruct ?????? Heq2)) 367 362 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 375 370 [ @le_S_to_le @Hi ] 376 371 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 377 [ normalize nodelta / by /372 [ normalize nodelta #X @X 378 373  #x cases x x #x1 #x2 379 374 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) 380 375 normalize nodelta 381 [ / by /376 [ #X @X 382 377  #y cases y y #y1 #y2 normalize nodelta >nth_append_first 383 [ / by /378 [ #X @X 384 379  @le_S_to_le @Hi 385 380 ] … … 394 389 [ <Hi @le_n 395 390  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) 396 [ normalize nodelta / by /391 [ normalize nodelta #X @X 397 392  #x cases x x #x1 #x2 398 393 (* USE: inc_pc = fst inc_sigma *) … … 403 398  #y cases y y #y1 #y2 #Heq >nth_append_first 404 399 [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉) 405 #Heq2 <Heq2 / by /400 #Heq2 <Heq2 #X @X 406 401  <Hi @le_n 407 402 ] … … 465 460 ] 466 461 ] 467 ] *)468 ] 469  (* policy_jump_equal → added = 0 *) cases daemon470 (*<(proj2 ?? (pair_destruct ?????? Heq2))462 ] 463 ] 464  (* policy_jump_equal → added = 0 *) 465 <(proj2 ?? (pair_destruct ?????? Heq2)) 471 466 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 472 467 (* USE[pass]: policy_jump_equal → added = 0 *) … … 483 478 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 484 479 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 485 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /480 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n % 486 481 2,4: @bitvector_of_nat_abs 487 482 [1,4: @le_S_to_le] … … 502 497 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 503 498 Heq >lookup_insert_miss 504 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))499 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit in ⊢ (???(???%) → ?); <(proj1 ?? (pair_destruct ?????? Heq1)) 505 500 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 506 501 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / … … 534 529 ] 535 530 ] 536 ] *)531 ] 537 532 ] 538 533  (* added = 0 → policy_pc_equal *) cases daemon
Note: See TracChangeset
for help on using the changeset viewer.