feat: SimpleDouble for Rust (#387)

.github/workflows/test_models_rust_tests.yml

@@ -35,7 +35,7 @@ jobs:
             TestModels/SimpleTypes/SimpleBlob,
             TestModels/SimpleTypes/SimpleBoolean,
             # TestModels/SimpleTypes/SimpleByte,
-            # TestModels/SimpleTypes/SimpleDouble,
+            TestModels/SimpleTypes/SimpleDouble,
             # TestModels/SimpleTypes/SimpleEnum,
             # TestModels/SimpleTypes/SimpleEnumV2,
             # TestModels/SimpleTypes/SimpleFloat,

TestModels/SimpleTypes/SimpleDouble/runtimes/rust/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "simple_double"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+dafny_runtime = { path = "../../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_standard_library = { path = "../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}
+simple_double_dafny = { path = "./dafny_impl"}
+
+[dependencies.aws-smithy-runtime]
+features = ["client"]
+
+[dependencies.aws-smithy-runtime-api]
+features = ["client"]
+
+[dependencies.aws-smithy-types]
+
+[dev-dependencies.tokio]
+version = "1.26.0"
+features = ["full"]

TestModels/SimpleTypes/SimpleDouble/runtimes/rust/README.md

@@ -0,0 +1,30 @@
+This directory is the code generation target for the SimpleInteger model when targetting Rust.
+
+Like the other targets, the crate is a combination of the output of three different components:
+
+1. The output of Dafny code generation for Rust (`src/implementation_from_dafny.rs`)
+2. The output of `smithy-dafny` shim/conversion generation for Rust (the `conversions` module)
+3. The output of `smithy-rs` (all other files)
+
+Most of the `smithy-rs` output is not modified,
+only trimmed down to cut out components that aren't relevant for Polymorph libraries.
+The main exception is `client.rs` and the operation builders such as `operation/get_integer.rs`,
+which instantiate the underlying Dafny client implementation and invoke operations on it, respectively,
+instead of sending the operation value through an orchestrated plugin stack
+that eventually serializes it and sends it to a remote service endpoint.
+
+This crate also includes manually-written Rust tests demonstrating what it's like
+to work with the Rust API we're exposing.
+Although we need to also get the Dafny-generated tests working,
+the manually-written ones are also valuable.
+
+It looks likely that `smithy-rs` is pluggable enough that we can plug our conversion code generation
+into it without having to fork its implementation.
+This means we should be able to get 2. and 3. above out of a single call to `smithy-rs`.
+Hence I've optimistically left the "// Code generated by software.amazon.smithy.rust.codegen.smithy-rs. DO NOT EDIT."
+header on both kinds of files.
+
+Note that even 1. is hand-modified, as the Dafny Rust code generator is not yet complete,
+and rejects some features such as the type paramter variance specifier on `Option<+T>`.
+We are trusting that Dafny will soon generate exactly the content of `implementation_from_dafny.rs`
+and it is a priority to set up CI to assert that ASAP.

TestModels/SimpleTypes/SimpleDouble/runtimes/rust/dafny_impl/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name = "simple_double_dafny"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+dafny_runtime = { path = "../../../../../dafny-dependencies/dafny_runtime_rust"}
+dafny_standard_library = { path = "../../../../../dafny-dependencies/StandardLibrary/runtimes/rust"}
+
+[lib]
+path = "src/implementation_from_dafny.rs"