Use mainline Dafny standard library for streaming, support Java

.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.7.0','4.9.1']" >> $GITHUB_OUTPUT
+        run: echo "dafny-versions-list=['4.7.0','4.9.1','nightly-2025-06-29-f5ca47b']" >> $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.9.1']" >> $GITHUB_OUTPUT
+        run: echo "only-new-dafny-versions-list=['4.9.1','nightly-2025-06-29-f5ca47b']" >> $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 }}

.gitmodules

@@ -4,4 +4,3 @@
 [submodule "TestModels/dafny-dependencies/dafny"]
 	path = TestModels/dafny-dependencies/dafny
 	url = https://github.com/dafny-lang/dafny.git
-	branch = actions-and-streaming-stdlibs

SmithyDafnyMakefile.mk

@@ -30,6 +30,7 @@
 #   of Model directories
 # AWS_SDK_CMD -- the `--aws-sdk` command to generate AWS SDK style interfaces.
 # STD_LIBRARY -- path from this file to the StandardLibrary Dafny project.
+# STREAMING_SUPPORT -- path from this file to the StreamingSupport Dafny project.
 # SMITHY_DEPS -- path from this file to smithy dependencies, such as custom traits.
 # GRADLEW -- the gradlew to use when building Java runtimes.
 #   defaults to $(SMITHY_DAFNY_ROOT)/codegen/gradlew
@@ -98,7 +99,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, ) \
+		$(if $(USES_STREAMING), --library:$(PROJECT_ROOT)/$(STREAMING_SUPPORT)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(DAFNY_OPTIONS) \
 		%
 
@@ -115,7 +116,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, ) \
+		$(if $(USES_STREAMING), --library:$(PROJECT_ROOT)/$(STREAMING_SUPPORT)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(DAFNY_OPTIONS) \
 		$(if ${PROC},-proc:*$(PROC)*,) \
 		$(FILE)
@@ -215,7 +216,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, ) \
+		$(if $(USES_STREAMING) , --library:$(PROJECT_ROOT)/$(STREAMING_SUPPORT)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES)
 
@@ -255,7 +256,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, ) \
+		$(if $(USES_STREAMING) , --library:$(PROJECT_ROOT)/$(STREAMING_SUPPORT)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
 		$(TRANSLATION_RECORD) \
 		$(SOURCE_TRANSLATION_RECORD) \
 		$(TRANSPILE_MODULE_NAME) \
@@ -264,7 +265,8 @@ 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) USE_DAFNY_STANDARD_LIBRARIES=$(USE_DAFNY_STANDARD_LIBRARIES), )
+	$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG) USES_STREAMING=$(USES_STREAMING), )
+	$(if $(USES_STREAMING), $(MAKE) -C $(PROJECT_ROOT)/$(STREAMING_SUPPORT) transpile_implementation_$(LANG) USES_STREAMING=$(USES_STREAMING), )
 	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES))
 
 transpile_dependencies_test:
@@ -337,7 +339,8 @@ _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) USE_DAFNY_STANDARD_LIBRARIES=$(USE_DAFNY_STANDARD_LIBRARIES), )
+	$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) polymorph_$(POLYMORPH_LANGUAGE_TARGET) LIBRARY_ROOT=$(PROJECT_ROOT)/$(STD_LIBRARY) USES_STREAMING=$(USES_STREAMING), )
+	$(if $(USES_STREAMING), $(MAKE) -C $(PROJECT_ROOT)/$(STREAMING_SUPPORT) polymorph_$(POLYMORPH_LANGUAGE_TARGET) LIBRARY_ROOT=$(PROJECT_ROOT)/$(STREAMING_SUPPORT) USES_STREAMING=$(USES_STREAMING), )
 	@$(foreach dependency, \
 		$(PROJECT_DEPENDENCIES), \
 		$(MAKE) -C $(PROJECT_ROOT)/$(dependency) polymorph_$(POLYMORPH_LANGUAGE_TARGET); \
@@ -359,7 +362,8 @@ polymorph_code_gen:
 _polymorph_code_gen: OUTPUT_DAFNY=\
     --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
 _polymorph_code_gen: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_code_gen: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
 _polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
@@ -386,7 +390,8 @@ polymorph_dafny:
 _polymorph_dafny: OUTPUT_DAFNY=\
 		--output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
 _polymorph_dafny: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_dafny: _polymorph
 
 dafny: polymorph_dafny verify
@@ -409,7 +414,8 @@ polymorph_dotnet:
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
 _polymorph_dotnet: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_dotnet: _polymorph
 
 # Generates java code for all namespaces in this project
@@ -427,7 +433,8 @@ polymorph_java:
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
 _polymorph_java: INPUT_DAFNY=\
-	--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+	--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_java: _polymorph
 
 # Generates python code for all namespaces in this project
@@ -593,6 +600,7 @@ transpile_dependencies_java: transpile_dependencies
 # Locally deploy all other dependencies 
 mvn_local_deploy_dependencies:
 	$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) mvn_local_deploy, )
+	$(if $(USES_STREAMING), $(MAKE) -C $(PROJECT_ROOT)/$(STREAMING_SUPPORT) mvn_local_deploy, )
 	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% mvn_local_deploy;, $(PROJECT_DEPENDENCIES))
 
 # The Java MUST all exist already through the transpile step.

TestModels/SharedMakefile.mk

@@ -7,6 +7,7 @@
 PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
 SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/..
 STD_LIBRARY := dafny-dependencies/StandardLibrary
+STREAMING_SUPPORT := dafny-dependencies/StreamingSupport
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 
@@ -16,7 +17,8 @@ include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
 _polymorph_code_gen: OUTPUT_DAFNY=\
     --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
 _polymorph_code_gen: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_code_gen: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
 _polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
@@ -45,7 +47,8 @@ polymorph_dafny:
 _polymorph_dafny: OUTPUT_DAFNY=\
 		--output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
 _polymorph_dafny: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_dafny: _polymorph
 _polymorph_dafny: OUTPUT_DAFNY_WRAPPED=\
     --output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model) \
@@ -55,15 +58,17 @@ _polymorph_dafny: _polymorph_wrapped
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
 _polymorph_java: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy  \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_java: _polymorph
 _polymorph_java: OUTPUT_JAVA_WRAPPED=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: _polymorph_wrapped
 
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
 _polymorph_dotnet: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy  \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 _polymorph_dotnet: _polymorph
 _polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped)
@@ -77,7 +82,8 @@ _polymorph_python: _polymorph_wrapped
 
 _polymorph_rust: OUTPUT_RUST_WRAPPED=--output-rust $(LIBRARY_ROOT)/runtimes/rust
 _polymorph_rust: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(USES_STREAMING), --include-dafny $(PROJECT_ROOT)/$(STREAMING_SUPPORT)/src/Index.dfy, )
 # For several TestModels we've just manually written the code generation target,
 # So we just want to ensure we can transpile and pass the tests in CI.
 # For those, make polymorph_rust should just be a no-op.

TestModels/Streaming/Makefile

@@ -3,7 +3,7 @@
 
 CORES=2
 
-USE_DAFNY_STANDARD_LIBRARIES=1
+USES_STREAMING=1
 
 ENABLE_EXTERN_PROCESSING=1
 
@@ -20,8 +20,9 @@ SERVICE_DEPS_SimpleStreaming :=
 
 SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 
-# This project has no dependencies 
-# DEPENDENT-MODELS:= 
+PROJECT_DEPENDENCIES :=
+
+PROJECT_INDEX :=
 
 # Python
 

TestModels/Streaming/Model/SimpleStreamingTypes.dfy

@@ -2,12 +2,13 @@
 // 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"
+include "../../dafny-dependencies/StreamingSupport/src/Index.dfy"
 module {:extern "simple.streaming.internaldafny.types" } SimpleStreamingTypes
 {
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-  import opened Std.Streams
+  import opened StandardLibrary.Streams
   // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
@@ -17,17 +18,17 @@ module {:extern "simple.streaming.internaldafny.types" } SimpleStreamingTypes
     nameonly number: int32
   )
   datatype BinaryOfOutput = | BinaryOfOutput (
-    nameonly binary: ByteStream
+    nameonly binary: DataStream<uint8, Error>
   )
   datatype ChunksInput = | ChunksInput (
-    nameonly bytesIn: ByteStream ,
+    nameonly bytesIn: DataStream<uint8, Error> ,
     nameonly chunkSize: CountingInteger
   )
   datatype ChunksOutput = | ChunksOutput (
-    nameonly bytesOut: ByteStream
+    nameonly bytesOut: DataStream<uint8, Error>
   )
   datatype CountBitsInput = | CountBitsInput (
-    nameonly bits: ByteStream
+    nameonly bits: DataStream<uint8, Error>
   )
   datatype CountBitsOutput = | CountBitsOutput (
     nameonly sum: int32
@@ -79,12 +80,8 @@ module {:extern "simple.streaming.internaldafny.types" } SimpleStreamingTypes
       returns (output: Result<CountBitsOutput, Error>)
       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
+               History`CountBits
       // Dafny will skip type parameters when generating a default decreases clause.
       decreases Modifies - {History}
       ensures
@@ -106,8 +103,6 @@ module {:extern "simple.streaming.internaldafny.types" } 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<ChunksOutput, Error>)
     // The public method to be called by library consumers
@@ -123,14 +118,12 @@ module {:extern "simple.streaming.internaldafny.types" } SimpleStreamingTypes
         && 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
+  type StreamingBlob = DataStream<uint8, Error>
   datatype Error =
       // Local Error structures are listed here
     | OverflowError (
@@ -180,7 +173,7 @@ abstract module AbstractSimpleStreamingService
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-  import opened Std.Streams
+  import opened StandardLibrary.Streams
   import opened Types = SimpleStreamingTypes
   import Operations : AbstractSimpleStreamingOperations
   function method DefaultSimpleStreamingConfig(): SimpleStreamingConfig
@@ -220,23 +213,15 @@ abstract module AbstractSimpleStreamingService
       returns (output: Result<CountBitsOutput, Error>)
       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
+               History`CountBits
       // 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)];
     }
@@ -256,8 +241,6 @@ 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)];
@@ -289,7 +272,7 @@ abstract module AbstractSimpleStreamingOperations {
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-  import opened Std.Streams
+  import opened StandardLibrary.Streams
   import opened Types = SimpleStreamingTypes
   type InternalConfig
   predicate ValidInternalConfig?(config: InternalConfig)
@@ -301,12 +284,8 @@ abstract module AbstractSimpleStreamingOperations {
   method CountBits ( config: InternalConfig , input: CountBitsInput )
     returns (output: Result<CountBitsOutput, Error>)
     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
+    modifies ModifiesInternalConfig(config)
     // Dafny will skip type parameters when generating a default decreases clause.
     decreases ModifiesInternalConfig(config)
     ensures
@@ -328,8 +307,6 @@ 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<ChunksOutput, Error>)
@@ -340,8 +317,6 @@ abstract module AbstractSimpleStreamingOperations {
     returns (output: Result<ChunksOutput, Error>)
     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)