Assert failing in strange way

[hmijail]

Dafny 3.3 (commit 88cf232)
macOS 11.6

The assert fails:

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

$ dafny baz.dfy
baz.dfy(17,23): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then

I have tried reducing further the file, but the moment I change anything, it stops failing.

Interestingly, Dafny 3.2 verified this file correctly. BUT, if the commented lines are uncommented, then the same failure appears there.

[hmijail]

I tried moving out the contents of the module, or removing the const (which is unused), but any of those changes would suddenly make the assert pass.

[robin-aws]

I've triangulated the breakage to this Dafny PR, which moved Boogie from 2.9.4 to 2.9.6: #1543. (Side note: git bisect is super handy for this. :)

Unfortunately there are quite a few Boogie changes between 2.9.4 and 2.9.5 so I'll have to continue searching through those in turn tomorrow. @keyboardDrummer do you see any obvious culprits in there?

It may not be practical to revert the offending change at this point, but I'm not sure what code change to suggest until we at least understand what Dafny change caused this.

[robin-aws]

Looks like it was boogie-org/boogie#439

[keyboardDrummer]

@hmijail it looks like you're running into an issue that we're calling 'verification instability', which is mentioned in this ticket. To summarise: some correct Dafny programs are difficult for Dafny to verify, and then may or may not verify depending on seemingly unimportant program changes (I'll call these changes refactorings).

Due to changes we made in Dafny's verification pipeline, upgrading Dafny has a similar effect to the verification of your program as applying refactorings. If you change your program to use a (much) small number then the verification instability disappears:

module foo {
   newtype uint128 = i:int | 0 <= i < 0x100
   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;  // 
    } 
}

@RustanLeino do you know how to make this program verify stably without having to restrict the number 0x1_0000_0000_0000_0000_0000_0000_0000_0000 to x_100 ?

[parno]

FWIW, we often find that use of non-linear arithmetic correlates strongly with proof instability. Hence, for any non-trivial project, we try to run with the /noNLarith flag on, and then rely on lemmas from the standard library. This requires more manual work, but leads to more predictable, stable behavior. For example, in this instance, a call to LemmaMulInequality(0, a1, b1) (see here) seems to do the trick, at least using my local installation.

[robin-aws]

Thanks @parno, awesome suggestion! I hadn't thought this qualified as a "non-trivial" assertion and didn't even think of using /noNLarith. This makes me all the more grateful that we have the standard library now. :)

I'm still interested in understanding why boogie-org/boogie#439 caused this to break, so I'd like to leave this open even if the solution above works for you @hmijail.

[franck44]

@robin-aws @parno @hmijail I discussed this issue with @hmijail (we work together) and indeed we found out that:

1. adding a simple lemma saying x >= 0 && y >= 0 ==> x * y >= 0 solved the problem
2. restricting to smaller number also solved the problem.
   What we were unsure about was that uncommenting the line that declares the types seemed to have an effect on the verification result. And that's what we were surprised of.
   I guess that declaring new types results in slightly different verification conditions and different SMT-solver assertions (or order thereof) which may yield to instability.

It is very good that there is a standard library now. In previous projects we wrote a lot of code with folk theorems about e.g. sequences (for instance [] + e == e + [] == e) and they can be shared.
Now we need a mechanism to import Dafny projects or libraries :-)

[keyboardDrummer]

What we were unsure about was that uncommenting the line that declares the types seemed to have an effect on the verification result. And that's what we were surprised of.

This behavior is indeed surprising, and it's an issue that I've been working to resolve. I didn't create a GitHub issue for this before but I've created one now: #1585

[hmijail]

Is there any way to make the Dafny Language Server use the /noNLarith flag?

[camrein]

Is there any way to make the Dafny Language Server use the /noNLarith flag?

Not yet. I was thinking about providing the option to apply all the Dafny settings that the language server doesn't support yet. Something like an expert setting where users should be aware that they may override settings the language server relies on (most importantly ModelViewFile).

For example, something like this:

dotnet DafnyLanguageServer.dll --dafny:settings="/noLarith"