Changeset 1501 for src/ASM


Ignore:
Timestamp:
Nov 8, 2011, 1:41:01 PM (8 years ago)
Author:
sacerdot
Message:

We must take in account the labelled_p predicate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1500 r1501  
    1313   final:
    1414    ∀hd.
    15      fetch hd ≠ Ret …
     15     fetch hd ≠ Ret … ≠ JmpA
    1616     fetch (execute 1 hd) = Cost … →
    1717      trace_lab_lab0 false
     
    1919    ∀hd.
    2020     fetch hd = Ret … → trace_lab_lab0 true
     21 | final_jmp:
     22    ∀hd.
     23     fetch hd = JmpA … →
     24      fetch (execute 1 hd) = Cost … →
     25       trace_lab_lab0 false
    2126 | call:
    2227    ∀b.∀bf.∀trace:trace_lab_ret.∀af,tl.
     
    3237     fetch hd ≠ Call … →
    3338     fetch (execute 1 hd) ≠ Cost … →
    34      fetch hd ≠ Ret …
     39     fetch hd ≠ Ret … ≠ JmpA
    3540      simple_path_0
    3641
     
    3843 mk_trace_lab_lab: ∀b.∀p:trace_lab_lab0 b → is_labelled (hd p) → trace_lab_lab b.
    3944
    40 definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s): trace_lab_ret ≝ ….
     45definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
    4146
    4247lemma simple_path_ok:
Note: See TracChangeset for help on using the changeset viewer.