Dafny 4.0 suggestion: Remove automatic compile-time filtering of subset types

[MikaelMayer]

As a conclusion to #1702
Basically, we can currently write:

type N = x : int | x > 0
type T = x: int | ....

predicate method p(t: T) { t > 0 }
function method f(n: N): Int

method f() {
  var setOfT: set<T> = ...;
  var x := set y: N | y in setOfT && p(y) :: f(y)
}

and

trait T
class N extends T
class M extends T

predicate method p(t: T) { t is N }
function method f(n: N): Int

method f() {
  var setOfT: set<T> = ...;
  var x := set y: N | y in setOfT && p(y) :: f(y)
}

This has the effect of actually implicitly emitting the condition x > 0 as part of the loop that build the set.

However, this kind of "automatic code generation" has some problems:

• It works only if the condition of N is not ghost, which can be hard to determine (i.e. if the condition of N has itself a set with another subset type....), and sometimes it contradicts expectations that we should be able to have a ghost subset type because we actually want the condition of N to be ghost.
• When N and T have predicates in common in such a way it should be possible for the programmer to only test a part of it to verify that a T is a N, they cannot do it in the current implementation. This means potential performance penalty without workaround
• There is a discrepancy between the type of y in the range (where it has to be assumed to be a T) and the term (where it can be assumed to be a N, because the compiler will emit the check). This makes reasoning about the code difficult, because y has two types.

Proposal

In this proposal, we would remove the compiler-generated code, and:

• In compiled code, allow variable types only matching the iterated collection element type or a supertype (like int in the example above), but not having two subset types.
• To return a subset type, one has to cast the value with an explicit as N where N is the subset type, so that we can verify it.

Thus, we would have:

type N = x : int | x > 0
type T = x: int | ....

predicate method p(t: T) { t > 0 }
function method f(n: N): Int

method f() {
  var setOfT: set<T> = ...;
  var x := set y: T | y in setOfT && p(y) :: f(y as N)
}

and

trait T
class N extends T
class M extends T

predicate method p(t: T) { t is N }
function method f(n: N): Int

method f() {
  var setOfT: set<T> = ...;
  var x := set y: T | y in setOfT && p(y) :: f(y as N)
}

which enables T and N to be ghost subset types, because p is compiled and can help to prove that y is a N anyway.

[keyboardDrummer]

Thus, we would have:

type N = x : int | x > 0
type T = x: int | ....

predicate method p(t: T)
function method f(n: N): Int

method f() {
  var setOfT: set<T> = ...;
  var x := set y: T | y in setOfT && p(y) :: f(y as N)
}

Aren't you missing a y >= 0 check in the range there, to allow the cast y as N to pass?

[MikaelMayer]

Aren't you missing a y >= 0 check in the range there, to allow the cast y as N to pass?

Yes, updated

[robin-aws]

I think in general requiring the extra x as T expression is completely reasonable. For the record though:

This makes reasoning about the code difficult, because y has two types.

I would avoid thinking of it this way. I strongly prefer saying that a symbol has a single type. The wrinkle is just that Dafny will sometimes allow you to use the symbol in a context that requires a more specific type. It is a kind of "automatic, statically-verified downcasting" that is only allowed if the required proof obligation is verified.

You are just making the argument that this can sometimes be confusing - I definitely agree with that (case in point: #2551) so I'm in favour of of this. In particular it seems to imply supporting is and as expressions where the RHS is a subset type, which I am also in favour of :)