chore: sync public with staging

.github/PULL_REQUEST_TEMPLATE.md

@@ -6,20 +6,3 @@
 
 
 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
-
-# Due to [dafny-lang/dafny#2500](https://github.com/dafny-lang/dafny/issues/2500), Traits are dangerous:
-1. [ ] Does this PR add any traits or classes that extend a trait?
-2. [ ] Are these traits annotated with `{:termination false}`?
-
-The override checks on 
-the specifications on
-a class' functions/methods/etc. validating
-that specifications are 
-at least as strong as those on
-the traits it implements
-are not working correctly when 
-that trait is defined in a different module 
-(and hence must have `{:termination false}` on it).
-
-As such, if either (1.) or (2.) is true:
-- [ ] manually verified all the trait specifications are copied onto classes that extend them?

.github/workflows/duvet.yaml

@@ -0,0 +1,50 @@
+# This workflow verifies
+# that the source is annotated
+# with respect to the specification
+name: Duvet report
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  duvet:
+    runs-on: ubuntu-latest
+    # This environment stores a token
+    # that can be used to checkout
+    # the ESDK specification
+    environment: "Duvet CI"
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          # This secret is in the configured environment
+          # Token created on # 12/14/2022
+          # expires in ~30 days 01/13/2023
+          token: ${{ secrets.PAT_SPEC }}
+          submodules: true
+
+      - name: Install duvet
+        shell: bash
+        run: |
+          cargo +stable install duvet
+
+      # //= aws-encryption-sdk-specification/framework/structures.md#overview
+      # //= type=implication
+      # //# These structures define a group of related fields that MUST hold certain properties.
+      # //# Wherever these structures are referenced in this specification,
+      # //# implementations MUST ensure that all properties of a structure's fields are upheld.
+      - name: Run the duvet report
+        shell: bash
+        run: |
+          make duvet
+
+      - uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: specification_compliance_report
+          path: specification_compliance_report.html

.github/workflows/library_dafny_verification.yml

@@ -0,0 +1,78 @@
+# This workflow performs static analysis checks.
+name: Library Dafny verification
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+  workflow_dispatch:
+    # Manual trigger for this workflow, either the normal version
+    # or the nightly build that uses the latest Dafny prerelease
+    # (accordingly to the "nightly" parameter).
+    inputs:
+      nightly:
+        description: 'Run the nightly build'
+        required: false
+        type: boolean
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  verification:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        library: [
+          AwsEncryptionSDK
+        ]
+        os: [ macos-latest ]
+    runs-on: ${{ matrix.os }}
+    environment: "MPL_DAFNY"
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
+    steps:
+      - uses: actions/checkout@v2
+      - name: Init Submodules
+        env:
+          # This secret is in the configured environment
+          # Token created on # 09/26/2023
+          # expires in ~30 days 10/26/2023
+          MPL_PAT: ${{ secrets.MPL_DAFNY }}
+        run: |
+            AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+            git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+            git config --global --add url.https://github.com/.insteadOf [email protected]:
+            git submodule update --init libraries
+            git submodule update --init --recursive mpl
+
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
+
+      - name: Verify ${{ matrix.library }} Dafny code
+        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 verify CORES=$CORES
+
+      - name: Check solver resource use
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make dafny-reportgenerator

.github/workflows/library_java_tests.yml

@@ -0,0 +1,169 @@
+# This workflow performs tests in Java.
+name: Library Java tests
+
+on: 
+  pull_request:
+  push:
+    branches:
+      - main
+  schedule:
+    # Nightly build against Dafny's nightly prereleases,
+    # for early warning of verification issues or regressions.
+    # Timing chosen to be adequately after Dafny's own nightly build,
+    # but this might need to be tweaked:
+    # https://github.com/dafny-lang/dafny/blob/master/.github/workflows/deep-tests.yml#L16
+    - cron: "30 16 * * *"
+
+jobs:
+  testJava:
+    # Don't run the nightly build on forks
+    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
+    strategy:
+      matrix:
+        library: [
+          #AwsEncryptionSDK
+        ]
+        os: [
+          # TODO just test on mac for now
+          #windows-latest,
+          #ubuntu-latest,
+          macos-latest
+        ]
+    runs-on: ${{ matrix.os }}
+    environment: "MPL_DAFNY"
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - uses: actions/checkout@v2
+      - name: Init Submodules
+        env:
+          # This secret is in the configured environment
+          # Token created on # 09/26/2023
+          # expires in ~30 days 10/26/2023
+          MPL_PAT: ${{ secrets.MPL_DAFNY }}
+        run: |
+            AUTH="$(echo -n "pat:${MPL_PAT}" | base64 | tr -d '\n')"
+            git config --global http.https://github.com/.extraheader "AUTHORIZATION: basic $AUTH"
+            git config --global --add url.https://github.com/.insteadOf [email protected]:
+            git submodule update --init libraries
+            git submodule update --init --recursive mpl
+
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v1
+        with:
+          aws-region: us-west-2
+          # TODO: This role was manually created.
+          role-to-assume: arn:aws:iam::370957321024:role/ESDK-Dafny-Private-CA-Read
+          role-session-name: JavaPrivateESDKDafnyTests
+
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
+        with:
+          # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
+
+      - name: Setup Java 8
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version:  8
+
+      - name: Build ${{ 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 build_java CORES=$CORES
+
+      # KMS and MPL tests need to use credentials which can call KMS
+      - name: Configure AWS Credentials for Tests
+        uses: aws-actions/configure-aws-credentials@v1
+        if: matrix.library == 'ComAmazonawsKms' || matrix.library == 'AwsCryptographicMaterialProviders' || matrix.library == 'TestVectorsAwsCryptographicMaterialProviders'
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2
+          role-session-name: JavaTests
+
+      - name: Test ${{ matrix.library }}
+        working-directory: ./${{ matrix.library }}
+        # TODO: DDB currently has no tests
+        if: matrix.library != 'ComAmazonawsDynamodb'
+        run: |
+          make test_java
+
+      - name: Setup Java 11
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: 11
+
+      - name: Clean for next Java
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: clean
+          build-root-directory: ./${{ matrix.library }}/runtimes/java          
+
+      - name: Compile Java 11
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java 11
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: runTests
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Setup Java 16
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: 16
+
+      - name: Clean for next Java
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: clean
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Compile Java 16
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java 16
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: runTests
+          build-root-directory: ./${{ matrix.library }}/runtimes/java     
+
+      - name: Setup Java 17
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'corretto'
+          java-version: 17
+
+      - name: Clean for next Java
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: clean
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Compile Java 17
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: build
+          build-root-directory: ./${{ matrix.library }}/runtimes/java
+
+      - name: Test Java 17
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: runTests
+          build-root-directory: ./${{ matrix.library }}/runtimes/java