diff --git a/.github/not-grep.toml b/.github/not-grep.toml deleted file mode 100644 index cd59507f15..0000000000 --- a/.github/not-grep.toml +++ /dev/null @@ -1,30 +0,0 @@ -[prefix] -"**/[!smithy-dafny-codegen-modules]/**/*.smithy" = """ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 -""" -"**/[!smithy-dafny-codegen-modules]/**/*.java" = """ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 -""" -"**/[!smithy-dafny-codegen-modules]/**/[!/obj/]*.cs" = """ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 -""" -# Exclude files from dafny-lang/libraries -"**/[!Wrappers]*.dfy" = """ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 -""" -"**/[!smithy-dafny-codegen-modules]/**/*.kts" = """ -// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 -""" -"**/[!smithy-dafny-codegen-modules]/**/*.mk" = """ -# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 -""" -"**/[!smithy-dafny-codegen-modules]/**/Makefile" = """ -# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. -# SPDX-License-Identifier: Apache-2.0 -""" \ No newline at end of file diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 2889b0d658..566c62f731 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -10,10 +10,10 @@ jobs: steps: - name: Populate Dafny versions list id: populate-dafny-versions-list - run: echo "dafny-versions-list=['4.5.0','4.8.0']" >> $GITHUB_OUTPUT + run: echo "dafny-versions-list=['4.7.0','4.9.1']" >> $GITHUB_OUTPUT - name: Populate Dafny versions list for "only new versions" languages (Python) id: populate-only-new-dafny-versions-list - run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT + run: echo "only-new-dafny-versions-list=['4.9.1']" >> $GITHUB_OUTPUT outputs: dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }} only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }} diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 8faf4ee73d..04d6304626 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -12,10 +12,10 @@ jobs: steps: - name: Populate Dafny versions list id: populate-dafny-versions-list - run: echo "dafny-versions-list=['4.5.0','4.8.0']" >> $GITHUB_OUTPUT + run: echo "dafny-versions-list=['4.5.0','4.9.1']" >> $GITHUB_OUTPUT - name: Populate Dafny versions list for "only new versions" languages (Python, Go) id: populate-only-new-dafny-versions-list - run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT + run: echo "only-new-dafny-versions-list=['4.9.1']" >> $GITHUB_OUTPUT outputs: dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }} only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }} diff --git a/.github/workflows/smithy-polymorph.yml b/.github/workflows/smithy-polymorph.yml index d15b18dfa4..3891b9c1a9 100644 --- a/.github/workflows/smithy-polymorph.yml +++ b/.github/workflows/smithy-polymorph.yml @@ -17,10 +17,12 @@ jobs: - uses: actions/checkout@v3 with: submodules: recursive + - uses: actions/setup-java@v3 with: distribution: "corretto" java-version: "17" + - name: Setup Dafny uses: dafny-lang/setup-dafny-action@v1.7.0 with: @@ -45,7 +47,3 @@ jobs: shell: bash working-directory: TestModels/SimpleTypes/SimpleString run: make polymorph_dafny - - - name: not-grep - if: matrix.os == 'ubuntu-22.04' - uses: mattsb42-meta/not-grep@1.0.0 diff --git a/.gitmodules b/.gitmodules index 03f9a1246c..15a4a6d0c9 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,7 @@ [submodule "smithy-dafny-codegen-modules/smithy-rs"] path = smithy-dafny-codegen-modules/smithy-rs url = https://github.com/smithy-lang/smithy-rs.git +[submodule "TestModels/dafny-dependencies/dafny"] + path = TestModels/dafny-dependencies/dafny + url = git@github.com:dafny-lang/dafny.git + branch = actions-and-streaming-stdlibs diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk index 1efcc850cf..ea3a254053 100644 --- a/SmithyDafnyMakefile.mk +++ b/SmithyDafnyMakefile.mk @@ -95,6 +95,7 @@ verify: --log-format csv \ --verification-time-limit $(VERIFY_TIMEOUT) \ --resource-limit $(MAX_RESOURCE_COUNT) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES), --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(DAFNY_OPTIONS) \ % @@ -110,6 +111,7 @@ verify_single: --log-format text \ --verification-time-limit $(VERIFY_TIMEOUT) \ --resource-limit $(MAX_RESOURCE_COUNT) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES), --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(DAFNY_OPTIONS) \ $(if ${PROC},-proc:*$(PROC)*,) \ $(FILE) @@ -207,6 +209,7 @@ transpile_implementation: $(DAFNY_OTHER_FILES) \ $(TRANSPILE_MODULE_NAME) \ $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(TRANSLATION_RECORD) \ $(TRANSPILE_DEPENDENCIES) @@ -245,6 +248,7 @@ transpile_test: $(DAFNY_OPTIONS) \ $(DAFNY_OTHER_FILES) \ $(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(TRANSLATION_RECORD) \ $(SOURCE_TRANSLATION_RECORD) \ $(TRANSPILE_MODULE_NAME) \ @@ -253,7 +257,7 @@ transpile_test: # If we are not the StandardLibrary, transpile the StandardLibrary. # Transpile all other dependencies transpile_dependencies: - $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG), ) + $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG) USE_DAFNY_STANDARD_LIBRARIES=$(USE_DAFNY_STANDARD_LIBRARIES), ) $(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES)) transpile_dependencies_test: @@ -326,7 +330,7 @@ _polymorph_wrapped: $(POLYMORPH_OPTIONS)"; _polymorph_dependencies: - $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) polymorph_$(POLYMORPH_LANGUAGE_TARGET) LIBRARY_ROOT=$(PROJECT_ROOT)/$(STD_LIBRARY), ) + $(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) polymorph_$(POLYMORPH_LANGUAGE_TARGET) LIBRARY_ROOT=$(PROJECT_ROOT)/$(STD_LIBRARY) USE_DAFNY_STANDARD_LIBRARIES=$(USE_DAFNY_STANDARD_LIBRARIES), ) @$(foreach dependency, \ $(PROJECT_DEPENDENCIES), \ $(MAKE) -C $(PROJECT_ROOT)/$(dependency) polymorph_$(POLYMORPH_LANGUAGE_TARGET); \ @@ -695,6 +699,8 @@ test_go: ########################## Python targets +python: polymorph_dafny transpile_python polymorph_python test_python + # Install packages via `python3 -m pip`, # which is the syntax Smithy-Python and Smithy-Dafny Python use # to invoke these packages. diff --git a/TestModels/Streaming/Makefile b/TestModels/Streaming/Makefile index d92cec9292..0aca2882f2 100644 --- a/TestModels/Streaming/Makefile +++ b/TestModels/Streaming/Makefile @@ -3,6 +3,10 @@ CORES=2 +USE_DAFNY_STANDARD_LIBRARIES=1 + +ENABLE_EXTERN_PROCESSING=1 + include ../SharedMakefile.mk NAMESPACE=simple.streaming @@ -18,4 +22,26 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy # This project has no dependencies # DEPENDENT-MODELS:= + +# Python + +PYTHON_MODULE_NAME=simple_streaming + +TRANSLATION_RECORD_PYTHON := \ + --translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr + # LIBRARIES := + +# Constants for languages that drop extern names (Python, Go) + +TYPES_FILE_PATH=Model/SimpleStreamingTypes.dfy +TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.streaming.internaldafny.types\" } SimpleStreamingTypes" +TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleStreamingTypes" + +INDEX_FILE_PATH=src/Index.dfy +INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.streaming.internaldafny\"} SimpleStreaming refines AbstractSimpleStreamingService" +INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleStreaming refines AbstractSimpleStreamingService" + +WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleStreamingImpl.dfy +WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.streaming.internaldafny.wrapped\"} WrappedSimpleStreamingService refines WrappedAbstractSimpleStreamingService" +WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleStreamingService refines WrappedAbstractSimpleStreamingService" \ No newline at end of file diff --git a/TestModels/Streaming/Model/SimpleStreamingTypes.dfy b/TestModels/Streaming/Model/SimpleStreamingTypes.dfy new file mode 100644 index 0000000000..c047e70e0d --- /dev/null +++ b/TestModels/Streaming/Model/SimpleStreamingTypes.dfy @@ -0,0 +1,351 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../../dafny-dependencies/StandardLibrary/src/Index.dfy" +module {:extern "simple.streaming.internaldafny.types" } SimpleStreamingTypes +{ + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Std.Streams + // Generic helpers for verification of mock/unit tests. + datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) + + // Begin Generated Types + + datatype BinaryOfInput = | BinaryOfInput ( + nameonly number: int32 + ) + datatype BinaryOfOutput = | BinaryOfOutput ( + nameonly binary: ByteStream + ) + datatype ChunksInput = | ChunksInput ( + nameonly bytesIn: ByteStream , + nameonly chunkSize: CountingInteger + ) + datatype ChunksOutput = | ChunksOutput ( + nameonly bytesOut: ByteStream + ) + datatype CountBitsInput = | CountBitsInput ( + nameonly bits: ByteStream + ) + datatype CountBitsOutput = | CountBitsOutput ( + nameonly sum: int32 + ) + type CountingInteger = x: int32 | IsValid_CountingInteger(x) witness * + predicate method IsValid_CountingInteger(x: int32) { + ( 1 <= x ) + } + class ISimpleStreamingClientCallHistory { + ghost constructor() { + CountBits := []; + BinaryOf := []; + Chunks := []; + } + ghost var CountBits: seq>> + ghost var BinaryOf: seq>> + ghost var Chunks: seq>> + } + trait {:termination false} ISimpleStreamingClient + { + // Helper to define any additional modifies/reads clauses. + // If your operations need to mutate state, + // add it in your constructor function: + // Modifies := {your, fields, here, History}; + // If you do not need to mutate anything: + // Modifies := {History}; + + ghost const Modifies: set + // For an unassigned field defined in a trait, + // Dafny can only assign a value in the constructor. + // This means that for Dafny to reason about this value, + // it needs some way to know (an invariant), + // about the state of the object. + // This builds on the Valid/Repr paradigm + // To make this kind requires safe to add + // to methods called from unverified code, + // the predicate MUST NOT take any arguments. + // This means that the correctness of this requires + // MUST only be evaluated by the class itself. + // If you require any additional mutation, + // then you MUST ensure everything you need in ValidState. + // You MUST also ensure ValidState in your constructor. + predicate ValidState() + ensures ValidState() ==> History in Modifies + ghost const History: ISimpleStreamingClientCallHistory + predicate CountBitsEnsuresPublicly(input: CountBitsInput , output: Result) + // The public method to be called by library consumers + method CountBits ( input: CountBitsInput ) + returns (output: Result) + requires + && ValidState() + // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` part. + requires + && input.bits.Valid() && History !in input.bits.Repr + modifies Modifies - {History} , + History`CountBits , + input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures CountBitsEnsuresPublicly(input, output) + ensures History.CountBits == old(History.CountBits) + [DafnyCallEvent(input, output)] + + predicate BinaryOfEnsuresPublicly(input: BinaryOfInput , output: Result) + // The public method to be called by library consumers + method BinaryOf ( input: BinaryOfInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`BinaryOf + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures BinaryOfEnsuresPublicly(input, output) + ensures History.BinaryOf == old(History.BinaryOf) + [DafnyCallEvent(input, output)] + // TODO: smithy-dafny isn't yet generating this + ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) + // The public method to be called by library consumers + method Chunks ( input: ChunksInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`Chunks + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures ChunksEnsuresPublicly(input, output) + ensures History.Chunks == old(History.Chunks) + [DafnyCallEvent(input, output)] + // TODO: smithy-dafny isn't yet generating this + ensures output.Success? ==> output.value.bytesOut.Valid() && fresh(output.value.bytesOut.Repr) + + } + datatype SimpleStreamingConfig = | SimpleStreamingConfig ( + + ) + type StreamingBlob = ByteStream + datatype Error = + // Local Error structures are listed here + | OverflowError ( + nameonly message: string + ) + // Any dependent models are listed here + + // The Collection error is used to collect several errors together + // This is useful when composing OR logic. + // Consider the following method: + // + // method FN(n:I) + // returns (res: Result) + // ensures A(I).Success? ==> res.Success? + // ensures B(I).Success? ==> res.Success? + // ensures A(I).Failure? && B(I).Failure? ==> res.Failure? + // + // If either A || B is successful then FN is successful. + // And if A && B fail then FN will fail. + // But what information should FN transmit back to the caller? + // While it may be correct to hide these details from the caller, + // this can not be the globally correct option. + // Suppose that A and B can be blocked by different ACLs, + // and that their representation of I is only eventually consistent. + // How can the caller distinguish, at a minimum for logging, + // the difference between the four failure modes? + // || (!access(A(I)) && !access(B(I))) + // || (!exit(A(I)) && !exit(B(I))) + // || (!access(A(I)) && !exit(B(I))) + // || (!exit(A(I)) && !access(B(I))) + | CollectionOfErrors(list: seq, nameonly message: string) + // The Opaque error, used for native, extern, wrapped or unknown errors + | Opaque(obj: object) + // A better Opaque, with a visible string representation. + | OpaqueWithText(obj: object, objMessage : string) + type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness * + // This dummy subset type is included to make sure Dafny + // always generates a _ExternBase___default.java class. + type DummySubsetType = x: int | IsDummySubsetType(x) witness 1 + predicate method IsDummySubsetType(x: int) { + 0 < x + } + +} +abstract module AbstractSimpleStreamingService +{ + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Std.Streams + import opened Types = SimpleStreamingTypes + import Operations : AbstractSimpleStreamingOperations + function method DefaultSimpleStreamingConfig(): SimpleStreamingConfig + method SimpleStreaming(config: SimpleStreamingConfig := DefaultSimpleStreamingConfig()) + returns (res: Result) + ensures res.Success? ==> + && fresh(res.value) + && fresh(res.value.Modifies) + && fresh(res.value.History) + && res.value.ValidState() + + // Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals + function method CreateSuccessOfClient(client: ISimpleStreamingClient): Result { + Success(client) + } + function method CreateFailureOfError(error: Error): Result { + Failure(error) + } + class SimpleStreamingClient extends ISimpleStreamingClient + { + constructor(config: Operations.InternalConfig) + requires Operations.ValidInternalConfig?(config) + ensures + && ValidState() + && fresh(History) + && this.config == config + const config: Operations.InternalConfig + predicate ValidState() + ensures ValidState() ==> + && Operations.ValidInternalConfig?(config) + && History !in Operations.ModifiesInternalConfig(config) + && Modifies == Operations.ModifiesInternalConfig(config) + {History} + predicate CountBitsEnsuresPublicly(input: CountBitsInput , output: Result) + {Operations.CountBitsEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method CountBits ( input: CountBitsInput ) + returns (output: Result) + requires + && ValidState() + // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` parts. + requires + && input.bits.Valid() && History !in input.bits.Repr + modifies Modifies - {History} , + History`CountBits , + input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures CountBitsEnsuresPublicly(input, output) + ensures History.CountBits == old(History.CountBits) + [DafnyCallEvent(input, output)] + { + // TODO: It's not clear how to actually ensure this, + // since the internal config is not visible to the trait + // so it can't really be a precondition there. + assume {:axiom} Operations.ModifiesInternalConfig(config) !! input.bits.Repr; + output := Operations.CountBits(config, input); + History.CountBits := History.CountBits + [DafnyCallEvent(input, output)]; + } + + predicate BinaryOfEnsuresPublicly(input: BinaryOfInput , output: Result) + {Operations.BinaryOfEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method BinaryOf ( input: BinaryOfInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`BinaryOf + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures BinaryOfEnsuresPublicly(input, output) + ensures History.BinaryOf == old(History.BinaryOf) + [DafnyCallEvent(input, output)] + // TODO: smithy-dafny isn't yet generating this + ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + { + output := Operations.BinaryOf(config, input); + History.BinaryOf := History.BinaryOf + [DafnyCallEvent(input, output)]; + } + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) + {Operations.ChunksEnsuresPublicly(input, output)} + // The public method to be called by library consumers + method Chunks ( input: ChunksInput ) + returns (output: Result) + requires + && ValidState() + modifies Modifies - {History} , + History`Chunks + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures + && ValidState() + ensures ChunksEnsuresPublicly(input, output) + ensures History.Chunks == old(History.Chunks) + [DafnyCallEvent(input, output)] + { + output := Operations.Chunks(config, input); + History.Chunks := History.Chunks + [DafnyCallEvent(input, output)]; + } + + } +} +abstract module AbstractSimpleStreamingOperations { + import opened Wrappers + import opened StandardLibrary.UInt + import opened UTF8 + import opened Std.Streams + import opened Types = SimpleStreamingTypes + type InternalConfig + predicate ValidInternalConfig?(config: InternalConfig) + function ModifiesInternalConfig(config: InternalConfig): set + predicate CountBitsEnsuresPublicly(input: CountBitsInput , output: Result) + // The private method to be refined by the library developer + + + method CountBits ( config: InternalConfig , input: CountBitsInput ) + returns (output: Result) + requires + // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` part. + && ValidInternalConfig?(config) + && input.bits.Valid() + && ModifiesInternalConfig(config) !! input.bits.Repr + // TODO: smithy-dafny isn't yet generating the `input.bits.Repr` part. + modifies ModifiesInternalConfig(config), input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures CountBitsEnsuresPublicly(input, output) + + + predicate BinaryOfEnsuresPublicly(input: BinaryOfInput , output: Result) + // The private method to be refined by the library developer + + + method BinaryOf ( config: InternalConfig , input: BinaryOfInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures BinaryOfEnsuresPublicly(input, output) + // TODO: smithy-dafny isn't yet generating this + ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) + // The private method to be refined by the library developer + + + method Chunks ( config: InternalConfig , input: ChunksInput ) + returns (output: Result) + requires + && ValidInternalConfig?(config) + // TODO: smithy-dafny isn't yet generating this + && input.bytesIn.Valid() + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures + && ValidInternalConfig?(config) + ensures ChunksEnsuresPublicly(input, output) +} diff --git a/TestModels/Streaming/Model/Streaming.smithy b/TestModels/Streaming/Model/Streaming.smithy index 88b312a854..e2e5fb27ef 100644 --- a/TestModels/Streaming/Model/Streaming.smithy +++ b/TestModels/Streaming/Model/Streaming.smithy @@ -1,30 +1,73 @@ +$version: "2" + +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 namespace simple.streaming @aws.polymorph#localService( - sdkId: "Streaming", - config: StreamingConfig, + sdkId: "SimpleStreaming", + config: SimpleStreamingConfig, ) -service Streaming { +service SimpleStreaming { version: "2021-11-01", - resources: [], - operations: [ GetBlob ], - errors: [], + operations: [ + CountBits, + BinaryOf, + Chunks + ] } -structure StreamingConfig {} +structure SimpleStreamingConfig {} + +@suppress(["UnsupportedFeatures"]) +@streaming +blob StreamingBlob -operation GetBlob { - input: GetBlobInput, - output: GetBlobOutput, +/// Calculates the sum of all bits +operation CountBits { + input := { + @required + bits: StreamingBlob + } + output := { + @required + sum: Integer + } + errors: [OverflowError] } -structure GetBlobInput { - value: StreamingBlob +@error("client") +structure OverflowError { + @required + message: String } -structure GetBlobOutput { - value: StreamingBlob +/// Returns the binary representation of the input. +operation BinaryOf { + input := { + @required + number: Integer + } + output := { + @required + binary: StreamingBlob + } } -@streaming -blob StreamingBlob \ No newline at end of file +@range(min: 1) +integer CountingInteger + +/// Returns input in chunks of the given size. +operation Chunks { + input := { + @required + bytesIn: StreamingBlob + + @required + chunkSize: CountingInteger + } + output := { + @required + bytesOut: StreamingBlob + } +} \ No newline at end of file diff --git a/TestModels/Streaming/README.md b/TestModels/Streaming/README.md index 8db9cbc177..e4122b5555 100644 --- a/TestModels/Streaming/README.md +++ b/TestModels/Streaming/README.md @@ -4,6 +4,7 @@ This project will implement the smithy trait [streaming](https://smithy.io/2.0/s ## Status -This project does not build. The `software.amazon.polymorph.smithydafny` project does not support code generation for the "streaming" trait. - -Once the Polymorph code generator supports code generation for this trait, these files should be extended to complete the type implementation. +This project only currently works on Python: the Dafny code generation +has been updated to support `@streaming` on blob shapes, +but only Python includes shim adaptors between the Dafny types +and the types used for Smithy-generated interfaces. diff --git a/TestModels/Streaming/codegen-patches/dafny/dafny-4.9.0.patch b/TestModels/Streaming/codegen-patches/dafny/dafny-4.9.0.patch new file mode 100644 index 0000000000..4736142a23 --- /dev/null +++ b/TestModels/Streaming/codegen-patches/dafny/dafny-4.9.0.patch @@ -0,0 +1,94 @@ +diff --git b/TestModels/Streaming/Model/SimpleStreamingTypes.dfy a/TestModels/Streaming/Model/SimpleStreamingTypes.dfy +index af6ad336f..50140cc6c 100644 +--- b/TestModels/Streaming/Model/SimpleStreamingTypes.dfy ++++ a/TestModels/Streaming/Model/SimpleStreamingTypes.dfy +@@ -79,8 +79,12 @@ module SimpleStreamingTypes + returns (output: Result) + requires + && ValidState() ++ // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` part. ++ requires ++ && input.bits.Valid() && History !in input.bits.Repr + modifies Modifies - {History} , +- History`CountBits ++ History`CountBits , ++ input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures +@@ -102,6 +106,8 @@ module SimpleStreamingTypes + && ValidState() + ensures BinaryOfEnsuresPublicly(input, output) + ensures History.BinaryOf == old(History.BinaryOf) + [DafnyCallEvent(input, output)] ++ // TODO: smithy-dafny isn't yet generating this ++ ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) + // The public method to be called by library consumers +@@ -212,8 +218,12 @@ abstract module AbstractSimpleStreamingService + returns (output: Result) + requires + && ValidState() ++ // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` parts. ++ requires ++ && input.bits.Valid() && History !in input.bits.Repr + modifies Modifies - {History} , +- History`CountBits ++ History`CountBits , ++ input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases Modifies - {History} + ensures +@@ -221,6 +231,10 @@ abstract module AbstractSimpleStreamingService + ensures CountBitsEnsuresPublicly(input, output) + ensures History.CountBits == old(History.CountBits) + [DafnyCallEvent(input, output)] + { ++ // TODO: It's not clear how to actually ensure this, ++ // since the internal config is not visible to the trait ++ // so it can't really be a precondition there. ++ assume {:axiom} Operations.ModifiesInternalConfig(config) !! input.bits.Repr; + output := Operations.CountBits(config, input); + History.CountBits := History.CountBits + [DafnyCallEvent(input, output)]; + } +@@ -240,6 +254,8 @@ abstract module AbstractSimpleStreamingService + && ValidState() + ensures BinaryOfEnsuresPublicly(input, output) + ensures History.BinaryOf == old(History.BinaryOf) + [DafnyCallEvent(input, output)] ++ // TODO: smithy-dafny isn't yet generating this ++ ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + { + output := Operations.BinaryOf(config, input); + History.BinaryOf := History.BinaryOf + [DafnyCallEvent(input, output)]; +@@ -283,8 +299,12 @@ abstract module AbstractSimpleStreamingOperations { + method CountBits ( config: InternalConfig , input: CountBitsInput ) + returns (output: Result) + requires +- && ValidInternalConfig?(config) +- modifies ModifiesInternalConfig(config) ++ // TODO: smithy-dafny isn't yet generating the `input.bits.Valid()` part. ++ && ValidInternalConfig?(config) ++ && input.bits.Valid() ++ && ModifiesInternalConfig(config) !! input.bits.Repr ++ // TODO: smithy-dafny isn't yet generating the `input.bits.Repr` part. ++ modifies ModifiesInternalConfig(config), input.bits.Repr + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) + ensures +@@ -306,6 +326,8 @@ abstract module AbstractSimpleStreamingOperations { + ensures + && ValidInternalConfig?(config) + ensures BinaryOfEnsuresPublicly(input, output) ++ // TODO: smithy-dafny isn't yet generating this ++ ensures output.Success? ==> output.value.binary.Valid() && fresh(output.value.binary.Repr) + + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) +@@ -316,6 +338,8 @@ abstract module AbstractSimpleStreamingOperations { + returns (output: Result) + requires + && ValidInternalConfig?(config) ++ // TODO: smithy-dafny isn't yet generating this ++ && input.bytesIn.Valid() + modifies ModifiesInternalConfig(config) + // Dafny will skip type parameters when generating a default decreases clause. + decreases ModifiesInternalConfig(config) diff --git a/TestModels/Streaming/runtimes/python/pyproject.toml b/TestModels/Streaming/runtimes/python/pyproject.toml new file mode 100644 index 0000000000..b2a6f3351b --- /dev/null +++ b/TestModels/Streaming/runtimes/python/pyproject.toml @@ -0,0 +1,26 @@ +[tool.poetry] +name = "simple-streaming" +version = "0.1.0" +description = "" +authors = ["AWS "] +packages = [ + { include = "simple_streaming", from = "src" } +] +# Include all of the following .gitignored files in package distributions, +# even though it is not included in version control +include = ["**/smithygenerated/**/*.py", "**/internaldafny/**/*.py"] + +[tool.poetry.dependencies] +python = "^3.11.0" +# TODO: Depend on PyPi once Smithy-Python publishes their Python package there +smithy-python = { path = "../../../../codegen/smithy-dafny-codegen-modules/smithy-python/python-packages/smithy-python", develop = false} + +smithy-dafny-standard-library = {path = "../../../dafny-dependencies/StandardLibrary/runtimes/python", develop = false} +DafnyRuntimePython = "^4.4.0" + +[tool.poetry.group.test.dependencies] +pytest = "^7.4.0" + +[build-system] +requires = ["poetry-core"] +build-backend = "poetry.core.masonry.api" diff --git a/TestModels/Streaming/runtimes/python/src/simple_streaming/__init__.py b/TestModels/Streaming/runtimes/python/src/simple_streaming/__init__.py new file mode 100644 index 0000000000..a610f8149d --- /dev/null +++ b/TestModels/Streaming/runtimes/python/src/simple_streaming/__init__.py @@ -0,0 +1,5 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# Initialize generated Dafny +from .internaldafny.generated import module_ \ No newline at end of file diff --git a/TestModels/Streaming/runtimes/python/test/internaldafny/__init__.py b/TestModels/Streaming/runtimes/python/test/internaldafny/__init__.py new file mode 100644 index 0000000000..76a5b798a2 --- /dev/null +++ b/TestModels/Streaming/runtimes/python/test/internaldafny/__init__.py @@ -0,0 +1,2 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 \ No newline at end of file diff --git a/TestModels/Streaming/runtimes/python/test/internaldafny/extern/wrapped_simple_streaming.py b/TestModels/Streaming/runtimes/python/test/internaldafny/extern/wrapped_simple_streaming.py new file mode 100644 index 0000000000..dafc610415 --- /dev/null +++ b/TestModels/Streaming/runtimes/python/test/internaldafny/extern/wrapped_simple_streaming.py @@ -0,0 +1,22 @@ +# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +# src imports +from simple_streaming.smithygenerated.simple_streaming.client import SimpleStreaming +from simple_streaming.smithygenerated.simple_streaming.shim import SimpleStreamingShim +from simple_streaming.smithygenerated.simple_streaming.config import dafny_config_to_smithy_config +import smithy_dafny_standard_library.internaldafny.generated.Wrappers as Wrappers + +# test imports, not qualified since this isn't in a package +import WrappedSimpleStreamingService + +class default__(WrappedSimpleStreamingService.default__): + + @staticmethod + def WrappedSimpleStreaming(config): + wrapped_config = dafny_config_to_smithy_config(config) + impl = SimpleStreaming(wrapped_config) + wrapped_client = SimpleStreamingShim(impl) + return Wrappers.Result_Success(wrapped_client) + +WrappedSimpleStreamingService.default__ = default__ \ No newline at end of file diff --git a/TestModels/Streaming/runtimes/python/test/internaldafny/test_dafny_wrapper.py b/TestModels/Streaming/runtimes/python/test/internaldafny/test_dafny_wrapper.py new file mode 100644 index 0000000000..d3e93c6711 --- /dev/null +++ b/TestModels/Streaming/runtimes/python/test/internaldafny/test_dafny_wrapper.py @@ -0,0 +1,24 @@ +""" +Wrapper file for executing Dafny tests from pytest. +This allows us to import modules required by Dafny-generated tests +before executing Dafny-generated tests. +pytest will find and execute the `test_dafny` method below, +which will execute the `__main__.py` file in the `dafny` directory. +""" + +import sys + +# Dafny-generated tests are not compiled as a package +# and require adding Dafny-generated test code to PYTHONPATH. +# These files are only on PYTHONPATH for tests executed from this file. + +internaldafny_dir = '/'.join(__file__.split("/")[:-1]) + +sys.path.append(internaldafny_dir + "/extern") +sys.path.append(internaldafny_dir + "/generated") + +# Initialize extern for test +from .extern import wrapped_simple_streaming + +def test_dafny(): + from .generated import __main__ \ No newline at end of file diff --git a/TestModels/Streaming/runtimes/python/tox.ini b/TestModels/Streaming/runtimes/python/tox.ini new file mode 100644 index 0000000000..b626d2496c --- /dev/null +++ b/TestModels/Streaming/runtimes/python/tox.ini @@ -0,0 +1,13 @@ +[tox] +isolated_build = True +envlist = + py{311,312} + +[testenv] +skip_install = true +allowlist_externals = poetry +commands_pre = + poetry lock + poetry install +commands = + poetry run pytest -s -v test/ \ No newline at end of file diff --git a/TestModels/Streaming/src/Chunker.dfy b/TestModels/Streaming/src/Chunker.dfy new file mode 100644 index 0000000000..8bcdedd95f --- /dev/null +++ b/TestModels/Streaming/src/Chunker.dfy @@ -0,0 +1,72 @@ +include "../Model/SimpleStreamingTypes.dfy" + +module Chunker { + + import Std.BoundedInts + + import opened Std.Wrappers + import opened Types = SimpleStreamingTypes + import opened StandardLibrary.UInt + import opened Std.Enumerators + import opened Std.Aggregators + + // An example of a Pipeline, which processes chunks of bytes + // as they flow through a stream. + // Pipelines let you define a stream transformation once + // in a way that allows external code to apply it to either + // push or pull-based streams: + // when a chunk becomes available to the pipeline, + // zero or more chunks are made available downstream. + @AssumeCrossModuleTermination + class Chunker extends Pipeline { + + const chunkSize: CountingInteger + var chunkBuffer: BoundedInts.bytes + + constructor(upstream: Enumerator, chunkSize: CountingInteger) + ensures Valid() + ensures history == [] + { + this.buffer := new Collector(); + this.upstream := upstream; + + this.chunkSize := chunkSize; + chunkBuffer := []; + history := []; + Repr := {this} + upstream.Repr; + new; + assume {:axiom} Valid(); + } + + method Process(event: Option, a: Accumulator) + requires Valid() + requires a.Valid() + requires Repr !! a.Repr + modifies Repr, a.Repr + ensures a.ValidAndDisjoint() + { + assert this in Repr; + assert this !in a.Repr; + match event { + case Some(bits) => { + chunkBuffer := chunkBuffer + bits; + } + case None => return; + } + + while chunkSize as int <= |chunkBuffer| + invariant a.ValidAndDisjoint() + { + a.CanConsumeAll(a.history, chunkBuffer[..chunkSize]); + a.Accept(chunkBuffer[..chunkSize]); + chunkBuffer := chunkBuffer[chunkSize..]; + } + + if event == None { + if 0 < |chunkBuffer| { + var _ := a.Invoke(chunkBuffer); + } + } + } + } +} \ No newline at end of file diff --git a/TestModels/Streaming/src/Index.dfy b/TestModels/Streaming/src/Index.dfy new file mode 100644 index 0000000000..882a2e30c2 --- /dev/null +++ b/TestModels/Streaming/src/Index.dfy @@ -0,0 +1,31 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "SimpleStreamingImpl.dfy" + +module {:extern "simple.streaming.internaldafny"} SimpleStreaming refines AbstractSimpleStreamingService { + import Operations = SimpleStreamingImpl + + function method DefaultSimpleStreamingConfig(): SimpleStreamingConfig { + SimpleStreamingConfig + } + + method SimpleStreaming(config: SimpleStreamingConfig) + returns (res: Result) + { + var client := new SimpleStreamingClient(Operations.Config); + return Success(client); + } + + class SimpleStreamingClient... { + predicate ValidState() { + && Operations.ValidInternalConfig?(config) + && Modifies == Operations.ModifiesInternalConfig(config) + {History} + } + + constructor(config: Operations.InternalConfig) { + this.config := config; + History := new ISimpleStreamingClientCallHistory(); + Modifies := Operations.ModifiesInternalConfig(config) + {History}; + } + } +} diff --git a/TestModels/Streaming/src/SimpleStreamingImpl.dfy b/TestModels/Streaming/src/SimpleStreamingImpl.dfy new file mode 100644 index 0000000000..a1513822db --- /dev/null +++ b/TestModels/Streaming/src/SimpleStreamingImpl.dfy @@ -0,0 +1,83 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +// Do not modify this file. This file is machine generated, and any changes to it will be overwritten. +include "../Model/SimpleStreamingTypes.dfy" +include "Chunker.dfy" +module {:options "/functionSyntax:4" } SimpleStreamingImpl refines AbstractSimpleStreamingOperations { + + import Std.Enumerators + import Std.Aggregators + import Std.Collections.Seq + import opened Chunker + + datatype Config = Config + type InternalConfig = Config + predicate ValidInternalConfig?(config: InternalConfig) + {true} + function ModifiesInternalConfig(config: InternalConfig): set + {{}} + predicate CountBitsEnsuresPublicly(input: CountBitsInput , output: Result) + {true} + + method CountBits ( config: InternalConfig , input: CountBitsInput ) + returns (output: Result) + { + var counter := new Aggregators.FoldingAccumulator(0, (sum, byte) => sum + BytesBitCount(byte)); + + Enumerators.ForEach(input.bits, counter); + + // Should really have the FoldingAccumulator fail instead, + // but this is a simpler correct approach. + if 0 <= counter.value < INT32_MAX_LIMIT { + return Success(CountBitsOutput(sum := counter.value as int32)); + } else { + return Failure(OverflowError(message := "Ah crap")); + } + } + + function BytesBitCount(b: BoundedInts.bytes): int { + Seq.FoldLeft((sum, byte) => sum + BitCount(byte), 0 as int, b) + } + + function BitCount(x: BoundedInts.uint8): int { + if x == 0 then + 0 + else if x % 2 == 1 then + 1 + BitCount(x / 2) + else + BitCount(x / 2) + } + + predicate BinaryOfEnsuresPublicly(input: BinaryOfInput , output: Result) + {true} + + + + method BinaryOf ( config: InternalConfig , input: BinaryOfInput ) + returns (output: Result) + + { + // TODO: Actually compute the binary + var fakeBinary: seq := [[12], [34, 56]]; + var fakeBinaryEnumerator := new Enumerators.SeqEnumerator(fakeBinary); + var fakeBinaryStream := new EnumeratorDataStream(fakeBinaryEnumerator, 3 as BoundedInts.uint64); + + return Success(BinaryOfOutput(binary := fakeBinaryStream)); + } + + + predicate ChunksEnsuresPublicly(input: ChunksInput , output: Result) + {true} + + method Chunks ( config: InternalConfig , input: ChunksInput ) + returns (output: Result) + { + // TODO: for now + assume {:axiom} input.bytesIn.history == []; + var chunker := new Chunker(input.bytesIn, input.chunkSize); + var chunkerStream := new EnumeratorDataStream(chunker, input.bytesIn.ContentLength()); + + return Success(ChunksOutput(bytesOut := chunkerStream)); + } + +} diff --git a/TestModels/Streaming/src/WrappedSimpleStreamingImpl.dfy b/TestModels/Streaming/src/WrappedSimpleStreamingImpl.dfy new file mode 100644 index 0000000000..58bf8aed5d --- /dev/null +++ b/TestModels/Streaming/src/WrappedSimpleStreamingImpl.dfy @@ -0,0 +1,10 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../Model/SimpleStreamingTypesWrapped.dfy" + +module {:extern "simple.streaming.internaldafny.wrapped"} WrappedSimpleStreamingService refines WrappedAbstractSimpleStreamingService { + import WrappedService = SimpleStreaming + function method WrappedDefaultSimpleStreamingConfig(): SimpleStreamingConfig { + SimpleStreamingConfig + } +} diff --git a/TestModels/Streaming/test/SimpleStreamingImplTest.dfy b/TestModels/Streaming/test/SimpleStreamingImplTest.dfy new file mode 100644 index 0000000000..411dae3b81 --- /dev/null +++ b/TestModels/Streaming/test/SimpleStreamingImplTest.dfy @@ -0,0 +1,71 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/Index.dfy" +include "../src/WrappedSimpleStreamingImpl.dfy" + +module SimpleStreamingImplTest { + import SimpleStreaming + import SimpleStreamingImpl + import Std.Enumerators + import Std.Aggregators + import Std.BoundedInts + import opened StandardLibrary.UInt + import opened Std.Streams + import opened SimpleStreamingTypes + import opened Wrappers + method{:test} TestClient(){ + var client :- expect SimpleStreaming.SimpleStreaming(); + TestCountBits(client); + TestBinaryOf(client); + } + + method TestCountBits(client: ISimpleStreamingClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var s: seq := [[0x0], [0x1, 0x2], [0x3], [], [0x4, 0x5]]; + var e := new Enumerators.SeqEnumerator(s); + var stream := new EnumeratorDataStream(e, length := 5 as BoundedInts.uint64); + var input: CountBitsInput := CountBitsInput(bits := stream); + + var ret :- expect client.CountBits(input); + + expect ret.sum == 7; + } + + method TestBinaryOf(client: ISimpleStreamingClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var input: BinaryOfInput := BinaryOfInput(number:=42); + + var ret :- expect client.BinaryOf(input); + + var collector := new Aggregators.Collector(); + + Enumerators.ForEach(ret.binary, collector); + + expect collector.values == [[12], [34, 56]]; + } + + method TestChunks(client: ISimpleStreamingClient) + requires client.ValidState() + modifies client.Modifies + ensures client.ValidState() + { + var s: seq := [[0x0], [0x1, 0x2], [0x3], [], [0x4, 0x5]]; + var e := new Enumerators.SeqEnumerator(s); + var stream := new EnumeratorDataStream(e, 5 as BoundedInts.uint64); + var input: ChunksInput := ChunksInput(bytesIn := stream, chunkSize := 2); + + var ret :- expect client.Chunks(input); + + var collector := new Aggregators.Collector(); + + Enumerators.ForEach(ret.bytesOut, collector); + + expect collector.values == [[0x0, 0x1], [0x2, 0x3], [0x4, 0x5]]; + } +} \ No newline at end of file diff --git a/TestModels/Streaming/test/WrappedSimpleStreamingTest.dfy b/TestModels/Streaming/test/WrappedSimpleStreamingTest.dfy new file mode 100644 index 0000000000..20e848dbf1 --- /dev/null +++ b/TestModels/Streaming/test/WrappedSimpleStreamingTest.dfy @@ -0,0 +1,15 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 +include "../src/WrappedSimpleStreamingImpl.dfy" +include "SimpleStreamingImplTest.dfy" + +module WrappedSimpleTypesStringTest { + import WrappedSimpleStreamingService + import SimpleStreamingImplTest + import opened Wrappers + method{:test} TestCountBits() { + var client :- expect WrappedSimpleStreamingService.WrappedSimpleStreaming(); + SimpleStreamingImplTest.TestCountBits(client); + SimpleStreamingImplTest.TestBinaryOf(client); + } +} diff --git a/TestModels/aws-sdks/s3/Makefile b/TestModels/aws-sdks/s3/Makefile index 8664027983..ddbb526b31 100644 --- a/TestModels/aws-sdks/s3/Makefile +++ b/TestModels/aws-sdks/s3/Makefile @@ -3,6 +3,7 @@ ENABLE_EXTERN_PROCESSING=1 CORES=2 +USE_DAFNY_STANDARD_LIBRARIES=1 include ../../SharedMakefile.mk diff --git a/TestModels/aws-sdks/s3/runtimes/python/pyproject.toml b/TestModels/aws-sdks/s3/runtimes/python/pyproject.toml index d1face08c1..fecc985010 100644 --- a/TestModels/aws-sdks/s3/runtimes/python/pyproject.toml +++ b/TestModels/aws-sdks/s3/runtimes/python/pyproject.toml @@ -14,6 +14,8 @@ include = ["**/smithygenerated/**/*.py", "**/internaldafny/generated/*.py"] python = "^3.11.0" boto3 = "^1.28.38" smithy-dafny-standard-library = {path = "../../../../dafny-dependencies/StandardLibrary/runtimes/python", develop = false} +# TODO: Depend on PyPi once Smithy-Python publishes their Python package there +smithy-python = { path = "../../../../../codegen/smithy-dafny-codegen-modules/smithy-python/python-packages/smithy-python", develop = false} [tool.poetry.group.test.dependencies] pytest = "^7.4.0" diff --git a/TestModels/aws-sdks/s3/test/TestComAmazonawsS3.dfy b/TestModels/aws-sdks/s3/test/TestComAmazonawsS3.dfy index 921c72a01c..7663aae4ec 100644 --- a/TestModels/aws-sdks/s3/test/TestComAmazonawsS3.dfy +++ b/TestModels/aws-sdks/s3/test/TestComAmazonawsS3.dfy @@ -7,6 +7,9 @@ module TestComAmazonawsS3 { import Com.Amazonaws.S3 import opened StandardLibrary.UInt import opened Wrappers + import opened Std.Enumerators + import opened Std.Aggregators + import opened Std.Streams const testBucket := "s3-dafny-test-bucket" const testObjectKey := "smithy-dafny-test-model-object-key" @@ -18,11 +21,15 @@ module TestComAmazonawsS3 { Key := testObjectKey ) ); + // Note the chunk size has to ensure all but the last chunk is >= 8192 bytes. + // For a small stream like this that means just one chunk. + var s: ByteStream := new SeqByteStream([ 97, 115, 100, 102 ], 10); + expect s is RewindableByteStream; PutObjectTest( input := S3.Types.PutObjectRequest( Bucket := testBucket, Key := testObjectKey, - Body := Wrappers.Some([ 97, 115, 100, 102 ]) + Body := Wrappers.Some(s) ) ); GetObjectTest( @@ -48,7 +55,7 @@ module TestComAmazonawsS3 { method GetObjectTest( nameonly input: S3.Types.GetObjectRequest, - nameonly expectedBody: S3.Types.StreamingBlob + nameonly expectedBody: BoundedInts.bytes ) { var client :- expect S3.S3Client(); @@ -60,7 +67,13 @@ module TestComAmazonawsS3 { // we only care about the Body var MyBody := ret.value.Body; expect MyBody.Some?; - expect MyBody.value == expectedBody; + + // TODO: These need to be generated as postconditions on GetObject instead + assume {:axiom} fresh(MyBody.value.Repr); + assume {:axiom} MyBody.value.Valid(); + + var bodyValue := Collect(MyBody.value); + expect bodyValue == expectedBody; } method GetObjectTestFailureNoSuchKey( @@ -83,7 +96,7 @@ module TestComAmazonawsS3 { var ret := client.PutObject(input); - expect(ret.Success?); + expect ret.Success?, ret; // just check that an ETag was returned var MyETag := ret.value.ETag; @@ -101,4 +114,13 @@ module TestComAmazonawsS3 { expect(ret.Success?); } + + method Collect(e: ByteStream) returns (s: BoundedInts.bytes) + requires e.Valid() + modifies e.Repr + { + var a := new Collector(); + ForEach(e, a); + return Seq.Flatten(a.values); + } } diff --git a/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml b/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml new file mode 100644 index 0000000000..b3ea6e4ac3 --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml @@ -0,0 +1,35 @@ +includes = [ + "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Actions.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Aggregators.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/Enumerators.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Actions/GenericAction.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/BoundedInts.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/DynamicArray.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Frames.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Math.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Relations.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Streams/Streams.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Termination.dfy", + "../dafny/Source/DafnyStandardLibraries/src/Std/Wrappers.dfy" +] + +[options] +# Options that help support more values of consuming context options +# (mostly turning on any more restrictive verification) +track-print-effects = true +enforce-determinism = false +reads-clauses-on-methods = true + +# Options that differ from Dafny's +unicode-char = false + +# TODO +allow-warnings = true + +# Options important for sustainable development +# of the libraries themselves. +resource-limit = 1000000 +# These give too many false positives right now, but should be enabled in the future +warn-redundant-assumptions = false +warn-contradictory-assumptions = false diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile index af2e417bce..f3984ba7f7 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/Makefile +++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile @@ -24,8 +24,8 @@ else RESET := "" endif -# Overriding this target just to generate the project.properties file -polymorph_dafny : +# Overriding this target just to generate the project.properties file. +polymorph_dafny: $(if $(USE_DAFNY_STANDARD_LIBRARIES), build_dafny_stdlibs, ) cd $(CODEGEN_CLI_ROOT); \ $(GRADLEW) run --args="\ --library-root $(LIBRARY_ROOT) \ @@ -107,10 +107,15 @@ transpile_implementation: --unicode-char:false \ --function-syntax:3 \ --output $(OUT) \ + $(if $(USE_DAFNY_STANDARD_LIBRARIES), bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \ $(DAFNY_OPTIONS) \ $(DAFNY_OTHER_FILES) \ $(TRANSPILE_MODULE_NAME) +build_dafny_stdlibs: + dafny build -t:lib --output bin/DafnyStandardLibraries-smithy-dafny-subset.doo DafnyStandardLibraries-smithy-dafny-subset.toml + rm -rf DafnyStandardLibraries-smithy-dafny-subset-lib + # Override SharedMakefile's build_java to not install # StandardLibrary as a dependency build_java: transpile_java diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py b/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py new file mode 100644 index 0000000000..7a6eff36bc --- /dev/null +++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py @@ -0,0 +1,67 @@ + +from _dafny import Seq +from smithy_python.interfaces.blobs import ByteStream +from smithy_dafny_standard_library.internaldafny.generated.Std_Streams import ByteStream as DafnyByteStream, RewindableByteStream as DafnyRewindableByteStream +from smithy_dafny_standard_library.internaldafny.generated.Std_Enumerators import Enumerator +from smithy_dafny_standard_library.internaldafny.generated.Std_Wrappers import Option, Option_Some, Option_None + +# Adaptor classes for wrapping up Python-native types as their +# corresponding Dafny interfaces, and vice-versa. +# These are the equivalent of type conversions, +# but avoiding having to load all data into memory at once. + +class DafnyByteStreamAsByteStream(ByteStream): + """Wrapper class adapting a Dafny ByteStream as a native ByteStream.""" + + def __init__(self, dafny_byte_stream): + self.dafny_byte_stream = dafny_byte_stream + + def read(self, size: int = -1) -> bytes: + # TODO: assert size is -1, buffer, + # or define a more specialized Action type for streams. + next = self.dafny_byte_stream.Next() + while next.is_Some and len(next.value) == 0: + next = self.dafny_byte_stream.Next() + # Do NOT return None, because that indicates "no data right now, might be more later" + return bytes(next.value) if next.is_Some else bytes() + + +class RewindableDafnyByteStreamAsByteStream(DafnyByteStreamAsByteStream): + """Wrapper class adapting a Dafny RewindableByteStream as a native ByteStream + that supports tell and seek. + """ + + def __init__(self, dafny_byte_stream): + if not isinstance(dafny_byte_stream, DafnyRewindableByteStream): + raise ValueError("Rewindable stream required") + super().__init__(dafny_byte_stream) + + def tell(self) -> int: + return self.dafny_byte_stream.Position() + + def seek(self, offset, whence=0): + match whence: + case 0: + position = offset + case 1: + position = self.dafny_byte_stream.Position() + offset + case 2: + position = self.dafny_byte_stream.ContentLength() + offset + return self.dafny_byte_stream.Seek(position) + + +class StreamingBlobAsDafnyDataStream(DafnyByteStream): + """Wrapper class adapting a native StreamingBlob as a Dafny ByteStream.""" + + def __init__(self, streaming_blob): + self.streaming_blob = streaming_blob + + def Next(self): + return Enumerator.Next(self) + + def Invoke(self, _) -> Option: + next = self.streaming_blob.read() + if next: + return Option_Some(Seq(next)) + else: + return Option_None() diff --git a/TestModels/dafny-dependencies/StandardLibrary/src/UInt.dfy b/TestModels/dafny-dependencies/StandardLibrary/src/UInt.dfy index 7f4613147d..0a5aaaf632 100644 --- a/TestModels/dafny-dependencies/StandardLibrary/src/UInt.dfy +++ b/TestModels/dafny-dependencies/StandardLibrary/src/UInt.dfy @@ -9,6 +9,8 @@ module StandardLibrary.UInt { newtype uint32 = x | 0 <= x < 0x1_0000_0000 newtype uint64 = x | 0 <= x < 0x1_0000_0000_0000_0000 + type bytes = seq + newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000 newtype int64 = x | -0x8000_0000_0000_0000 <= x < 0x8000_0000_0000_0000 newtype posInt64 = x | 0 < x < 0x8000_0000_0000_0000 witness 1 diff --git a/TestModels/dafny-dependencies/dafny b/TestModels/dafny-dependencies/dafny new file mode 160000 index 0000000000..70831a8332 --- /dev/null +++ b/TestModels/dafny-dependencies/dafny @@ -0,0 +1 @@ +Subproject commit 70831a8332ccbca883ac54b273db26d98cc06e48 diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/TestModelTest.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/TestModelTest.java index 2c9547dfa3..40f5cea6eb 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/TestModelTest.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/TestModelTest.java @@ -33,7 +33,11 @@ protected static Stream discoverTestModels() throws IOException { .resolve("TestModels"); var allTestModels = Files .walk(testModelRoot) - .filter(p -> Files.exists(p.resolve("Makefile"))) + .filter(p -> + Files.exists(p.resolve("Makefile")) && + (Files.isDirectory(p.resolve("Model")) || + Files.isDirectory(p.resolve("model"))) + ) .map(testModelRoot::relativize) .map(Path::toString); @@ -83,4 +87,18 @@ protected Path getTestModelPath(String relativeTestModelPath) { .resolve("TestModels") .resolve(relativeTestModelPath); } + + protected void testModels(String relativeTestModelPath) { + // The @streaming support depends on our subset of the Dafny standard libraries + // which cannot be built for old versions of Dafny. + if ( + relativeTestModelPath.endsWith("Streaming") || + relativeTestModelPath.endsWith("s3") + ) { + DafnyVersion dafnyVersion = CodegenEngine.getDafnyVersionFromDafny(); + if (dafnyVersion.compareTo(DafnyVersion.parse("4.9.0")) < 0) { + Assumptions.assumeTrue(false); + } + } + } } diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydafny/DafnyTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydafny/DafnyTestModels.java index f913a9e7fd..67ef3d4160 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydafny/DafnyTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydafny/DafnyTestModels.java @@ -29,7 +29,9 @@ class DafnyTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForDafny(String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + Assumptions.assumeFalse(DISABLED_TESTS.contains(relativeTestModelPath)); Path testModelPath = getTestModelPath(relativeTestModelPath); diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java index da8f77119e..07e9301d3c 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithydotnet/DotnetTestModels.java @@ -41,7 +41,9 @@ class DotnetTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForDotnet(String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + Assumptions.assumeFalse(DISABLED_TESTS.contains(relativeTestModelPath)); Path testModelPath = getTestModelPath(relativeTestModelPath); diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java index 2bb352aa83..ca6034d4f6 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithygo/GoTestModels.java @@ -47,7 +47,9 @@ class GoTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForGo(final String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + Assumptions.assumeFalse(DISABLED_TESTS.contains(relativeTestModelPath)); Path testModelPath = getTestModelPath(relativeTestModelPath); diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java index d7f1a3292c..8cf0ec9952 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyjava/JavaTestModels.java @@ -59,7 +59,9 @@ class JavaTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForJava(String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + // This test is hacked up to pass for Java in a way that doesn't work // for older Dafny versions. if (relativeTestModelPath.endsWith("Constraints")) { diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithypython/PythonTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithypython/PythonTestModels.java index f902e63e06..1632f95916 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithypython/PythonTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithypython/PythonTestModels.java @@ -11,7 +11,9 @@ import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; +import software.amazon.polymorph.CodegenEngine; import software.amazon.polymorph.TestModelTest; +import software.amazon.polymorph.smithydafny.DafnyVersion; class PythonTestModels extends TestModelTest { @@ -29,7 +31,6 @@ class PythonTestModels extends TestModelTest { DISABLED_TESTS.add("SimpleTypes/SimpleFloat"); DISABLED_TESTS.add("SimpleTypes/SimpleShort"); DISABLED_TESTS.add("SimpleTypes/SimpleTimestamp"); - DISABLED_TESTS.add("Streaming"); DISABLED_TESTS.add("SQSExtended"); DISABLED_TESTS.add("aws-sdks/ddb-lite"); DISABLED_TESTS.add("aws-sdks/glue"); @@ -43,7 +44,9 @@ class PythonTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForPython(String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + Assumptions.assumeFalse(DISABLED_TESTS.contains(relativeTestModelPath)); Path testModelPath = getTestModelPath(relativeTestModelPath); diff --git a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java index 1c06c9612d..aa300e28ca 100644 --- a/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java +++ b/codegen/smithy-dafny-codegen-test/src/test/java/software/amazon/polymorph/smithyrust/RustTestModels.java @@ -50,7 +50,9 @@ class RustTestModels extends TestModelTest { @ParameterizedTest @MethodSource("discoverTestModels") - void testModelsForRust(String relativeTestModelPath) { + protected void testModels(String relativeTestModelPath) { + super.testModels(relativeTestModelPath); + Assumptions.assumeFalse(DISABLED_TESTS.contains(relativeTestModelPath)); Path testModelPath = getTestModelPath(relativeTestModelPath); diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java index 2db0afdbbb..93e2424d9c 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java @@ -151,7 +151,7 @@ public Map generate() { .of( Stream .concat( - DafnyNameResolver.modulePreludeStandardImports(), + DafnyNameResolver.modulePreludeStandardImports(model, serviceShape), nameResolver .dependentModels() .stream() @@ -319,7 +319,14 @@ public TokenTree generateBlobTypeDefinition(final ShapeId blobShapeId) { final Optional lengthConstraint = blobShape .getTrait(LengthTrait.class) .map(DafnyApiCodegen::generateLengthConstraint); - return generateSubsetType(blobShapeId, "seq", lengthConstraint); + if (blobShape.hasTrait(StreamingTrait.class)) { + // TODO: need to handle @length too, + // something like `forall produced | a.CanProduce(produced) :: min <= |Enumerated(produced)| <= max + // (which should have a simpler helper predicate version, especially when allowing for reference types) + return generateTypeSynonym(blobShapeId, "ByteStream"); + } else { + return generateSubsetType(blobShapeId, "seq", lengthConstraint); + } } public TokenTree generateBoolTypeDefinition(final ShapeId boolShapeId) { @@ -1983,7 +1990,7 @@ public TokenTree generateDependantErrorDataTypeConstructor( public TokenTree generateAbstractBody() { final TokenTree abstractModulePrelude = TokenTree - .of(DafnyNameResolver.abstractModulePrelude(serviceShape)) + .of(DafnyNameResolver.abstractModulePrelude(model, serviceShape)) .lineSeparated(); if (serviceShape.hasTrait(ServiceTrait.class)) { @@ -2005,7 +2012,7 @@ public TokenTree generateAbstractBody() { // This method needs to be called before typesModulePrelude is calculated public TokenTree generateAbstractServiceModule(ServiceShape serviceShape) { final TokenTree abstractModulePrelude = TokenTree - .of(DafnyNameResolver.abstractModulePrelude(serviceShape)) + .of(DafnyNameResolver.abstractModulePrelude(model, serviceShape)) .lineSeparated(); final TokenTree moduleHeader = TokenTree.of( "abstract module %s".formatted( @@ -2819,7 +2826,7 @@ public TokenTree generateAbstractWrappedLocalService( "abstract module WrappedAbstract%sService".formatted(baseModuleName) ); final TokenTree abstractModulePrelude = TokenTree - .of(DafnyNameResolver.wrappedAbstractModulePrelude(serviceShape)) + .of(DafnyNameResolver.wrappedAbstractModulePrelude(model, serviceShape)) .lineSeparated(); final String configTypeName = nameResolver.baseTypeForShape( @@ -3048,7 +3055,9 @@ private TokenTree generateAbstractOperationsModule( final TokenTree body = TokenTree .of( - TokenTree.of(DafnyNameResolver.abstractModulePrelude(serviceShape)), + TokenTree.of( + DafnyNameResolver.abstractModulePrelude(model, serviceShape) + ), TokenTree.of("type %s".formatted(internalConfigType)), TokenTree.of( "predicate %s(config: %s)".formatted( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyNameResolver.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyNameResolver.java index 90f49d776e..80cce84b3e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyNameResolver.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyNameResolver.java @@ -4,11 +4,15 @@ package software.amazon.polymorph.smithydafny; import com.google.common.base.Joiner; +import com.google.common.collect.Streams; +import com.squareup.javapoet.ParameterizedTypeName; +import java.nio.ByteBuffer; import java.nio.file.Path; import java.util.*; import java.util.stream.Stream; import javax.annotation.Nonnull; import javax.annotation.Nullable; +import org.reactivestreams.Publisher; import software.amazon.polymorph.smithyjava.NamespaceHelper; import software.amazon.polymorph.traits.LocalServiceTrait; import software.amazon.polymorph.traits.PositionalTrait; @@ -19,8 +23,10 @@ import software.amazon.polymorph.utils.TokenTree; import software.amazon.smithy.aws.traits.ServiceTrait; import software.amazon.smithy.model.Model; +import software.amazon.smithy.model.neighbor.Walker; import software.amazon.smithy.model.shapes.*; import software.amazon.smithy.model.traits.ReadonlyTrait; +import software.amazon.smithy.model.traits.StreamingTrait; import software.amazon.smithy.utils.StringUtils; public record DafnyNameResolver( @@ -72,8 +78,7 @@ public String baseTypeForShape(final ShapeId shapeId) { } return switch (shape.getType()) { - case BLOB, - BOOLEAN, + case BOOLEAN, STRING, ENUM, // currently unused in model and unsupported in StandardLibrary.UInt @@ -83,6 +88,13 @@ public String baseTypeForShape(final ShapeId shapeId) { DOUBLE, LIST, MAP -> dafnyModulePrefixForShape(shape) + shapeName; + case BLOB -> { + if (shape.hasTrait(StreamingTrait.class)) { + yield "ByteStream"; + } else { + yield dafnyModulePrefixForShape(shape) + shapeName; + } + } case STRUCTURE -> { if (shape.hasTrait(ReferenceTrait.class)) { yield baseTypeForShape( @@ -356,15 +368,32 @@ public String historicalCallHistoryPostfix() { return "CallHistory"; } - public static Stream modulePreludeStandardImports() { - return Stream.of( + public static Stream modulePreludeStandardImports( + Model model, + ServiceShape serviceShape + ) { + Stream basics = Stream.of( "import opened Wrappers", "import opened StandardLibrary.UInt", "import opened UTF8" ); + // Include StandardLibrary.Streams only if the service uses @streaming. + // This is because Rust doesn't yet support the Dafny streaming traits, + // so that code is essentially #ifdef'd out. + if ( + new Walker(model) + .walkShapes(serviceShape) + .stream() + .anyMatch(s -> s.hasTrait(StreamingTrait.class)) + ) { + return Streams.concat(basics, Stream.of("import opened Std.Streams")); + } else { + return basics; + } } public static Stream abstractModulePrelude( + Model model, ServiceShape serviceShape ) { final String typesModuleName = dafnyTypesModuleName( @@ -373,7 +402,7 @@ public static Stream abstractModulePrelude( return Stream .concat( - modulePreludeStandardImports(), + modulePreludeStandardImports(model, serviceShape), Stream.of("import opened Types = %s".formatted(typesModuleName)) ) .map(i -> Token.of(i)); @@ -403,10 +432,11 @@ public static String abstractOperationsModuleName(ServiceShape serviceShape) { } public static Stream wrappedAbstractModulePrelude( + Model model, ServiceShape serviceShape ) { return Stream.concat( - abstractModulePrelude(serviceShape), + abstractModulePrelude(model, serviceShape), Stream.of( TokenTree.of( "import WrappedService : %s".formatted( diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Native.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Native.java index b43cc9b7ce..2035d91e4f 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Native.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Native.java @@ -34,6 +34,7 @@ import software.amazon.smithy.model.shapes.ShapeType; import software.amazon.smithy.model.traits.BoxTrait; import software.amazon.smithy.model.traits.EnumTrait; +import software.amazon.smithy.model.traits.StreamingTrait; /** * Provides a consistent mapping between names of diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java index 14dc1a9239..18686cb43f 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/AwsSdkToDafnyShapeVisitor.java @@ -75,12 +75,16 @@ protected String getDefault(Shape shape) { @Override public String blobShape(BlobShape shape) { - // if it's a streaming blob, read it first if (shape.hasTrait(StreamingTrait.class)) { - return "Seq(" + dataSource + ".read())"; + writer.addStdlibImport( + "smithy_dafny_standard_library.internaldafny.extern.streams", + "StreamingBlobAsDafnyDataStream" + ); + return "StreamingBlobAsDafnyDataStream(%1$s)".formatted(dataSource); + } else { + writer.addStdlibImport("_dafny", "Seq"); + return "Seq(" + dataSource + ")"; } - writer.addStdlibImport("_dafny", "Seq"); - return "Seq(" + dataSource + ")"; } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java index c08a9b7d3e..6a2029a1f3 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/shapevisitor/DafnyToAwsSdkShapeVisitor.java @@ -29,6 +29,7 @@ import software.amazon.smithy.model.shapes.TimestampShape; import software.amazon.smithy.model.shapes.UnionShape; import software.amazon.smithy.model.traits.EnumTrait; +import software.amazon.smithy.model.traits.StreamingTrait; import software.amazon.smithy.python.codegen.GenerationContext; import software.amazon.smithy.python.codegen.PythonWriter; @@ -74,7 +75,17 @@ protected String getDefault(Shape shape) { @Override public String blobShape(BlobShape shape) { - return "bytes(%1$s)".formatted(dataSource); + if (shape.hasTrait(StreamingTrait.class)) { + writer.addStdlibImport( + "smithy_dafny_standard_library.internaldafny.extern.streams", + "RewindableDafnyByteStreamAsByteStream" + ); + return "RewindableDafnyByteStreamAsByteStream(%1$s)".formatted( + dataSource + ); + } else { + return "bytes(%1$s)".formatted(dataSource); + } } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java index 482e8d4ccd..06679418c7 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java @@ -29,6 +29,7 @@ import software.amazon.smithy.model.shapes.StructureShape; import software.amazon.smithy.model.shapes.TimestampShape; import software.amazon.smithy.model.shapes.UnionShape; +import software.amazon.smithy.model.traits.StreamingTrait; import software.amazon.smithy.python.codegen.GenerationContext; import software.amazon.smithy.python.codegen.PythonWriter; @@ -92,7 +93,15 @@ protected String getDefault(Shape shape) { @Override public String blobShape(BlobShape shape) { - return "bytes(%1$s)".formatted(dataSource); + if (shape.hasTrait(StreamingTrait.class)) { + writer.addStdlibImport( + "smithy_dafny_standard_library.internaldafny.extern.streams", + "DafnyByteStreamAsByteStream" + ); + return "DafnyByteStreamAsByteStream(%1$s)".formatted(dataSource); + } else { + return "bytes(%1$s)".formatted(dataSource); + } } @Override diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java index 6e9be991bf..bdbf0c627e 100644 --- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java +++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java @@ -29,6 +29,7 @@ import software.amazon.smithy.model.shapes.StructureShape; import software.amazon.smithy.model.shapes.TimestampShape; import software.amazon.smithy.model.shapes.UnionShape; +import software.amazon.smithy.model.traits.StreamingTrait; import software.amazon.smithy.python.codegen.GenerationContext; import software.amazon.smithy.python.codegen.PythonWriter; @@ -93,8 +94,16 @@ protected String getDefault(Shape shape) { @Override public String blobShape(BlobShape shape) { - writer.addStdlibImport("_dafny", "Seq"); - return "Seq(" + dataSource + ")"; + if (shape.hasTrait(StreamingTrait.class)) { + writer.addStdlibImport( + "smithy_dafny_standard_library.internaldafny.extern.streams", + "StreamingBlobAsDafnyDataStream" + ); + return "StreamingBlobAsDafnyDataStream(%1$s)".formatted(dataSource); + } else { + writer.addStdlibImport("_dafny", "Seq"); + return "Seq(" + dataSource + ")"; + } } @Override