Changeset 1459 for src/ASM/Assembly.ma
 Timestamp:
 Oct 24, 2011, 2:34:02 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1417 r1459 4 4 include "ASM/Fetch.ma". 5 5 include "ASM/Status.ma". 6 include alias "basics/logic.ma". 6 7 7 8 definition assembly_preinstruction ≝ … … 565 566 ]. 566 567 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: 568 lemma label_does_not_occur: 611 569 ∀i,p,l. 612 570 is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false. … … 631 589 ] 632 590 qed. 591 592 (* lemma coerc_sigma: 593 ∀A,P.∀p:A.P p → Σx:A.P x. 594 #A #P #a #p % [ @a  /2/] 595 qed. 596 coercion coerc_sigma:∀A,P.∀p:A.P p → Σx:A.P x 597 ≝ coerc_sigma on p: ? to (Sig ??). *) 633 598 634 599 lemma coerc_pair_sigma: … … 673 638 lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 674 639 % [ @addr  @Haddr ] 675  #l' #Hocc #Hl lapply (o eo_Some_Stronger … Hocc) Hocc; #Hocc640  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) Hocc; #Hocc 676 641 lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq 677 642 [ >Heq in Hocc; #Hocc normalize in Hocc; … … 683 648 ] 684 649 ] 685 >( blai … Hl) normalize nodelta @nmk //650 >(label_does_not_occur i … Hl) normalize nodelta @nmk // 686 651 ] 687 652  #Hi #l #Hocc >(injective_S … Hi) >nth_append_second … … 811 776 ∀i:ℕ.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 812 777 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉. 813 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 let rec jump_expansion_start (program: list labelled_instruction): 783 (Σpolicy.jump_in_policy program policy) ≝ 784 foldl_strong (option Identifier × pseudo_instruction) 785 (λprefix.Σpolicy.jump_in_policy prefix policy) 786 program 787 (λprefix.λx.λtl.λprf.λpolicy. 788 let 〈label,instr〉 ≝ x in 789 match instr with 790 [ Instruction i ⇒ match i with 791 [ JC _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 792  JNC _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 793  JZ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 794  JNZ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 795  JB _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 796  JNB _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 797  JBC _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 798  CJNE _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 799  DJNZ _ _ ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 800  _ ⇒ (eject … policy) 801 ] 802  Call c ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 803  Jmp j ⇒ insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 804  _ ⇒ (eject … policy) 805 ] 806 ) (Stub ? ?). 807 [43: normalize #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] ] 808 whd #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 809 #Hi 810 [2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84: 811 >nth_append_second >(injective_S … Hi) 812 [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: @le_n] 813 <minus_n_n #Hj normalize in Hj; @⊥ @Hj 814 4,6,52,54,56,58,60,62,64,66,68: >nth_append_second >(injective_S … Hi) 815 [2,4,6,8,10,12,14,16,18,20,22: @le_n] 816 <minus_n_n #Hj % [1,3,5,7,9,11,13,15,17,19,21: @O ] % 817 [1,3,5,7,9,11,13,15,17,19,21: @short_jump ] @lookup_opt_insert_hit 818 ] 819 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 820 lapply (sig2 … policy) #Hpolicy elim (Hpolicy i (le_S_S_to_le … Hi) Hj) 821 #p #H elim H #j #Hpj % 822 [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,63,65,67,69,71,73,75,77,79,81,83: @p] % 823 [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,63,65,67,69,71,73,75,77,79,81,83: @j] 824 [2,3,26,27,28,29,30,31,32,33,34: >lookup_opt_insert_miss] 825 [2,4,6,8,10,12,14,16,18,20,22: @bitvector_of_nat_abs @lt_to_not_eq @(le_S_S_to_le … Hi) ] @Hpj 826 qed. 827 828 (* not really recursive *) 814 829 let rec jump_expansion_step (program: list labelled_instruction) 815 830 (old_policy: Σpolicy.jump_in_policy program policy): … … 870 885 [ @Hn 871 886  #z normalize nodelta <Hn @lookup_opt_insert_miss 872 @notb_elim >eq_bv_false [ //  @nmk #H @(absurd (i = (prefix))) 873 [ @(bitvector_of_nat_ok … H) 874  @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 875 ] ] 887 @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 876 888 ] 877 889 4,5: #id cases (lookup ??? old_policy ?) #x #y normalize nodelta <Hn 878 @lookup_opt_insert_miss @notb_elim >eq_bv_false 879 [1,3: // 880 2,4: @nmk #H @(absurd (i = (prefix))) 881 [1,3: @(bitvector_of_nat_ok … H) 882 2,4: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 883 ] ] 890 @lookup_opt_insert_miss @bitvector_of_nat_abs 891 @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 884 892 ] ] ] 885 893  #Hi >nth_append_second >(injective_S … Hi) … … 934 942 whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss 935 943 [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 936  @notb_elim >eq_bv_false [ //  @nmk #H @(absurd (i = (prefix))) 937 [ @(bitvector_of_nat_ok … H) 938  @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 939 ] ] 944  @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 940 945 ] 941 946 ] … … 943 948 normalize nodelta >lookup_insert_miss 944 949 [1,3: @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 945 2,4: @notb_elim >eq_bv_false [1,3: //  2,4: @nmk #H @(absurd (i = (prefix))) 946 [1,3: @(bitvector_of_nat_ok … H) 947 2,4: @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 948 ] ] 950 2,4: @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) 949 951 ] 950 952 ] … … 981 983 qed. 982 984 983 definition jump_expansion_internal: list labelled_instruction → jump_expansion_policy ≝ 984 λprogram. 985 Stub ? ?. 986 985 let rec jump_expansion_internal (program: list labelled_instruction) 986 (n: ℕ) on n: (Σpolicy:jump_expansion_policy.jump_in_policy program policy) ≝ 987 match n with 988 [ O ⇒ jump_expansion_start program 989  S m ⇒ jump_expansion_step program (jump_expansion_internal program m) 990 ]. 991 [ @(sig2 … (jump_expansion_start program)) 992  @(proj1 … (sig2 … (jump_expansion_step program (jump_expansion_internal program m)))) 993 ] 994 qed. 995 987 996 (**************************************** START OF POLICY ABSTRACTION ********************) 988 997
Note: See TracChangeset
for help on using the changeset viewer.