feat: Support CollectionOfErrors error message (#219)

Co-authored-by: lavaleri <[email protected]>

Author: texastony

.github/workflows/ci_examples_java.yml

@@ -44,7 +44,7 @@ jobs:
       contents: read
     steps:
       - name: Configure AWS Credentials
-        uses: aws-actions/configure-aws-credentials@v1
+        uses: aws-actions/configure-aws-credentials@v2
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2

.github/workflows/ci_test_java.yml

@@ -46,7 +46,7 @@ jobs:
       contents: read
     steps:
       - name: Configure AWS Credentials
-        uses: aws-actions/configure-aws-credentials@v1
+        uses: aws-actions/configure-aws-credentials@v2
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2

.github/workflows/ci_test_net.yml

@@ -78,7 +78,7 @@ jobs:
         run: make setup_net
 
       - name: Configure AWS Credentials
-        uses: aws-actions/configure-aws-credentials@v1
+        uses: aws-actions/configure-aws-credentials@v2
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2

.github/workflows/ci_test_vector_java.yml

@@ -29,7 +29,7 @@ jobs:
           cors: '*'
 
       - name: Configure AWS Credentials
-        uses: aws-actions/configure-aws-credentials@v1
+        uses: aws-actions/configure-aws-credentials@v2
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -419,7 +419,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  // || (!exit(A(I)) && !exit(B(I)))
  // || (!access(A(I)) && !exit(B(I)))
  // || (!exit(A(I)) && !access(B(I)))
- | CollectionOfErrors(list: seq<Error>)
+ | CollectionOfErrors(list: seq<Error>, nameonly message: string)
  // The Opaque error, used for native, extern, wrapped or unknown errors
  | Opaque(obj: object)
  type OpaqueError = e: Error | e.Opaque? witness *

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -834,7 +834,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  // || (!exit(A(I)) && !exit(B(I)))
  // || (!access(A(I)) && !exit(B(I)))
  // || (!exit(A(I)) && !access(B(I)))
- | CollectionOfErrors(list: seq<Error>)
+ | CollectionOfErrors(list: seq<Error>, nameonly message: string)
  // The Opaque error, used for native, extern, wrapped or unknown errors
  | Opaque(obj: object)
  type OpaqueError = e: Error | e.Opaque? witness *

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -152,7 +152,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  // || (!exit(A(I)) && !exit(B(I)))
  // || (!access(A(I)) && !exit(B(I)))
  // || (!exit(A(I)) && !access(B(I)))
- | CollectionOfErrors(list: seq<Error>)
+ | CollectionOfErrors(list: seq<Error>, nameonly message: string)
  // The Opaque error, used for native, extern, wrapped or unknown errors
  | Opaque(obj: object)
  type OpaqueError = e: Error | e.Opaque? witness *

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy

@@ -124,6 +124,7 @@ module
       assert UnreservedPrefix(attributeName);
       assert UnreservedPrefix(attributeNames[i]);
     }
+
     assert (forall attribute <- attributeNames :: UnreservedPrefix(attribute));
     assert (forall attribute <- config.attributeActionsOnEncrypt.Keys :: UnreservedPrefix(attribute));
     assert (forall attribute <- config.attributeActionsOnEncrypt.Keys :: !(ReservedPrefix <= attribute));
@@ -201,6 +202,12 @@ module
     assert Operations.ValidInternalConfig?(internalConfig);
 
     var client := new DynamoDbItemEncryptorClient(internalConfig);
+
+    assert fresh(client.Modifies
+      - ( if config.keyring.Some? then config.keyring.value.Modifies else {})
+      - ( if config.cmm.Some? then config.cmm.value.Modifies else {} )
+      - ( if config.legacyOverride.Some? then config.legacyOverride.value.encryptor.Modifies else {}));
+
     return Success(client);
   }
 

DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

@@ -206,7 +206,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  // || (!exit(A(I)) && !exit(B(I)))
  // || (!access(A(I)) && !exit(B(I)))
  // || (!exit(A(I)) && !access(B(I)))
- | CollectionOfErrors(list: seq<Error>)
+ | CollectionOfErrors(list: seq<Error>, nameonly message: string)
  // The Opaque error, used for native, extern, wrapped or unknown errors
  | Opaque(obj: object)
  type OpaqueError = e: Error | e.Opaque? witness *

DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java

@@ -84,7 +84,8 @@ public static Error Error(CollectionOfErrors nativeValue) {
         nativeValue.list(), 
         ToDafny::Error, 
         Error._typeDescriptor());
-    return Error.create_CollectionOfErrors(list);
+    DafnySequence<? extends Character> message = software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(nativeValue.getMessage());
+    return Error.create_CollectionOfErrors(list, message);
   }
 
   public static BeaconVersion BeaconVersion(