Constraint-less newtypes assumed to be nonempty

[RustanLeino]

Dafny version

4.6.0

Code to produce this issue

type Empty = x: int | false witness *

newtype NewEmpty = Empty

method OperateOnNewEmpty(x: NewEmpty)
  ensures false
{
  var y: Empty := x as Empty;
}

method Main() {
  var x: NewEmpty := *;
  OperateOnNewEmpty(x); // BOGUS: NewEmpty is assumed to be nonempty, so x is considered definitely assigned here
  print 10 / 0; // boom!
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 2 verified, 0 errors
Unhandled exception. System.DivideByZeroException: Attempted to divide by zero.
   at System.Numerics.BigInteger.op_Division(BigInteger dividend, BigInteger divisor)
   at System.Numerics.BigInteger.Divide(BigInteger dividend, BigInteger divisor)
   at Dafny.Helpers.EuclideanDivision(BigInteger a, BigInteger b)
   at _module.__default._Main(ISequence`1 __noArgsParameter)
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)

What happened?

A constraint-less newtype (that is, a declaration of the form newtype N = T for some previous type T) is only as nonempty as its base type. Yet, Dafny assumes NewEmpty to be nonempty. (This was correct years ago, before Dafny started supporting empty types.)

To fix this issue, the verifier should perform a non-emptiness test on constraint-less newtypes, just as if the type had been declared with a (trivial) constraint:

newtype NewEmpty = x: Empty | true

If this test fails and Dafny reports an error, then it would be nice to let the program declare a witness clause on the constraint-less newtype. However, at this time, only newtype declarations with constraints are (syntactically) allowed a witness clause. I propose that this be changed at the same time as the soundness bug is fixed.

What type of operating system are you experiencing the problem on?

Mac