feat: partial @streaming blob support for Python

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

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

.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/[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]

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

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)
@@ -206,6 +208,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)
 
@@ -243,6 +246,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) \
@@ -251,7 +255,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:
@@ -324,7 +328,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); \
@@ -685,6 +689,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.

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"