- Timestamp:
- Jul 16, 2012, 11:28:11 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2161 r2188 709 709 (nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction < 2^16 710 710 ∨ 711 S (nat_of_bitvector … ppc) = |instr_list| ∧ 711 (∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc < nat_of_bitvector … ppc' → 712 let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in 713 instruction_size lookup_labels sigma policy ppc' instruction' = 0) 714 ∧ 712 715 nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16). 713 716 … … 893 896 ppc = bitvector_of_nat … (|pre|) ∧ 894 897 |code| ≤ 2^16 ∧ 895 (|code| = 2^16 → |pre| = |instr_list|) ∧898 True(*(ppc = zero … → code = [])*) ∧ 896 899 (nat_of_bitvector … (sigma ppc) = |code| ∨ 897 sigma ppc = zero … ∧ |code| = 2^16) ∧ 900 sigma ppc = zero … ∧ |code| = 2^16 ∧ 901 (|pre| < 2^16 → ∀ppc'. ∀ppc_ok':nat_of_bitvector … ppc' < |instr_list|. nat_of_bitvector … ppc ≤ nat_of_bitvector … ppc' → 902 let instruction' ≝ \fst (fetch_pseudo_instruction instr_list ppc' ppc_ok') in 903 instruction_size lookup_labels sigma policy ppc' instruction' = 0) 904 ) ∧ 898 905 ∀ppc'.∀ppc_ok'. 899 906 (nat_of_bitvector … ppc' < nat_of_bitvector … ppc ∨ |pre| = 2^16) → … … 917 924 [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode 918 925 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 919 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 # Hfold5 #Hfold3 #Hfold2whd926 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #_ #Hfold5 #Hfold3 whd 920 927 <eq_create_label_cost_map whd % 921 [2: #ppc #LTppc @Hfold 2>Hfold1 @(eqb_elim (|instr_list|) 2^16)928 [2: #ppc #LTppc @Hfold3 >Hfold1 @(eqb_elim (|instr_list|) 2^16) 922 929 [ #limit %2 @limit 923 930 | #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 924 931 @not_eq_to_le_to_lt assumption ] 925 | >length_reverse % try assumption cases Hfold 3 -Hfold3926 [ #Hfold 3 <Hfold3% >Hfold1 %927 | #Hfold5%2 <Hfold1 assumption ]]932 | >length_reverse % try assumption cases Hfold5 -Hfold5 933 [ #Hfold5 <Hfold5 % >Hfold1 % 934 | * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]] 928 935 | * #sigma_pol_ok1 #_ #instr_list_ok % 929 [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]]936 [ % % [%] // >sigma_pol_ok1 % ] 930 937 #ppc' #ppc_ok' #abs @⊥ cases abs 931 938 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip] … … 933 940 | * #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 934 941 #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH 935 * * * #IH1 #IH2 #IH4 * 936 [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append 937 >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X 938 lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')] 939 #IH3 #IH5 942 * * * #IH1 #IH2 #IH2' #IH3 #IH4 940 943 cut (|prefix| < |instr_list|) 941 944 [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list … … 963 966 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ] 964 967 #EQpc_delta2 965 cases (sigma_pol_ok2 … ppc_ok) -sigma_pol_ok2968 cases (sigma_pol_ok2 … ppc_ok) 966 969 <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2 967 970 #sigma_pol3 #sigma_pol4 968 971 % [ % [% [% ] ] ] 969 972 [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat 970 | >length_append >length_reverse <IH3 <EQpc_delta >commutative_plus 971 cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ] 972 | >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta 973 | >length_append >length_reverse <EQpc_delta 974 cases IH3 -IH3 975 [ #IH3 <IH3 >commutative_plus 976 cases sigma_pol4 [ #LT @(transitive_le … LT) // | * #_ #EQ >EQ % ] 977 | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction 978 >IH3c try % assumption ] 979 (* cut (ppc ≠ zero …) 980 [% #EQppc_zero @(absurd … IH3b) >IH2' [ @not_eq_O_S ] assumption ] #Not_eq_ppc_zero 981 cut (bitvector_of_nat ? (S (pred (nat_of_bitvector … ppc))) = ppc) 982 [ inversion (nat_of_bitvector … ppc) 983 [2: #p #_ #H normalize in match (pred ?); 984 lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector 985 #H' <H' % 986 | #H @⊥ 987 lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector 988 #H' @(absurd ?? Not_eq_ppc_zero) >H' % ]] #EQppc lapply ppc_ok; <EQppc #S_pred_ppc_ok 989 cases (sigma_pol_ok2 (bitvector_of_nat 16 (pred (nat_of_bitvector 16 ppc))) ?) 990 [2: @(transitive_lt … ppc_ok) >nat_of_bitvector_bitvector_of_nat_inverse 991 [2: cases daemon (*CSC: True *) | cases daemon (*CSC: True*) ] 992 | #Sigma_pol1 * 993 [ cases daemon (*??????????*) 994 | * #Sigma_pol2 #Sigma_pol3 lapply (Sigma_pol2 … S_pred_ppc_ok ?) 995 [ cases daemon (*CSC: True *) ] 996 whd in ⊢ (% → ?); <eq_create_label_cost_map #H >H % ]]]*) 997 | %(* >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta 973 998 #abs >abs in sigma_pol4; * 974 999 [ #abs' cases (absurd ? abs' (not_le_Sn_n …)) 975 1000 | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1 976 >nat_of_bitvector_bitvector_of_nat_inverse // ] 977 | >length_append >length_reverse <IH3 <EQpc_delta cases sigma_pol4 978 [ #LT %1 >sigma_pol3 >nat_of_bitvector_add 979 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption] 980 >nat_of_bitvector_bitvector_of_nat_inverse try assumption // 981 | * #EQ1 #EQ2 %2 % 982 [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus 983 >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero 984 | >commutative_plus assumption ]] 1001 >nat_of_bitvector_bitvector_of_nat_inverse // ]*) 1002 | >length_append >length_reverse 1003 cases IH3 -IH3 1004 [ #IH3 <IH3 <EQpc_delta cases sigma_pol4 1005 [ #LT %1 >sigma_pol3 >nat_of_bitvector_add 1006 [2: >nat_of_bitvector_bitvector_of_nat_inverse assumption] 1007 >nat_of_bitvector_bitvector_of_nat_inverse try assumption // 1008 | * #EQ1 #EQ2 %2 % 1009 [ lapply (eq_f … (bitvector_of_nat 16) … EQ2) <add_bitvector_of_nat_plus 1010 >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X % // 1011 | #LLT_prefix 1012 cut (S (nat_of_bitvector … ppc) < 2^16) 1013 [ >length_append in LLT_prefix; <plus_n_Sm <plus_n_O #LLT_prefix 1014 >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ] 1015 -LLT_prefix #LLT_prefix 1016 #ppc' #ppc_ok' #LEQ_newppc_ppc' whd >EQ1 try % 1017 @(lt_to_le_to_lt … LEQ_newppc_ppc') normalize nodelta 1018 >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]] 1019 | * * #IH5 #IH6 #IH7 %2 % [% ] 1020 [ normalize nodelta >sigma_pol3 >IH5 1021 >add_commutative <add_zero >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1022 >EQpc_delta2 >eq_fetch_pseudo_instruction >IH7 try % assumption 1023 | >IH6 <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction >IH7 try % 1024 assumption 1025 | #LLT_prefix 1026 cut (S (nat_of_bitvector … ppc) < 2^16) 1027 [ >length_append in LLT_prefix; <plus_n_Sm <plus_n_O #LLT_prefix 1028 >IH1 >nat_of_bitvector_bitvector_of_nat_inverse assumption ] 1029 -LLT_prefix #LLT_prefix 1030 #ppc' #ppc_ok' #LEQ_newppc_ppc' whd @IH7 try assumption 1031 @(transitive_le … LEQ_newppc_ppc') normalize nodelta 1032 >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]] 985 1033 | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2 986 1034 #EQpc_delta2 #eq_fetch_pseudo_instruction * 987 [2: #eq_S_prefix_bound (*@(IH5 ? LTppc') 1035 [2: #eq_S_prefix_bound 1036 cut (instr_list = prefix @ [〈label,pi〉 ]) [ cases daemon (*CSC: easy *) ] #EQinstr_list 988 1037 @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction' 989 @pair_elim*) cases daemon 1038 @pair_elim #len #assembledi #eq_assembly_1_pseudoinstruction % 1039 [ 1040 | 1041 ] 990 1042 | #LTppc_ppc 991 1043 cases (le_to_or_lt_eq … LTppc_ppc) … … 1005 1057 [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 % 1006 1058 |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ] 1007 >reverse_append >reverse_reverse >IH3 <(length_reverse … code) 1008 @nth_safe_prepend 1059 >reverse_append >reverse_reverse 1060 cases IH3 -IH3 1061 [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend 1062 | cases daemon (*CSC: ?????????? *) ] 1009 1063 | #LTppc'' 1010 1064 cut (nat_of_bitvector … ppc' < |instr_list|) … … 1025 1079 @(transitive_le … H) // 1026 1080 | @le_S_S //*) ]]]] 1027 #X lapply (IH 5ppc' X)1081 #X lapply (IH4 ppc' X) 1028 1082 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1029 1083 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH … … 1035 1089 | #j #LTj >reverse_append >reverse_reverse #K 1036 1090 >IH 1037 [2: >length_reverse <IH3 (*CSC: USE MONOTONICITY*) cases daemon1091 [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon 1038 1092 | @shift_nth_prefix ]]]]] 1039 1093 (* |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add … … 1045 1099 [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]] 1046 1100 *) 1101 cases daemon 1047 1102 qed. 1048 1103
Note: See TracChangeset
for help on using the changeset viewer.