I am pleased to announce the first release of marble, a Rocq library whose purpose is to make it easier to work comfortably with Rocq’s primitive integers and primitive arrays.
It offers a simple Hoare logic that helps write and verify code that uses integers, arrays, and array-based data structures.
It offers ready-made support for loops of various kinds, a range of operations on arrays, as well as two array-based data structures, namely vectors and priority queues.
It is available now via opam install rocq-marble.
In the future, I am hoping/planning to include more data structures and algorithms.