This project contains definitions and lemmas that are generally useful to any verification project using Gobra.
Currently, the project contains packages to reason about sets (sets), sequences (seqs), maps in Go (gomaps), and mathematical maps (dicts), but we hope to gradually increase its functionality.
We draw inspiration from multiple sources, including dafny-lang/libraries, vstd, and the Why3 standard library. Furthermore, this library builds on top of utility packages originally developed for diverse verification projects, e.g., VerifiedSCION and viperproject/program-proofs-gobra.
This project was originally developed as a Practical Work project by Daniel Nezamabadi at ETH Zurich. You can find more details about it in the report.
The goal of this project is to make it easy to maintain and re-use common definitions across different verification projects that use Gobra. If you find yourself re-using definitions between projects, or if you develop libraries that might benefit others, please consider contributing.