Implement smithy-dafny-codegen library that supports dafny-client-codegen smithy-build.json plugin for AWS SDK generation

[robin-aws]

This will support the standard workflow for generating a client for a given Smithy model, as described here: https://smithy.io/2.0/guides/using-code-generation/generating-a-client.html. Ours will only support AWS service models at first, since the implementation will emit Dafny and target language code to wrap up existing AWS SDKs.

This should be mostly wrapping up existing functionality in this tool. There are some minor open design questions about how to configure things, since in our case we will be emitting a project that will handle one or more Dafny-supported target languages.

The workflow for users should be perfectly parallel to how it works for other smithy-<language> tools:

1. Add the common software.amazon.smithy Gradle plugin
2. Add this new smithy-dafny-codegen library as an implementation dependency
3. Configure the dafny-codegen Smithy build plugin in a smithy-build.json file.

A typical smithy-build.json file might look something like this:

{
    "version": "1.0",
    "plugins": {
        "dafny-codegen": {
            "service": "com.amazonaws.kms#TrentService",
            "targetLanguages": ["cs", "java"],
        }
    }
}

(The configuration for a given SmithyBuildPlugin seems to be an arbitrary JSON object, and we'll likely need more properties)

Given this configuration, the plugin should output a "complete Dafny project" just as other codegen plugins do - e.g. see this documentation about the typescript-codegen plugin: https://smithy.io/2.0/guides/using-code-generation/generating-a-client.html#add-the-codegen-plugin. The definition of a "Dafny project" is fuzzy at the time of writing this, however. I would suggest generating a Makefile to build the result for the configured target languages, which will involve invoking dafny as well as target language tooling. In the future there should be more Dafny-native support for project management, such as dafny-lang/dafny#3169 and/or dafny-lang/dafny#2907, at which point we can offer a more standard output style option.

[robin-aws]

Corrected my understanding: there's one big "Smithy Gradle plugin" (https://github.com/awslabs/smithy-gradle-plugin/). Smithy has its own plugin mechanism that we need to implement: https://github.com/awslabs/smithy/blob/main/smithy-build/src/main/java/software/amazon/smithy/build/SmithyBuildPlugin.java

[alex-chew]

Note to self - check on the current best practice for configuring client region.

[robin-aws]

Note I'm going to cut a PR to add a new TestModel to show a complete example project for generating a Dafny client for a given AWS service. TTD FTW! :)

[robin-aws]

I have to do a bit more to hook it up to the CI, but this should help clarify the requirements beyond the issue description: https://github.com/awslabs/polymorph/tree/smithy-client-codegen-test-model/TestModels/aws-sdks/sqs

[robin-aws]

Another wrinkle: Smithy codegen has a notion of "edition": https://smithy.io/2.0/guides/building-codegen/configuring-the-generator.html#edition

That applies equally well to smithy-dafny, as how we map Smithy shapes to Dafny types will evolve over time just as it does in other languages. But our implementation of wrapping existing SDKs means we have to know the "edition" of those SDKs too. The existing codegen CLI is already modeling this concept with switches like --java-aws-sdk-version. We'll need an equivalent bit of smithy-build.json configuration, unless we can somehow discover this metadata on the target language SDK software artifacts.