smithy-dafny-codegen

smithy-dafny-codegen

This library supports the standard Smithy workflow for generating a Dafny client for a given Smithy model, as described in the Smithy codegen docs.

WARNING: All internal and external interfaces are considered unstable and subject to change without notice. This includes the interfaces in the code generated by this library.

Limitations

1. Dafny supports compilation to multiple other target programming languages, but of those targets, this plugin currently only supports .NET. Experimental support for Java exists but does not yet work for arbitrary service models.
2. This plugin does not yet handle all Smithy features, and may hit errors or generate incorrect code for some models. See the section below on "Using projections" for details on how to cleanly avoid unsupported features.

Generating a client

This repository builds Dafny declarations and Dafny clients from Smithy models.

For now the library only supports AWS service models, since the implementation will generate both Dafny code and target language code to wrap existing AWS SDKs. This means only services with the aws.api#service trait are supported.

The TestModel/sqs package in this repo is an example of how to build a Dafny client. The steps needed to build a Dafny client are as follows:

1. Create a new directory for your package. For example, "foo-client".

2. Create a build.gradle.kts file with the following contents:

    buildscript {
        repositories {
            mavenCentral()
        }
        dependencies {
            "classpath"("software.amazon.smithy:smithy-cli:1.28.1")
        }
    }
   
    plugins {
        id("software.amazon.smithy").version("0.6.0")
    }
   
    repositories {
        mavenLocal()
        mavenCentral()
    }
   
    dependencies {
        implementation("software.amazon.smithy:smithy-model:1.28.1")
        implementation("software.amazon.smithy:smithy-aws-traits:1.28.1")
        implementation("software.amazon.smithy.dafny:smithy-dafny-codegen:0.1.0")
    }

   You may need additional Smithy dependencies depending on what Smithy features your service model depends on, such as AWS-specific traits. See https://smithy.io/2.0/guides/using-code-generation/index.html for more examples.

   Note the exact version of the software.amazon.smithy dependencies MAY NOT need to be 1.28.1 exactly, but MUST be consistent.

3. Make a copy of the TestModels/dafny-dependencies/StandardLibrary directory for the generated code to refer to.

   This is necessary because the runtime library code the generated code will depend on is not yet available as a shared Dafny library.

4. Create a smithy-build.json file with the following contents, substituting "smithy.example#ExampleService" with the name of the service to generate a client for, and specifying the set of target languages to support in the generated client:

   {
     "version": "1.0",
     "plugins": {
       "dafny-client-codegen": {
         "edition": "2023.10",
         "service": "smithy.example#ExampleService",
         "targetLanguages": ["dotnet"],
         "dafnyVersion": "4.3.0",
         "includeDafnyFile": "[relative]/[path]/[to]/StandardLibrary/src/Index.dfy"
       }
     }
   }

   See DafnyClientCodegenPluginSettings.java for more details about plugin settings.

5. Create a directory named model. This is where all of your Smithy models will go.

6. Copy the model for the service into the model directory. The Smithy models for AWS services can be found in several Smithy-based SDK projects, such as https://github.com/aws/aws-sdk-js-v3/tree/main/codegen/sdk-codegen/aws-models.

7. Run gradle build (alternatively, you can use a Gradle wrapper).

8. The generated client can be found under the build/smithyprojections, the exact path depending on the name of the service. For example, build/smithyprojections/example-client/source/dafny-client-codegen.

See the Smithy documentation for more information on building Smithy projects with Gradle.

Using projections

This plugin does not yet handle all Smithy features, especially since at the time of writing this, Dafny itself does not have a strongly idiomatic representation for some concepts. Fortunately, the Smithy Gradle plugin provides several "transforms" that can be used to filter a service model to remove unsupported shapes.

The following example removes all operations that transitively refer to one of the shape types that this plugin does not yet support:

{
  "version": "1.0",
  "projections": {
    "dafny-supported": {
      "transforms": [
        {
          "name": "excludeShapesBySelector",
          "args": {
            "selector": "operation :test(~> document)"
          }
        },
        {
          "name": "removeUnusedShapes",
          "args": {}
        }
      ],
      "plugins": {
        "dafny-client-codegen": {
          "service": "smithy.example#ExampleService",
          "targetLanguages": ["dotnet"],
          "includeDafnyPath": "[relative]/[path]/[to]/smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/src/Index.dfy"
        }
      }
    }
  }
}

Note that if you are using transformations to avoid unsupported features, the plugin has to be applied specifically to projections that use such transformations, and not at the top level were it will be applied to all projections. Otherwise the built-in "source" projection will still hit errors.

Refer to the Smithy documentation for more information about other transforms that might be useful, but bear in mind that removing arbitrary shapes may lead to a client that will fail to compile or not function correctly.

Development

The file layout of the library follows the Codegen repo layout described in the Smithy documentation.

Most configuration (e.g. config) and build files (e.g. build.gradle.kts) were adapted from the corresponding files in the smithy-typescript and/or smithy-go repositories.