cleanup

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -384,7 +384,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       // invariant forall k <- fieldMap :: fieldMap[k] in record
     {
       var utf8Value :- UTF8.Encode(ATTR_PREFIX + Paths.PathToString(fields[i].key)).MapFailure(e =>E(e));
-      // TODO - check for duplicates
+      // To Be Done - check for duplicates
       fieldMap := fieldMap[utf8Value := fields[i].key];
     }
     var keys : seq<UTF8.ValidUTF8Bytes> := SortedSets.ComputeSetToOrderedSequence2(fieldMap.Keys, ByteLess);
@@ -853,7 +853,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     :- NeedBinary(encRecord, FooterPath);
     :- Need(exists x :: (x in encRecord && x.action == SIGN), E("At least one Authenticate Action must be SIGN"));
 
-    // TODO - no longer need NeedBinary
+    // To Be Done - no longer need NeedBinary
     var headerSerialized :- GetBinary(encRecord, HeaderPath);
     var footerSerialized :- GetBinary(encRecord, FooterPath);
     //= specification/structured-encryption/decrypt-structure.md#parse-the-header
@@ -919,7 +919,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //   and the key-value pairs in the [Encryption Context parsed from the header](./header.md#encryption-context).
     // - Algorithm Suite ID: The algorithm suite [indicated by the Message Format Flavor](./header.md#format-flavor)
     //   parsed in the header.
-    // - Encrypted Data Keys: The [Encrypted Data Keys parsed from the header](./header.md#encrypted-data-keys).  
+    // - Encrypted Data Keys: The [Encrypted Data Keys parsed from the header](./header.md#encrypted-data-keys).
 
     var matR := cmm.DecryptMaterials(
       CMP.DecryptMaterialsInput (

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -57,7 +57,7 @@ module StructuredEncryptionHeader {
   type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
   type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
 
-  predicate method IsVersion2Schema(data : CanonCryptoList) 
+  predicate method IsVersion2Schema(data : CanonCryptoList)
   {
     exists x <- data :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
   }

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -1,14 +1,17 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
 include "../Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy"
 include "Util.dfy"
 
 module SortCanon {
   export provides
-    AuthSort,
-    CryptoSort,
-    AuthBelow,
-    CryptoBelow,
-    StructuredEncryptionUtil,
-    Relations
+      AuthSort,
+      CryptoSort,
+      AuthBelow,
+      CryptoBelow,
+      StructuredEncryptionUtil,
+      Relations
 
   import opened Wrappers
   import opened StandardLibrary

DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

@@ -170,7 +170,7 @@ module TestHeader {
     expect legend == [ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND, ENCRYPT_AND_SIGN_LEGEND, SIGN_ONLY_LEGEND];
   }
 
-    method {:test} {:vcs_split_on_every_assert} TestSchemaOrderLength2() {
+  method {:test} {:vcs_split_on_every_assert} TestSchemaOrderLength2() {
     var schemaMap : CryptoList := [
       MakeCrypto("aa", ENCRYPT_AND_SIGN),
       MakeCrypto("zzz", ENCRYPT_AND_SIGN),