Changeset 2211
- Timestamp:
- Jul 18, 2012, 3:57:09 PM (8 years ago)
- Location:
- src/ASM
- Files:
-
- 4 edited
-
Policy.ma (modified) (9 diffs)
-
PolicyFront.ma (modified) (5 diffs)
-
PolicyStep.ma (modified) (29 diffs)
-
Util.ma (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2153 r2211 17 17 (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉))) 18 18 (sigma_compact_unsafe program (create_label_map program) x)) 19 (\fst x <2^16)19 (\fst x ≤ 2^16) 20 20 ]) ≝ 21 21 let labels ≝ create_label_map program in … … 260 260 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ 261 261 sigma_compact_unsafe program (create_label_map program) p ∧ 262 \fst p <2^16.262 \fst p ≤ 2^16. 263 263 ∀l.|l| ≤ |program| → ∀acc:ℕ. 264 264 match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with … … 332 332 \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧ 333 333 sigma_compact_unsafe program (create_label_map program) p ∧ 334 \fst p <2^16.334 \fst p ≤ 2^16. 335 335 match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with 336 336 [ None ⇒ True … … 418 418 match p with 419 419 [ None ⇒ True 420 | Some pol ⇒ And (*And (out_of_program_none program pol)*) 421 (sigma_compact program (create_label_map program) pol) 422 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 420 | Some pol ⇒ And (And (And 421 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 422 (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉))) 423 (sigma_compact program (create_label_map program) pol)) 424 (\fst pol ≤ 2^16) 423 425 ]. 424 426 #program @(\snd (jump_expansion_internal program (S (2*|program|)))) … … 441 443 [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS) 442 444 | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq 443 @conj 444 [ @(equal_compact_unsafe_compact ?? Fp) 445 @conj [ @conj [ @conj 446 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 447 | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) 448 ] 449 | @(equal_compact_unsafe_compact ?? Fp) 445 450 [ lapply (jump_pc_equal program (2*|program|)) 446 451 >Feq >Geq normalize nodelta #H @H @Heq 447 | cases daemon 452 | cases daemon (* true, but have to add this to properties *) 448 453 | @(proj2 ?? (proj1 ?? HGp)) 449 454 ] 450 (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*) 451 >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq 452 [ destruct (Geq) / by / 453 | cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq; 454 #x cases x -x #Sch #So normalize nodelta cases So 455 [ normalize nodelta #_ #ABS destruct (ABS) 456 | -So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq))) 457 cases Sch in HSp Seq; #HSp #Seq 458 [ @refl 459 | normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp)) 460 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))) 461 @Heq 462 ] 463 ] 464 ] 465 ]*) 466 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 455 ] 456 | @(proj2 ?? HGp) 467 457 ] 468 458 ] … … 552 542 #z cases z -z #Gch #Go cases Go normalize nodelta 553 543 [ #HGp #Geq @I 554 | -Go #Gp normalize nodelta #HGp #Geq @conj 555 [ @(equal_compact_unsafe_compact ?? Fp) 544 | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj 545 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 546 | @(proj2 ?? (proj1 ?? (proj1 ?? HGp))) 547 ] 548 | @(equal_compact_unsafe_compact ?? Fp) 556 549 [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta 557 550 #H @H #i #Hi … … 580 573 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 581 574 ] 582 | cases daemon 575 | cases daemon (* true, but have to add to properties in some way *) 583 576 | @(proj2 ?? (proj1 ?? HGp)) 584 577 ] 585 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 578 ] 579 | @(proj2 ?? HGp) 586 580 ] 587 581 ] … … 608 602 include alias "basics/logic.ma". 609 603 604 lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map. 605 And (And (And 606 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0) 607 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) 608 (sigma_compact program (create_label_map program) p)) 609 (\fst p ≤ 2^16).i ≤ j → j ≤ |program| → 610 \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤ 611 \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉). 612 #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n 613 [ <plus_n_O #_ @le_n 614 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H))) 615 lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H) 616 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol))) 617 cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %); 618 [ normalize nodelta #_ #abs cases abs 619 | #x cases x -x #pc #jl #EQ normalize nodelta 620 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol))) 621 cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %); 622 [ normalize nodelta #_ #abs cases abs 623 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp 624 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 625 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r 626 ] 627 ] 628 ] 629 qed. 630 610 631 (* The glue between Policy and Assembly. *) 611 632 (*CSC: modified to really use the specification in Assembly.ma.*) … … 630 651 #fpc #fpol #Hfpol 631 652 @conj 632 [ lapply (proj 2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)653 [ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉) 633 654 #x #y #Hx normalize nodelta >Hx / by refl/ 634 | cases daemon (* leaving this until stabilisation of sigma predicate *) 635 (*#ppc #ppc_ok normalize nodelta @conj 636 [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok) 655 | #ppc #ppc_ok normalize nodelta @conj 656 [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok) 637 657 >bitvector_of_nat_inverse_nat_of_bitvector 638 658 lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 639 [ normalize nodelta #_#abs cases abs640 | #x cases x -x # x1 #y1 normalize nodelta #Hl_ppc641 > (plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus642 >bitvector_of_nat_inverse_nat_of_bitvector643 lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol))644 cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %);645 [ normalize nodelta #_ #abs cases abs646 | #x cases x -x #x2 #y2 normalize nodelta #Hl_Sppc647 #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉)648 > (lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta649 >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???);650 >(nth_safe_nth … 〈None ?, Comment []〉)651 >Hcompact <plus_n_O652 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #bnormalize nodelta653 whd in match instruction_size; normalize nodelta654 whd in match assembly_1_pseudoinstruction; normalize nodelta655 whd in match expand_pseudo_instruction; normalize nodelta656 cases b657 [2,3,6: # p [3: #q] normalize nodelta @refl658 |4,5: # p normalize nodelta659 >(lookup_opt_lookup_hit … Hl_Sppc〈0,short_jump〉) normalize nodelta660 >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉)normalize nodelta661 whd in match (create_label_map ?);662 cases ( lookup ??(bitvector_of_nat ?663 (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p0)) fpol 〈0,short_jump〉)664 # z1 #z2normalize nodelta @refl659 [ #Hl normalize nodelta #abs cases abs 660 | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm 661 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative 662 lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol)) 663 cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %); 664 [ #Hl normalize nodelta #abs cases abs 665 | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact 666 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 667 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 668 >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size; 669 normalize nodelta whd in match assembly_1_pseudoinstruction; 670 normalize nodelta whd in match expand_pseudo_instruction; 671 normalize nodelta whd in match fetch_pseudo_instruction; 672 normalize nodelta 673 lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok)) 674 cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %); 675 #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉) 676 >Hli normalize nodelta cases instr 677 [2,3,6: #x [3: #y] normalize nodelta % 678 |4,5: #x normalize nodelta 679 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 680 whd in match create_label_map; normalize nodelta 681 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 682 cases (bvt_lookup … (bitvector_of_nat ? 683 (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 684 #lpc #ljl normalize nodelta @refl 665 685 |1: #pi cases pi 666 686 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 667 [1,2,3,6,7,24,25: # p #q668 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: # p]669 normalize nodelta @refl670 |9,10,11,12,13,14,15,16,17: [ 1,2,6,7: #p |3,4,5,8,9: #q #p] normalize nodelta687 [1,2,3,6,7,24,25: #x #y 688 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 689 normalize nodelta % 690 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 671 691 whd in match expand_relative_jump; normalize nodelta 672 692 whd in match expand_relative_jump_internal; normalize nodelta 673 >(lookup_opt_lookup_hit … Hl_Sppc〈0,short_jump〉) normalize nodelta674 >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉)normalize nodelta675 whd in match (create_label_map ?);676 cases ( lookup ??(bitvector_of_nat ?677 (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p0)) fpol 〈0,short_jump〉)678 # z1 #z2 normalize nodelta @refl693 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 694 whd in match create_label_map; normalize nodelta 695 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 696 cases (bvt_lookup … (bitvector_of_nat ? 697 (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 698 #lpc #ljl normalize nodelta % 679 699 ] 680 700 ] 681 701 ] 682 ] 683 | cases daemon (* XXX remains to be done *) 684 ] *) 685 ] 686 qed. 702 ] 703 | (* Basic proof scheme: 704 - ppc < |snd program|, hence our instruction is in the program 705 - either we are the last non-zero-size instruction, in which case we are 706 either smaller than 2^16 (because the entire program is), or we are exactly 707 2^16 and something weird happens 708 - or we are not, in which case we are definitely smaller than 2^16 (by transitivity 709 through the next non-zero instruction) 710 *) 711 elim (le_to_or_lt_eq … (proj2 ?? Hfpol)) #Hfpc 712 [ %1 @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) 713 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok) 714 >bitvector_of_nat_inverse_nat_of_bitvector 715 lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 716 [ normalize nodelta #_ #abs cases abs 717 | #x cases x -x #pc #jl #EQ normalize nodelta 718 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol)) 719 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %); 720 [ normalize nodelta #_ #abs cases abs 721 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size; 722 normalize nodelta whd in match assembly_1_pseudoinstruction; 723 normalize nodelta whd in match expand_pseudo_instruction; 724 normalize nodelta whd in match fetch_pseudo_instruction; 725 normalize nodelta 726 lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok)) 727 cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %); 728 #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉) 729 >Hli normalize nodelta cases instr 730 [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 731 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 732 [1,3,5: <H 733 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 734 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X 735 |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 736 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 737 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 738 ] 739 |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 740 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 741 [1,3: <add_bitvector_of_nat_Sm in SEQ; 742 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ 743 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta 744 cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 745 #lpc #ljl normalize nodelta #H <H 746 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 747 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector 748 >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2 749 |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 750 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 751 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 752 ] 753 |1: #pi cases pi 754 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 755 [1,2,3,6,7,24,25: #x #y 756 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 757 normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 758 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 759 [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: 760 <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 761 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X 762 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 763 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 764 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 765 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 766 ] 767 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] 768 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 769 normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse 770 [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ; 771 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ 772 whd in match expand_relative_jump; normalize nodelta 773 whd in match expand_relative_jump_internal; normalize nodelta 774 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta 775 cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 776 #lpc #ljl normalize nodelta #H <H 777 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 778 <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector 779 >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2 780 |2,4,6,8,10,12,14,16,18: 781 lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 782 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 783 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H 784 ] 785 ] 786 ] 787 ] 788 ] 789 | (* the program is of length 2^16 and ppc is followed by only zero-size instructions 790 * until the end of the program *) 791 elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))) 792 [ lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok) 793 >bitvector_of_nat_inverse_nat_of_bitvector 794 lapply (refl ? (lookup_opt … ppc fpol)) 795 cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 796 [ #_ normalize nodelta #abs cases abs 797 | #x cases x -x #pc #jl #EQ normalize nodelta 798 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol)) 799 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %); 800 [ #_ normalize nodelta #abs cases abs 801 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc 802 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta 803 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 804 >nat_of_bitvector_bitvector_of_nat_inverse 805 [2: <Hfpc >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @Hpc ] 806 elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))) 807 [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 808 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1 809 >Hc in HSpc; 810 whd in match create_label_map; 811 whd in match fetch_pseudo_instruction; normalize nodelta 812 >(nth_safe_nth … 〈None ?, Comment []〉) 813 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 814 #lbl #ins normalize nodelta 815 whd in match instruction_size; 816 whd in match assembly_1_pseudoinstruction; 817 whd in match expand_pseudo_instruction; normalize nodelta 818 <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector 819 >add_commutative #SEQ cases ins 820 [2,3,6: #x [3: #y] normalize nodelta #H @H 821 |4,5: #x normalize nodelta 822 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 823 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 824 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 825 #lpc #ljl normalize nodelta #H @H 826 |1: #pi cases pi 827 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 828 [1,2,3,6,7,24,25: #x #y 829 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 830 normalize nodelta #H @H 831 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 832 whd in match expand_relative_jump; 833 whd in match expand_relative_jump_internal; normalize nodelta 834 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 835 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 836 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 837 #lpc #ljl normalize nodelta #H @H 838 ] 839 ] 840 | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 841 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj 842 [ #ppc' #ppc_ok' #Hppc' 843 (* S ppc < ppc' < |\snd program| *) 844 (* lookup S ppc = 2^16 *) 845 (* lookup |\snd program| = 2^16 *) 846 (* lookup ppc' = 2^16 → instruction size = 0 *) 847 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok') 848 >bitvector_of_nat_inverse_nat_of_bitvector 849 lapply (refl ? (lookup_opt … ppc' fpol)) 850 cases (lookup_opt … ppc' fpol) in ⊢ (???% → %); 851 [ normalize nodelta #_ #abs cases abs 852 | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta 853 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol)) 854 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %); 855 [ normalize nodelta #_ #abs cases abs 856 | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta 857 #Hpcompact 858 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok')) 859 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1 860 lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?)) 861 <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2 862 lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1 863 >bitvector_of_nat_inverse_nat_of_bitvector 864 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc 865 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok') 866 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1 867 lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?)) 868 <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2 869 lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2 870 >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc 871 >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H 872 @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction; 873 normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉) 874 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H; 875 #lbl #ins normalize nodelta 876 whd in match instruction_size; 877 whd in match assembly_1_pseudoinstruction; 878 whd in match expand_pseudo_instruction; normalize nodelta 879 <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector 880 >add_commutative #SXEQ cases ins 881 [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H) 882 |4,5: #x normalize nodelta 883 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) 884 >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) 885 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 886 #lpc #ljl normalize nodelta #H @(sym_eq ??? H) 887 |1: #pi cases pi 888 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 889 [1,2,3,6,7,24,25: #x #y 890 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta 891 #H @(sym_eq ??? H) 892 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 893 whd in match expand_relative_jump; 894 whd in match expand_relative_jump_internal; normalize nodelta 895 >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) 896 >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) 897 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 898 #lpc #ljl normalize nodelta #H @(sym_eq ??? H) 899 ] 900 ] 901 ] 902 ] 903 | >Hc in Hspc; 904 whd in match create_label_map; 905 whd in match fetch_pseudo_instruction; normalize nodelta 906 >(nth_safe_nth … 〈None ?, Comment []〉) 907 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 908 #lbl #ins normalize nodelta 909 whd in match instruction_size; 910 whd in match assembly_1_pseudoinstruction; 911 whd in match expand_pseudo_instruction; normalize nodelta 912 <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector 913 >add_commutative #SEQ cases ins 914 [2,3,6: #x [3: #y] normalize nodelta #H @H 915 |4,5: #x normalize nodelta 916 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 917 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 918 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 919 #lpc #ljl normalize nodelta #H @H 920 |1: #pi cases pi 921 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 922 [1,2,3,6,7,24,25: #x #y 923 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta 924 #H @H 925 |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta 926 whd in match expand_relative_jump; 927 whd in match expand_relative_jump_internal; normalize nodelta 928 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 929 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) 930 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉) 931 #lpc #ljl normalize nodelta #H @H 932 ] 933 ] 934 ] 935 ] 936 ] 937 ] 938 | >bitvector_of_nat_inverse_nat_of_bitvector 939 <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 940 cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc 941 >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?)); 942 <plus_O_n whd in match instruction_size; normalize nodelta 943 lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?)) 944 [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %); 945 #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass) 946 #Hli >Hli 947 lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?) 948 [5: >Hass / by / 949 ] 950 ] 951 ] 952 ] 953 ] 954 ] 955 qed. -
src/ASM/PolicyFront.ma
r2152 r2211 122 122 let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in 123 123 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in 124 (*opc ≤ pc ∧*)jmpleq oj j.124 jmpleq oj j. 125 125 126 126 (* this is the instruction size as determined by the jump length given *) … … 407 407 (∀i.i ≤ |program| → ∃pc. 408 408 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 409 (\fst p <2^16)409 (\fst p ≤ 2^16) 410 410 ] ≝ 411 411 λprogram.λlabels. … … 425 425 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉 426 426 ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in 427 if g eb (\fst (pi1 ?? final_policy)) 2^16 then427 if gtb (\fst (pi1 ?? final_policy)) 2^16 then 428 428 None ? 429 429 else … … 431 431 [ / by I/ 432 432 | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg 433 @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 434 | @conj [ @conj [ @conj [ @conj (*[@conj 435 [ (* out_of_program_none *) 436 #i #Hi2 >append_length <commutative_plus @conj 437 [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi 438 cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi 439 [ >lookup_opt_insert_miss 440 [ (* USE[pass]: out_of_program_none → *) 441 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2)) 442 @le_S_to_le @le_S_to_le @Hi 443 | @bitvector_of_nat_abs 444 [ @Hi2 445 | @(transitive_lt … Hi2) @le_S_to_le @Hi 446 | @sym_neq @lt_to_not_eq @le_S_to_le @Hi 447 ] 448 ] 449 | >lookup_opt_insert_miss 450 [ <Hi 451 (* USE[pass]: out_of_program_none → *) 452 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?)) 453 [ >Hi @Hi2 454 | @le_S @le_n 455 ] 456 | @bitvector_of_nat_abs 457 [ @Hi2 458 | @(transitive_lt … Hi2) <Hi @le_n 459 | @sym_neq @lt_to_not_eq <Hi @le_n 460 ] 461 ] 462 ] 463 | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf 464 normalize nodelta cases (decidable_eq_nat i (S (|prefix|))) 465 [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H) 466 | #Hi >lookup_opt_insert_miss 467 [ #Hl 468 (* USE[pass]: out_of_program_none ← *) 469 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl)) 470 [ #Hi3 @Hi3 471 | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi 472 ] 473 | @bitvector_of_nat_abs 474 [ @Hi2 475 | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length 476 <plus_n_Sm @le_S_S @le_plus_n_r 477 | @Hi 478 ] 479 ] 480 ] 481 ] 482 | *) 433 @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ] 434 | @conj [ @conj [ @conj [ @conj 483 435 [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp 484 436 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi … … 594 546 ] 595 547 ] 596 | @conj [ @conj [ @conj [ @conj (*[ @conj 597 [ #i cases i 598 [ #Hi2 @conj 599 [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / 600 | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl) 601 ] 602 | -i #i #Hi2 @conj 603 [ #Hi >lookup_opt_insert_miss 604 [ / by refl/ 605 | @bitvector_of_nat_abs 606 [ @Hi2 607 | / by / 608 | @sym_neq @lt_to_not_eq / by / 609 ] 610 ] 611 | #_ @le_S_S @le_O_n 612 ] 613 ] *) 548 | @conj [ @conj [ @conj [ @conj 614 549 [ #i cases i 615 550 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O -
src/ASM/PolicyStep.ma
r2152 r2211 17 17 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉))) 18 18 (sigma_compact_unsafe program labels policy)) 19 (\fst policy <2^16)).19 (\fst policy ≤ 2^16)). 20 20 (Σx:bool × (option ppc_pc_map). 21 21 let 〈no_ch,y〉 ≝ x in … … 30 30 (sigma_jump_equal program old_policy p → no_ch = true)) 31 31 (no_ch = true → sigma_pc_equal program old_policy p)) 32 (\fst p <2^16)32 (\fst p ≤ 2^16) 33 33 ]) 34 34 ≝ … … 93 93 (Stub ??)〉〉 94 94 ) in 95 if g eb (\fst final_policy) 2^16 then95 if gtb (\fst final_policy) 2^16 then 96 96 〈eqb final_added 0, None ?〉 97 97 else … … 127 127 ] 128 128 | #abs >abs in Hsig; #Hsig 129 @(absurd ? Hsig) @l e_to_not_lt @leb_true_to_le <geb_to_leb@Hge129 @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge 130 130 ] 131 131 | normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 … … 141 141 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2 142 142 ] 143 | @not_l e_to_lt @leb_false_to_not_le <geb_to_leb@p1143 | @not_lt_to_le @ltb_false_to_not_lt @p1 144 144 ] 145 145 |4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); … … 153 153 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 154 * commented out for full proofs, but this needs a lot of memory and time *) 155 [ (* not_jump_default *) cases daemon (*156 #i >append_length <commutative_plus #Hi normalize in Hi;155 [ (* not_jump_default *) cases daemon 156 (* #i >append_length <commutative_plus #Hi normalize in Hi; 157 157 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 158 158 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss … … 160 160 [ >(nth_append_first ? i prefix ?? Hi) 161 161 (* USE[pass]: not_jump_default *) 162 @(proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)162 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi) 163 163 | @bitvector_of_nat_abs 164 164 [ @(transitive_lt ??? Hi) ] … … 199 199 ] 200 200 ] *) 201 | (* 0 ↦ 0 *) cases daemon (*202 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss201 | (* 0 ↦ 0 *) cases daemon 202 (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 203 203 [ cases (decidable_eq_nat 0 (|prefix|)) 204 204 [ #Heq <Heq >lookup_insert_hit 205 205 (* USE: inc_pc = fst policy *) 206 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 206 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 207 <Heq 207 208 (* USE[pass]: 0 ↦ 0 *) 208 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 209 <Heq #ONE #TWO >TWO >ONE @refl 209 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 210 210 | #Hneq >lookup_insert_miss 211 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))211 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))) 212 212 | @bitvector_of_nat_abs 213 213 [3: @Hneq] … … 216 216 | @bitvector_of_nat_abs 217 217 [3: @lt_to_not_eq / by / ] 218 ] 218 ] 219 219 [1,3: / by / 220 220 |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S … … 226 226 >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 227 227 ] 228 | (* jump_increase *) cases daemon (*229 #i >append_length >commutative_plus #Hi normalize in Hi;228 | (* jump_increase *) cases daemon 229 (* #i >append_length >commutative_plus #Hi normalize in Hi; 230 230 cases (le_to_or_lt_eq … Hi) -Hi; #Hi 231 231 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 232 232 [ (* USE[pass]: jump_increase *) 233 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi))233 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi)) 234 234 <(proj2 ?? (pair_destruct ?????? Heq2)) 235 235 @pair_elim #opc #oj #EQ1 >lookup_insert_miss … … 322 322 ] *) 323 323 ] 324 | (* sigma_compact_unsafe *) cases daemon (*325 #i >append_length <commutative_plus #Hi normalize in Hi;324 | (* sigma_compact_unsafe *) cases daemon 325 (* #i >append_length <commutative_plus #Hi normalize in Hi; 326 326 <(proj2 ?? (pair_destruct ?????? Heq2)) 327 327 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi … … 332 332 [ >lookup_opt_insert_miss 333 333 [ (* USE[pass]: sigma_compact_unsafe *) 334 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)334 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 335 335 [ @le_S_to_le @Hi ] 336 336 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 351 351 | >Hi >lookup_opt_insert_hit normalize nodelta 352 352 (* USE[pass]: sigma_compact_unsafe *) 353 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)353 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?) 354 354 [ <Hi @le_n 355 355 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 357 357 | #x cases x -x #x1 #x2 358 358 (* USE: inc_pc = fst inc_sigma *) 359 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))359 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 360 360 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 361 361 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); … … 393 393 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 394 394 (* USE: out_of_program_none ← *) 395 lapply (proj2 ?? (proj 1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?))395 lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?)) 396 396 [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r 397 397 | >Hi 398 398 (* USE: inc_pc = fst policy *) 399 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))399 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 400 400 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma)) 401 401 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %); 402 402 [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|)) 403 [ @H @refl403 [ @H % 404 404 | @le_to_not_lt @le_n 405 405 ] … … 427 427 ] *) 428 428 ] 429 | (* policy_jump_equal → added = 0 *) cases daemon (*430 <(proj2 ?? (pair_destruct ?????? Heq2))429 | (* policy_jump_equal → added = 0 *) cases daemon 430 (* <(proj2 ?? (pair_destruct ?????? Heq2)) 431 431 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 432 432 (* USE[pass]: policy_jump_equal → added = 0 *) 433 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?)433 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?) 434 434 [ cases instr in Heq1 Heq; 435 435 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % … … 437 437 #Heq lapply Holdeq -Holdeq 438 438 (* USE: inc_pc = fst inc_sigma *) 439 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))439 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 440 440 lapply (Heq (|prefix|) ?) 441 441 [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] … … 458 458 <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq 459 459 (* USE: inc_pc = fst inc_sigma *) 460 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))460 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 461 461 lapply (Heq (|prefix|) ?) 462 462 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] … … 496 496 ] *) 497 497 ] 498 | (* added = 0 → policy_pc_equal *) cases daemon (*499 (* USE : added = 0 → policy_pc_equal *)500 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))498 | (* added = 0 → policy_pc_equal *) cases daemon 499 (* USE[pass]: added = 0 → policy_pc_equal *) 500 (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 501 501 <(proj2 ?? (pair_destruct ?????? Heq2)) 502 502 <(proj1 ?? (pair_destruct ?????? Heq2)) … … 527 527 [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) 528 528 @sym_eq (* USE: fst p = lookup |prefix| *) 529 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))529 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 530 530 |2,4,6: @bitvector_of_nat_abs 531 531 [3,6,9: @lt_to_not_eq @le_n … … 538 538 |2,4,6: >Hi >lookup_insert_hit 539 539 (* USE fst p = lookup |prefix| *) 540 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))540 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 541 541 <(Hold Hadded (|prefix|) (le_n (|prefix|))) 542 542 (* USE: sigma_compact (from old_sigma) *) … … 587 587 [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 588 588 (* USE: fst p = lookup |prefix| *) 589 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))589 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 590 590 |2,4: @bitvector_of_nat_abs 591 591 [3,6: @lt_to_not_eq @le_n … … 601 601 @jump_length_le_max / by I/ 602 602 |2,4: #H (* USE: fst p = lookup |prefix| *) 603 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))603 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 604 604 <(Hold ? (|prefix|) (le_n (|prefix|))) 605 605 [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H … … 671 671 >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq 672 672 (* USE: fst p = lookup |prefix| *) 673 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))673 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 674 674 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 675 675 @bitvector_of_nat_abs … … 686 686 >Hi >lookup_insert_hit 687 687 (* USE fst p = lookup |prefix| *) 688 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))688 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 689 689 <(Hold Hadded (|prefix|) (le_n (|prefix|))) 690 690 (* USE: sigma_compact (from old_sigma) *) … … 746 746 [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq 747 747 (* USE: fst p = lookup |prefix| *) 748 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))748 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 749 749 |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 750 750 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n … … 797 797 ] *) 798 798 ] 799 | (* out_of_program_none *) cases daemon 799 | (* out_of_program_none *) cases daemon 800 800 (* #i #Hi2 >append_length <commutative_plus @conj 801 801 [ (* → *) #Hi normalize in Hi; … … 969 969 ] *) 970 970 ] 971 | (* sigma_safe *) cases daemon 972 (* #i >append_length >commutative_plus #Hi normalize in Hi; 971 | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi; 973 972 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 974 973 [ >nth_append_first [2: @Hi] … … 978 977 [ elim (le_to_or_lt_eq … Hi) -Hi #Hi 979 978 [ >lookup_insert_miss 980 [ lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 981 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) 982 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)) 983 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) in ⊢ (???% → %); 984 [ normalize nodelta #_ #abs cases abs 985 | #x cases x -x #ipc #ij #EQi normalize nodelta 986 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 987 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 988 [ normalize nodelta #_ #abs cases abs 989 | #x cases x -x #Sipc #Sij #EQSi normalize nodelta #Hcompact 990 >(lookup_opt_lookup_hit … EQi 〈0,short_jump〉) 991 >(lookup_opt_lookup_hit … EQSi 〈0,short_jump〉) >Hcompact 992 normalize nodelta (*cases ij*) normalize nodelta 993 lapply (refl ? (nth i ? prefix 〈None ?, Comment []〉)) 994 cases (nth i ? prefix 〈None ?, Comment []〉) in ⊢ (???% → %); 995 #lbl #ins normalize nodelta #Hins #Hind #dest #Hi 996 lapply (Hind dest Hi) -Hind #Hind 997 elim (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) 998 [ #Hle elim (le_to_or_lt_eq … Hle) -Hle #Hle 999 [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle 1000 [ >(le_to_leb_true ?? (le_S_to_le ?? Hle)) in Hind; 1001 >(le_to_leb_true ?? (le_S ?? (le_S_to_le ?? Hle))) 1002 normalize nodelta >lookup_insert_miss 1003 [ >lookup_insert_miss 1004 [ #H @H 1005 | @bitvector_of_nat_abs 1006 [3: @lt_to_not_eq @Hle 1007 |1: @(transitive_lt ??? Hle) 1008 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1009 >append_length @le_S_S @le_plus_n_r 1010 ] 1011 | @bitvector_of_nat_abs 1012 [3: @lt_to_not_eq @le_S_to_le @le_S_S @Hle 1013 |1: @(transitive_lt ??? Hle) @le_S_to_le 1014 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1015 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 1016 ] 1017 | >Hle >Hle in Hind; >(le_to_leb_true ?? (le_n (|prefix|))) 1018 >(le_to_leb_true ?? (le_S ?? (le_n (|prefix|)))) 1019 normalize nodelta >lookup_insert_miss 1020 [ >lookup_insert_hit 1021 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1022 #H @H 1023 | @bitvector_of_nat_abs 1024 [3: @lt_to_not_eq @le_n 1025 |1: @le_S_to_le 1026 ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1027 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 1028 ] 1029 ] 1030 | >Hle >Hle in Hind; 1031 >(not_le_to_leb_false (S (|prefix|)) (|prefix|)) 1032 [2: @le_to_not_lt @le_n] 1033 >(le_to_leb_true ?? (le_n (S (|prefix|)))) 1034 normalize nodelta >lookup_insert_hit 1035 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1036 [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1037 | lapply (proj2 ?? (proj1 ?? Hpolicy)) 1038 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1039 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1040 [ normalize nodelta #_ #_ #abs cases abs 1041 | #x cases x -x #opc #oj #EQo 1042 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1043 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1044 [ normalize nodelta #_ #_ #abs cases abs 1045 | #x cases x -x #Sopc #Soj #EQSo normalize nodelta 1046 #Hadded #Hcommon 1047 >(lookup_opt_lookup_hit … EQSo 〈0,short_jump〉) 1048 >Hcommon >(lookup_opt_lookup_hit … EQo 〈0,short_jump〉) in Holdeq; 1049 #Holdeq >(proj1 ?? (pair_destruct ?????? Holdeq)) 1050 >(commutative_plus old_pc ?) >associative_plus 1051 <Hadded 1052 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 1053 >prf >nth_append_second 1054 [ <minus_n_n whd in match (nth ????); >p1 cases instr in Heq1; 1055 [2,3,6: #x [3: #y] normalize nodelta #Heq1 1056 <(proj2 ?? (pair_destruct ?????? Heq1)) 1057 <(commutative_plus inc_pc) 1058 >(instruction_size_irrelevant ?? oj short_jump) 1059 [1,3,5: #H @H 1060 |2,4,6: @nmk #H @H 1061 ] 1062 |4,5: #x normalize nodelta #Heq1 1063 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1064 cases daemon (* axiomatise this *) 1065 |1: #pi cases pi 1066 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 1067 [1,2,3,6,7,24,25: #x #y 1068 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 1069 normalize nodelta #Heq1 1070 <(proj2 ?? (pair_destruct ?????? Heq1)) 1071 <(commutative_plus inc_pc) 1072 >(instruction_size_irrelevant ?? oj short_jump) 1073 [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: 1074 #H @H 1075 |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 1076 @nmk #H @H 1077 ] 1078 |9,10,11,12,13,14,15,16,17: 1079 #x [3,4,5,8,9: #y] normalize nodelta #Heq1 1080 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1081 cases daemon (* axiomatise this *) 1082 ] 1083 ] 1084 | @le_n 1085 ] 1086 ] 1087 ] 1088 ] 1089 ] 1090 | #X >(not_le_to_leb_false … X) 1091 >(not_le_to_leb_false … (lt_to_not_le … (le_S_to_le … (not_le_to_lt … X)))) in Hind; 1092 normalize nodelta <(proj1 ?? (pair_destruct ?????? Heq2)) 1093 cases instr in Heq1; 1094 [2,3,6: #x [3: #y] normalize nodelta #_ #H @H 1095 |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind 1096 cases daemon (* axiomatise this *) 1097 |1: #pi cases pi 1098 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 1099 [1,2,3,6,7,24,25: #x #y 1100 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 1101 normalize nodelta #_ #H @H 1102 |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 1103 normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 1104 #Hind cases daemon (* axiomatise this *) 1105 ] 1106 ] 1107 ] 1108 ] 1109 ] 1110 | @bitvector_of_nat_abs 1111 [3: @lt_to_not_eq @Hi 1112 |1: @(transitive_lt ??? Hi) 1113 ] 1114 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 1115 @le_S_S @le_plus_n_r 1116 ] 1117 | >Hi >lookup_insert_hit lapply ((proj2 ?? Hpolicy) i) 1118 ] XXX to be continued *) 979 [ >lookup_insert_miss 980 [ (* USE[pass]: sigma_safe *) 981 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 982 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 983 #pc #j normalize nodelta 984 cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉) 985 #Spc #Sj normalize nodelta 986 cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta 987 #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr 988 [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta 989 [1,4,7: *) 990 1119 991 ] 1120 992 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj -
src/ASM/Util.ma
r2149 r2211 1755 1755 cases (lt_to_not_zero … relevant) 1756 1756 qed. 1757 1758 lemma ltb_false_to_not_lt: ∀p,q:ℕ.ltb p q = false → p ≮ q. 1759 #p #q #H @leb_false_to_not_le @H 1760 qed. 1761 1762 lemma ltb_true_to_lt: ∀p,q:ℕ.ltb p q = true → p < q. 1763 #p #q #H @leb_true_to_le @H 1764 qed. 1765 1766 lemma plus_equals_zero: ∀x,y:ℕ.x + y = x → y = 0. 1767 #x #y cases y 1768 [ #_ @refl 1769 | -y #y elim x 1770 [ <plus_O_n / by / 1771 | -x #x #Hind #H2 @Hind normalize in H2; @injective_S @H2 1772 ] 1773 ] 1774 qed.
Note: See TracChangeset
for help on using the changeset viewer.
