From 790fd8ebfb5bc96f7e14dd20c117f0e0691afb6c Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 29 Sep 2023 09:23:00 -0400
Subject: [PATCH 1/4] feat: repair dependencies in item encryptor

---
 ...ryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy | 3 +++
 .../Model/DynamoDbItemEncryptor.smithy                      | 6 +++++-
 .../dbencryptionsdk/dynamodb/itemencryptor/ToNative.java    | 3 +++
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy
index b8f56e854..22e6c6737 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy
+++ b/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)
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
index 1898aabd3..eea12cbdb 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
+++ b/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
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToNative.java
index d75c1557b..eca5d5e0b 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToNative.java
+++ b/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());
     }

From df81395188923e1c701c2ee1e29b9f55a2c9be42 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 29 Sep 2023 09:27:55 -0400
Subject: [PATCH 2/4] update dafny runtime to match mpl

---
 DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj b/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
index d10e7485e..06ca3fb03 100644
--- a/DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
+++ b/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

From 103dce327080e74fca9fc0acf9c900bf3fadfb83 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 29 Sep 2023 09:46:47 -0400
Subject: [PATCH 3/4] repair transforms dependencies

---
 .../Model/DynamoDbEncryptionTransforms.smithy                | 5 +++++
 .../dbencryptionsdk/dynamodb/transforms/ToNative.java        | 3 +++
 2 files changed, 8 insertions(+)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
index 8a5ee8974..a03e06297 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
@@ -11,6 +11,7 @@ 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.polymorph#localService
 use aws.polymorph#javadoc
@@ -22,6 +23,7 @@ use aws.polymorph#javadoc
     DynamoDB_20120810,
     DynamoDbEncryption,
     DynamoDbItemEncryptor,
+    StructuredEncryption
   ]
 )
 service DynamoDbEncryptionTransforms {
@@ -96,6 +98,9 @@ structure DynamoDbItemEncryptorReference {}
 @aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption)
 structure DynamoDbEncryptionReference {}
 
+@aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption)
+structure StructuredEncryptionReference {}
+
 @error("client")
 structure DynamoDbEncryptionTransformsException {
   @required
diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToNative.java
index 158939c10..e50bde40c 100644
--- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToNative.java
+++ b/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();

From d3f74fda8c031706474c1e070712e7ce4881d284 Mon Sep 17 00:00:00 2001
From: Andy Jewell <ajewell@amazon.com>
Date: Fri, 29 Sep 2023 10:05:43 -0400
Subject: [PATCH 4/4] more dependencies

---
 ...wsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy | 6 ++++++
 .../Model/DynamoDbEncryptionTransforms.smithy               | 5 +++++
 2 files changed, 11 insertions(+)

diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
index af0673b39..8d9f2b539 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
+++ b/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.
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
index a03e06297..191202af9 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
@@ -12,6 +12,7 @@ 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
@@ -101,8 +102,12 @@ 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,
 }
+