chore(STD-Dafny): HasSubString (#952)

* chore(STD-Dafny): HasSubString

StandardLibrary/src/Sequence.dfy

@@ -0,0 +1,42 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "UInt.dfy"
+
+module StandardLibrary.Sequence {
+  // export provides SequenceEqual, StandardLibrary
+  import opened UInt
+
+  predicate method SequenceEqualNat<T(==)>(seq1: seq<T>, seq2: seq<T>, start1: nat, start2: nat, size: nat) : (ret : bool)
+    requires start1 + size <= |seq1|
+    requires start2 + size <= |seq2|
+    ensures ret ==> seq1[start1..start1 + size] == seq2[start2..start2 + size]
+  {
+    if |seq1| > UINT64_MAX_LIMIT || |seq2| > UINT64_MAX_LIMIT then
+      // This line of code will never be executed, but is included for correctness
+      seq1[start1..start1 + size] == seq2[start2..start2 + size]
+    else
+      SequenceEqual(seq1, seq2, start1 as uint64, start2 as uint64, size as uint64)
+  }
+
+  predicate SequenceEqual<T(==)>(seq1: seq64<T>, seq2: seq64<T>, start1: uint64, start2: uint64, size: uint64) : (ret : bool)
+    requires start1 as nat + size as nat <= |seq1|
+    requires start2 as nat + size as nat <= |seq2|
+    ensures ret <==> seq1[start1..start1 + size] == seq2[start2..start2 + size]
+  {
+    seq1[start1..start1 + size] == seq2[start2..start2 + size]
+  } by method {
+    var j := start2 as uint64;
+    for i := start1 as uint64 to (start1 + size) as uint64
+      invariant j == i - start1 + start2
+      invariant forall k : uint64 | start1 <= k < i :: seq1[k] == seq2[k - start1 + start2]
+    {
+      if seq1[i] != seq2[j] {
+        return false;
+      }
+      j := j + 1;
+    }
+    return true;
+  }
+
+}

StandardLibrary/src/String.dfy

@@ -1,8 +1,13 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
+include "../../libraries/src/Wrappers.dfy"
+include "Sequence.dfy"
 
 module StandardLibrary.String {
-  export provides Int2String, Base10Int2String
+  import Wrappers
+  import opened UInt
+  import opened Sequence
+  export provides Int2String, Base10Int2String, HasSubString, Wrappers, UInt
 
   const Base10: seq<char> := ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
 
@@ -48,4 +53,37 @@ module StandardLibrary.String {
   {
     Int2String(n, Base10)
   }
+
+  /* Returns the index of a substring or None, if the substring is not in the string */
+  method HasSubString(haystack: string, needle: string)
+    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 o.None? && |needle| <= |haystack| && |haystack| <= (UINT64_MAX_LIMIT-1) ==>
+              (forall i | 0 <= i <= (|haystack|-|needle|) :: haystack[i..][..|needle|] != needle)
+  {
+    if |haystack| < |needle| {
+      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;
+
+    for index := 0 to limit
+      invariant forall i | 0 <= i < index :: haystack[i..][..size] != needle
+    {
+      if SequenceEqual(seq1 := haystack, seq2 := needle, start1 := index, start2 := 0, size := size) {
+        return Wrappers.Some(index as nat);
+      }
+    }
+    return Wrappers.None;
+  }
 }

StandardLibrary/src/UInt.dfy

@@ -16,6 +16,7 @@ module StandardLibrary.UInt {
   const UINT64_LIMIT := BoundedInts.UINT64_MAX as int + 1
   const INT32_MAX_LIMIT := BoundedInts.INT32_MAX as int
   const INT64_MAX_LIMIT := BoundedInts.INT64_MAX as int
+  const UINT64_MAX_LIMIT := BoundedInts.UINT64_MAX as int
 
   predicate method UInt8Less(a: uint8, b: uint8) { a < b }
 

StandardLibrary/test/TestString.dfy

@@ -0,0 +1,35 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../src/StandardLibrary.dfy"
+include "../src/String.dfy"
+include "../../libraries/src/Wrappers.dfy"
+
+module TestStrings {
+  import StandardLibrary.String
+  import opened Wrappers
+
+  method {:test} TestHasSubStringPositive()
+  {
+    var actual := String.HasSubString("Koda is a Dog.", "Koda");
+    expect actual == Some(0), "'Koda' is in 'Koda is a Dog.' at index 0, but HasSubString does not think so";
+    actual := String.HasSubString("Koda is a Dog.", "Koda is a Dog.");
+    expect actual == Some(0), "'Koda is a Dog.' is in 'Koda is a Dog.' at index 0, but HasSubString does not think so";
+    actual := String.HasSubString("Koda is a Dog.", "Dog.");
+    expect actual == Some(10), "'Dog.' is in 'Koda is a Dog.' at index 10, but HasSubString does not think so";
+    actual := String.HasSubString("Koda is a Dog.", ".");
+    expect actual == Some(13), "'.' is in 'Koda is a Dog.' at index 13, but HasSubString does not think so";
+    actual := String.HasSubString("Koda is a Dog.", "");
+    expect actual == Some(0), "The empty string is in 'Koda is a Dog.' at index 0, but HasSubString does not think so";
+  }
+
+  method {:test} TestHasSubStringNegative()
+  {
+    var actual := String.HasSubString("Robbie is a Dog.", "Koda");
+    expect actual == None, "'Robbie is a Dog.' does not contain Koda";
+    actual := String.HasSubString("\t", " ");
+    expect actual == None, "A tab is not a space";
+    actual := String.HasSubString("large", "larger");
+    expect actual == None, "Needle larger than haystack";
+  }
+}