Dafny Standard Library

[mmwinchell]

Hello everyone! For the past couple of months, we have been working on creating a standard library for Dafny. We would love to hear your feedback on our Collections and Nonlinear Arithmetic libraries. The original discussion about the Dafny standard library can be found here .

[robin-aws]

A few more comments - publishing these as I may not get to the rest, but @RustanLeino is intending to review this ASAP as well.

[robin-aws]

(meta-comment, not asking for changes here) I was about to ask if there was any attempt to use the built in nat type since there are so many x > 0 conditions here, but then I realized that nat actually defines whole numbers rather than natural numbers since it includes 0. :(

Ignoring that for the moment, I assume that trying to use any subset types in all of this would destabilize the proofs and be a lot of work?

[sarahc7]

This makes sense for what we have right now, but we might want to extend DivMod.dfy to support negative numbers in the future.

[RustanLeino]

I'm sending these comments for now. In addition, I have two general remarks:

• I don't know the BSD-2 license, but if I'm using Dafny, I assume familiarity with the MIT License. I'm guessing BSD-2 is used because some of the standard library originated in VeriBetrFS. However, if there's no strong reason to use BSD-2, then it would be easier if we could stay with just the MIT License.
• We should not have any explicit triggers in the library. Users of the library will mimic its style, and triggers are terribly confusing to most users, especially new users. It would be terrible if the library has the effect of encouraging users to write :trigger annotations that they don't understand. Dafny does a good job in selecting triggers automatically (which you can see from the hover text in the IDEs). If Dafny does this incorrectly, the best recourse is to file a bug and improve Dafny. Please, no explicit triggers.

[parno]

@robin-aws Thanks again for all of the detailed feedback! It's great to have more people thinking about this.

@RustanLeino Re: BSD-2, yes that was added as a result of pulling in files developed as part of VeriBetrFS (

libraries/LICENSE

Line 26 in 3fe33d3

1) BSD-2 License: https://github.com/vmware-labs/verified-betrfs/blob/master/LICENSE.txt

). I'm not an expert on open source licenses, but StackOverflow (clearly a reputable source of legal advice) says (https://opensource.stackexchange.com/a/582):

So what both the 2-clause BSD license and the MIT license have in common are:

Permits use
Permits redistribution
Permits redistribution with modification
Provision to retain the copyright notice and warranty disclaimer
In addition the MIT license also explicitly allows:

merging
publishing
sublicensing
selling
However, all these freedoms are implied by the BSD license, because all these activities can be considered "use" and/or "redistribution" of the software.

The practical differences between the 2-clause BSD license and the MIT license are marginal. Which one to pick is mostly up to personal taste.

Since we know the VeriBetrFS folks quite well, we could potentially talk to them about relicensing the relevant files. I don't know if that will be problematic for the VMware members of VeriBetrFS.

[parno]

@RustanLeino Re: triggers: Our experience has been that carefully chosen, conservative triggers are quite important for making verification scale. I agree that new Dafny users shouldn't have to write their own triggers, but in a standard library, we have the luxury of the collective wisdom of Dafny expert users, so it seems like an opportunity to use that to ensure the quantifiers in the standard library don't result in bad performance for users of the library, who may find it challenging to identify the problem, and even if they do, won't be able to easily change the standard library to make it more conservative.

As a concrete example, given forall x :: x in m ==> x in m' && m'[x] == m[x], we chose a trigger of m'[x], which is the most likely to be relevant for subsequent proof steps. Dafny chooses the more liberal trigger set of {m[x]}, {m'[x]}, {x in m'}, {x in m}. This seems fine in the average case, but may lead to slow performance in larger developments.

As another concrete example in the other direction, if we strip the triggers from the Nonlinear library, many of the lemmas no longer go through.

Perhaps we could add something to the README telling readers that triggers are an advanced topic, and not something to worry about if you're just starting with the language?

[Chris-Hawblitzel]

@RustanLeino Just to add to what Bryan said about triggers, I agree that in cases where Dafny chooses good triggers in the first place, it's redundant clutter to have manual triggers that tell Dafny to do what it would have done anyway. But in places where programmers have already carefully selected better triggers than Dafny did, I wouldn't want to throw them out. I've found manual triggers to be essential for efficiency in some places where Dafny chooses triggers that lead to too many quantifier instantiations. For example, I recently had to maintain some proofs for the Ironfleet project. Here is one of the problematic quantifiers I encountered that was causing a proof to time out:

        ensures  forall i :: 0 <= i < |replica_order| ==> 
                 AbstractifyConcreteReplicas(replicas, replica_order)[i] == replicas[replica_order[i]].sched;

Here, the author intended this quantifier to provide information about AbstractifyConcreteReplicas(replicas, replica_order)[i] for all i, so this term is the only appropriate term to use as a trigger. The automatic trigger selection algorithm, though, doesn't know what the authors' intentions are, and adds a second trigger, replica_order[i]. This second trigger causes the timeout in a proof that uses the ensures clause. The fix is a manual trigger:

        ensures  forall i {:trigger AbstractifyConcreteReplicas(replicas, replica_order)[i]} :: 0 <= i < |replica_order| ==> 
                 AbstractifyConcreteReplicas(replicas, replica_order)[i] == replicas[replica_order[i]].sched;

Often, we only add manual triggers as a last resort when we find that proofs are slow. In this case, though, it was painful to diagnose the performance issue in someone else's proof. I would have rather that the authors wrote their intended trigger in the first place.

[jonhnet]

Rustan, I generally agree with your intuition: As someone who's committed to not thinking about triggers, I teach students four methods for responding to timeouts, none of which involve thinking about triggers. However, the standard library seems like it's in the inner circle along with dafny itself; it should be allowed to work necessary magic to better balance automation with timeout protection. What if, not just in the README but in front of every line with a {:trigger}, we add a boilerplate comment that says: ":trigger is an advanced automation control. Avoid its use in user code. Professional drivers on a closed track" to discourage cargo cult programming?

Dafny does a good job in selecting triggers automatically

It does when it does, which is 99% of the time. But we've learned in big projects that the other 1% is a limiting factor for development scale. This is a bit of a derail, but we need better tooling for diagnosing and correcting timeouts; the current situation is a significant hurdle for Dafny's growth.

[RustanLeino]

@parno @Chris-Hawblitzel @jonhnet Thank you for your valuable comments about triggers. It seems we share the intent of using manual triggers only when there's good reason to believe the manual one does better. I like the idea of adding some comment about triggers being an advanced feature (e.g., in the README file). It would then be nice if each manual trigger is accompanied with a comment like those you used in your replies above. (E.g., "Here, Dafny would pick ..., but the intent of the quantifier is ..., so this quantifier is manually given the stricter trigger ...".)

[robin-aws]

Thank you so much for this exciting contribution @mmwinchell @sarahc7 and @parno! This is really going to improve the experience when creating a new codebase in Dafny. I'm going to go add it to my favourite Dafny codebase right now. :)

[parno]

Thanks very much for all of the thoughtful feedback and help landing this PR!

And thanks @robin-aws for helping track the remaining issues.