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.
