Skip to content

Commit 64067c7

Browse files
josecorellajosecorella
authored
chore(GHA): add dafny interoperability action (#674)
1 parent 8150ee0 commit 64067c7

File tree

3 files changed

+596
-0
lines changed

3 files changed

+596
-0
lines changed

‎.github/workflows/dafny_interop.yml

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
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+
esdk-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+
dafny-interop-net:
25+
uses: ./.github/workflows/dafny_interop_test_net.yml
26+
with:
27+
mpl-dafny: ${{inputs.mpl-dafny}}
28+
mpl-commit: ${{inputs.mpl-commit}}
29+
esdk-dafny: ${{inputs.esdk-dafny}}
30+
dafny-interop-net-test-vectors:
31+
uses: ./.github/workflows/dafny_interop_test_vector_net.yml
32+
with:
33+
mpl-dafny: ${{inputs.mpl-dafny}}
34+
mpl-commit: ${{inputs.mpl-commit}}
35+
esdk-dafny: ${{inputs.esdk-dafny}}

‎.github/workflows/dafny_interop_test_net.yml

Lines changed: 253 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,253 @@
1+
# This workflow performs tests in DotNet with MPL nightly latest.
2+
name: Library DotNet Backwards Interop 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+
esdk-dafny:
17+
description: "The Dafny version to compile the DBESDK with (4.2.0, dafny-nightly, etc..)"
18+
required: true
19+
type: string
20+
21+
jobs:
22+
testDotNet:
23+
strategy:
24+
fail-fast: false
25+
matrix:
26+
os: [
27+
windows-latest,
28+
ubuntu-latest,
29+
macos-12,
30+
]
31+
runs-on: ${{ matrix.os }}
32+
permissions:
33+
id-token: write
34+
contents: read
35+
env:
36+
DOTNET_CLI_TELEMETRY_OPTOUT: 1
37+
DOTNET_NOLOGO: 1
38+
steps:
39+
- name: Support longpaths on Git checkout
40+
run: |
41+
git config --global core.longpaths true
42+
- uses: actions/checkout@v3
43+
with:
44+
submodules: recursive
45+
fetch-depth: 0
46+
47+
- name: Setup .NET Core SDK 6
48+
uses: actions/setup-dotnet@v3
49+
with:
50+
dotnet-version: '6.0.x'
51+
52+
- name: Setup MPL Dafny
53+
uses: dafny-lang/[email protected]
54+
with:
55+
dafny-version: ${{ inputs.mpl-dafny }}
56+
57+
- name: Update MPL submodule
58+
working-directory: submodules/MaterialProviders
59+
run: |
60+
git fetch
61+
git checkout ${{inputs.mpl-commit}}
62+
git pull
63+
git submodule update --init --recursive
64+
git rev-parse HEAD
65+
66+
- name: Download Dependencies
67+
working-directory: AwsEncryptionSDK
68+
run: make setup_net
69+
70+
- name: Configure AWS Credentials
71+
uses: aws-actions/configure-aws-credentials@v4
72+
with:
73+
aws-region: us-west-2
74+
role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
75+
role-session-name: DDBEC-Dafny-Net-Tests
76+
77+
- name: Compile MPL with Dafny ${{inputs.mpl-dafny}}
78+
shell: bash
79+
working-directory: mpl
80+
run: |
81+
make setup_net
82+
# This works because `node` is installed by default on GHA runners
83+
CORES=$(node -e 'console.log(os.cpus().length)')
84+
make transpile_net CORES=$CORES
85+
86+
- name: Setup ESDK Dafny
87+
uses: dafny-lang/[email protected]
88+
with:
89+
dafny-version: ${{ inputs.esdk-dafny}}
90+
91+
- name: Build ESDK implementation
92+
shell: bash
93+
working-directory: AwsEncryptionSDK
94+
run: |
95+
# This works because `node` is installed by default on GHA runners
96+
make transpile_implementation_net
97+
make transpile_test_net
98+
99+
- name: Test .NET Framework net48
100+
working-directory: ./AwsEncryptionSDK
101+
if: matrix.os == 'windows-latest'
102+
shell: bash
103+
run: |
104+
make test_net FRAMEWORK=net48
105+
106+
- name: Test .NET net6.0
107+
working-directory: ./AwsEncryptionSDK
108+
shell: bash
109+
run: |
110+
if [ "$RUNNER_OS" == "macOS" ]; then
111+
make test_net_mac_intel FRAMEWORK=net6.0
112+
else
113+
make test_net FRAMEWORK=net6.0
114+
fi
115+
116+
- name: Test Examples on .NET Framework net48
117+
working-directory: ./AwsEncryptionSDK
118+
if: matrix.os == 'windows-latest'
119+
shell: bash
120+
run: |
121+
dotnet test \
122+
runtimes/net/Examples \
123+
--framework net48
124+
125+
- name: Test Examples on .NET net6.0
126+
working-directory: ./AwsEncryptionSDK
127+
shell: bash
128+
run: |
129+
if [ "$RUNNER_OS" == "macOS" ]; then
130+
DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib"
131+
dotnet test \
132+
runtimes/net/Examples \
133+
--framework net6.0
134+
else
135+
dotnet test \
136+
runtimes/net/Examples \
137+
--framework net6.0
138+
fi
139+
140+
- name: Unzip ESDK-NET @ v4.0.0 Valid Vectors
141+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
142+
shell: bash
143+
run: |
144+
NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
145+
mkdir -p $NET_400_VALID_VECTORS
146+
DOWNLOAD_NAME=valid-Net-4.0.0.zip
147+
unzip -o -qq $DOWNLOAD_NAME -d $NET_400_VALID_VECTORS
148+
149+
- name: Run ESDK-NET @ v4.0.0 Valid Vectors expect success
150+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
151+
continue-on-error: true
152+
shell: bash
153+
run: |
154+
NET_400_VALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Valid/vectors
155+
ESDK_NET_V400_POLICY="forbid" \
156+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
157+
dotnet test --framework net48
158+
ESDK_NET_V400_POLICY="forbid" \
159+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_VALID_VECTORS/manifest.json" \
160+
dotnet test --framework net6.0 --logger "console;verbosity=quiet"
161+
162+
- name: Unzip ESDK-NET @ v4.0.0 Invalid Vectors
163+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
164+
shell: bash
165+
run: |
166+
NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
167+
mkdir -p $NET_400_INVALID_VECTORS
168+
DOWNLOAD_NAME=invalid-Net-4.0.0.zip
169+
unzip -o -qq $DOWNLOAD_NAME -d $NET_400_INVALID_VECTORS
170+
171+
- name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 48 expect failure
172+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
173+
continue-on-error: true
174+
shell: bash
175+
run: |
176+
NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
177+
ESDK_NET_V400_POLICY="forbid" \
178+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
179+
dotnet test --framework net48
180+
# Dotnet test returns 1 for failure.
181+
TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
182+
# We want this to fail, so if it returned 1, step passes, else it fails
183+
# TODO Post-#619: Refactor Test Vectors to expect failure,
184+
# as I doubt this true false logic works
185+
186+
- name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET 6.0 expect failure
187+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
188+
continue-on-error: true
189+
shell: bash
190+
run: |
191+
NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
192+
if [ "$RUNNER_OS" == "macOS" ]; then
193+
ESDK_NET_V400_POLICY="forbid" \
194+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
195+
DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
196+
dotnet test --framework net6.0
197+
else
198+
ESDK_NET_V400_POLICY="forbid" \
199+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
200+
dotnet test --framework net6.0
201+
fi
202+
# Dotnet test returns 1 for failure.
203+
TEMP=$?; if [[ "$TEMP" -eq 1 ]]; then true; else false; fi;
204+
# We want this to fail, so if it returned 1, step passes, else it fails
205+
# TODO Post-#619: Refactor Test Vectors to expect failure,
206+
# as I doubt this true false logic works
207+
208+
- name: Run ESDK-NET @ v4.0.0 Invalid Vectors .NET expect Success
209+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
210+
shell: bash
211+
run: |
212+
NET_400_INVALID_VECTORS=$GITHUB_WORKSPACE/v4Net400Invalid/vectors
213+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
214+
dotnet test --framework net48 --logger "console;verbosity=quiet"
215+
if [ "$RUNNER_OS" == "macOS" ]; then
216+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
217+
DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
218+
dotnet test --framework net6.0 --logger "console;verbosity=quiet"
219+
else
220+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_400_INVALID_VECTORS/manifest.json" \
221+
dotnet test --framework net6.0 --logger "console;verbosity=quiet"
222+
fi
223+
224+
- name: Unzip ESDK-NET @ v4.0.1 Vectors
225+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors/resources
226+
shell: bash
227+
run: |
228+
NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
229+
mkdir -p $NET_401_VECTORS
230+
DOWNLOAD_NAME=v4-Net-4.0.1.zip
231+
unzip -o -qq $DOWNLOAD_NAME -d $NET_401_VECTORS
232+
233+
- name: Run ESDK-NET @ v4.0.1 Vectors expect success
234+
working-directory: ./AwsEncryptionSDK/runtimes/net/TestVectorsNative/TestVectors
235+
shell: bash
236+
run: |
237+
NET_401_VECTORS=$GITHUB_WORKSPACE/v4Net401/vectors
238+
# We expect net48 to run only for Windows
239+
if [ "$RUNNER_OS" == "Windows" ]; then
240+
ESDK_NET_V400_POLICY="forbid" \
241+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
242+
dotnet test --framework net48
243+
fi
244+
if [ "$RUNNER_OS" == "macOS" ]; then
245+
DYLD_LIBRARY_PATH="/usr/local/opt/[email protected]/lib" \
246+
ESDK_NET_V400_POLICY="forbid" \
247+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
248+
dotnet test --framework net6.0 --logger "console;verbosity=quiet"
249+
else
250+
ESDK_NET_V400_POLICY="forbid" \
251+
DAFNY_AWS_ESDK_TEST_VECTOR_MANIFEST_PATH="$NET_401_VECTORS/manifest.json" \
252+
dotnet test --framework net6.0 --logger "console;verbosity=quiet"
253+
fi

0 commit comments

Comments
 (0)