Add optimizable bulk operations to Actions, native and external SetReaders #6274
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…-streaming-stdlibs
…-streaming-stdlibs # Conflicts: # Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
…-streaming-stdlibs
…ing-libs # Conflicts: # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
…o more-streaming-libs
robin-aws
changed the title
MikaelMayer
reviewed
Jun 20, 2025
Source/DafnyStandardLibraries/examples/TargetSpecific/ActionsExternsExamples-cs-java.dfy
Outdated
Show resolved
Hide resolved
MikaelMayer
approved these changes
Jun 24, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
What was changed?
Adds bulk operations to the Actions library -
Producer.ForEach(renamed fromForEachRemaining),Producer.Fill, andBulkAction.Map- which can use type tests to optimize for common producers and consumers. This is particularly useful when using these traits to handle binary data, especially in streaming workflows, since it allows simple modelling of operations in terms of individual byte values, but does not force actually processing individual bytes at a time (which can introduce a lot of overhead, especially in languages like Java where the type system forces boxing values intoBytewrappers).Also:
ValidChange()toValidatableand several related helper predicates/lemmas/etc, since the specification of the bulk actions heavily relied on twostate invariants of actions such asold(history) <= history.ActionsExterns.MakeSetReader<T>(s: set<T>), which creates aProducer<T>that reads the contents of a set in nondeterministic order in linear time. This is currently only implemented for Java and C#.--hidden-no-verifyoption recorded in doo files even though it is still normally unchecked, but added Makefile tests to ensure this is never used in checked-in doo files.How has this been tested?
Added lots of additional examples. Note that the bulk operations are not really tested super well, especially in the use case of interacting with external producers and consumers, but a pending change to https://github.com/smithy-lang/smithy-dafny will have substantially more coverage by using these traits to support streaming for services such as S3.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.