Changeset 1593 for src/ASM/Assembly.ma
 Timestamp:
 Dec 7, 2011, 3:48:32 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1592 r1593 409 409 qed. 410 410 411 (* definition of & operations on jump length *) 411 412 inductive jump_length: Type[0] ≝ 412 413  short_jump: jump_length … … 414 415  long_jump: jump_length. 415 416 417 definition max_length: jump_length → jump_length → jump_length ≝ 418 λj1.λj2. 419 match j1 with 420 [ long_jump ⇒ long_jump 421  medium_jump ⇒ 422 match j2 with 423 [ long_jump ⇒ long_jump 424  _ ⇒ medium_jump 425 ] 426  short_jump ⇒ j2 427 ]. 428 429 definition jmple: jump_length → jump_length → Prop ≝ 430 λj1.λj2. 431 match j1 with 432 [ short_jump ⇒ 433 match j2 with 434 [ short_jump ⇒ False 435  _ ⇒ True 436 ] 437  medium_jump ⇒ 438 match j2 with 439 [ long_jump ⇒ True 440  _ ⇒ False 441 ] 442  long_jump ⇒ False 443 ]. 444 445 definition jmpleq: jump_length → jump_length → Prop ≝ 446 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 447 448 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y). 449 #x #y cases x cases y /3 by inl, inr, nmk, I/ 450 qed. 451 452 lemma jmpleq_max_length: ∀ol,nl. 453 jmpleq ol (max_length ol nl). 454 #ol #nl cases ol cases nl 455 /2 by or_introl, or_intror, I/ 456 qed. 457 458 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b). 459 #a #b cases a cases b /2/ 460 %2 @nmk #H destruct (H) 461 qed. 462 463 416 464 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *) 417 465 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16. … … 548 596 definition label_map ≝ identifier_map ASMTag (nat × nat). 549 597 598 definition is_label ≝ 599 λx:labelled_instruction.λl:Identifier. 600 let 〈lbl,instr〉 ≝ x in 601 match lbl with 602 [ Some l' ⇒ l' = l 603  _ ⇒ False 604 ]. 605 550 606 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝ 551 607 λpc.λjmp_len.λinstr. … … 557 613 ] in 558 614 pc + (bv). 559 560 definition is_label ≝ 561 λx:labelled_instruction.λl:Identifier. 562 let 〈lbl,instr〉 ≝ x in 563 match lbl with 564 [ Some l' ⇒ l' = l 565  _ ⇒ False 566 ]. 567 615 568 616 lemma label_does_not_occur: 569 617 ∀i,p,l. … … 705 753 ]. 706 754 707 definition max_length: jump_length → jump_length → jump_length ≝708 λj1.λj2.709 match j1 with710 [ long_jump ⇒ long_jump711  medium_jump ⇒712 match j2 with713 [ long_jump ⇒ long_jump714  _ ⇒ medium_jump715 ]716  short_jump ⇒ j2717 ].718 719 definition jmple: jump_length → jump_length → Prop ≝720 λj1.λj2.721 match j1 with722 [ short_jump ⇒723 match j2 with724 [ short_jump ⇒ False725  _ ⇒ True726 ]727  medium_jump ⇒728 match j2 with729 [ long_jump ⇒ True730  _ ⇒ False731 ]732  long_jump ⇒ False733 ].734 735 definition jmpleq: jump_length → jump_length → Prop ≝736 λj1.λj2.jmple j1 j2 ∨ j1 = j2.737 738 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).739 #x #y cases x cases y /3 by inl, inr, nmk, I/740 qed.741 742 lemma jmpleq_max_length: ∀ol,nl.743 jmpleq ol (max_length ol nl).744 #ol #nl cases ol cases nl745 /2 by or_introl, or_intror, I/746 qed.747 748 755 definition is_jump' ≝ 749 756 λx:preinstruction Identifier. … … 771 778 ]. 772 779 780 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x). 781 #x cases x #l #i cases i 782 [#id cases id 783 [1,2,3,6,7,33,34: 784 #x #y %2 whd in match (is_jump ?); /2 by nmk/ 785 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: 786 #x %2 whd in match (is_jump ?); /2 by nmk/ 787 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ 788 9,10,14,15: #x %1 // 789 11,12,13,16,17: #x #y %1 // 790 ] 791 2,3: #x %2 /2 by nmk/ 792 4,5: #x %1 // 793 6: #x #y %2 /2 by nmk/ 794 ] 795 qed. 796 797 773 798 definition jump_in_policy ≝ 774 799 λprefix:list labelled_instruction.λpolicy:jump_expansion_policy. … … 776 801 (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔ 777 802 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉). 778 779 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m. 780 /2/ qed. 781 803 804 (* these should be moved to BitVector at some point *) 782 805 lemma bitvector_of_nat_ok: 783 806 ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y. … … 789 812 790 813 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).814 ∀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 815 #n #x #y #Hx #Hy #Heq @notb_elim 793 816 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y))) … … 797 820 ] 798 821 qed. 799 800 822 801 823 lemma jump_not_in_policy: ∀prefix:list labelled_instruction. … … 1213 1235 qed. 1214 1236 1215 lemma le_plus:1216 ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.1217 #n #m elim m m;1218 [ #Hn % [ @O  <(le_n_O_to_eq n Hn) // ]1219  #m #Hind #Hn cases (le_to_or_lt_eq … Hn) Hn; #Hn1220 [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k)  >Hk // ]1221  % [ @O  <Hn // ]1222 ]1223 ]1224 qed.1225 1226 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.1227 #n (elim n) normalize /2 by S_pred/ qed.1228 1229 1237 lemma pe_step: ∀program:(Σl:list labelled_instruction.l < 2^16). 1230 1238 ∀p1,p2:Σpolicy. … … 1253 1261 ] 1254 1262 qed. 1255 1263 1264 (* this is in the stdlib, but commented out, why? *) 1265 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. 1266 #n (elim n) normalize /2 by S_pred/ qed. 1267 1256 1268 lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.l < 2^16).∀n:ℕ. 1257 1269 policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) → 1258 1270 ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k). 1259 #program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H H Hk k;1271 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H H Hk k; 1260 1272 lapply Heq Heq; lapply n n; elim z z; 1261 1273 [ #n #Heq <plus_n_O @pe_refl … … 1267 1279 qed. 1268 1280 1269 lemma dec_bounded_forall:1270 ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).1271 #P #HP_dec #k elim k k1272 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O1273  #k #Hind cases Hind1274 [ #Hk cases (HP_dec k)1275 [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)1276 [ #H @(Hk … (le_S_S_to_le … H))1277  #H >(injective_S … H) @HPk1278 ]1279  #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k)))  @HPk ]1280 ]1281  #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn'))  @Hk ]1282 ]1283 ]1284 qed.1285 1286 lemma dec_bounded_exists:1287 ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).1288 #P #HP_dec #k elim k k1289 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O1290  #k #Hind cases Hind1291 [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn)  @(proj2 … Hn) ]1292  #Hk cases (HP_dec k)1293 [ #HPk %1 @(ex_intro … k) @conj [ @le_n  @HPk ]1294  #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))1295 [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj1296 [ @(le_S_S_to_le … H)  @(proj2 … Hn) ]  @Hk ]1297  #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn)  @HPk ]1298 ]1299 ]1300 ]1301 ]1302 qed.1303 1304 lemma not_exists_forall:1305 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.1306 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)1307 @conj [ @Hx  @Habs ]1308 qed.1309 1310 lemma not_forall_exists:1311 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.1312 #k #P #Hdec elim k1313 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O1314  k #k #Hind #Hfa cases (Hdec k)1315 [ #HP elim (Hind ?)1316 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ]1317  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)1318 [ #H2 @H @(le_S_S_to_le … H2)1319  #H2 >(injective_S … H2) @HP1320 ]1321 ]1322  #HP @(ex_intro … k) @conj [ @le_n  @HP ]1323 ]1324 ]1325 qed.1326 1327 1281 lemma thingie: 1328 1282 ∀A:Prop.(A + ¬A) → (¬¬A) → A. … … 1333 1287 qed. 1334 1288 1335 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b). 1336 #a #b cases a cases b /2/ 1337 %2 @nmk #H destruct (H) 1338 qed. 1289 include "utilities/extralib.ma". 1339 1290 1340 1291 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.l<2^16). … … 1441 1392 qed. 1442 1393 1394 (* these lemmas seem superfluous, but not sure how *) 1443 1395 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b. 1444 1396 #a elim a … … 1486 1438 qed. 1487 1439 1488 lemma eq_plus_S_to_lt:1489 ∀n,m,p:ℕ.n = m + (S p) → m < n.1490 //1491 qed.1492 1493 (* how to do this with a sigmatype and elimination? *)1494 1440 lemma measure_special: ∀program:(Σl:list labelled_instruction.l < 2^16). 1495 1441 ∀policy:Σp:jump_expansion_policy. … … 1549 1495 qed. 1550 1496 1551 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).1552 #x cases x #l #i cases i1553 [#id cases id1554 [1,2,3,6,7,33,34:1555 #x #y %2 whd in match (is_jump ?); /2 by nmk/1556 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:1557 #x %2 whd in match (is_jump ?); /2 by nmk/1558 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/1559 9,10,14,15: #x %1 //1560 11,12,13,16,17: #x #y %1 //1561 ]1562 2,3: #x %2 /2 by nmk/1563 4,5: #x %1 //1564 6: #x #y %2 /2 by nmk/1565 ]1566 qed.1567 1568 1497 lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.l < 2^16. 1569 1498 l ≤ program → measure_int l (jump_expansion_internal program 0) 0 = 0.
Note: See TracChangeset
for help on using the changeset viewer.