Mentions légales du service

Skip to content
  • BLANCHET Bruno's avatar
    cv2fstar: preserved invariant · 076808e8
    BLANCHET Bruno authored
    - generate declarations and lemmas so that the user can give an invariant
    satisfied by the oracle functions and prove it. By default, this invariant
    is always true.
    - axiomatize that the adversary can call any oracle functions between
    two consecutive calls to oracle functions in the F* code. The effect
    of the adversary calls is any change that preserves the invariant mentioned
    above. This is implemented by a suitable definition of the CVST abbreviation.
    This point can be deactivated by the setting fstarConcurrent = false:
    with this setting, there are no adversary calls between oracle function calls.
    - setting fstarDebug: by default (fstarDebug = false), the printing functions
    for the state are removed and the events are ghost. When fstarDebug = true,
    we get the situation we had previously (printing functions available, events
    are not ghost because they are needed for printing).
    - declare a separate function for decomposition of tuples, to help F*;
    be more precise on which typ...
    076808e8
To find the state of this project's repository at the time of any of these versions, check out the tags.