Changeset 3112
 Timestamp:
 Apr 9, 2013, 6:05:49 PM (8 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r3104 r3112 1234 1234 ; oc_injective_costlabels : 1235 1235 partial_injection … (λpc.lookup_opt … pc costlabels) 1236 ; oc_costlabels_are_zero : (* this will imply that cost labels are only assigned to nops *) 1237 ∀ppc,l.lookup_opt … ppc costlabels = Some ? l → 1238 lookup … ppc cm (zero …) = zero … 1236 1239 }. 
src/ASM/ASMCosts.ma
r3102 r3112 50 50 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize 51 51 try (#x #y #abs) try (#x #abs) try #abs destruct 52 qed. 53 54 lemma OC_costed_is_nop : ∀loc. 55 let S ≝ OC_abstract_status loc in 56 ∀st,l.as_label S st = Some ? l → current_instruction (cm loc) st = NOP ?. 57 #loc #st #l #EQ 58 whd in ⊢ (??%?); 59 whd in match fetch; normalize nodelta 60 >(oc_costlabels_are_zero loc … EQ) % qed. 61 62 lemma OC_class_to_uncosted : ∀loc. 63 let S ≝ OC_abstract_status loc in 64 ∀st. 65 match as_classify S st with 66 [ cl_other ⇒ True  _ ⇒ ¬as_costed … st ]. 67 #loc #st 68 whd in match (as_costed ??); inversion (as_label ??) 69 [ #_ cases (as_classify ??) %* #A @A % ] 70 #l #EQ whd in match (as_classify ??); >(OC_costed_is_nop … EQ) % 52 71 qed. 53 72 
src/ASM/Assembly.ma
r3104 r3112 922 922 let ppc ≝ lookup_labels (\fst newident_oldident) in 923 923 insert … (sigma ppc) (\snd newident_oldident) symboltable) (Stub ??) (renamed_symbols p)) 924 (sigma (lookup_labels (final_label p))) ? .924 (sigma (lookup_labels (final_label p))) ??. 925 925 [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode 926 926 >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok … … 934 934 [ #Hfold5 <Hfold5 % >Hfold1 % 935 935  * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]] 936  cases daemon 936  cases daemon (* injectivity of cost labels *) 937  cases daemon (* cost labels correspond to nops *) 937 938  * #sigma_pol_ok1 #_ #instr_list_ok % 938 939 [ % % [%] // >sigma_pol_ok1 % ]
Note: See TracChangeset
for help on using the changeset viewer.