Changeset 1363
 Timestamp:
 Oct 12, 2011, 9:11:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1309 r1363 556 556 let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (bv)) false in 557 557 new_pc. 558 559 definition is_label ≝ 560 λx:labelled_instruction.λl:Identifier. 561 let 〈lbl,instr〉 ≝ x in 562 match lbl with 563 [ Some l' ⇒ l' = l 564  _ ⇒ False 565 ]. 558 566 567 lemma oeo_Some_Stronger: 568 ∀id,id',i,prefix. 569 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 570 (eq_bv ? id' id ∧ does_not_occur id prefix) ∨ 571 (¬eq_bv ? id' id ∧ occurs_exactly_once id prefix). 572 #id #id' #i #prefix elim prefix 573 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? _ ⇒ ?]) → ?) 574 change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????) 575 [ normalize // 576  normalize #H @⊥ @H 577 ] 578  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 579 cases he; normalize nodelta 580 [ #H @ (IH H) 581  #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??) 582 generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id) 583 cases (eq_bv ???) in ⊢ (???% → %) #Heq 584 [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta 585 [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf 586  #H >(does_not_occur_Some) 587 [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??) 588 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta 589 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??) 590 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 591  @(sym_eq … H) 592 ] 593 ] 594  normalize nodelta #H lapply (IH H) IH H; #Hor @orb_elim 595 generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) 596 #Heq2 597 [ normalize nodelta <Heq2 in Hor; #Hor normalize in Hor; 598 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??) 599 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta 600 cases (does_not_occur id tl) in Hor; normalize nodelta // 601  normalize nodelta whd in match (occurs_exactly_once ??) 602 whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id) 603 >Heq normalize nodelta <Heq2 in Hor; normalize // 604 ] 605 ] 606 ] 607 ] 608 qed. 609 610 lemma bla: 611 ∀i,p,l. 612 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false. 613 #i #p #l generalize in match i; elim p 614 [ #i >nth_nil #H @⊥ @H 615  #h #t #IH #i cases i i 616 [ cases h #hi #hp cases hi normalize 617 [ #H @⊥ @H 618  #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l) 619 >(eq_eq_bv … Heq) // 620 ] 621  #i #H whd in match (does_not_occur ??) 622 whd in match (instruction_matches_identifier ??) 623 cases h #hi #hp cases hi normalize 624 [ @(IH i) @H 625  #l' cases (eq_v ??? l' l) 626 [ normalize // 627  normalize @(IH i) @H 628 ] 629 ] 630 ] 631 ] 632 qed. 633 559 634 definition create_label_trie: list labelled_instruction → jump_expansion_policy → 560 635 label_trie ≝ 561 636 λprogram.λpolicy. 562 let 〈final_ n, final_pc, final_labels〉 ≝637 let 〈final_pc, final_labels〉 ≝ 563 638 foldl_strong (option Identifier × pseudo_instruction) 564 (λprefix.Σres.True) 639 (λprefix.Σres. 640 let 〈pc,labels〉 ≝ res in 641 ∀i:ℕ.i < prefix → 642 ∀l.occurs_exactly_once l prefix > 643 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 644 ∃a.lookup_opt … l labels = Some ? 〈i,a〉 645 ) 565 646 program 566 647 (λprefix.λx.λtl.λprf.λacc. 567 let 〈 n,pc,labels〉 ≝ acc in648 let 〈pc,labels〉 ≝ acc in 568 649 let 〈label,instr〉 ≝ x in 569 650 let new_labels ≝ 570 651 match label with 571 652 [ None ⇒ labels 572  Some l ⇒ insert … l 〈 n, pc〉 labels653  Some l ⇒ insert … l 〈prefix, pc〉 labels 573 654 ] in 574 let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, long_jump〉 in655 let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (prefix)) policy 〈pc, long_jump〉 in 575 656 let new_pc ≝ add_instruction_size pc jmp_len instr in 576 〈 S n,new_pc, new_labels〉577 ) 〈 0,zero ?, Stub ? ?〉 in657 〈new_pc, new_labels〉 658 ) 〈zero ?, Stub ? ?〉 in 578 659 final_labels. 579 @I 660 [ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length 661 <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 662 [ #Hi #l cases label 663 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl 664 lapply (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; Ha; #addr #Haddr 665 % [ @addr  @Haddr ] 666  #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) Hocc; #Hocc 667 lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq 668 [ >Heq in Hocc; #Hocc normalize in Hocc; 669 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 670 @⊥ @(absurd … Hocc) 671  >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?) 672 [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; // 673  @Hocc 674  #H elim H #addr #Haddr % [ @addr  <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ] 675 ] 676 ] 677 >(bla i … Hl) normalize nodelta @nmk // 678 ] 679  #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 680 [ <minus_n_n #Hl normalize in Hl; cases label in Hl; 681 [ normalize nodelta #H @⊥ @H 682  #l' normalize nodelta #Heq % [ @pc  <Heq @lookup_opt_insert_hit ] 683 ] 684  @le_n 685 ] 686 ] 687  #i #Hi #l #Hl @⊥ @Hl 688 ] 580 689 qed. 581 690 … … 1025 1134 generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]] 1026 1135 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ % 1027  > length_append<IH0 normalize; IHn1; (*CSC: otherwise it diverges!*) //1136  >append_length <IH0 normalize; IHn1; (*CSC: otherwise it diverges!*) // 1028 1137  >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ % 1029 1138  #id normalize nodelta; labels1; cases label; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.