chore: use --rust-module-name (#673)

Transpile Rust code with --rust-module-name, meaning that then generated implementation_from_dafny.rs file should not need to be edited; rather, a hand written lib.rs file is used instead.

The post-transpile patching steps were removed.

Most of the files changed are to bring each TestModel to the new scheme, i.e. we remove implementation_from_dafny.rs from the cargo.toml file and create a lib.rs file.

The version of Dafny used for testing was also bumped up to the current HEAD.

.github/workflows/pull.yml

@@ -53,7 +53,7 @@ jobs:
         # Rust code generation is under development and depends on pending changes to the
         # Dafny Rust code generation, so we test on a specific unreleased commit instead.
         dafny-version:
-          - 1d6d38326e967d78079fce3523bbaf35671cefff
+          - 5f2330113320f2af0476473fd267b5b547f94cba
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

SmithyDafnyMakefile.mk

@@ -58,6 +58,7 @@ GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnySedMakefile.mk
 
+
 # This flag enables pre-processing on extern module names.
 # This pre-processing is required to compile to Python and Go.
 # This is disabled by default.
@@ -79,6 +80,7 @@ ENABLE_EXTERN_PROCESSING?=
 #    ensures DAFNY_PROCESSES(cpus) * Z3_PROCESSES(cpus) <= cpus
 #  {}
 
+
 # Verify the entire project
 verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
 verify:DAFNY_PROCESSES=$(shell echo $$(( ($(CORES) - 1 ) / ($(CORES) >= 3 ? 2 : 1))))
@@ -558,23 +560,26 @@ rust: polymorph_dafny transpile_rust polymorph_rust test_rust
 
 # The Dafny Rust code generator only supports a single crate for everything,
 # so (among other consequences) we compile src and test code together.
-transpile_rust: | transpile_implementation_rust
+transpile_rust: copy_rust_externs transpile_implementation_rust
+
+copy_rust_externs:
+	runtimes/rust/copy_externs.sh || true
 
 transpile_implementation_rust: TARGET=rs
 transpile_implementation_rust: OUT=implementation_from_dafny
 transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX)
 transpile_implementation_rust: TEST_INDEX=$(RUST_TEST_INDEX)
 # The Dafny Rust code generator is not complete yet,
 # so we want to emit code even if there are unsupported features in the input.
-transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix
+transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix --rust-module-name implementation_from_dafny
 # The Dafny Rust code generator only supports a single crate for everything,
 # so we inline all dependencies by not passing `-library` to Dafny.
 transpile_implementation_rust: TRANSPILE_DEPENDENCIES=
 transpile_implementation_rust: STD_LIBRARY=
 transpile_implementation_rust: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
 transpile_implementation_rust: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
 transpile_implementation_rust: DAFNY_OTHER_FILES=$(RUST_OTHER_FILES)
-transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust patch_after_transpile_rust
+transpile_implementation_rust: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust
 
 transpile_dependencies_rust: LANG=rust
 transpile_dependencies_rust: transpile_dependencies
@@ -589,35 +594,13 @@ _mv_implementation_rust:
 	rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
 	rm -rf implementation_from_dafny-rust
 
-patch_after_transpile_rust:
-	export service_deps_var=SERVICE_DEPS_$(MAIN_SERVICE_FOR_RUST) ; \
-	export namespace_var=SERVICE_NAMESPACE_$(MAIN_SERVICE_FOR_RUST) ; \
-	export SERVICE=$(MAIN_SERVICE_FOR_RUST) ; \
-	$(MAKE) _patch_after_transpile_rust ; \
-
-_patch_after_transpile_rust: OUTPUT_RUST=--output-rust $(LIBRARY_ROOT)/runtimes/rust
-_patch_after_transpile_rust:
-	cd $(CODEGEN_CLI_ROOT); \
-	./../gradlew run --args="\
-	patch-after-transpile \
-	--library-root $(LIBRARY_ROOT) \
-	$(OUTPUT_RUST) \
-	--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \
-	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
-	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
-	--namespace $($(namespace_var)) \
-	$(AWS_SDK_CMD) \
-	$(POLYMORPH_OPTIONS) \
-	$(if $(TRANSPILE_TESTS_IN_RUST), --local-service-test, ) \
-	";
-
 build_rust:
 	cd runtimes/rust; \
 	cargo build
 
 test_rust:
 	cd runtimes/rust; \
-	cargo test -- --nocapture
+	cargo test --release -- --nocapture
 
 ########################## Cleanup targets
 
@@ -733,7 +716,7 @@ local_transpile_impl_rust_single: DAFNY_OTHER_FILES=$(RUST_OTHER_FILES)
 local_transpile_impl_rust_single: deps_var=SERVICE_DEPS_$(SERVICE)
 local_transpile_impl_rust_single: service_deps_var=SERVICE_DEPS_$(SERVICE)
 local_transpile_impl_rust_single: namespace_var=SERVICE_NAMESPACE_$(SERVICE)
-local_transpile_impl_rust_single: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust _patch_after_transpile_rust
+local_transpile_impl_rust_single: $(if $(TRANSPILE_TESTS_IN_RUST), transpile_test, transpile_implementation) _mv_implementation_rust
 
 
 local_transpile_impl_single: deps_var=SERVICE_DEPS_$(SERVICE)

TestModels/Aggregate/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ simple_aggregate = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Aggregate/runtimes/rust/src/lib.rs

@@ -0,0 +1,24 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_aggregate_config::SimpleAggregateConfig;
+pub use client::Client;

TestModels/Constraints/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ features = ["full"]
 
 [dev-dependencies]
 simple_constraints = { path = ".", features = ["wrapped-client"] }
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Constraints/runtimes/rust/src/lib.rs

@@ -0,0 +1,24 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_constraints_config::SimpleConstraintsConfig;
+pub use client::Client;

TestModels/Constructor/runtimes/rust/Cargo.toml

@@ -19,6 +19,3 @@ constructor = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Constructor/runtimes/rust/src/lib.rs

@@ -0,0 +1,24 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_constructor_config::SimpleConstructorConfig;
+pub use client::Client;

TestModels/Dependencies/runtimes/rust/Cargo.toml

@@ -19,6 +19,3 @@ dependencies = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Dependencies/runtimes/rust/src/lib.rs

@@ -0,0 +1,25 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::_WrappedSimpleDependenciesTest_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_dependencies_config::SimpleDependenciesConfig;
+pub use client::Client;

TestModels/Documentation/runtimes/rust/Cargo.toml

@@ -18,6 +18,3 @@ documentation = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Documentation/runtimes/rust/src/lib.rs

@@ -0,0 +1,23 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_documentation_config::SimpleDocumentationConfig;
+pub use client::Client;

TestModels/Errors/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ features = ["full"]
 
 [dev-dependencies]
 simple_errors = { path = ".", features = ["wrapped-client"] }
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Errors/runtimes/rust/src/lib.rs

@@ -0,0 +1,24 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub(crate) use crate::implementation_from_dafny::r#_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_errors_config::SimpleErrorsConfig;
+pub use client::Client;

TestModels/Extendable/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ features = ["full"]
 
 [dev-dependencies]
 simple_extendable = { path = ".", features = ["wrapped-client"] }
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/Extendable/runtimes/rust/src/lib.rs

@@ -0,0 +1,27 @@
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
+
+pub mod client;
+pub mod conversions;
+pub mod deps;
+/// Common errors and error handling utilities.
+pub mod error;
+pub(crate) mod implementation_from_dafny;
+/// All operations that this crate can perform.
+pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
+pub mod wrapped;
+pub mod factory;
+pub(crate) use crate::implementation_from_dafny::_SimpleExtendableResourcesTest_Compile;
+pub(crate) use crate::implementation_from_dafny::_WrappedTest_Compile;
+pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::simple;
+pub use crate::types::simple_extendable_resources_config::SimpleExtendableResourcesConfig;
+pub use client::Client;

TestModels/LanguageSpecificLogic/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ language_specific_logic = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"

TestModels/LanguageSpecificLogic/runtimes/rust/src/lib.rs

@@ -1,24 +1,27 @@
-#![allow(deprecated)]
-
-// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT.
+#![allow(
+    deprecated,
+    non_upper_case_globals,
+    unused,
+    non_snake_case,
+    non_camel_case_types
+)]
 
 pub mod client;
-pub mod types;
-
+pub mod conversions;
+pub mod deps;
+pub mod externs;
 /// Common errors and error handling utilities.
 pub mod error;
-
+pub(crate) mod implementation_from_dafny;
 /// All operations that this crate can perform.
 pub mod operation;
+mod standard_library_conversions;
+mod standard_library_externs;
+pub mod types;
 
-mod conversions;
-
-pub mod implementation_from_dafny;
-
-mod externs;
-
-#[cfg(feature = "wrapped-client")]
-pub mod wrapped;
-
+pub(crate) use crate::implementation_from_dafny::_Wrappers_Compile;
+pub(crate) use crate::implementation_from_dafny::UTF8;
+pub(crate) use crate::implementation_from_dafny::language;
+pub(crate) use crate::implementation_from_dafny::_LanguageSpecificLogicImpl_Compile;
+pub use crate::types::language_specific_logic_config::LanguageSpecificLogicConfig;
 pub use client::Client;
-pub use types::language_specific_logic_config::LanguageSpecificLogicConfig;

TestModels/LocalService/runtimes/rust/Cargo.toml

@@ -20,6 +20,3 @@ local_service = { path = ".", features = ["wrapped-client"] }
 [dependencies.tokio]
 version = "1.26.0"
 features = ["full"]
-
-[lib]
-path = "src/implementation_from_dafny.rs"