Design support for @streaming trait (including hand-written TestModel)

[robin-aws]

Depends on https://github.com/dafny-lang/libraries/issues/70 to first define the idiomatic representation of streams in Dafny.

[robin-aws]

Renamed this to reflect the need for defining what the Dafny interfaces to implement will look like, and how they will be adapted to the various kinds of streaming input/output types each target language supports.

[kessplas]

Support for the @streaming trait entails support for both data streams and event streams as described in the Smithy docs.

An example of an operation requiring streaming support is S3::PutObject:

        "com.amazonaws.s3#PutObject": {
            "type": "operation",
            "input": {
                "target": "com.amazonaws.s3#PutObjectRequest"
            },
            "output": {
                "target": "com.amazonaws.s3#PutObjectOutput"
            },
...
        "com.amazonaws.s3#PutObjectRequest": {
            "type": "structure",
            "members": {
                "ACL": {
                    "target": "com.amazonaws.s3#ObjectCannedACL",
                    "traits": {
                        "smithy.api#documentation": "[...]",
                        "smithy.api#httpHeader": "x-amz-acl"
                    }
                },
                "Body": {
                    "target": "com.amazonaws.s3#StreamingBlob",
                    "traits": {
                        "smithy.api#default": "",
                        "smithy.api#documentation": "<p>Object data.</p>",
                        "smithy.api#httpPayload": {}
                    }
                },
...
        "com.amazonaws.s3#StreamingBlob": {
            "type": "blob",
            "traits": {
                "smithy.api#streaming": {}
            }
        },

An example of code generated from this model can be found withIn the AWS SDK Go v2; the Body member of the PutObjectInput structure is an io.Reader.

In order to support S3 clients in the AWS SDK, Smithy-Dafny must support at least data streams to be able to generate Dafny code that can interact with services such as S3 which have @streaming traits in their models.

Event streams would allow Smithy-Dafny projects to support async streaming in the AWS SDK for Java which uses Reactive Streams to implement its event streaming functionality. Additionally, support for event streams would enable simpler implementations of other streaming functionality. Ideally, there would also be a way to convert between event streams and data streams.

[kessplas]

There are a number of examples of stream types in various "native" languages/runtimes that Smithy-Dafny will need to be able to handle. They can be broadly classified to one or more of each category:

• Smithy
• AWS SDKs (non-Smithy)
• Native code

In more detail:

Smithy

More specifically, this category refers to the streaming types which Smithy-* code generators generate. In some languages, such as Python and Go, this is defined by the existing codegen. In other languages, such as Java and .NET, this is subject to implementation with the codegen within Smithy-Dafny.

AWS SDKs

More specifically, this category refers to the streaming types which various AWS SDKs use. These may or may not match the streaming types produced by Smithy, depending on whether or not the given AWS SDK was generating using Smithy or not.

Native Code

This refers to streaming types which are found in the native language runtimes, and may be used in various implementations outside of the Smithy/AWS SDK dependency closure.

Examples

Java - Java.IO

InputStream

public abstract class InputStream implements Closeable {
    public abstract int read() throws IOException;
    public void close() throws IOException {}
}

OutputStream

public abstract class OutputStream implements Closeable, Flushable {
    public abstract void write(int b) throws IOException;
    public void flush() throws IOException {}
    public void close() throws IOException {}
}

Defined in the core java.io package. Used in the AWS SDK for Java v1 and v2 (and thus Amazon S3 Encryption Client) as well as the AWS Encryption SDK for Java. This stream API could be classified as a data stream, in the Smithy-parlance.

Java - ReactiveStreams

Subscriber

public interface Subscriber<T> {
    public void onSubscribe(Subscription s);

    public void onNext(T t);

    public void onError(Throwable t);

    public void onComplete();
}

See original source for Javadoc comments.

Publisher

public interface Publisher<T> {
    public void subscribe(Subscriber<? super T> s);
}

See original source for Javadoc comments.

Defined in the Reactive Streams library, not part of the core Java API. Used by the AWS SDK v2 to support asynchronous programming and thus the S3EC. Note that the AWS SDK also includes and uses the SdkPublisher interface which specifies additional methods. This stream API could be classified as an event stream, in the Smithy-parlance.

Currently, the Java codegen in Smithy-Dafny generates a ByteBuffer for blob shapes with the @streaming trait. I haven't tested event streams.

[kessplas]

Also, I have published a branch of Lucas's Python-POC which adds a simple Streaming test model: https://github.com/smithy-lang/smithy-dafny/tree/justplaz/python-poc-streaming