Skip to content
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.

Sign up for GitHub

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

Jump to bottom

feat: Allow forall statements in statement expressions #5894

Merged
merged 16 commits into from
Dec 1, 2024
Merged

feat: Allow forall statements in statement expressions #5894

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
31f2136
Improve code and comments
RustanLeino Nov 4, 2024
414c4c1
Make test run with both resolvers
RustanLeino Nov 4, 2024
6f97e14
Allow forall statements in statement expressions
RustanLeino Nov 4, 2024
216b63a
Deprecate forall statements with parenthesized bound variables
RustanLeino Nov 4, 2024
2921cd4
Update documentation
RustanLeino Nov 4, 2024
fd7ea46
Add release notes
RustanLeino Nov 4, 2024
ace95ab
Fix deprecated parentheses in standard library
RustanLeino Nov 4, 2024
463a5f6
Adjust tests
RustanLeino Nov 4, 2024
137f3ad
Merge branch 'master' into forall-stmt-in-expr
RustanLeino Nov 7, 2024
2e60809
Merge branch 'master' into forall-stmt-in-expr
RustanLeino Nov 7, 2024
1ede1ce
Move deprecation tests to Deprecation.dfy
RustanLeino Nov 7, 2024
e191c36
Rename Parallel* test files to ForallStmt*
RustanLeino Nov 7, 2024
1dbad1b
Applying renaming in test files
RustanLeino Nov 7, 2024
81ca722
Merge branch 'master' into forall-stmt-in-expr
RustanLeino Nov 14, 2024
0923ee9
Merge branch 'master' into forall-stmt-in-expr
RustanLeino Nov 27, 2024
4f79e30
Merge branch 'master' into forall-stmt-in-expr
RustanLeino Dec 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using JetBrains.Annotations;

namespace Microsoft.Dafny;

Expand Down Expand Up @@ -36,7 +37,7 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr
}

/// <summary>
/// Map a list of quantified variables to an eqivalent list of bound variables plus a single range expression.
/// Map a list of quantified variables to an equivalent list of bound variables plus a single range expression.
/// The transformation looks like this in general:
///
/// x1 <- C1 | E1, ..., xN <- CN | EN
Expand All @@ -48,7 +49,7 @@ public QuantifiedVar(IToken tok, string name, Type type, Expression domain, Expr
/// Note the result will be null rather than "true" if there are no such domains or ranges.
/// Some quantification contexts (such as comprehensions) will replace this with "true".
/// </summary>
public static void ExtractSingleRange(List<QuantifiedVar> qvars, out List<BoundVar> bvars, out Expression range) {
public static void ExtractSingleRange(List<QuantifiedVar> qvars, out List<BoundVar> bvars, [CanBeNull] out Expression range) {
bvars = new List<BoundVar>();
range = null;

Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/AST/Grammar/ParseErrors.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,7 @@ public enum ErrorId {
p_no_decreases_expressions_with_star,
p_assert_needs_by_or_semicolon,
p_deprecated_forall_with_no_bound_variables,
p_deprecated_forall_statement_with_parentheses_around_bound_variables,
p_forall_with_ensures_must_have_body,
p_deprecated_modify_statement_with_block,
p_calc_operator_must_be_transitive,
Expand Down
78 changes: 48 additions & 30 deletions Source/DafnyCore/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3091,36 +3091,45 @@ RevealStmt<out Statement s>
.

/*------------------------------------------------------------------------*/
ForallStmt<out Statement/*!*/ s>
ForallStmt<out Statement s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x = Token.NoToken;
List<BoundVar> bvars = null;
Attributes qattrs = null;
Expression range = null;
var ens = new List<AttributedExpression/*!*/>();
IToken startToken = null;
BlockStmt block = null;
IToken bodyStart, bodyEnd;
IToken tok = Token.NoToken;
.)
"forall" (. x = t; tok = x; startToken = t; .)
"forall" (. startToken = t; .)

( IF(la.kind == _openparen) /* disambiguation needed, because of the possibility of a body-less forall statement */
"(" [ QuantifierDomain<out bvars, out qattrs, out range, true, true, true> ] ")"
| [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */
QuantifierDomain<out bvars, out qattrs, out range, true, true, true>
]
"(" (. errors.Deprecated(ErrorId.p_deprecated_forall_statement_with_parentheses_around_bound_variables, t,
"parentheses around the forall-statement bound variables are deprecated and not needed");
.)
[ QuantifierDomain<out bvars, out qattrs, out range, true, true, true> ]
")"
| [ IF(IsIdentifier(la.kind)) /* disambiguation needed, because of the possibility of a body-less forall statement */
QuantifierDomain<out bvars, out qattrs, out range, true, true, true>
]
)
(. if (bvars == null) errors.Deprecated(ErrorId.p_deprecated_forall_with_no_bound_variables, startToken, "a forall statement with no bound variables is deprecated; use an 'assert by' statement instead");
if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
(. if (bvars == null) {
errors.Deprecated(ErrorId.p_deprecated_forall_with_no_bound_variables, startToken,
"a forall statement with no bound variables is deprecated; use an 'assert by' statement instead");
}
bvars ??= new List<BoundVar>();
.)

ForallStatementEnsuresAndBody<out s, startToken, bvars, qattrs, range>
.

ForallStatementEnsuresAndBody<.out Statement s, IToken startToken, List<BoundVar> bvars, Attributes qattrs, Expression/*?*/ range.>
= (. var ens = new List<AttributedExpression/*!*/>();
BlockStmt block = null;
range ??= new LiteralExpr(startToken, true);
.)
{
EnsuresClause<ens, true>
}
[ IF(la.kind == _lbrace) /* if the input continues like a block statement, take it to be the body of the forall statement; a body-less forall statement must continue in some other way */
BlockStmt<out block, out bodyStart, out bodyEnd>
BlockStmt<out block, out _, out _>
]
(. if (theOptions.DisallowSoundnessCheating && block == null && 0 < ens.Count) {
SemErr(ErrorId.p_forall_with_ensures_must_have_body, t, "a forall statement with an ensures clause must have a body");
Expand Down Expand Up @@ -3994,7 +4003,7 @@ MapComprehensionExpr<out Expression e, bool allowLemma, bool allowLambda, bool a
bool finite = true;
.)
( "map" | "imap" (. finite = false; .) ) (. IToken mapToken = t; .)
QuantifierDomain<out bvars, out attrs, out range, allowLemma, allowLambda, allowBitwiseOps>
QuantifierDomain<out bvars, out attrs, out range, true, true, true>
QSep
Expression<out bodyRight, allowLemma, allowLambda, allowBitwiseOps>
[ IF(IsGets()) /* greedily parse ":=" */ (. bodyLeft = bodyRight; .)
Expand All @@ -4019,7 +4028,8 @@ EndlessExpression<out Expression e, bool allowLemma, bool allowLambda, bool allo
| QuantifierExpression<out e, allowLemma, allowLambda> /* types are such that we can allow bitwise operations in the quantifier body */
| SetComprehensionExpr<out e, allowLemma, allowLambda, allowBitwiseOps>
| StmtInExpr<out s>
Expression<out e, allowLemma, allowLambda, allowBitwiseOps> (. e = new StmtExpr(s.Tok, s, e) { RangeToken = new RangeToken(s.StartToken, e.EndToken) }; .)
Expression<out e, allowLemma, allowLambda, allowBitwiseOps>
(. e = new StmtExpr(s.Tok, s, e) { RangeToken = new RangeToken(s.StartToken, e.EndToken) }; .)
| LetExpression<out e, allowLemma, allowLambda, allowBitwiseOps>
| MapComprehensionExpr<out e, allowLemma, allowLambda, allowBitwiseOps>
)
Expand Down Expand Up @@ -4497,20 +4507,30 @@ QuantifierExpression<out Expression q, bool allowLemma, bool allowLambda>
List<BoundVar/*!*/> bvars;
Attributes attrs;
Expression range;
Expression/*!*/ body;
q = dummyExpr;
.)
( Forall (. x = t; univ = true; .)
| Exists (. x = t; .)
)
QuantifierDomain<out bvars, out attrs, out range, allowLemma, allowLambda, true>
QSep
Expression<out body, allowLemma, allowLambda>
(. if (univ) {
q = new ForallExpr(x, new RangeToken(x, t), bvars, range, body, attrs);
} else {
q = new ExistsExpr(x, new RangeToken(x, t), bvars, range, body, attrs);
}
.)
QuantifierDomain<out bvars, out attrs, out range, true, true, true>
( IF(univ && (la.kind == _ensures || la.kind == _lbrace))
// It's a forall statement. Parse it as part of a StmtExpr.
Copy link
Member

@MikaelMayer MikaelMayer Nov 7, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That works. It means we could theoretically do the same for if statements (last week I would have loved to have that) and I think that could be useful too and less surprising in the future, although out of scope for this PR.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree it's out of scope for this PR, but I do find it an interesting idea. I suppose such an if statement would still just be for the StmtExpr, rather than being an alternative syntax for if-then-else expressions? This would then allow you to write some proofs inside the if statement and follow that by the expression you want to return. (I have never felt the need for this myself, but perhaps only because I knew the feature wasn't available.)

Some new users confuse if-then-else expressions and if statements (which, curiously, seems not to be a confusion in languages that use the more cryptic ? : for the former). On one hand, also allowing if statements in expressions might add to that confusion. But on the other hand, maybe this would give us a place in the parser to give a better error message if the program gets this wrong.

While we're thinking about such things, one could also imagine other statements, in particular while loops, in expressions. Again, such a while statement would just be for the StmtExpr, to allow an inline proof that uses a loop.

ForallStatementEnsuresAndBody<out var forallStatement, x, bvars, attrs, range>
Expression<out var expr, allowLemma, allowLambda>
(. q = new StmtExpr(forallStatement.Tok, forallStatement, expr) {
RangeToken = new RangeToken(forallStatement.StartToken, forallStatement.EndToken)
};
.)

| QSep
Expression<out var body, allowLemma, allowLambda>
(. if (univ) {
q = new ForallExpr(x, new RangeToken(x, t), bvars, range, body, attrs);
} else {
q = new ExistsExpr(x, new RangeToken(x, t), bvars, range, body, attrs);
}
.)
)
.

/*------------------------------------------------------------------------*/
Expand Down Expand Up @@ -4584,9 +4604,7 @@ SetComprehensionExpr<out Expression q, bool allowLemma, bool allowLambda, bool a
// This production used to have its own version of QuantifierDomain in which the
// range was not optional, so we map null to "true" here so that the rest of the
// logic doesn't hit exceptions.
if (range == null) {
range = LiteralExpr.CreateBoolLiteral(new AutoGeneratedToken(t), true);
}
range ??= LiteralExpr.CreateBoolLiteral(new AutoGeneratedToken(t), true);
q = new SetComprehension(setToken, new RangeToken(setToken, t), finite, bvars, range, body, attrs);
}
.)
Expand Down
26 changes: 13 additions & 13 deletions Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivIsOrderedByDenominatorAuto()
ensures forall x: int, y: int, z: int {:trigger x / y, x / z} :: 0 <= x && 1 <= y <= z ==> x / y >= x / z
{
forall (x: int, y: int, z: int | 0 <= x && 1 <= y <= z)
forall x: int, y: int, z: int | 0 <= x && 1 <= y <= z
ensures x / y >= x / z
{
LemmaDivIsOrderedByDenominator(x, y, z);
Expand All @@ -173,7 +173,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivIsStrictlyOrderedByDenominatorAuto()
ensures forall x: int, d: int {:trigger x / d} :: 0 < x && 1 < d ==> x / d < x
{
forall (x: int, d: int | 0 < x && 1 < d )
forall x: int, d: int | 0 < x && 1 < d
ensures x / d < x
{
LemmaDivIsStrictlyOrderedByDenominator(x, d);
Expand Down Expand Up @@ -204,7 +204,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
:: 0 < d && R == a%d + b%d - (a+b)%d ==> d*((a+b)/d) - R == d*(a/d) + d*(b/d)
{
// https://github.com/dafny-lang/dafny/issues/4771
forall (a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d && R == a%d + b%d - (a+b)%d)
forall a: int, b: int, d: int, R: int {:trigger d * ((a + b) / d) - R, d*(a/d) + d*(b/d)} | 0< d && R == a%d + b%d - (a+b)%d
ensures d*((a+b)/d) - R == d*(a/d) + d*(b/d)
{
LemmaDividingSums(a, b, d, R);
Expand All @@ -224,7 +224,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivPosIsPosAuto()
ensures forall x: int, d: int {:trigger x / d} :: 0 <= x && 0 < d ==> 0 <= x / d
{
forall (x: int, d: int | 0 <= x && 0 < d)
forall x: int, d: int | 0 <= x && 0 < d
ensures 0 <= x / d
{
LemmaDivPosIsPos(x, d);
Expand All @@ -243,7 +243,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivPlusOneAuto()
ensures forall x: int, d: int {:trigger 1 + x / d, (d + x) / d} :: 0 < d ==> 1 + x / d == (d + x) / d
{
forall (x: int, d: int | 0 < d)
forall x: int, d: int | 0 < d
ensures 1 + x / d == (d + x) / d
{
LemmaDivPlusOne(x, d);
Expand All @@ -262,7 +262,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivMinusOneAuto()
ensures forall x: int, d: int {:trigger -1 + x / d, (-d + x) / d} :: 0 < d ==> -1 + x / d == (-d + x) / d
{
forall (x: int, d: int | 0 < d)
forall x: int, d: int | 0 < d
ensures -1 + x / d == (-d + x) / d
{
LemmaDivMinusOne(x, d);
Expand All @@ -280,7 +280,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaBasicDivAuto()
ensures forall x: int, d: int {:trigger x / d} :: 0 <= x < d ==> x / d == 0
{
forall (x: int, d: int | 0 <= x < d)
forall x: int, d: int | 0 <= x < d
ensures x / d == 0
{
LemmaBasicDiv(d);
Expand All @@ -299,7 +299,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivIsOrderedAuto()
ensures forall x: int, y: int, z: int {:trigger x / z, y / z} :: x <= y && 0 < z ==> x / z <= y / z
{
forall (x: int, y: int, z: int | x <= y && 0 < z)
forall x: int, y: int, z: int | x <= y && 0 < z
ensures x / z <= y / z
{
LemmaDivIsOrdered(x, y, z);
Expand All @@ -319,7 +319,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivDecreasesAuto()
ensures forall x: int, d: int {:trigger x / d} :: 0 < x && 1 < d ==> x / d < x
{
forall (x: int, d: int | 0 < x && 1 < d)
forall x: int, d: int | 0 < x && 1 < d
ensures x / d < x
{
LemmaDivDecreases(x, d);
Expand All @@ -339,7 +339,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaDivNonincreasingAuto()
ensures forall x: int, d: int {:trigger x / d } :: 0 <= x && 0 < d ==> x / d <= x
{
forall (x: int, d: int | 0 <= x && 0 < d)
forall x: int, d: int | 0 <= x && 0 < d
ensures x / d <= x
{
LemmaDivNonincreasing(x, d);
Expand Down Expand Up @@ -409,7 +409,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
ensures forall x: int, y: int, z: int {:trigger y * z, x % (y * z), y * ((x / y) % z) + x % y}
:: 0 <= x && 0 < y && 0 < z ==> 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y
{
forall (x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z)
forall x: int, y: int, z: int | 0 <= x && 0 < y && 0 < z
ensures 0 < y * z && x % (y * z) == y * ((x / y) % z) + x % y
{
LemmaBreakdown(x, y, z);
Expand All @@ -428,7 +428,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
lemma LemmaRemainderUpperAuto()
ensures forall x: int, d: int {:trigger x - d, d * d} :: 0 <= x && 0 < d ==> x - d < x / d * d
{
forall (x: int, d: int | 0 <= x && 0 < d)
forall x: int, d: int | 0 <= x && 0 < d
ensures x - d < x / d * d
{
LemmaRemainderUpper(x, d);
Expand Down Expand Up @@ -627,7 +627,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
ensures forall x: int, y: int, z: int {:trigger x * (y / z), (x * y) / z}
:: 0 <= x && 0 < z ==> x * (y / z) <= (x * y) / z
{
forall (x: int, y: int, z: int | 0 <= x && 0 < z)
forall x: int, y: int, z: int | 0 <= x && 0 < z
ensures x * (y / z) <= (x * y) / z
{
LemmaMulHoistInequality(x, y, z);
Expand Down
Loading