diff --git a/.scripts/FStar.IntN.fstip b/.scripts/FStar.IntN.fstip
index 4539e0be778..af6b501aabc 100644
--- a/.scripts/FStar.IntN.fstip
+++ b/.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
diff --git a/.scripts/FStar.IntN.fstp b/.scripts/FStar.IntN.fstp
index b436b9f4f46..95ea0fabeea 100644
--- a/.scripts/FStar.IntN.fstp
+++ b/.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))
diff --git a/ulib/FStar.Int.fst b/ulib/FStar.Int.fst
index 6fcc31698ce..1e1872d0428 100644
--- a/ulib/FStar.Int.fst
+++ b/ulib/FStar.Int.fst
@@ -169,6 +169,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 = ()
diff --git a/ulib/FStar.Int.fsti b/ulib/FStar.Int.fsti
index e2eb7665468..a5593d21163 100644
--- a/ulib/FStar.Int.fsti
+++ b/ulib/FStar.Int.fsti
@@ -371,6 +371,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.
@@ -421,6 +428,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)
diff --git a/ulib/FStar.Int128.fst b/ulib/FStar.Int128.fst
index 6faec2ad412..b9cb2afa960 100644
--- a/ulib/FStar.Int128.fst
+++ b/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))
diff --git a/ulib/FStar.Int128.fsti b/ulib/FStar.Int128.fsti
index 9ae111e1d5a..c7f4f0edad1 100644
--- a/ulib/FStar.Int128.fsti
+++ b/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.
@@ -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
diff --git a/ulib/FStar.Int16.fst b/ulib/FStar.Int16.fst
index e5d20f049ff..32b31f607fc 100644
--- a/ulib/FStar.Int16.fst
+++ b/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))
diff --git a/ulib/FStar.Int16.fsti b/ulib/FStar.Int16.fsti
index 19591c94583..782a5a3e4d2 100644
--- a/ulib/FStar.Int16.fsti
+++ b/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
diff --git a/ulib/FStar.Int32.fst b/ulib/FStar.Int32.fst
index f151f625095..491883b9f7a 100644
--- a/ulib/FStar.Int32.fst
+++ b/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))
diff --git a/ulib/FStar.Int32.fsti b/ulib/FStar.Int32.fsti
index c3042e76abc..3f9cbdea139 100644
--- a/ulib/FStar.Int32.fsti
+++ b/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
diff --git a/ulib/FStar.Int64.fst b/ulib/FStar.Int64.fst
index 93fcec8e02c..53f251e0781 100644
--- a/ulib/FStar.Int64.fst
+++ b/ulib/FStar.Int64.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))
diff --git a/ulib/FStar.Int64.fsti b/ulib/FStar.Int64.fsti
index 4823c5c5965..0e664f0a53c 100644
--- a/ulib/FStar.Int64.fsti
+++ b/ulib/FStar.Int64.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
diff --git a/ulib/FStar.Int8.fst b/ulib/FStar.Int8.fst
index dc904fe97fc..015afe7d5ac 100644
--- a/ulib/FStar.Int8.fst
+++ b/ulib/FStar.Int8.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))
diff --git a/ulib/FStar.Int8.fsti b/ulib/FStar.Int8.fsti
index 2d51c6eabdf..11ec0459566 100644
--- a/ulib/FStar.Int8.fsti
+++ b/ulib/FStar.Int8.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