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

[robin-aws]

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]

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.