feat: bump to dafny 4.8.0 and mpl 1.6.0 (#1356)

* feat: move to dafny 4.8.0
aws · Sep 16, 2024 · fedc0ad · fedc0ad
1 parent 8849c1e
commit fedc0ad
Show file tree

Hide file tree

Showing 52 changed files with 881 additions and 88 deletions.
diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml
@@ -0,0 +1,21 @@
+#
+# This local action sets up code dependencies
+# to run Smithy-Dafny CI in GitHub Actions workflows.
+#
+
+name: "Install Smithy-Dafny codegen dependencies"
+description: "Install Java package dependencies required to run Smithy-Dafny codegen"
+runs:
+  using: "composite"
+  steps:
+    - name: Install smithy-dafny-codegen Rust dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
+        build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
+
+    - name: Install smithy-dafny-codegen Python dependencies locally
+      uses: gradle/gradle-build-action@v2
+      with:
+        arguments: :smithy-python-codegen:pTML
+        build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen
diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml
@@ -33,6 +33,7 @@ jobs:
       - uses: actions/checkout@v3
         with:
           submodules: recursive
+      - run: git submodule update --init --recursive submodules/smithy-dafny
 
       # Only used to format generated code
       # and to translate version strings such as "nightly-latest"
@@ -47,8 +48,17 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - uses: ./.github/actions/polymorph_codegen
         with:
-          dafny: ${{ env.DAFNY_VERSION }}
+          dafny: ${{ inputs.dafny }}
           library: ${{ matrix.library }}
           diff-generated-code: true
diff --git a/DynamoDbEncryption/.gitignore b/DynamoDbEncryption/.gitignore
@@ -1,6 +1,8 @@
 TestResults
 ImplementationFromDafny.cs
 TestsFromDafny.cs
+ImplementationFromDafny-cs.dtr
+TestsFromDafny-cs.dtr
 **/bin
 **/obj
 node_modules

diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,51 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+index 9601968..a2a04f8 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
+@@ -7,10 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
++    // BEGIN MANUAL EDIT
++    public static AWS.Cryptography.KeyStore.KeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient value)
++    {
++      if (value is software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient dafnyValue)
++      {
++        return new AWS.Cryptography.KeyStore.KeyStore(dafnyValue);
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(AWS.Cryptography.KeyStore.KeyStore value)
++    {
++      if (value is AWS.Cryptography.KeyStore.KeyStore nativeValue)
++      {
++        return nativeValue.impl();
++      }
++      throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
++    }
++    public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value)
++    {
++      if (value is NativeWrapper_LegacyDynamoDbEncryptor nativeWrapper) return nativeWrapper._impl;
++      return new LegacyDynamoDbEncryptor(value);
+
++    }
++    public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value)
++    {
++      switch (value)
++      {
++        case LegacyDynamoDbEncryptor valueWithImpl:
++          return valueWithImpl._impl;
++        case LegacyDynamoDbEncryptorBase nativeImpl:
++          return new NativeWrapper_LegacyDynamoDbEncryptor(nativeImpl);
++        default:
++          throw new System.ArgumentException(
++              "Custom implementations of LegacyDynamoDbEncryptor must extend LegacyDynamoDbEncryptorBase.");
++      }
++    }
++    // END MANUAL EDIT
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+index 2f95341..36226d3 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbTablesEncryptionConfig value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig(); converted.TableEncryptionConfigs = (System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTableEncryptionConfig>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig__M22_tableEncryptionConfigs(concrete._tableEncryptionConfigs); return converted;
diff --git a/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+index da904fc..c5b0bed 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput value)
+     {
+       software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput(); converted.EncryptedItem = (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(concrete._encryptedItem); return converted;
diff --git a/DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch b/DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch
@@ -0,0 +1,15 @@
+diff --git b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
+index d0a4e58..4e9890c 100644
+--- b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
++++ a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
+@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.StructuredEncryption
+ {
+   public static class TypeConversion
+   {
+-    private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
+-
+-    private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
+-
+     public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S18_AuthenticateAction(software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._IAuthenticateAction value)
+     {
+       if (value.is_SIGN) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction.SIGN;
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy
@@ -237,31 +237,31 @@ module TestFixtures {
     assume {:axiom} fresh(encryption.Modifies);
   }
 
-  method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
-    returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
-    ensures encryption.ValidState()
-    ensures fresh(encryption)
-    ensures fresh(encryption.Modifies)
-  {
-    var keyring := GetKmsKeyring();
-    encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
-      DynamoDbTablesEncryptionConfig(
-        tableEncryptionConfigs := map[
-          "foo" := DynamoDbTableEncryptionConfig(
-            logicalTableName := "foo",
-            partitionKeyName := "bar",
-            sortKeyName := sortKey,
-            attributeActionsOnEncrypt := actions,
-            allowedUnsignedAttributes := Some(["plain"]),
-            allowedUnsignedAttributePrefix := None(),
-            algorithmSuiteId := None(),
-            keyring := Some(keyring)
-          )
-        ]
-      )
-    );
-    assume {:axiom} fresh(encryption.Modifies);
-  }
+  // method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
+  //   returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
+  //   ensures encryption.ValidState()
+  //   ensures fresh(encryption)
+  //   ensures fresh(encryption.Modifies)
+  // {
+  //   var keyring := GetKmsKeyring();
+  //   encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
+  //     DynamoDbTablesEncryptionConfig(
+  //       tableEncryptionConfigs := map[
+  //         "foo" := DynamoDbTableEncryptionConfig(
+  //           logicalTableName := "foo",
+  //           partitionKeyName := "bar",
+  //           sortKeyName := sortKey,
+  //           attributeActionsOnEncrypt := actions,
+  //           allowedUnsignedAttributes := Some(["plain"]),
+  //           allowedUnsignedAttributePrefix := None(),
+  //           algorithmSuiteId := None(),
+  //           keyring := Some(keyring)
+  //         )
+  //       ]
+  //     )
+  //   );
+  //   assume {:axiom} fresh(encryption.Modifies);
+  // }
 
   // type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
 

diff --git a/...software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java b/...software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java
@@ -103,9 +103,17 @@ > GetBranchKeyIdFromDdbKey(
           this._impl.GetBranchKeyIdFromDdbKey(nativeInput);
         software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput dafnyOutput =
           ToDafny.GetBranchKeyIdFromDdbKeyOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }