libraries

Libraries useful for Dafny programs

This is a fork of dafny-lang/libraries with variance declarations on type parameters removed, and which therefore supports compilation to Java despite dafny-lang/dafny#2013.

Status

At the moment, we're just collecting generally useful Dafny code.

Once we have some amount of code which is used successfully by several projects, we might restructure this repo, informed by the concrete use cases.

So, please do use this library, give feedback, and contribute code, but also expect breaking changes.

Contributions

Any contributions of generally useful code are welcome, just open a pull request! Please follow the library style guidelines. If the way to use your new code is not obvious, please add some examples in the examples directory to illustrate how to use the code. We use the LLVM integrated tester (lit) to test the library files and ensure they all verify correctly. Please see Dafny's documentation on installation and testing for more details.

Acknowledgements

Much of this code came from or was inspired by code from the following projects:

• Ironclad Apps
• IronFleet
• Vale
• Verified BetrFS
• Verifying OpenTitan