Add USE_DAFNY_STANDARD_LIBRARIES

SmithyDafnyMakefile.mk

@@ -95,7 +95,7 @@ verify:
 		--log-format csv \
 		--verification-time-limit $(VERIFY_TIMEOUT) \
 		--resource-limit $(MAX_RESOURCE_COUNT) \
-		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(DAFNY_OPTIONS) \
 		%
 
@@ -111,7 +111,7 @@ verify_single:
 		--log-format text \
 		--verification-time-limit $(VERIFY_TIMEOUT) \
 		--resource-limit $(MAX_RESOURCE_COUNT) \
-		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(DAFNY_OPTIONS) \
 		$(if ${PROC},-proc:*$(PROC)*,) \
 		$(FILE)
@@ -208,7 +208,7 @@ transpile_implementation:
 		$(DAFNY_OTHER_FILES) \
 		$(TRANSPILE_MODULE_NAME) \
 		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
-		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES)
 
@@ -246,7 +246,7 @@ transpile_test:
 		$(DAFNY_OPTIONS) \
 		$(DAFNY_OTHER_FILES) \
 		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
-		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(TRANSLATION_RECORD) \
 		$(SOURCE_TRANSLATION_RECORD) \
 		$(TRANSPILE_MODULE_NAME) \
@@ -328,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); \

TestModels/Streaming/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+USE_DAFNY_STANDARD_LIBRARIES=1
+
 include ../SharedMakefile.mk
 
 NAMESPACE=simple.streaming

TestModels/Streaming/Model/SimpleStreamingTypes.dfy

@@ -8,7 +8,7 @@ module SimpleStreamingTypes
   import opened StandardLibrary.UInt
   import opened StandardLibrary.Streams
   import opened UTF8
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
@@ -338,7 +338,7 @@ abstract module AbstractSimpleStreamingOperations {
     returns (output: Result<ChunksOutput, Error>)
     requires
       && ValidInternalConfig?(config)
-         // TODO: smithy-dafny isn't yet generating this
+      // 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.

TestModels/Streaming/Model/Streaming.smithy

@@ -28,6 +28,7 @@ service SimpleStreaming {
 
 structure SimpleStreamingConfig {}
 
+@suppress(["UnsupportedFeatures"])
 @streaming
 blob StreamingBlob
 

TestModels/aws-sdks/s3/Makefile

@@ -3,6 +3,7 @@
 
 ENABLE_EXTERN_PROCESSING=1
 CORES=2
+USE_DAFNY_STANDARD_LIBRARIES=1
 
 include ../../SharedMakefile.mk
 

TestModels/dafny-dependencies/StandardLibrary/Makefile

@@ -25,7 +25,7 @@ else
 endif
 
 # Overriding this target just to generate the project.properties file.
-polymorph_dafny:
+polymorph_dafny: $(if $(USE_DAFNY_STANDARD_LIBRARIES), build_dafny_stdlibs, )
 	cd $(CODEGEN_CLI_ROOT); \
 	$(GRADLEW) run --args="\
 	--library-root $(LIBRARY_ROOT) \

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 {
 
@@ -46,6 +48,15 @@ class PythonTestModels extends TestModelTest {
   void testModelsForPython(String relativeTestModelPath) {
     Assumptions.assumeFalse(DISABLED_TESTS.contains(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);
+      }
+    }
+
     Path testModelPath = getTestModelPath(relativeTestModelPath);
     make(testModelPath, "setup_prettier");
     make(testModelPath, "polymorph_dafny");