chore(dotnet): release 4.1.1

.github/workflows/pull.yml

@@ -8,20 +8,20 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
-  #     dafny: '4.2.0'
+  #     dafny: '4.9.0'
   pr-ci-net:
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy

@@ -17,7 +17,7 @@ include "Serialize/EncryptionContext.dfy"
 
 module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOperations {
 
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
   import EncryptDecryptHelpers

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy

@@ -15,7 +15,7 @@ module EncryptDecryptHelpers {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MessageBody
   import SerializableTypes
   import opened SerializeFunctions

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy

@@ -7,7 +7,7 @@ module
   {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" }
   EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService {
   import Operations = AwsEncryptionSdkOperations
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MaterialProviders
   import AwsCryptographyMaterialProvidersTypes
 

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy

@@ -12,7 +12,7 @@ module KeyDerivation {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import HeaderTypes
   import SerializableTypes
 

AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy

@@ -22,7 +22,7 @@ module MessageBody {
   import opened UInt = StandardLibrary.UInt
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Streams
   import UTF8
   import SerializableTypes

AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy

@@ -9,7 +9,7 @@ module Fixtures {
   import primitivesTypes = AwsCryptographyPrimitivesTypes
   import mplTypes = AwsCryptographyMaterialProvidersTypes
   import opened UInt = StandardLibrary.UInt
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
 
   // The following are test resources that exist in tests accounts:
 
@@ -20,7 +20,7 @@ module Fixtures {
 
   const branchKeyStoreName := "KeyStoreDdbTable"
   const logicalKeyStoreName := branchKeyStoreName
-  const branchKeyId := "75789115-1deb-4fe3-a2ec-be9e885d1945"
+  const branchKeyId := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
 
   // UTF-8 encoded "aws-crypto-"
   const RESERVED_ENCRYPTION_CONTEXT: UTF8.ValidUTF8Bytes :=

AwsEncryptionSDK/runtimes/net/CHANGELOG.md

@@ -1,5 +1,9 @@
 # Changelog
 
+## 4.1.1
+
+Update .csproj files to prevent use of AWS-SDK-NET V4
+
 ## 4.1.0
 
 ### Notes

AwsEncryptionSDK/runtimes/net/ESDK.csproj

@@ -8,7 +8,7 @@
       <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
       <IsPackable>true</IsPackable>
 
-      <Version>4.1.0</Version>
+      <Version>4.1.1</Version>
 
       <AssemblyName>AWS.Cryptography.EncryptionSDK</AssemblyName>
       <PackageId>AWS.Cryptography.EncryptionSDK</PackageId>
@@ -29,11 +29,8 @@
   </PropertyGroup>
 
   <ItemGroup>
-      <!-- TODO: manually upgraded to match the latest from MPL, is that reasonable? -->
-      <PackageReference Include="AWSSDK.Core" Version="3.7.300.2" />
-      <PackageReference Include="DafnyRuntime" Version="4.2.0" />
-      <PackageReference Include="BouncyCastle.Cryptography" Version="2.2.1" />
-      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="1.3.0" />
+      <PackageReference Include="DafnyRuntime" Version="[4.2.0,4.8.0]" />
+      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[1.7.6]" />
       <!--
         System.Collections.Immutable can be removed once dafny.msbuild is updated with
         https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned

SharedMakefileV2.mk

@@ -6,9 +6,19 @@
 # that are shared by all libraries in this repo.
 PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
 
-SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/smithy-dafny
+SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/mpl/smithy-dafny
 GRADLEW := ./runtimes/java/gradlew
 
 VERIFY_TIMEOUT := 150
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
+
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+
+transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
+transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts
+
+transpile_implementation_java: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
+transpile_test_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts