Changeset 2193 for src/ASM/Assembly.ma
- Timestamp:
- Jul 17, 2012, 2:12:05 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2192 r2193 896 896 ppc = bitvector_of_nat … (|pre|) ∧ 897 897 |code| ≤ 2^16 ∧ 898 True(*(ppc = zero … → code = [])*) ∧899 898 (nat_of_bitvector … (sigma ppc) = |code| ∨ 900 899 sigma ppc = zero … ∧ |code| = 2^16 ∧ … … 924 923 [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode 925 924 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 926 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #_#Hfold5 #Hfold3 whd925 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 whd 927 926 <eq_create_label_cost_map whd % 928 927 [2: #ppc #LTppc @Hfold3 >Hfold1 @(eqb_elim (|instr_list|) 2^16) … … 940 939 | * #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 941 940 #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH 942 * * * #IH1 #IH2 #IH2'#IH3 #IH4941 * * #IH1 #IH2 #IH3 #IH4 943 942 cut (|prefix| < |instr_list|) 944 943 [ >prf >length_append normalize <plus_n_Sm @le_S_S // ] #LT_prefix_instr_list … … 969 968 <eq_fetch_pseudo_instruction <eq_create_label_cost_map <EQpc_delta2 970 969 #sigma_pol3 #sigma_pol4 971 % [ % [% [% ]] ]970 % [ % [% ] ] 972 971 [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat 973 972 | >length_append >length_reverse <EQpc_delta … … 977 976 | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction 978 977 >IH3c try % assumption ] 979 | % (*CSC: Stupid proof of True, drop fake invariant *)980 978 | >length_append >length_reverse 981 979 cases IH3 -IH3
Note: See TracChangeset
for help on using the changeset viewer.