Skip to content

Commit fedc0ad

Browse files
josecorellajosecorella
authored
feat: bump to dafny 4.8.0 and mpl 1.6.0 (#1356)
* feat: move to dafny 4.8.0
1 parent 8849c1e commit fedc0ad

File tree

52 files changed

+881
-88
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

52 files changed

+881
-88
lines changed

‎.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
#
2+
# This local action sets up code dependencies
3+
# to run Smithy-Dafny CI in GitHub Actions workflows.
4+
#
5+
6+
name: "Install Smithy-Dafny codegen dependencies"
7+
description: "Install Java package dependencies required to run Smithy-Dafny codegen"
8+
runs:
9+
using: "composite"
10+
steps:
11+
- name: Install smithy-dafny-codegen Rust dependencies locally
12+
uses: gradle/gradle-build-action@v2
13+
with:
14+
arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
15+
build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
16+
17+
- name: Install smithy-dafny-codegen Python dependencies locally
18+
uses: gradle/gradle-build-action@v2
19+
with:
20+
arguments: :smithy-python-codegen:pTML
21+
build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen

‎.github/workflows/ci_codegen.yml

+11-1
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ jobs:
3333
- uses: actions/checkout@v3
3434
with:
3535
submodules: recursive
36+
- run: git submodule update --init --recursive submodules/smithy-dafny
3637

3738
# Only used to format generated code
3839
# and to translate version strings such as "nightly-latest"
@@ -47,8 +48,17 @@ jobs:
4748
with:
4849
dotnet-version: ${{ matrix.dotnet-version }}
4950

51+
- name: Setup Java 17 for codegen
52+
uses: actions/setup-java@v3
53+
with:
54+
distribution: "corretto"
55+
java-version: "17"
56+
57+
- name: Install Smithy-Dafny codegen dependencies
58+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
59+
5060
- uses: ./.github/actions/polymorph_codegen
5161
with:
52-
dafny: ${{ env.DAFNY_VERSION }}
62+
dafny: ${{ inputs.dafny }}
5363
library: ${{ matrix.library }}
5464
diff-generated-code: true

‎DynamoDbEncryption/.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
TestResults
22
ImplementationFromDafny.cs
33
TestsFromDafny.cs
4+
ImplementationFromDafny-cs.dtr
5+
TestsFromDafny-cs.dtr
46
**/bin
57
**/obj
68
node_modules

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
2+
index 9601968..a2a04f8 100644
3+
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
4+
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
5+
@@ -7,10 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
6+
{
7+
public static class TypeConversion
8+
{
9+
- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
10+
-
11+
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
12+
+ // BEGIN MANUAL EDIT
13+
+ 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)
14+
+ {
15+
+ if (value is software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient dafnyValue)
16+
+ {
17+
+ return new AWS.Cryptography.KeyStore.KeyStore(dafnyValue);
18+
+ }
19+
+ throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
20+
+ }
21+
+ 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)
22+
+ {
23+
+ if (value is AWS.Cryptography.KeyStore.KeyStore nativeValue)
24+
+ {
25+
+ return nativeValue.impl();
26+
+ }
27+
+ throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
28+
+ }
29+
+ 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)
30+
+ {
31+
+ if (value is NativeWrapper_LegacyDynamoDbEncryptor nativeWrapper) return nativeWrapper._impl;
32+
+ return new LegacyDynamoDbEncryptor(value);
33+
34+
+ }
35+
+ 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)
36+
+ {
37+
+ switch (value)
38+
+ {
39+
+ case LegacyDynamoDbEncryptor valueWithImpl:
40+
+ return valueWithImpl._impl;
41+
+ case LegacyDynamoDbEncryptorBase nativeImpl:
42+
+ return new NativeWrapper_LegacyDynamoDbEncryptor(nativeImpl);
43+
+ default:
44+
+ throw new System.ArgumentException(
45+
+ "Custom implementations of LegacyDynamoDbEncryptor must extend LegacyDynamoDbEncryptorBase.");
46+
+ }
47+
+ }
48+
+ // END MANUAL EDIT
49+
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)
50+
{
51+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
2+
index 2f95341..36226d3 100644
3+
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
4+
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
5+
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
6+
{
7+
public static class TypeConversion
8+
{
9+
- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
10+
-
11+
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
12+
-
13+
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)
14+
{
15+
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;

‎DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
2+
index da904fc..c5b0bed 100644
3+
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
4+
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
5+
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
6+
{
7+
public static class TypeConversion
8+
{
9+
- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
10+
-
11+
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
12+
-
13+
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)
14+
{
15+
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;

‎DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
diff --git b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
2+
index d0a4e58..4e9890c 100644
3+
--- b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
4+
+++ a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
5+
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.StructuredEncryption
6+
{
7+
public static class TypeConversion
8+
{
9+
- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
10+
-
11+
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
12+
-
13+
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)
14+
{
15+
if (value.is_SIGN) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction.SIGN;

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy

+25-25
Original file line numberDiff line numberDiff line change
@@ -237,31 +237,31 @@ module TestFixtures {
237237
assume {:axiom} fresh(encryption.Modifies);
238238
}
239239

240-
method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
241-
returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
242-
ensures encryption.ValidState()
243-
ensures fresh(encryption)
244-
ensures fresh(encryption.Modifies)
245-
{
246-
var keyring := GetKmsKeyring();
247-
encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
248-
DynamoDbTablesEncryptionConfig(
249-
tableEncryptionConfigs := map[
250-
"foo" := DynamoDbTableEncryptionConfig(
251-
logicalTableName := "foo",
252-
partitionKeyName := "bar",
253-
sortKeyName := sortKey,
254-
attributeActionsOnEncrypt := actions,
255-
allowedUnsignedAttributes := Some(["plain"]),
256-
allowedUnsignedAttributePrefix := None(),
257-
algorithmSuiteId := None(),
258-
keyring := Some(keyring)
259-
)
260-
]
261-
)
262-
);
263-
assume {:axiom} fresh(encryption.Modifies);
264-
}
240+
// method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option<string>)
241+
// returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient)
242+
// ensures encryption.ValidState()
243+
// ensures fresh(encryption)
244+
// ensures fresh(encryption.Modifies)
245+
// {
246+
// var keyring := GetKmsKeyring();
247+
// encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms(
248+
// DynamoDbTablesEncryptionConfig(
249+
// tableEncryptionConfigs := map[
250+
// "foo" := DynamoDbTableEncryptionConfig(
251+
// logicalTableName := "foo",
252+
// partitionKeyName := "bar",
253+
// sortKeyName := sortKey,
254+
// attributeActionsOnEncrypt := actions,
255+
// allowedUnsignedAttributes := Some(["plain"]),
256+
// allowedUnsignedAttributePrefix := None(),
257+
// algorithmSuiteId := None(),
258+
// keyring := Some(keyring)
259+
// )
260+
// ]
261+
// )
262+
// );
263+
// assume {:axiom} fresh(encryption.Modifies);
264+
// }
265265

266266
// type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
267267

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java

+10-2
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,17 @@ > GetBranchKeyIdFromDdbKey(
103103
this._impl.GetBranchKeyIdFromDdbKey(nativeInput);
104104
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput dafnyOutput =
105105
ToDafny.GetBranchKeyIdFromDdbKeyOutput(nativeOutput);
106-
return Result.create_Success(dafnyOutput);
106+
return Result.create_Success(
107+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
108+
Error._typeDescriptor(),
109+
dafnyOutput
110+
);
107111
} catch (RuntimeException ex) {
108-
return Result.create_Failure(ToDafny.Error(ex));
112+
return Result.create_Failure(
113+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
114+
Error._typeDescriptor(),
115+
ToDafny.Error(ex)
116+
);
109117
}
110118
}
111119

0 commit comments

Comments
 (0)