At every point in a proved project I’ve done, I’ve had to analyze which proofs take the most number of steps and then optimize them. There’s a gnatprove option to get what you want.
Proving between platforms on the same piece of code should behave the same, though I would advise at least building and testing on each release for macOS and Windows (I was able to uncover some hard coded UNIX paths in my code as a result).
Shameless plug but you might find my project useful, especially as your codebase grows (there’s certain niceties like spark proof coverage, status badges, dashboard etc). There is some work being done on caching gnatprove in CI for my GitHub Action, though it is more rudimentary compared to the base CLI in that regard for now.
I typically skip proofs in CI for this reason - most hosted runners just aren’t beefy enough to prove in a reasonable timeframe. One option is to just report the successful proof, something like:
gh api \
--method POST --silent \
-H "Accept: application/vnd.github+json" -H "X-GitHub-Api-Version: 2022-11-28" \
/repos/$OWNER/$REPO/statuses/$SHA \
-f "context=signoff" -f "state=success" -f "description=Signed off by $USER ($SECONDS seconds)"
but instead of “Signed off by” you could add some kind of digitally-signed artifact, a hash of the gnatprove output, perhaps, depending on your paranoia level.
Or if you wish to skip running gnatprove in CI entirely, you can always run gnatprove and commit the gnatprove.out, which can one can read from directly.
Albeit running gnatprove on one’s local machine for every git push is still not a computationally “cheap” gate.
I feel doing it on every release gives you a sensible balance there, as it reassures users while you can run gnatprove for local development.
This is not entirely true. Before SPARK 14, one had to tell the prover what the sizes of the predefined numeric types and theSystem.Min_Int, System.Max_Int, and System.Max_*_Modulus constants were to get meaningful proofs for a specific platform; something that could be proved for one platform might fail on another. So for a single proof to apply to all platforms, you have to ensure that all your numeric types have fixed sizes, regardless of platform. Effectively that means no use of the Long_* predefined types, or types declared using the System constants.
Technically, proofs can differ between those three platforms. There can be differences in the runtime, or in sizes of some predefined types. But it can be mitigated and overall it’s quite rare.
For CI use, I would suggest the use of a “file cache”. This feature is hidden behind the option —memcached-server=file:path, where “file” is a fixed string and “path” is a path on disk (yes the name is a bit awkward; no memcached server is needed for this feature). Gnatprove then saves proof results in that folder. If you save and restore it for the next CI run (typically CI have this feature to restore a cache folder), you should see important speedups.
I added a make prove-stats target (wrapping gnatprove --report=statistics for exactly that purpose). Here are the most difficult proved checks:
Check
Result
topoproof-geometry-intersections.adb:390:7
precondition proved in max 19 s
topoproof-geometry-intersections.adb:382:13
overflow check proved in max 18 s
topoproof-geometry-segment_sequences.adb:209:17
loop invariant after first iteration proved in max 16 s
topoproof-geometry-intersections.adb:331:38
overflow check proved in max 11 s
topoproof-geometry-intersections.adb:334:38
overflow check proved in max 10 s
topoproof-geometry-intersections.adb:352:12
overflow check proved in max 10 s
topoproof-geometry-intersections.adb:357:12
overflow check proved in max 7 s
topoproof-geometry-intersections.adb:82:10
postcondition proved in max 7 s
topoproof-geometry-intersections.adb:383:22
overflow check proved in max 7 s
topoproof-geometry-intersections.adb:768:10
postcondition proved in max 5 s
Max steps used for a successful proof: 81,857.
No single step stands out spectacularly for now — the hardest checks are the overflow checks in the intersections module, which is expected given the amount of arithmetic there.
I’ved knocked out a lot of steps by allowing shortcuts via proving more in long chains, instead of relying on implicitly deduced intermediary results (adidng pre/post, or adding Assert, or Assert_And_Cut). In my limited experience doing this, 82k steps is more than 10x what I normally see.
Yes, your’re right, a single check is donne in more than 70k steps and 20s.
The second is 2k steps and the third 1,6k.
It seems that CVC5 is confused on this one, Z3 is doing the job in no time.
Interesting : there is the same check twice, once on the x axis and once on the y axis. Z3 uses 1 step on both, CVC5 73k steps on one, 1 on the other.
The lazy solution proposed by GLM is to put Z3 before CVC5 in the list of the provers
I have a better view now of what is normal and what is not, thanks.
Following up on my own experiment above: I measured the “lazy solution”
instead of just assuming it. The setup: the one hard subprogram alone
(--limit-subp), clean GNATprove session (no proof cache), --timeout=30,
level 2 — 22 checks, all proved:
--prover=
Wall time
z3,cvc5,altergo
5.0 s
z3 alone
5.0 s
cvc5,z3,altergo (default)
9.2 s
cvc5 alone
9.1 s
altergo,cvc5,z3
26.8 s
So putting Z3 first does halve the cost of the hard subprogram, with no
penalty to expect elsewhere: every other check in the project is proved in
1 s or less, under either prover. Z3 alone matches Z3-first because it
settles all 22 checks of this subprogram by itself — and on the whole
project it stays the second wheel (CVC5 discharges 93–97 % of the checks),
which is exactly why the order matters: the first prover that succeeds ends
the attempt.
One sentence on what puts CVC5 on its knees: the check is a goal of
nonlinear integer arithmetic — the strict betweenness of a crossing
quotient whose bounds are cubic products of exact grid deltas — and CVC5’s
heuristics happen to explore it the hard way (73k steps on the x-axis
instance) while Z3’s arithmetic decision procedures see through it at once;
the same check costing CVC5 a single step on the y axis confirms it is
heuristic bad luck, not intrinsic hardness.
One caveat from the same table: don’t put a weak-but-fast prover in front.
altergo first burns ~24 s failing on the hard checks before CVC5 pays for
them again — worst of all orders.
Thanks for the pointer! The screenshots do look nice, but I couldn’t really figure out what impact it would have on my dev environment. I’m reluctant to install heavy machinery for my personal projects — I have no requirement to document proofs there.
My needs are actually pretty simple:
A CI status at a glance, in the README, as a badge.
A more complete status with coverage figures, in a developer-facing space.
Automatic production of cross-references — not necessarily requirements, just things like the list of FIXMEs in the source files. (For that one, I already have a plan for a small dedicated Ada utility.)
And I’d like that status to automatically take into account the results of unit tests, integration tests, bbt runs, gnatprove, etc. From what I’ve seen, you’ve worked on exactly that question.
The other point that bothers me is the dependence on GitHub for so many things. When you produce raw results but the only way to display them graphically is through GitHub’s CI, that doesn’t sit right with me.
Right now I have overly complicated Makefiles, full of greps — and with all that, I haven’t even got back to the level I was at ten years ago. Back then, for instance, I generated HTML-annotated sources with gcov or lcov, accessible from the docs, all produced locally, with no need for codecov or any other remote service.
So anything that helps me simplify things and keep my production flow local is welcome.
And if I could replace the Makefile commands with alr build / alr test on the simplest projects, that would be even better — though I don’t hold out much hope!
As much as I call it a toolchain (I hope to provide the well thought out feature set of a toolchain) I don’t want it too come with the bloat that one typically is associates with a toolchain (a.k.a a boatload of dependencies). The core CLI has no deps except Python for bundling docs and Alire + Ada stdlib. gnatprove is resolved at runtime.
CI as well as ergonomics with what the tool can provide is being worked on.
fyi, Forgejo Actions/Gitea are mostly compatible with GitHub Actions spec. I can get around to writing one and testing on an instance I self host for local dev. Codeberg’s CI however is pretty much out of reach due to their stance on AI assisted projects (yes I think one can tell just looking at the repo and the commit velocity): Protecting our FLOSS commons from LLMs — Codeberg News.
Personally I don’t like that GitHub CI is the de facto pretty much everywhere. I could stick to the workaround back in the day to interface with Alire crate publishing back in the day, though the aforementioned stance on AI among other UX headaches bring me back to GitHub. afaik as it stands the ecosystem of CI heavily favours GitHub in general, not just for Ada this is an issue with many other languages.
For the most part the CI aims to have parity with the base CLI, not the other way around. If there are CI specific quirks and features I should have in the base CLI do create a GitHub Issue and I will get around to working on it.
for instance I love golang myself, but almost all the libraries are pulled from github URLs
and quite frankly, there is still a bit to do. bbt support is something I am heavily considering adding down the road.
If that is of any help, bbt can export a JUnit-format XML file (cf. bbt issue 28 and trendy_test issue 5 for reference), and tries to help with building badges. I’m not sure the latter is done well, though — it seems to me that too much of the burden falls outside the tool, in the Makefile.
