Changeset 3112


Ignore:
Timestamp:
Apr 9, 2013, 6:05:49 PM (4 years ago)
Author:
tranquil
Message:

added invariant that costlabels are only assigned to NOPs (not proved
yet, assembly has a new cases daemon)

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r3104 r3112  
    12341234; oc_injective_costlabels :
    12351235  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 …
    12361239}.
  • src/ASM/ASMCosts.ma

    r3102 r3112  
    5050 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
    5151 try (#x #y #abs) try (#x #abs) try #abs destruct
     52qed.
     53
     54lemma OC_costed_is_nop : ∀loc.
     55let 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
     58whd in ⊢ (??%?);
     59whd in match fetch; normalize nodelta
     60>(oc_costlabels_are_zero loc … EQ) % qed.
     61
     62lemma OC_class_to_uncosted : ∀loc.
     63let S ≝ OC_abstract_status loc in
     64∀st.
     65match as_classify S st with
     66[ cl_other ⇒ True | _ ⇒ ¬as_costed … st ].
     67#loc #st
     68whd 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) %
    5271qed.
    5372
  • src/ASM/Assembly.ma

    r3104 r3112  
    922922        let ppc ≝ lookup_labels (\fst newident_oldident) in
    923923         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))) ??.
    925925  [ cases (foldl_strong ? (λx.Σy.?) ???) in p1; #ignore_revcode #Hfold #EQignore_revcode
    926926    >EQignore_revcode in Hfold; #Hfold #sigma_pol_ok #instr_list_ok
     
    934934      [ #Hfold5 <Hfold5 % >Hfold1 %
    935935      | * #Hfold51 #Hfold52 %2 <Hfold1 assumption ]]
    936   | cases daemon
     936  | cases daemon (* injectivity of cost labels *)
     937  | cases daemon (* cost labels correspond to nops *)
    937938  | * #sigma_pol_ok1 #_ #instr_list_ok %
    938939    [ % % [%] // >sigma_pol_ok1 % ]
Note: See TracChangeset for help on using the changeset viewer.