Add rotate_left and rotate_right operations to machine integers#4080
Open
remix7531 wants to merge 3 commits intoFStarLang:masterfrom
Open
Add rotate_left and rotate_right operations to machine integers#4080remix7531 wants to merge 3 commits intoFStarLang:masterfrom
remix7531 wants to merge 3 commits intoFStarLang:masterfrom
Conversation
- 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
Author
|
@microsoft-github-policy-service agree |
mtzguido
reviewed
Jan 20, 2026
Member
|
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? |
Author
remix7531
commented
Jan 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.