chore: update MPL submodule (#476)

josecorella · web-flow · commit de3a9f3e230e · 2023-10-05T20:00:38.000-04:00
* chore: update MPL submodule, bouncycastle, Dafny 4.2
diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml
@@ -63,7 +63,7 @@ jobs:
         uses: dafny-lang/setup-dafny-action@v1.6.1
         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
diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml
@@ -59,7 +59,7 @@ jobs:
         uses: dafny-lang/setup-dafny-action@v1.6.1
         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
diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml
@@ -60,7 +60,7 @@ jobs:
         uses: dafny-lang/setup-dafny-action@v1.6.1
         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 }}
diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml
@@ -41,7 +41,7 @@ jobs:
       - name: Setup Dafny
         uses: dafny-lang/setup-dafny-action@v1.6.1
         with:
-          dafny-version: '4.1.0'
+          dafny-version: '4.2.0'
 
       - name: Setup Java ${{ matrix.java-version }}
         uses: actions/setup-java@v3
diff --git a/.github/workflows/ci_verification.yml b/.github/workflows/ci_verification.yml
@@ -50,7 +50,7 @@ jobs:
         uses: dafny-lang/setup-dafny-action@v1.6.1
         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
diff --git a/.gitmodules b/.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
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ExecuteTransactionTransform.dfy b/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.");
       }
     }
diff --git a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj b/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>
 
     <!--
diff --git a/TestVectors/README.md b/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.
diff --git a/codebuild/release/release-prod.yml b/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
diff --git a/codebuild/release/validate-release.yml b/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
diff --git a/codebuild/staging/release-staging.yml b/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
diff --git a/codebuild/staging/validate-staging.yml b/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
diff --git a/project.properties b/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
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 13e0ac3c3c5eea83494706e4a96f40126d8f38a8
+Subproject commit cce342923ce5602f2e6162dccca44ecefaffca68

Original file line number	Diff line number	Diff line change
`@@ -41,12 +41,15 @@ module ExecuteTransactionTransform {`
`41`	`41`	`{`
`42`	`42`	`for i := 0 to \|input.sdkInput.TransactStatements\|`
`43`	`43`	`invariant forall x : nat \| 0 <= x < i ::`
`44`		`- var statement := DdbStatement.TableFromStatement(input.sdkInput.TransactStatements[x].Statement);`
`45`		`- statement.Success? && statement.value !in config.tableEncryptionConfigs;`
	`44`	`+ var tableName := DdbStatement.TableFromStatement(input.sdkInput.TransactStatements[x].Statement);`
	`45`	`+ tableName.Success? && tableName.value !in config.tableEncryptionConfigs`
`46`	`46`	`{`
`47`	`47`	`var statement := input.sdkInput.TransactStatements[i].Statement;`
`48`		`- var tableName :- MapString(DdbStatement.TableFromStatement(statement));`
`49`		`- if tableName in config.tableEncryptionConfigs {`
	`48`	`+ var tableName := DdbStatement.TableFromStatement(statement);`
	`49`	`+ if tableName.Failure? {`
	`50`	`+ return Failure(Error.DynamoDbEncryptionTransformsException(message := tableName.error));`
	`51`	`+ }`
	`52`	`+ if tableName.value in config.tableEncryptionConfigs {`
`50`	`53`	`return MakeError("ExecuteTransaction not Supported on encrypted tables.");`
`51`	`54`	`}`
`52`	`55`	`}`