- Timestamp:
- Jul 6, 2012, 11:30:52 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2154 r2156 775 775 ppc = bitvector_of_nat … (|pre|) ∧ 776 776 |code| ≤ 2^16 ∧ 777 (|code| = 2^16 → |pre| = |instr_list|) ∧ 777 778 (nat_of_bitvector … (sigma ppc) = |code| ∨ 778 779 sigma ppc = zero … ∧ |code| = 2^16) ∧ … … 798 799 [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode 799 800 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok 800 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * #Hfold1 #Hfold4#Hfold3 #Hfold2 whd801 cases (Hfold sigma_pol_ok instr_list_ok) -Hfold * * * #Hfold1 #Hfold4 #Hfold5 #Hfold3 #Hfold2 whd 801 802 <eq_create_label_cost_map whd % 802 803 [2: #ppc #LTppc @Hfold2 >Hfold1 @(eqb_elim (|instr_list|) 2^16) … … 808 809 | #Hfold5 %2 <Hfold1 assumption ]] 809 810 | * #sigma_pol_ok1 #_ #instr_list_ok % 810 [ % % // >sigma_pol_ok1 %]811 [ % % [%] // [#abs change with (0=S ?) in abs; destruct(abs) | >sigma_pol_ok1 % ]] 811 812 #ppc' #ppc_ok' #abs @⊥ cases abs 812 813 [#abs2 cases (not_le_Sn_O ?) [#H @(H abs2) | skip] … … 814 815 | * #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 815 816 #IH cases (IH ? instr_list_ok) [2: % assumption ] -IH 816 * * #IH1 #IH2 * 817 [2: #H @⊥ cases daemon (*CSC: impossible case, using Jaaps's ? *)] 817 * * * #IH1 #IH2 #IH4 * 818 [2: * #_ #H @⊥ lapply (IH4 H) >prf >length_append 819 >(plus_n_O (|prefix|)) in ⊢ (??%? → ?); #X 820 lapply (injective_plus_r … X) >length_append normalize #abs' destruct(abs')] 818 821 #IH3 #IH5 819 822 cut (|prefix| < |instr_list|) … … 835 838 lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta 836 839 cut (pc_delta < 2^16) 837 [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok 838 % [ % [% ] ] 840 [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq 841 cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd)) 842 [ whd in match instruction_size; normalize nodelta 843 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels [ >p2 | skip] % ] 844 #EQpc_delta2 845 % [ % [% [% ] ] ] 839 846 [ >length_append normalize nodelta >IH1 @sym_eq @add_bitvector_of_nat 840 847 | >length_append >length_reverse <IH3 cases daemon (*CSC: maybe, using monotonicity*) 848 | lapply (sigma_pol_ok2 … ppc_ok) * #sigma_pol_ok3 849 <eq_fetch_pseudo_instruction <eq_create_label_cost_map #sigma_pol4 850 >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta >EQpc_delta2 851 #abs >abs in sigma_pol4; * 852 [ #abs' cases (absurd ? abs' (not_le_Sn_n …)) 853 | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1 854 >nat_of_bitvector_bitvector_of_nat_inverse // ] 841 855 | cases (sigma_pol_ok2 … ppc_ok) 842 856 whd in match instruction_size; normalize nodelta >p2 <eq_fetch_pseudo_instruction
Note: See TracChangeset
for help on using the changeset viewer.