Skip to content

Commit 7292294

Browse files
josecorellajosecorella
committed
split up test vector verfication
1 parent 25a936f commit 7292294

File tree

6 files changed

+91
-19
lines changed

6 files changed

+91
-19
lines changed

‎.github/workflows/library_dafny_verification.yml

+2-19
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@ jobs:
2828
DynamoDbEncryptionTransforms,
2929
DynamoDbItemEncryptor,
3030
StructuredEncryption,
31-
TestVectors,
3231
]
3332
os: [macos-12]
3433
runs-on: ${{ matrix.os }}
@@ -64,30 +63,14 @@ jobs:
6463
diff-generated-code: false
6564

6665
- name: Verify ${{ matrix.library }} Dafny code
67-
if: ${{ matrix.library != 'TestVectors' }}
6866
working-directory: ./DynamoDbEncryption
6967
run: |
7068
# This works because `node` is installed by default on GHA runners
7169
CORES=$(node -e 'console.log(os.cpus().length)')
7270
make verify_service CORES=$CORES SERVICE=${{ matrix.library }}
73-
71+
7472
- name: Check solver resource use
75-
if: (success() || failure()) && ${{ matrix.library != 'TestVectors' }}
73+
if: success() || failure()
7674
working-directory: ./DynamoDbEncryption
7775
run: |
7876
make dafny-reportgenerator
79-
80-
- name: Verify TestVectors Dafny code
81-
if: ${{ matrix.library == 'TestVectors' }}
82-
working-directory: ${{ matrix.library }}
83-
run: |
84-
# This works because `node` is installed by default on GHA runners
85-
CORES=$(node -e 'console.log(os.cpus().length)')
86-
make verify CORES=$CORES
87-
88-
- name: Check solver resource use
89-
if: (success() || failure()) && ${{ matrix.library == 'TestVectors' }}
90-
working-directory: ${{matrix.library}}
91-
run: |
92-
make dafny-reportgenerator
93-

‎.github/workflows/manual.yml

+5
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,11 @@ jobs:
2727
with:
2828
dafny: ${{ inputs.dafny }}
2929
regenerate-code: ${{ inputs.regenerate-code }}
30+
manual-ci-test-vector-verification:
31+
uses: ./.github/workflows/test_vector_verification.yml
32+
with:
33+
dafny: ${{ inputs.dafny }}
34+
regenerate-code: ${{ inputs.regenerate-code }}
3035
manual-ci-java:
3136
uses: ./.github/workflows/ci_test_java.yml
3237
with:

‎.github/workflows/nightly.yml

+7
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,13 @@ jobs:
2525
with:
2626
dafny: "nightly-latest"
2727
regenerate-code: true
28+
dafny-nightly-test-vector-verification:
29+
# Don't run the cron builds on forks
30+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
31+
uses: ./.github/workflows/test_vector_verification.yml
32+
with:
33+
dafny: "nightly-latest"
34+
regenerate-code: true
2835
dafny-nightly-java:
2936
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
3037
uses: ./.github/workflows/ci_test_java.yml

‎.github/workflows/pull.yml

+5
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,11 @@ jobs:
2424
uses: ./.github/workflows/library_dafny_verification.yml
2525
with:
2626
dafny: ${{needs.getVerifyVersion.outputs.version}}
27+
pr-ci-test-vector-verification:
28+
needs: getVerifyVersion
29+
uses: ./.github/workflows/test_vector_verification.yml
30+
with:
31+
dafny: ${{needs.getVerifyVersion.outputs.version}}
2732
pr-ci-java:
2833
needs: getVersion
2934
uses: ./.github/workflows/ci_test_java.yml

‎.github/workflows/push.yml

+5
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,11 @@ jobs:
2626
uses: ./.github/workflows/library_dafny_verification.yml
2727
with:
2828
dafny: ${{needs.getVerifyVersion.outputs.version}}
29+
push-ci-test-vector-verification:
30+
needs: getVerifyVersion
31+
uses: ./.github/workflows/test_vector_verification.yml
32+
with:
33+
dafny: ${{needs.getVerifyVersion.outputs.version}}
2934
pr-ci-java:
3035
needs: getVersion
3136
uses: ./.github/workflows/ci_test_java.yml

‎.github/workflows/test_vector_verification.yml

+67
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
# This workflow performs static analysis checks.
2+
name: Test Vectors Dafny verification
3+
4+
on:
5+
workflow_call:
6+
inputs:
7+
dafny:
8+
description: "The Dafny version to run"
9+
required: true
10+
type: string
11+
regenerate-code:
12+
description: "Regenerate code using smithy-dafny"
13+
required: false
14+
default: false
15+
type: boolean
16+
17+
jobs:
18+
verification:
19+
# Don't run the nightly build on forks
20+
if: github.event_name != 'schedule' || github.repository_owner == 'aws'
21+
strategy:
22+
matrix:
23+
os: [macos-12]
24+
runs-on: ${{ matrix.os }}
25+
defaults:
26+
run:
27+
shell: bash
28+
env:
29+
DOTNET_CLI_TELEMETRY_OPTOUT: 1
30+
DOTNET_NOLOGO: 1
31+
steps:
32+
- uses: actions/checkout@v3
33+
with:
34+
submodules: recursive
35+
36+
- name: Setup Dafny
37+
uses: dafny-lang/[email protected]
38+
with:
39+
dafny-version: ${{ inputs.dafny }}
40+
41+
# dafny-reportgenerator requires next6
42+
# but only 7.0 is installed on macos-12-large
43+
- name: Setup .NET Core SDK '6.0.x'
44+
uses: actions/setup-dotnet@v3
45+
with:
46+
dotnet-version: "6.0.x"
47+
48+
- name: Regenerate code using smithy-dafny if necessary
49+
if: ${{ inputs.regenerate-code }}
50+
uses: ./.github/actions/polymorph_codegen
51+
with:
52+
dafny: ${{ env.DAFNY_VERSION }}
53+
library: TestVectors
54+
diff-generated-code: false
55+
56+
- name: Verify TestVectors
57+
working-directory: ./TestVectors
58+
run: |
59+
# This works because `node` is installed by default on GHA runners
60+
CORES=$(node -e 'console.log(os.cpus().length)')
61+
make verify CORES=$CORES
62+
63+
- name: Check solver resource use
64+
if: success() || failure()
65+
working-directory: ./TestVectors
66+
run: |
67+
make dafny-reportgenerator

0 commit comments

Comments
 (0)