- 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 types need tuples
- function <PROTOCOL>.Effect.get_state() to obtain the current state
(can be used in proofs only)
- prove assert in
examplesnd/cv2fstar/cv_impl_run/secret_reach/src/Application.fst

Co-authored-by: Aymeric Fromherz <aymeric.fromherz@inria.fr>