-
Notifications
You must be signed in to change notification settings - Fork 12
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main' into update-names
- Loading branch information
Showing
94 changed files
with
1,832 additions
and
345 deletions.
There are no files selected for viewing
21 changes: 21 additions & 0 deletions
21
.github/actions/install_smithy_dafny_codegen_dependencies/action.yml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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: submodules/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: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| # 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 | ||
| dbesdk-dafny: | ||
| description: "The Dafny version to compile the DBESDK with (4.2.0, nightly-latest, etc..)" | ||
| required: true | ||
| type: string | ||
|
|
||
| jobs: | ||
| getMplHeadVersion: | ||
| uses: ./.github/workflows/mpl_head_version.yml | ||
| with: | ||
| mpl-head: ${{inputs.mpl-commit}} | ||
| dafny-interop-java: | ||
| needs: getMplHeadVersion | ||
| uses: ./.github/workflows/dafny_interop_java.yml | ||
| with: | ||
| mpl-dafny: ${{inputs.mpl-dafny}} | ||
| mpl-commit: ${{inputs.mpl-commit}} | ||
| mpl-version: ${{needs.getMplHeadVersion.outputs.version}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-dafny}} | ||
| dafny-interop-java-test-vectors: | ||
| needs: getMplHeadVersion | ||
| uses: ./.github/workflows/dafny_interop_test_vector_java.yml | ||
| with: | ||
| mpl-dafny: ${{inputs.mpl-dafny}} | ||
| mpl-commit: ${{inputs.mpl-commit}} | ||
| mpl-version: ${{needs.getMplHeadVersion.outputs.version}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-dafny}} | ||
| dafny-interop-java-examples: | ||
| needs: getMplHeadVersion | ||
| uses: ./.github/workflows/dafny_interop_examples_java.yml | ||
| with: | ||
| mpl-dafny: ${{inputs.mpl-dafny}} | ||
| mpl-commit: ${{inputs.mpl-commit}} | ||
| mpl-version: ${{needs.getMplHeadVersion.outputs.version}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-dafny}} | ||
| dafny-interop-net: | ||
| uses: ./.github/workflows/dafny_interop_test_net.yml | ||
| with: | ||
| mpl-dafny: ${{inputs.mpl-dafny}} | ||
| mpl-commit: ${{inputs.mpl-commit}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-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}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-dafny}} | ||
| dafny-interop-net-examples: | ||
| uses: ./.github/workflows/dafny_interop_examples_net.yml | ||
| with: | ||
| mpl-dafny: ${{inputs.mpl-dafny}} | ||
| mpl-commit: ${{inputs.mpl-commit}} | ||
| dbesdk-dafny: ${{inputs.dbesdk-dafny}} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,100 @@ | ||
| # This workflow performs tests in Java with MPL nightly latest. | ||
| name: Library Java Backwards Example 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 | ||
| mpl-version: | ||
| description: "The MPL version to use" | ||
| required: true | ||
| type: string | ||
| dbesdk-dafny: | ||
| description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)" | ||
| required: true | ||
| type: string | ||
|
|
||
| jobs: | ||
| testExamplesJava: | ||
| strategy: | ||
| max-parallel: 1 | ||
| matrix: | ||
| java-version: [8, 11, 16, 17] | ||
| os: [macos-12] | ||
| runs-on: ${{ matrix.os }} | ||
| permissions: | ||
| id-token: write | ||
| contents: read | ||
| steps: | ||
| - 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-Java-Tests | ||
|
|
||
| - uses: actions/checkout@v3 | ||
| with: | ||
| submodules: recursive | ||
| fetch-depth: 0 | ||
|
|
||
| - name: Setup MPL Dafny | ||
| uses: dafny-lang/[email protected] | ||
| 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: Setup Java ${{ matrix.java-version }} | ||
| uses: actions/setup-java@v4 | ||
| with: | ||
| distribution: "corretto" | ||
| java-version: ${{ matrix.java-version }} | ||
|
|
||
| - name: Build MPL with Dafny ${{inputs.mpl-dafny}} | ||
| working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders | ||
| 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 | ||
| - name: Setup DBESDK Dafny | ||
| uses: dafny-lang/[email protected] | ||
| with: | ||
| dafny-version: ${{ inputs.dbesdk-dafny}} | ||
|
|
||
| - name: Update project.properties if using MPL HEAD | ||
| run: | | ||
| sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties | ||
| - name: Build implementation | ||
| shell: bash | ||
| working-directory: ./DynamoDbEncryption | ||
| run: | | ||
| make transpile_implementation_java | ||
| make transpile_test_java | ||
| make mvn_local_deploy | ||
| - name: Test Examples | ||
| working-directory: ./Examples | ||
| run: | | ||
| # Run simple examples | ||
| gradle -p runtimes/java/DynamoDbEncryption test | ||
| # Run migration examples | ||
| gradle -p runtimes/java/Migration/PlaintextToAWSDBE test | ||
| gradle -p runtimes/java/Migration/DDBECToAWSDBE test |
Oops, something went wrong.