Epic: Verification Durability #1582
Labels
part: verifier
Translation from Dafny to Boogie (translator)
priority: not yet
Will reconsider working on this when we're looking for work
Comments
This was referenced Dec 2, 2021
robin-aws
added a commit
to dafny-lang/libraries
that referenced
this issue
Mar 11, 2022
This change adds a best practice we recommend for all Dafny projects: measuring the cost of each individual verification task and setting an upper bound in CI, to guard against future verification instability (see dafny-lang/dafny#1582). This is done with two steps: 1. Add the /verificationLogger:csv parameter when invoking dafny, which outputs a CSV file with verification results. 2. Invoke the dafny-reportgenerator tool with a configured maximum cost, which will fail the build if any task's cost crosses that threshold. There are more details on the latter tool here: https://github.com/dafny-lang/dafny-reportgenerator The good news is that (at least after #36), this codebase is in good shape! :) All tasks take less than 5 seconds across a few runs, so I've set 10 seconds as the upper bound for now. I would prefer to bound the resource count instead since that is a more predictable metric, but Dafny doesn't record the resource count when splitting happens until the upcoming 3.5 release. Note that because the /verificationLogger options cause extra output, I've also changed the lit configuration to no longer assert the exact output of dafny when verifying everything. This will make the build more stable by not depending on the exact console output, as all of the code here is always expected to verify successfully.
MikaelMayer
added
the
priority: not yet
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
An important benefit of programming in Dafny is that verification is automatically baked into the development process. This means that it isn't just enough that a program verifies once: it needs to continue to verify with every change as the program evolves over time.
The nature of the Dafny verifier, however, means that code that previously verified successfully can easily fail to verify when small factors change. This includes changes to seemingly unrelated code elsewhere in a project, but also changes to the verifier itself as Dafny evolves.
The Dafny core team is tackling this issue from at least two different angles: providing ways to measure this lack of durability, and improving the verification process so that its behavior is more predictable in the face of changes. The
/verificationLogger:trxoption added in 3.3 is the first iteration on the first angle, and a short wiki with more details on how to use it effectively is in the works.Child issues/PRs:
The text was updated successfully, but these errors were encountered: