Changeset 1592 for src/ASM/Assembly.ma
 Timestamp:
 Dec 7, 2011, 2:50:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1578 r1592 553 553 let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in 554 554 let bv: list (BitVector 8) ≝ match ilist with 555 [ None ⇒ (* hmm,this shouldn't happen *) [ ]555 [ None ⇒ (* this shouldn't happen *) [ ] 556 556  Some l ⇒ flatten … (map … assembly1 l) 557 557 ] in … … 777 777 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉). 778 778 779 axiom bitvector_of_nat_abs:780 ∀x,y:ℕ.x ≠ y → ¬eq_bv 16 (bitvector_of_nat 16 x) (bitvector_of_nat 16 y).781 782 779 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. 783 780 /2/ qed. 781 782 lemma bitvector_of_nat_ok: 783 ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. 784 #n elim n n 785 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl 786  #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *) 787 ] 788 qed. 789 790 lemma bitvector_of_nat_abs: 791 ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y). 792 #n #x #y #Hx #Hy #Heq @notb_elim 793 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) 794 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %); 795 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H // 796  #H // 797 ] 798 qed. 799 784 800 785 801 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. 786 802 ∀policy:(Σp:jump_expansion_policy. 787 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧803 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 788 804 jump_in_policy prefix p). 789 805 ∀i:ℕ.i < prefix → … … 802 818 qed. 803 819 804 definition jump_expansion_start: ∀program:list labelled_instruction. 820 definition jump_expansion_start: 821 ∀program:(Σl:list labelled_instruction.l < 2^16). 805 822 Σpolicy:jump_expansion_policy. 806 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧823 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 807 824 jump_in_policy program policy ∧ 808 825 ∀i.i < program → is_jump (nth i ? program 〈None ?, Comment []〉) → … … 811 828 foldl_strong (option Identifier × pseudo_instruction) 812 829 (λprefix.Σpolicy:jump_expansion_policy. 813 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧830 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 814 831 jump_in_policy prefix policy ∧ 815 832 ∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → … … 842 859 #i >append_length <commutative_plus #Hi normalize in Hi; 843 860 [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: 844 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i) 845 [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: 846 <Hi @le_n_Sn 847 ] 848 @le_S_to_le @le_S_to_le @Hi 861 #Hi2 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i) 862 [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121: 863 @le_S_to_le @le_S_to_le @Hi 864 2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122: 865 @Hi2 866 3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123: 867 <Hi @le_n_Sn 868 4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124: 869 @Hi2 870 ] 849 871 ] 850 872 cases (le_to_or_lt_eq … Hi) Hi; #Hi … … 858 880 ] 859 881 #H elim H; H; #t1 #H elim H; H #t2 #H 860 lapply (proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) 861 #H2 >H2 in H; #H destruct (H) 882 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) in H; 883 [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: 884 #H destruct (H) 885 ] 886 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 887 @le_plus_n_r 862 888 ] 863 889 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) … … 872 898 [1,3,5,7,9,11,13,15,17,19,21: @conj 873 899 [1,3,5,7,9,11,13,15,17,19,21: 874 #i >append_length <commutative_plus #Hi normalize in Hi; >lookup_opt_insert_miss900 #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss 875 901 [1,3,5,7,9,11,13,15,17,19,21: 876 @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi)) 877 ] 878 >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 902 @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2) 903 ] 904 >eq_bv_sym @bitvector_of_nat_abs 905 [1,4,7,10,13,16,19,22,25,28,31: 906 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 907 @le_plus_n_r 908 2,5,8,11,14,17,20,23,26,29,32: @Hi2 909 3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi 910 ] 879 911 ] 880 912 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) … … 885 917 @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 886 918 ] 887 @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 919 @bitvector_of_nat_abs 920 [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) 921 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 922 ] 923 @(transitive_lt … (sig2 ?? program)) 924 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 888 925 ] 889 926 @conj >(injective_S … Hi) #H … … 900 937 @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj) 901 938 ] 902 @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 939 @bitvector_of_nat_abs 940 [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi)) 941 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 942 ] 943 @(transitive_lt … (sig2 ?? program)) 944 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 903 945 ] 904 946 #_ >(injective_S … Hi) @lookup_opt_insert_hit … … 915 957 jump_expansion_policy → Prop ≝ 916 958 λprogram.λop.λp. 917 (* (∀i:ℕ.i < program →918 lookup_opt … (bitvector_of_nat ? i) op = lookup_opt … (bitvector_of_nat ? i) p) ∨ *)919 959 (∀i:ℕ.i < program → 920 960 jmpleq … … 922 962 (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))). 923 963 924 definition jump_expansion_step: ∀program: list labelled_instruction.964 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 925 965 ∀old_policy:(Σpolicy. 926 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧966 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 927 967 jump_in_policy program policy). 928 968 (Σpolicy. 929 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧969 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 930 970 jump_in_policy program policy ∧ 931 971 policy_increase program old_policy policy) … … 936 976 foldl_strong (option Identifier × pseudo_instruction) 937 977 (λprefix.ℕ × Σpolicy. 938 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧978 (∀i.i ≥ prefix → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 939 979 jump_in_policy prefix policy ∧ 940 980 policy_increase prefix old_policy policy … … 965 1005 final_policy. 966 1006 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 967 [ cases (lookup ??? old_policy ?) #h #n cases add_instr968 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) )1007 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr 1008 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2) 969 1009  #z normalize nodelta >lookup_opt_insert_miss 970 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi)) 971  >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 1010 [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2) 1011  >eq_bv_sym @bitvector_of_nat_abs 1012 [ @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1013 @le_S_S @le_plus_n_r 1014  @Hi2 1015  @lt_to_not_eq @Hi 1016 ] 972 1017 ] 973 1018 ] … … 979 1024  #z elim (proj1 ?? Hacc Hj) #h #n elim n n #n #Hn 980 1025 % [ @h  % [ @n  <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs 981 @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) ] ] 1026 [3: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 1027 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1028 ] 1029 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1030 @le_S_S @le_plus_n_r 1031 ] ] 982 1032 ] 983 1033  lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc … … 985 1035 normalize nodelta #x #y [2: #z] 986 1036 #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?)) 987 [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) 1037 [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs 1038 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1039 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1040 ] 1041 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1042 @le_S_S @le_plus_n_r 988 1043  @Hl 989 1044 ] … … 994 1049 [3,5,11: #H @⊥ @H (* instr is not a jump *) 995 1050 4,6,12: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 996 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) 997 #H destruct (H) 1051 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) 1052 [1,3,5: #H destruct (H)] 1053 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1054 @le_S_S @le_plus_n_r 998 1055 7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n 999 1056 whd in match (snd ???); @(ex_intro ?? pc) … … 1016 1073 72,73,74: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 1017 1074 #x #y normalize nodelta 1018 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 1075 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) 1076 [1,3,5: #H destruct (H)] 1077 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1078 @le_S_S @le_plus_n_r 1019 1079 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 1020 1080 #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 1021 1081 #x #y normalize nodelta 1022 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 1082 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) 1083 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)] 1084 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1085 @le_S_S @le_plus_n_r 1023 1086 38,39,40,43,44,70,71: #x #y #H elim H H; #h #H elim H H #n 1024 1087 cases (lookup ??? old_policy ?) #x #y normalize nodelta 1025 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) #H destruct (H) 1088 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) 1089 [1,3,5,7,9,11,13: #H destruct (H)] 1090 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1091 @le_S_S @le_plus_n_r 1026 1092 46,47,51,52: #id #_ // 1027 1093 48,49,50,53,54: #x #id #_ // … … 1041 1107  cases (lookup ?? (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1042 1108 #x #y normalize nodelta 1043 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) // 1109 >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix)) ?) 1110 [ // 1111  @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1112 @le_S_S @le_plus_n_r 1113 ] 1044 1114 ] 1045  >(proj1 ?? (jump_not_in_policy programold_policy (prefix) ?))1115  >(proj1 ?? (jump_not_in_policy (eject … program) old_policy (prefix) ?)) 1046 1116 [ // 1047 1117  >prf >p1 >nth_append_second [ <minus_n_n … … 1069 1139 #y #z normalize nodelta normalize nodelta >lookup_insert_miss 1070 1140 [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 1071  @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) 1141  @bitvector_of_nat_abs 1142 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1143 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 1144 ] 1145 @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm 1146 @le_S_S @le_plus_n_r 1072 1147 ] 1073 1148  >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (prefix) ?) ?) … … 1101 1176 qed. 1102 1177 1103 let rec jump_expansion_internal (program: list labelled_instruction)1178 let rec jump_expansion_internal (program: Σl:list labelled_instruction.l < 2^16) 1104 1179 (n: ℕ) on n: (Σpolicy:jump_expansion_policy. 1105 1180 And 1106 (∀i:ℕ.i ≥ program → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)1181 (∀i:ℕ.i ≥ program → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?) 1107 1182 (jump_in_policy program policy)) ≝ 1108 1183 match n with … … 1152 1227 #n (elim n) normalize /2 by S_pred/ qed. 1153 1228 1154 lemma pe_step: ∀program: list labelled_instruction.1229 lemma pe_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 1155 1230 ∀p1,p2:Σpolicy. 1156 (∀i:ℕ.i ≥ program → lookup_opt … (bitvector_of_nat ? i) policy = None ?)1231 (∀i:ℕ.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?) 1157 1232 ∧jump_in_policy program policy. 1158 1233 policy_equal program p1 p2 → … … 1179 1254 qed. 1180 1255 1181 lemma equal_remains_equal: ∀program: list labelled_instruction.∀n:ℕ.1256 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.l < 2^16).∀n:ℕ. 1182 1257 policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) → 1183 1258 ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k). … … 1250 1325 qed. 1251 1326 1252 (* lemma de_morgan1:1253 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.1254 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA  @H ]  @Hnot ]1255 qed. *)1256 1257 1327 lemma thingie: 1258 1328 ∀A:Prop.(A + ¬A) → (¬¬A) → A. … … 1268 1338 qed. 1269 1339 1270 (* lemma incr_or_equal: ∀program:list labelled_instruction. 1271 ∀policy:(Σp:jump_expansion_policy. 1272 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1273 jump_in_policy program p). 1274 policy_equal program policy (jump_expansion_step program policy) ∨ 1275 ∃n:ℕ.n < (program) ∧ jmple 1276 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1277 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)). 1278 #program #policy cases (dec_bounded_exists 1279 (λk. 1280 \snd (bvt_lookup ?? (bitvector_of_nat ? k) policy 〈0,short_jump〉) ≠ 1281 \snd (bvt_lookup ?? (bitvector_of_nat ? k) (jump_expansion_step program policy) 〈0,short_jump〉)) 1282 ? (program)) 1283 [ #H %2 elim H H; #i #Hi 1284 cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi)) 1285 [ #H @(ex_intro ?? i (conj ?? (proj1 ?? Hi) H)) 1286  #H @⊥ @(absurd ? H (proj2 ?? Hi)) 1287 ] 1288  #H %1 whd #i #Hi @(thingie ? (dec_eq_jump_length ??)) elim H H #H; @nmk #H2 @H 1289 @(ex_intro … i) @conj [ @Hi  @H2 ] 1290  #n cases (dec_eq_jump_length (\snd (lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1291 (\snd (lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) 1292 [ #H %2 @nmk #H1 elim H1 #H2 @H2 @H 1293  #H %1 @H 1294 ] 1295 ] 1296 qed. *) 1297 1298 lemma policy_not_equal_incr: ∀program:list labelled_instruction. 1340 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.l<2^16). 1299 1341 ∀policy:(Σp:jump_expansion_policy. 1300 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧1342 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1301 1343 jump_in_policy program p). 1302 1344 ¬policy_equal program policy (jump_expansion_step program policy) → … … 1338 1380 λprogram.λpolicy.measure_int program policy 0. 1339 1381 1340 (* lemma measure_le: ∀program.∀policy.∀x,y:ℕ.1341 x ≤ y → measure_int program policy x ≤ measure_int program policy y.1342 #program #policy1343 elim program1344 [ //1345  #h #t #Hind #x #y #Hxy whd in match (measure_int ??x); whd in match (measure_int ??y);1346 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,short_jump〉))1347 [ @Hind @Hxy1348 2,3: @Hind @monotonic_le_plus_l @Hxy1349 ]1350 ]1351 qed. *)1352 1353 1382 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. 1354 1383 measure_int program policy (x+d) = measure_int program policy x + d. … … 1367 1396 qed. 1368 1397 1369 lemma measure_incr_or_equal: ∀program.∀policy:Σp:jump_expansion_policy. 1370 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1398 lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.l<2^16. 1399 ∀policy:Σp:jump_expansion_policy. 1400 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1371 1401 jump_in_policy program p.∀l.l ≤ program → ∀acc:ℕ. 1372 1402 measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc. 1373 #program #policy #l (* lapply (le_n (program)) *)elim l l;1403 #program #policy #l elim l l; 1374 1404 [ #Hp #acc normalize @le_n 1375 1405  #h #t #Hind #Hp #acc … … 1461 1491 qed. 1462 1492 1463 lemma measure_special: ∀program.∀policy:Σp:jump_expansion_policy. 1464 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1493 (* how to do this with a sigmatype and elimination? *) 1494 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1495 ∀policy:Σp:jump_expansion_policy. 1496 (∀i.i ≥ program → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1465 1497 jump_in_policy program p. 1466 1498 measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 → 1467 1499 policy_equal program policy (jump_expansion_step program policy). 1468 #program lapply (le_n (program)) elim program in ⊢ (?%? → ∀policy.??(?%??)(?%??) → ?%??); 1469 [ #_ #policy #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1470  #h #t #Hind #Hp #policy #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1500 #program #policy lapply (le_n (program)) @(list_ind ? 1501 (λx.x ≤ program → measure_int x (eject … policy) 0 = measure_int x (eject … (jump_expansion_step program policy)) 0 → 1502 policy_equal x (eject … policy) (eject … (jump_expansion_step program policy))) 1503 ?? program) 1504 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1505  #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1471 1506 [ #Hi @Hind 1472 1507 [ @(transitive_le … Hp) // … … 1531 1566 qed. 1532 1567 1533 lemma measure_zero: ∀l.∀program .1568 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1534 1569 l ≤ program → measure_int l (jump_expansion_internal program 0) 0 = 0. 1535 #l #program elim l (* lapply (le_n (program)) elim program in ⊢ (?%? → ?%(?%??)?); *)1570 #l #program elim l 1536 1571 [ // 1537 1572  #h #t #Hind #Hp whd in match (measure_int ???); … … 1547 1582 qed. 1548 1583 1549 definition je_fixpoint: ∀program: list labelled_instruction.1584 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.l < 2^16). 1550 1585 Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p. 1551 1586 #program @(dp … (jump_expansion_internal program (2*program))) … … 1599 1634 qed. 1600 1635 1636 let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n: 1637 BitVectorTrie jump_length 16 ≝ 1638 match n with 1639 [ O ⇒ acc 1640  S n' ⇒ 1641 match lookup_opt … (bitvector_of_nat 16 n') policy with 1642 [ None ⇒ transform_policy n' policy acc 1643  Some x ⇒ let 〈pc,length〉 ≝ x in 1644 transform_policy n' policy (insert … pc length acc) 1645 ] 1646 ]. 1647 1601 1648 (**************************************** START OF POLICY ABSTRACTION ********************) 1602 1649 1603 definition policy_type≝ Word → jump_length. 1604 1605 definition jump_expansion': pseudo_assembly_program → policy_type ≝ 1650 definition policy_type ≝ Word → jump_length. 1651 1652 definition jump_expansion': 1653 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1654 policy_type ≝ 1606 1655 λprogram.λpc. 1607 let policy ≝ jump_expansion_internal (\snd program) (\snd program) in 1608 let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in 1609 j. 1610 1656 let policy ≝ 1657 transform_policy (\snd program) (eject … (je_fixpoint (\snd program))) (Stub ??) in 1658 lookup ? ? pc policy long_jump. 1659 /2 by Stub, dp/ 1660 qed. 1661 1611 1662 definition assembly_1_pseudoinstruction_safe ≝ 1612 1663 λprogram: pseudo_assembly_program.
Note: See TracChangeset
for help on using the changeset viewer.