Skip to content

Commit 45a2b63

Browse files
kessplaskessplas
authored
Merge branch 'main' into update-names
2 parents 68b1f53 + b9333fb commit 45a2b63

File tree

94 files changed

+1832
-345
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

94 files changed

+1832
-345
lines changed

‎.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
#
2+
# This local action sets up code dependencies
3+
# to run Smithy-Dafny CI in GitHub Actions workflows.
4+
#
5+
6+
name: "Install Smithy-Dafny codegen dependencies"
7+
description: "Install Java package dependencies required to run Smithy-Dafny codegen"
8+
runs:
9+
using: "composite"
10+
steps:
11+
- name: Install smithy-dafny-codegen Rust dependencies locally
12+
uses: gradle/gradle-build-action@v2
13+
with:
14+
arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
15+
build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
16+
17+
- name: Install smithy-dafny-codegen Python dependencies locally
18+
uses: gradle/gradle-build-action@v2
19+
with:
20+
arguments: :smithy-python-codegen:pTML
21+
build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen

‎.github/actions/polymorph_codegen/action.yml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,11 @@ runs:
9797
run: |
9898
echo "PROJECT_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'PROJECT_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT
9999
100+
- name: Print dotnet version
101+
shell: bash
102+
run: |
103+
dotnet --version
104+
100105
- name: Regenerate Dafny code using smithy-dafny
101106
# Unfortunately Dafny codegen doesn't work on Windows:
102107
# https://github.com/smithy-lang/smithy-dafny/issues/317

‎.github/workflows/check_only_key_word.yml

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# This workflow checks if you are checking in dafny code
2+
# with the keyword {:only}, it adds a message to the pull
3+
# request to remind you to remove it.
4+
name: Check {:only} decorator presence
5+
6+
on:
7+
pull_request:
8+
9+
jobs:
10+
grep-only-verification-keyword:
11+
runs-on: ubuntu-latest
12+
permissions:
13+
issues: write
14+
pull-requests: write
15+
steps:
16+
- uses: actions/checkout@v3
17+
with:
18+
fetch-depth: 0
19+
20+
- name: Check only keyword
21+
id: only-keyword
22+
shell: bash
23+
run:
24+
# checking in code with the dafny decorator {:only}
25+
# will not verify the entire file or maybe the entire project depending on its configuration
26+
# This action checks if you are either adding or removing the {:only} decorator and posting on the pr if you are.
27+
echo "ONLY_KEYWORD=$(git diff origin/main origin/${GITHUB_HEAD_REF} **/*.dfy | grep -i {:only})" >> "$GITHUB_OUTPUT"
28+
29+
- name: Check if ONLY_KEYWORD is not empty
30+
id: comment
31+
env:
32+
PR_NUMBER: ${{ github.event.number }}
33+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
34+
ONLY_KEYWORD: ${{ steps.only-keyword.outputs.ONLY_KEYWORD }}
35+
if: ${{env.ONLY_KEYWORD != ''}}
36+
run: |
37+
COMMENT="It looks like you are adding or removing the dafny keyword {:only}.\nIs this intended?"
38+
COMMENT_URL="https://api.github.com/repos/${{ github.repository }}/issues/${PR_NUMBER}/comments"
39+
curl -s -H "Authorization: token ${GITHUB_TOKEN}" -X POST $COMMENT_URL -d "{\"body\":\"$COMMENT\"}"
40+
exit 1

‎.github/workflows/ci_codegen.yml

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,13 @@ jobs:
3333
- uses: actions/checkout@v3
3434
with:
3535
submodules: recursive
36+
- run: git submodule update --init --recursive submodules/smithy-dafny
3637

3738
# Only used to format generated code
3839
# and to translate version strings such as "nightly-latest"
3940
# to an actual DAFNY_VERSION.
4041
- name: Setup Dafny
41-
uses: dafny-lang/setup-dafny-action@v1.7.2
42+
uses: dafny-lang/setup-dafny-action@v1.8.0
4243
with:
4344
dafny-version: ${{ inputs.dafny }}
4445

@@ -47,8 +48,20 @@ jobs:
4748
with:
4849
dotnet-version: ${{ matrix.dotnet-version }}
4950

51+
- name: Create temporary global.json
52+
run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
53+
54+
- name: Setup Java 17 for codegen
55+
uses: actions/setup-java@v3
56+
with:
57+
distribution: "corretto"
58+
java-version: "17"
59+
60+
- name: Install Smithy-Dafny codegen dependencies
61+
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
62+
5063
- uses: ./.github/actions/polymorph_codegen
5164
with:
52-
dafny: ${{ env.DAFNY_VERSION }}
65+
dafny: ${{ inputs.dafny }}
5366
library: ${{ matrix.library }}
5467
diff-generated-code: true

‎.github/workflows/ci_examples_java.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ jobs:
5353
java-version: ${{ matrix.java-version }}
5454

5555
- name: Setup Dafny
56-
uses: dafny-lang/setup-dafny-action@v1.7.2
56+
uses: dafny-lang/setup-dafny-action@v1.8.0
5757
with:
5858
dafny-version: ${{ inputs.dafny }}
5959

‎.github/workflows/ci_examples_net.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ jobs:
4646
dotnet-version: ${{ matrix.dotnet-version }}
4747

4848
- name: Setup Dafny
49-
uses: dafny-lang/setup-dafny-action@v1.7.2
49+
uses: dafny-lang/setup-dafny-action@v1.8.0
5050
with:
5151
dafny-version: ${{ inputs.dafny }}
5252

‎.github/workflows/ci_test_java.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
submodules: recursive
4848

4949
- name: Setup Dafny
50-
uses: dafny-lang/setup-dafny-action@v1.7.2
50+
uses: dafny-lang/setup-dafny-action@v1.8.0
5151
with:
5252
dafny-version: ${{ inputs.dafny }}
5353

‎.github/workflows/ci_test_net.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
dotnet-version: ${{ matrix.dotnet-version }}
4848

4949
- name: Setup Dafny
50-
uses: dafny-lang/setup-dafny-action@v1.7.2
50+
uses: dafny-lang/setup-dafny-action@v1.8.0
5151
with:
5252
dafny-version: ${{ inputs.dafny }}
5353

‎.github/workflows/ci_test_vector_java.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ jobs:
5656
submodules: recursive
5757

5858
- name: Setup Dafny
59-
uses: dafny-lang/setup-dafny-action@v1.7.2
59+
uses: dafny-lang/setup-dafny-action@v1.8.0
6060
with:
6161
dafny-version: ${{ inputs.dafny }}
6262

‎.github/workflows/ci_test_vector_net.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ jobs:
5252
submodules: recursive
5353

5454
- name: Setup Dafny
55-
uses: dafny-lang/setup-dafny-action@v1.7.2
55+
uses: dafny-lang/setup-dafny-action@v1.8.0
5656
with:
5757
dafny-version: ${{ inputs.dafny }}
5858

‎.github/workflows/dafny-interop.yml

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
# This workflow is for testing backwards compatibility of a dafny version
2+
# and tests if a project that consumes the mpl will be backwards compatible with
3+
# a newer version of Dafny
4+
name: Dafny Interoperability Test
5+
6+
on:
7+
workflow_dispatch:
8+
inputs:
9+
mpl-dafny:
10+
description: "The Dafny version to compile the MPL with (4.2.0, nightly-latest, etc..)"
11+
required: true
12+
type: string
13+
mpl-commit:
14+
description: "The MPL branch/commit to use"
15+
required: false
16+
default: "main"
17+
type: string
18+
dbesdk-dafny:
19+
description: "The Dafny version to compile the DBESDK with (4.2.0, nightly-latest, etc..)"
20+
required: true
21+
type: string
22+
23+
jobs:
24+
getMplHeadVersion:
25+
uses: ./.github/workflows/mpl_head_version.yml
26+
with:
27+
mpl-head: ${{inputs.mpl-commit}}
28+
dafny-interop-java:
29+
needs: getMplHeadVersion
30+
uses: ./.github/workflows/dafny_interop_java.yml
31+
with:
32+
mpl-dafny: ${{inputs.mpl-dafny}}
33+
mpl-commit: ${{inputs.mpl-commit}}
34+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
35+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
36+
dafny-interop-java-test-vectors:
37+
needs: getMplHeadVersion
38+
uses: ./.github/workflows/dafny_interop_test_vector_java.yml
39+
with:
40+
mpl-dafny: ${{inputs.mpl-dafny}}
41+
mpl-commit: ${{inputs.mpl-commit}}
42+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
43+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
44+
dafny-interop-java-examples:
45+
needs: getMplHeadVersion
46+
uses: ./.github/workflows/dafny_interop_examples_java.yml
47+
with:
48+
mpl-dafny: ${{inputs.mpl-dafny}}
49+
mpl-commit: ${{inputs.mpl-commit}}
50+
mpl-version: ${{needs.getMplHeadVersion.outputs.version}}
51+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
52+
dafny-interop-net:
53+
uses: ./.github/workflows/dafny_interop_test_net.yml
54+
with:
55+
mpl-dafny: ${{inputs.mpl-dafny}}
56+
mpl-commit: ${{inputs.mpl-commit}}
57+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
58+
dafny-interop-net-test-vectors:
59+
uses: ./.github/workflows/dafny_interop_test_vector_net.yml
60+
with:
61+
mpl-dafny: ${{inputs.mpl-dafny}}
62+
mpl-commit: ${{inputs.mpl-commit}}
63+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}
64+
dafny-interop-net-examples:
65+
uses: ./.github/workflows/dafny_interop_examples_net.yml
66+
with:
67+
mpl-dafny: ${{inputs.mpl-dafny}}
68+
mpl-commit: ${{inputs.mpl-commit}}
69+
dbesdk-dafny: ${{inputs.dbesdk-dafny}}

‎.github/workflows/dafny_interop_examples_java.yml

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
# This workflow performs tests in Java with MPL nightly latest.
2+
name: Library Java Backwards Example Tests
3+
4+
on:
5+
workflow_call:
6+
inputs:
7+
mpl-dafny:
8+
description: "The Dafny version to compile the MPL with (4.2.0, dafny-nightly, etc..)"
9+
required: true
10+
type: string
11+
mpl-commit:
12+
description: "The MPL commit to use"
13+
required: false
14+
default: "main"
15+
type: string
16+
mpl-version:
17+
description: "The MPL version to use"
18+
required: true
19+
type: string
20+
dbesdk-dafny:
21+
description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
22+
required: true
23+
type: string
24+
25+
jobs:
26+
testExamplesJava:
27+
strategy:
28+
max-parallel: 1
29+
matrix:
30+
java-version: [8, 11, 16, 17]
31+
os: [macos-12]
32+
runs-on: ${{ matrix.os }}
33+
permissions:
34+
id-token: write
35+
contents: read
36+
steps:
37+
- name: Configure AWS Credentials
38+
uses: aws-actions/configure-aws-credentials@v4
39+
with:
40+
aws-region: us-west-2
41+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
42+
role-session-name: DDBEC-Dafny-Java-Tests
43+
44+
- uses: actions/checkout@v3
45+
with:
46+
submodules: recursive
47+
fetch-depth: 0
48+
49+
- name: Setup MPL Dafny
50+
uses: dafny-lang/[email protected]
51+
with:
52+
dafny-version: ${{ inputs.mpl-dafny }}
53+
54+
- name: Update MPL submodule
55+
working-directory: submodules/MaterialProviders
56+
run: |
57+
git fetch
58+
git checkout ${{inputs.mpl-commit}}
59+
git pull
60+
git submodule update --init --recursive
61+
git rev-parse HEAD
62+
63+
- name: Setup Java ${{ matrix.java-version }}
64+
uses: actions/setup-java@v4
65+
with:
66+
distribution: "corretto"
67+
java-version: ${{ matrix.java-version }}
68+
69+
- name: Build MPL with Dafny ${{inputs.mpl-dafny}}
70+
working-directory: submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders
71+
run: |
72+
# This works because `node` is installed by default on GHA runners
73+
CORES=$(node -e 'console.log(os.cpus().length)')
74+
make build_java CORES=$CORES
75+
76+
- name: Setup DBESDK Dafny
77+
uses: dafny-lang/[email protected]
78+
with:
79+
dafny-version: ${{ inputs.dbesdk-dafny}}
80+
81+
- name: Update project.properties if using MPL HEAD
82+
run: |
83+
sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
84+
85+
- name: Build implementation
86+
shell: bash
87+
working-directory: ./DynamoDbEncryption
88+
run: |
89+
make transpile_implementation_java
90+
make transpile_test_java
91+
make mvn_local_deploy
92+
93+
- name: Test Examples
94+
working-directory: ./Examples
95+
run: |
96+
# Run simple examples
97+
gradle -p runtimes/java/DynamoDbEncryption test
98+
# Run migration examples
99+
gradle -p runtimes/java/Migration/PlaintextToAWSDBE test
100+
gradle -p runtimes/java/Migration/DDBECToAWSDBE test

0 commit comments

Comments
 (0)