diff --git a/tests/micro-benchmarks/Test.FStar.String.TestMain.fst b/tests/micro-benchmarks/Test.FStar.String.TestMain.fst
new file mode 100644
index 00000000000..ef47c8e7610
--- /dev/null
+++ b/tests/micro-benchmarks/Test.FStar.String.TestMain.fst
@@ -0,0 +1,44 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+module Test.FStar.String.TestMain
+
+open FStar.String
+open FStar.String.Base
+open FStar.String.Properties
+open FStar.String.Match
+open FStar.IO
+open FStar.Class.Printable
+
+let main () =
+ print_string "Running TestMain.main() \n";
+ print_string("lines \"\" 0 " ^ (to_string (lines "" 0)) ^ "\n");
+ assert_norm(strlen "ABCDEF" = 6);
+ assert_norm(strlen "ABC123" = 6);
+ print_string("streq_upto' \"ABCDEF\" \"ABC123\" 1 " ^ 
+             (to_string (streq_upto' "ABCDEF" "ABC123" 1))  ^ "\n");
+ print_string("streq_upto' \"ABCDEF\" \"ABC123\" 2 " ^ 
+             (to_string (streq_upto' "ABCDEF" "ABC123" 2))  ^ "\n");
+ print_string("streq_upto' \"ABCDEF\" \"ABC123\" 3 " ^ 
+             (to_string (streq_upto' "ABCDEF" "ABC123" 3))  ^ "\n");
+ print_string("streq_upto' \"ABCDEF\" \"ABC123\" 4 " ^ 
+             (to_string (streq_upto' "ABCDEF" "ABC123" 4))  ^ "\n")
+
+#push-options "--warn_error -272"
+let _ = main ()
+#pop-options
diff --git a/tests/micro-benchmarks/Test.FStar.String.fst b/tests/micro-benchmarks/Test.FStar.String.fst
new file mode 100644
index 00000000000..7d12cc46cfb
--- /dev/null
+++ b/tests/micro-benchmarks/Test.FStar.String.fst
@@ -0,0 +1,139 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+///  Some of these tests are marked with expect_failure as they won't run at
+/// validation time given an interface file for operations. There is run -time
+/// test code for them in another FStar.String.TestMain. Which at this point
+/// only prints.
+/// 
+
+module Test.FStar.String
+
+open FStar.String
+
+open FStar.String
+open FStar.String.Base
+open FStar.String.Properties
+open FStar.String.Match
+open FStar.Class.Printable
+
+///   Is this caused by strlen being UTF8 characters instead of bytes?
+///  And there is no byte length.
+let _ = assert_norm(strlen "A" = 1)
+let _ = assert(streq_upto "A" "AB" 0)
+let _ = assert(streq_upto "AB" "AB" 0)
+
+let _ = assert_norm(streq_upto "AB" "AB" 1)
+let _ = assert_norm(streq_upto "AB" "AB" 2)
+
+[@@expect_failure]
+let _ = assert_norm(lines "" 0 = (0,0))
+
+[@@expect_failure]
+let _ = assert_norm(lines "A" 0 = (0,0))
+let _ = assert_norm(strlen "A" = 1)
+
+let strlen_A_1 () : Lemma (strlen "A" = 1) = assert_norm(strlen "A" = 1)
+
+[@@expect_failure]
+let _ = assert_norm(strlen_A_1(); lines "A" 1 = (0,1))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "A\n" = 2);
+        assert_norm(lines "A\n" 1 = (0,1))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 0 = (0,0))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 1 = (0,1))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 2 = (0,2))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 3 = (1,0))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 4 = (1,1))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 5 = (2,0))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "AB\nC\nD" = 6);
+        assert_norm(lines  "AB\nC\nD" 6 = (2,1))
+
+/// A few streq_uptos 
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto "ABCDEF" "ABCDEF" 0)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto "ABCDEF" "ABCDEF" 1)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto "ABCDEF" "ABCDEF" 6)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto "ABCDEF" "ABCDEF" 6)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(~(streq_upto "ABCDEF" "ABC" 6))
+
+/// A few streq_upto'
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABCDEF" 0)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABCDEF" 1)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABCDEF" 6)
+
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABCDEF" 6)
+
+[@@expect_failure]
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(strlen "ABC123" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABC123" 1)
+
+[@@expect_failure]
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(strlen "ABC123" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABC123" 2)
+[@@expect_failure]
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(strlen "ABC123" = 6);
+        assert_norm(streq_upto' "ABCDEF" "ABC123" 3)
+
+[@@expect_failure]
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(strlen "ABC123" = 6);
+        assert_norm(~(streq_upto' "ABCDEF" "ABC123" 4))
+
+[@@expect_failure]
+let _ = assert_norm(strlen "ABCDEF" = 6);
+        assert_norm(strlen "ABC123" = 6);
+        assert_norm(~(streq_upto' "ABCDEF" "ABC123" 5))
diff --git a/ulib/FStar.ImmutableArray.fsti b/ulib/FStar.ImmutableArray.fsti
index 402d9820290..bb6339630d9 100644
--- a/ulib/FStar.ImmutableArray.fsti
+++ b/ulib/FStar.ImmutableArray.fsti
@@ -79,3 +79,17 @@ let elem_precedes (#a:Type u#a) (s:t a) (i : nat{i < length s})
       assert (memP (index l i) l);
       memP_precedes (index l i) l
     )
+
+let index_extensionality (#a: Type) (ia1 ia2: t a) 
+: Lemma
+  (requires
+    (length ia1 == length ia2 /\
+    (forall (i: nat) . i < length ia1 ==> index ia1 i == index ia2 i)))
+  (ensures (ia1 == ia2))
+= 
+  let l1 = (to_list ia1) in 
+  let l2 = (to_list ia2) in
+  FStar.List.Tot.index_extensionality l1 l2;
+  of_list_to_list ia1;
+  of_list_to_list ia2
+
diff --git a/ulib/FStar.Seq.Properties.fst b/ulib/FStar.Seq.Properties.fst
index d7d564abdbd..ff0ac2baf2a 100644
--- a/ulib/FStar.Seq.Properties.fst
+++ b/ulib/FStar.Seq.Properties.fst
@@ -665,3 +665,11 @@ let map_seq_append #a #b f s1 s2 =
   Classical.forall_intro (map_seq_index f (Seq.append s1 s2));
   assert (Seq.equal (map_seq f (Seq.append s1 s2))
                     (Seq.append (map_seq f s1) (map_seq f s2)))
+
+let index_extensionality (#a: eqtype) (s1 s2: seq a) : 
+Lemma (requires
+         (length s1 == length s2 /\
+         (forall (i: nat) . i < length s1 ==> index s1 i == index s2 i)))
+  (ensures (s1 == s2))
+= lemma_eq_intro s1 s2;
+  lemma_eq_elim s1 s2
diff --git a/ulib/FStar.Seq.Properties.fsti b/ulib/FStar.Seq.Properties.fsti
index 0f5bb3513e6..f4b410bcdc5 100644
--- a/ulib/FStar.Seq.Properties.fsti
+++ b/ulib/FStar.Seq.Properties.fsti
@@ -760,3 +760,10 @@ val map_seq_index (#a #b:Type) (f:a -> Tot b) (s:Seq.seq a) (i:nat{i < Seq.lengt
 val map_seq_append (#a #b:Type) (f:a -> Tot b) (s1 s2:Seq.seq a)
   : Lemma (ensures (map_seq f (Seq.append s1 s2) ==
                     Seq.append (map_seq f s1) (map_seq f s2)))
+
+val index_extensionality (#a: eqtype) (s1 s2: seq a) 
+: Lemma
+  (requires
+    (length s1 == length s2 /\
+    (forall (i: nat) . i < length s1 ==> index s1 i == index s2 i)))
+  (ensures (s1 == s2))
diff --git a/ulib/FStar.String.Base.fst b/ulib/FStar.String.Base.fst
new file mode 100644
index 00000000000..f148c88ae39
--- /dev/null
+++ b/ulib/FStar.String.Base.fst
@@ -0,0 +1,35 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+module FStar.String.Base
+
+let rec streq_upto'' (s1: string) (s2: string{strlen s1 = strlen s2})
+                     (to: nat{to <= strlen s1}) (from: nat{from <= strlen s1 /\ streq_upto s1 s2 from /\ from <= to}):
+  Tot (b:bool{b <==> streq_upto s1 s2 to})
+  (decreases strlen s1 - from)
+=     
+ if from = to 
+ then true
+ else if from = strlen s1 
+ then true
+ else if index s1 from <> index s2 from
+ then false 
+ else streq_upto'' s1 s2 to (from+1)
+
+let streq_upto' s1 (s2: string{strlen s1 = strlen s2}) (to: nat{to <= strlen s1}):
+  Tot (b:bool{b <==> streq_upto s1 s2 to})
+= streq_upto'' s1 s2 to 0
diff --git a/ulib/FStar.String.Base.fsti b/ulib/FStar.String.Base.fsti
new file mode 100644
index 00000000000..ef85b891b6b
--- /dev/null
+++ b/ulib/FStar.String.Base.fsti
@@ -0,0 +1,32 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Base
+open FStar.String
+
+///  Partial equivalence properties.
+
+let streq_upto s1 s2 (pos: nat) =
+  (pos <= strlen s1 /\ pos <= strlen s2 /\
+   (forall (i: nat{i < pos}). index s1 i = index s2 i))
+
+let streq_upto_min s1 s2 (pos: int{pos < (min (strlen s1) (strlen s2))}) =
+  (forall (i: nat{i <= pos}). index s1 i = index s2 i)
+
+///  The boolean form of streq.
+
+val streq_upto' s1 (s2: string{strlen s1 = strlen s2}) (to: nat{to <= strlen s1}):
+  Tot (b:bool{b <==> streq_upto s1 s2 to})
diff --git a/ulib/FStar.String.Match.fst b/ulib/FStar.String.Match.fst
new file mode 100644
index 00000000000..9e4c7dc1682
--- /dev/null
+++ b/ulib/FStar.String.Match.fst
@@ -0,0 +1,105 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+module FStar.String.Match
+
+open FStar.String.Properties
+
+let rec first_diff' s1 s2
+   (pos: nat{pos <= strlen s1 /\ pos <= strlen s2 /\ streq_upto s1 s2 pos}) : 
+   Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
+             (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
+             (Some? o ==> streq_upto_min s1 s2 (Some?.v o) /\
+              (((Some?.v o) = strlen s1  \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2) \/
+              (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
+                (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))
+        })
+       (decreases (strlen s1 - pos))
+=
+ if pos = strlen s1 && pos = strlen s2
+ then None
+ else if pos >= (strlen s1) || pos >= (strlen s2)
+ then Some pos
+ else begin 
+   if (index s1 pos) <> (index s2 pos) 
+   then Some pos
+   else first_diff' s1 s2 (pos+1)
+ end
+
+let first_diff s1 s2 = first_diff' s1 s2 0
+
+let rec lines' s (upto:nat{upto <= strlen s}) 
+           lastnewline lines chars (pos: nat{pos <= upto && pos <= strlen s}) :
+  Tot (nat & nat) 
+      (decreases upto - pos)
+= if pos = upto 
+  then (if lastnewline then (lines+1, chars) else (lines, chars))
+  else if index s pos = '\n'  
+  then lines' s upto true  lines  0 (pos + 1)
+  else (if lastnewline 
+        then lines' s upto false (lines+1) chars    (pos + 1)
+        else lines' s upto false lines    (chars+1) (pos + 1))
+
+///  Return the line and character upto pos counting each starting at zero.
+let lines (s: string) (upto:nat{upto <= strlen s}) : Tot (nat & nat) = 
+  lines' s upto false 0 0 0
+
+///  Difference Properties
+
+let first_diff'_none_strlen_same (s1 s2: string) :
+  Lemma (None? (first_diff' s1 s2 0) ==> strlen s1 = strlen s2)
+= ()
+
+let none_first_diff_impl_index_extensionality (s1 s2: string) :
+  Lemma (None? (first_diff s1 s2) ==>
+          length s1 = length s2 /\
+          (forall (i: nat) . i < length s1 ==> index s1 i = index s2 i))
+= ()
+
+let none_first_diff_impl_deq (s1 s2: string) :
+  Lemma (None? (first_diff s1 s2) ==> s1 = s2)
+= introduce None? (first_diff s1 s2) ==> s1 = s2
+  with pf_none . begin
+   pf_none;
+   index_extensionality s1 s2
+  end
+
+let deq_impl_none_first_diff (s1 s2: string) :
+  Lemma (s1 = s2 ==> None? (first_diff s1 s2))
+= ()
+
+let deq_iff_none_first_diff (s1 s2: string) :
+  Lemma (s1 = s2 <==> None? (first_diff s1 s2))
+= none_first_diff_impl_deq s1 s2;
+  deq_impl_none_first_diff s1 s2
+
+let first_diff_strlen_neq (s1 s2 : string) :
+ Lemma (strlen s1 <> strlen s2 ==> Some? (first_diff s1 s2 ))
+= ()
+
+let first_diff_neq_some (s1 s2 : string) :
+ Lemma (s1 <> s2 ==> Some? (first_diff s1 s2))
+= if strlen s1 <> strlen s2 
+  then first_diff_strlen_neq s1 s2
+  else 
+    match first_diff s1 s2 with
+    | Some d -> ()
+    | None   -> begin 
+       none_first_diff_impl_deq s1 s2;
+       assert(s1 = s2)
+     end 
diff --git a/ulib/FStar.String.Match.fsti b/ulib/FStar.String.Match.fsti
new file mode 100644
index 00000000000..5369c983d62
--- /dev/null
+++ b/ulib/FStar.String.Match.fsti
@@ -0,0 +1,58 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+module FStar.String.Match
+
+open FStar.String
+open FStar.String.Base
+
+///  Return the first difference position as an option for the whole string.
+val first_diff (s1 s2: string) : 
+   Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
+             (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
+             (Some? o ==> 
+               streq_upto_min s1 s2 (Some?.v o) /\
+              (((Some?.v o) = strlen s1  \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2)
+              \/
+              (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
+                (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))
+        })
+
+
+///  Return the line and character upto pos counting each starting at zero.
+val lines (s: string) (upto: nat{upto <= strlen s}) :  Tot (nat & nat) 
+
+val none_first_diff_impl_index_extensionality (s1 s2: string) :
+  Lemma (None? (first_diff s1 s2) ==>
+          length s1 = length s2 /\
+          (forall (i: nat) . i < length s1 ==> index s1 i = index s2 i))
+
+val none_first_diff_impl_deq (s1 s2: string) :
+  Lemma (None? (first_diff s1 s2) ==> s1 = s2)
+
+val deq_impl_none_first_diff (s1 s2: string) :
+  Lemma (s1 = s2 ==> None? (first_diff s1 s2))
+
+val deq_iff_none_first_diff (s1 s2: string) :
+  Lemma (s1 = s2 <==> None? (first_diff s1 s2))
+
+val first_diff_strlen_neq (s1 s2 : string) :
+ Lemma (strlen s1 <> strlen s2 ==> Some? (first_diff s1 s2 ))
+
+val first_diff_neq_some (s1 s2 : string) :
+ Lemma (s1 <> s2 ==> Some? (first_diff s1 s2))
diff --git a/ulib/FStar.String.Properties.fst b/ulib/FStar.String.Properties.fst
new file mode 100644
index 00000000000..97cb7c64291
--- /dev/null
+++ b/ulib/FStar.String.Properties.fst
@@ -0,0 +1,99 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+module FStar.String.Properties
+
+///  Length properties
+
+let strlen_is_list_length (s: string) :
+ Lemma (strlen s = List.Tot.length (list_of_string s))
+= ()
+
+let list_length_is_strlen (lc: list char) :
+ Lemma (strlen (string_of_list lc) = List.Tot.length lc)
+= list_of_string_of_list lc
+
+let deq_lengths (s1 s2: string) :
+ Lemma (s1 = s2 ==> strlen s1 = strlen s2)
+= ()
+
+let strlen_string_of_char (c: char) :
+ Lemma ((strlen (string_of_char c)) = 1)
+= ()
+
+///  Index properties
+
+let indexes_deq_list_of_string (s:string)  :
+  Lemma (forall (i : nat{i < length s}). List.Tot.index (list_of_string s) i == index s i)
+= introduce forall (i : nat{i < length s}). List.Tot.index (list_of_string s) i == index s i
+  with index_list_of_string s i
+
+let indexes_deq_string_of_list (lc: list char)  :
+  Lemma (list_of_string_of_list lc;
+         forall (i : nat{i < List.Tot.length lc}). 
+            index (string_of_list lc) i == List.Tot.index lc i)
+= list_of_string_of_list lc;
+  introduce forall (i : nat{i < List.Tot.length lc}). 
+             index (string_of_list lc) i == List.Tot.index lc i
+  with index_string_of_list lc i
+
+
+let index_extensionality (s1 s2: string)
+: Lemma
+  (requires
+    (strlen s1 = strlen s2 /\
+    (forall (i: nat) . i < strlen s1 ==> index s1 i = index s2 i)))
+  (ensures (s1 = s2))
+= let l1 = (list_of_string s1) in 
+  let l2 = (list_of_string s2) in
+  indexes_deq_list_of_string s1;
+  indexes_deq_list_of_string s2;
+  List.Tot.index_extensionality l1 l2;
+  string_of_list_of_string s1;
+  string_of_list_of_string s2
+
+///  Streq_upto properties
+
+let streq_upto_strlen_impl_deq s1 s2 :
+  Lemma (requires strlen s1 = strlen s2)
+        (ensures streq_upto s1 s2 (strlen s1) ==> s1 = s2)
+= introduce streq_upto s1 s2 (strlen s1) ==> s1 = s2 
+  with pf_streq_upto . begin
+   pf_streq_upto;
+   index_extensionality s1 s2
+  end
+
+let streq_impl_streq_upto_strlen s1 s2 :
+  Lemma (s1 = s2 ==> streq_upto s1 s2 (strlen s1))
+= ()
+
+let streq_iff_streq_upto_strlen s1 s2 :
+  Lemma (requires strlen s1 = strlen s2)
+        (ensures s1 = s2 <==> streq_upto s1 s2 (strlen s1))
+= streq_impl_streq_upto_strlen s1 s2;
+  streq_upto_strlen_impl_deq   s1 s2
+
+let streq_upto_zero s1 (s2: string{strlen s1 = strlen s2}) :
+  Lemma (streq_upto s1 s2 0)
+= ()
+
+///  Empty string properties.
+
+let strlen_empty () :
+  Lemma (strlen "" = 0)
+= assert_norm(strlen "" = 0) 
diff --git a/ulib/FStar.String.Properties.fsti b/ulib/FStar.String.Properties.fsti
new file mode 100644
index 00000000000..44cc48dfffb
--- /dev/null
+++ b/ulib/FStar.String.Properties.fsti
@@ -0,0 +1,76 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+   Author: Brian Milnes <briangmilnes@gmail.com>
+
+*)
+
+module FStar.String.Properties
+
+open FStar.String
+open FStar.String.Base
+
+///  Length properties
+
+val strlen_is_list_length (s: string) :
+ Lemma (strlen s = List.Tot.length (list_of_string s))
+
+val list_length_is_strlen (lc: list char) :
+ Lemma (strlen (string_of_list lc) = List.Tot.length lc)
+
+val deq_lengths (s1 s2: string) :
+ Lemma (s1 = s2 ==> strlen s1 = strlen s2)
+
+val strlen_string_of_char (c: char) :
+ Lemma ((strlen (string_of_char c)) = 1)
+
+///  Generalized list_of_string and string_of_list 
+
+val indexes_deq_list_of_string (s:string)  :
+  Lemma (forall (i : nat{i < length s}). List.Tot.index (list_of_string s) i == index s i)
+
+val indexes_deq_string_of_list (lc: list char)  :
+  Lemma (list_of_string_of_list lc;
+         forall (i : nat{i < List.Tot.length lc}). 
+            index (string_of_list lc) i == List.Tot.index lc i)
+
+///  Deq at all indexes gives you string equality.
+
+val index_extensionality (s1 s2: string) :
+ Lemma
+  (requires
+    strlen s1 = strlen s2 /\
+     (forall (i: nat) . i < strlen s1 ==> index s1 i = index s2 i))
+  (ensures (s1 == s2))
+
+///  Streq_upto properties
+
+val streq_upto_strlen_impl_deq s1 s2 :
+  Lemma (requires strlen s1 = strlen s2)
+        (ensures streq_upto s1 s2 (strlen s1) ==> s1 = s2)
+
+val streq_impl_streq_upto_strlen s1 s2 :
+  Lemma (s1 = s2 ==> streq_upto s1 s2 (strlen s1))
+
+val streq_iff_streq_upto_strlen s1 s2 :
+  Lemma (requires strlen s1 = strlen s2)
+        (ensures s1 = s2 <==> streq_upto s1 s2 (strlen s1))
+
+val streq_upto_zero s1 (s2: string{strlen s1 = strlen s2}) :
+  Lemma (streq_upto s1 s2 0)
+
+///  Empty string properties.
+
+val strlen_empty () :
+  Lemma (strlen "" = 0)
diff --git a/ulib/FStar.String.fsti b/ulib/FStar.String.fsti
index ba6245670af..7a5f8870094 100644
--- a/ulib/FStar.String.fsti
+++ b/ulib/FStar.String.fsti
@@ -1,5 +1,5 @@
 (*
-   Copyright 2008-2019 Microsoft Research
+   Copyright 2008-2024 Microsoft Research
 
    Licensed under the Apache License, Version 2.0 (the "License");
    you may not use this file except in compliance with the License.
@@ -14,7 +14,9 @@
    limitations under the License.
 *)
 module FStar.String
+
 open FStar.List.Tot
+
 (* String is a primitive type in F*.
 
    Most of the functions in this interface have a special status in