Verification behavior changes when making unrelated changes

[keyboardDrummer]

Due to the way the Dafny verification pipeline currently works, the runtime or success of a proof verification may change when changes unrelated to that proof are made to a Dafny program.

An example of this was shown in #1570, where using Dafny 3.2, the program verifies, but no longer verifies when some commented lines are uncommented. This behavior is surprising since the commented lines are unused type definitions so they should not influence the program.

module foo {
   newtype uint128 = i:int | 0 <= i < 0x1_0000_0000_0000_0000_0000_0000_0000_0000
   const MAX_UINT8 : int := 0x100 - 1
  //  type uint = uint128 
}

import opened foo

//datatype Status = Success(uint: uint) | Failure(error: string)

method bar(a: uint128, b: uint128) 
{ 
    var a1: nat := a as nat;
    var b1: nat := b as nat; 
    if (a1 >= 0 && b1 >= 0) {
      assert (a1 * b1) >= 0;  //    <------------------------- FAILS
    } 
}

Implementation

To resolve this issue, the Dafny verification pipeline must, for each proof it sends to the SMT solver, ensure that the sent SMT commands remain exactly the same when changes unrelated to the proof are made to the Dafny program.

Related PRs:

• Use implementation specific counters when generating ids, instead of a global counter boogie-org/boogie#439
• Prune constants boogie-org/boogie#442
• Fix pruning bugs related to trigger boogie-org/boogie#449
• Introduce aggressive pruning and the related 'uses' keyword for constants and functions boogie-org/boogie#450
• Allow keeping SMT commands unchanged when Boogie identifiers are renamed boogie-org/boogie#452
• Enable turning off skolemid boogie-org/boogie#453

[keyboardDrummer]

Resolved by #1612