Supports compiling the common Dafny tests in a test model for Rust. This involved having to change some properties of how we lay out the Rust crates:
Removed the dafny_impl sub-crate and moved implementation_from_dafny.rs into the main src directory - hence replacing ::simple_boolean_dafny with crate::implementation_from_dafny everywhere. I originally had this separated to better divide Dafny-generated code from Smithy-generated code, but it made implementing externs hard/impossible, and Dafny tests make use of "wrapped services" which are essentially testing-only extern shims.
Added tests/tests_from_dafny/_wrapped.rs with the implementation of the "wrapped service", which is implementing the Dafny-client interface using the Rust idiomatic client.
Removed async from the client interfaces - we'd originally kept these for better forwards-compatibility, but AFAICT it's impossible to implement the synchronous Dafny-generated trait methods with async methods. This just means that in the future we'll eventually have to provide separate async clients, but that's happened with the AWS SDKs frequently as well.
Raised the visibility of a few things in the main crate to pub so that the dafny_tests integration test crate can see them - open to feedback here on whether it's reasonable or we should find a better solution.
Not ready to merge yet because this relies on a newer Dafny feature branch commit, which I'll tackle in a separate PR first since it will be noisy to update all the patch files.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Issue #, if available: Resolves #458
Description of changes:
Supports compiling the common Dafny tests in a test model for Rust. This involved having to change some properties of how we lay out the Rust crates:
dafny_implsub-crate and movedimplementation_from_dafny.rsinto the mainsrcdirectory - hence replacing::simple_boolean_dafnywithcrate::implementation_from_dafnyeverywhere. I originally had this separated to better divide Dafny-generated code from Smithy-generated code, but it made implementing externs hard/impossible, and Dafny tests make use of "wrapped services" which are essentially testing-only extern shims.tests/tests_from_dafny/_wrapped.rswith the implementation of the "wrapped service", which is implementing the Dafny-client interface using the Rust idiomatic client.asyncfrom the client interfaces - we'd originally kept these for better forwards-compatibility, but AFAICT it's impossible to implement the synchronous Dafny-generated trait methods with async methods. This just means that in the future we'll eventually have to provide separate async clients, but that's happened with the AWS SDKs frequently as well.pubso that thedafny_testsintegration test crate can see them - open to feedback here on whether it's reasonable or we should find a better solution.Not ready to merge yet because this relies on a newer Dafny feature branch commit, which I'll tackle in a separate PR first since it will be noisy to update all the patch files.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.