chore: update MPL submodule

.github/workflows/ci_examples_java.yml

@@ -63,7 +63,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Build and locally deploy dependencies for examples
         shell: bash

.github/workflows/ci_test_java.yml

@@ -59,7 +59,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Setup Java ${{ matrix.java-version }}
         uses: actions/setup-java@v3

.github/workflows/ci_test_net.yml

@@ -60,7 +60,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Download Dependencies 
         working-directory: ./${{ matrix.library }}

.github/workflows/ci_test_vector_java.yml

@@ -41,7 +41,7 @@ jobs:
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: '4.1.0'
+          dafny-version: '4.2.0'
 
       - name: Setup Java ${{ matrix.java-version }}
         uses: actions/setup-java@v3

.github/workflows/ci_verification.yml

@@ -50,7 +50,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "submodules/MaterialProviders"]
 	path = submodules/MaterialProviders
-	url = https://github.com/aws/aws-cryptographic-material-providers-library-java.git
+	url = https://github.com/aws/aws-cryptographic-material-providers-library-dafny.git
 [submodule "submodules/smithy-dafny"]
 	path = submodules/smithy-dafny
 	url = https://github.com/awslabs/smithy-dafny.git

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ExecuteTransactionTransform.dfy

@@ -41,12 +41,15 @@ module ExecuteTransactionTransform {
   {
     for i := 0 to |input.sdkInput.TransactStatements|
       invariant forall x : nat | 0 <= x < i ::
-        var statement := DdbStatement.TableFromStatement(input.sdkInput.TransactStatements[x].Statement);
-        statement.Success? && statement.value !in config.tableEncryptionConfigs;
+        var tableName := DdbStatement.TableFromStatement(input.sdkInput.TransactStatements[x].Statement);
+        tableName.Success? && tableName.value !in config.tableEncryptionConfigs
     {
       var statement := input.sdkInput.TransactStatements[i].Statement;
-      var tableName :- MapString(DdbStatement.TableFromStatement(statement));
-      if tableName in config.tableEncryptionConfigs {
+      var tableName := DdbStatement.TableFromStatement(statement);
+      if tableName.Failure? {
+        return Failure(Error.DynamoDbEncryptionTransformsException(message := tableName.error));
+      }
+      if tableName.value in config.tableEncryptionConfigs {
         return MakeError("ExecuteTransaction not Supported on encrypted tables.");
       }
     }

DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

@@ -5,14 +5,14 @@
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>disable</Nullable>
         <LangVersion>10</LangVersion>
-        <TargetFrameworks>net6.0</TargetFrameworks>
+        <TargetFrameworks>net6.0;net48</TargetFrameworks>
         <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
     </PropertyGroup>
 
     <ItemGroup>
         <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
         <PackageReference Include="DafnyRuntime" Version="4.2.0" />
-        <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
+        <PackageReference Include="BouncyCastle.Cryptography" Version="2.2.1" />
         <!--
           System.Collections.Immutable can be removed once dafny.msbuild is updated with
           https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
@@ -27,10 +27,11 @@
     </ItemGroup>
 
     <ItemGroup>
-        <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj" />
-        <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj" />
-        <ProjectReference Include="../../../submodules/MaterialProviders/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj" />
-        <ProjectReference Include="../../../submodules/MaterialProviders/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj" />
+        <PackageReference Include="AWS.Cryptography.Internal.StandardLibrary" Version="1.1.1" />
+        <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="1.0.0" />
+        <PackageReference Include="AWS.Cryptography.Internal.AwsCryptographyPrimitives" Version="1.0.0" />
+        <PackageReference Include="AWS.Cryptography.Internal.ComAmazonawsDynamodb" Version="1.0.0" />
+        <PackageReference Include="AWS.Cryptography.Internal.ComAmazonawsKms" Version="1.0.0" />
     </ItemGroup>
 
     <!--

TestVectors/README.md

@@ -7,7 +7,7 @@ This validates the Database Encryption SDK's cross-version compatibility.
 
 ### Development Requirements
 
-* Dafny 4.1.0: https://github.com/dafny-lang/dafny
+* Dafny 4.2.0: https://github.com/dafny-lang/dafny
 
   The code that executes the test vectors is written in Dafny. 
   You must install the Dafny runtime to compile the Dafny tests into Java.

codebuild/release/release-prod.yml

@@ -21,7 +21,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.2.0/dafny-4.2.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6

codebuild/release/validate-release.yml

@@ -14,7 +14,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.2.0/dafny-4.2.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6

codebuild/staging/release-staging.yml

@@ -21,7 +21,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.2.0/dafny-4.2.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6

codebuild/staging/validate-staging.yml

@@ -18,7 +18,7 @@ phases:
     commands:
       - cd ..
       # Get Dafny
-      - curl https://github.com/dafny-lang/dafny/releases/download/v4.1.0/dafny-4.1.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
+      - curl https://github.com/dafny-lang/dafny/releases/download/v4.2.0/dafny-4.2.0-x64-ubuntu-20.04.zip  -L -o dafny.zip
       - unzip -qq dafny.zip && rm dafny.zip
       - export PATH="$PWD/dafny:$PATH"
       # Get Gradle 7.6

project.properties

@@ -1,4 +1,4 @@
 projectJavaVersion=3.1.0
 mplDependencyJavaVersion=1.0.0
-dafnyRuntimeJavaVersion=4.1.0
+dafnyRuntimeJavaVersion=4.2.0
 smithyDafnyJavaConversionVersion=0.1