Merge branch 'main' into scchatur/PerfTest

Author: ShubhamChaturvedi7

.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
@@ -92,5 +92,6 @@ jobs:
           # Run simple examples
           gradle -p runtimes/java/DynamoDbEncryption test 
           # Run migration examples
+          gradle -p runtimes/java/Migration/PlaintextToAWSDBE test
           gradle -p runtimes/java/Migration/DDBECToAWSDBE test
 

.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

CONTRIBUTING.md

@@ -56,4 +56,4 @@ If you discover a potential security issue in this project we ask that you notif
 
 ## Licensing
 
-See the [LICENSE](LICENSE) file for our project's licensing. We will ask you to confirm the licensing of your contribution.
+See the [LICENSE](LICENSE.txt) file for our project's licensing. We will ask you to confirm the licensing of your contribution.

DynamoDbEncryption/README.md

@@ -1,8 +1,10 @@
-## DynamoDb Encryption
+## DynamoDbEncryption
+
+This project implements the AWS Database Encryption SDK for DynamoDB.
 
 ### Code Organization
 
-DynamoDb Encryption is a project containing the following Dafny 'localServices' under `dafny`:
+DynamoDbEncryption is a project containing the following Dafny 'localServices' under `dafny`:
 - DynamoDbEncryption: A config-less entry point for shared structures and helper methods related to DDB Encryption.
 - DynamoDbItemEncryptor: A client responsible for the encryption and decryption of DDB Items (sans any DDB API call).
 - DynamoDbEncryptionTransforms: An internal interface responsible for appropriately adding encryption to DDB APIs.
@@ -63,7 +65,8 @@ Common Makefile targets are:
 
 ### Development Requirements
 
-TODO
+* Dafny 4.1.0: https://github.com/dafny-lang/dafny
+* A Java 8 or newer development environment
 
 #### (Optional) Dafny Report Generator Requirements
 

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 *