Merge branch 'main' into fabian

Guidelines.md

@@ -1,4 +1,8 @@
-Following are guidelines that one should follow unless there is a good technical reason not to.
+The Dafny 386 guidelines.
+
+By default, you should adhere the following guidelines to structure your development. 
+It may happen that not following the guidelines would lead to a better solution: when that is
+the case, you should present your case with the rest of the developers. 
 
 * Languages features to avoid:
     * import opened.
@@ -8,10 +12,13 @@ Following are guidelines that one should follow unless there is a good technical
 
 * Even if a function is not meant to be part of the compiled code, don't use ghost unless necessary.
 * Do not attach postconditions to functions. Instead, prove the postcondition as a separate lemma.
+* Use function preconditions only when the function is genuinely partial and that making total would requires the use of the error monad or a dummy value.
 * Make functions opaque.
 * Name preconditions of lemmas and reveal them only when necessary.
 * Be mindful of resource usage and refine your proof until it is less than 1M.
-* In particular, avoid `{:vcs_split_on_every_assert}` as this can increase the verification time a lot.
+* Do not use internal prover directives such as `{:vcs_split_on_every_assert}` or `{:trigger}`.
+* A method should have a unique postcondition that establishes its equivalence with a functional model.
+* Local variables must be typed explicitly. 
 * Keep proofs short and modular, as for a pencil and paper proof.
 * Prefer structured proofs in natural deduction rathen than sequences of assertions.
 * Unless it is logically or mathematically necessary:
@@ -143,6 +150,7 @@ lemma Foo2()
       </td>
    </tr>
 </table>
+
 * Establish preconditions of assertion in a by clause. For example, consider lemma Foo() requires A ensures B
 <table>
    <tr>