-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Subset types fully accepted in comprehensions #1702
base: master
Are you sure you want to change the base?
Conversation
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";
} |
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
} |
I have a question here. |
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 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 lhs0, lhs1, ... := M(...); In this statement, there is only one RHS and it is a method call, and there are as many LHSs as The two possibilities above look syntactically identical if there is one LHS and one RHS, and the RHS has the form lhs := P(...); If |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is the additional isGhost
parameter to VarDeclStmt
really needed? More to the point, does it do the right thing?
Source/Dafny/Dafny.atg
Outdated
@@ -2730,7 +2730,7 @@ VarDeclStatement<.out Statement/*!*/ s.> | |||
} else { | |||
update = new UpdateStmt(assignTok, endTok, lhsExprs, rhss); | |||
} | |||
s = new VarDeclStmt(x, endTok, lhss, update); | |||
s = new VarDeclStmt(x, endTok, lhss, update, isGhost); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Source/Dafny/AST/DafnyAst.cs
Outdated
|
||
/// <summary> | ||
/// Set, map, forall and exists comprehensions's range can be typed in two ways. | ||
/// When in a non-ghost context (defautl), bounds variables in the range have to be typed |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(defautl)
--> (default)
Test/git-issues/git-issue-1604g.dfy
Outdated
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
I just reached a fantastic milestone. All the tests are now passing. |
Can you give an example where a compilable body constrains Actually, could you add a few examples to the PR description if what will now be allowed that previously was not allowed? |
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -1061,6 +1065,30 @@ public enum AutoInitInfo { MaybeEmpty, Nonempty, CompilableValue } | |||
} | |||
} | |||
|
|||
// Returns true if it's possible to check that a value has this type at run-time. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you, as a follow-up PR, move all the Microsoft.Dafny.Type
related types out of DafnyAst.cs ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's a good idea for a refactoring. I can even apply @cpitclaudel 's trick to duplicate the file and thus keep the history.
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -1061,6 +1065,30 @@ public enum AutoInitInfo { MaybeEmpty, Nonempty, CompilableValue } | |||
} | |||
} | |||
|
|||
// Returns true if it's possible to check that a value has this type at run-time. | |||
public bool IsCompilable() { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 newtype
s need because their constraint does not need to be checked at run-time.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
Test/git-issues/git-issue-1604.dfy
Outdated
var x: set<Cell> := getOriginalSet(); | ||
var b := true; | ||
|
||
// This line should work because c should be of type Cell as the constraint is not compilable |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
// 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
?
Source/Dafny/AST/DafnyAst.cs
Outdated
return otherType != null && !otherType.Equals(Type, true); | ||
} | ||
|
||
private Type otherType = null; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you put fields at the top of the type declaration? Also, what is the meaning of otherType? Could you add a comment?
function method g(n: CompiledNat): int { n } | ||
|
||
// Here n is inferred to be an int and the constraint for f fails. | ||
const m := set x | n in {-1, 0, 1, 2} && f(n) >= 1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this be set n
?
function method g(n: CompiledNat): int { n } | ||
|
||
// Here n is inferred to be an int and the constraint for f fails. | ||
const m := set x | n in {-1, 0, 1, 2} && f(n) >= 1 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What happens if you explicitly type n
to GhostNat
?
docs/DafnyRef/Topics.md
Outdated
### 23.2.1. Subset types | ||
|
||
[Subset types](#sec-subset-types) | ||
Most of the time, subset types are carrying extra constraints so, unless it is trivial to infer them, only their base type is inferred, and the verifier checks the constraints. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
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. |
docs/DafnyRef/Topics.md
Outdated
@@ -10,6 +10,31 @@ TO BE WRITTEN | |||
|
|||
TO BE WRITTEN | |||
|
|||
### 23.2.1. Subset types |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll update the documentation, thanks for pointing this out.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 ofQ
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 ifC
holds, whereas the second one having not necessarily compatible types will need to checkQ(t)
for everyt
.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 sinceC
enforce it. However, this mechanism might be very hard to enforce. Currently, because when the predicates are compilable, the type oft
int in setOfTp && C
is inferred by the resolver to beTQ
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We might want to keep this change for a big version change as a separate PR
Sounds good. Thanks for explaining!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Source/Dafny/Resolver.cs
Outdated
@@ -2669,7 +2669,7 @@ public class ModuleBindings { | |||
scope.PushMarker(); | |||
var added = scope.Push(dd.Var.Name, dd.Var); | |||
Contract.Assert(added == Scope<IVariable>.PushResult.Success); | |||
ResolveExpression(dd.Constraint, new ResolveOpts(new CodeContextWrapper(dd, true), false)); | |||
ResolveExpression(dd.Constraint, new ResolveOpts(new CodeContextWrapper(dd, true), false, true /*Wish: use explicit "ghost" or "compiled" to set this flag?*/)); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please resolve the Wish. I think it's OK like it is. You could consider replacing true
with isSpecification: true
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Source/Dafny/Resolver.cs
Outdated
@@ -14520,22 +14586,29 @@ public class ResolveOpts { | |||
public readonly bool isReveal; | |||
public readonly bool isPostCondition; | |||
public readonly bool InsideOld; | |||
public readonly bool isSpecification; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it also be possible to instead of introducing the parameter isSpecification
to wrap the codeContext using new CodeContextWrapper(codeContext, isGhostContext: true)
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That sounds like a good idea, I did not see there was a CodeContextWrapper until now. Let me try
Source/Dafny/AST/DafnyAst.cs
Outdated
return otherType != null && !otherType.Equals(Type, true); | ||
} | ||
|
||
private Type otherType = null; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How do you feel about letting
CompilableType
andOriginalType
use a backing field, and implementingType
usingType => CurrentTypeAssumedToBeCompilable ? CompilableType : OriginalType
?
OriginalType
could usetype
as its backing field.
Thanks! That was helpful. I implemented it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
(testgit-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.
Source/Dafny/Resolver.cs
Outdated
// No need to add other constraints, the verifier will take care of that. | ||
return true; | ||
} | ||
resolver.ConstrainSubtypeRelation(t, u.GetCompilableParentType(), errorMsg, true); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -2788,6 +2813,9 @@ public class MapType : CollectionType { | |||
return Domain.MayInvolveReferences || Range.MayInvolveReferences; | |||
} | |||
} | |||
public override bool DoesNotContainGhostConstraints() { | |||
return Range.DoesNotContainGhostConstraints() && Domain.DoesNotContainGhostConstraints(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this covered in the tests?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
?
Source/Dafny/AST/DafnyAst.cs
Outdated
@@ -2684,6 +2706,9 @@ public abstract class CollectionType : NonProxyType { | |||
return Arg.MayInvolveReferences; | |||
} | |||
} | |||
public override bool DoesNotContainGhostConstraints() { | |||
return Arg.DoesNotContainGhostConstraints(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this covered in the tests?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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)
@@ -0,0 +1,15 @@ | |||
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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'.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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')
Source/Dafny/AST/DafnyAst.cs
Outdated
AsSubsetType: SubsetTypeDecl | ||
{ | ||
IsConstraintCompilable: false, | ||
constraintInformation: ConstraintInformation(_, var constraintReason, var constraintLocation) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@@ -0,0 +1,20 @@ | |||
git-issue-1604f.dfy(38,8): Error: Could not prove that the bound variable 'f' satisfies the (non runtime testable) type SpecialFruit after the range, where it's assumed to be of type Fruit based on inferred bounds. | |||
git-issue-1604f.dfy(16,31): [Related location] The constraint of SpecialFruit 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') | |||
git-issue-1604f.dfy(38,40): Error: possible violation of function precondition. Careful: variable f has type Fruit and not SpecialFruit because the range is compiled and SpecialFruit cannot be tested at run-time |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So, why don't we get an error about a precondition violation?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess you're overwriting the error message from line 5737:
string errorMessage = CustomErrorMessage(p.Attributes);
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
docs/DafnyRef/Topics.md
Outdated
const s: set<nat> := {1, 2, 3} | ||
type NonNegative = x | x > 0 witness 1 | ||
|
||
// not only x > 0 will be tested, but also x >= 0 (from nat) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm surprised. Why would x >= 0
from nat be tested? The source collection s
already contains nat
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
docs/DafnyRef/Topics.md
Outdated
@@ -34,6 +34,20 @@ const m := set x | n in {-1, 0, 1, 2} && f(n) >= 1 | |||
const m := set x | n in {-1, 0, 1, 2} && g(n) >= 1 | |||
``` | |||
|
|||
A special case to be aware of: if the type in the comprehension differs from the collection, | |||
but both are compilable, the type of the comprehension will be fully tested, which could be viewed as a performance problem if only one specific trait needed to be tested. For example: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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:"
@@ -5497,7 +5497,7 @@ public class XConstraint { | |||
return true; | |||
} | |||
|
|||
resolver.ConstrainSubtypeRelation(collectionElementType, requestedVariableType.GetCompilableParentType(), errorMsg, true); | |||
resolver.ConstrainSubtypeRelation(requestedVariableType.GetCompilableParentType(), collectionElementType, errorMsg, true); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should a test be added for this change as well?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@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. |
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
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). |
# Conflicts: # RELEASE_NOTES.md # Source/Dafny/AST/DafnyAst.cs # Source/Dafny/Resolver.cs # Source/Dafny/Verifier/Translator.cs
I'm sorry but I don't follow. What does it matter if I add additional constraints to The below program does not test 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);
} |
I assume you meant 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 |
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:
|
Not sure if this makes sense, but would it be possible to rewrite comprehensions to avoid having to switch the type of 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."
} |
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. |
scope.PushMarker(); | ||
ScopePushBoundVarsWithoutAssumptions(e); | ||
if (e.Range != null) { | ||
WithoutReporting(() => { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What creates the duplication between line 15305-15307 and 15296-15298 ? How come we need this code twice?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
} | ||
|
||
/// Ensures ret != null ==> !ret.DoesNotContainGhostConstraints() && ret is one of the type of e.AllBoundVars[i] | ||
private void ScopePushBoundVarsAssumingCompilable(ComprehensionExpr e, ResolveOpts opts, [CanBeNull] ResolveTypeOption resolveTypeOption = null) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
It's very hard to compare "user benefit" on the same scale as "the weight of having it in the codebase".
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".
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)
These are not "surprises", every part is necessary for the whole thing to work as-is.
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.
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: 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
This is because it believes it has to find a trigger for q as well, which of course it can't. |
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 ? |
Nice.
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 |
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 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 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). |
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 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! :) |
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 |
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:are no longer errors.
This PR completely lifts the restriction that map comprehensions, set comprehensions and quantifier expressions iterate only on runtime-testable types.
Recent updates
High-level summary of changes
Resolver and verifier
For any comprehension (map, set, quantifiers) over a bound variable:
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 3c
is of typeA
(assumingtype GA = a : A | ghostconstraint(a)
) fore.Range
but it'sGA
fore.RangeIsGhost
, and in 4c
is of typeGA
in any case. Moreover, after resolution, the type of the bound variablec
will beA
and its secondaryType will beGA
, but that's only as a convention as this type is not used further since the identifiers have their own types: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.
set c: CompiledEvenCell | …
, where the resolver has figured out that typeCompiledEvenCell
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 typeCompiledEvenCell
. The compiler will emit code that tests each candidatec
value to be aCompiledEvenCell
before it evaluates the body of the comprehension. (By “candidate values”, I mean the values that the comprehension expression’sBoundedPool
will produce. For example, if theBoundedPool
discovers bounds0 <= c < 100
, then the candidate values are the first 100 numbers, and if the BoundedPool discoversc in S
, then the candidate values are the values in the setS
.)set c: GhostEvenCell | …
, where theGhostEvenCell
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:GhostEvenCell
, then everything is fine. For example, if theBoundedPool
discoversc in S
whereS
has typeset<GhostEvenCell>
, then everything is fine. Then, the compiler emits code that evaluates the body of the comprehension for every candidate value.T
that is not a subtype ofGhostEvenCell
, 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 everyT
value (as if bound variablec
could have been declared to have typeT
) and (b) everyT
value that satisfies the body is in fact aGhostEvenCell
. If the verifier is able to check this, then the comprehension is allowed and the compiler can useT
as the static type of the bound variable used in the emitted codeBreaking changes:
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.