Changeset 2110 for src/ASM/Assembly.ma
- Timestamp:
- Jun 26, 2012, 4:05:15 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2108 r2110 801 801 (*CSC: move elsewhere *) 802 802 lemma fetch_pseudo_instruction_append: 803 ∀l1,l2. |l1@l2| <2^16 → ∀ppc,ppc_ok,ppc_ok'.803 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'. 804 804 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 805 805 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' = … … 807 807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 808 808 cut (|l1| + nat_of_bitvector … ppc < 2^16) 809 [ @(transitive_l t … l1l2_ok) >length_append /2 by monotonic_lt_plus_r/]809 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ] 810 810 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add 811 811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption … … 833 833 ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))). 834 834 835 (*CSC: Move elsewhere *) 836 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. 837 835 838 definition assembly: 836 839 ∀p: pseudo_assembly_program. … … 840 843 sigma_policy_specification p sigma policy → 841 844 let 〈preamble,instr_list〉 ≝ p in 842 |instr_list| <2^16 →845 |instr_list| ≤ 2^16 → 843 846 let 〈assembled,costs〉 ≝ res in 847 |assembled| ≤ 2^16 ∧ 844 848 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 845 849 let datalabels ≝ construct_datalabels preamble in 846 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in850 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 847 851 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 848 852 ∀ppc. ∀ppc_ok:nat_of_bitvector … ppc < |instr_list|. … … 861 865 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 862 866 let datalabels ≝ construct_datalabels preamble in 863 let lookup_labels ≝ λx. sigma (bitvector_of_nat ? (lookup_def … labels_to_ppc x 0)) in867 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 864 868 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 865 869 let 〈ignore,revcode〉 ≝ pi1 … ( … … 868 872 (λpre. Σppc_code:(Word × (list Byte)). 869 873 sigma_policy_specification 〈preamble,instr_list〉 sigma policy → 870 |instr_list| <2^16 →874 |instr_list| ≤ 2^16 → 871 875 let 〈ppc,code〉 ≝ ppc_code in 872 876 ppc = bitvector_of_nat … (|pre|) ∧ 873 877 nat_of_bitvector … (sigma ppc) = |code| ∧ 874 878 ∀ppc'.∀ppc_ok'. 875 nat_of_bitvector … ppc' < nat_of_bitvector … ppc→879 (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) → 876 880 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' ppc_ok' in 877 881 let 〈len,assembledi〉 ≝ … … 892 896 [ cases (foldl_strong ? (λx.Σy.?) ???) in p2; #ignore_revcode #Hfold #EQignore_revcode 893 897 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 894 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2 895 >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 898 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd % 899 [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16) 900 [ #limit %2 @limit 901 | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 902 @not_eq_to_le_to_lt assumption ] 903 | >length_reverse <Hfold3 904 @(transitive_le … (S (nat_of_bitvector … (sigma ignore)))) 905 [ // | change with (? < ?); @lt_nat_of_bitvector ]] 896 906 | * #sigma_pol_ok1 #_ #instr_list_ok % 897 907 [ % // >sigma_pol_ok1 % ] 898 #ppc' #ppc_ok' #abs @⊥ cases (not_le_Sn_O ?) [#H @(H abs) | skip] 908 #ppc' #ppc_ok' #abs @⊥ cases abs 909 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip] 910 |#abs2 change with (0 = S ?) in abs2; destruct(abs2) ] 899 911 | * #sigma_pol_ok1 #sigma_pol_ok2 #instr_list_ok cases ppc_code in p1; -ppc_code #ppc_code #IH #EQppc_code >EQppc_code in IH; -EQppc_code 900 912 #IH cases (IH ? instr_list_ok) [2: % assumption ] * #IH1 #IH3 #IH2 whd % [% 901 913 [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon 902 914 |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]] 903 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc 904 cases (le_to_or_lt_eq … LTppc_ppc) 905 [2: #S_S_eq normalize nodelta in S_S_eq; 906 (*CSC: TRUE, NEEDS SOME WORK *) 907 cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf 908 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc 909 >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]); 910 >fetch_pseudo_instruction_append 911 [3: @le_S_S @le_O_n 912 |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H 913 |4: <prf <p_refl in instr_list_ok; #H @H ] 914 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 915 #j #LTj >nat_of_bitvector_add 916 >nat_of_bitvector_bitvector_of_nat_inverse 917 [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon 918 |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ] 919 >reverse_append >reverse_reverse >IH3 <(length_reverse … code) 920 @nth_safe_prepend 921 | #LTppc'' 922 cut (nat_of_bitvector … ppc' < |instr_list|) 923 [ normalize nodelta in LTppc''; 924 @(transitive_le … (nat_of_bitvector … ppc)) 925 [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse 926 [ // 927 | <p_refl in instr_list_ok; #instr_list_ok 928 @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ] 929 | @le_S_S_to_le >nat_of_bitvector_add in LTppc''; 930 [ >commutative_plus #H @H 931 | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus 932 @(transitive_le … (S (|instr_list|))) 933 [2: <p_refl in instr_list_ok; #instr_list_ok assumption 934 | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|)) 935 >length_append >nat_of_bitvector_bitvector_of_nat_inverse 936 [2: <p_refl in instr_list_ok; >prf >length_append #H 937 @(transitive_le … H) // 938 | @le_S_S // ]]]]] 915 #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 * 916 cases daemon (* 917 ?????????????? PRIMA NON C'ERA L'OR :-( 918 MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED 919 [2: #eq_S_prefix_bound -IH @(IH2 ? LTppc') 920 @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction' 921 @pair_elim 922 | #LTppc_ppc 923 cases (le_to_or_lt_eq … LTppc_ppc) 924 [2: #S_S_eq normalize nodelta in S_S_eq; 925 (*CSC: TRUE, NEEDS SOME WORK *) 926 cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf 927 >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc 928 >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]); 929 >fetch_pseudo_instruction_append 930 [3: @le_S_S @le_O_n 931 |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H 932 |4: <prf <p_refl in instr_list_ok; #H @H ] 933 #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 934 #j #LTj >nat_of_bitvector_add 935 >nat_of_bitvector_bitvector_of_nat_inverse 936 [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon 937 |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ] 938 >reverse_append >reverse_reverse >IH3 <(length_reverse … code) 939 @nth_safe_prepend 940 | #LTppc'' 941 cut (nat_of_bitvector … ppc' < |instr_list|) 942 [ normalize nodelta in LTppc''; 943 @(transitive_le … (nat_of_bitvector … ppc)) 944 [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse 945 [ // 946 | <p_refl in instr_list_ok; #instr_list_ok 947 @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ] 948 | @le_S_S_to_le >nat_of_bitvector_add in LTppc''; 949 [ >commutative_plus #H @H 950 | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus 951 @(transitive_le … (|instr_list|)) 952 [2: <p_refl in instr_list_ok; #instr_list_ok assumption 953 | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|)) 954 >length_append >nat_of_bitvector_bitvector_of_nat_inverse 955 [2: <p_refl in instr_list_ok; >prf >length_append #H 956 @(transitive_le … H) // 957 | @le_S_S // ]]]]] 939 958 #X lapply (IH2 ppc' X) 940 959 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction … … 952 971 | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse 953 972 [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]] 954 qed.973 *)qed. 955 974 956 975 definition assembly_unlabelled_program:
Note: See TracChangeset
for help on using the changeset viewer.