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

rishav-karanjit · web-flow · commit d69f25313a18 · 2025-05-12T09:41:10.000-07:00
diff --git a/.github/workflows/ci_test_go.yml b/.github/workflows/ci_test_go.yml
@@ -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:
@@ -45,7 +45,7 @@ jobs:
         with:
           port: 8000
           cors: "*"
-          
+
       - name: Support longpaths
         run: |
           git config --global core.longpaths true
@@ -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:
@@ -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
 
@@ -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: |
diff --git a/.github/workflows/ci_todos.yml b/.github/workflows/ci_todos.yml
@@ -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
diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
@@ -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) }}
diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
@@ -1,5 +1,4 @@
 # This workflow runs for every push to main
-# TODO: CI for Go
 name: Push CI
 
 on:
@@ -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
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy
@@ -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
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Index.dfy
@@ -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
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Index.dfy
@@ -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
 {
 
diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -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
+    else
+      "../../../" + mplKeysPath
+  }
 
   method AddJson(prev : TestVectorConfig, file : string, keyVectors: KeyVectors.KeyVectorsClient)
     returns (output : Result<TestVectorConfig, string>)
@@ -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()
       )
     );
 
diff --git a/submodules/smithy-dafny b/submodules/smithy-dafny
@@ -1 +1 @@
-Subproject commit 276aacb938b78401f0f50006c01195e7d241b216
+Subproject commit 2f83e28ad9532b24c93d2229476c9a268355d338

Original file line number	Diff line number	Diff line change
`@@ -16,7 +16,7 @@ include "UpdateExpr.dfy"`
`16`	`16`	`include "Util.dfy"`
`17`	`17`	`include "Virtual.dfy"`
`18`	`18`
`19`		`-module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption`
	`19`	`+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny" } DynamoDbEncryption`
`20`	`20`	`refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbService`
`21`	`21`	`{`
`22`	`22`	`import Operations = AwsCryptographyDbEncryptionSdkDynamoDbOperations`
Original file line number	Diff line number	Diff line change
`@@ -4,7 +4,7 @@`
`4`	`4`	`include "AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy"`
`5`	`5`	`include "Util.dfy"`
`6`	`6`
`7`		`-module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor`
	`7`	`+module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny" } DynamoDbItemEncryptor`
`8`	`8`	`refines AbstractAwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorService`
`9`	`9`	`{`
`10`	`10`	`import opened DynamoDbItemEncryptorUtil`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,7 @@`
`3`	`3`
`4`	`4`	`include "AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy"`
`5`	`5`
`6`		`-module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption`
	`6`	`+module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny" } StructuredEncryption`
`7`	`7`	`refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionService`
`8`	`8`	`{`
`9`	`9`