Simple automation for signed inequalities.

[scuellar]

In array_inequlities I propose a strategy to solve signed inequalities without overflow. Luckily, there should not be any overflow in any signed arithmetic generated by LLVM. The idea is straight forward:

1. Translate the signed bit vector inequalities into Z inequalities, using modulo arithmetic.
2. Remove the module (with the subgoal that there is no overflow)
3. Solve the inequality in the Z world
4. Your subgoals are signed bit vector inequalities, rinse and repeat.

The current file shows just a prototype of what can be achieved, but it does remove a lot of the burden from the prover. I leave it to discussion if this is a worthwhile direction.

The benefits of this strategy are as follows:

• If the tactic fails, the unproven goal will be a proof that something doesn't overflow. You probably forgot to add that invariant!
• This can easily be extended to support unsigned bit vectors, for cases without overflow. You can further support overflow if you do some magic with the modulo arithmetic, but this part will be trickier.
• It is relatively simple, and only relies on the well supported lia for Zs.
• It should support all vector lengths (e.g. 64, 32, 16, etc...) at the same time.

Cons:

• It has many inefficiencies although most can be overcome with some engineering. Ultimately, the most efficient approach is to do the rewrite during code generation.
• Runs on Ltac which is notoriously difficult to debug.

[RyanGlScott]

Can you elaborate on what you mean by "the most efficient approach is to do the rewrite during code generation"?

[scuellar]

Can you elaborate on what you mean by "the most efficient approach is to do the rewrite during code generation"?

Suppose you have a program P, with a variety of Bvs arithmetic equations (perhaps for different lengths).

The current semantics allows for signed overflow, which is a valid refinement of LLVM semantics, but not the only one. If you instead interpret signed overflow as undefined, then you can always refine P by a program P_Z which only does arithmetic on Z. Ideally the refinement P ~ P_Z can be discharged by saw. Then the coq proofs are only dealing with Z which is easier, with the support of the standard library. On the other hand, bit operations (e.g. shr, bitwise and) are a bit harder, so it's a tradeoff.

[RyanGlScott]

Just to make this a bit more concrete, are you saying that you would want to change Heapster's code generation such that all of the functions take proof arguments of, say, type (x < y)%Z instead of isBvult w x y? (atBVVec is a function of this shape that comes to mind.)

[eddywestbrook]

I'm not quite sure we would want to change the Heapster specification extraction in this way. Given that, it sounds like the approach described above could be a good way to go, at least as far as I understand it. Maybe we could discuss in more detail at some point in person, @scuellar?