Enable Boogie variables to be monotonic

[keyboardDrummer]

Changes

Add the following field to Variable:

    /// <summary>
    /// Prevents this variable from being havoc'd. Useful in situation where havoc commands are generated,
    /// such as after WhileCmds
    ///
    /// One use-case is the definite assignment tracking variables in Dafny, that only go from false to true,
    /// And can return an error if they're still false at the wrong point.
    /// </summary>
    public bool Monotonic { get; set;  }

Testing

Added a CLI test

[shazqadeer]

I didn't quite understand this feature. Could you provide more background on the Dafny feature motivating this change? Perhaps provide a concrete Dafny example.

[keyboardDrummer]

I didn't quite understand this feature. Could you provide more background on the Dafny feature motivating this change? Perhaps provide a concrete Dafny example.

Dafny has assignment tracking variables. Whenever a variable is assigned, it's associated tracking variable is set to true. Whenever a variable is used, we assert that its tracking variable is true. When a loop modifies a variable, then its associated tracking variable is set to true inside the loop, making Boogie consider this tracking variable one of the loop targets, and havoc'ing it after the loop. If the tracking variable was already set to true before the loop, this information is lost.

To counteract that information loss, Dafny will, before the loop, assign the values of tracking variables (all of them, since it does not know what the loop targets are) to temporary storage variables, and after the loop assume tempStorage_i ==> trackingVariable_i. This trick works but introduces unnecessary SMT, and requires unnecessary bookkeeping on the Dafny side. Code is here: https://github.com/dafny-lang/dafny/blob/0597aba89a5ca027fcb148bbbaa7048d863f60ca/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs#L1391

With the change in this PR, Dafny can mark all tracking variables as monotonic, so that they won't be havoc'ed by loops, and then it doesn't need the above mechanism. However, I can't think of any other use-cases than what Dafny does. It only works because Dafny only ever asserts that tracking variables are true, so the effect of the solver knowing a tracking variable is false, versus it not knowing the value, is the same: both give an assertion error.

[keyboardDrummer]

Closing since I felt this was too much of a hack