feat: Subset types fully accepted in comprehensions

[MikaelMayer]

To best review this PR, follow the links that cover most relevant parts.

To best understand the impact of this PR, in this test file, all the comprehensions where the bound variable is a GhostEvenCell would not even resolve before. Now they resolve and verify. For example:

datatype Cell = Cell(x: int)
predicate isEven(x: int) {  x % 2 == 0 }
type GhostEvenCell = c: Cell | isEven(c.x) witness Cell(0)

predicate method isSetOfGhostEvenCells(s: set<GhostEvenCell>) {
  forall c :: c in s ==> returnsOneIfGhostEvenCell(c) == 1
  //     ^ GhostEvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in forall expression.
}
method Main() {
  var x: set<Cell> := getOriginalSet();
  var b := true;
 b := b && isSetOfGhostEvenCells(set c: GhostEvenCell | c in x && c.x % 2 == 0);
  //                                 ^ GhostEvenCell is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension.
...

are no longer errors.

---

This PR completely lifts the restriction that map comprehensions, set comprehensions and quantifier expressions iterate only on runtime-testable types.

• Most of tests from git-issue-1604.dfy would fail to verify and/or to compile correctly before
• The tests from git-issue-1604b.dfy are now all correctly failing in the verifier instead of the resolver.
• The tests from git-issue-1604d.dfy test successfully how nested runtime-testable subset types can emit nested conditions in the compiler
• The tests from git-issue-1604e.dfy verify that only nested run-time compilable subset types are accepted by the compiler, and no combination containing any non-runtime testable types. Note that the error messages are very explicit about the path leading to the error.
• See how the error messages evolved nicely for git-issue-697c.dfy

Recent updates

• In the case of failing assertions on comprehensions, smoothly indicate to users if they use variables whose type in the range has been inferred to be the compiled type instead of another type.
• For parameters with a run-time testable type, it will keep the constraint that the argument should be assignable to it. For parameters with non-run-time testable types, it will always assume the run-time testable type for the argument, and let the verifier do the rest. It makes this PR backwards compatible.

High-level summary of changes

Resolver and verifier

For any comprehension (map, set, quantifiers) over a bound variable:

• Nothing in the resolver changed if the expression is in a specification context, or in a ghost statement, or if the bound variable type is statically known to be run-time testable, or if ghost inference established that an expression is ghost (new).
• Else, if the type is not necessarily run-time testable, the bound variable obtains a secondary type (defined here in the AST (the enclosing method ScopePushBoundVarsAssumingNonGhost is used both for comprehensions and quantifiers, so I added the interface IBoundVarBearingExpressionWithToken to access bound variables and the token seamlessly)), which is either the lowest parent of the type known to be run-time testable, or a proxy type with the constraint that it has to be run-time testable.
  • New: The range is cloned (for quantifiers, but also for set and map comprehensions) and typed against the two possible types (for quantifiers, but also for set and map comprehensions)
  • The rationale is that we cannot assume a type stronger than the collection type for the bound variable of a comprehension., which was the source of a soundness issue that this PR solves.
    After resolution, the bound variable's main type stays to be the type in the range and it stores the secondary type it had in the term. This is because compilation will use this type.

Example for the resolver and verifier and notes for the IDE

In the example below, in 1 c is just an annotation for the inference type engine, in 2 and 3 c is of type A (assuming type GA = a : A | ghostconstraint(a)) for e.Range but it's GA for e.RangeIsGhost, and in 4 c is of type GA in any case. Moreover, after resolution, the type of the bound variable c will be A and its secondaryType will be GA, but that's only as a convention as this type is not used further since the identifiers have their own types:

forall c: GA | c in setOfA && predicate1(c) :: predicate2(c)`
`      1       2                         3                4

• (New) When translating to Boogie, we keep a map of variables that have double types, so that in the case an call precondition might not hold, we can at least warn the user if the expression contains a variable which has been inferred differently
• Note that, in the verifier, we will always assume that the variable at least satisfies any subset constraint of the collection type
• Note that, for the IDE, we display the secondary types because a scope defines only one type per variable. However, error messages are clear enough about what is being assumed for the verifier (see for example this error report for this line, appreciate the use of nested tokens for this!)

Story specification

The changes above precisly support the following plan for run-time type checks in comprehensions (as suggested by @RustanLeino). I write down this plan below because it can give some insights about the need for this PR.

• Consider a comprehension like set c: CompiledEvenCell | …, where the resolver has figured out that type CompiledEvenCell is run-time checkable. In this case, the verifier proceeds as it has in the past, namely to just assume c to be a value of type CompiledEvenCell. The compiler will emit code that tests each candidate c value to be a CompiledEvenCell before it evaluates the body of the comprehension. (By “candidate values”, I mean the values that the comprehension expression’s BoundedPool will produce. For example, if the BoundedPool discovers bounds 0 <= c < 100, then the candidate values are the first 100 numbers, and if the BoundedPool discovers c in S, then the candidate values are the values in the set S.)
• Consider a comprehension like set c: GhostEvenCell | …, where the GhostEvenCell may not be run-time checkable. In this case, it may be impossible to emit compiled code. However, there are two cases where we can and will allow it:
  • If the static type of the candidate values is already a subtype of GhostEvenCell, then everything is fine. For example, if the BoundedPool discovers c in S where S has type set<GhostEvenCell>, then everything is fine. Then, the compiler emits code that evaluates the body of the comprehension for every candidate value.
  • NEW If the static type of the candidate values is a type T that is not a subtype of GhostEvenCell, then the verifier will check if, by chance, the body of the comprehension is written in such a way that (a) it is well-formed for every T value (as if bound variable c could have been declared to have type T) and (b) every T value that satisfies the body is in fact a GhostEvenCell. If the verifier is able to check this, then the comprehension is allowed and the compiler can use T as the static type of the bound variable used in the emitted code

Breaking changes:

ghost const zero := 0
type GhostNat = x : int | x >= zero
const S: set<int> := {-1, 0, 1};
type GhostNatInS = x : int | x in (set j: GhostNat | j in S)

Previously, it would just accept it because it would parse the constraint of the type as ghost.
Now, it will complain that it cannot determine that j is GhostNat. The workaround is to wrap the set in a ghost predicate, so that it will never believe GhostNatInS should be compilable.

ghost const zero := 0
type GhostNat = x : int | x >= zero
const S: set<int> := {-1, 0, 1};
type GhostNatInS = x : int | GhostNatInS?(x)

predicate GhostNatInS?(x: int) {
  x in (set j: GhostNat | j in S)
}

[RustanLeino]

With this PR, I get some results I don't expect. Please see the comments in the following test program. Can you please comment on this?

datatype Fruit = Apple(x: int) | Peach(y: bool)

predicate method CIsSpecial(f: Fruit) {
  match f
  case Apple(x) => x % 2 == 0
  case Peach(y) => y
}

predicate GIsSpecial(f: Fruit) {
  CIsSpecial(f)
}

type SpecialFruit = f: Fruit | GIsSpecial(f) witness Apple(0)

function method G(f: Fruit): int
  requires GIsSpecial(f)
{
  match f
  case Apple(x) => 10 / (x - 3)
  case Peach(y) => if y then 5 else G(f)
}

method Main() {
  var a := {Apple(2), Apple(3), Peach(false), Apple(4), Peach(true)};

  ghost var b := set f: SpecialFruit | f in a && G(f) < 10; // since the RHS expression occurs in a ghost context, I would not have expected an error

  ghost var yes := true;
  if yes {
    // this is a ghost context
    var c := set f: SpecialFruit | f in a && G(f) < 10; // since this is in a ghost context, I would not have expected an error
  }

  // The next line complains about cannot-be-compiled (nice), but also gives a (to the user seemingly unrelated) precondition violation.
  Print(set f: SpecialFruit | f in a && G(f) < 10);

  // The next line gives error (good), but I'm wishing for an error message that says something about compilation. How come this
  // line doesn't also give the cannot-be-compiled error that the previous line gives?
  Print(set f: SpecialFruit | G(f) < 10 && f in a && CIsSpecial(f));

  Print(set f: SpecialFruit | f in a && CIsSpecial(f) && G(f) < 10); // verifies, compiles, and runs (good!)

  Print(set f: SpecialFruit | CIsSpecial(f) && G(f) < 10 && f in a); // verifies, compiles, and runs (good!)
}

method Print(s: set<Fruit>) {
  print s, "\n";
}

[RustanLeino]

I also have a question about the (intentional) breaking change in the type inference. Please see the following example.

predicate EvenNat(n: nat) { n % 2 == 0 }
predicate TrueInt(x: int) { true }

method NatTypeInferenceType() {
  // These behave as they had before
  assert forall n: nat :: EvenNat(n) ==> TrueInt(n); // correct, since n is nat
  assert forall x: int :: EvenNat(x) ==> TrueInt(x); // precondition violation, since EvenNat expects a nat and x is int
  assert forall x: int :: 0 <= x && EvenNat(x) ==> TrueInt(x); // good
  assert forall x: int :: EvenNat(x) && 0 <= x ==> TrueInt(x); // precondition violation (good)
  assert forall n :: EvenNat(n) ==> TrueInt(n); // since n is inferred to be an int, an precondition violation is reported

  // In the following, n used to be inferred as nat (in which case no verification errors were generated), but now
  // n is inferred as int. Does this breaking change make a difference for many programs?
  assert forall n :: EvenNat(n) ==> n == n; // since n is inferred to be an int, an precondition violation is reported
  assert forall n :: EvenNat(n) ==> true; // since n is inferred to be an int, an precondition violation is reported
}

[MikaelMayer]

ghost var b := set f: SpecialFruit | f in a && G(f) < 10; // since the RHS expression occurs in a ghost context, I would not have expected an error

I have a question here. ghost var b := doet not generally ensures that the right hand side is not computed. For example, if the right-hand-side was a method with side-effects, it would be computed at run-time and its value would be discarded.
Is there a mechanism that decides whether or not compute the right-hand-side? If so, could you point it out to me?

[RustanLeino]

ghost var b := set f: SpecialFruit | f in a && G(f) < 10; // since the RHS expression occurs in a ghost context, I would not have expected an error

I have a question here. ghost var b := doet not generally ensures that the right hand side is not computed. For example, if the right-hand-side was a method with side-effects, it would be computed at run-time and its value would be discarded. Is there a mechanism that decides whether or not compute the right-hand-side? If so, could you point it out to me?

Here's how to distinguish these cases. First, think of any

[ghost] var locals := RHSs;

as first declaring the variables and then doing the assignment:

[ghost] var locals;
locals := RHSs;

Next, there are two possible statements that the syntax LHSs := RHSs; can refer to. One possibility is that LHSs := RHSs; is a (simple or simultaneous) assignment:

lhs0, lhs1, ... := rhs0, rhs1, ...;

where the number of LHSs equals the number of RHSs, and all of the RHSs are expressions. For this assignment statement, the compiler will erase any lhs_i := rhs_i where the lhs_i is ghost. The other possibility is that LHSs := RHSs; is a method-call statement:

lhs0, lhs1, ... := M(...);

In this statement, there is only one RHS and it is a method call, and there are as many LHSs as M has out-parameters. For this statement, the compiler will erase any lhs_i that corresponds to a ghost out-parameter of M; and if M itself is a ghost method, then the compiler erases the entire statement.

The two possibilities above look syntactically identical if there is one LHS and one RHS, and the RHS has the form P(...):

lhs := P(...);

If P is a function, then P(...) is an expression, so the statement is a simple assignment statement. If P is a method, then the statement is a method-call statement.

[RustanLeino]

Is the additional isGhost parameter to VarDeclStmt really needed? More to the point, does it do the right thing?

[RustanLeino]

This seems suspicious to me. isGhost says whether or not the ghost keyword was used as part of the declaration. But this does not determine anything about ghostness of any initializing RHSs. For example, if the RHS is a method call (where all of the method's out-parameters are ghost), then

ghost var x, y, z := M(...);

declares 3 ghost variables and then performs a non-ghost method call. As an example in the other direction, suppose N is a non-ghost method with 3 out parameters, the first and third of which are ghost. Then, in

var x, y, z := N(...);

the local variables x and z will be "auto-ghosted". Hence, this statement declares 2 ghost variables and 1 non-ghost variable and then makes a non-ghost method call. As a third example, consider

var x, y, z := E, F, G;

where E and G and ghost expressions and F is a non-ghost expression. Here, x and z will again be auto-ghosted, so the statement declares 2 ghost variables, 1 non-ghost variable, and then performs a simultaneous assignment.

[MikaelMayer]

You're right, and in the newest code, I actually had removed the code that was checking this "declared ghost" attribute., so I removed it.

Something interesting now is that, if we have the statement:
var h := forall x: GhostSubsetType:: x in OriginalType ==> PredicateFailingOnNonGhostSubsetType(x);
then h will be inferred to be ghost and thus it will accept the GhostSubsetType on the right.

However, it enable me to further think about this ghost inference and here is something that did not work before and that now works thanks to my last commit:

method firstParameterGhost(ghost b: bool) {
}
function method firstParameterGhostFun(ghost b: bool) {
}
method Main() {
  firstParameterGhost(forall x: GhostSubsetType:: x in OriginalType ==> PredicateFailingOnNonGhostSubsetType(x));
  var x := firstParameterGhostFun(forall x: GhostSubsetType:: x in OriginalType ==> PredicateFailingOnNonGhostSubsetType(x));
}

Now it correctly infers the actual binding to be ghost and accepts the usual typing.

[RustanLeino]

(defautl) --> (default)

[RustanLeino]

The comments on L12, L16, and L17 say that errors are reported, but the .expect file doesn't show any errors. Please update the comments.

[MikaelMayer]

I'm not use if you are commenting the right file, because the expect file does show three errors:
https://github.com/dafny-lang/dafny/pull/1702/files#diff-3adf349d1fbe3d24aaf31d072ed9c82757730d1ed46b657bcbf074483ac27d96

[MikaelMayer]

I just reached a fantastic milestone. All the tests are now passing.
@keyboardDrummer and @robin-aws you can now step in and give me feedback, probably on the implementation side.

[keyboardDrummer]

If the static type of the candidate values is already a subtype of GhostEvenCell, then everything is fine. For example, if the BoundedPool discovers c in S where S has type set, then everything is fine. Then, the compiler emits code that evaluates the body of the comprehension for every candidate value.

Can you give an example where a compilable body constrains set c: GhostEvenCell | body to be a subset of GhostEventCell or point me to a test-case where this is the case?

Actually, could you add a few examples to the PR description if what will now be allowed that previously was not allowed?

[keyboardDrummer]

Could you, as a follow-up PR, move all the Microsoft.Dafny.Type related types out of DafnyAst.cs ?

[MikaelMayer]

That's a good idea for a refactoring. I can even apply @cpitclaudel 's trick to duplicate the file and thus keep the history.

[keyboardDrummer]

Shouldn't this be a virtual method implemented in the specific types? Otherwise the definition might get outdated if we add a new type of type.

[MikaelMayer]

The problem will only arise if we add more types that cannot be checked at run-time, meaning they carry ghost constraints. This can be the case only when there is a subset type declaration, or when the type has not been inferred yet. That's the only two possible case where we cannot say for sure that the type is compilable.
Compilability being used only in the case of type conversion (i.e. checking for a constraint), it is not a property newtypes need because their constraint does not need to be checked at run-time.

[keyboardDrummer]

Yes, I understand the above, but still shouldn't the type specify whether it's possible to check that a value has this type at run-time, instead of a single method determining that for all types?

[keyboardDrummer]

// This line should work because c should be of type Cell as the constraint is not compilable

I don't get this line.

Is the type of c inferred to be GhostEvenCell based on the call to ghostEvenCellIsOneOrMore ?

How is set c: GhostEvenCell | .. :: c compilable? Shouldn't c : GhostEvenCell imply that we can't generate the values of c in a compiled context? Does the constraint isEvenCell(c) make it compilable, since it is compilable and happens to constrain c: Cell to the same subset as c: GhostEventCell?

[keyboardDrummer]

Can you put fields at the top of the type declaration? Also, what is the meaning of otherType? Could you add a comment?

[keyboardDrummer]

Should this be set n ?

[keyboardDrummer]

What happens if you explicitly type n to GhostNat ?

[keyboardDrummer]

My assumption is that if a compiler can not infer a type for me, then I have to explicitly provide the type, but I believe that's not what you're trying to say here, is it?

[MikaelMayer]

Can you give an example where a compilable body constrains set c: GhostEvenCell | body to be a subset of GhostEventCell or point me to a test-case where this is the case?

Yes, here:
https://github.com/dafny-lang/dafny/pull/1702/files#diff-3650380410d4f90c335dd7eaf17caf895d7630fe4720fdc0a58889666ac58fdfR77

Let me add examples in the PR

[MikaelMayer]

Let me add examples in the PR

I added examples at the beginning of the PR description for the two things this PR handles, namely authorizing subset types in comprehensions, as well as fixing the compiler soundness bug.

[keyboardDrummer]

The PR description contains this segment about when quantifiers over subset types with ghost constraints can still be compiled:

Consider a comprehension like set c: GhostEvenCell | …, where the GhostEvenCell may not be run-time checkable. In this case, it may be impossible to emit compiled code. However, there are two cases where we can and will allow it:

• If the static type of the candidate values is already a subtype of GhostEvenCell, then everything is fine. For example, if the BoundedPool discovers c in S where S has type set, then everything is fine. Then, the compiler emits code that evaluates the body of the comprehension for every candidate value.
• NEW If the static type of the candidate values is a type T that is not a subtype of GhostEvenCell, then the verifier will check if, by chance, the body of the comprehension is written in such a way that (a) it is well-formed for every T value (as if bound variable c could have been declared to have type T) and (b) every T value that satisfies the body is in fact a GhostEvenCell. If the verifier is able to check this, then the comprehension is allowed and the compiler can use T as the static type of the bound variable used in the emitted code

Shouldn't that explanation be in the documentation as well?

Honestly, the above seems quite complicated. Do users really need to compile code that references subset types with ghost constraints? It seems simpler not to allow it. Can't the user just change the constraint of their subset type so it's no longer a ghost constraint? What's the motivating example where a user needs to have a ghost constraint subset type be part of a compiled quantifier?

[MikaelMayer]

Let's be empirical: subset types are one of the things that are the most powerful things in Dafny, because they can embed pre and post conditions implicitly anywhere.

Do users really need to compile code that references subset types with ghost constraints?
What's the motivating example where a user needs to have a ghost constraint subset type be part of a quantifier?

Let me elaborate on this to explain to you why this is not only useful, but also necessary for real code.
The ghost constraint only indicates specifications that these values must adhere to, and one good thing is that they are not checked at compile-time, so it means performance improvement. But if they are not checked at compile-time, we need to verify that these constraint hold anyway.
It's like the "function by method" paradigm. We might want to ensure a predicate (the constraint of the subset type), but there might be a more efficient way to compute it.

For example, if you had:

predicate P(t) { A && B }
predicate Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)

Let's say you have a set<TP> and you need a set<TQ> in a compiled context:

var setOfTp: set<TP> := ...
set t: TQ | t in setOfTp

Without this PR, you'd have to 1) make the predicate P and Q not ghost, which transitively would result in every of their dependencies being not ghost, including constant fields. That's a bummer.
2) The predicate Q(t) would be checked for every element of setOfTp, which includes expressions we already know hold like A and B. That's a performance penalty that any user would prefer to avoid if possible.

With this PR, you don't change the ghostness of P or Q, and you'd write the set comprehension

set t: TQ | t in setOfTp && C

And that just works as expected, the verifier can prove after && C that t is a TQ

It seems simpler not to allow it.
I'm not sure what you mean here. Of course it is simpler to not support a construct than to support it. Can you please elaborate a bit more?

Can't the user just change the constraint of their subset type so it's no longer a ghost constraint?
First, it's not always possible. Some constraints might refer to ghost fields of classes for example. Second, as explained before, verification aims at removing run-time checking of constraints so that the code can be more performant.
So, if a user can do it, they can definitely change a constraint to be compilable and they won't have any problem, because that constraint will be checked. But this PR gives them the freedom to choose.

[MikaelMayer]

I'll update the documentation, thanks for pointing this out.

[keyboardDrummer]

Okay, thanks for the explanation.

So does this program

predicate P(t) { A && B }
predicate Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

Perform better than this one?

predicate P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp

And what about this one?

predicate P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

[MikaelMayer]

Both of your last examples are not allowed, because Q is non-ghost and is trying to call a ghost predicate in an expression that is not a specification of Q
What you probably want is to compare:

predicate P(t) { A && B }
predicate Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

with

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp

The first one will just enumerate all the elements of setOfTp and then check if C holds, whereas the second one having not necessarily compatible types will need to check Q(t) for every t.

However, there is still an open question for this one:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

Here, theoretically, the verifier should be able to prove that it's not necessary to do the check Q(t) for every element since C enforce it.
However, this mechanism might be very hard to enforce. Currently, because when the predicates are compilable, the type of t in t in setOfTp && C is inferred by the resolver to be TQ directly. The reason for that is that this condition can be checked by the compiler, so it's safe to do so, so C will hold anyway.
If someone would really like to have compiled predicates but benefit from an optimization of not re-checking the previous predicates, in this context, they would be able to do so by writing the following:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ, p: TP | p in setOfTp && C[t/p] && t == p :: t

This is saying "Take all the elements of setOfTp with their original type, verify the additional constraint, and if it holds assign it to t, thus verifying that this constraint hold", which I believe is acceptable.

[keyboardDrummer]

Both of your last examples are not allowed, because Q is non-ghost and is trying to call a ghost predicate in an expression that is not a specification of Q What you probably want is to compare:

predicate P(t) { A && B }
predicate Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

with

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp

The first one will just enumerate all the elements of setOfTp and then check if C holds, whereas the second one having not necessarily compatible types will need to check Q(t) for every t.

However, there is still an open question for this one:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

Here, theoretically, the verifier should be able to prove that it's not necessary to do the check Q(t) for every element since C enforce it. However, this mechanism might be very hard to enforce. Currently, because when the predicates are compilable, the type of t in t in setOfTp && C is inferred by the resolver to be TQ directly. The reason for that is that this condition can be checked by the compiler, so it's safe to do so, so C will hold anyway. If someone would really like to have compiled predicates but benefit from an optimization of not re-checking the previous predicates, in this context, they would be able to do so by writing the following:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ, p: TP | p in setOfTp && C[t/p] && t == p :: t

This is saying "Take all the elements of setOfTp with their original type, verify the additional constraint, and if it holds assign it to t, thus verifying that this constraint hold", which I believe is acceptable.

Thanks for the great explanation, and you were right about what I probably wanted.

Can we add the various alternatives and their performance impact to the documentation? Please correct me if I'm wrong, but these are the alternatives I see now:

• Compilable constraint subset type that is checked at runtime. (this one is already in the documentation)
• Compilable constraint subset type that is checked at compile-time. (your last example)
• Ghost constraint subset type that is not allowed (this one is already in the documentation)
• Ghost constraint subset type that is allowed because
  • Source collection is already a subset of the bound variable type
  • Comprehension range constraint specifies a subset of the bound variable type

[keyboardDrummer]

One more thing, is the emitting of runtime checked constraints something that is added in this PR, or did that already exist?

My preference would be for runtime checks to require an explicit piece of syntax, so the performance impact is clear to the user. Something like t is TQ in the following:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && t is TQ

Which would cause a runtime check of Q(t) for every element in setOfTp.

In this approach, the verifier should always verify that the range of the comprehension only produces elements of type TQ, so a program like:

predicate method P(t) { A && B }
predicate method Q(t) { P(t) && C }
type TP := t | P(t)
type TQ := t | Q(t)
set t: TQ | t in setOfTp && C

Would also verify and only produce the runtime check C but not A && B

[MikaelMayer]

One more thing, is the emitting of runtime checked constraints something that is added in this PR, or did that already exist?

That emission already existed before, in the previous CreateForEach method, when the subset type had a compilable constraint:
https://github.com/dafny-lang/dafny/pull/1702/files#diff-daf85b4917468b5fae254d3b53259f20e3558d36340819d1e91a2b6ba2d4e18fL4663
https://github.com/dafny-lang/dafny/pull/1702/files#diff-daf85b4917468b5fae254d3b53259f20e3558d36340819d1e91a2b6ba2d4e18fL4705
It was was not always checking the subtype as well (hence the compiler soundness bug).

Your point is a very interest one and it might require more consideration, because it would break existing code, which i tried to avoid if possible. For example:

var s := set x: nat | x in setOfInt

verifies and compiles, before this PR. This PR keeps that same behavior.

Your idea needs the check x >= 0 or x is nat needs to become explicit. We might want to keep this change for a big version change as a separate PR, if we agree on that (which is possible, after all, I like performance and I like it when things are not made invisibly).

[keyboardDrummer]

We might want to keep this change for a big version change as a separate PR

Sounds good. Thanks for explaining!

[MikaelMayer]

Can we add the various alternatives and their performance impact to the documentation? Please correct me if I'm wrong, but these are the alternatives I see now:

• Compilable constraint subset type that is checked at runtime. (this one is already in the documentation)

• Compilable constraint subset type that is checked at compile-time. (your last example)

• Ghost constraint subset type that is not allowed (this one is already in the documentation)

• Ghost constraint subset type that is allowed because

  • Source collection is already a subset of the bound variable type
  • Comprehension range constraint specifies a subset of the bound variable type

I added three examples to cover these missing cases in the documentation.

[keyboardDrummer]

Please resolve the Wish. I think it's OK like it is. You could consider replacing true with isSpecification: true

[MikaelMayer]

Thanks for pointing it out. You made me realize that there was yet another soundness bug there, here is a repro:

ghost const zero := 0
type GhostNat = x : int | x >= zero
const S: set<int> := {-1, 0, 1};
type GhostNatInS = x : int | x in (set j: GhostNat | j in S)

function method FailIfNotGhostNat(i: GhostNat): int {
  if i < 0 then 1/0 else i
}

method Main() {
  var s := forall x: GhostNatInS | x in S :: FailIfNotGhostNat(x) == x;
  print s;
}

If we resolve the constraint with "isSpecification: true", then j will have the type GhostNat, and the current computation of ExpressionTester.CheckIfCompilable will return that it is compilable, when it is not.
I'm fixing it soon with the next commit (both isSpecification is false and the code context is not ghost here for this fix)
I also add this file as a test file.

[keyboardDrummer]

What's the meaning of this field? Could you add a comment?

I see it has a similar affect as codeContext.IsGhost, based on the later line
!opts.isSpecification && !opts.codeContext.IsGhost

Do we need both?

[MikaelMayer]

This fields means that we are in an expression that is always ghost. For example, invariants, assertion bodies and "by" statements, calc statements, or pre/postconditions.

The codeContext might not be ghost, for example if we are in a compiled method, the codeContext is the method and isGhost is false. I was originally relying on it, only to discover that it's not useful to say an expression is ghost. It works only for lemma or ghost functions.

Hence, I added this option so that the resolver can quickly infer if an expression is ghost, even before ghost inference, so that it will not bother creating two types for variables in comprehensions with a ghost constraint.
We could remove it by letting the ghost inference mechanism to automatically select the right inference, but since this mechanism is new, I am more willing to put some code (isSpecification:true) that ensures every expression in a specification position is still resolved the same.

[keyboardDrummer]

Would it also be possible to instead of introducing the parameter isSpecification to wrap the codeContext using new CodeContextWrapper(codeContext, isGhostContext: true) ?

[MikaelMayer]

That sounds like a good idea, I did not see there was a CodeContextWrapper until now. Let me try

[keyboardDrummer]

The name otherType doesn't tell me much, and the value of it and type, and their associated meaning, seem to be swapped sometimes. Can we replace the swapping mechanic with values that are assigned once?

I believe there's

• the type that the user has specified for the bound variable
• The closest supertype of specified type which is also compilable, which is the same as the specified type if that is compilable.

[MikaelMayer]

Indeed, these types are swapped sometimes, but here is something to note:
otherType is not the publicly accessible field. The fields that should be publicly accessed to access stable types are are CompilableType``and OriginalType`.

The rationale because of the swapping is that I did not want to change the "scope" mechanism that is being used by the resolver: scope.Push(v.Name, v);. It pushes both the variable's name and the variable itself (with is .Type) in the scope.
However, I needed to resolve the range in two settings: when the type of that variable is the type the user has specified (in case it's explicit), and when the type of that variable is the compilable supertype of the original type.
For the resolver, swapping enables resolution to not care about that is the context which defines the variable's type, just access Type.
I tried alternatively to create another bound variable with the other type, but it would then allocate a new compiled name for it, which was undesirable.

[keyboardDrummer]

I see. So there are three public fields: Type, CompilableType and OriginalType, and two backing field type and otherType, that work with the boolean CurrentTypeAssumedToBeCompilable.

How do you feel about letting CompilableType and OriginalType use a backing field, and implementing Type using Type => CurrentTypeAssumedToBeCompilable ? CompilableType : OriginalType ?

OriginalType could use type as its backing field.

---

I'm still trying to grasp why BoundVariable needs four state changing operations:

• AssumeCompilableType
• AssumeCompilableTypeIfAny
• AssumeOriginalType
• AcceptOriginalTypeAssumption

I would have hoped you only go from one state to another, but it seems like you go back and forth.

        if (s.IsBindingGuard) {
          var exists = (ExistsExpr)s.Guard;
          AssumeOriginalTypeForBoundedVariables(exists!);
          foreach (var v in exists!.BoundVars) {
            ScopePushAndReport(scope, v, "bound-variable");
          }
        }
        dominatingStatementLabels.PushMarker();
        ResolveBlockStatement(s.Thn, codeContext);
        dominatingStatementLabels.PopMarker();
        scope.PopMarker();
        if (s.IsBindingGuard) {
          var exists = (ExistsExpr)s.Guard;
          AssumeCompilableTypeForBoundedVariables(exists!);
        }

What's the reason for the above code?

---

Would it be possible to use only two public types, Type and SpecifiedType, where SpecifiedType has its own backing field and is always the user specified type, and implement BoundVariable.AssumeOriginalType by saying Type = SpecifiedType
and BoundVariable.AssumeCompilableType with Type = compilableType ?

[MikaelMayer]

How do you feel about letting CompilableType and OriginalType use a backing field, and implementing Type using Type => CurrentTypeAssumedToBeCompilable ? CompilableType : OriginalType ?

OriginalType could use type as its backing field.

Thanks! That was helpful. I implemented it.

[MikaelMayer]

What's the reason for the above code?

Ok I managed to simplify it at the end, but here is the story because I think there is still more work to do in the future. I first came across the following case:

if x :| P(x) {
  S(x);
}

Which actually uses an exists expression with a bound variable x, but further makes the "then branch" bound with that same bound variable. Hence, it's as if the "then body" was part of the "term expression" of the exists. However, after resolving the Exists expression, the resolver currently sets back the "compiled" type for the bound variable, if it exists, for the verifier later to verify that the ghost constraint holds.
So, I need to temporarily revert back to the "specified type" so that type inference in the then body uses the specified type, not the compilable type, and then I put the "compiled type" for later.

I just tried to ensure that the verifier uses the compilable type anyway, so that we don't need to switch back and forth (and leave the specified type for bound variables).

This lead me to discover the following inception challenge that would require more thinking now:

ghost const zero := 0
type GhostNat = x : int | x >= zero
const S: set<int> := {-1, 0, 1};
type GhostNatInS = x : int | x in (set j: GhostNat | j in S && j >= 0)

function method FailIfNotGhostNatInS(i: GhostNatInS): int {
  if i < 0 then 1/0 else i
}

method Main() {
  var s := forall x: GhostNatInS | x in S :: FailIfNotGhostNatInS(x) == x;
  print s;
}

The challenging question is:

Is the constraint of the type GhostNatInS ghost or not?

If it is statically ghost, then the Dafny verifier will detect that the forall range cannot prove that x is GhostNatInS. If it is not statically ghost, then the Dafny verifier will verify that j in S && j >= 0 implies that j is GhostNat, which is true, and then succeed, which is what we want.
However, "ghostness" is currently inferred statically from the subset constraint itself, and there is no check to determine if set i: GhostNat | ... is ghost, so it will infer it's compilable (because it has bounds). The constraint is currently parsed as ghost anyway, so it's consistent with the fact that it should not find any kind of ghostness to infer that the constraint is compilable.

Note that if any bound variable with a ghost constraint was triggering its enclosing expression to be ghost, that means that the above example would not work because s would be ghost and the print statement would fail, and this PR expressedly aims at avoiding this abusive ghost inference.

To sum up, we have the following problem:

• The constraint of GhostNatInS is currently resolved as in a "ghost context", so that it tolerates if the bound variable has a ghost subset type.
• When checking whether the constraint is ghost or not, we don't infer that bound variables with a ghost subset type trigger the whole expression to be ghost. If we did the same algorithm would infer that every comprehension with a ghost subset type cannot be compiled, which this PR aims at avoiding.
• Thus, the algorithm thinks it can inline this constraint. In the example, above, and if we removed j >= 0 (test git-issue-1604h.dfy), it would throw an exception at run-time after the Dafny verifier would tell everything is ok

The current master avoid all these problems because it does not allow ghost constraints in compiled contexts, and because the constraint is immediately resolved to be compilable or not after resolution and (set j | ...)` does not have inferred bounds yet (bounds inference comes after resolution), it's marked as ghost. So, it's a kind of a hack that it works.

In this PR, I changed the way we parse the subset constraint, and assumed it's compilable, so that the verifier will verify such subset types. This mean it introduces one breaking change: It's no longer possible to have ghost comprehensions in the constraint of a subset type, they would need to be wrapped in a ghost predicate instead. I'll document that.

@RustanLeino, if you are able to follow, I would love your advice on this. It seems that it would be great to add the keywords "ghost" and/or "compiled" to the type to be able to enforce one or the other.

[keyboardDrummer]

I looks like here we're saying the specified type of the bound variable, and of that its compilable parent type, should be a subtype of the source collection type of the comprehension. Do I read that correctly?

I think I expected that to be the other way around, that the source collection type should be a subtype of the compilable parent type of the specified bound variable type.

Could you help resolve my confusion?

[MikaelMayer]

Linking back to where the constraint SubsetTypeOfCompilable is defined, we have:

Types[0] = u = v.Type = requestedType
Types[1] = t = collectionVarType = collectionElementType

So, the added constraint states that the collectionVarType should be a subtype of the compiled supertype of the requested type, which is exactly what you expected.
With the renaming I'm pushing, it should be clearer.

[keyboardDrummer]

The new code is

resolver.ConstrainSubtypeRelation(collectionElementType, requestedVariableType.GetCompilableParentType(), errorMsg, true);

The first argument is the superType and the second the subType, so it's saying that the compilable parent type should be a subset type of the collection element type. That's not correct right?

[MikaelMayer]

Yikes! You're right, the supertype arguably comes first based on the signature, which I did not expect by reading the code.
It probably did not bother in practice because there was only one type for the collection type and it chose it (whether it was the upper or lower bound), but I see how it could create errors. Let me fix that.

[keyboardDrummer]

Is this covered in the tests?

[MikaelMayer]

I haven't found a case when the ghost inference did consider a map with a "ghost" subset type either in the Range or its domain as "compilable", so I don't think I can come up with a case where returning true or false here would make a difference in files
Would you like however that I add small unit tests for all of these public functions in DafnyPipeline.Test?

[keyboardDrummer]

Is this covered in the tests?

[MikaelMayer]

I haven't found a case when the ghost inference did consider a seq with a "ghost" subset type in its Range as "compilable", so I don't think I can come up with a case where returning true or false here would make a difference in files
Let's continue the discussion here:
#1702 (comment)

[keyboardDrummer]

Consider phrasing

git-issue-1604e.dfy(65,37): Error: Could not prove that the bound variable 'go' satisfies the (non runtime testable) type GhostOrdinalCell after the range, where it's assumed to be of type Cell based on inferred bounds.
git-issue-1604e.dfy(24,24): [Related location] The constraint of GhostOrdinalCell is not run-time testable because it depends on the non-runtime-testable subset type GhostNaturalCell
git-issue-1604e.dfy(13,35): [Related location] The constraint of GhostNaturalCell cannot be tested at run-time because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')

as

git-issue-1604e.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added.
git-issue-1604e.dfy(24,24): [Related location] The subset type GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because its constraint calls a ghost predicate. Consider declaring the predicate with 'predicate method'.

[MikaelMayer]

I'm changing almost everything according to your suggestions, except 1) I do include the type of the collection element in the error message and 2) the reason in in the last one, because that would touch other pieces of error reporting. The original error I catch is "a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')", and I just wrap it with a "because".

Here is the final rendering:

git-issue-1604e.dfy(65,37): Error: Could not prove that the range constrains the bound variable 'go' to be of type GhostOrdinalCell, and since GhostOrdinalCell is a ghost subset type, no runtime type filter can be added on the collection whose elements have the type Cell.
git-issue-1604e.dfy(24,24): [Related location] The subset type GhostOrdinalCelltype GhostOrdinalCell is ghost because it depends on the ghost subset type GhostNaturalCell
git-issue-1604e.dfy(13,35): [Related location] GhostNaturalCell is ghost because a call to a ghost predicate is allowed only in specification contexts (consider declaring the predicate with 'predicate method')

[keyboardDrummer]

Consider renaming constraintReason and constraintLocation to baseTypeReason and baseTypeLocation. I'm dropping the word constraint because we're in the property IsConstraintCompilable so it seems clear enough that we're dealing with constraints.

[keyboardDrummer]

So, why don't we get an error about a precondition violation?

[MikaelMayer]

git-issue-1604f.dfy(38,40): Error: possible violation of function precondition
is an error about a precondition violation. I'm just adding more useful information in case some users are confused, as @RustanLeino suggested. What do you mean here?

[keyboardDrummer]

I don't understand why the original precondition violation error is not shown. Based on the code it seemed like you were adding an extra error but not hiding an existing now.

[MikaelMayer]

The code shows I'm adding an extra message to the original precondition violation error:
https://github.com/dafny-lang/dafny/pull/1702/files#diff-2375e053597753dae383e30da45bce3a97e5fa2e7e9a3fc601cf68923df03516R5747
error message used here (unchanged lines)
https://github.com/dafny-lang/dafny/pull/1702/files#diff-2375e053597753dae383e30da45bce3a97e5fa2e7e9a3fc601cf68923df03516R5758-R5760

[keyboardDrummer]

I guess you're overwriting the error message from line 5737:
string errorMessage = CustomErrorMessage(p.Attributes);

[MikaelMayer]

Only if errorMessage == null, so I wouldn't call it "overriding", just "provide another default message".
But you pointed out one important thing: There was duplication in the error, which can now be resolved by the new ProofObligationDescription. I added an optional hint to it and I'm now only filling that hint instead of modifying the error message.

[keyboardDrummer]

I'm surprised. Why would x >= 0 from nat be tested? The source collection s already contains nat.

[MikaelMayer]

You're right. I just added an optimization in the compiler so that if it reaches the original collection's type, it stops emitting constraints. Thus I also changed the example in this documentation to reflect a case when the compiler cannot arrive to the same type of the collection, and emits all constraints until int. Thus, the trick is still valid afterwards.

[keyboardDrummer]

Consider being more explicit about what happens at runtime:

the type of the comprehension will be fully tested => at runtime, a filter is applied to the elements from the collection that keeps only values of the comprehension type.

[MikaelMayer]

Reformulated as:

"A special case to be aware of: if the type in the comprehension differs from the collection,
but both are compilable, at runtime, every subset constraint yields a filter to be applied to the elements from the collection to keep only values of the comprehension type. Filtering starts either at the base type, or at the collection type if it happens to be a parent of the comprehension type.
In the first case, it is still possible to customize the emission of the filter to avoid testing redundant constraints. For example:"

[keyboardDrummer]

Should a test be added for this change as well?

[MikaelMayer]

I understand your concern. If the code still works after swapping two arguments, but this version is more meaningful, we should ensure tests break if we revert that change (or if someone comes after me thinking they will fix a potential bug).
As of today though, I don't see an easy way to test this.
To make a test that would work on the second but fail on the first

• We would need a case where the bound variable's type is not explicitly given in the comprehension. Otherwise, this constraint would not even be emitted in the first place.
• We would also need that, at the time of confirming this constraint
  • the bound variable's type that must hold after the range is determined (first "if" of "ConfirmSubsetTypeOfCompilable" in Resolver.cs)
  • the collection's type must not be determined yet (second "if" of "ConfirmSubsetTypeOfCompilable" in Resolver.cs). That "if" could also be a point of discussion, basically, it says that if the two types are determined, then we can just let the verifier do its job, we don't need resolution checks, even if the types would not match.

Given the above, and that the confirmation of the constraint happens after the comprehension is resolved, I don't know how to create a test where the collection's type is determined by the inferred type of the bound variable. I even discovered a bug doing so (#2074 - thanks for your prompt !) so it's unlikely I can myself even create a test for that purpose anytime soon.

[keyboardDrummer]

@MikaelMayer could we go back to the motivating example again? I'd like to understand this well. You gave the following example:

predicate P(t: int) { 
  t > 3
}

predicate Q(t: int) { 
  P(t) && t < 19
}

type TP = t: int | P(t) witness 20
type TQ = t: int | Q(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := set t: TQ | t in setOfTp && t < 19; // Possible with the new changes
}

But, a user could also do this right?

predicate P(t: int) { 
  t > 3
}

predicate Q(t: int) { 
  P(t) && t < 19
}

predicate method QminusP(t: int) { 
  t < 19
}

type TP = t: int | P(t) witness 20
type TQ = t: TP | QminusP(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := set t: TQ | t in setOfTp && QminusP(t);
}

It doesn't seem difficult to massage the types to get the desired code and runtime performance.

[MikaelMayer]

But, a user could also do this right?

In this example, yes, the architecture you suggest is way better ! It's always better to have a "hierarchy" so that to only test what is relevant, not overlapping properties.

Your refactoring would not be possible however if we replaced TP with:

type TP = t: int | P(t) && t % 3 != 0 witness 20

In that case, TP and TQ don't have something in common so, if the predicates were compilable, the compiler would still test P(t).

[keyboardDrummer]

But, a user could also do this right?

In this example, yes, the architecture you suggest is way better ! It's always better to have a "hierarchy" so that to only test what is relevant, not overlapping properties.

Your refactoring would not be possible however if we replaced TP with:

type TP = t: int | P(t) && t % 3 != 0 witness 20

In that case, TP and TQ don't have something in common so, if the predicates were compilable, the compiler would still test P(t).

I'm sorry but I don't follow. What does it matter if I add additional constraints to P or TP that are not explicitly constrained in TQ ?

The below program does not test P(t) && t % 3 != 0 at runtime right?

predicate P(t: int) { 
  t > 3
}

predicate Q(t: int) { 
  P(t) && t < 19
}

predicate method QminusP(t: int) { 
  t < 19
}

type TP = t: int | P(t) && t % 3 != 0 witness 20
type TQ = t: TP | QminusP(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := set t: TQ | t in setOfTp && QminusP(t);
}

[MikaelMayer]

The below program does not test P(t) && t % 3 != 0 at runtime right?

I assume you meant predicate method P and same for Q, correct me if I'm wrong.

My example was supposed to apply on my original code:

predicate method P(t: int) { 
  t > 3
}
predicate method Q(t: int) { 
  P(t) && t < 19
}
type TP = t: int | P(t) && t % 3 == 0 witness 20
type TQ = t: int | Q(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := set t: TQ | t in setOfTp;
}

In this case, you cannot define TQ in function of TP, nor with a trick like QMinusP, so Q(t) will be cheched at compile-time and thus P(t) will be evaluated, although we know it was true because the value is of type TP.
Of course, one way to solve this problem is to define the "smallest ancestor" of TP and TQ that only checks P(t) so that it does not need to be checked at compile-time.

[keyboardDrummer]

Thanks for all the changes. I find the code much more readable now.

However, I do still have some concerns with this PR, some of which are quite subjective. Would you mind getting a second reviewer to weigh in on these? I don't want to block your PR but I also don't feel comfortable enough to approve it.

Here are my remaining concerns:

1. It's not clear to me that the user-benefit of this feature outweighs the weight of having it in the codebase. I'm not sure if this is a trade-off we've made before, but I know that it's one that other compiler teams like the .NET Roslyn team make, and I think it would be good if we do as well. It would be good if we had some references to trade-offs other teams have made but sadly those weren't so easy to find.
   1. On the benefit side: it seems like users can restructure their types to get the same benefit this PR provides. Have Dafny users expressed they want this feature?
   2. On the cost side: I rate the complexity of this PR as high. There are some surprises in the code, BoundVar switching between different type modes, Range expressions being cloned and typed in different ways. Resolution happening with and without reporting.
2. (minor) This PR will sometimes treat a variable that occurs in a range expression as having a different type than the type it was explicitly declared with, which feels like it breaks a language invariant. In the worst case I can imagine a user no longer being sure what types their variables have in locations other than range expressions.

[keyboardDrummer]

Not sure if this makes sense, but would it be possible to rewrite comprehensions to avoid having to switch the type of BoundVar and needing RangeIfGhost ?

I was thinking of introducing a second bound variable without an implicit type whose type is inferred to be the compilable type of the comprehension, and to explicitly add the constraint of the user specified bound variable type when possible.

Example:

predicate method P(t: int) { 
  t > 3
}
predicate [method] Q(t: int) { 
  P(t) && t < 19
}
type TP = t: int | P(t) && t % 3 != 0 witness 20
type TQ = t: int | Q(t) witness 10

predicate method C(t: int)

method Foo() {
  var tps: set<TP> := { 4, 5, 20 };
  var original := set q: TQ | q in tps && C(q);
  var rewritten := set q: TQ, p | p in tps [&& Q(p)] && q == p && C(p) :: q;
  // If tps would be of type set<TQ>, we could skip the rewrite.
  // If Q is non-ghost, "&& Q(p)" is added, there are no errors and the runtime code filters on Q(t).
  // If Q is ghost, "&& Q(p)"  is not added and the result depends on the definition of C.
  // If Q is ghost and C(t) { t < 19 }, then there are no errors and the runtime code only filters on C(t).
  // If Q is ghost and C(t) something unrelated, we get the error 
  // "Dafny's heuristics can't figure out how to produce a bounded set of values for 'q'. Consider making the constraint of TQ non-ghost."
}

[keyboardDrummer]

The below program does not test P(t) && t % 3 != 0 at runtime right?

I assume you meant predicate method P and same for Q, correct me if I'm wrong.

My example was supposed to apply on my original code:

predicate method P(t: int) { 
  t > 3
}
predicate method Q(t: int) { 
  P(t) && t < 19
}
type TP = t: int | P(t) && t % 3 == 0 witness 20
type TQ = t: int | Q(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := set t: TQ | t in setOfTp;
}

In this case, you cannot define TQ in function of TP, nor with a trick like QMinusP, so Q(t) will be cheched at compile-time and thus P(t) will be evaluated, although we know it was true because the value is of type TP. Of course, one way to solve this problem is to define the "smallest ancestor" of TP and TQ that only checks P(t) so that it does not need to be checked at compile-time.

What if I do the following:

predicate method P(t: int) { 
  t > 3
}
predicate method Q(t: int) { 
  P(t) && t < 19
}
type TP = t: int | P(t) && t % 3 != 0 witness 20
type TQ = t: int | Q(t) witness 10

method Foo() {
  var setOfTp: set<TP> := { 4, 5, 20 };
  var setOfTq := SelectFilter<TP, TQ>(setOfTp, tp => if tp < 19 then Some(tp) else None); 
}

function SelectFilter<From, To>(input: set<From>, cast: From -> Option<To>): set<To> 
{
  if |input| > 0 then (
    var s :| s in input; 
    var rec := SelectFilter(input - {s}, cast); 
    var toCast := cast(s); 
    if toCast.IsFailure() then rec else {toCast.Extract()} + rec)
  else 
    {}
}

Then I can avoid having to do restructure my types and checking Q(t) at runtime.

[keyboardDrummer]

What creates the duplication between line 15305-15307 and 15296-15298 ? How come we need this code twice?

[MikaelMayer]

I explain here the reasons about that, but essentially, it's not the same code, one is for the Range, the other is for RangeIsGhost

[keyboardDrummer]

Calls to ScopePushBoundVarsAssumingCompilable and ScopePushBoundVarsWithoutAssumptions seem to occur in pairs. Would it make sense to capture this pattern in a function WithAssumingCompilable that takes an action which it executes between the two calls?

[MikaelMayer]

1. It's not clear to me that the user-benefit of this feature outweighs the weight of having it in the codebase. I'm not sure if this is a trade-off we've made before, but I know that it's one that other compiler teams like the .NET Roslyn team make, and I think it would be good if we do as well. It would be good if we had some references to trade-offs other teams have made but sadly those weren't so easy to find.

It's very hard to compare "user benefit" on the same scale as "the weight of having it in the codebase".
The fact that we have set that can be defined using a single predicate for both enumeration and filtering is something unseen in other languages.
The feature of set comprehensions (and any comprehension) was unfortunately not developed with respect to the feature of ghost subset types, until this PR both could not work together.
Hence, although this PR says it's a feature, it could arguably be said that it fixes a feature mismatch.

1. On the benefit side: it seems like users can restructure their datatypes to get the same benefit this PR provides. Have Dafny users expressed they want this feature?

This PR provide support for subset types, not datatypes, so I'm not sure about your remark. Let me assume you mean "subset type" instead of "datatype".
In the current version of Dafny, they just cannot get "the same benefit this PR provide" by restructuring subset types, what you probably have in mind is either what you mentioned elsewhere.

1. require to add the support for ghost subset types in set comprehensions but verify that they are not iterated on. This is nontrivial work, and it would be strictly less powerful than what this PR implements.
2. Use a special helper function like the one you suggested that they would define themselves (or would be part of the library). But whatever implementation you make of this function, in Dafny, you'll always be much slower than a native implementation that we can control on the compiler. Moreover, it would be much less idiomatic.

Yes, users have expressed repeatedly the need to have better integration of subset types, and bugs or missing features concerning them are one of the major thing preventing their adoption. (#2020, #1875, #1715, #1680 and many others)

2. On the cost side: I rate the complexity of this PR as high. There are some surprises in the code, BoundVar switching between different type modes, Range expressions being cloned and typed in different ways. Resolution happening with and without reporting.
3. (minor) This PR will sometimes treat a variable that occurs in a range expression as having a different type than the type it was explicitly declared with, which feels like it breaks a language invariant. In the worst case I can imagine a user no longer being sure what types their variables have in locations other than range expressions.

These are not "surprises", every part is necessary for the whole thing to work as-is.

1. Bound vars need to switch types because it's not possible for the bound variables to have a single type and a comprehension to work with subset types with the current syntax and the way it's compiled (a predicate and heuristics to find the collection)
2. Resolution has to happen before ghost inference (that's a decision taken a long time ago), and ghost inference will change the way set comprehension resolution works because of 1., and resolution cannot happen twice on an expression (it will throw an exception). Hence, range needs to be duplicated before resolution
3. I need to disable error reporting for the second time the range is resolved, because all the resolution errors would be reported twice.

However, I could have a compelling alternative to this PR that you might like that does not have what you call "surprise", that is based on your comments but still suffers from one drawback that I invite you to comment on.
The alternative is to parse and resolve as usual, and then, right when we know for sure when an expression is ghost or not:

• If the comprehensions is in a ghost context (specification or ghost statements), then we don't change a thing.
• Else, for every variable that has a ghost subset type, we verify that it's
  • Either the iteration variable of a set of the same element's type
  • Or defined by an equality to another variable (i.e. the verifier will normally have to ensure that the ghost subset constraint hold at this point)

This approach would be enable the same scenarios as this PR, but would make the set comprehensions slightly more verbose.

With this PR, in a compiled context where TQ is a ghost subset type

set q: TQ | q in tps && PredicateThatEnsuresItIsATQIfP(q);

With the alternative:

set q: TP, qTerm: TQ | q in tps && PredicateThatEnsuresItIsATQIfP(q) && qTerm == q :: qTerm;

I would be happy to report error messages on the first one like:
“the collection is of type TP, but q is requested to have a ghost subset type TQ which is not a supertype of TP. Consider changing set q: TQ | .... to set q: TP, qTerm: TQ | ... && qTerm == q :: qTerm

That way, we avoid the change of type that your rewriting would have. Indeed, the collection is not always necessarily found to be at the beginning, so I don't think it's possible to formalize your rewriting in every case. With requiring the user to explicit write the conversion, we would also avoid any heuristics in "rewriting".

Except from the fact that this notation is a bit more verbose than what this PR offer, it would have the advantage that it would not "switch types" in the background, and could have a simpler implementation requiring only the user to manually write everything that this PR does automatically, without good or bad surprise.

One problem though. Dafny will complain (like it does for set p: TP, q: TP | p in tps && q == p :: q; even now)

/!\ No trigger covering all quantified variables found.",

This is because it believes it has to find a trigger for q as well, which of course it can't.
How do you think we could get rid of this warning?

[MikaelMayer]

Because also @robin-aws agreed that the alternative would be better, I asked @cpitclaudel to help me solve the last issue, and he just gave me a better alternative:

With this PR, in a compiled context where TQ is a ghost subset type

set q: TQ | q in tps && PredicateThatEnsuresItIsATQIfP(q);

With @cpitclaudel alternative's:

set q: TP | q in tps && PredicateThatEnsuresItIsATQIfP(q):: q as TQ;

It already works even on master! The only thing that would be now necessary is to 1) document this somewhere and 2) enable iterating on ghost subset types if it's the same as the collection's type.

Are you ok with this @keyboardDrummer ?

[keyboardDrummer]

Because also @robin-aws agreed that the alternative would be better, I asked @cpitclaudel to help me solve the last issue, and he just gave me a better alternative:

With this PR, in a compiled context where TQ is a ghost subset type

set q: TQ | q in tps && PredicateThatEnsuresItIsATQIfP(q);

With @cpitclaudel alternative's:

set q: TP | q in tps && PredicateThatEnsuresItIsATQIfP(q):: q as TQ;

It already works even on master!

Nice.

The only thing that would be now necessary is to 1) document this somewhere and 2) enable iterating on ghost subset types if it's the same as the collection's type.

Are you ok with this @keyboardDrummer ?

That seems strictly better than what we have.

However, my preference would be to remove the implicit runtime filter operation entirely (breaking change!), so users that want to filter and cast a set always need to do

set q: TP | q in tps && PredicateThatEnsuresItIsATQIfP(q) :: q as TQ

even if the TQ constraint is compilable.

The code

predicate method P(t: int) { 
  t > 3
}
predicate method Q(t: int) { 
  P(t) && t < 19
}
type TP = t: int | P(t) && t % 3 != 0 witness 20
type TQ = t: int | Q(t) witness 10

method Foo() {
  var tps: set<TP> := { 4, 5, 20 };
  var tqs := set q: TQ | q in tps
}

Could give the error message:

"Dafny's heuristics can't figure out how to produce a bounded set of values for 'q'. Only a bounded set of values of type TP was found. See (documentation link) for how to cast values of one set to another."

[robin-aws]

I'm coming into this very late but will offer my opinion in the hopes it unblocks things. Please let me know if I have any incorrect mental assumes because I haven't been able to read every comment. :)

First off, thank you for all the hard work getting this to function correctly! Regardless of what we decide, I don't want to throw it away.

The original PR description gives an example and says "Previously, it would just accept it because it would parse the constraint of the type as ghost." Are you saying the current tip of master allows this, or do you mean before the earlier soundness fix in this area? I want to confirm whether this PR is solving an active soundness issue or just providing more expressivity in the language.

[MikaelMayer]

I'm coming into this very late but will offer my opinion in the hopes it unblocks things. Please let me know if I have any incorrect mental assumes because I haven't been able to read every comment. :)

First off, thank you for all the hard work getting this to function correctly! Regardless of what we decide, I don't want to throw it away.

The original PR description gives an example and says "Previously, it would just accept it because it would parse the constraint of the type as ghost." Are you saying the current tip of master allows this, or do you mean before the earlier soundness fix in this area? I want to confirm whether this PR is solving an active soundness issue or just providing more expressivity in the language.

The current tip of master does not allow ghost subset types as per the soundness fix in another already merged PR.
The last 2 comments before your post are the most important.
This PR is only reinserting ghost subset types in a sound way, i.e. the consensus is that we could allow them only when iterating elements of that same ghost subset type, and use the "as" keyword to get a set of something more precise.

The only difference is that, do we want to implement the breaking change where we remove inlining compilable subset type constraints? That would make things easier to implement (no more check if a subset type constraint is compilable or not), and to reason about (no more hidden added code, even unexpectedly).

[robin-aws]

Great, thanks for clearing that up @MikaelMayer.

For the record, I'll first state that I strongly agree that a Dafny symbol should have a single type assigned to it, regardless of reference context. The complexity in a user's mental model of their code is very high otherwise, and affects how you document the language and even how tooling like IDEs communicate about errors. Although "smart casting" in the style of Kotlin can be convenient, given that Dafny can provably avoid the runtime cost of downcasting, I'd much prefer more explict as expressions as needed instead. If users get really tired of repeating themselves with pairs of is T and as T expressions, there are features like #1715 that would help address that. I'm impressed with the technical difficulty of the earlier solution, but I don't think the tradeoff would have been worth it.

I do agree that @keyboardDrummer's most recent suggestion would simply things, but I don't like the idea of a breaking change only in the name of simplifying the semantics and implementation. The compilation of comprehensions can definitely be "surprising" and involve "hidden code" already, but allowing an undecidable value to be compiled at all means that there is no one simple way to map a comprehension's syntax to executable code: there will always be heuristics to decide what we accept and what we reject. The upside is a ton of flexibility for compilers to optimize, but the downside is needing to help users understand how their code will behave at runtime. I think we should spend effort in documenting how these concepts are compiled, and possibly offer more insight in tooling.

It's entirely possible that with that guidance, this work reduces not to an implementation change but to documentation changes to offer guidance on how to solve the problems this was intended to help solve. Perhaps that means we can add more positive variations on test cases that show what DOES work. If this is the case, I hope you'll agree the journey was worthwhile even if it didn't end up where you thought it would! :)

[keyboardDrummer]

allowing an undecidable value to be compiled at all means that there is no one simple way to map a comprehension's syntax to executable code: there will always be heuristics to decide what we accept and what we reject.

Could you, maybe just for my education, elaborate on the other "hidden code" scenario's? Compared to the implicit filter on subset type constraints, what are other surprising runtime operations that happen in comprehensions?

Simple examples like set x | x in xs && x > 2 or set x | 0 <= x && x <= 4 are as fast as I would expect them to be.