Changeset 1555 for src/ASM/Assembly.ma
 Timestamp:
 Nov 24, 2011, 5:19:30 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1528 r1555 1 1 include "ASM/ASM.ma". 2 include "ASM/BitVectorTrie.ma".3 2 include "ASM/Arithmetic.ma". 4 3 include "ASM/Fetch.ma". … … 592 591 qed. 593 592 594 (* lemma coerc_sigma:595 ∀A,P.∀p:A.P p → Σx:A.P x.596 #A #P #a #p % [ @a  /2/]597 qed.598 coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x599 ≝ coerc_sigma on p: ? to (Sig ??). *)600 601 593 lemma coerc_pair_sigma: 602 594 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x). … … 606 598 ≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). 607 599 608 let rec create_label_map (program: list labelled_instruction) 609 (policy: jump_expansion_policy):600 definition create_label_map: ∀program:list labelled_instruction. 601 ∀policy:jump_expansion_policy. 610 602 (Σlabels:label_map. 611 ∀i:ℕ.lt i (program) (* XXX using < causes (false?) ambiguity *)→603 ∀i:ℕ.lt i (program) → 612 604 ∀l.occurs_exactly_once l program → 613 605 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 614 606 ∃a.lookup … labels l = Some ? 〈i,a〉 615 607 ) ≝ 608 λprogram.λpolicy. 616 609 let 〈final_pc, final_labels〉 ≝ 617 610 foldl_strong (option Identifier × pseudo_instruction) 618 611 (λprefix.ℕ × (Σlabels. 619 ∀i:ℕ. i < prefix→612 ∀i:ℕ.lt i (prefix) → 620 613 ∀l.occurs_exactly_once l prefix → 621 614 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → … … 724 717 ]. 725 718 726 definition jmple q: jump_length → jump_length → Prop ≝719 definition jmple: jump_length → jump_length → Prop ≝ 727 720 λj1.λj2. 728 721 match j1 with 729 [ short_jump ⇒ True 730  medium_jump ⇒ 722 [ short_jump ⇒ 731 723 match j2 with 732 724 [ short_jump ⇒ False 733 725  _ ⇒ True 734 726 ] 735  long_jump⇒727  medium_jump ⇒ 736 728 match j2 with 737 729 [ long_jump ⇒ True 738 730  _ ⇒ False 739 731 ] 732  long_jump ⇒ False 740 733 ]. 741 734 742 lemma jmpleq_max_length: ∀x,y.jmpleq y (max_length y x). 743 #x #y744 cases y745 [ // 746  cases x //747  //748 ]749 qed. 750 735 definition jmpleq: jump_length → jump_length → Prop ≝ 736 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 737 738 lemma jmpleq_max_length: ∀ol,nl. 739 jmpleq ol (max_length ol nl). 740 #ol #nl cases ol cases nl 741 /2 by or_introl, or_intror, I/ 742 qed. 743 751 744 definition is_jump' ≝ 752 745 λx:preinstruction Identifier. … … 776 769 definition jump_in_policy ≝ 777 770 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. 778 ∀i:ℕ.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 779 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉. 771 ∀i:ℕ.i < prefix → 772 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 773 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉). 780 774 781 775 axiom bitvector_of_nat_abs: 782 776 ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y). 783 784 let rec jump_expansion_start (program: list labelled_instruction): 785 (Σpolicy.jump_in_policy program policy) ≝ 777 778 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. 779 /2/ qed. 780 781 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 782 ∀policy:(Σp:jump_expansion_policy. 783 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 784 jump_in_policy prefix p). 785 ∀i:ℕ.i < prefix → 786 ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 787 lookup_opt … (bitvector_of_nat 16 i) policy = None ?. 788 #prefix #policy #i #Hi @conj 789 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy)) 790 cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?); 791 [ #H @H 792  #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi)) 793 @(ex_intro … y (ex_intro … z H)) 794 ] 795  #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj) 796 #H elim H H; #x #H elim H H; #y #H >H in Hnone; #abs destruct (abs) 797 ] 798 qed. 799 800 definition jump_expansion_start: ∀program:list labelled_instruction. 801 Σpolicy:jump_expansion_policy.(∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy program policy ≝ 802 λprogram. 786 803 foldl_strong (option Identifier × pseudo_instruction) 787 (λprefix.Σpolicy .jump_in_policy prefix policy)804 (λprefix.Σpolicy:jump_expansion_policy.(∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy prefix policy) 788 805 program 789 806 (λprefix.λx.λtl.λprf.λpolicy. … … 791 808 match instr with 792 809 [ Instruction i ⇒ match i with 793 [ JC _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy794  JNC _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy795  JZ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy796  JNZ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy797  JB _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy798  JNB _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy799  JBC _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy800  CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy801  DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy810 [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 811  JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 812  JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 813  JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 814  JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 815  JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 816  JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 817  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 818  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 802 819  _ ⇒ (eject … policy) 803 820 ] 804  Call c ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy805  Jmp j ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy821  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 822  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 806 823  _ ⇒ (eject … policy) 807 824 ] 808 825 ) (Stub ? ?). 809 [43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] ] 810 whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 811 #Hi 812 [2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84: 813 >nth_append_second >(injective_S … Hi) 814 [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,58,60,62: @le_n] 815 <minus_n_n #Hj normalize in Hj; @⊥ @Hj 816 4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi) 817 [2,4,6,8,10,12,14,16,18,20,22: @le_n] 818 <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] % 819 [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit 826 @conj 827 (* nonjumps, lookup_opt = None *) 828 [1,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,69,71,73,75,77,79,81,83: 829 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 830 Hi; #Hi @((proj1 ?? (sig2 ?? policy)) i) 831 [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,63,65: 832 @le_S_to_le @le_S_to_le @Hi 833 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,58,60,62,64,66: 834 <Hi @le_n_Sn 835 ] 836 (* nonjumps, lookup_opt = Some *) 837 2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84: 838 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 839 Hi; #Hi 840 [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,63,65: 841 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 842 @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 843 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,58,60,62,64,66: 844 @conj >(injective_S … Hi) 845 [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,63,65: 846 >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 847 <minus_n_n #H @⊥ @H 848 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,58,60,62,64,66: 849 #H elim H; H; #t1 #H elim H; H #t2 #H 850 lapply (proj1 ?? (sig2 ?? policy) (prefix) (le_n (prefix))) 851 #H2 >H2 in H; #H destruct (H) 852 ] 853 ] 854 (* jumps, lookup_opt = None *) 855 3,5,51,53,55,57,59,61,63,65,67: #i >append_length <commutative_plus #Hi normalize in Hi; 856 >lookup_opt_insert_miss 857 [1,3,5,7,9,11,13,15,17,19,21,23: @((proj1 ?? (sig2 ?? policy)) i) @(le_S_to_le … Hi) 858 2,4,6,8,10,12,14,16,18,20,22,24: >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 859 ] 860 (* nonjumps, lookup_opt = Some *) 861 4,6,52,54,56,58,60,62,64,66,68: #i >append_length <commutative_plus #Hi normalize in Hi; 862 cases (le_to_or_lt_eq … Hi) Hi; #Hi 863 [1,3,5,7,9,11,13,15,17,19,21,23: >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 864 >lookup_opt_insert_miss 865 [1,3,5,7,9,11,13,15,17,19,21,23: @((proj2 ?? (sig2 ?? policy)) i) @(le_S_S_to_le … Hi) 866 2,4,6,8,10,12,14,16,18,20,22,24: @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 867 ] 868 2,4,6,8,10,12,14,16,18,20,22,24: @conj >(injective_S … Hi) #H 869 [2,4,6,8,10,12,14,16,18,20,22,24: >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 870 <minus_n_n // ] 871 @(ex_intro ? ? 0 (ex_intro ? ? short_jump (lookup_opt_insert_hit ? ? 16 ? policy))) 872 ] 873 (* cases for the empty program *) 874 85: #i #Hi // 875 86: whd #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] 820 876 ] 821 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 822 lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj) 823 #p #H elim H #j #Hpj % 824 [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,63,65,67,69,71,73,75,77,79,81,83: @p] % 825 [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,63,65,67,69,71,73,75,77,79,81,83: @j] 826 [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss] 827 [2,4,6,8,10,12,14,16,18,20,22: @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) ] @Hpj 828 qed. 829 830 (* not really recursive *) 831 let rec jump_expansion_step (program: list labelled_instruction) 832 (old_policy: Σpolicy.jump_in_policy program policy): 877 qed. 878 879 definition policy_increase: list labelled_instruction → jump_expansion_policy → 880 jump_expansion_policy → Prop ≝ 881 λprogram.λop.λp. 882 (* (∀i:ℕ.i < program → 883 lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *) 884 (∀i:ℕ.i < program → 885 jmpleq 886 (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉)) 887 (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))). 888 889 definition jump_expansion_step: ∀program:list labelled_instruction. 890 ∀old_policy:(Σpolicy. 891 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 892 jump_in_policy program policy). 833 893 (Σpolicy. 834 And (jump_in_policy program policy) (* XXX ∧ causes ambiguity *) 835 (jump_in_policy program policy → 836 (∀i.lt i (program) (* XXX < causes ambiguity *) → is_jump (nth i ? program 〈None ?, Comment []〉) → 837 jmpleq 838 (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉)) 839 (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉))) 840 ) 841 ) ≝ 894 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 895 jump_in_policy program policy ∧ 896 policy_increase program old_policy policy) 897 ≝ 898 λprogram.λold_policy. 842 899 let labels ≝ create_label_map program old_policy in 843 900 let 〈final_pc, final_policy〉 ≝ 844 901 foldl_strong (option Identifier × pseudo_instruction) 845 902 (λprefix.ℕ × Σpolicy. 903 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 846 904 jump_in_policy prefix policy ∧ 847 (jump_in_policy prefix policy → 848 (∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 849 jmpleq 850 (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉)) 851 (\snd (lookup … (bitvector_of_nat 16 i) policy 〈0,short_jump〉))) 852 ) 905 policy_increase prefix old_policy policy 853 906 ) 854 907 program … … 876 929 ) 〈0, Stub ? ?〉 in 877 930 final_policy. 878 [ @conj 879 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 880 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 881 lapply (sig2 … policy) #Hacc elim ((proj1 … Hacc) i (le_S_S_to_le … Hi) Hj) #h #n elim n 882 n #n #Hn 883 % [ @h  % [ @n  normalize nodelta cases instr normalize nodelta 884 [2,3: #x cases (lookup ??? old_policy ?) #y #z @Hn 885 6: #x #y cases (lookup ??? old_policy ?) #w #z @Hn 886 1: #pi cases (lookup ??? old_policy ?) #x #y cases (jump_expansion_step_instruction ???) 887 [ @Hn 888  #z normalize nodelta <Hn @lookup_opt_insert_miss 889 @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 931 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 932 [ cases (lookup ??? old_policy ?) #h #n cases add_instr 933 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi)) 934  #z normalize nodelta >lookup_opt_insert_miss 935 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi)) 936  >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 937 ] 938 ] 939  cases (le_to_or_lt_eq … Hi) Hi; 940 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj 941 [ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 942 cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y 943 [ @(proj1 ?? Hacc Hj) 944  #z elim (proj1 ?? Hacc Hj) #h #n elim n n #n #Hn 945 % [ @h  % [ @n  <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs 946 @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) ] ] 947 ] 948  lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 949 #H elim H H; #h #H elim H H; #n cases add_instr cases (lookup ??? old_policy ?) 950 normalize nodelta #x #y [2: #z] 951 #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?)) 952 [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) 953  @Hl 954 ] 955 ] 956  #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 957 <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr 958 [1: #pi  2,3: #x  4,5: #id  6: #x #y] @conj normalize nodelta 959 [3,5,11: #H @⊥ @H (* instr is not a jump *) 960 4,6,12: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 961 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) 962 #H destruct (H) 963 7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n 964 whd in match (snd ???); @(ex_intro ?? pc) 965 [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id))) 966  @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id))) 967 ] @lookup_opt_insert_hit 968 8,10: #_ // 969 1,2: cases pi 970 [35,36,37: #H @⊥ @H 971 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H 972 1,2,3,6,7,33,34: #x #y #H @⊥ @H 973 9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n 974 whd in match (snd ???); 975 @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?)) 976 @lookup_opt_insert_hit 977 11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n 978 whd in match (snd ???); 979 @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?)) 980 @lookup_opt_insert_hit 981 72,73,74: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 982 #x #y normalize nodelta 983 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 984 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 985 #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 986 #x #y normalize nodelta 987 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 988 38,39,40,43,44,70,71: #x #y #H elim H H; #h #H elim H H #n 989 cases (lookup ??? old_policy ?) #x #y normalize nodelta 990 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 991 46,47,51,52: #id #_ // 992 48,49,50,53,54: #x #id #_ // 993 ] 994 ] 995 ] 996 ] 997  lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %); 998 [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 999 cases (le_to_or_lt_eq … Hi) Hi; #Hi 1000 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1001 #x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 1002  normalize nodelta >(injective_S … Hi) 1003 >lookup_opt_lookup_miss 1004 [ >lookup_opt_lookup_miss 1005 [ // 1006  cases (lookup ?? (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1007 #x #y normalize nodelta 1008 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) // 890 1009 ] 891 4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn 892 @lookup_opt_insert_miss @bitvector_of_nat_abs 893 @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 894 ] ] ] 895  #Hi >nth_append_second >(injective_S … Hi) 896 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 897 [2,3: #x #Hj @⊥ @Hj 898 6: #x #y #Hj @⊥ @Hj 899 1: #pi cases pi 900 [35,36,37: #Hj @⊥ @Hj 901 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj 902 1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj 903 9,10,14,15: #j normalize nodelta #_ 904 % [1,3,5,7: @pc 905 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 906 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %); 907 #x #y #Hl normalize nodelta 908 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j)) 909 2,4,6,8: @lookup_opt_insert_hit 910 ] ] 911 11,12,13,16,17: #x #j normalize nodelta #_ 912 % [1,3,5,7,9: @pc 913 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 914 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %); 915 #x #y #Hl normalize nodelta 916 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j)) 917 2,4,6,8,10: @lookup_opt_insert_hit 918 ] ] 919 ] 920 4,5: #j normalize nodelta #_ 921 % [1,3: @pc 922 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 923 #x #y normalize nodelta 924 % [1: @(max_length y (select_jump_length (create_label_map program old_policy) pc j)) 925 3: @(max_length y (select_call_length (create_label_map program old_policy) pc j)) 926 2,4: @lookup_opt_insert_hit 927 ] 928 ] 929 ] 930  @le_n 1010  >(proj1 ?? (jump_not_in_policy program old_policy (prefix) ?)) 1011 [ // 1012  >prf >p1 >nth_append_second [ <minus_n_n 1013 generalize in match Ha; normalize nodelta cases instr normalize nodelta 1014 [1: #pi cases pi 1015 [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/ 1016 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/ 1017 35,36,37: #H normalize /2 by nmk/ 1018 9,10,14,15: #id whd in match (jump_expansion_step_instruction ???); 1019 #H destruct (H) 1020 11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???); 1021 #H destruct (H) 1022 ] 1023 2,3: #x #H normalize /2 by nmk/ 1024 6: #x #y #H normalize /2 by nmk/ 1025 4,5: #id #H destruct (H) 1026 ]  @le_n ] 1027  >prf >append_length normalize <plus_n_Sm @le_plus_n_r 1028 ] 931 1029 ] 932 1030 ] 933  #Hjip #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 934 [ #Hi >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 935 lapply (sig2 … policy) #Hpolicy normalize nodelta cases instr normalize nodelta 936 [2,3: #x cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #y #z 937 normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 938 6: #x #y cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #w #z 939 normalize nodelta @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 940 1: #pi cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #x #y 941 cases (jump_expansion_step_instruction ???) 942 [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 943  #z normalize nodelta 944 whd in match (snd ℕ jump_expansion_policy ?); >lookup_insert_miss 945 [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 946  @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 1031  #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi; 1032 cases (le_to_or_lt_eq … Hi) Hi; #Hi 1033 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1034 #y #z normalize nodelta normalize nodelta >lookup_insert_miss 1035 [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 1036  @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) 1037 ] 1038  >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (prefix) ?) ?) 1039 [ #a #H elim H H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H) 1040 normalize nodelta >lookup_insert_hit @jmpleq_max_length 1041  >prf >p1 >nth_append_second 1042 [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta 1043 [1: #pi cases pi 1044 [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H) 1045 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) 1046 35,36,37: #H normalize in H; destruct (H) 1047 9,10,14,15: #id #H // 1048 11,12,13,16,17: #x #id #H // 1049 ] 1050 2,3: #x #H normalize in H; destruct (H) 1051 6: #x #y #H normalize in H; destruct (H) 1052 4,5: #id #H // 947 1053 ] 948 ] 949 4,5: #id cases (lookup ? 16 (bitvector_of_nat 16 (prefix)) old_policy ?) #x #y 950 normalize nodelta >lookup_insert_miss 951 [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 952 2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 953 ] 1054  @le_n ] 1055  >prf >append_length normalize <plus_n_Sm @le_plus_n_r 954 1056 ] 955  #Hi >nth_append_second >(injective_S … Hi) 956 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 957 [2,3: #x #Hj @⊥ @Hj 958 6: #x #y #Hj @⊥ @Hj 959 1: #pi cases pi 960 [35,36,37: #Hj @⊥ @Hj 961 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj 962 1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj 963 9,10,14,15: #j normalize nodelta #_ 964 cases (lookup ???? 〈0,short_jump〉) #x #y 965 whd in match (snd ℕ jump_expansion_policy ?); 966 >lookup_insert_hit normalize @jmpleq_max_length 967 11,12,13,16,17: #z #j normalize nodelta #_ 968 cases (lookup ???? 〈0,short_jump〉) #x #y 969 whd in match (snd ℕ jump_expansion_policy ?); 970 >lookup_insert_hit normalize @jmpleq_max_length 971 ] 972 4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y 973 whd in match (snd ℕ jump_expansion_policy ?); 974 >lookup_insert_hit normalize @jmpleq_max_length 975 ] 976  @le_n 977 ] 978 ] 979 ] 980  @conj 981 [ #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 982  #H #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 983 ] 1057 ] 1058 ] ] 1059  @conj [ @conj 1060 [ #i #Hi // 1061  #i #Hi @conj [ >nth_nil #H @⊥ @H  #H elim H #x #H1 elim H1 #y #H2 1062 normalize in H2; destruct (H2) ] 1063 ] 1064  #i #Hi @⊥ @(absurd (i<0)) [ @Hi  @(not_le_Sn_O) ] 984 1065 ] 985 1066 qed. 986 1067 987 1068 let rec jump_expansion_internal (program: list labelled_instruction) 988 (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝ 1069 (n: ℕ) on n: (Σpolicy:jump_expansion_policy. 1070 And 1071 (∀i:ℕ.i ≥ program → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?) 1072 (jump_in_policy program policy)) ≝ 989 1073 match n with 990 1074 [ O ⇒ jump_expansion_start program … … 995 1079 ] 996 1080 qed. 1081 1082 definition policy_equal ≝ 1083 λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy. 1084 ∀n:ℕ.n < program → 1085 (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) = 1086 (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)). 1087 1088 lemma pe_refl: 1089 ∀program.reflexive ? (policy_equal program). 1090 #program whd #x whd #n #Hn @refl 1091 qed. 1092 1093 lemma pe_sym: 1094 ∀program.symmetric ? (policy_equal program). 1095 #program whd #x #y #Hxy whd #n #Hn 1096 >(Hxy n Hn) @refl 1097 qed. 1098 1099 lemma pe_trans: 1100 ∀program.transitive ? (policy_equal program). 1101 #program whd #x #y #z #Hxy #Hyz whd #n #Hn 1102 >(Hxy n Hn) @(Hyz n Hn) 1103 qed. 1104 1105 lemma le_plus: 1106 ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k. 1107 #n #m elim m m; 1108 [ #Hn % [ @O  <(le_n_O_to_eq n Hn) // ] 1109  #m #Hind #Hn cases (le_to_or_lt_eq … Hn) Hn; #Hn 1110 [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k)  >Hk // ] 1111  % [ @O  <Hn // ] 1112 ] 1113 ] 1114 qed. 1115 1116 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. 1117 #n (elim n) normalize /2 by S_pred/ qed. 1118 1119 lemma pe_step: ∀program:list labelled_instruction. 1120 ∀p1,p2:Σpolicy. 1121 (∀i:ℕ.i ≥ program → lookup_opt … (bitvector_of_nat ? i) policy = None ?) 1122 ∧jump_in_policy program policy. 1123 policy_equal program p1 p2 → 1124 policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2). 1125 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H 1126 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1)) 1127 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?); 1128 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl) 1129 #Hnotjmp >lookup_opt_lookup_miss 1130 [ >lookup_opt_lookup_miss 1131 [ @refl 1132  @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn)) 1133 [ @(proj1 ?? (sig2 … (jump_expansion_step program p2))) 1134  @Hnotjmp 1135 ] 1136 ] 1137  @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn)) 1138 [ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1))) 1139  @Hnotjmp 1140 ] 1141 ] 1142  #x #Hl cases daemon 1143 ] 1144 qed. 1145 1146 lemma equal_remains_equal: ∀program:list labelled_instruction.∀n:ℕ. 1147 policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) → 1148 ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k). 1149 #program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H H Hk k; 1150 lapply Heq Heq; lapply n n; elim z z; 1151 [ #n #Heq <plus_n_O @pe_refl 1152  #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n))) 1153 [ @Heq 1154  @pe_step @Hind @Heq 1155 ] 1156 ] 1157 qed. 1158 1159 lemma dec_bounded_forall: 1160 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n). 1161 #P #HP_dec #k elim k k 1162 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O 1163  #k #Hind cases Hind 1164 [ #Hk cases (HP_dec k) 1165 [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn) 1166 [ #H @(Hk … (le_S_S_to_le … H)) 1167  #H >(injective_S … H) @HPk 1168 ] 1169  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ] 1170 ] 1171  #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ] 1172 ] 1173 ] 1174 qed. 1175 1176 lemma dec_bounded_exists: 1177 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n). 1178 #P #HP_dec #k elim k k 1179 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O 1180  #k #Hind cases Hind 1181 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ] 1182  #Hk cases (HP_dec k) 1183 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ] 1184  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn)) 1185 [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj 1186 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ] 1187  #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn)  @HPk ] 1188 ] 1189 ] 1190 ] 1191 ] 1192 qed. 1193 1194 lemma not_exists_forall: 1195 ∀A:Type[0].∀P:A → Prop.¬(∃x.P x) → ∀x.¬P x. 1196 #A #P #Hex #x @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) @Habs 1197 qed. 1198 1199 lemma de_morgan1: 1200 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B. 1201 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA  @H ]  @Hnot ] 1202 qed. 1203 1204 lemma thingie: 1205 ∀A:Prop.(A + ¬A) → (¬¬A) → A. 1206 #A #Adec #nnA cases Adec 1207 [ // 1208  #H @⊥ @(absurd (¬A) H nnA) 1209 ] 1210 qed. 1211 1212 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b). 1213 #a #b cases a cases b /2/ 1214 %2 @nmk #H destruct (H) 1215 qed. 1216 1217 lemma incr_or_equal: ∀program:list labelled_instruction. 1218 ∀policy:(Σp:jump_expansion_policy. 1219 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1220 jump_in_policy program p). 1221 policy_equal program policy (jump_expansion_step program policy) ∨ 1222 ∃n:ℕ.jmple 1223 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1224 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)). 1225 #program #policy cases (dec_bounded_exists 1226 (λk. 1227 \snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠ 1228 \snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉)) 1229 ? (program)) 1230 [ #H %2 elim H H; #i #Hi 1231 cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi)) 1232 [ #H @(ex_intro … i H) 1233  #H @⊥ @(absurd ? H (proj2 ?? Hi)) 1234 ] 1235  #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H H #H; @nmk #H2 @H 1236 @(ex_intro … i) @conj [ @Hi  @H2 ] 1237  #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1238 (\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) 1239 [ #H %2 @nmk #H1 elim H1 #H2 @H2 @H 1240  #H %1 @H 1241 ] 1242 ] 1243 qed. 997 1244 998 1245 (**************************************** START OF POLICY ABSTRACTION ********************)
Note: See TracChangeset
for help on using the changeset viewer.