chore(dafny): Make HasSubString generic (#1549)

Author: ajewellamz

StandardLibrary/src/String.dfy

@@ -7,6 +7,7 @@ module StandardLibrary.String {
   import Wrappers
   import opened UInt
   import opened Sequence
+  import opened MemoryMath
   export provides Int2String, Base10Int2String, HasSubString, Wrappers, UInt
 
   const Base10: seq<char> := ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
@@ -55,27 +56,26 @@ module StandardLibrary.String {
   }
 
   /* Returns the index of a substring or None, if the substring is not in the string */
-  method HasSubString(haystack: string, needle: string)
+  method HasSubString<T(==)>(haystack: seq<T>, needle: seq<T>)
     returns (o: Wrappers.Option<nat>)
 
     ensures o.Some? ==>
               && o.value <= |haystack| - |needle| && haystack[o.value..(o.value + |needle|)] == needle
               && (forall i | 0 <= i < o.value :: haystack[i..][..|needle|] != needle)
 
-    ensures |haystack| < |needle| || |haystack| > (UINT64_MAX_LIMIT-1) ==> o.None?
+    ensures |haystack| < |needle| ==> o.None?
 
     ensures o.None? && |needle| <= |haystack| && |haystack| <= (UINT64_MAX_LIMIT-1) ==>
               (forall i | 0 <= i <= (|haystack|-|needle|) :: haystack[i..][..|needle|] != needle)
   {
-    if |haystack| < |needle| {
+    SequenceIsSafeBecauseItIsInMemory(haystack);
+    SequenceIsSafeBecauseItIsInMemory(needle);
+    if |haystack| as uint64 < |needle| as uint64 {
       return Wrappers.None;
     }
 
-    // `-1` is needed because of how `limit` is calculated below
-    expect |haystack| <= (UINT64_MAX_LIMIT-1);
-
     var size : uint64 := |needle| as uint64;
-    var limit: uint64 := |haystack| as uint64 - size + 1;
+    var limit: uint64 := Add(|haystack| as uint64 - size, 1);
 
     for index := 0 to limit
       invariant forall i | 0 <= i < index :: haystack[i..][..size] != needle