Liquid types in Ada and SPARK...

[rod-chapman]

A possibly useful source of reference and background info for you: a very similar facility (called "dynamic subtype predicate") has existed in Ada since the 2012 revision of the language. It is fully implemented in GCC. Support for static verification (also using Z3, CVC4, but via with Why3 infrastructure) also exists in the SPARK Ada subset and verification tools.

You could learn a lot from all that work.

[fan-tom]

Thank you @rod-chapman for these references! How did you find this project, I almost abandoned it since faced troubles with precise handling branching and loops, could you suggest me what can I read about how to infer loop invariants (if it is possible at all)?

[rod-chapman]

The project was brought to my attention by Alastair Reid at Google Research. He has been keeping close track of projects doing verification with Rust.

Inference of loop invariants is still a hard problem. I know of a few teams that have tried it, but I don't know of any significant success.

[alastairreid]

An incomplete but useful thing to consider for loop invariants is to use a 'guess and check' approach where you first guess a possible invariant and then use SMT to check whether it holds.

This paper describes an approach (that I have not personally tried) where the guessing part works like this:

1. Gathering some data from an actual run. Which might result in x,y pairs such as 1,3 2,6 3,9.
2. Using linear algebra to produce a guessed invariant "y = 3 * x"

This looks so simple that I keep hoping for an excuse to implement it myself.
There may be more recent papers with improvements - worth doing at least a shallow search if you think this is promising.