chore(examples): Add examples for Rust Encryption SDK (#685)

.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.0'
+      dafny: '4.8.1'
   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.0'
+      dafny: '4.8.1'
   # daily-ci-java:
   #   if: github.event_name != 'schedule' || github.repository_owner == 'aws'
   #   uses: ./.github/workflows/library_java_tests.yml
@@ -27,10 +27,15 @@ jobs:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'
+  daily-ci-rust:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_rust_tests.yml
+    with:
+      dafny: '4.8.1'
 
   daily-ci-interop-tests:
     if: github.event_name != 'schedule' || github.repository_owner == 'aws'
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'

.github/workflows/library_rust_tests.yml

@@ -0,0 +1,159 @@
+# This workflow performs tests in Rust.
+name: Library Rust tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: 'The Dafny version to run'
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+
+# env:
+  # Used for Test Vectors
+  # VECTORS_URL: https://github.com/awslabs/aws-encryption-sdk-test-vectors/raw/master/vectors/awses-decrypt/python-2.3.0.zip
+
+jobs:
+  testRust:
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [
+          windows-latest,
+          ubuntu-latest,
+          macos-12,
+        ]
+    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
+      - name: Init Submodules
+        shell: bash
+        run: |
+          git submodule update --init libraries
+          git submodule update --init --recursive mpl
+          git submodule update --init --recursive smithy-dafny
+
+      - 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: RustTests
+
+      - 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
+        # TODO: Use [email protected] for Rust instead of rust-unsound branch
+        # uses: dafny-lang/[email protected]
+        # with:
+        #   dafny-version: ${{ inputs.dafny }}
+        shell: bash
+        run: |
+          git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
+          cd dafny/
+          make exe
+
+          echo $PWD/Scripts >> $GITHUB_PATH
+
+      # 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|#&|' 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 Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: "17"
+
+      - 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: AwsEncryptionSDK
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
+      # TODO: Remove this after checking in Rust polymorph code
+      - name: Run make polymorph_rust
+        shell: bash
+        working-directory: ./AwsEncryptionSDK
+        run: |
+          make polymorph_rust
+
+      - name: Compile AwsEncryptionSDK implementation
+        shell: bash
+        working-directory: ./AwsEncryptionSDK
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_rust TRANSPILE_TESTS_IN_RUST=1 CORES=$CORES
+
+      # Remove Rust hacks
+      - 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: Compile MPL TestVectors implementation
+      #   shell: bash
+      #   working-directory: ./mpl/TestVectorsAwsCryptographicMaterialProviders
+      #   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: Test Rust
+        working-directory: ./AwsEncryptionSDK
+        shell: bash
+        run: |
+          make test_rust
+
+      - name: Test Examples for Rust
+        working-directory: ./AwsEncryptionSDK/runtimes/rust
+        shell: bash
+        run: |
+          cargo test --examples

.github/workflows/manual.yml

@@ -32,3 +32,8 @@ jobs:
     with:
       dafny: ${{ inputs.dafny }}
       regenerate-code: ${{ inputs.regenerate-code }}
+  manual-ci-rust:
+    uses: ./.github/workflows/library_rust_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}
+      regenerate-code: ${{ inputs.regenerate-code }}

.github/workflows/nighly_dafny.yml

@@ -31,6 +31,12 @@ jobs:
     with:
       dafny: 'nightly-latest'
       regenerate-code: true
+  dafny-nightly-rust:
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    uses: ./.github/workflows/library_rust_tests.yml
+    with:
+      dafny: 'nightly-latest'
+      regenerate-code: true
 
   cut-issue-on-failure:
     runs-on: ubuntu-latest

.github/workflows/pull.yml

@@ -8,20 +8,24 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'
   pr-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'
   # 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.0'
+      dafny: '4.8.1'
+  pr-ci-rust:
+    uses: ./.github/workflows/library_rust_tests.yml
+    with:
+      dafny: '4.8.1'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'

.github/workflows/push.yml

@@ -10,20 +10,24 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'
   push-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'
   # 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.0'
+      dafny: '4.8.1'
+  push-ci-rust:
+    uses: ./.github/workflows/library_rust_tests.yml
+    with:
+      dafny: '4.8.1'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.8.0'
+      dafny: '4.8.1'

.gitignore

@@ -5,7 +5,7 @@
 build/*
 test/**/Output/*
 /package-lock.json
-/node_modules
+**/node_modules
 
 # Duvet output
 specification_compliance_report.html

AwsEncryptionSDK/.gitignore

@@ -5,3 +5,5 @@ TestsFromDafny.cs
 bin/
 obj/
 
+# Ignore *-cs.dtr files
+*-cs.dtr

AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/AwsCryptographyEncryptionSdkTypes.dfy

@@ -175,7 +175,7 @@ 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)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 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.0
-dafnyRuntimeJavaVersion=4.8.0
+dafnyVersion=4.8.1
+dafnyRuntimeJavaVersion=4.8.1