-
Notifications
You must be signed in to change notification settings - Fork 261
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
Add by
blocks to function and method calls
#5192
Comments
I feel like the readability of
This is how I'm leaning. I wonder if we could leverage the var result: nat;
opaque {
assert 0 < x;
result := f(x);
} We'd likely need an expression variant of this as well, and I'm less sure of the optimal syntax there. Perhaps: var result: nat := opaque(assert 0 < x; f(x)); |
I do like this, and it's very general. I wonder whether, if we did this, we could make it possible for any block to be opaque. That is, in addition to examples like the one above, we could say something like: if P opaque { s1 } else opaque { s2 } That could possibly introduce parsing issues, especially if |
I would think that usually you don't want to confine all the additional facts to a particular scope. For example if I have: assert preConditionOfFooCall;
var x := fooCall(a, b);
assert makeUseOfFooCallPostcondition(x) I cannot rewrite this to: opaque {
assert preConditionOfFooCall;
var x := fooCall(a, b);
}
assert makeUseOfFooCallPostcondition(x) What I would need is more like: knowing {
assert preConditionOfFooCall;
} do {
var x := fooCall(a,b);
} until {
assert makeUseOfFooCallPostcondition(x)
} The last block What I don't like about the above is how verbose it is. Alternatively, you enable a shorter syntax that only allows providing knowledge that's used for a single statement, by introducing var x := fooCall(a,b) by { // The by clause can be added at the end of a statement, like assert .. by
assert preConditionOfFooCall;
};
assert makeUseOfFooCallPostcondition(x); For expressions, we already have |
Agreed that in some cases you'd want to expose some facts from an opaque block, and I was also going to suggest supporting: opaque ensuring postConditionOfFooCall {
assert preConditionOfFooCall;
var x := fooCall(a, b);
}
assert makeUseOfFooCallPostcondition(x) That feels pretty natural given the precedent in |
What would the difference be between that and the following? assert postConditionOfFooCall by {
assert preConditionOfFooCall;
var x := fooCall(a, b);
}
assert makeUseOfFooCallPostcondition(x) The one thing I can think of is that it would allow non-ghost code. Do you have any other differences in mind? |
Allowing non-ghost code is pretty key though, if we're trying to provide a way to attach proofs to arbitrary pieces of code to prove it's well-formed/corect, without having those facts leak into the rest of the code. |
The irony :P |
Oh, yes, I entirely agree. We need to allow non-ghost code in this new feature. But if that's the only difference with |
More than that, I think at a deep level if you say For another perspective: |
One related point is that if we had That special case is probably still worth its own syntax for readability, though, so I wouldn't suggest deprecating |
Yep, that all sounds good to me. One question that raises, which comes up in the example @keyboardDrummer posted above. It seems that side effects from It also seems like this structure might generalize to expressions, as well. I'm not sure if the same syntax makes sense, but the same overall structure might. Perhaps it would also be possible to leave out the |
Having to write var x := fooCall(a,b) by { // The by clause can be added at the end of a statement, like assert .. by
assert preConditionOfFooCall;
};
assert makeUseOfFooCallPostcondition(x); Also, to make
// implicit var x;
opaque
ensuring postConditionOfFooCall[p1->a,p2->b,result->x]
ensuring postConditionOfFooCall[p1->a,p2->b,result->y]
{
assert preConditionOfFooCall;
var x := fooCall(a, b);
y := fooCall(a, b);
}
// implicit havoc x;
// implicit havoc y;
// implicit assume postConditionOfFooCall[p1->a,p2->b,result->x] && postConditionOfFooCall[p1->a,p2->b,result->y]
assert makeUseOfFooCallPostcondition(x) I think both of the above automations are not intuitive:
|
What are we missing for expressions? I feel the tree structure of expressions already enables granular control of which information is available where, with the rule that information only flows down the tree. |
Yes I don't think we want declarations to escape I do think we need an expression variant. You could almost get away with just allowing opaque blocks in the statement part of statement-expressions ( We could just support the same outer syntax in expression contexts: var x := opaque {
var y := SomeLemmaMaybe(z);
assert preConditionOfFoo;
Foo(z)
}; In other words in statement contexts you can do Yup, the |
One interesting open question for me, independent of syntax: it seems like we need some way of obtaining a value while being able to hide all the facts needed to obtain it. What about when the type of the obtained value is a subset type? Would we still retain the fact that the value satisfies the subset type predicate, for the sake of the type system? I'd actually suggest we even throw away that fact, only because then there's the option of allowing it to escape via something like var x := opaque ensuring IsOdd(x) { ... } ...given that |
Given verification is ultimately solving an SMT program, that's not fully true. AFAICT it's easy for one assertion to help satisfy another one textually above it. Even ignoring that, I think this situation is common: function Foo(x: nat): nat {
assert preconditionOfBar;
var y := Bar(x);
// preconditionOfBar is no longer needed,
// and can be noise that makes assertions from here on more expensive
assert preconditionOfArfle;
Arfle(y)
} |
That still has the downside that it would havoc any variable that it modifies, so you have to put the effect of those modifications in the ensures clause. If you also don't allow modifying variables, then it seems like it would have the same power as the current What do you have against allowing a Also, how do you compare what you mentioned versus what I mentioned before: know {
assert preConditionOfFooCall;
} during {
var x := fooCall(a,b);
} until {
assert makeUseOfFooCallPostcondition(x)
} Now there is no need to write an ensures expression to capture the modifications to
What I meant was that we should make it so that information only flows down the expression tree. This would mean that var x :=
SomeLemmaMaybe(z);
assert preConditionOfFoo;
Foo(z); Would have the same semantics as what you described var x := opaque {
SomeLemmaMaybe(z);
assert preConditionOfFoo;
Foo(z)
}; |
I too prefer that variables declared in any kind of curly braced block, in Dafny, should not escape. So I suggest we focus on solutions that would not break this nice principle. I also had suggested that in a StmtExpr function Foo(x: nat): nat {
assert h: preconditionOfBar;
var y := (reveal h; Bar(x)); // Parentheses not needed since reveal h introduces a StmtExpr
// preconditionOfBar is no longer needed but is not visible anyway, yay!
assert preconditionOfArfle;
Arfle(y)
} Assertions and requirements in functions can have labels since June 2023, I added them knowing that they would match what happens in statements and also would enable such scenario about making some facts opaque. The only problem was for methods calls, I had not suggested anything, so the above would not work if Bar and Foo were methods. An alternative, under the condition we accept that local assertions don't escape, would be to support method Foo(x: nat) returns (j: nat) {
assert h: preconditionOfBar;
var y := (reveal h; // Parentheses not needed since reveal h introduces a StmtRHS
Bar(x)); // Method call.
} That would have the benefit of looking similar to the scoped assumptions and reveal in expressions, although it might be a bit trickier to parse. I was suggested also that we could declare a variable "opaque" (both in expressions and in statements), so that it also immediately lets user use the variable's name for revealing it. My original proposal was to use "opaque" as a wrapper of expressions but it would require to introduce a label anyway like "opaque h: expression" and would make things a bit harder to handle. |
After all of this discussion, I'm leaning in a similar direction to @MikaelMayer, I think. More specifically:
Given all that, what I'd propose we do for now is pin down the semantics of And, as for the expression forms, how about we discuss those in the context of a separate issue? |
Implemented by #5662 |
Summary
We could reduce brittleness by allowing the preconditions for a function or method call to be proved in local blocks, rather than scoped to the entire definition in which the call occurs.
Background and Motivation
Reducing verification brittleness often requires hiding information from the solver, so as to allow it to focus on the information most relevant to the current goal. The
assert ... by { ... }
construct currently allows intermediate assertions, lemma calls, and other proof steps to appear in theby
block, and the facts these steps introduce are visible only within theby
block itself and the proof obligation stating the validity of the assertion. Calls to other functions and methods are one of the most significant sources of new proof obligations, and currently cannot benefit from a similar mechanism.Proposed Feature
Extend the language so that a method call of the form
o.m(...);
could also be writteno.m(...) by { ... }
. The contents of theby
block would be used in proving that any preconditions ofm
are satisfied. This would ideally be implemented similarly to howassert ... by
is implemented.Open question: should the contents of the
by
block also be used to prove the well-formedness of the entire call expression or statement?Alternatives
Not having this feature, or something similar, limits how well we can reduce brittleness. There are a number of other things we could do that would address either some or all of the goals of this proposal, however.
We could allow a
by { ... }
block to appear on any sub-expression, which would allow proof of the preconditions for function calls but not method calls. It may be that we do this, and that function calls are handled by this more general mechanism. Even if we aim to do this for arbitrary expressions, implementing it for function call expressions may be a good place to start.We could allow specific preconditions to be opaque and named from the caller's perspective. This would allow us to write something like
assert m.Pre1 by { reveal m.Pre1; ... }; o.m(...)
. This would achieve largely the same goals, but may be more verbose. Note that both features could also co-exist. And this feature could be approximated, with no language changes, by making all preconditions in a program directly call opaque functions.We could provide a general mechanism for limiting the scope of new facts that arise from assertions, lemma calls, postconditions, etc. By placing a call within a more limited scope, it would be possible to prove any side conditions of it in such a way that they don't impact other proofs outside of the block.
The text was updated successfully, but these errors were encountered: