Add rotate_left and rotate_right operations to machine integers

[remix7531]

This adds the left and right rotation operations on machine integers which are used in many crypto algorithms. I added the trivial identity and inverse lemma.

• Add rotate_left_vec and rotate_right_vec to FStar.BitVector with lemmas
• Add rotate_left and rotate_right to FStar.UInt and FStar.Int with identity and inverse lemmas
• Add bvrol and bvror to FStar.BV (SMT bitvector theory)
• Update templates (.scripts/.fstip/.fstp) for code generation
• Add OCaml extraction support in FStar_Ints.ml.body and FStar_UInt8.ml
• Add tests in tests/machine_integers/TestRotate.fst

[remix7531]

@microsoft-github-policy-service agree

[mtzguido]

Hi @remix7531, thank you for the PR! In general this looks good to me, and thank you for going through the (tricky) integer modules and making this work. I left a few comments with questions, but this mostly looks good to me.

Out of curiosity can you say where you want to use this?

[remix7531]

Hi @mtzguido . Thanks for your feedback! I will address it soon.

I am working on proofs for RustCrypo's SHA-2 (and others) using HAX and F*. I wrote a specification for SHA-2 in F* but the rotation operation is missing.

[remix7531]

@mtzguido Can you give an estimate on when this PR is going to be merged? Any blockers?

[nikswamy]

This looks pretty good, thanks. The main missing piece is to map the new functions rotate_left/right functions in FStar.BV to the corresponding operations in Z3's bit vector theory, as is done for the other functions in FStar.BV. I'll try adding that quickly and then hopefully we can merge it this week.

[nikswamy]

Can you try this branch on your code? https://github.com/FStarLang/FStar/tree/refs/heads/_nik_bvrol_bvror
If it works, can you merge it into your PR branch.
Thanks!