Skip to content

Commit 0067712

Browse files
author
Shubham Chaturvedi
committed
feat: All shapes complete
1 parent d3cd446 commit 0067712

File tree

12 files changed

+522
-527
lines changed

12 files changed

+522
-527
lines changed

AwsEncryptionSDK/Makefile

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,9 @@ GO_DEPENDENCY_MODULE_NAMES := \
4848
--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/kms \
4949
--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/mpl \
5050
--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/primitives \
51-
--dependency-library-name=aws.cryptography.materialProviders=github.com/aws/aws-cryptographic-material-providers-library/mpl
51+
--dependency-library-name=aws.cryptography.materialProviders=github.com/aws/aws-cryptographic-material-providers-library/mpl \
52+
--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
53+
--dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms
5254

5355

5456
TRANSLATION_RECORD_GO := \

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -175,8 +175,15 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types"
175175
// || (!exit(A(I)) && !access(B(I)))
176176
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
177177
// The Opaque error, used for native, extern, wrapped or unknown errors
178-
| Opaque(obj: object, alt_text : string)
178+
| Opaque(obj: object)
179179
type OpaqueError = e: Error | e.Opaque? witness *
180+
// This dummy subset type is included to make sure Dafny
181+
// always generates a _ExternBase___default.java class.
182+
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
183+
predicate method IsDummySubsetType(x: int) {
184+
0 < x
185+
}
186+
180187
}
181188
abstract module AbstractAwsCryptographyEncryptionSdkService
182189
{

AwsEncryptionSDK/project.properties

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
# This file stores the top level dafny version information.
22
# All elements of the project need to agree on this version.
3-
dafnyVersion=4.8.0
4-
dafnyRuntimeJavaVersion=4.8.0
3+
dafnyVersion=4.8.1
4+
dafnyRuntimeJavaVersion=4.8.1

AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService/shim.go

Lines changed: 1 addition & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)