feat(TestVectors): Add Rust support

.github/workflows/daily_ci.yml

@@ -11,13 +11,13 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   daily-ci-verification:
     # Don't run the cron builds on forks
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   # daily-ci-java:
   #   if: github.event_name != 'schedule' || github.repository_owner == 'aws'
   #   uses: ./.github/workflows/library_java_tests.yml
@@ -27,15 +27,15 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   daily-ci-rust:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_rust_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
 
   daily-ci-interop-tests:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'

.github/workflows/library_interop_test_vectors.yml

@@ -25,7 +25,7 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        language: [java, net]
+        language: [java, net, rust]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -38,6 +38,14 @@ jobs:
           run: |
             git config --global core.longpaths true
 
+        # TestVectors will call KMS
+        - 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: InterOpTests
+
         - uses: actions/checkout@v3
         #  Not all submodules are needed.
         # We manually pull the submodule we DO need.
@@ -51,15 +59,40 @@ 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"
             java-version: 17
 
+        - 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|#&|' 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 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 }}
 
@@ -89,21 +122,33 @@ jobs:
             # This works because `node` is installed by default on GHA runners
             CORES=$(node -e 'console.log(os.cpus().length)')
             make transpile_net
-
+
+        - 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
 
-        # TestVectors will call KMS
-        - 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: InterOpTests
-
         - name: Create Manifests
           working-directory: ./${{ matrix.library }}
           run: make test_generate_vectors_${{ matrix.language }}
@@ -132,8 +177,8 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        encrypting_language: [java, net]
-        decrypting_language: [java, net]
+        encrypting_language: [java, net, rust]
+        decrypting_language: [java, net, rust]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -145,6 +190,7 @@ jobs:
       - name: Support longpaths on Git checkout
         run: |
           git config --global core.longpaths true
+
       # TestVectors will call KMS
       - name: Configure AWS Credentials
         uses: aws-actions/configure-aws-credentials@v2
@@ -159,19 +205,45 @@ jobs:
       - run: git submodule update --init libraries
       - run: git submodule update --init --recursive mpl
 
+      # Set up runtimes
       - name: Setup .NET Core SDK ${{ matrix.dotnet-version }}
         if: matrix.decrypting_language == 'net'
         uses: actions/setup-dotnet@v3
         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"
           java-version: 17
 
+      - 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|#&|' 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 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:
@@ -204,6 +276,26 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_net
 
+      - 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

@@ -22,21 +22,17 @@ jobs:
         os: [
           windows-latest,
           ubuntu-latest,
-          macos-12,
+          macos-13,
         ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
       contents: read
-    env:
-      # TODO: do we need this here?
-      DOTNET_CLI_TELEMETRY_OPTOUT: 1
-      DOTNET_NOLOGO: 1
     steps:
       - name: Support longpaths on Git checkout
         run: |
           git config --global core.longpaths true
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - name: Init Submodules
         shell: bash
         run: |
@@ -81,6 +77,7 @@ jobs:
           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

.github/workflows/pull.yml

@@ -8,28 +8,28 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   pr-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
   #     dafny: '4.2.0'
   pr-ci-net:
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   pr-ci-rust:
     uses: ./.github/workflows/library_rust_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   pr-dafny-test-vectors:
     uses: ./.github/workflows/library_interop_test_vectors.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'

.github/workflows/push.yml

@@ -10,24 +10,24 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   push-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   # push-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
   #     dafny: '4.2.0'
   push-ci-net:
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   push-ci-rust:
     uses: ./.github/workflows/library_rust_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.1'
+      dafny: '4.9.0'

AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/java/dafny-4.9.0.patch

@@ -0,0 +1,13 @@
+diff --git a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java
+index 67ac1304..7282539c 100644
+--- a/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java
++++ b/AwsEncryptionSDK/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/encryptionsdk/model/EncryptInput.java
+@@ -192,7 +192,7 @@ public class EncryptInput {
+           "`frameLength` must be greater than or equal to 1"
+         );
+       }
+-      if (this._frameLengthSet && this.frameLength() > 4294967296) {
++      if (this._frameLengthSet && this.frameLength() > 4294967296L) {
+         throw new IllegalArgumentException(
+           "`frameLength` must be less than or equal to 4294967296."
+         );

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

@@ -175,8 +175,17 @@ module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.types"
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
-  type OpaqueError = e: Error | e.Opaque? witness *
+    | Opaque(obj: object)
+      // A better Opaque, with a visible string representation.
+    | OpaqueWithText(obj: object, objMessage : string)
+  type OpaqueError = e: Error | e.Opaque? || e.OpaqueWithText? witness *
+  // This dummy subset type is included to make sure Dafny
+  // always generates a _ExternBase___default.java class.
+  type DummySubsetType = x: int | IsDummySubsetType(x) witness 1
+  predicate method IsDummySubsetType(x: int) {
+    0 < x
+  }
+
 }
 abstract module AbstractAwsCryptographyEncryptionSdkService
 {

AwsEncryptionSDK/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.1
-dafnyRuntimeJavaVersion=4.8.1
+dafnyVersion=4.9.0
+dafnyRuntimeJavaVersion=4.9.0