Extend the library of Coq rewrite rules for bitvector operations

[brianhuffman]

There are already some lemmas proved in SAWCorePrelude_proofs.v. We should extend this library with more theorems that we find useful for working with bitvector terms.

[m-yac]

Although I've since added a large number of bitvector lemmas to SAWCoreBitvectors.v, these were added in a very ad-hoc way and basically none of them were proven. I just recently realized some of them are actually false, and many important ones are missing, so I think we need to have a better solution then just adding Admitted bitvector lemmas every time we need them for a Heapster proof.

One option is to use the lemmas in the bits library - which I didn't know existed until just now! The advantage of this is that we don't have to add any new dependencies, but a disadvantage is that Heapster proofs mostly need inequality lemmas, and that part is not as fleshed out in bits. After a first pass I can't find another standard bitvector Coq library which does any better, however.

Another issue specific to Heapster is that even with less Admitteds, our proof automation still has no way to reason about bitvector goals – taking care of bitvector goals in the automation would cut down on the size of Heapster proofs dramatically. We could try extending the automation to do this ourselves, but coming up with a way to do that which is not ad-hoc and is in any way performant sounds like a whole paper. Ideally, we would use a library which has a tactic that lets us prove bitvector goals automatically...

So, another option is to use SMTCoq's bitvectors, which would let us take care of any bitvector goals automatically by deferring to an external solver. A big disadvantage of this is that new user would now have to follow these special instructions to compile versions of CVC4 and veriT compatible with SMTCoq. Unclear if that extra overhead to a new user is worth it.

@brianhuffman @eddywestbrook @jpaykin thoughts?

[robdockins]

FWIW, I am also interested in this question from the Cryptol->Coq extraction angle; in particular there are a number of purely stub implementations of operations that need to be fleshed out, and it's fairly critical to get them right. As far as I can tell, bits doesn't implement some of the ones we want (division operations, lg2).

[robdockins]

On that note, actually, this looks problematic to me,

https://github.com/GaloisInc/saw-script/blob/9ddb61776077f42375730576a5b6d7b683b6d1be/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v#L318-L323

Note the recursive call is to shiftL, which is pretty suspect.

[jpaykin]

I just recently realized some of them are actually false, and many important ones are missing, so I think we need to have a better solution then just adding Admitted bitvector lemmas every time we need them for a Heapster proof.

@m-yac In response to this particular issue, I wonder if we could set up a workflow where bitvector lemmas are verified using SMT solvers ourselves (maybe even SAW/cryptol?) before being added to Coq as axioms. This would only result in partial verification---the SMT theorems would be limited to bitvectors of concrete widths---but would at least add confidence around the correctness of new axioms. It would mean we could use our own tools instead of relying on SMTCoq and their dependencies, but it would be less integrated into Coq itself.

We could try extending the automation to do this ourselves, but coming up with a way to do that which is not ad-hoc and is in any way performant sounds like a whole paper. Ideally, we would use a library which has a tactic that lets us prove bitvector goals automatically...

If all the end goals are over concrete values, reflection might be the best choice here, and the bits library already depends on ssreflect and extracts all their operations to ocaml. It might be worth talking to the maintainers of that library and see if they have a suggestion for doing this well. I don't have experience with ssreflect, but I have used reflection in general, and I could envision that either an ocaml plugin-based tactic or just a general reflect tactic shouldn't be too hard to implement (knock on wood).

[robdockins]

For sufficiently small examples (say, bitvectors from 0 to 8 bits), you could just to a pretty naive boolean quantifier elimination process, which would amount to exhaustive enumeration of the inputs. That would provide a pretty decent smoke test for lemmas.

[m-yac]

I implemented Rob's suggestion (if I'm understanding it correctly) in #1495, though checking bitvectors with any more than 3 or 4 bits was simply too slow on my machine. This found four incorrect lemmas, and now I have more confidence in the rest.

For a long-term solution, I'm curious to hear more about what you're envisioning @jpaykin. The goals that show up in the automation often involve a non-obvious sequence of rewrites (both from hypotheses and existing lemmas) to prove. We would still need to write some algorithm to deduce this sequence of rewrites from the reflected goal + hyps, right? If so, what is that algorithm? Wouldn't it have to be something with around the same complexity of omega?

[jpaykin]

@m-yac I just took a closer look at the goals, and my idea doesn't really make sense... I was thinking the goals were all about concrete bitvector values, but that's not the case.

In general, for a reflection tactic to handle goals with variables in them, it needs a good normal form for expressions. Adam Chlipala (http://adam.chlipala.net/cpdt/html/Reflection.html) has some examples of doing this on non-equality relations, but I'm not sure how this would translate to bitvectors