search

smithy-lang / smithy-dafny

Apache License 2.0
7 stars 8 forks source link

[.NET & Java] Expect Equivlence check across runtimes yields different results #362

Open texastony opened 1 month ago

texastony commented 1 month ago

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

  1. Clone the MPL: git clone --recurse-submodules git@github.com:aws/aws-cryptographic-material-providers-library.git
  2. Checkout the branch with the interesting commit: git checkout -track --recurse-submodules origin/tony/feat-keystore-kms-config
  3. Checkout the interesting commit: git checkout 0c7ae78287ba81191b8d7ca4bcf022636fe0e8d4
  4. Build and test Java, notice failure: cd AwsCryptographicMaterialProviders; make build_java; make test_java
  5. Build and test .NET, notice success: make transpile_net; make test_net FRAMEWORK=net6.0
robin-aws commented 1 month ago

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.

texastony commented 1 month ago

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.