From a6ccaf78a722b77a417ebec4edce105b51f5cdd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Fri, 12 Jul 2024 12:05:18 -0700 Subject: [PATCH 01/11] chore: bump dafny verification to 4.7.0 (#666) --- .github/workflows/daily_ci.yml | 2 +- .github/workflows/pull.yml | 2 +- .github/workflows/push.yml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/daily_ci.yml b/.github/workflows/daily_ci.yml index 7b1b83047..3824b6cef 100644 --- a/.github/workflows/daily_ci.yml +++ b/.github/workflows/daily_ci.yml @@ -17,7 +17,7 @@ jobs: if: github.event_name != 'schedule' || github.repository_owner == 'aws' uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.2.0' + dafny: '4.7.0' # daily-ci-java: # if: github.event_name != 'schedule' || github.repository_owner == 'aws' # uses: ./.github/workflows/library_java_tests.yml diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index ad9a6d9ca..523b5149b 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -12,7 +12,7 @@ jobs: pr-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.2.0' + dafny: '4.7.0' # pr-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 399783d51..98de8408c 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -14,7 +14,7 @@ jobs: push-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.2.0' + dafny: '4.7.0' # push-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: From 79580208fc3cccdf29bfd3cfa16ee3305bc32c59 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Tue, 16 Jul 2024 12:25:09 -0700 Subject: [PATCH 02/11] chore(MPL): bump MPL to 1.5.1 (#667) --- mpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mpl b/mpl index b6d28dcd6..cdd4885cb 160000 --- a/mpl +++ b/mpl @@ -1 +1 @@ -Subproject commit b6d28dcd6968b00fa200fc0d51a1c83f437191ab +Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d From 99c489dbf0415483764de7817e6f05cf4e1ffad0 Mon Sep 17 00:00:00 2001 From: Rishav karanjit Date: Tue, 30 Jul 2024 09:24:01 -0700 Subject: [PATCH 03/11] chore(CI): Add smithy diff checker gha (#670) --- .github/workflows/smithy-diff.yml | 38 +++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 .github/workflows/smithy-diff.yml diff --git a/.github/workflows/smithy-diff.yml b/.github/workflows/smithy-diff.yml new file mode 100644 index 000000000..b874861c1 --- /dev/null +++ b/.github/workflows/smithy-diff.yml @@ -0,0 +1,38 @@ +# This workflow checks if specfic files were modified, +# if they were they require more than one approval from CODEOWNERS +name: Check Smithy Files + +on: + pull_request: + +jobs: + require-approvals: + runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 + + - name: Get Files changed + id: file-changes + shell: bash + run: + # Checks to see if any of the smithy Models are being updated. + # Doing this check allows us to catch things like, missing @javadoc trait documentation or bug in smithy dafny that has not be resolved. + echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD_REF} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT" + + - name: Check if FILES is not empty + id: comment + env: + PR_NUMBER: ${{ github.event.number }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + FILES: ${{ steps.file-changes.outputs.FILES }} + if: ${{env.FILES != ''}} + run: | + # TODO: If https://github.com/smithy-lang/smithy-dafny/issues/491 is resolved, remove comment about this issue. + COMMENT="@${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?" + COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" + curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" From 8150ee0a04e823f985c5dc5ad0d96a9aa20e6c29 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 20 Aug 2024 15:15:53 -0700 Subject: [PATCH 04/11] fix: Remove --recursive from action to update mpl submodule (#672) Fixes both failures in the nightly build, since it was trying to also update the specification, which wasn't necessary and doesn't update cleanly: https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/10475570505. Also removed --init since that was pointless in this case. --- .github/actions/polymorph_codegen/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index fa68036b1..691f1d09c 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -61,7 +61,7 @@ runs: if: inputs.update-and-regenerate-mpl == 'true' shell: bash run: | - git submodule update --init --recursive --remote --merge mpl + git submodule update --remote --merge mpl - name: Don't regenerate dependencies unless requested id: dependencies From 64067c743ca84b52d5474d0b0595de95aff251f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Thu, 22 Aug 2024 09:39:33 -0700 Subject: [PATCH 05/11] chore(GHA): add dafny interoperability action (#674) --- .github/workflows/dafny_interop.yml | 35 ++ .github/workflows/dafny_interop_test_net.yml | 253 ++++++++++++++ .../dafny_interop_test_vector_net.yml | 308 ++++++++++++++++++ 3 files changed, 596 insertions(+) create mode 100644 .github/workflows/dafny_interop.yml create mode 100644 .github/workflows/dafny_interop_test_net.yml create mode 100644 .github/workflows/dafny_interop_test_vector_net.yml diff --git a/.github/workflows/dafny_interop.yml b/.github/workflows/dafny_interop.yml new file mode 100644 index 000000000..3fa0800c9 --- /dev/null +++ b/.github/workflows/dafny_interop.yml @@ -0,0 +1,35 @@ +# This workflow is for testing backwards compatibility of a dafny version +# and tests if a project that consumes the mpl will be backwards compatible with +# a newer version of Dafny +name: Dafny Interoperability Test + +on: + workflow_dispatch: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, nightly-latest, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL branch/commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, nightly-latest, etc..)" + required: true + type: string + +jobs: + dafny-interop-net: + uses: ./.github/workflows/dafny_interop_test_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + esdk-dafny: ${{inputs.esdk-dafny}} + dafny-interop-net-test-vectors: + uses: ./.github/workflows/dafny_interop_test_vector_net.yml + with: + mpl-dafny: ${{inputs.mpl-dafny}} + mpl-commit: ${{inputs.mpl-commit}} + esdk-dafny: ${{inputs.esdk-dafny}} diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml new file mode 100644 index 000000000..7c4b447a2 --- /dev/null +++ b/.github/workflows/dafny_interop_test_net.yml @@ -0,0 +1,253 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Tests + +on: + workflow_call: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +jobs: + testDotNet: + strategy: + fail-fast: false + matrix: + os: [ + windows-latest, + ubuntu-latest, + macos-12, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + 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@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Test .NET Framework net48 + working-directory: ./AwsEncryptionSDK + if: matrix.os == 'windows-latest' + shell: bash + run: | + make test_net FRAMEWORK=net48 + + - name: Test .NET net6.0 + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + if [ "$RUNNER_OS" == "macOS" ]; then + make test_net_mac_intel FRAMEWORK=net6.0 + else + make test_net FRAMEWORK=net6.0 + fi + + - name: Test Examples on .NET Framework net48 + working-directory: ./AwsEncryptionSDK + if: matrix.os == 'windows-latest' + shell: bash + run: | + dotnet test \ + runtimes/net/Examples \ + --framework net48 + + - name: Test Examples on .NET net6.0 + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + if [ "$RUNNER_OS" == "macOS" ]; then + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" + dotnet test \ + runtimes/net/Examples \ + --framework net6.0 + else + dotnet test \ + runtimes/net/Examples \ + --framework net6.0 + fi + + - name: Unzip ESDK-NET @ v4.0.0 Valid Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors + mkdir -p $NET_400_VALID_VECTORS + DOWNLOAD_NAME=valid-Net-4.0.0.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_400_VALID_VECTORS + + - name: Run ESDK-NET @ v4.0.0 Valid Vectors expect success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \ + dotnet test --framework net48 + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + + - name: Unzip ESDK-NET @ v4.0.0 Invalid Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + mkdir -p $NET_400_INVALID_VECTORS + DOWNLOAD_NAME=invalid-Net-4.0.0.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_400_INVALID_VECTORS + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 48 expect failure + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net48 + # Dotnet test returns 1 for failure. + TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi; + # We want this to fail, so if it returned 1, step passes, else it fails + # TODO Post-#619: Refactor Test Vectors to expect failure, + # as I doubt this true false logic works + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 6.0 expect failure + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + continue-on-error: true + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + if [ "$RUNNER_OS" == "macOS" ]; then + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 + else + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 + fi + # Dotnet test returns 1 for failure. + TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi; + # We want this to fail, so if it returned 1, step passes, else it fails + # TODO Post-#619: Refactor Test Vectors to expect failure, + # as I doubt this true false logic works + + - name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET expect Success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + shell: bash + run: | + NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net48 --logger "console;verbosity=quiet" + if [ "$RUNNER_OS" == "macOS" ]; then + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + else + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + fi + + - name: Unzip ESDK-NET @ v4.0.1 Vectors + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources + shell: bash + run: | + NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors + mkdir -p $NET_401_VECTORS + DOWNLOAD_NAME=v4-Net-4.0.1.zip + unzip -o -qq $DOWNLOAD_NAME -d $NET_401_VECTORS + + - name: Run ESDK-NET @ v4.0.1 Vectors expect success + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + shell: bash + run: | + NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors + # We expect net48 to run only for Windows + if [ "$RUNNER_OS" == "Windows" ]; then + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net48 + fi + if [ "$RUNNER_OS" == "macOS" ]; then + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + else + ESDK_NET_V400_POLICY="forbid" \ + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \ + dotnet test --framework net6.0 --logger "console;verbosity=quiet" + fi diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml new file mode 100644 index 000000000..7343e363d --- /dev/null +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -0,0 +1,308 @@ +# This workflow performs tests in DotNet with MPL nightly latest. +name: Library DotNet Backwards Interop Test Vectors + +on: + workflow_call: + inputs: + mpl-dafny: + description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + mpl-commit: + description: "The MPL commit to use" + required: false + default: "main" + type: string + esdk-dafny: + description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" + required: true + type: string + +env: + # Used in examples + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID: arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID_2: arn:aws:kms:eu-central-1:658956600833:key/75414c93-5285-4b57-99c9-30c1cf0a22c2 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID: arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID_2: arn:aws:kms:eu-west-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_US_EAST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_EU_WEST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + # 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: + decrypt_python_vectors: + strategy: + matrix: + os: [ + windows-latest, + ubuntu-latest, + macos-12, + ] + runs-on: ${{matrix.os}} + permissions: + id-token: write + contents: read + env: + 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@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Fetch Python 2.3.0 Test Vectors + working-directory: ./ + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + mkdir -p $PYTHON_23_VECTOR_PATH + DOWNLOAD_NAME=python23.zip + curl --no-progress-meter --output $DOWNLOAD_NAME --location $VECTORS_URL + unzip -o -qq $DOWNLOAD_NAME -d $PYTHON_23_VECTOR_PATH + rm $DOWNLOAD_NAME + + - name: Decrypt Python 2.3.0 Test Vectors on .net48 (Windows ONLY) + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + if: matrix.os == 'windows-latest' + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + dotnet test --framework net48 + + - name: Decrypt Python 2.3.0 Test Vectors on .net6.0 + working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors + if: matrix.os != 'windows-latest' + shell: bash + run: | + PYTHON_23_VECTOR_PATH=$GITHUB_WORKSPACE/python23/vectors + if [ "$RUNNER_OS" == "macOS" ]; then + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + DYLD_LIBRARY_PATH="/usr/local/opt/openssl@1.1/lib" \ + dotnet test --framework net6.0 + else + DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$PYTHON_23_VECTOR_PATH/manifest.json" \ + dotnet test --framework net6.0 + fi + + generate_vectors: + strategy: + matrix: + os: [ + ubuntu-latest, + macos-12, + ] + runs-on: ${{ matrix.os }} + permissions: + id-token: write + contents: read + env: + 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@v3 + with: + submodules: recursive + fetch-depth: 0 + + - name: Setup .NET Core SDK 6 + uses: actions/setup-dotnet@v3 + with: + dotnet-version: '6.0.x' + + - name: Setup MPL Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.mpl-dafny }} + + - name: Update MPL submodule + working-directory: submodules/MaterialProviders + run: | + git fetch + git checkout ${{inputs.mpl-commit}} + git pull + git submodule update --init --recursive + git rev-parse HEAD + + - name: Download Dependencies + working-directory: AwsEncryptionSDK + run: make setup_net + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + with: + aws-region: us-west-2 + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 + role-session-name: DDBEC-Dafny-Net-Tests + + - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} + shell: bash + working-directory: mpl + run: | + make setup_net + # This works because `node` is installed by default on GHA runners + CORES=$(node -e 'console.log(os.cpus().length)') + make transpile_net CORES=$CORES + + - name: Setup ESDK Dafny + uses: dafny-lang/setup-dafny-action@v1.7.2 + with: + dafny-version: ${{ inputs.esdk-dafny}} + + - name: Build ESDK implementation + shell: bash + working-directory: AwsEncryptionSDK + run: | + # This works because `node` is installed by default on GHA runners + make transpile_implementation_net + make transpile_test_net + + - name: Generate Test Vectors with .NET Framework net6.0 + # TODO Post-#619: Fix Zip file creation on Windows + if: matrix.os != 'windows-latest' + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + mkdir -p $NET_41_VECTOR_PATH + GEN_PATH=runtimes/net/TestVectorsNative/TestVectorGenerator + dotnet run --project $GEN_PATH --framework net6.0 -- \ + --encrypt-manifest $GEN_PATH/resources/0006-awses-message-decryption-generation.v2.json \ + --output-dir $NET_41_VECTOR_PATH + + - name: Zip the Generated Test Vectors for ESDK-JS on Mac/Linux + if: matrix.os != 'windows-latest' + working-directory: ./AwsEncryptionSDK + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + cd $NET_41_VECTOR_PATH + zip -qq net41.zip -r . + + - name: Upload Zip File + uses: actions/upload-artifact@v4 + if: matrix.os != 'windows-latest' + with: + name: ${{matrix.os}}_vector_artifact + path: AwsEncryptionSDK/net41/vectors/*.zip + + decrypt_net_vectors_with_js: + needs: generate_vectors + strategy: + matrix: + os: [ + ubuntu-latest, + macos-12, + ] + 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@v2 + - name: Init Submodules + shell: bash + run: | + git submodule update --init libraries + git submodule update --init --recursive mpl + git submodule update --init smithy-dafny + + - name: Configure AWS Credentials + uses: aws-actions/configure-aws-credentials@v4 + 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 + + - name: Set up Dirs + working-directory: ./AwsEncryptionSDK + run: | + NET_41_VECTOR_PATH=AwsEncryptionSDK/net41/vectors + mkdir -p $NET_41_VECTOR_PATH + + - name: Download Encrypt Manifest Artifact + uses: actions/download-artifact@v4 + with: + name: ${{matrix.os}}_vector_artifact + path: AwsEncryptionSDK/net41/vectors + + - uses: actions/setup-node@v4 + with: + node-version: 17 + + - name: Install deps + run: | + openssl version + npm install @aws-crypto/integration-node + npm install fast-xml-parser + + - name: Decrypt Generated Test Vectors with ESDK-JS + working-directory: ./AwsEncryptionSDK + # TODO Post-#619: Fix Zip file creation on Windows + shell: bash + run: | + NET_41_VECTOR_PATH=net41/vectors + cd $NET_41_VECTOR_PATH + npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 \ No newline at end of file From 959d22e46fad266f69bca7f9c59fddb7d9ada7b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 14:07:24 -0700 Subject: [PATCH 06/11] chore: update mpl submodule name gha (#675) --- .github/workflows/dafny_interop_test_net.yml | 2 +- .github/workflows/dafny_interop_test_vector_net.yml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 7c4b447a2..54c4db81b 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -55,7 +55,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 7343e363d..3e403b60d 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -65,7 +65,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} @@ -175,7 +175,7 @@ jobs: dafny-version: ${{ inputs.mpl-dafny }} - name: Update MPL submodule - working-directory: submodules/MaterialProviders + working-directory: mpl run: | git fetch git checkout ${{inputs.mpl-commit}} @@ -305,4 +305,4 @@ jobs: run: | NET_41_VECTOR_PATH=net41/vectors cd $NET_41_VECTOR_PATH - npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 \ No newline at end of file + npx -y @aws-crypto/integration-node decrypt -v net41.zip -c cpu -f 100 From 4f0359508ad1f181337191df995e5dfe0010b0e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 14:45:18 -0700 Subject: [PATCH 07/11] chore: fix permissions and add env vars (#676) Co-authored-by: Lucas McDonald --- .github/workflows/dafny_interop_test_net.yml | 15 +++++++++++++-- .../workflows/dafny_interop_test_vector_net.yml | 4 ++-- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 54c4db81b..5027b630e 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -18,6 +18,17 @@ on: required: true type: string +env: + # Used in examples + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID: arn:aws:kms:us-west-2:658956600833:key/b3537ef1-d8dc-4780-9f5a-55776cbb2f7f + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_KEY_ID_2: arn:aws:kms:eu-central-1:658956600833:key/75414c93-5285-4b57-99c9-30c1cf0a22c2 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID: arn:aws:kms:us-east-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_KMS_MRK_KEY_ID_2: arn:aws:kms:eu-west-1:658956600833:key/mrk-80bd8ecdcd4342aebd84b7dc9da498a7 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_US_EAST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + AWS_ENCRYPTION_SDK_EXAMPLE_LIMITED_ROLE_ARN_EU_WEST_1: arn:aws:iam::370957321024:role/GitHub-CI-ESDK-Dafny-Role-us-west-2 + # 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: testDotNet: strategy: @@ -71,8 +82,8 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index 3e403b60d..d8fb938ae 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -81,8 +81,8 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash From 25c36259253db6a79682587c582ea4761209b21e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Mon, 26 Aug 2024 16:18:11 -0700 Subject: [PATCH 08/11] chore: use correct dirs in gha (#677) --- .github/workflows/dafny_interop_test_net.yml | 4 ++-- .github/workflows/dafny_interop_test_vector_net.yml | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml index 5027b630e..fd56e893e 100644 --- a/.github/workflows/dafny_interop_test_net.yml +++ b/.github/workflows/dafny_interop_test_net.yml @@ -87,7 +87,7 @@ jobs: - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners @@ -101,7 +101,7 @@ jobs: - name: Build ESDK implementation shell: bash - working-directory: AwsEncryptionSDK + working-directory: ./AwsEncryptionSDK run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml index d8fb938ae..2940a1a67 100644 --- a/.github/workflows/dafny_interop_test_vector_net.yml +++ b/.github/workflows/dafny_interop_test_vector_net.yml @@ -86,7 +86,7 @@ jobs: - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners @@ -100,7 +100,7 @@ jobs: - name: Build ESDK implementation shell: bash - working-directory: AwsEncryptionSDK + working-directory: ./AwsEncryptionSDK run: | # This works because `node` is installed by default on GHA runners make transpile_implementation_net @@ -191,12 +191,12 @@ jobs: uses: aws-actions/configure-aws-credentials@v4 with: aws-region: us-west-2 - role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2 - role-session-name: DDBEC-Dafny-Net-Tests + role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 + role-session-name: NetTests - name: Compile MPL with Dafny ${{inputs.mpl-dafny}} shell: bash - working-directory: mpl + working-directory: mpl/TestVectorsAwsCryptographicMaterialProviders run: | make setup_net # This works because `node` is installed by default on GHA runners From 1839c533a2e3bb57d6c860981bec2642d69c3b3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Thu, 29 Aug 2024 11:51:17 -0700 Subject: [PATCH 09/11] chore: add check only keyword action (#679) --- .github/workflows/check_only_keyword.yml | 40 ++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 .github/workflows/check_only_keyword.yml diff --git a/.github/workflows/check_only_keyword.yml b/.github/workflows/check_only_keyword.yml new file mode 100644 index 000000000..94e2fe95a --- /dev/null +++ b/.github/workflows/check_only_keyword.yml @@ -0,0 +1,40 @@ +# This workflow checks if you are checking in dafny code +# with the keyword {:only}, it adds a message to the pull +# request to remind you to remove it. +name: Check {:only} decorator presence + +on: + pull_request: + +jobs: + grep-only-verification-keyword: + runs-on: ubuntu-latest + permissions: + issues: write + pull-requests: write + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 + + - name: Check only keyword + id: only-keyword + shell: bash + run: + # checking in code with the dafny decorator {:only} + # will not verify the entire file or maybe the entire project depending on its configuration + # This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are. + echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT" + + - name: Check if ONLY_KEYWORD is not empty + id: comment + env: + PR_NUMBER: ${{ github.event.number }} + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }} + if: ${{env.ONLY_KEYWORD != ''}} + run: | + COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?" + COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" + curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" + exit 1 From 68e75fb10084cf94dc8ccbedf7a98a3c6569dd3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Corella?= <39066999+josecorella@users.noreply.github.com> Date: Fri, 20 Sep 2024 15:39:04 -0700 Subject: [PATCH 10/11] chore: regen code for 4.8.0 and bump mpl (#681) --- .../action.yml | 21 ++++ .github/actions/polymorph_codegen/action.yml | 26 ++--- .github/workflows/library_codegen.yml | 11 ++- .github/workflows/pull.yml | 8 +- .github/workflows/push.yml | 8 +- .github/workflows/smithy-diff.yml | 11 ++- .../AwsEncryptionSdk/dotnet/dafny-4.8.0.patch | 96 +++++++++++++++++++ .../dafny/AwsEncryptionSdk/Model/esdk.smithy | 3 - AwsEncryptionSDK/project.properties | 3 +- AwsEncryptionSDK/runtimes/net/ESDK.csproj | 2 +- SharedMakefileV2.mk | 7 ++ mpl | 2 +- smithy-dafny | 2 +- 13 files changed, 168 insertions(+), 32 deletions(-) create mode 100644 .github/actions/install_smithy_dafny_codegen_dependencies/action.yml create mode 100644 AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch diff --git a/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml new file mode 100644 index 000000000..da00a4c70 --- /dev/null +++ b/.github/actions/install_smithy_dafny_codegen_dependencies/action.yml @@ -0,0 +1,21 @@ +# +# This local action sets up code dependencies +# to run Smithy-Dafny CI in GitHub Actions workflows. +# + +name: "Install Smithy-Dafny codegen dependencies" +description: "Install Java package dependencies required to run Smithy-Dafny codegen" +runs: + using: "composite" + steps: + - name: Install smithy-dafny-codegen Rust dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML + build-root-directory: smithy-dafny/smithy-dafny-codegen-modules/smithy-rs + + - name: Install smithy-dafny-codegen Python dependencies locally + uses: gradle/gradle-build-action@v2 + with: + arguments: :smithy-python-codegen:pTML + build-root-directory: smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen diff --git a/.github/actions/polymorph_codegen/action.yml b/.github/actions/polymorph_codegen/action.yml index 691f1d09c..7f6b4f29b 100644 --- a/.github/actions/polymorph_codegen/action.yml +++ b/.github/actions/polymorph_codegen/action.yml @@ -88,18 +88,20 @@ runs: make -C mpl/AwsCryptographicMaterialProviders setup_prettier make -C mpl/ComAmazonawsKms setup_prettier make -C mpl/ComAmazonawsDynamodb setup_prettier - - - name: Regenerate Java code using smithy-dafny - # npx seems to be unavailable on Windows GHA runners, - # so we don't regenerate Java code on them either. - if: runner.os != 'Windows' - working-directory: ./${{ inputs.library }} - shell: bash - # smithy-dafny also formats generated code itself now, - # so prettier is a necessary dependency. - run: | - make setup_prettier - make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} + + # In the ESDK Dafny it does not make sense to run smithy dafny for java code + # since the java esdk written natively and not through dafny + #- name: Regenerate Java code using smithy-dafny + # # npx seems to be unavailable on Windows GHA runners, + # # so we don't regenerate Java code on them either. + # if: runner.os != 'Windows' + # working-directory: ./${{ inputs.library }} + # shell: bash + # # smithy-dafny also formats generated code itself now, + # # so prettier is a necessary dependency. + # run: | + # make setup_prettier + # make polymorph_java ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }} - name: Regenerate .NET code using smithy-dafny working-directory: ./${{ inputs.library }} diff --git a/.github/workflows/library_codegen.yml b/.github/workflows/library_codegen.yml index 9780c1348..e11e71685 100644 --- a/.github/workflows/library_codegen.yml +++ b/.github/workflows/library_codegen.yml @@ -38,7 +38,7 @@ jobs: # it to verify the Dafny code. Instead we manually pull the submodules we DO need. - run: git submodule update --init libraries - run: git submodule update --init --recursive mpl - - run: git submodule update --init smithy-dafny + - run: git submodule update --init --recursive smithy-dafny # Only used to format generated code # and to translate version strings such as "nightly-latest" @@ -53,6 +53,15 @@ jobs: with: dotnet-version: ${{ matrix.dotnet-version }} + - 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 + - uses: ./.github/actions/polymorph_codegen with: dafny: ${{ env.DAFNY_VERSION }} diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml index 523b5149b..655eea31c 100644 --- a/.github/workflows/pull.yml +++ b/.github/workflows/pull.yml @@ -8,11 +8,11 @@ jobs: pr-ci-codegen: uses: ./.github/workflows/library_codegen.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.7.0' + dafny: '4.8.0' # pr-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: @@ -20,8 +20,8 @@ jobs: pr-ci-net: uses: ./.github/workflows/library_net_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index 98de8408c..0df538b37 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -10,11 +10,11 @@ jobs: pr-ci-codegen: uses: ./.github/workflows/library_codegen.yml with: - dafny: '4.2.0' + dafny: '4.8.0' push-ci-verification: uses: ./.github/workflows/library_dafny_verification.yml with: - dafny: '4.7.0' + dafny: '4.8.0' # push-ci-java: # uses: ./.github/workflows/library_java_tests.yml # with: @@ -22,8 +22,8 @@ jobs: push-ci-net: uses: ./.github/workflows/library_net_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' pr-test-vectors: uses: ./.github/workflows/library_interop_tests.yml with: - dafny: '4.2.0' + dafny: '4.8.0' diff --git a/.github/workflows/smithy-diff.yml b/.github/workflows/smithy-diff.yml index b874861c1..3092c9470 100644 --- a/.github/workflows/smithy-diff.yml +++ b/.github/workflows/smithy-diff.yml @@ -3,7 +3,8 @@ name: Check Smithy Files on: - pull_request: + pull_request_review: + types: [submitted] jobs: require-approvals: @@ -19,20 +20,22 @@ jobs: - name: Get Files changed id: file-changes shell: bash + env: + GITHUB_HEAD: ${{github.event.pull_request.head.ref}} run: # Checks to see if any of the smithy Models are being updated. # Doing this check allows us to catch things like, missing @javadoc trait documentation or bug in smithy dafny that has not be resolved. - echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD_REF} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT" + echo "FILES=$(git diff --name-only origin/main origin/${GITHUB_HEAD} | grep '\.smithy$' | tr '\n' ' ')" >> "$GITHUB_OUTPUT" - name: Check if FILES is not empty id: comment env: - PR_NUMBER: ${{ github.event.number }} + PR_NUMBER: ${{ github.event.pull_request.number }} GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} FILES: ${{ steps.file-changes.outputs.FILES }} if: ${{env.FILES != ''}} run: | # TODO: If https://github.com/smithy-lang/smithy-dafny/issues/491 is resolved, remove comment about this issue. - COMMENT="@${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?" + COMMENT="@${{github.event.pull_request.user.login}} and @${{github.actor}}, I noticed you are updating the smithy model files.\nDoes this update need new or updated javadoc trait documentation?\n Are you adding constraints inside list, map or union? Do you know about this issue: https://github.com/smithy-lang/smithy-dafny/issues/491?" COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments" curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}" diff --git a/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch new file mode 100644 index 000000000..9f2382998 --- /dev/null +++ b/AwsEncryptionSDK/codegen-patches/AwsEncryptionSdk/dotnet/dafny-4.8.0.patch @@ -0,0 +1,96 @@ +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +index 1dc37f40..e2187b21 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/AwsEncryptionSdkConfig.cs +@@ -28,7 +28,7 @@ namespace AWS.Cryptography.EncryptionSDK + { + return this._maxEncryptedDataKeys.HasValue; + } +- public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4__0__0__RetryPolicy ++ public AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy NetV4_0_0_RetryPolicy + { + get { return this._netV4_0_0_RetryPolicy; } + set { this._netV4_0_0_RetryPolicy = value; } +diff --git b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +index cb1b30bb..dc6e24f9 100644 +--- b/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs ++++ a/AwsEncryptionSDK/runtimes/net/Generated/AwsEncryptionSdk/TypeConversion.cs +@@ -7,22 +7,22 @@ namespace AWS.Cryptography.EncryptionSDK + { + public static class TypeConversion + { +- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z"; +- +- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z"; +- + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig value) + { + software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig concrete = (software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig)value; AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig converted = new AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig(); if (concrete._commitmentPolicy.is_Some) converted.CommitmentPolicy = (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(concrete._commitmentPolicy); + if (concrete._maxEncryptedDataKeys.is_Some) converted.MaxEncryptedDataKeys = (long)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(concrete._maxEncryptedDataKeys); +- if (concrete._netV4_0_0_RetryPolicy.is_Some) converted.NetV4__0__0__RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4_0_0_RetryPolicy); return converted; ++ // BEGIN MANUAL EDIT ++ if (concrete._netV4__0__0__RetryPolicy.is_Some) converted.NetV4_0_0_RetryPolicy = (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(concrete._netV4__0__0__RetryPolicy); return converted; ++ // END MANUAL EDIT + } + public static software.amazon.cryptography.encryptionsdk.internaldafny.types._IAwsEncryptionSdkConfig ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig(AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkConfig value) + { + value.Validate(); + AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy var_commitmentPolicy = value.IsSetCommitmentPolicy() ? value.CommitmentPolicy : (AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy)null; + long? var_maxEncryptedDataKeys = value.IsSetMaxEncryptedDataKeys() ? value.MaxEncryptedDataKeys : (long?)null; +- AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4__0__0__RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // BEGIN MANUAL EDIT ++ AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy var_netV4_0_0_RetryPolicy = value.IsSetNetV4__0__0__RetryPolicy() ? value.NetV4_0_0_RetryPolicy : (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null; ++ // END MANUAL EDIT + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.AwsEncryptionSdkConfig(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(var_commitmentPolicy), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M20_maxEncryptedDataKeys(var_maxEncryptedDataKeys), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(var_netV4_0_0_RetryPolicy)); + } + public static AWS.Cryptography.EncryptionSDK.AwsEncryptionSdkException FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException(software.amazon.cryptography.encryptionsdk.internaldafny.types.Error_AwsEncryptionSdkException value) +@@ -96,16 +96,22 @@ namespace AWS.Cryptography.EncryptionSDK + + return new software.amazon.cryptography.encryptionsdk.internaldafny.types.EncryptOutput(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M10_ciphertext(value.Ciphertext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M17_encryptionContext(value.EncryptionContext), ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S13_EncryptOutput__M16_algorithmSuiteId(value.AlgorithmSuiteId)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy value) ++ // END MANUAL EDIT + { + if (value.is_FORBID__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY; + if (value.is_ALLOW__RETRY) return AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY; + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } +- public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4_0_0_RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static software.amazon.cryptography.encryptionsdk.internaldafny.types._INetV4__0__0__RetryPolicy ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_FORBID__RETRY(); +- if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4_0_0_RetryPolicy.create_ALLOW__RETRY(); ++ // BEGIN MANUAL EDIT ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.FORBID_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_FORBID__RETRY(); ++ if (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy.ALLOW_RETRY.Equals(value)) return software.amazon.cryptography.encryptionsdk.internaldafny.types.NetV4__0__0__RetryPolicy.create_ALLOW__RETRY(); ++ // END MANUAL EDIT + throw new System.ArgumentException("Invalid AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value"); + } + public static AWS.Cryptography.MaterialProviders.ESDKCommitmentPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M16_commitmentPolicy(Wrappers_Compile._IOption value) +@@ -124,13 +130,19 @@ namespace AWS.Cryptography.EncryptionSDK + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S15_CountingNumbers((long)value)); + } +- public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // BEGIN MANUAL EDIT ++ public static AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(Wrappers_Compile._IOption value) ++ // END MANUAL EDIT + { + return value.is_None ? (AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)null : FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy(value.Extract()); + } +- public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // BEGIN MANUAL EDIT ++ public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S22_AwsEncryptionSdkConfig__M21_netV4_0_0_RetryPolicy(AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy value) ++ // END MANUAL EDIT + { +- return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // BEGIN MANUAL EDIT ++ return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S21_NetV4_0_0_RetryPolicy((AWS.Cryptography.EncryptionSDK.NetV4_0_0_RetryPolicy)value)); ++ // END MANUAL EDIT + } + public static string FromDafny_N3_aws__N12_cryptography__N13_encryptionSdk__S25_AwsEncryptionSdkException__M7_message(Dafny.ISequence value) + { diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy index ba12c4325..d184d5545 100644 --- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy +++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/Model/esdk.smithy @@ -3,7 +3,6 @@ namespace aws.cryptography.encryptionSdk use aws.cryptography.primitives#AwsCryptographicPrimitives use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders -///////////// // ESDK Client Creation // TODO add a trait to indicate that 'Client' should not be appended to this name, @@ -56,7 +55,6 @@ structure AwsEncryptionSdkConfig { string NetV4_0_0_RetryPolicy -///////////// // ESDK Operations operation Encrypt { @@ -127,7 +125,6 @@ structure DecryptOutput { // the message format and message header in Smithy. } -///////////// // Errors @error("client") diff --git a/AwsEncryptionSDK/project.properties b/AwsEncryptionSDK/project.properties index dd7eb37b9..02e193a7d 100644 --- a/AwsEncryptionSDK/project.properties +++ b/AwsEncryptionSDK/project.properties @@ -1,3 +1,4 @@ # This file stores the top level dafny version information. # All elements of the project need to agree on this version. -dafnyVersion=4.2.0 +dafnyVersion=4.8.0 +dafnyRuntimeJavaVersion=4.8.0 diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj index 71d8aa95b..c2abb450e 100644 --- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj +++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj @@ -31,7 +31,7 @@ - +