feat(Rust): Interop test vectors; bump Dafny to 4.9.0 (#1004)

.github/workflows/library_interop_tests.yml

@@ -25,7 +25,7 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        language: [java, net, python]
+        language: [java, net, python, rust]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -37,11 +37,19 @@ jobs:
         run: |
           git config --global core.longpaths true
 
+      # Test Vectors need to call KMS
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
+          role-session-name: InterOpTests
+
       - uses: actions/checkout@v3
       #  Not all submodules are needed.
       # We manually pull the submodule we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       # Set up runtimes
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
@@ -50,8 +58,9 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      # Setup Java in Rust is needed for running polymorph
       - name: Setup Java 17
-        if: matrix.language == 'java'
+        if: matrix.language == 'java' || matrix.language == 'rust'
         uses: actions/setup-java@v3
         with:
           distribution: "corretto"
@@ -67,8 +76,32 @@ jobs:
           pip install --upgrade tox
           pip install poetry
 
+      - name: Setup Rust Toolchain for GitHub CI
+        if: matrix.language == 'rust'
+        uses: actions-rust-lang/[email protected]
+        with:
+          components: rustfmt
+      # TODO - uncomment this after Rust formatter works
+      # - name: Rustfmt Check
+      #   uses: actions-rust-lang/rustfmt@v1
+
+      # TODO: Remove this after the formatting in Rust starts working
+      - name: smithy-dafny Rust hacks
+        if: matrix.language == 'rust'
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
+          else
+            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
+          fi
+
+      - name: Setup NASM for Windows in Rust (aws-lc-sys)
+        if: matrix.language == 'rust' && matrix.os == 'windows-latest'
+        uses: ilammy/setup-nasm@v1
+
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.7.0
         with:
           dafny-version: ${{ inputs.dafny }}
 
@@ -108,20 +141,32 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_python
 
+      - name: Install Smithy-Dafny codegen dependencies
+        if: matrix.language == 'rust'
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      # TODO: Remove this after checking in Rust polymorph code
+      - name: Run make polymorph_rust
+        if: matrix.language == 'rust'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make polymorph_rust
+
+      - name: Build ${{ matrix.library }} implementation in Rust
+        if: matrix.language == 'rust'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_rust TRANSPILE_TESTS_IN_RUST=1 CORES=$CORES
+
       - name: Setup gradle
         if: matrix.language == 'java'
         uses: gradle/gradle-build-action@v2
         with:
           gradle-version: 7.2
 
-      # Test Vectors need to call KMS
-      - name: Configure AWS Credentials for Tests
-        uses: aws-actions/configure-aws-credentials@v2
-        with:
-          aws-region: us-west-2
-          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-MPL-Dafny-Role-us-west-2
-          role-session-name: InterOpTests
-
       - name: Create Manifests
         working-directory: ./${{ matrix.library }}
         run: make test_generate_vectors_${{ matrix.language }}
@@ -147,8 +192,8 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        encrypting_language: [java, net, python]
-        decrypting_language: [java, net, python]
+        encrypting_language: [java, net, python, rust]
+        decrypting_language: [java, net, python, rust]
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
     permissions:
@@ -158,6 +203,7 @@ jobs:
       - name: Support longpaths on Git checkout
         run: |
           git config --global core.longpaths true
+
       # KMS and MPL tests need to use credentials which can call KMS
       - name: Configure AWS Credentials for Tests
         uses: aws-actions/configure-aws-credentials@v2
@@ -170,7 +216,7 @@ jobs:
       #  Not all submodules are needed.
       # We manually pull the submodule we DO need.
       - run: git submodule update --init libraries
-      - run: git submodule update --init smithy-dafny
+      - run: git submodule update --init --recursive smithy-dafny
 
       # Set up runtimes
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
@@ -179,8 +225,9 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      # Setup Java in Rust is needed for running polymorph
       - name: Setup Java 17
-        if: matrix.decrypting_language == 'java'
+        if: matrix.decrypting_language == 'java' || matrix.decrypting_language == 'rust'
         uses: actions/setup-java@v3
         with:
           distribution: "corretto"
@@ -196,6 +243,30 @@ jobs:
           pip install --upgrade tox
           pip install poetry
 
+      - name: Setup Rust Toolchain for GitHub CI
+        if: matrix.decrypting_language == 'rust'
+        uses: actions-rust-lang/[email protected]
+        with:
+          components: rustfmt
+      # TODO - uncomment this after Rust formatter works
+      # - name: Rustfmt Check
+      #   uses: actions-rust-lang/rustfmt@v1
+
+      # TODO: Remove this after the formatting in Rust starts working
+      - name: smithy-dafny Rust hacks
+        if: matrix.decrypting_language == 'rust'
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
+          else
+            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' smithy-dafny/SmithyDafnyMakefile.mk
+          fi
+
+      - name: Setup NASM for Windows in Rust (aws-lc-sys)
+        if: matrix.decrypting_language == 'rust' && matrix.os == 'windows-latest'
+        uses: ilammy/setup-nasm@v1
+
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
@@ -237,6 +308,26 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_python
 
+      - name: Install Smithy-Dafny codegen dependencies
+        if: matrix.decrypting_language == 'rust'
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      # TODO: Remove this after checking in Rust polymorph code
+      - name: Run make polymorph_rust
+        if: matrix.decrypting_language == 'rust'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make polymorph_rust
+
+      - name: Build ${{ matrix.library }} implementation in Rust
+        if: matrix.decrypting_language == 'rust'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_rust TRANSPILE_TESTS_IN_RUST=1 CORES=$CORES
+
       - name: Download Encrypt Manifest Artifact
         uses: actions/download-artifact@v4
         with:

.github/workflows/library_rust_tests.yml

@@ -66,7 +66,7 @@ jobs:
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: nightly-latest
+          dafny-version: 4.9.0
 
       # TODO: Remove this after the formatting in Rust starts working
       - name: smithy-dafny Rust hacks

.gitignore

@@ -5,7 +5,7 @@
 build/*
 test/**/Output/*
 /package-lock.json
-/node_modules
+node_modules
 *.log
 
 # Python docs build Artifacts

AwsCryptographicMaterialProviders/project.properties

@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.8.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0

AwsCryptographyPrimitives/project.properties

@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.8.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0

ComAmazonawsDynamodb/project.properties

@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.8.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0

ComAmazonawsDynamodb/runtimes/rust/Cargo.toml

@@ -3,14 +3,6 @@ name = "aws-mpl-ddb"
 version = "0.1.0"
 edition = "2021"
 rust-version = "1.80.0"
-keywords = ["crypto", "cryptography", "security", "encryption", "client-side", "clientside"]
-license = "ISC AND (Apache-2.0 OR ISC)"
-description = "aws-esdk is a library for implementing client side encryption."
-homepage = "https://github.com/aws/aws-database-encryption-sdk-dynamodb/tree/main/releases/rust/db_esdk"
-repository = "https://github.com/aws/aws-database-encryption-sdk-dynamodb/tree/main/releases/rust/db_esdk"
-authors = ["AWS-CryptoTools"]
-documentation = "https://docs.rs/crate/aws-esdk"
-readme = "README.md"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

ComAmazonawsKms/project.properties

@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.8.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0

TestVectorsAwsCryptographicMaterialProviders/Makefile

@@ -95,6 +95,38 @@ WRAPPED_INDEX_FILE_PATH=dafny/TestVectorsAwsCryptographicMaterialProviders/src/L
 WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.materialproviders.internaldafny.wrapped\" } WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService"
 WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedMaterialProviders refines WrappedAbstractAwsCryptographyMaterialProvidersService"
 
+# Rust SED Hacks
+IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE=runtimes/rust/src/implementation_from_dafny.rs
+IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN="WrappedMaterialProvidersMain::_default::Main();"
+IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN= \
+	"let args: Vec<String> = std::env::args().collect();\
+	let dafny_strings = args.iter().map(|x| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(\&x)).collect::<Vec<_>>();\
+	let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings);\
+	r\#_WrappedMaterialProvidersMain_Compile::_default::Main(\&dafny_args);"
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1 = "\#\[cfg(feature = \"wrapped-client\")\]"
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;'
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;'
+REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;'
+
+transpile_implementation_rust: _replace_main_method_name_rust
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+_polymorph_rust: _remove_wrapped_client_rust
+
+_replace_main_method_name_rust:
+	$(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN)
+
+# TODO: Remove after wrapped client issue is fixed in Rust
+_remove_wrapped_client_rust:
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
+	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2)
+
 # Python
 
 # smithy.api namespace is a workaround for having a wrapped localService shim in a different Python package,
@@ -145,6 +177,12 @@ test_generate_vectors_python:
 	python3 -m tox -c runtimes/python --verbose -e cli -- encrypt-manifest --encrypt-manifest-output runtimes/python
 	cp dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json runtimes/python
 
+test_generate_vectors_rust:
+	cd runtimes/rust && \
+	cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt-manifest --encrypt-manifest-output . && \
+	cd ../../
+	cp dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json runtimes/rust/
+
 test_encrypt_vectors_java:
 	gradle -p runtimes/java run --args="encrypt --manifest-path . --decrypt-manifest-path ."
 
@@ -158,6 +196,11 @@ test_encrypt_vectors_python:
 	rm -rf runtimes/python/.tox
 	python3 -m tox -c runtimes/python --verbose -e cli -- encrypt --manifest-path runtimes/python --decrypt-manifest-path runtimes/python
 
+test_encrypt_vectors_rust:
+	cd runtimes/rust && \
+	cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt --manifest-path . --decrypt-manifest-path . && \
+	cd ../../
+
 test_decrypt_encrypt_vectors_java:
 	gradle -p runtimes/java run --args="decrypt --manifest-path ."
 
@@ -170,3 +213,8 @@ test_decrypt_encrypt_vectors_net:
 test_decrypt_encrypt_vectors_python:
 	rm -rf runtimes/python/.tox
 	python3 -m tox -c runtimes/python --verbose -e cli -- decrypt --manifest-path runtimes/python
+
+test_decrypt_encrypt_vectors_rust:
+	cd runtimes/rust && \
+	cargo run --bin test-vectors --features="wrapped-client" --release -- decrypt --manifest-path . && \
+	cd ../../

TestVectorsAwsCryptographicMaterialProviders/project.properties

@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.8.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0

TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/.gitignore

@@ -36,3 +36,5 @@ src/client.rs
 src/aes_kdf_ctr.rs
 src/aes_gcm.rs
 Cargo.lock
+
+/*.json

TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml

@@ -1,11 +1,14 @@
 [package]
-name = "aws-esdk-test-vectors"
+name = "aws-mpl-test-vectors"
 version = "0.1.0"
 edition = "2021"
 rust-version = "1.80.0"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
+[features]
+wrapped-client = []
+
 [dependencies]
 aws-config = "1.5.8"
 aws-lc-rs = "1.10.0"
@@ -21,3 +24,10 @@ dashmap = "6.1.0"
 pem = "3.0.4"
 tokio = {version = "1.41.0", features = ["full"] }
 uuid = { version = "1.11.0", features = ["v4"] }
+
+[dev-dependencies]
+aws-mpl-test-vectors = { path = ".", features = ["wrapped-client"] }
+
+[[bin]]
+name = "test-vectors"
+path = "src/main.rs"

TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/lib.rs → TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/src/main.rs

@@ -62,3 +62,10 @@ pub(crate) use crate::implementation_from_dafny::UUID;
 pub(crate) use crate::implementation_from_dafny::_StormTracker_Compile;
 pub(crate) use crate::implementation_from_dafny::_LocalCMC_Compile;
 pub(crate) use crate::implementation_from_dafny::_TestWrappedMaterialProvidersMain_Compile;
+
+fn main() {
+    let args: Vec<String> = std::env::args().collect();
+    let dafny_strings = args.iter().map(|x| dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&x)).collect::<Vec<_>>();
+    let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings);
+    crate::implementation_from_dafny::r#_WrappedMaterialProvidersMain_Compile::_default::Main(&dafny_args);
+}