You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This turns out to be a difference in error reporting between the Java and .NET KMS SDKs. I was able to diagnosis it pretty quickly after reproducing by adding a second argument to the expect statement (which is printed when the expect fails):
expect beaconKeyResultSr.error == Types.Error.ComAmazonawsKms(ComAmazonawsKmsTypes.Error.IncorrectKeyException(message := Some("The key ID in the request does not identify a CMK that can perform this operation."))), beaconKeyResultSr.error;
Because the test failure then says:
TestDiscoveryGetKeys.TestGetKeysForMrk: FAILED
dafny/AwsCryptographyKeyStore/test/TestDiscoveryGetKeys.dfy(155,4): AwsCryptographyKeyStoreTypes.Error.ComAmazonawsKms(ComAmazonawsKmsTypes.Error.IncorrectKeyException(Wrappers.Option.Some(The key ID in the request does not identify a CMK that can perform this operation. (Service: Kms, Status Code: 400, Request ID: b57aa5dd-6b23-43b8-ac11-ccc7b7f474d2))))
i.e. the Java SDK appends extra information to the error message that the .NET SDK does not.
Although there's no soundness bug here, it's worth figuring out how to avoid recurrence since this could be a common trap for smithy-dafny users, since "Dafny code, regardless of which runtime language it is compiled to, MUST behave the same." depends heavily on external code behaving the same as well.
Interesting.
My solution was to verify the Error Type, but not the Error Message.
i.e: expect nestedError.IncorrectKeyException?;, as compared to Expecting a long string to be equal.
Issue
Dafny code, regardless of which runtime language it is compiled to, MUST behave the same.
However, an integration test in the AWS Cryptographic Material Providers Library
reliably passed in .NET but failed in Java.
This suggests a behavioral difference in the Java and .NET artifacts
created by Dafny & Smithy-Dafny.
Reproduction
git clone --recurse-submodules git@github.com:aws/aws-cryptographic-material-providers-library.git
git checkout -track --recurse-submodules origin/tony/feat-keystore-kms-config
git checkout 0c7ae78287ba81191b8d7ca4bcf022636fe0e8d4
cd AwsCryptographicMaterialProviders; make build_java; make test_java
make transpile_net; make test_net FRAMEWORK=net6.0
The text was updated successfully, but these errors were encountered: