 Timestamp:
 Jul 24, 2012, 7:15:24 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2246 r2248 453 453 454 454 lemma jump_expansion_step6: 455 ∀program : list labelled_instruction.(* 456 (Σl:list labelled_instruction.S (l)< 2 \sup 16 ∧is_well_labelled_p l)*) 457 ∀labels : label_map.(* 458 (Σlm:label_map 459 .(∀l:identifier ASMTag 460 .occurs_exactly_once ASMTag pseudo_instruction l program 461 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 462 =address_of_word_labels_code_mem program l))*) 463 ∀old_sigma : 464 Σpolicy:ppc_pc_map 465 .(*not_jump_default program policy 466 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 467 〈O,short_jump〉) 468 =O 469 ∧\fst policy 470 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (program)) 471 (\snd policy) 〈O,short_jump〉) 472 ∧*)sigma_compact_unsafe program labels policy 473 (*∧\fst policy≤ 2 \sup 16*). 455 ∀program : list labelled_instruction. 456 ∀labels : label_map. 457 ∀old_sigma : Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy. 474 458 ∀prefix : list (option Identifier×pseudo_instruction). 475 459 ∀x : option Identifier×pseudo_instruction. 476 460 ∀tl : list (option Identifier×pseudo_instruction). 477 ∀prf : program=prefix@[x]@tl.(* 478 acc : 479 (Σx0:ℕ×ppc_pc_map 480 .(let 〈added,policy〉 ≝x0 in 481 not_jump_default prefix policy 482 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 483 〈O,short_jump〉) 484 =O 485 ∧\fst policy 486 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 487 (\snd policy) 〈O,short_jump〉) 488 ∧jump_increase prefix old_sigma policy 489 ∧sigma_compact_unsafe prefix labels policy 490 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 491 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 492 ∧out_of_program_none prefix policy 493 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 494 (\snd policy) 〈O,short_jump〉) 495 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) 496 (\snd old_sigma) 〈O,short_jump〉) 497 +added 498 ∧sigma_safe prefix labels added old_sigma policy))*) 461 ∀prf : program=prefix@[x]@tl. 499 462 ∀inc_added : ℕ. 500 ∀inc_pc_sigma : ppc_pc_map.(* 501 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 463 ∀inc_pc_sigma : ppc_pc_map. 502 464 ∀label : option Identifier. 503 465 ∀instr : pseudo_instruction. 504 ∀p1 : x≃〈label,instr〉.(* 505 add_instr ≝ 506 match instr 507 in pseudo_instruction 508 return λ_:pseudo_instruction.(option jump_length) 509 with 510 [Instruction (i:(preinstruction Identifier))⇒ 511 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 512 (prefix) i 513 Comment (_:String)⇒None jump_length 514 Cost (_:costlabel)⇒None jump_length 515 Jmp (j:Identifier)⇒ 516 Some jump_length 517 (select_jump_length labels old_sigma inc_pc_sigma inc_added (prefix) j) 518 Call (c:Identifier)⇒ 519 Some jump_length 520 (select_call_length labels old_sigma inc_pc_sigma inc_added (prefix) c) 521 Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]*) 466 ∀p1 : x≃〈label,instr〉. 522 467 ∀inc_pc : ℕ. 523 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.(* 524 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*) 468 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16. 525 469 ∀old_pc : ℕ. 526 470 ∀old_length : jump_length. … … 529 473 〈O,short_jump〉 530 474 =〈old_pc,old_length〉. 531 ∀Hpolicy1 :(* 532 (not_jump_default prefix 〈inc_pc,inc_sigma〉 533 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 534 〈O,short_jump〉) 535 =O 536 ∧inc_pc 537 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 538 〈O,short_jump〉) 539 ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉 540 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 541 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 542 ∧( *)inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉.(*) 543 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 544 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (prefix)) inc_sigma 545 〈O,short_jump〉) 546 =old_pc+inc_added 547 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*) 548 ∀Hpolic2: inc_pc 549 =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 〈O,short_jump〉). 475 ∀Hpolicy1 : inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉. 476 ∀Hpolic2: inc_pc =\fst (lookup … (bitvector_of_nat … (prefix)) inc_sigma 〈O,short_jump〉). 550 477 ∀added : ℕ. 551 478 ∀policy : ppc_pc_map. … … 588 515 (* USE[pass]: added = 0 → policy_pc_equal *) 589 516 lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 Heq1 590 inversion instr normalize nodelta 591 [ #pi #Hins whd in match jump_expansion_step_instruction; normalize nodelta 592 lapply (destination_of_None_to_is_jump_false pi) 593 lapply (destination_of_Some_to_is_jump_true pi) 594 cases (destination_of ?) normalize nodelta 595 [ #_ #dest_None  #tgt #dest_Some #_ ]] 596 try (#x #y #Hins #Heq1 #Hold #Hadded #i #Hi) 597 try (#x #Hins #Heq1 #Hold #Hadded #i #Hi) 598 try (#Heq1 #Hold #Hadded #i #Hi) 517 #Hins #Hold #Hadded #i #Hi 599 518 >append_length in Hi; >commutative_plus #Hi normalize in Hi; 600 519 cases (le_to_or_lt_eq … Hi) Hi #Hi 601 [1,3,5,7,9,11,13: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 602 [1,3,5,7,9,11,13: <Heq2b >lookup_insert_miss 603 [1,3,5,7,9,11,13: >lookup_insert_miss 604 [1,3,5,7,9,11,13: 520 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 521 [ <Heq2b >lookup_insert_miss 522 [ >lookup_insert_miss 523 [ cases instr in Hadded; normalize nodelta 524 [ whd in match jump_expansion_step_instruction; normalize nodelta 525 #pi cases (destination_of ?) normalize nodelta ] 526 try (#x #y #Hadded) try (#x #Hadded) try #Hadded 605 527 try @(Hold Hadded i (le_S_to_le … Hi)) 606 528 @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero 607 *: @bitvector_of_nat_abs try assumption 608 [2,4,6,8,10,12,14: @lt_to_not_eq @Hi 609 *: @(transitive_lt ??? Hi) assumption ]] 610 *: @bitvector_of_nat_abs try assumption 611 [2,4,6,8,10,12,14: @lt_to_not_eq @le_S @Hi 612 *: @(transitive_lt … Hi) assumption ]] 613 *: >Hi >lookup_insert_miss 614 [1,3,5,7,9,11,13: >lookup_insert_hit 529  @bitvector_of_nat_abs try assumption 530 [2: @lt_to_not_eq @Hi 531  @(transitive_lt ??? Hi) assumption ]] 532  @bitvector_of_nat_abs try assumption 533 [2: @lt_to_not_eq @le_S @Hi 534  @(transitive_lt … Hi) assumption ]] 535  >Hi >lookup_insert_miss 536 [ cases instr in Hadded; normalize nodelta 537 [ whd in match jump_expansion_step_instruction; normalize nodelta 538 #pi cases (destination_of ?) normalize nodelta ] 539 try (#x #y #Hadded) try (#x #Hadded) try #Hadded 540 >lookup_insert_hit 615 541 try (>(Hold Hadded (prefix) (le_n (prefix))) 616 542 @sym_eq (* USE: fst p = lookup prefix *) … … 625 551 (* USE fst p = lookup prefix *) 626 552 >Hpolicy2 627 <(Hold ? (prefix) (le_n (prefix))) try @Hadded 628 [3,7,9: @plus_zero_zero [2,4,6: >commutative_plus @Hadded *: skip]] 553 <(Hold ? (prefix) (le_n (prefix))) 554 [2: cases instr in Hadded; normalize nodelta 555 [ whd in match jump_expansion_step_instruction; normalize nodelta 556 #pi cases (destination_of ?) normalize nodelta ] 557 try (#x #y #Hadded) try (#x #Hadded) try #Hadded 558 try @Hadded 559 @plus_zero_zero [2,4,6: >commutative_plus @Hadded *: skip]] 629 560 (* USE: sigma_compact (from old_sigma) *) 630 561 lapply (pi2 ?? old_sigma (prefix) ?) 631 [1,3,5,7,9,11,13: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 632 *: 633 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 634 [1,3,5,7,9,11,13: normalize nodelta #_ #ABS cases ABS 635 *: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 636 [1,3,5,7,9,11,13: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS 637 *: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ 562 [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 563  inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 564 [ normalize nodelta #_ #ABS cases ABS 565  inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 566 [ normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS 567  normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ 638 568 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 639 569 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 640 570 >prf >p1 >Hins >nth_append_second try % 641 <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1)) 642 #H >H @plus_left_monotone 571 <minus_n_n whd in match (nth ????); 572 cases instr in Hins Hadded; normalize nodelta 573 [ whd in match jump_expansion_step_instruction; normalize nodelta 574 #pi lapply (destination_of_None_to_is_jump_false pi) 575 lapply (destination_of_Some_to_is_jump_true pi) 576 cases (destination_of ?) normalize nodelta 577 [ #_ #dest_None  #tgt #dest_Some #_ ]] 578 try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X) 579 <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone 643 580 [1,3,4,7: @instruction_size_irrelevant try % 644 581 whd in match is_jump; normalize nodelta >dest_None % … … 1276 1213 cases (pair_destruct ?????? Heq2) Heq2 #Heq2a #Heq2b 1277 1214 % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]] 1278 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be1279 * commented out for full proofs, but this needs a lot of memory and time *)1280 1215 [ (* not_jump_default *) 1281 1216 @(jump_expansion_step1 … Heq1 Heq2b) try assumption … … 1301 1236 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) 1302 1237 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1303  (* added = 0 → policy_pc_equal *) cases daemon (*1304 @(jump_expansion_step6 … Heq1 …Heq2b) try assumption1238  (* added = 0 → policy_pc_equal *) 1239 @(jump_expansion_step6 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 … Heq2a Heq2b) try assumption 1305 1240 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 1306 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))1307 *)1241 try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1242 cases (pi2 … old_sigma) * #_ #X #_ @X 1308 1243  (* out_of_program_none *) 1309 1244 @(jump_expansion_step7 … Heq2b) … … 1314 1249  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1315 1250  @(proj2 ?? (proj1 ?? Hpolicy)) ] 1316  (* sigma_safe *) cases daemon (*1317 @jump_expansion_step9 try assumption1251  (* sigma_safe *) 1252 @jump_expansion_step9 (*try assumption 1318 1253 @(proj2 ?? Hpolicy) *) 1319 1254 ]
Note: See TracChangeset
for help on using the changeset viewer.