Skip to content

Commit 962c6ff

Browse files
ajewellamzajewellamz
committed
rebuild release
1 parent 05a5085 commit 962c6ff

File tree

1,976 files changed

+160300
-461744
lines changed

Some content is hidden

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

1,976 files changed

+160300
-461744
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -476,8 +476,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
476476
// || (!exit(A(I)) && !access(B(I)))
477477
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
478478
// The Opaque error, used for native, extern, wrapped or unknown errors
479-
| Opaque(obj: object, alt_text : string)
480-
type OpaqueError = e: Error | e.Opaque? witness *
479+
| Opaque(obj: object)
480+
// A better Opaque, with a visible string representation.
481+
| OpaqueWithText(obj: object, objMessage : string)
482+
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
483+
// This dummy subset type is included to make sure Dafny
484+
// always generates a _ExternBase___default.java class.
485+
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
486+
predicate method IsDummySubsetType(x: int) {
487+
0 < x
488+
}
489+
481490
}
482491
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
483492
{

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
7070
// We expect this interface to be implemented in the native language,
7171
// so any errors thrown by the native implementation will appear as Opaque errors
7272
if err.Opaque? then
73-
MPL.Opaque(obj:=err.obj, alt_text:=err.alt_text)
73+
MPL.Opaque(obj:=err.obj)
7474
else
7575
MPL.AwsCryptographicMaterialProvidersException(message:="Unexpected error while getting Branch Key ID.")
7676
}

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -728,8 +728,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
728728
// || (!exit(A(I)) && !access(B(I)))
729729
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
730730
// The Opaque error, used for native, extern, wrapped or unknown errors
731-
| Opaque(obj: object, alt_text : string)
732-
type OpaqueError = e: Error | e.Opaque? witness *
731+
| Opaque(obj: object)
732+
// A better Opaque, with a visible string representation.
733+
| OpaqueWithText(obj: object, objMessage : string)
734+
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
735+
// This dummy subset type is included to make sure Dafny
736+
// always generates a _ExternBase___default.java class.
737+
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
738+
predicate method IsDummySubsetType(x: int) {
739+
0 < x
740+
}
741+
733742
}
734743
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
735744
{

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -159,8 +159,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
159159
// || (!exit(A(I)) && !access(B(I)))
160160
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
161161
// The Opaque error, used for native, extern, wrapped or unknown errors
162-
| Opaque(obj: object, alt_text : string)
163-
type OpaqueError = e: Error | e.Opaque? witness *
162+
| Opaque(obj: object)
163+
// A better Opaque, with a visible string representation.
164+
| OpaqueWithText(obj: object, objMessage : string)
165+
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
166+
// This dummy subset type is included to make sure Dafny
167+
// always generates a _ExternBase___default.java class.
168+
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
169+
predicate method IsDummySubsetType(x: int) {
170+
0 < x
171+
}
172+
164173
}
165174
abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
166175
{

‎DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -283,8 +283,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
283283
// || (!exit(A(I)) && !access(B(I)))
284284
| CollectionOfErrors(list: seq<Error>, nameonly message: string)
285285
// The Opaque error, used for native, extern, wrapped or unknown errors
286-
| Opaque(obj: object, alt_text : string)
287-
type OpaqueError = e: Error | e.Opaque? witness *
286+
| Opaque(obj: object)
287+
// A better Opaque, with a visible string representation.
288+
| OpaqueWithText(obj: object, objMessage : string)
289+
type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
290+
// This dummy subset type is included to make sure Dafny
291+
// always generates a _ExternBase___default.java class.
292+
type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
293+
predicate method IsDummySubsetType(x: int) {
294+
0 < x
295+
}
296+
288297
}
289298
abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
290299
{

‎DynamoDbEncryption/runtimes/rust/dafny_runtime_rust/Cargo.toml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ version = "0.1.0"
44
edition = "2021"
55

66
[dependencies]
7-
once_cell = "1.20.2"
8-
num = "0.4.3"
9-
itertools = "0.13.0"
7+
once_cell = "1.18.0"
8+
num = "0.4"
9+
itertools = "0.11.0"

0 commit comments

Comments
 (0)