Skip to content

feat: repair dependencies in item encryptor #465

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Sep 29, 2023
Merged

feat: repair dependencies in item encryptor #465

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
790fd8e
feat: repair dependencies in item encryptor
ajewellamz Sep 29, 2023
df81395
update dafny runtime to match mpl
ajewellamz Sep 29, 2023
103dce3
repair transforms dependencies
ajewellamz Sep 29, 2023
d3f74fd
more dependencies
ajewellamz Sep 29, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions ...amoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
{
Expand All @@ -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)
Expand Down Expand Up @@ -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.
Expand Down
10 changes: 10 additions & 0 deletions ...DbEncryption/dafny/DynamoDbEncryptionTransforms/Model/DynamoDbEncryptionTransforms.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -22,6 +24,7 @@ use aws.polymorph#javadoc
DynamoDB_20120810,
DynamoDbEncryption,
DynamoDbItemEncryptor,
StructuredEncryption
]
)
service DynamoDbEncryptionTransforms {
Expand Down Expand Up @@ -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 {}
Comment on lines +102 to +106
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Issue: We SHOULD NOT need these.
I know you slacked me, stating this solved an issue.
I would like to understand why/how this solved that issue.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Resolving this and will Approve the PR.

We SHOULD create a GHI against Smithy-Dafny for this,
describing the problem (dependency error discovery when generating Dafny)
the solution (use LocalService's dependencies field for error and include discovery)
and the work around (add references to the local model).


@error("client")
structure DynamoDbEncryptionTransformsException {
@required
message: String,
}

3 changes: 3 additions & 0 deletions .../DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand Down
6 changes: 5 additions & 1 deletion DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -31,7 +32,8 @@ use aws.cryptography.dbEncryptionSdk.dynamoDb#DynamoDbEncryption
AwsCryptographicPrimitives,
DynamoDB_20120810,
AwsCryptographicMaterialProviders,
DynamoDbEncryption
StructuredEncryption,
DynamoDbEncryption,
]
)
service DynamoDbItemEncryptor {
Expand Down Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions ...nerated/software/amazon/cryptography/dbencryptionsdk/dynamodb/itemencryptor/ToNative.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
}
Expand Down
3 changes: 3 additions & 0 deletions ...-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/transforms/ToNative.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
2 changes: 1 addition & 1 deletion DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down