Changeset 1810
 Timestamp:
 Mar 7, 2012, 7:16:55 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r1809 r1810 506 506 j1 = j2. 507 507 508 definition nec_plus_ultra ≝ 509 λprogram:list labelled_instruction.λp:jump_expansion_policy. 510 ¬(∀i.i < program → \snd (bvt_lookup … (bitvector_of_nat 16 i) p 〈0,0,short_jump〉) = long_jump). 511 508 512 (* One step in the search for a jump expansion fixpoint. *) 509 513 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.l < 2^16). … … 517 521 let 〈changed,pc,y〉 ≝ x in 518 522 match y with 519 [ None ⇒ pc > 2^16 523 [ None ⇒ pc > 2^16 ∧ nec_plus_ultra program old_policy 520 524  Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧ 521 525 jump_in_policy program p ∧ … … 562 566 else 563 567 〈final_changed,final_pc,Some jump_expansion_policy final_policy〉. 564 [ normalize nodelta @leb_true_to_le @p2 568 [ normalize nodelta @conj 569 [ @leb_true_to_le @p2 570  @nmk #Hfull (* XXX *) cases daemon 571 ] 565 572  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 566 573 >H2 in H; >p1 normalize nodelta // … … 955 962 956 963 (* This function executes n steps from the starting point. *) 957 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16)958 (n: ℕ) on n:(Σx: ℕ × (option jump_expansion_policy).959 let 〈 pc,y〉 ≝ x in964 (*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16) 965 (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy). 966 let 〈ch,pc,y〉 ≝ x in 960 967 match y with 961 968 [ None ⇒ pc > 2^16 … … 965 972 [ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉 966 973  S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 967 match z return λx. z=x → Σa: ℕ × (option jump_expansion_policy).? with974 match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with 968 975 [ None ⇒ λp2.〈pc,None ?〉 969 976  Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?») 970 977 ] (refl … z) 978 ].*) 979 980 let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (l) 2^16) (n: ℕ) 981 on n:(Σx:bool × ℕ × (option jump_expansion_policy). 982 let 〈c,pc,y〉 ≝ x in 983 match y with 984 [ None ⇒ pc > 2^16 985  Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) 986 ]) ≝ 987 match n with 988 [ O ⇒ 〈true,0,Some ? (pi1 ?? (jump_expansion_start program))〉 989  S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 990 match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with 991 [ None ⇒ λp2.〈false,pc,None ?〉 992  Some op ⇒ λp2.if ch 993 then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?») 994 else (jump_expansion_internal program m) 995 ] (refl … z) 971 996 ]. 972 997 [ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 973  normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m)) 974 <p1 >p2 / by / 975 4: cases (jump_expansion_step program (create_label_map program op) «op,?») 976 #p cases p #q #r cases r normalize nodelta 977 [ / by / 978  #j #H @conj 979 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 980  @(proj2 ?? (proj1 ?? (proj1 ?? H))) 981 ] 982 ] 983  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 / by / 998  lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 999 3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / 1000  normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?») 1001 #p cases p p #p cases p p #p #q #r cases r normalize nodelta 1002 [ #H @(proj1 ?? H) 1003  #j #H @conj 1004 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 1005  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 1006 ] 1007 ] 984 1008 ] 985 1009 qed. 986 1010 987 1011 lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program). 988 1012 #program whd #x whd #n #Hn … … 1060 1084 #x1 cases x1 #p1 #j1 x1; #H1 #Heqj #Hj #k elim k 1061 1085 [ <plus_n_O >Heqj @Hj 1062  #k' k <plus_n_Sm lapply (refl ? (jump_expansion_internal program (n+k'))) 1086  #k' k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k'))); 1087 lapply (refl ? (jump_expansion_internal program (n+k'))) 1063 1088 cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %); 1064 #x2 cases x2 #p2 #j2 x2; normalize nodelta #H #Heqj21089 #x2 cases x2 x2 #x2 cases x2 x2 #c2 #p2 #j2 normalize nodelta #H #Heqj2 1065 1090 cases j2 in H Heqj2; 1066 1091 [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); … … 1154 1179  #h #t #Hind #Hp #acc 1155 1180 lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy)) 1156 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 #p #q pi1; cases q 1181 cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 pi1 #pi1 cases pi1 1182 #p #q #r pi1; cases r 1157 1183 [ // 1158  #x #Hx #Hjeq normalize nodelta lapply (proj2 ?? (proj1 ?? Hx) (t) Hp)1184  #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (t) Hp) 1159 1185 whd in match (measure_int ???); whd in match (measure_int ? x ?); 1160 1186 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,0,short_jump〉) … … 1169 1195 3: @(transitive_le ? (measure_int t x (acc+1))) 1170 1196 ] 1171 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / /]1197 [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] 1172 1198 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1173 1199 ] 1174 1200  #Heq >Heq cases y3 normalize nodelta 1175 [2,3: >measure_plus >measure_plus @le_plus / /]1201 [2,3: >measure_plus >measure_plus @le_plus / by le_n/] 1176 1202 >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn 1177 1203 ] … … 1234 1260 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) 1235 1261 cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %); 1236 #p cases p #pc #pol normalize nodelta cases pol1262 #p cases p p #p cases p p #ch #pc #pol normalize nodelta cases pol 1237 1263 [ // 1238 1264  #p normalize nodelta #Hpol #eqpol lapply (le_n (program)) … … 1245 1271 [ @(transitive_le … Hp) // 1246 1272  whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; 1247 lapply (proj2 ?? (proj1 ?? Hpol) (t) Hp)1273 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (t) Hp) 1248 1274 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in Hm; 1249 1275 #x cases x x #x1 #x2 #x3 … … 1254 1280 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1255 1281 lapply (measure_incr_or_equal program policy t ? 0) 1256 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / /1282 [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1257 1283 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1258 1284 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) … … 1262 1288 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1263 1289 lapply (measure_incr_or_equal program policy t ? 0) 1264 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / /1290 [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 1265 1291 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1266 1292 #H #_ @(injective_plus_r … H) … … 1270 1296  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1271 1297 whd in match (measure_int ? p ?) in Hm; 1272 lapply (proj2 ?? (proj1 ?? Hpol) (t) Hp)1298 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (t) Hp) 1273 1299 cases (bvt_lookup ?? (bitvector_of_nat ? (t)) ? 〈0,0,short_jump〉) in 1274 1300 Hm; … … 1333 1359 policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p. 1334 1360 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*program)))) 1335 (*@(ex_intro … (2*program)) #k #Hk*)1336 1361 cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) 1337 1362 (\snd (pi1 ?? (jump_expansion_internal program k))) 1338 1363 (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*program)) 1339 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k @pe_trans 1364 [ #Hex elim Hex Hex #x #Hx @(ex_intro … x) #k #Hk 1365 @pe_trans 1340 1366 [ @(\snd (pi1 ?? (jump_expansion_internal program x))) 1341 1367  @pe_sym @equal_remains_equal 1342 1368 [ @(proj2 ?? Hx) 1343  @(transitive_le ? (2*program)) 1344 [ @le_S_S_to_le @le_S @(proj1 ?? Hx) 1345  @le_S_S_to_le @le_S @Hk 1346 ] 1369  @le_S_S_to_le @le_S @Hk 1347 1370 ] 1348 1371  @equal_remains_equal … … 1351 1374 ] 1352 1375 ] 1353  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @pe_sym @equal_remains_equal 1376  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @(ex_intro … (2*program)) #k #Hk 1377 @pe_sym @equal_remains_equal 1354 1378 [ lapply (refl ? (jump_expansion_internal program (2*program))) 1355 1379 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → %); 1356 #jep cases jep #pc #x jep cases x normalize nodelta 1357 [ #Hjep #Heqx >Heqx lapply (step_none program (2*pi1 ?? program) ? 1) 1358 [ >Heqx //  <plus_n_Sm <plus_n_O #H >H // ] 1359  #pol_2prog #H2prog #Heq2prog lapply (measure_full (pi1 ?? program) pol_2prog) #Hfull 1360 whd in match (policy_equal ???); lapply Heq2prog Heq2prog; 1361 lapply (refl ? (jump_expansion_internal program (2*program))) 1362 cases (jump_expansion_internal program (2*program)) in ⊢ (???% → % → %); 1363 #z cases z #fpc #pol z cases pol normalize nodelta 1364 [ #Heq2prog #Hjep #Hploq destruct (Hploq) 1365  #p #Heq2prog #Hjep #Hploq whd in match (jump_expansion_internal ??); 1366 >Hjep normalize nodelta 1367 lapply (refl ? (jump_expansion_step program (create_label_map program p) «p,?»)) 1368 [2: cases (jump_expansion_step program (create_label_map program p) «p,?») in ⊢ (???% → %); 1369 #x cases x #Spc #Spol x cases Spol normalize nodelta 1370 [ #Hy #Hgnarf cases daemon (* XXX *) 1371  #y #Hy #Hgnarf #i #Hi lapply (proj2 ?? (proj1 ?? Hy) i Hi) 1372 lapply (Hfull ? i Hi) 1373 [2: lapply (sym_eq ??? (proj1 ?? Hpy)) #Hblp >(Some_eq ??? Hblp) 1374 >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq))) 1375 cases (bvt_lookup ?? (bitvector_of_nat 16 i) pol_2prog 〈0,0,short_jump〉) 1376 #blp cases blp #a #b #c blp #EQ >EQ normalize nodelta 1377 cases (bvt_lookup ?? (bitvector_of_nat 16 i) y 〈0,0,short_jump〉) 1378 #blp cases blp #d #e #f blp normalize nodelta cases f 1379 [1,2: #H elim H #H2 [1,3: @⊥ @H2 2,4: destruct (H2) ] 1380  #_ // 1381 ] 1382  @le_to_le_to_eq 1383 [ @measure_le 1384  cut (∀x.x ≤ (2*pi1 ?? program) → 1385 ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ 1386 x ≤ measure_int program p 0)) 1387 [ #n elim n 1388 [ #_ whd in match (jump_expansion_internal program 0); 1389 @(ex_intro … (jump_expansion_start program)) % [ @refl  1390 >measure_zero @le_n ] 1391  n #n' #Hind #Hn' elim (le_to_or_lt_eq … Hn') 1392 [ #H2n' elim (Hind ?) 1393 [ Hgnarf #pn' lapply (refl ? (jump_expansion_internal program (S n'))) 1394 cases (jump_expansion_internal program (S n')) in ⊢ (???% → %); 1395 #x cases x x #npc #npol cases npol normalize nodelta 1396 [ #Hbla #Hnone #Hsome lapply (step_none program (S n')) 1397 >Hnone normalize nodelta #Ht elim (le_to_eq_plus ?? Hn') 1398 #k #Hk lapply (Ht ? k) [ //  <Hk >Hjep #H destruct (H) ] 1399  #Spol #Hbla #HSpol #H3 @(ex_intro ?? Spol) @conj [ @refl  1400 lapply (measure_incr_or_equal program pn' program) 1401 lapply (pi2 ?? (jump_expansion_internal program n')) 1402 >(proj1 ?? H3) 1403 lapply (refl ? (jump_expansion_internal program n')) 1404 lapply H3 H3 1405 cases (jump_expansion_internal program n') in ⊢ (% → ???% → %); 1406 #x cases x x #npc #npol normalize nodelta #Hbli #H3 #EQ 1407 >(proj1 ?? H3) in Hbli EQ; #Hbli #EQ 1408 whd in match (jump_expansion_internal program (S n')) in HSpol; 1409 >EQ in HSpol; normalize nodelta 1410 ] ] 1411 1412 1413 1414  1415 ] 1416  1417 ] 1418 ] 1419 1420  #gloeirks elim (gloeirks (2*program) (le_n ?)) #q 1421 >Hjep >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq))) 1422 #H >(Some_eq ??? (proj1 ?? H)) @(proj2 ?? H) 1423 ] 1380 #x cases x x #x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol; 1381 [ (* if we're at None in 2*program, we're at None in S 2*program too *) 1382 #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ 1383 normalize nodelta // 1384  #Fp #HFp #EQ whd in match (jump_expansion_internal ??); 1385 >EQ normalize nodelta 1386 lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»)) 1387 [ @HFp 1388  lapply (measure_full program Fp ?) 1389 [ @le_to_le_to_eq 1390 [ @measure_le 1391  (* XXX *) cases daemon 1392 ] 1393  #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %); 1394 #x cases x x #x cases x x #Gch #Gpc #Gpol cases Gpol normalize nodelta 1395 [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull 1396  #Gp #HGp #EQ2 cases Fch 1397 [ normalize nodelta #i #Hi 1398 lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉)) 1399 cases (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉) in ⊢ (???% → %); 1400 #x cases x x #p #a #j normalize nodelta #H 1401 lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H 1402 #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle) 1403 #x cases x x #p #a #j' cases j' normalize nodelta #H elim H H #H 1404 [1,3: @⊥ @H 1405 2,4: destruct (H) 1406 5,6: @refl 1424 1407 ] 1408  normalize nodelta /2 by pe_int_refl/ 1425 1409 ] 1426 1410 ] 1427 ]] 1428 ] 1429 ] 1430  @le_S_to_le @Hk 1431 ] 1432  (* TO BE CHANGED *) 1433 #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 1434 [ %1 // 1435 2,3: #x %2 @nmk whd in match (policy_equal ???); [2: //] 1436 whd in match (eject_policy_opt ???); #H destruct (H) 1437 4: #p1 #p2 whd in match (policy_equal ???); @dec_bounded_forall #m 1411 ] 1412 ] 1413 ] 1414  @le_S_S_to_le @le_S @Hk 1415 ] 1416  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 1417 #x cases x x #x cases x x #nch #npc #npol normalize nodelta #Hnpol 1418 #x cases x x #x cases x x #Sch #Scp #Spol normalize nodelta #HSpol 1419 cases npol in Hnpol; cases Spol in HSpol; 1420 [ #Hnpol #HSpol %1 // 1421 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); // 1422 #H destruct (H) 1423 4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m 1438 1424 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) 1439 1425 #x cases x x #x1 #x2 #x3 … … 1443 1429 ] 1444 1430 ] 1431 qed. 1445 1432 1446 1433 (* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into … … 1462 1449 definition jump_expansion': 1463 1450 ∀program:preamble × (Σl:list labelled_instruction.l < 2^16). 1464 policy_type≝1465 λprogram.λ pc.1451 ∀lookup_labels.policy_type lookup_labels ≝ 1452 λprogram.λlookup_labels.λpc. 1466 1453 let policy ≝ 1467 1454 transform_policy (\snd program) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in 1468 lookup ? ? pc policy long_jump. 1455 (* here we must use jump_length_ok *) 1456 bvt_lookup ? ? pc policy long_jump. 1469 1457 /2 by Stub, mk_Sig/ 1470 1458 qed.
Note: See TracChangeset
for help on using the changeset viewer.