Add shift_arithmetic_left for signed integers

Add shift_arithmetic_left to FStar.Int and FStar.Int{8,16,32,64,128}.
This performs a left shift on the two's complement representation
without requiring the input to be non-negative.

The existing shift_left requires 0 <= a, matching C semantics where
left-shifting a negative signed integer is undefined behavior.
shift_arithmetic_left accepts any signed integer, matching the
semantics of << on signed integers in Rust and C++20+.

Changes:
- FStar.Int.fsti: definition + two bit-level lemmas
- FStar.Int.fst: trivial proofs for the lemmas
- .scripts/FStar.IntN.fstip: val + infix operator (<<<^)
- .scripts/FStar.IntN.fstp: implementation
- Regenerated FStar.Int{8,16,32,64,128}.{fsti,fst} via mk_int.sh

This commit was created with the assistance of Claude (Anthropic).

Author: remix7531

.scripts/FStar.IntN.fstip

@@ -89,6 +89,13 @@ 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))
 
+(** Shift left on the two's complement representation.
+    Unlike [shift_left], this operates on any signed integer (including negative values).
+    This matches the semantics of [<<] on signed integers in C++ and Rust. *)
+val shift_arithmetic_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.shift_arithmetic_left (v a) (UInt32.v s) = v c))
+
 (* Rotate operators *)
 
 (** Rotate right.
@@ -125,6 +132,7 @@ 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 ( >>>^) = shift_arithmetic_right
+inline_for_extraction unfold let ( <<<^) = shift_arithmetic_left
 inline_for_extraction unfold let ( =^ )  = eq
 inline_for_extraction unfold let ( <>^ ) = ne
 inline_for_extraction unfold let ( >^ )  = gt

.scripts/FStar.IntN.fstp

@@ -51,6 +51,8 @@ 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 shift_arithmetic_left a s = Mk (shift_arithmetic_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))

ulib/FStar.Int.fst

@@ -187,6 +187,10 @@ let shift_arithmetic_right_lemma_1 #n a s i = ()
 
 let shift_arithmetic_right_lemma_2 #n a s i = ()
 
+let shift_arithmetic_left_lemma_1 #n a s i = ()
+
+let shift_arithmetic_left_lemma_2 #n a s i = ()
+
 (* Rotate operators lemmas *)
 
 let rotate_left_lemma #n a s i = ()

ulib/FStar.Int.fsti

@@ -399,6 +399,13 @@ let shift_right (#n:pos) (a:int_t n{0 <= a}) (s:nat) : Tot (int_t n) =
 let shift_arithmetic_right (#n:pos) (a:int_t n) (s:nat) : Tot (int_t n) =
   from_vec (shift_arithmetic_right_vec #n (to_vec #n a) s)
 
+(** Shift left on the two's complement representation.
+    Unlike [shift_left], this operates on any signed integer (including negative values).
+    The result is the same bitwise operation: shift bits left and fill with zeroes.
+    This matches the semantics of [<<] on signed integers in C++ and Rust. *)
+let shift_arithmetic_left (#n:pos) (a:int_t n) (s:nat) : Tot (int_t n) =
+  from_vec (shift_left_vec #n (to_vec #n a) s)
+
 (* Rotate operators *)
 
 (** Rotate left.
@@ -449,6 +456,16 @@ val shift_arithmetic_right_lemma_2: #n:pos -> a:int_t n -> s:nat -> i:nat{i < n
         (ensures (nth (shift_arithmetic_right #n a s) i = nth #n a (i - s)))
 	[SMTPat (nth (shift_arithmetic_right #n a s) i)]
 
+val shift_arithmetic_left_lemma_1: #n:pos -> a:int_t n -> s:nat -> i:nat{i < n && i >= n - s} ->
+  Lemma (requires True)
+	(ensures (nth (shift_arithmetic_left #n a s) i = false))
+	[SMTPat (nth (shift_arithmetic_left #n a s) i)]
+
+val shift_arithmetic_left_lemma_2: #n:pos -> a:int_t n -> s:nat -> i:nat{i < n && i < n - s} ->
+  Lemma (requires True)
+        (ensures (nth (shift_arithmetic_left #n a s) i = nth #n a (i + s)))
+	[SMTPat (nth (shift_arithmetic_left #n a s) i)]
+
 (* Rotate operators lemmas *)
 val rotate_left_lemma: #n:pos -> a:int_t n -> s:nat -> i:nat{i < n} ->
   Lemma (requires True)

ulib/FStar.Int128.fst

@@ -70,6 +70,8 @@ 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 shift_arithmetic_left a s = Mk (shift_arithmetic_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))

ulib/FStar.Int128.fsti

@@ -110,6 +110,13 @@ 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))
 
+(** Shift left on the two's complement representation.
+    Unlike [shift_left], this operates on any signed integer (including negative values).
+    This matches the semantics of [<<] on signed integers in C++ and Rust. *)
+val shift_arithmetic_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.shift_arithmetic_left (v a) (UInt32.v s) = v c))
+
 (* Rotate operators *)
 
 (** Rotate right for non-negative values *)
@@ -142,6 +149,7 @@ 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 ( >>>^) = shift_arithmetic_right
+inline_for_extraction unfold let ( <<<^) = shift_arithmetic_left
 inline_for_extraction unfold let ( =^ )  = eq
 inline_for_extraction unfold let ( <>^ ) = ne
 inline_for_extraction unfold let ( >^ )  = gt

ulib/FStar.Int16.fst

@@ -70,6 +70,8 @@ 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 shift_arithmetic_left a s = Mk (shift_arithmetic_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))

ulib/FStar.Int16.fsti

@@ -110,6 +110,13 @@ 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))
 
+(** Shift left on the two's complement representation.
+    Unlike [shift_left], this operates on any signed integer (including negative values).
+    This matches the semantics of [<<] on signed integers in C++ and Rust. *)
+val shift_arithmetic_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.shift_arithmetic_left (v a) (UInt32.v s) = v c))
+
 (* Rotate operators *)
 
 (** Rotate right.
@@ -146,6 +153,7 @@ 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 ( >>>^) = shift_arithmetic_right
+inline_for_extraction unfold let ( <<<^) = shift_arithmetic_left
 inline_for_extraction unfold let ( =^ )  = eq
 inline_for_extraction unfold let ( <>^ ) = ne
 inline_for_extraction unfold let ( >^ )  = gt

ulib/FStar.Int32.fst

@@ -70,6 +70,8 @@ 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 shift_arithmetic_left a s = Mk (shift_arithmetic_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))

ulib/FStar.Int32.fsti

@@ -110,6 +110,13 @@ 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))
 
+(** Shift left on the two's complement representation.
+    Unlike [shift_left], this operates on any signed integer (including negative values).
+    This matches the semantics of [<<] on signed integers in C++ and Rust. *)
+val shift_arithmetic_left (a:t) (s:UInt32.t) : Pure t
+  (requires (UInt32.v s < n))
+  (ensures (fun c -> FStar.Int.shift_arithmetic_left (v a) (UInt32.v s) = v c))
+
 (* Rotate operators *)
 
 (** Rotate right.
@@ -146,6 +153,7 @@ 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 ( >>>^) = shift_arithmetic_right
+inline_for_extraction unfold let ( <<<^) = shift_arithmetic_left
 inline_for_extraction unfold let ( =^ )  = eq
 inline_for_extraction unfold let ( <>^ ) = ne
 inline_for_extraction unfold let ( >^ )  = gt