hmijail
commented
1 month ago Question 3 is probably the most pressing, since that would affect the usefulness of --isolate-assertions and the strategies to use it.
Open hmijail opened 1 month ago
hmijail
commented
1 month ago Question 3 is probably the most pressing, since that would affect the usefulness of --isolate-assertions and the strategies to use it.
keyboardDrummer
commented
1 month ago 1) Given that these functions are transparent, shouldn't cheap() end up being equivalent to expensive()?
Your examples are bit large. Any chance you could simplify them to make it easier to answer your questions?
2) Given that --isolate-assertions breaks expensive() down to ABs, shouldn't the verification of those ABs be cheaper
Yes but only in general. There may still be one AB that is (almost) as expensive as the whole. I'm working on a PR that will hopefully make --isolate-assertions more effective though.
3) Question 3 is probably the most pressing, since that would affect the usefulness of --isolate-assertions and the strategies to use it.
Does the following example answer your question?
function Foo() {
assert false; // Always fails
assert false; // This assertion never fails because the previous one establishes false,
// regardless of whether you're using `--isolate-assertions` or not
}4) P() shows a couple of commented-out && assert {:split_here} true that partition the function just like the smaller functions did for P1(). Indeed, this improves verification of P(). If the only reason to extract those smaller functions is to ease verification, is it then equivalent to use split_here?
Note that if you're already using --isolate-assertions, then adding splits shouldn't have any positive effect. Also, splits will only affect the verification where they are placed, so adding splits to functions will only makes verifying the wellformedness of that function easier, but won't affect callers of that function.
One more thing to note is that we're adding hide statements as an easier to use, and more performant version of {:opaque}: https://github.com/dafny-lang/dafny/pull/5562
But it's still work on progress.
Dafny version
4.7
Code to produce this issue
Command to run and resulting output
What happened?
Consider the function expensive(). Its verification times out with over 50M Resource Units. To try to tackle it, I tried using --isolate-assertions. Some of the resulting Assertion Batches still timed out over 50M.
Separately I tried manually breaking down expensive() into smaller functions, and then invoking them all inside of cheap(). Turns out that cheap() verifies with <200K RU - over 2 orders of magnitude better. But I don't understand what could cause such a big difference.
I understand that there is a degree of randomness here because of both how the Assertion Batches are constructed, and of what the solver might "discover" while working without isolated assertions. But apart from that, I wonder if I'm missing something more fundamental, hence these questions:
assume false, right? Therefore, will AB 6 (and subsequent ones) be "poisoned" by this?&& assert {:split_here} truethat partition the function just like the smaller functions did for P1(). Indeed, this improves verification of P(). If the only reason to extract those smaller functions is to ease verification, is it then equivalent to use split_here?What type of operating system are you experiencing the problem on?
Mac