chore(test-vectors): Decrypt .NET Retry flag manifests using Rust

.github/workflows/library_net_tests.yml

@@ -165,7 +165,7 @@ jobs:
         with:
           aws-region: us-west-2
           role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 
-          role-session-name: NetTests
+          role-session-name: NetTestVectors
 
       - name: Setup .NET Core SDK 6
         uses: actions/setup-dotnet@v3

.github/workflows/library_rust_tests.yml

@@ -19,6 +19,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
+        library: [AwsEncryptionSDK]
         os: [
           windows-latest,
           ubuntu-latest,
@@ -53,11 +54,11 @@ jobs:
       # TODO - uncomment this after Rust formatter works
       # - name: Rustfmt Check
       #   uses: actions-rust-lang/rustfmt@v1
-      
+
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: 4.9.0
+          dafny-version: ${{ inputs.dafny }}
 
       # TODO: Remove this after the formatting in Rust starts working
       - name: smithy-dafny Rust hacks
@@ -87,59 +88,151 @@ jobs:
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}
-          library: AwsEncryptionSDK
+          library: ${{ matrix.library }}
           diff-generated-code: false
           update-and-regenerate-mpl: true
 
       # TODO: Remove this after checking in Rust polymorph code
+      # Also uncomment rust check_polymorph_diff for Rust in .github/actions/polymorph_codegen/action.yml
       - name: Run make polymorph_rust
         shell: bash
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         run: |
           make polymorph_rust
 
-      - name: Compile AwsEncryptionSDK implementation
+      - name: Compile ${{ matrix.library }} implementation
         shell: bash
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         run: |
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_rust CORES=$CORES
 
-      # Remove Rust hacks once Dafny fixes this
-      - name: Update implementation_from_dafny.rs to add deps
-        shell: bash
-        working-directory: ./AwsEncryptionSDK/runtimes/rust/src
-        run: |
-          if [ "$RUNNER_OS" == "macOS" ]; then
-            sed -i '' '/pub use types::aws_encryption_sdk_config::AwsEncryptionSdkConfig;/a\
-            pub use crate::deps::aws_cryptography_materialProviders;\
-            pub use crate::deps::aws_cryptography_keyStore;\
-            pub use crate::deps::com_amazonaws_kms;
-            ' implementation_from_dafny.rs
-          else
-            sed -i '/pub use types::aws_encryption_sdk_config::AwsEncryptionSdkConfig;/a\
-            pub use crate::deps::aws_cryptography_materialProviders;\
-            pub use crate::deps::aws_cryptography_keyStore;\
-            pub use crate::deps::com_amazonaws_kms;
-            ' implementation_from_dafny.rs
-          fi
-
       - name: Test Linter for Rust examples and implementation_from_dafny.rs
-        working-directory: ./AwsEncryptionSDK/runtimes/rust
+        working-directory: ${{ matrix.library }}/runtimes/rust
         shell: bash
         run: |
           cargo clippy
           cargo clippy --example main
 
       - name: Test Rust
-        working-directory: ./AwsEncryptionSDK
+        working-directory: ${{ matrix.library }}
         shell: bash
         run: |
           make test_rust
 
       - name: Test Examples for Rust
-        working-directory: ./AwsEncryptionSDK/runtimes/rust
+        working-directory: ${{ matrix.library }}/runtimes/rust
         shell: bash
         run: |
           cargo test --release --examples
+
+  testVectors:
+    strategy:
+      fail-fast: false
+      matrix:
+        library: [TestVectors]
+        os: [
+          # Sed script doesn't work properly on windows
+          # windows-latest,
+          ubuntu-latest,
+          macos-13,
+        ]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
+      - uses: actions/checkout@v3
+      - name: Init Submodules
+        shell: bash
+        run: |
+          git submodule update --init libraries
+          git submodule update --init --recursive mpl
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v2
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2
+          role-session-name: RustTestVectors
+
+      - name: Setup Rust Toolchain for GitHub CI
+        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
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      # TODO: Remove this after the formatting in Rust starts working
+      - name: smithy-dafny Rust hacks
+        shell: bash
+        run: |
+          if [ "$RUNNER_OS" == "macOS" ]; then
+            sed -i '' 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk
+          else
+            sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk
+          fi
+
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Setup NASM for Windows (aws-lc-sys)
+        if: matrix.os == 'windows-latest'
+        uses: ilammy/setup-nasm@v1
+
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ inputs.regenerate-code }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: ${{ matrix.library }}
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
+      # TODO: Remove this after checking in Rust polymorph code
+      # Also uncomment rust check_polymorph_diff for Rust in .github/actions/polymorph_codegen/action.yml
+      - name: Run make polymorph_rust
+        shell: bash
+        working-directory: ${{ matrix.library }}
+        run: |
+          make polymorph_rust
+
+      - name: Compile ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+            make transpile_rust CORES=$CORES
+
+      - name: Unzip .NET Retry Flag Manifests
+        shell: bash
+        working-directory: TestVectors/dafny/TestVectors/test/
+        run: |
+          unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0
+          unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1
+          unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0
+
+      - name: Test Rust
+        working-directory: ${{ matrix.library }}
+        shell: bash
+        run: |
+          # Without this, running test vectors fails due to `fatal runtime error: stack overflow`
+          export RUST_MIN_STACK=104857600
+          make test_rust

TestVectors/dafny/TestVectors/test/RunMain.dfy

@@ -60,7 +60,7 @@ module {:extern} TestWrappedESDKMain {
       )
     );
     print "ONLY WORRY IF THE ABOVE TESTS PASSED!!! THESE TESTS ARE SUPPOSED TO FAIL!\n";
-    print "IF THE TESTS FAIL OTHER THAN A AES GCM TAG VALIDATION EXCEPTION, CUT AN ISSUE.\n";
+    print "IF THE TESTS FAIL OTHER THAN A `AES GCM TAG VALIDATION EXCEPTION` or `AES Decrypt : gather Unspecified`, CUT AN ISSUE.\n";
     print "IF THE TESTS ALL FAIL IT MEANS THE TEST PASSED!";
     expect result.Failure?;
   }