search

smithy-lang / smithy-dafny

Apache License 2.0
10 stars 8 forks source link

Smithy-generated Dafny interface allows custom implementations of non-@extendable resources #671

Open robin-aws opened 1 month ago

robin-aws commented 1 month ago

Found this while working on SQSExtended in #666.

I neglected to add @extendable to my resource, but was able to write a successful Dafny test of the local service. Then I tried a Java equivalent, and it threw an IllegalArgumentException saying custom implementations are not supported. I'm glad Java correctly respected the Smithy model, but it would have saved a fair bit of time if Dafny did in the first place.

Bonus marks if we can encode this as a requires clause somewhere so Dafny code that tries to provide a custom implementation doesn't even verify. :)

texastony commented 1 month ago

When you say the Dafny does not prevent this, do you mean you can write Dafny source code that extends non-extendable resources?

If so... I am not certain this impacts Smithy-Dafny consumers very much, if those consumers are like Crypto Tools.

i.e: I have a hard time imagining a Crypto Tools customer writing a Dafny implemention of the MPL's Key Store.