-
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.