Skip to content

chore(dafny): make CI to work for all runtimes #1871

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 11 commits into from
May 12, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions .github/workflows/ci_test_go.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ jobs:
strategy:
matrix:
library: [DynamoDbEncryption, TestVectors]
os: [ubuntu-22.04]
os: [ubuntu-22.04, macos-13]
go-version: ["1.23"]
runs-on: ${{ matrix.os }}
permissions:
Expand All @@ -45,7 +45,7 @@ jobs:
with:
port: 8000
cors: "*"

- name: Support longpaths
run: |
git config --global core.longpaths true
Expand All @@ -68,7 +68,7 @@ jobs:

- name: Create temporary global.json
run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json

- name: Setup Java 17 for codegen
uses: actions/setup-java@v3
with:
Expand Down Expand Up @@ -104,7 +104,7 @@ jobs:
run: |
git submodule update --init --recursive submodules/smithy-dafny
git submodule update --init --recursive submodules/MaterialProviders

- name: Install Smithy-Dafny codegen dependencies
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies

Expand All @@ -121,14 +121,14 @@ jobs:
working-directory: ./${{ matrix.library }}
run: |
make polymorph_go

- name: Copy ${{ matrix.library }} Vector Files
if: ${{ matrix.library == 'TestVectors' }}
shell: bash
working-directory: ./${{ matrix.library }}
run: |
cp runtimes/java/*.json runtimes/go/TestsFromDafny-go/

- name: Test ${{ matrix.library }}
working-directory: ./${{ matrix.library }}
run: |
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci_todos.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,4 +22,4 @@
# GOOD_TODO_COUNT=$( { grep -r "TODO.*\(github.com\/.*issues.*\/[1-9][0-9]*\|CrypTool-[1-9][0-9]*\)" . --exclude-dir=./releases --exclude-dir=./submodules --exclude-dir=./.git --exclude-dir=./TestVectors/runtimes --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
# if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then
# exit 1;
# fi
# fi
161 changes: 78 additions & 83 deletions .github/workflows/pull.yml
Original file line number Diff line number Diff line change
@@ -1,99 +1,94 @@
# This workflow runs for every pull request
# TODO: CI for Go
name: PR CI

on:
pull_request:
push:
branches:
- Golang/reviewed
schedule:
- cron: "00 16 * * 1-5"

jobs:
getVersion:
uses: ./.github/workflows/dafny_version.yml
getVerifyVersion:
uses: ./.github/workflows/dafny_verify_version.yml
# pr-ci-format:
# needs: getVersion
# uses: ./.github/workflows/library_format.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-codegen:
# needs: getVersion
# uses: ./.github/workflows/ci_codegen.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-verification:
# needs: getVerifyVersion
# uses: ./.github/workflows/library_dafny_verification.yml
# with:
# dafny: ${{needs.getVerifyVersion.outputs.version}}
# pr-ci-test-vector-verification:
# needs: getVerifyVersion
# uses: ./.github/workflows/test_vector_verification.yml
# with:
# dafny: ${{needs.getVerifyVersion.outputs.version}}
# pr-ci-java:
# needs: getVersion
# uses: ./.github/workflows/ci_test_java.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-java-test-vectors:
# needs: getVersion
# uses: ./.github/workflows/ci_test_vector_java.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-java-examples:
# needs: getVersion
# uses: ./.github/workflows/ci_examples_java.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-net:
# needs: getVersion
# uses: ./.github/workflows/ci_test_net.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-rust:
# needs: getVersion
# uses: ./.github/workflows/library_rust_tests.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
pr-ci-format:
needs: getVersion
uses: ./.github/workflows/library_format.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-codegen:
needs: getVersion
uses: ./.github/workflows/ci_codegen.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-verification:
needs: getVerifyVersion
uses: ./.github/workflows/library_dafny_verification.yml
with:
dafny: ${{needs.getVerifyVersion.outputs.version}}
pr-ci-test-vector-verification:
needs: getVerifyVersion
uses: ./.github/workflows/test_vector_verification.yml
with:
dafny: ${{needs.getVerifyVersion.outputs.version}}
pr-ci-java:
needs: getVersion
uses: ./.github/workflows/ci_test_java.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-java-test-vectors:
needs: getVersion
uses: ./.github/workflows/ci_test_vector_java.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-java-examples:
needs: getVersion
uses: ./.github/workflows/ci_examples_java.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-net:
needs: getVersion
uses: ./.github/workflows/ci_test_net.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-rust:
needs: getVersion
uses: ./.github/workflows/library_rust_tests.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-go:
needs: getVersion
uses: ./.github/workflows/ci_test_go.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-net-test-vectors:
# needs: getVersion
# uses: ./.github/workflows/ci_test_vector_net.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-net-examples:
# needs: getVersion
# uses: ./.github/workflows/ci_examples_net.yml
# with:
# dafny: ${{needs.getVersion.outputs.version}}
# pr-ci-all-required:
# if: always()
# needs:
# - getVersion
# - getVerifyVersion
# - pr-ci-format
# - pr-ci-codegen
# - pr-ci-verification
# - pr-ci-test-vector-verification
# - pr-ci-java
# - pr-ci-java-test-vectors
# - pr-ci-java-examples
# - pr-ci-net
# - pr-ci-rust
# - pr-ci-net-test-vectors
# - pr-ci-net-examples
# runs-on: ubuntu-22.04
# steps:
# - name: Verify all required jobs passed
# uses: re-actors/alls-green@release/v1
# with:
# jobs: ${{ toJSON(needs) }}
pr-ci-net-test-vectors:
needs: getVersion
uses: ./.github/workflows/ci_test_vector_net.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-net-examples:
needs: getVersion
uses: ./.github/workflows/ci_examples_net.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-all-required:
if: always()
needs:
- getVersion
- getVerifyVersion
- pr-ci-format
- pr-ci-codegen
- pr-ci-verification
- pr-ci-test-vector-verification
- pr-ci-java
- pr-ci-java-test-vectors
- pr-ci-java-examples
- pr-ci-net
- pr-ci-rust
- pr-ci-go
- pr-ci-net-test-vectors
- pr-ci-net-examples
runs-on: ubuntu-22.04
steps:
- name: Verify all required jobs passed
uses: re-actors/alls-green@release/v1
with:
jobs: ${{ toJSON(needs) }}
6 changes: 5 additions & 1 deletion .github/workflows/push.yml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
# This workflow runs for every push to main
# TODO: CI for Go
name: Push CI

on:
Expand Down Expand Up @@ -57,6 +56,11 @@ jobs:
uses: ./.github/workflows/library_rust_tests.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-go:
needs: getVersion
uses: ./.github/workflows/ci_test_go.yml
with:
dafny: ${{needs.getVersion.outputs.version}}
pr-ci-net-test-vectors:
needs: getVersion
uses: ./.github/workflows/ci_test_vector_net.yml
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ include "UpdateExpr.dfy"
include "Util.dfy"
include "Virtual.dfy"

module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption
module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption
refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService
{
import Operations = AwsCryptographyDbEncryptionSdkDynamoDbOperations
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
include "AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy"
include "Util.dfy"

module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor
module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor
refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService
{
import opened DynamoDbItemEncryptorUtil
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy"

module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption
module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption
refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService
{

Expand Down
12 changes: 9 additions & 3 deletions TestVectors/dafny/DDBEncryption/src/Index.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,14 @@ module WrappedDDBEncryptionMain {
import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
import WrappedItemEncryptor

// TODO: Add extern for DEFAULT_KEYS
const DEFAULT_KEYS : string := "../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json"
function method GetDefaultKeysPath(): string
{
var mplKeysPath := "submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/test/keys.json";
if OsLang.GetLanguageShort() == "Go" then
"../../../../" + mplKeysPath
Comment on lines +25 to +26
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For context: Go generates code into runtimes/go/<Implementation-From-Dafny> or <Test-From-Dafny>/. When we run make test_go, it runs from runtimes/go/Test-From-Dafny/. For all other runtimes it runs from runtimes/<runtime>

else
"../../../" + mplKeysPath
}

method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient)
returns (output : Result<TestVectorConfig, string>)
Expand Down Expand Up @@ -52,7 +58,7 @@ module WrappedDDBEncryptionMain {
// Parsing JSON is very slow in Python. Parse JSON as infrequently as possible.
var keyVectors :- expect KeyVectors.KeyVectors(
KeyVectorsTypes.KeyVectorsConfig(
keyManifestPath := DEFAULT_KEYS
keyManifestPath := GetDefaultKeysPath()
)
);

Expand Down
2 changes: 1 addition & 1 deletion submodules/smithy-dafny
Loading