Changeset 2228
- Timestamp:
- Jul 20, 2012, 9:10:21 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2225 r2228 647 647 [ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉) 648 648 #x #y #Hx normalize nodelta >Hx / by refl/ 649 | #ppc #ppc_ok normalize nodelta @conj 649 | #ppc #ppc_ok normalize nodelta 650 >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) = 651 \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉)) 652 [2: whd in match fetch_pseudo_instruction; normalize nodelta 653 >(nth_safe_nth … 〈None ?, Comment []〉) 654 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 655 #lbl #ins % ] 656 @conj 650 657 [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok) 651 658 >bitvector_of_nat_inverse_nat_of_bitvector 652 lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);653 [ #Hl normalize nodelta#abs cases abs654 | #x cases x -x#pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm659 inversion (lookup_opt ????) normalize nodelta 660 [ #Hl #abs cases abs 661 | * #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm 655 662 >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative 656 lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol)) 657 cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %); 658 [ #Hl normalize nodelta #abs cases abs 659 | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact 663 inversion (lookup_opt ????) normalize nodelta 664 [ #_ #abs cases abs 665 | * #Spc #Sjl #SHl normalize nodelta #Hcompact 660 666 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta 661 667 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 662 >add_bitvector_of_nat_plus >Hcompact @eq_f @eq_f @eq_f 663 whd in match (fetch_pseudo_instruction ???); >nth_safe_nth 664 [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]] 668 >add_bitvector_of_nat_plus >Hcompact % ]] 665 669 | (* Basic proof scheme: 666 670 - ppc < |snd program|, hence our instruction is in the program … … 675 679 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok) 676 680 >bitvector_of_nat_inverse_nat_of_bitvector 677 lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %); 678 [ normalize nodelta #_ #abs cases abs 679 | #x cases x -x #pc #jl #EQ normalize nodelta 680 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol)) 681 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %); 682 [ normalize nodelta #_ #abs cases abs 683 | #x cases x -x #Spc #Sjl #SEQ normalize nodelta 684 #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 681 inversion (lookup_opt ????) normalize nodelta 682 [ #_ #abs cases abs 683 | * #pc #jl #Hl normalize nodelta 684 inversion (lookup_opt ????) normalize nodelta 685 [ #_ #abs cases abs 686 | * #Spc #Sjl #SHl normalize nodelta #Hcompact 687 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta 685 688 >nat_of_bitvector_bitvector_of_nat_inverse 686 689 [2: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)) 687 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ〈0,short_jump〉)690 >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) 688 691 #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H ] 689 692 lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)) 690 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >H -H #H @(transitive_le … H) 691 cut (∀x,y. x=y → x ≤ y) [ #x #y * %] #eq_to_leq @eq_to_leq @eq_f @eq_f 692 whd in match (fetch_pseudo_instruction ???); >nth_safe_nth 693 [ cases (nth ? labelled_instruction ??) |2: skip] normalize nodelta // ]] 693 >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) >Hcompact #X @X ]] 694 694 | (* the program is of length 2^16 and ppc is followed by only zero-size instructions 695 695 * until the end of the program *) … … 712 712 [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 713 713 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1 714 >Hc in HSpc; 715 whd in match create_label_map; 716 whd in match fetch_pseudo_instruction; normalize nodelta 717 >(nth_safe_nth … 〈None ?, Comment []〉) 718 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉) 719 #lbl #ins normalize nodelta #X @X 714 >Hc in HSpc; #X @X 720 715 | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc 721 716 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj 722 [ #ppc' #ppc_ok' #Hppc' 717 [2: >Hc in Hspc; #X @X 718 | #ppc' #ppc_ok' #Hppc' 723 719 (* S ppc < ppc' < |\snd program| *) 724 720 (* lookup S ppc = 2^16 *) … … 727 723 lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok') 728 724 >bitvector_of_nat_inverse_nat_of_bitvector 729 lapply (refl ? (lookup_opt … ppc' fpol)) 730 cases (lookup_opt … ppc' fpol) in ⊢ (???% → %); 731 [ normalize nodelta #_ #abs cases abs 732 | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta 733 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol)) 734 cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %); 735 [ normalize nodelta #_ #abs cases abs 736 | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta 725 inversion (lookup_opt ????) normalize nodelta 726 [ #_ #abs cases abs 727 | * #xpc #xjl #XEQ normalize nodelta 728 inversion (lookup_opt ????) normalize nodelta 729 [ #_ #abs cases abs 730 | * #Sxpc #Sxjl #SXEQ normalize nodelta 737 731 #Hpcompact 738 732 lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok')) … … 756 750 ] 757 751 ] 758 | >Hc in Hspc;759 whd in match create_label_map;760 whd in match fetch_pseudo_instruction; normalize nodelta761 >(nth_safe_nth … 〈None ?, Comment []〉)762 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)763 #lbl #ins normalize nodelta764 whd in match instruction_size;765 whd in match assembly_1_pseudoinstruction;766 whd in match expand_pseudo_instruction; normalize nodelta767 <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector768 >add_commutative #SEQ cases ins769 [2,3,6: #x [3: #y] normalize nodelta #H @H770 |4,5: #x normalize nodelta771 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)772 >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)773 cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)774 #lpc #ljl normalize nodelta #H @H775 |1: #pi normalize nodelta #X @X776 ]777 752 ] 778 753 ]
Note: See TracChangeset
for help on using the changeset viewer.