Add rotate_left and rotate_right operations to machine integers

.scripts/FStar.IntN.fstip

@@ -89,6 +89,22 @@ val shift_arithmetic_right (a:t) (s:UInt32.t) : Pure t
   (requires (UInt32.v s < n))
   (ensures (fun c -> FStar.Int.shift_arithmetic_right (v a) (UInt32.v s) = v c))
 
+(* Rotate operators *)
+
+(** Rotate right.
+    Note: Rotation is performed at the bit level and is essentially unsigned.
+    The sign bit is rotated just like any other bit. *)
+val rotate_right (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.rotate_right (v a) (UInt32.v s) = v c))
+
+(** Rotate left.
+    Note: Rotation is performed at the bit level and is essentially unsigned.
+    The sign bit is rotated just like any other bit. *)
+val rotate_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.rotate_left (v a) (UInt32.v s) = v c))
+
 (* Comparison operators *)
 let eq  (a:t) (b:t) : Tot bool = eq  #n (v a) (v b)
 let ne  (a:t) (b:t) : Tot bool = ne  #n (v a) (v b)

.scripts/FStar.IntN.fstp

@@ -51,6 +51,10 @@ let shift_left a s = Mk (shift_left (v a) (UInt32.v s))
 
 let shift_arithmetic_right a s = Mk (shift_arithmetic_right (v a) (UInt32.v s))
 
+let rotate_right a s = Mk (rotate_right (v a) (UInt32.v s))
+
+let rotate_left a s = Mk (rotate_left (v a) (UInt32.v s))
+
 let to_string _ = admit ()
 
 //AR: this is to workaround the interleaving semantics of pragmas in FStar.Int128.fst

.scripts/FStar.UIntN.fstip

@@ -193,6 +193,18 @@ val shift_left (a:t) (s:UInt32.t) : Pure t
   (requires (UInt32.v s < n))
   (ensures (fun c -> FStar.UInt.shift_left (v a) (UInt32.v s) = v c))
 
+(**** Rotate operators *)
+
+(** Rotate right, rotating at most the integer width *)
+val rotate_right (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.UInt.rotate_right (v a) (UInt32.v s) = v c))
+
+(** Rotate left, rotating at most the integer width *)
+val rotate_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.UInt.rotate_left (v a) (UInt32.v s) = v c))
+
 (**** Comparison operators *)
 
 (** Equality
@@ -310,6 +322,8 @@ inline_for_extraction unfold let ( &^ )  = logand
 inline_for_extraction unfold let ( |^ )  = logor
 inline_for_extraction unfold let ( <<^ ) = shift_left
 inline_for_extraction unfold let ( >>^ ) = shift_right
+inline_for_extraction unfold let ( <<<^ ) = rotate_left
+inline_for_extraction unfold let ( >>>^ ) = rotate_right
 inline_for_extraction unfold let ( =^ )  = eq
 inline_for_extraction unfold let ( <>^ ) = ne
 inline_for_extraction unfold let ( >^ )  = gt

.scripts/FStar.UIntN.fstp

@@ -57,6 +57,10 @@ let shift_right a s = Mk (shift_right (v a) (UInt32.v s))
 
 let shift_left a s = Mk (shift_left (v a) (UInt32.v s))
 
+let rotate_right a s = Mk (rotate_right (v a) (UInt32.v s))
+
+let rotate_left a s = Mk (rotate_left (v a) (UInt32.v s))
+
 let lemma_sub_msbs a b
     = from_vec_propriety (to_vec (v a)) 1;
       from_vec_propriety (to_vec (v b)) 1;

tests/machine_integers/TestRotate.fst

@@ -0,0 +1,191 @@
+module TestRotate
+
+open FStar.All
+open FStar.IO
+
+module U8   = FStar.UInt8
+module U16  = FStar.UInt16
+module U32  = FStar.UInt32
+module U64  = FStar.UInt64
+module I8   = FStar.Int8
+module I32  = FStar.Int32
+
+let check s (b:bool) : ML unit =
+    if not b then failwith s
+
+(* Test rotate_left for UInt32 *)
+let test_u32_rotate_left () : ML unit =
+    (* Rotate left by 0 should be identity *)
+    check "u32_rol_0"
+        (U32.to_string (U32.rotate_left 0x12345678ul 0ul) = "305419896");
+
+    (* Rotate left by 4 (one nibble): 0x12345678 -> 0x23456781 *)
+    check "u32_rol_4"
+        (U32.to_string (U32.rotate_left 0x12345678ul 4ul) = "591751041");
+
+    (* Rotate left by 8 (one byte): 0x12345678 -> 0x34567812 *)
+    check "u32_rol_8"
+        (U32.to_string (U32.rotate_left 0x12345678ul 8ul) = "878082066");
+
+    (* Rotate left by 16 (two bytes): 0x12345678 -> 0x56781234 *)
+    check "u32_rol_16"
+        (U32.to_string (U32.rotate_left 0x12345678ul 16ul) = "1450709556");
+
+    (* Rotate left by 1 *)
+    check "u32_rol_1_ff"
+        (U32.to_string (U32.rotate_left 0xFFFFFFFFul 1ul) = "4294967295");
+
+    (* Rotate left by 1 on 1 *)
+    check "u32_rol_1_one"
+        (U32.to_string (U32.rotate_left 1ul 1ul) = "2");
+
+    (* Rotate left by 31 on 1 *)
+    check "u32_rol_31_one"
+        (U32.to_string (U32.rotate_left 1ul 31ul) = "2147483648");
+    ()
+
+(* Test rotate_right for UInt32 *)
+let test_u32_rotate_right () : ML unit =
+    (* Rotate right by 0 should be identity *)
+    check "u32_ror_0"
+        (U32.to_string (U32.rotate_right 0x12345678ul 0ul) = "305419896");
+
+    (* Rotate right by 4 (one nibble): 0x12345678 -> 0x81234567 *)
+    check "u32_ror_4"
+        (U32.to_string (U32.rotate_right 0x12345678ul 4ul) = "2166572391");
+
+    (* Rotate right by 8 (one byte): 0x12345678 -> 0x78123456 *)
+    check "u32_ror_8"
+        (U32.to_string (U32.rotate_right 0x12345678ul 8ul) = "2014458966");
+
+    (* Rotate right by 16 (two bytes): 0x12345678 -> 0x56781234 *)
+    check "u32_ror_16"
+        (U32.to_string (U32.rotate_right 0x12345678ul 16ul) = "1450709556");
+
+    (* Rotate right by 1 on all ones *)
+    check "u32_ror_1_ff"
+        (U32.to_string (U32.rotate_right 0xFFFFFFFFul 1ul) = "4294967295");
+
+    (* Rotate right by 1 on 1 should give high bit *)
+    check "u32_ror_1_one"
+        (U32.to_string (U32.rotate_right 1ul 1ul) = "2147483648");
+    ()
+
+(* Test rotate_left for UInt8 *)
+let test_u8_rotate_left () : ML unit =
+    (* Rotate left by 0 should be identity *)
+    check "u8_rol_0"
+        (U8.to_string (U8.rotate_left 0x12uy 0ul) = "18");
+
+    (* Rotate left by 4 (one nibble): 0x12 -> 0x21 *)
+    check "u8_rol_4"
+        (U8.to_string (U8.rotate_left 0x12uy 4ul) = "33");
+
+    (* Rotate left by 1 on all ones *)
+    check "u8_rol_1_ff"
+        (U8.to_string (U8.rotate_left 0xFFuy 1ul) = "255");
+
+    (* Rotate left by 1 on 1 *)
+    check "u8_rol_1_one"
+        (U8.to_string (U8.rotate_left 1uy 1ul) = "2");
+
+    (* Rotate left by 7 on 1 *)
+    check "u8_rol_7_one"
+        (U8.to_string (U8.rotate_left 1uy 7ul) = "128");
+    ()
+
+(* Test rotate_right for UInt8 *)
+let test_u8_rotate_right () : ML unit =
+    (* Rotate right by 0 should be identity *)
+    check "u8_ror_0"
+        (U8.to_string (U8.rotate_right 0x12uy 0ul) = "18");
+
+    (* Rotate right by 4 (one nibble): 0x12 -> 0x21 *)
+    check "u8_ror_4"
+        (U8.to_string (U8.rotate_right 0x12uy 4ul) = "33");
+
+    (* Rotate right by 1 on 1 *)
+    check "u8_ror_1_one"
+        (U8.to_string (U8.rotate_right 1uy 1ul) = "128");
+    ()
+
+(* Test rotate_left for UInt64 *)
+let test_u64_rotate_left () : ML unit =
+    (* Rotate left by 0 should be identity *)
+    check "u64_rol_0"
+        (U64.to_string (U64.rotate_left 0x123456789ABCDEFuL 0ul) = "81985529216486895");
+
+    (* Rotate left by 4: 0x0123456789ABCDEF -> 0x123456789ABCDEF0 *)
+    check "u64_rol_4"
+        (U64.to_string (U64.rotate_left 0x123456789ABCDEFuL 4ul) = "1311768467463790320");
+
+    (* Rotate left by 1 on 1 *)
+    check "u64_rol_1_one"
+        (U64.to_string (U64.rotate_left 1uL 1ul) = "2");
+
+    (* Rotate left by 63 on 1 *)
+    check "u64_rol_63_one"
+        (U64.to_string (U64.rotate_left 1uL 63ul) = "9223372036854775808");
+    ()
+
+(* Test rotate_right for UInt64 *)
+let test_u64_rotate_right () : ML unit =
+    (* Rotate right by 0 should be identity *)
+    check "u64_ror_0"
+        (U64.to_string (U64.rotate_right 0x123456789ABCDEFuL 0ul) = "81985529216486895");
+
+    (* Rotate right by 1 on 1 *)
+    check "u64_ror_1_one"
+        (U64.to_string (U64.rotate_right 1uL 1ul) = "9223372036854775808");
+    ()
+
+(* Test inverse property: rotate_right(rotate_left(x, s), s) = x *)
+let test_inverse_u32 () : ML unit =
+    let x = 0x12345678ul in
+    check "u32_inverse_4"
+        (U32.rotate_right (U32.rotate_left x 4ul) 4ul = x);
+    check "u32_inverse_8"
+        (U32.rotate_right (U32.rotate_left x 8ul) 8ul = x);
+    check "u32_inverse_16"
+        (U32.rotate_right (U32.rotate_left x 16ul) 16ul = x);
+    check "u32_inverse_1"
+        (U32.rotate_right (U32.rotate_left x 1ul) 1ul = x);
+    check "u32_inverse_31"
+        (U32.rotate_right (U32.rotate_left x 31ul) 31ul = x);
+    ()
+
+(* Test inverse property the other way: rotate_left(rotate_right(x, s), s) = x *)
+let test_inverse_u32_other () : ML unit =
+    let x = 0x12345678ul in
+    check "u32_inverse_other_4"
+        (U32.rotate_left (U32.rotate_right x 4ul) 4ul = x);
+    check "u32_inverse_other_8"
+        (U32.rotate_left (U32.rotate_right x 8ul) 8ul = x);
+    check "u32_inverse_other_16"
+        (U32.rotate_left (U32.rotate_right x 16ul) 16ul = x);
+    ()
+
+(* Test signed Int32 rotate (non-negative values only) *)
+let test_i32_rotate () : ML unit =
+    check "i32_rol_0"
+        (I32.to_string (I32.rotate_left 0x12345678l 0ul) = "305419896");
+    check "i32_rol_4"
+        (I32.to_string (I32.rotate_left 0x12345678l 4ul) = "591751041");
+    check "i32_ror_0"
+        (I32.to_string (I32.rotate_right 0x12345678l 0ul) = "305419896");
+    ()
+
+let main () : ML int =
+    test_u32_rotate_left ();
+    test_u32_rotate_right ();
+    test_u8_rotate_left ();
+    test_u8_rotate_right ();
+    test_u64_rotate_left ();
+    test_u64_rotate_right ();
+    test_inverse_u32 ();
+    test_inverse_u32_other ();
+    test_i32_rotate ();
+    print_string "correct\n";
+    0
+
+let _ = main ()

tests/machine_integers/TestRotate.out.expected

@@ -0,0 +1 @@
+correct

ulib/FStar.BV.fst

@@ -96,6 +96,29 @@ let int2bv_shr #n #x #y #z pf =
   int2bv_nat_lemma #n y;
   inverse_vec_lemma #n (bvshr #n (int2bv #n x) y)
 
+(* Rotate operations *)
+let bvrol' (#n: pos) (a: bv_t n) (s: bv_t n): bv_t n =
+  B.rotate_left_vec #n a (bv2int #n s)
+let bvrol (#n: pos) (a: bv_t n) (s: nat): bv_t n =
+  bvrol' #n a (int2bv_nat #n s)
+
+let int2bv_rol' #n #x #y #z pf =
+  inverse_vec_lemma #n (bvrol' #n (int2bv #n x) (int2bv #n y))
+let int2bv_rol #n #x #y #z pf =
+  int2bv_nat_lemma #n y;
+  inverse_vec_lemma #n (bvrol #n (int2bv #n x) y)
+
+let bvror' (#n: pos) (a: bv_t n) (s: bv_t n): bv_t n =
+  B.rotate_right_vec #n a (bv2int #n s)
+let bvror (#n: pos) (a: bv_t n) (s: nat): bv_t n =
+  bvror' #n a (int2bv_nat #n s)
+
+let int2bv_ror' #n #x #y #z pf =
+  inverse_vec_lemma #n (bvror' #n (int2bv #n x) (int2bv #n y))
+let int2bv_ror #n #x #y #z pf =
+  int2bv_nat_lemma #n y;
+  inverse_vec_lemma #n (bvror #n (int2bv #n x) y)
+
 
 
 let bvult #n a b = (bv2int #n a) < (bv2int #n b)

ulib/FStar.BV.fsti

@@ -198,6 +198,52 @@ val int2bv_shr:
     squash (bvshr #n (int2bv #n x) y == z)
   -> Lemma (int2bv #n (shift_right #n x y) == z)
 
+(**** Rotate operations *)
+
+(** Bitwise rotate left: rotate by bit-vector. *)
+val bvrol' (#n: pos) (a: bv_t n) (s: bv_t n) : Tot (bv_t n)
+
+(** Bitwise rotate left: rotate by integer. *)
+val bvrol  (#n: pos) (a: bv_t n) (s: nat)    : Tot (bv_t n)
+
+val int2bv_rol':
+    #n: pos ->
+    #x: uint_t n ->
+    #y: uint_t n ->
+    #z: bv_t n ->
+    squash (bvrol' #n (int2bv #n x) (int2bv #n y) == z)
+  -> Lemma (int2bv #n (rotate_left #n x y) == z)
+
+val int2bv_rol:
+    #n: pos ->
+    #x: uint_t n ->
+    #y: uint_t n ->
+    #z: bv_t n ->
+    squash (bvrol #n (int2bv #n x) y == z)
+  -> Lemma (int2bv #n (rotate_left #n x y) == z)
+
+(** Bitwise rotate right: rotate by bit-vector. *)
+val bvror' (#n: pos) (a: bv_t n) (s: bv_t n) : Tot (bv_t n)
+
+(** Bitwise rotate right: rotate by integer. *)
+val bvror  (#n: pos) (a: bv_t n) (s: nat)    : Tot (bv_t n)
+
+val int2bv_ror':
+    #n: pos ->
+    #x: uint_t n ->
+    #y: uint_t n ->
+    #z: bv_t n ->
+    squash (bvror' #n (int2bv #n x) (int2bv #n y) == z)
+  -> Lemma (int2bv #n (rotate_right #n x y) == z)
+
+val int2bv_ror:
+    #n: pos ->
+    #x: uint_t n ->
+    #y: uint_t n ->
+    #z: bv_t n ->
+    squash (bvror #n (int2bv #n x) y == z)
+  -> Lemma (int2bv #n (rotate_right #n x y) == z)
+
 (**** Arithmetic operations *)
 unfold
 let bv_zero #n = int2bv #n 0

ulib/FStar.BitVector.fst

@@ -116,3 +116,47 @@ let shift_arithmetic_right_vec_lemma_2 (#n: pos) (a: bv_t n) (s: nat) (i: nat{i
     : Lemma (ensures index (shift_arithmetic_right_vec #n a s) i = index a (i - s))
       [SMTPat (index (shift_arithmetic_right_vec #n a s) i)] = ()
 
+(**** Rotate operators *)
+
+(** Relating the indexes of the rotated left vector to the original *)
+let rotate_left_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
+    : Lemma (ensures index (rotate_left_vec #n a s) i = index a ((i + s) % n))
+      [SMTPat (index (rotate_left_vec #n a s) i)] =
+  let s' = s % n in
+  if s' = 0 then ()
+  else if i < n - s' then ()
+  else ()
+
+(** Relating the indexes of the rotated right vector to the original *)
+let rotate_right_vec_lemma (#n: pos) (a: bv_t n) (s: nat) (i: nat{i < n})
+    : Lemma (ensures index (rotate_right_vec #n a s) i = index a ((i + n - (s % n)) % n))
+      [SMTPat (index (rotate_right_vec #n a s) i)] =
+  let s' = s % n in
+  if s' = 0 then ()
+  else if i < s' then ()
+  else ()
+
+(** Rotate left by n is identity *)
+let rotate_left_vec_full_identity (#n: pos) (a: bv_t n)
+    : Lemma (ensures rotate_left_vec #n a n = a)
+      [SMTPat (rotate_left_vec #n a n)] =
+  assert (n % n = 0);
+  Seq.lemma_eq_intro (rotate_left_vec #n a n) a
+
+(** Rotate right by n is identity *)
+let rotate_right_vec_full_identity (#n: pos) (a: bv_t n)
+    : Lemma (ensures rotate_right_vec #n a n = a)
+      [SMTPat (rotate_right_vec #n a n)] =
+  assert (n % n = 0);
+  Seq.lemma_eq_intro (rotate_right_vec #n a n) a
+
+(** Rotate left and right are inverses *)
+let rotate_left_right_vec_inverse (#n: pos) (a: bv_t n) (s: nat)
+    : Lemma (ensures rotate_right_vec #n (rotate_left_vec #n a s) s = a) =
+  Seq.lemma_eq_intro (rotate_right_vec #n (rotate_left_vec #n a s) s) a
+
+(** Rotate right and left are inverses *)
+let rotate_right_left_vec_inverse (#n: pos) (a: bv_t n) (s: nat)
+    : Lemma (ensures rotate_left_vec #n (rotate_right_vec #n a s) s = a) =
+  Seq.lemma_eq_intro (rotate_left_vec #n (rotate_right_vec #n a s) s) a
+