Much cleaner strings with index_extensionality (and for Seq and ImmutableArray) that does not create a new eq.

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 <[email protected]>
+
+*)
+
+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

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 <[email protected]>
+
+*)
+
+///  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))

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
+

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

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))

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 <[email protected]>
+
+*)
+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

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 - 1)}). 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})