unsoundness: dafny seems to assume tuple and inductive datatypes are inhabited

[erniecohen]

the following verifies in 3.0.0:

trait C { predicate f() ensures false }
predicate bad() ensures false { var c:(C) :| true; c.f() }

[RustanLeino]

(The problem is not related to tuples or inductive datatypes. The parentheses in (C) do not make it a 1-tuple. There are no 1-tuples in Dafny, so (C) is the same as C.)

This is a problem. Dafny treats all types as nonempty, and it also enforces that property. But not for traits! This is an oversight. The only place where this is a problem is where Dafny is taking responsibility for the existence of a value of type C. I think this happens only in

• local-variable declarations and out-parameter declarations
• assign-such-that statements and let-such-that expressions

Furthermore, if these above cases appear in compiled code, then the situation seems fine, because then Dafny will enforce definite-assignment rules for the uses of those variables (in the first case) and the compiler will say that it doesn't know how to generate code for the such-that constructs (in the second case). However, in ghost contexts, these checks are not used.

Something needs to be done to prevent those cases in ghost code. (I'm not sure what the best solution is.)

For the record, here is another repro:

trait D {
  lemma False()
    ensures false
}

lemma Bad()
  ensures false
{
  var d: D;   // or, the following also exhibits the problem:   var d: D :| true;
  d.False();
}

method Main() {
  Bad();
  var x := 3 / 0;  // the verifier and compiler are happy, the but compiled code crashes when run
}

[RustanLeino]

I've given this some thought. I think the solution is to reverse the dozen-years-old design decision that all types must be nonempty. Types should be distinguished along the following virtues:

• Nonempty type. This means variables in ghost contexts can be used before explicit initialization.
• Auto-init type. This implies the type is nonempty, and means that variables can be auto-initialized by the compiler.

Up until now, "nonempty type" has been used incorrectly for these two purposes, and it's also been confused with a type being inductive (meaning that its values respect Dafny's well-founded ordering -- actually, it would be an erroneous well-founded ordering if some type was not inductive in this sense) and a type having the possibility of causing logical contradictions (because of cycles in type definitions that can cause cardinality discrepancies if strong positivity were not enforced).