feat: partial @streaming blob support for Python (#747)

Adds partial support for the `@streaming` Smithy trait on blobs, depending on a `actions-and-streaming-stdlibs` branch of Dafny that adds an Actions standard library, and only implemented when targeting Python so far. Event streaming is not technically supported yet because more codegen changes are necessary, but this will be a relatively small delta, as the Dafny types involved are already handled.

The motivation behind merging this incomplete work is largely to get the test model coverage into CI, so that it doesn't regress as the feature is completed, especially when Dafny verification is perturbed in future versions. The next priority will be to complete the Dafny branch and merge it to Dafny mainline.

Note that `smithy-dafny` will still emit a `DANGER` validation event saying that `@streaming` is not supported, which is intentional in order to guard against using the feature in production before it is fully completed: the test models exercising it explicitly suppress this event.

* Added a `dafny` submodule under `TestModels/dafny-dependencies/dafny` tracking the `actions-and-streaming-stdlibs` branch, just to access the contents of `Source/DafnyStandardLibraries/src/Std/Actions` etc. This copy of Dafny is never built or used for any other building tasks.
* Added a build task under `StandardLibrary` to build a .doo file from a subset of the Dafny standard library files above (using `DafnyStandardLibraries-smithy-dafny-subset.toml`). This is then used as a `--library` argument when verifying/translating polymorph libraries. This approach allows the standard library source to be built with different but compatible options such as `--reads-clauses-on-methods`.
  * This is guarded by a `USE_DAFNY_STANDARD_LIBRARIES` Makefile variable, since a newer Dafny is required for this to work.
* Bumped the high watermark Dafny version tested in CI to 4.9.1, which is necessary since the standard library above uses newer features like `@`-attributes.
* Modified Dafny and Python codegen to emit references to the `ByteStream` and `RewindableByteStream` types, and removed the previous workaround to first `.read()` all data in Python.
  * Because streams have mutable state, the Dafny code generation needs to take them into account when generating things like `modifies` clauses. I haven't yet implemented this, instead using a patch file to add the missing specification to the `Streaming` test model code.
* Modified the `aws-sdk/s3` test model and fleshed the `Streaming` test model out to actually test the feature.
* Removes not-grep, since our globs are actually completely broken and the tool doesn't support our current code layout, and it was complaining about the contents of the `dafny` submodule. See #763.

Reviewer note: it is worth reading the contents of the pending [Actions](https://github.com/dafny-lang/dafny/tree/actions-and-streaming-stdlibs/Source/DafnyStandardLibraries/src/Std/Actions) and [Streams](https://github.com/dafny-lang/dafny/tree/actions-and-streaming-stdlibs/Source/DafnyStandardLibraries/src/Std/Streams) Dafny libraries, but they are still under construction and I'm not claiming they will not change before being merged. Interface feedback is welcome but is not intended to be a hard requirement in scope for this review.

Author: robin-aws

.github/not-grep.toml

@@ -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 }}

.github/workflows/pull.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 }}

.github/workflows/push.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/[email protected]
         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/[email protected]

.github/workflows/smithy-polymorph.yml

@@ -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 = [email protected]:dafny-lang/dafny.git
+	branch = actions-and-streaming-stdlibs

.gitmodules

@@ -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.

SmithyDafnyMakefile.mk

@@ -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"