FStar.BV: expose bvshl, bvshr and bvmod with bit vector rhs

[amosr]

The bit-shifting and modulus operations in FStar.BV currently take natural numbers in the right-hand side. This incurs some conversion overhead, as the SMT-LIB primitives take bit vectors. This commit implements bit vector native versions called bvshl', bvshr' and bvmod_unsafe.

[mtzguido]

NB still testing - just wanted to check if ci worked

No problem with using PRs to check this, but make ci from a clean repo is pretty much exactly what CI does (and it may also be faster depending on your setup). Make docker-ci goes a step further and runs the check within a container, like the CI machine does, but unless you're changing external dependencies make ci is usually good enough.

[amosr]

Thanks Guido, make ci is very helpful

[amosr]

Sorry, I marked it as "ready to review", but it's not actually encoding the new bvshl' operator correctly yet.

[amosr]

I think this is ready for review now. I'll ping @nikswamy too since we discussed this on Slack earlier.

I've added new binary functions that take two bit vectors: bvshl', bvshr', bvmul'. For modulo, I've named the new function bvmod_unsafe to match the existing bvdiv_unsafe. (I believe the encoding for bvdiv_unsafe was also slightly incorrect, which I've fixed.)

I am not convinced about the names bvshl' etc. It's not very descriptive and it's unfortunate that it's inconsistent with bvdiv_unsafe. But I can't think of anything short and descriptive, so I've just used them for now. Happy to change it.

(I was also not sure where to put the test. It's not really a bug report, but I couldn't see a better place for it.)

[nikswamy]

Many thanks Amos! I just made a couple of small fixes and merged this. I also checked that this didn't cause any regressions in the related projects in the Everest repo.

As a next step, it might be worth considering a breaking change that swaps the names around to make the primed version of the operators the default ... but that's for another day.

[amosr]

Thanks Nik!