I’m happy to announce Rocq-bottom, a new Rocq library of formally verified abstract domains, currently targeting non-relational integer abstractions. The library currently provides formally verified Intervals, Congruences, and Known Bits abstractions, some of their reduced products, together with transfer functions and refinement operators for integer expressions.
It can show, for instance, that
- Z.lor [3,5] [4,5] ∈ [4,7],
- Z.add 0b001? + 0b001? ∈ 0b01??,
- for the problem x * y = 10 with 3 ≤ x ≤ 10, 1 ≤ y ≤ 10, backward multiplication can tighten the bounds to 5 ≤ x ≤ 10 and 1 ≤ y ≤ 2.
The goal of this development is not only to prove that the algorithms it contains are sound, but also that they are best (e.g., the intervals above are the tightest). All of this is developed in constructive logic, without any extra axiom. The theoretical foundations are described in the paper Rocq Bottom: Beyond Soundness with Precise Reasoning about Analysis Precision, to be published at SAS this year.
In addition, the algorithm should be efficient and practical, so that they can be integrated easily in static analyzers.
The development has reached an important first milestone, as we now have best forward and backward transfer functions over unbounded integer intervals for all the C-like integer operators (Z.add, Z.sub, Z.mul, Z.quot, Z.rem, Z.shiftl, Z.shiftr, Z.land, Z.lor, Z.lxor, Z.eqb, Z.leb, Z.ltb).
The next steps are to develop best transfer functions for the products Interval × Congruence, Interval × Congruence × Known Bits, and then build on that to build bitvector abstractions.
I’m new to Rocq and the development can probably be improved in many ways. I’d love to hear your thoughts, feedback, or suggestions!