From 5fa0e5044084938ef8e9309448553728270fe2f9 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Mon, 24 Mar 2025 08:51:54 +0000
Subject: [PATCH] feat: add `BitVec.(toInt, toFin)_rotate(Left, Right)` (#7616)

This PR introduces `BitVec.(toInt, toFin)_rotate(Left, Right)`,
completing the API for `BitVec.rotate(Left, Right)`
---
 src/Init/Data/BitVec/Lemmas.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 1b2a29f221..54d21c5db1 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -4015,6 +4015,16 @@ theorem toNat_rotateLeft {x : BitVec w} {r : Nat} :
     (x.rotateLeft r).toNat = (x.toNat <<< (r % w)) % (2^w) ||| x.toNat >>> (w - r % w) := by
   simp only [rotateLeft_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
 
+theorem toInt_rotateLeft {x : BitVec w} {r : Nat} :
+  (x.rotateLeft r).toInt =
+    ((x <<< (r % w)).toNat ||| (x >>> (w - r % w)).toNat : Int).bmod (2 ^ w) := by
+  simp [rotateLeft_def, toInt_shiftLeft, toInt_ushiftRight, toInt_or]
+
+theorem toFin_rotateLeft {x : BitVec w} {r : Nat} :
+  (x.rotateLeft r).toFin =
+    Fin.ofNat' (2 ^ w) (x.toNat <<< (r % w)) ||| x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (w - r % w)) := by
+  simp [rotateLeft_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or]
+
 /-! ## Rotate Right -/
 
 /-- `rotateRight` is defined in terms of left and right shifts. -/
@@ -4161,6 +4171,14 @@ theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
     (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w) := by
   simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]
 
+theorem toInt_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toInt = ((x >>> (r % w)).toNat ||| (x <<< (w - r % w)).toNat : Int).bmod (2 ^ w) := by
+  simp [rotateRight_def, toInt_shiftLeft, toInt_ushiftRight, toInt_or]
+
+theorem toFin_rotateRight {x : BitVec w} {r : Nat} :
+    (x.rotateRight r).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (r % w)) ||| Fin.ofNat' (2 ^ w) (x.toNat <<< (w - r % w)) := by
+  simp [rotateRight_def, toFin_shiftLeft, toFin_ushiftRight, toFin_or]
+
 /- ## twoPow -/
 
 theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i := by