m

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -474,7 +474,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbService

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoDbEncryptionBranchKeyIdSupplier.dfy

@@ -70,7 +70,7 @@ module DynamoDbEncryptionBranchKeyIdSupplier {
     // We expect this interface to be implemented in the native language,
     // so any errors thrown by the native implementation will appear as Opaque errors
     if err.Opaque? then
-      MPL.Opaque(obj:=err.obj)
+      MPL.Opaque(obj:=err.obj, alt_text:=err.alt_text)
     else
       MPL.AwsCryptographicMaterialProvidersException(message:="Unexpected error while getting Branch Key ID.")
   }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy

@@ -728,7 +728,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
@@ -773,7 +773,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
                obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj
     modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true
                                                                            && t8.search.Some?
-                            , t9 <- t8.search.value.versions :: t9.keyStore,
+                            , t9 <- t8.search.value.versions | true
+                            :: t9.keyStore,
                obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj
     ensures res.Success? ==>
               && fresh(res.value)
@@ -792,7 +793,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
                                obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
                        ) - ( set tmps13 <- set t13 <- config.tableEncryptionConfigs.Values | true
                                                                                              && t13.search.Some?
-                                             , t14 <- t13.search.value.versions :: t14.keyStore,
+                                             , t14 <- t13.search.value.versions | true
+                                             :: t14.keyStore,
                                obj <- tmps13.Modifies | obj in tmps13.Modifies :: obj
                        ) )
               && fresh(res.value.History)

DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy

@@ -159,7 +159,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService

DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy

@@ -283,7 +283,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService

DynamoDbEncryption/runtimes/rust/src/intercept.rs

@@ -23,7 +23,6 @@ macro_rules! modify_request {
             .store_put(OriginalRequest(Input::erase($request.clone())));
 
         // transform the request
-        // *$request = tokio::task::block_in_place(|| {
         let result = tokio::task::block_in_place(|| {
             tokio::runtime::Handle::current().block_on(async {
                 $self