chore: add MemoryMath to Index.dfy

Author: ajewellamz

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy

@@ -309,7 +309,7 @@ module RawAESKeyring {
                   && AESDecryptRequest.iv == GetIvFromProvInfo(edk.keyProviderInfo)
              )
           && AESDecryptRequest.aad == CanonicalEncryptionContext.EncryptionContextToAAD(input.materials.encryptionContext).value
-      // Can not prove this at this timbe because there may be wrapping involved.
+      // Can not prove this at this time because there may be wrapping involved.
       // && output.value.materials.plaintextDataKey.value
       //   == Seq.Last(cryptoPrimitives.History.AESDecrypt).output.value;
 
@@ -386,7 +386,7 @@ module RawAESKeyring {
       //# If no decryption succeeds, the keyring MUST fail and MUST NOT modify
       //# the [decryption materials](structures.md#decryption-materials).
       return Failure(Types.CollectionOfErrors(list := errors,
-                                              message := "Raw AES Keyring was unable to decrypt any encrypted data key. The list of encountered Exceptions is avaible via `list`."));
+                                              message := "Raw AES Keyring was unable to decrypt any encrypted data key. The list of encountered Exceptions is available via `list`."));
     }
 
     function method SerializeProviderInfo(iv: seq<uint8>): seq<uint8>
@@ -453,7 +453,7 @@ module RawAESKeyring {
     ensures DeserializeEDKCiphertext(SerializeEDKCiphertext(encOutput), |encOutput.authTag|) == encOutput
   {}
 
-  lemma EDKDeserializeSerialze(ciphertext: seq<uint8>, tagLen: nat)
+  lemma EDKDeserializeSerialize(ciphertext: seq<uint8>, tagLen: nat)
     requires tagLen <= |ciphertext|
     ensures SerializeEDKCiphertext(DeserializeEDKCiphertext(ciphertext, tagLen)) == ciphertext
   {}

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestConfig.dfy

@@ -118,7 +118,7 @@ module TestConfig {
     // create and use us-east-2 Keystore and Branch Key
     // Assert call to get Branch Key ID succeeds.
     // As long as tests are run NOT in us-east-2,
-    // this prooves that the DDB Client used the region
+    // this proves that the DDB Client used the region
     // from the KMS Key ARN to initialize the DDB Client
 
     var keyStoreConfig := Types.KeyStoreConfig(
@@ -145,7 +145,7 @@ module TestConfig {
     // create and use us-east-2 Keystore and Branch Key
     // Assert call to get Branch Key ID succeeds.
     // As long as tests are run NOT in us-east-2,
-    // this prooves that the DDB Client used the region
+    // this proves that the DDB Client used the region
     // from the KMS Key ARN to initialize the DDB Client
     keyStoreConfig := Types.KeyStoreConfig(
       id := None,
@@ -178,7 +178,7 @@ module TestConfig {
     // create and use us-east-2 Keystore and Branch Key
     // Assert call to get Branch Key ID FAILS.
     // As long as tests are run NOT in us-east-2,
-    // this prooves that the DDB Client used the region
+    // this proves that the DDB Client used the region
     // from the KMS Key ARN to initialize the DDB Client
     keyStoreConfig := Types.KeyStoreConfig(
       id := None,

StandardLibrary/src/Actions.dfy

@@ -347,7 +347,7 @@ module Actions {
              Last(attemptsState).output,
              DropLast(attemptsState))
            // Attempts are made until there is a success
-           // so attemps will be amde up of failures
+           // so attempts will be made up of failures
            // with one final Success at the end.
         && forall i
              | 0 <= i < |DropLast(attemptsState)|

StandardLibrary/src/Index.dfy

@@ -9,6 +9,7 @@ include "./ConcurrentCall.dfy"
 include "./FloatCompare.dfy"
 include "./GetOpt.dfy"
 include "./HexStrings.dfy"
+include "./MemoryMath.dfy"
 include "./OsLang.dfy"
 include "./Sets.dfy"
 include "./Sorting.dfy"