Changeset 2141 for src/ASM/PolicyFront.ma
 Timestamp:
 Jun 28, 2012, 8:08:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2102 r2141 253 253 ∀dest.is_jump_to instr dest → 254 254 let paddr ≝ lookup_def … labels dest 0 in 255 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump*)256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in255 let addr ≝ bitvector_of_nat ? (if leb paddr (prefix) (* jump to address already known *) 256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉) 257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 258 258 match j with 259 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ … … 265 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 266 266 ]. 267 268 267 269 268 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 324 323 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 325 324 let paddr ≝ lookup_def … labels lbl 0 in 326 let addr ≝ bitvector_of_nat ? (if leb p pc paddr (* forward jump*)327 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added328 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in325 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 326 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 327 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 329 328 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 330 329 if sj_possible … … 339 338 let paddr ≝ lookup_def ? ? labels lbl 0 in 340 339 let addr ≝ bitvector_of_nat ? 341 (if leb ppc paddr (* forward jump *) 342 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) 343 + added 344 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 340 (if leb paddr ppc (* jump to address already known *) 341 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) 342 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 345 343 let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in 346 344 if aj_possible … … 354 352 let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in 355 353 let paddr ≝ lookup_def … labels lbl 0 in 356 let addr ≝ bitvector_of_nat ? (if leb p pc paddr (* forward jump*)357 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added358 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in354 let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) 355 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) 356 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in 359 357 let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in 360 358 if sj_possible … … 395 393 qed. 396 394 397 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.398 #a #b / by refl/399 qed.400 401 lemma nth_last: ∀A,a,l.402 nth (l) A l a = a.403 #A #a #l elim l404 [ / by /405  #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind406 ]407 qed.408 409 395 (* The first step of the jump expansion: everything to short. *) 410 396 definition jump_expansion_start: 411 ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ).397 ∀program:(Σl:list labelled_instruction.S (l) < 2^16 ∧ is_well_labelled_p l). 412 398 ∀labels:label_map. 413 399 Σpolicy:option ppc_pc_map. 414 400 match policy with 415 401 [ None ⇒ True 416  Some p ⇒ And (And (And (And (And (And (And402  Some p ⇒ And (And (And (And (And (And 417 403 (out_of_program_none (pi1 ?? program) p) 418 404 (not_jump_default (pi1 ?? program) p)) 419 (sigma_compact_unsafe program labels p))420 405 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 421 406 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 407 (sigma_compact_unsafe program labels p)) 422 408 (∀i.i ≤ program → ∃pc. 423 409 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 424 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = Some ? 〈\fst p,short_jump〉)) 425 (\fst p < 2^16) 410 (\fst p < 2^16) 426 411 ] ≝ 427 412 λprogram.λlabels. 428 413 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 429 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And414 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And 430 415 (out_of_program_none prefix policy) 431 416 (not_jump_default prefix policy)) 432 (sigma_compact_unsafe prefix labels policy))433 417 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 434 418 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 419 (sigma_compact_unsafe prefix labels policy)) 435 420 (∀i.i ≤ prefix → ∃pc. 436 421 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) 437 (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd policy) =438 Some ? 〈\fst policy,short_jump〉))439 422 program 440 423 (λprefix.λx.λtl.λprf.λp. … … 451 434  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 452 435 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 453  @conj [ @conj [ @conj [ @conj [ @conj [ @conj436  @conj [ @conj [ @conj [ @conj [ @conj 454 437 [ (* out_of_program_none *) 455 438 #i #Hi2 >append_length <commutative_plus @conj … … 457 440 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 458 441 [ >lookup_opt_insert_miss 459 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2)) 442 [ (* USE[pass]: out_of_program_none → *) 443 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2)) 460 444 @le_S_to_le @le_S_to_le @Hi 461 445  @bitvector_of_nat_abs … … 467 451  >lookup_opt_insert_miss 468 452 [ <Hi 469 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (prefix))) ?)) 453 (* USE[pass]: out_of_program_none → *) 454 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?)) 470 455 [ >Hi @Hi2 471 456  @le_S @le_n … … 483 468  #Hi >lookup_opt_insert_miss 484 469 [ #Hl 485 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl)) 470 (* USE[pass]: out_of_program_none ← *) 471 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl)) 486 472 [ #Hi3 @Hi3 487 473  #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi … … 489 475  @bitvector_of_nat_abs 490 476 [ @Hi2 491  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length477  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length 492 478 <plus_n_Sm @le_S_S @le_plus_n_r 493 479  @Hi … … 500 486 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 501 487 [ >lookup_insert_miss 502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi) 488 [ (* USE[pass]: not_jump_default *) 489 lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi) 503 490 >nth_append_first 504 491 [ #H #H2 @H @H2 … … 506 493 ] 507 494  @bitvector_of_nat_abs 508 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm 509 @le_plus_a @le_S @Hi 510  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S 511 @le_plus_n_r 495 [ @(transitive_lt ??? Hi) @le_S_to_le] 496 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 497 <plus_n_Sm @le_S_S @le_plus_n_r 512 498  @lt_to_not_eq @le_S @Hi 513 499 ] 514 500 ] 515 501  >Hi >lookup_insert_miss 516 [ #_ elim (proj2 ?? (proj1 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 502 [ #_ (* USE: everything is short *) 503 elim ((proj2 ?? Hp) (prefix) (le_n (prefix))) #pc #Hl 517 504 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl 518 505  @bitvector_of_nat_abs 519 [ @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r520  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S506 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r 507  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S 521 508 @le_plus_n_r 522 509  @lt_to_not_eq @le_n … … 524 511 ] 525 512 ] 513 ] 514  (* 0 ↦ 0 *) 515 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 516 >lookup_insert_miss 517 [ (* USE[pass]: 0 ↦ 0 *) 518 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 519  @bitvector_of_nat_abs 520 [ / by / 521  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm 522 @le_S_S @le_plus_n_r 523  @lt_to_not_eq / by / 524 ] 525 ] 526 ] 527  (* fst p = pc *) 528 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 529 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 526 530 ] 527 531  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; … … 530 534 [ >lookup_opt_insert_miss 531 535 [ >lookup_opt_insert_miss 532 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi) 536 [ (* USE[pass]: policy_compact_unsafe *) 537 lapply (proj2 ?? (proj1 ?? Hp) i Hi) 533 538 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) 534 539 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); … … 548 553 [2: lapply (le_S_to_le … Hi) Hi #Hi] 549 554 @bitvector_of_nat_abs 550 [1,4: @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <commutative_plus555 [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus 551 556 @le_plus_a @Hi 552 2,5: @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm557 2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm 553 558 @le_S_S @le_plus_n_r 554 559 3,6: @lt_to_not_eq @le_S_S @Hi … … 556 561  >lookup_opt_insert_miss 557 562 [ >Hi >lookup_opt_insert_hit normalize nodelta 558 >(proj2 ?? Hp) normalize nodelta >nth_append_second 559 [ <minus_n_n whd in match (nth ????); @refl 563 (* USE: everything is short, fst p = pc *) 564 elim ((proj2 ?? Hp) (prefix) (le_n ?)) #pc #Hl 565 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl 566 >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second 567 [ <minus_n_n whd in match (nth ????); >EQ @refl 560 568  @le_n 561 569 ] 562 570  @bitvector_of_nat_abs 563 [ @(transitive_lt … (p i2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus571 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus 564 572 @le_plus_a @le_n 565  @(transitive_lt … (p i2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm573  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm 566 574 @le_S_S @le_plus_n_r 567 575  @lt_to_not_eq @le_S_S >Hi @le_n … … 570 578 ] 571 579 ] 572  (* 0 ↦ 0 *) 573 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 574 >lookup_insert_miss 575 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 576  @bitvector_of_nat_abs 577 [ / by / 578  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 579 @le_S_S @le_plus_n_r 580  @lt_to_not_eq / by / 581 ] 582 ] 583 ] 584  (* fst p = pc *) 585 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 586 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 587 ] 588  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; 580  (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; 589 581 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 590 582 cases (le_to_or_lt_eq … Hi) Hi #Hi 591 583 [ >lookup_opt_insert_miss 592 [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) 584 [ (* USE[pass]: everything is short *) 585 @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) 593 586  @bitvector_of_nat_abs 594 [ @(transitive_lt … (p i2 ?? program)) >prf >append_length @le_S_S >commutative_plus595 @le_plus_a @le_S_S_to_le @Hi596  @(transitive_lt … (p i2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S597 @le_S_S @le_ plus_n_r587 [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 588 >commutative_plus @le_plus_a @le_S_S_to_le @Hi 589  @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm 590 @le_S_S @le_S_S @le_plus_n_r 598 591  @lt_to_not_eq @Hi 599 592 ] … … 603 596 ] 604 597 ] 605  (* lookup at the end *) cases p p #p cases p p #pc #sigma #Hp cases x 606 #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit 607 / by refl/ 608 ] 609  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 598  @conj [ @conj [ @conj [ @conj [ @conj 610 599 [ #i cases i 611 600 [ #Hi2 @conj … … 629 618  i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O 630 619 ] 631 ] 620 ] ] ] 621 >lookup_insert_hit @refl 632 622  #i cases i 633 623 [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n 634 624  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 635 625 ] 636 ]637  >lookup_insert_hit @refl638 ]639  >lookup_insert_hit @refl640 626 ] 641 627  #i cases i … … 643 629  i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 644 630 ] 645 ]646  >lookup_opt_insert_hit @refl647 631 ] 648 632 ] … … 676 660 include alias "basics/logic.ma". 677 661 678 lemma blerpque: ∀a,b,i.662 lemma jump_length_equal_max: ∀a,b,i. 679 663 is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → 680 664 (max_length a b) = a. … … 699 683 qed. 700 684 701 lemma etblorp: ∀a,b,i.is_jump i →685 lemma jump_length_le_max: ∀a,b,i.is_jump i → 702 686 instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. 703 687 #a #b #i cases i … … 706 690 1: #pi cases pi 707 691 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 708 [1,2,3,6,7,24,25: #x #y 709 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 710 #H cases H 692 try (#x #y #H) try (#x #H) try (#H) cases H 711 693 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 712 694 #_ cases a cases b 713 [2,3: cases x #ad cases ad 714 [15,34: #b #Hb / by le_n/ 715 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 716 1,4,5,6,7,8,9: / by le_n/ 717 11,12: cases x #ad cases ad 718 [15,34: #b #Hb / by le_n/ 719 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb 695 [1,4,5,6,7,8,9: / by le_n/ 720 696 10,13,14,15,16,17,18: / by le_n/ 721 20,21: cases x #ad cases ad722 [15,34: #b #Hb / by le_n/723 1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb724 697 19,22,23,24,25,26,27: / by le_n/ 725 29,30: cases x #ad cases ad #a1 #a2726 [1,3: cases a2 #ad2 cases ad2727 [1,8,20,27: #b #Hb / by le_n/728 2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb729 2,4: cases a1 #ad1 cases ad1730 [2,4,21,23: #b #Hb / by le_n/731 1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb732 ]733 698 28,31,32,33,34,35,36: / by le_n/ 734 38,39: cases x #ad cases ad735 [1,4,20,23: #b #Hb / by le_n/736 2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb737 699 37,40,41,42,43,44,45: / by le_n/ 738 700 46,47,48,49,50,51,52,53,54: / by le_n/ … … 741 703 73,74,75,76,77,78,79,80,81: / by le_n/ 742 704 ] 705 try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) 706 cases x * #ad 707 try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) 708 #z @(subaddressing_mode_elim … z) #w normalize / by / 743 709 ] 744 710 ] 745 711 qed. 746 712 747 lemma minus_zero_to_le: ∀n,m:ℕ.n  m = 0 → n ≤ m. 748 #n 749 elim n 750 [ #m #_ @le_O_n 751  #n' #Hind #m cases m 752 [ #H n whd in match (minus ??) in H; >H @le_n 753  #m' m #H whd in match (minus ??) in H; @le_S_S @Hind @H 754 ] 755 ] 756 qed. 757 758 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0. 759 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r 760 qed. 761 762 lemma not_true_is_false: 763 ∀b:bool.b ≠ true → b = false. 764 #b cases b 765 [ #H @⊥ @(absurd ?? H) @refl 766  #H @refl 767 ] 768 qed. 769 770 lemma occurs_does_not: ∀tag,A,id,list_instr. 771 does_not_occur tag A id list_instr = true → 772 occurs_exactly_once tag A id list_instr = true → 773 False. 774 #tag #A #id #list_instr elim list_instr 775 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS) 776  #h #t #Hind whd in match (does_not_occur ????); 777 whd in match (occurs_exactly_once ????); 778 cases (instruction_matches_identifier ?? id h) normalize nodelta 779 [ #ABS destruct (ABS) 780  @Hind 781 ] 782 ] 783 qed. 784 785 lemma label_in_program: ∀program:(Σl.S (l) < 2^16).∀labels:(Σlm. 713 lemma label_in_program: ∀program:(Σl.S (l) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm. 786 714 ∀l.occurs_exactly_once ?? l program → 787 715 bitvector_of_nat ? (lookup_def ?? lm l 0) = … … 789 717 occurs_exactly_once ?? x program → 790 718 lookup_def ASMTag ℕ labels x O≤program. 791 #program cases program program #program #Hprogram #labels #x cases labels 792 labels #labels #H lapply (H x) H 793 generalize in match (lookup_def … labels x 0); 794 whd in match address_of_word_labels_code_mem; 795 whd in match index_of; normalize nodelta elim program in Hprogram; 796 [ #Hprogram #n cases not_implemented 797  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv 798 whd in match (occurs_exactly_once ????) in Hocc; 799 whd in match (index_of_internal ????) in Hbv; 800 lapply (refl ? (instruction_matches_identifier … x h)) 801 lapply Hocc; lapply Hbv; Hocc Hbv 802 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); 803 normalize nodelta #Hbv #Hocc #EQ 804 [ >(bitvector_of_nat_ok 16 n 0) 805 [ @le_O_n 806  >(eq_eq_bv … Hbv) @I 807  / by / 808  cases daemon 809 ] 810  cases n in Hbv; 811 [ #_ @le_O_n 812  n #n #Hbv @le_S_S @(Hind … Hocc) 813 [ @(transitive_lt … Hprogram) @le_n 814  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) 815 [ >Hbv >eq_bv_refl @I 816  @(transitive_lt … Hprogram) cases daemon 817  cases daemon 818  #H >(index_of_label_from_internal … Hocc) 819 <plus_O_n >(index_of_label_from_internal … Hocc) in H; 820 #H >(injective_S … H) <plus_O_n @refl 821 ] 822 ] 823 ] 824 ] 825 ] 826 qed. 719 #program cases program program #program #Hprogram #labels #x cases labels 720 labels #labels #H lapply (H x) H 721 generalize in match (lookup_def … labels x 0); 722 whd in match address_of_word_labels_code_mem; 723 whd in match index_of; normalize nodelta elim program in Hprogram; 724 [ #Hprogram #n cases not_implemented 725  #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) Hlm #Hbv 726 whd in match (occurs_exactly_once ????) in Hocc; 727 whd in match (index_of_internal ????) in Hbv; 728 lapply (refl ? (instruction_matches_identifier … x h)) 729 lapply Hocc; lapply Hbv; Hocc Hbv 730 cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); 731 normalize nodelta #Hbv #Hocc #EQ 732 [ >(bitvector_of_nat_ok 16 n 0) 733 [ @le_O_n 734  >(eq_eq_bv … Hbv) @I 735  / by / 736  cases daemon 737 ] 738  cases n in Hbv; 739 [ #_ @le_O_n 740  n #n #Hbv @le_S_S @(Hind … Hocc) 741 [ @conj 742 [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n 743  cases daemon (* axiomatize this *) 744 ] 745  #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) 746 [ >Hbv >eq_bv_refl @I 747  @(transitive_lt … (proj1 ?? Hprogram)) cases daemon 748  cases daemon 749  #H >(index_of_label_from_internal … Hocc) 750 <plus_O_n >(index_of_label_from_internal … Hocc) in H; 751 #H >(injective_S … H) <plus_O_n @refl 752 ] 753 ] 754 ] 755 ] 756 ] 757 qed. 758 759 lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (l)) < 2^16 ∧ is_well_labelled_p l). 760 ∀labels.∀old_sigma.∀sigma. 761 sigma_pc_equal program old_sigma sigma → 762 sigma_safe program labels 0 old_sigma sigma → 763 sigma_compact_unsafe program labels sigma → 764 sigma_compact program labels sigma. 765 #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi 766 lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) 767 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) 768 cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %); 769 [ / by / 770  #x cases x x #x1 #x2 #EQ 771 cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) 772 [ / by / 773  #y cases y y #y1 #y2 normalize nodelta #H #H2 774 cut (instruction_size_jmplen x2 775 (\snd (nth i ? program 〈None ?, Comment []〉)) = 776 instruction_size … (bitvector_of_nat ? i) 777 (\snd (nth i ? program 〈None ?, Comment []〉))) 778 [5: #H3 <H3 @H2 779 4: whd in match (instruction_size_jmplen ??); 780 whd in match (instruction_size …); 781 whd in match (assembly_1_pseudoinstruction …); 782 whd in match (expand_pseudo_instruction …); 783 normalize nodelta whd in match (append …) in H; 784 cases (nth i ? program 〈None ?,Comment []〉) in H; 785 #lbl #instr cases instr 786 [2,3,6: #x [3: #y] normalize nodelta #H @refl 787 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 788 lapply (Hj x (refl ? x)) Hj normalize nodelta 789 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 790 cases x2 normalize nodelta 791 [1,4: whd in match short_jump_cond; normalize nodelta 792 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 793 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 794 normalize nodelta 795 >(Hequal (lookup_def ?? labels x 0) ?) 796 [2,4,6,8: @(label_in_program program labels x) 797 cases daemon (* XXX this has to come from somewhere else *) 798 ] 799 <plus_n_O 800 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 801 #result #flags normalize nodelta 802 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 803 cases (get_index' bool 2 0 flags) normalize nodelta 804 [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 805 1,2,3,4: cases (eq_bv 9 upper ?) 806 [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3) 807 1,3,5,7: #_ normalize nodelta @refl 808 ] 809 ] 810 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 811 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 812 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 813 normalize nodelta 814 (* USE: added = 0 → policy_pc_equal (from fold) *) 815 >(Hequal (lookup_def ?? labels x 0) ?) 816 [2,4,6,8: @(label_in_program program labels x) 817 cases daemon (* XXX this has to come from somewhere else *)] 818 <plus_n_O 819 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 820 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 821 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 822 #result #flags normalize nodelta 823 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 824 cases (get_index' bool 2 0 flags) normalize nodelta 825 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 826 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 827 lapply (refl ? (leb (lookup_def ?? labels x 0) ([]@program))) 828 cases (leb (lookup_def ?? labels x 0) ([]@program)) in ⊢ (???% → %); #Hlab 829 normalize nodelta 830 (* USE: added = 0 → policy_pc_equal (from fold) *) 831 >(Hequal (lookup_def ?? labels x 0) ?) 832 [2,4,6,8: @(label_in_program program labels x) 833 cases daemon (* XXX this has to come from somewhere else *)] 834 <plus_n_O normalize nodelta 835 cases (vsplit bool 5 11 ?) #addr1 #addr2 836 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 837 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 838 #result #flags normalize nodelta 839 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 840 cases (get_index' bool 2 0 flags) normalize nodelta 841 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 842 ] 843 1: #pi cases pi 844 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 845 [1,2,3,6,7,24,25: #x #y 846 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 847 normalize nodelta #H @refl 848 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 849 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 850 #Hj lapply (Hj x (refl ? x)) Hj 851 whd in match expand_relative_jump; normalize nodelta 852 whd in match expand_relative_jump_internal; normalize nodelta 853 whd in match expand_relative_jump_unsafe; normalize nodelta 854 whd in match expand_relative_jump_internal_unsafe; 855 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 856 <(plus_n_Sm i 0) <plus_n_O 857 cases daemon (* XXX this needs subadressing mode magic, see above *) 858 ] 859 ] 860 ] 861 ] 862 ] 863 qed.
Note: See TracChangeset
for help on using the changeset viewer.