feat: repair dependencies in item encryptor (#465)

* feat: repair dependencies in item encryptor et al

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -4,6 +4,8 @@
 include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  include "../../DynamoDbEncryption/src/Index.dfy"
  include "../../DynamoDbItemEncryptor/src/Index.dfy"
+ include "../../StructuredEncryption/src/Index.dfy"
+ include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy"
  include "../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy"
  module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transforms.internaldafny.types" } AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes
  {
@@ -12,6 +14,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  import opened UTF8
  import AwsCryptographyDbEncryptionSdkDynamoDbTypes
  import AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
+ import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
+ import AwsCryptographyMaterialProvidersTypes
  import ComAmazonawsDynamodbTypes
  // Generic helpers for verification of mock/unit tests.
  datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
@@ -696,6 +700,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  // Any dependent models are listed here
  | AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDb: AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error)
  | AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor: AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error)
+ | AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryption: AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error)
+ | AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders: AwsCryptographyMaterialProvidersTypes.Error)
  | ComAmazonawsDynamodb(ComAmazonawsDynamodb: ComAmazonawsDynamodbTypes.Error)
  // The Collection error is used to collect several errors together
  // This is useful when composing OR logic.

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy

@@ -11,6 +11,8 @@ use com.amazonaws.dynamodb#AttributeMap
 use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
 use aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor#DynamoDbItemEncryptor
 use aws.cryptography.dbEncryptionSdk.dynamoDb#VersionNumber
+use aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption
+use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
 
 use aws.polymorph#localService
 use aws.polymorph#javadoc
@@ -22,6 +24,7 @@ use aws.polymorph#javadoc
     DynamoDB_20120810,
     DynamoDbEncryption,
     DynamoDbItemEncryptor,
+    StructuredEncryption
   ]
 )
 service DynamoDbEncryptionTransforms {
@@ -96,8 +99,15 @@ structure DynamoDbItemEncryptorReference {}
 @aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption)
 structure DynamoDbEncryptionReference {}
 
+@aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption)
+structure StructuredEncryptionReference {}
+
+@aws.polymorph#reference(service: aws.cryptography.materialProviders#AwsCryptographicMaterialProviders)
+structure AwsCryptographicMaterialProvidersReference {}
+
 @error("client")
 structure DynamoDbEncryptionTransformsException {
   @required
   message: String,
 }
+

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -3,6 +3,7 @@
 // Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
 include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  include "../../DynamoDbEncryption/src/Index.dfy"
+ include "../../StructuredEncryption/src/Index.dfy"
  include "../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy"
  include "../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/src/Index.dfy"
  include "../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/src/Index.dfy"
@@ -12,6 +13,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  import opened StandardLibrary.UInt
  import opened UTF8
  import AwsCryptographyDbEncryptionSdkDynamoDbTypes
+ import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
  import AwsCryptographyMaterialProvidersTypes
  import AwsCryptographyPrimitivesTypes
  import ComAmazonawsDynamodbTypes
@@ -126,6 +128,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  )
  // Any dependent models are listed here
  | AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDb: AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error)
+ | AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryption: AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error)
  | AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders: AwsCryptographyMaterialProvidersTypes.Error)
  | AwsCryptographyPrimitives(AwsCryptographyPrimitives: AwsCryptographyPrimitivesTypes.Error)
  | ComAmazonawsDynamodb(ComAmazonawsDynamodb: ComAmazonawsDynamodbTypes.Error)

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy

@@ -23,6 +23,7 @@ use aws.cryptography.dbEncryptionSdk.dynamoDb#PlaintextOverride
 use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
 use aws.cryptography.primitives#AwsCryptographicPrimitives
 use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
+use aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption
 
 @localService(
   sdkId: "DynamoDbItemEncryptor",
@@ -31,7 +32,8 @@ use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
     AwsCryptographicPrimitives,
     DynamoDB_20120810,
     AwsCryptographicMaterialProviders,
-    DynamoDbEncryption
+    StructuredEncryption,
+    DynamoDbEncryption,
   ]
 )
 service DynamoDbItemEncryptor {
@@ -206,6 +208,8 @@ structure DecryptItemOutput {
 
 @aws.polymorph#reference(service: aws.cryptography.primitives#AwsCryptographicPrimitives)
 structure AtomicPrimitivesReference {}
+@aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption)
+structure StructuredEncryptionReference {}
 
 /////////////
 // Errors

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

@@ -62,6 +62,9 @@ public static RuntimeException Error(Error dafnyValue) {
     if (dafnyValue.is_AwsCryptographyMaterialProviders()) {
       return software.amazon.cryptography.materialproviders.ToNative.Error(dafnyValue.dtor_AwsCryptographyMaterialProviders());
     }
+    if (dafnyValue.is_AwsCryptographyDbEncryptionSdkStructuredEncryption()) {
+      return software.amazon.cryptography.dbencryptionsdk.structuredencryption.ToNative.Error(dafnyValue.dtor_AwsCryptographyDbEncryptionSdkStructuredEncryption());
+    }
     if (dafnyValue.is_AwsCryptographyDbEncryptionSdkDynamoDb()) {
       return software.amazon.cryptography.dbencryptionsdk.dynamodb.ToNative.Error(dafnyValue.dtor_AwsCryptographyDbEncryptionSdkDynamoDb());
     }

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

@@ -115,6 +115,9 @@ public static RuntimeException Error(Error dafnyValue) {
     if (dafnyValue.is_AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor()) {
       return software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative.Error(dafnyValue.dtor_AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor());
     }
+    if (dafnyValue.is_AwsCryptographyDbEncryptionSdkStructuredEncryption()) {
+      return software.amazon.cryptography.dbencryptionsdk.structuredencryption.ToNative.Error(dafnyValue.dtor_AwsCryptographyDbEncryptionSdkStructuredEncryption());
+    }
     OpaqueError.Builder nativeBuilder = OpaqueError.builder();
     nativeBuilder.obj(dafnyValue);
     return nativeBuilder.build();

DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

@@ -11,7 +11,7 @@
 
     <ItemGroup>
         <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
-        <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
+        <PackageReference Include="DafnyRuntime" Version="4.2.0" />
         <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
         <!--
           System.Collections.Immutable can be removed once dafny.msbuild is updated with