.github/actions/install_smithy_dafny_codegen_dependencies/action.yml

@@ -8,14 +8,30 @@ description: "Install Java package dependencies required to run Smithy-Dafny cod
 runs:
   using: "composite"
   steps:
-    - name: Install smithy-dafny-codegen Rust dependencies locally
-      uses: gradle/gradle-build-action@v2
+    - name: Setup Java 17 for codegen
+      uses: actions/setup-java@v3
       with:
-        arguments: :codegen-client:pTML :codegen-core:pTML :rust-runtime:pTML
-        build-root-directory: submodules/smithy-dafny/smithy-dafny-codegen-modules/smithy-rs
+        distribution: "corretto"
+        java-version: "17"
 
-    - name: Install smithy-dafny-codegen Python dependencies locally
-      uses: gradle/gradle-build-action@v2
+    - name: Install smithy-dafny-codegen dependencies locally
+      shell: bash
+      run: |
+        make -C submodules/smithy-dafny mvn_local_deploy_polymorph_dependencies
+
+    - name: Setup Python, black, and docformatter for code formatting
+      uses: actions/setup-python@v4
       with:
-        arguments: :smithy-python-codegen:pTML
-        build-root-directory: submodules/smithy-dafny/codegen/smithy-dafny-codegen-modules/smithy-python/codegen
+        python-version: ${{ matrix.python-version }}
+        architecture: x64
+    - shell: bash
+      run: |
+        python -m pip install --upgrade pip
+        python -m pip install --upgrade black
+        python -m pip install --upgrade docformatter
+
+    # Without this the if-dafny-at-least command includes "Downloading ..." output
+    - name: Arbitrary makefile target to force downloading Gradle
+      shell: bash
+      run: |
+        make -C submodules/MaterialProviders/StandardLibrary setup_net

.github/actions/polymorph_codegen/action.yml

@@ -141,6 +141,12 @@ runs:
       run: |
         make polymorph_dotnet ${{ steps.dependencies.outputs.PROJECT_DEPENDENCIES }}
 
+    - name: Regenerate Go code using smithy-dafny
+      working-directory: ./${{ inputs.library }}
+      shell: bash
+      run: |
+        make polymorph_go
+
     - name: Check regenerated code against commited code
       # Composite action inputs seem to not actually support booleans properly for some reason
       if: inputs.diff-generated-code == 'true'

.github/workflows/ci_codegen.yml

@@ -18,6 +18,7 @@ jobs:
         # in this workflow
         dotnet-version: ["6.0.x"]
         os: [ubuntu-22.04]
+        go-version: [1.23]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
@@ -48,6 +49,15 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      - name: Install Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: ${{ matrix.go-version }}
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
       - name: Create temporary global.json
         run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
 

.github/workflows/ci_examples_java.yml

@@ -26,7 +26,6 @@ on:
 jobs:
   testJava:
     strategy:
-      max-parallel: 1
       matrix:
         java-version: [8, 11, 16, 17]
         os: [macos-13]
@@ -71,6 +70,9 @@ jobs:
         run: |
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_examples_net.yml

@@ -59,6 +59,9 @@ jobs:
           git submodule update --init --recursive
           git rev-parse HEAD
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_go.yml

@@ -0,0 +1,148 @@
+# This workflow performs tests in Go.
+name: Library Go tests
+
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      regenerate-code:
+        description: "Regenerate code using smithy-dafny"
+        required: false
+        default: false
+        type: boolean
+      mpl-version:
+        description: "MPL version to use"
+        required: false
+        type: string
+      mpl-head:
+        description: "Running on MPL HEAD"
+        required: false
+        default: false
+        type: boolean
+
+jobs:
+  testGo:
+    strategy:
+      fail-fast: false
+      matrix:
+        library: [DynamoDbEncryption, TestVectors]
+        os: [ubuntu-22.04, macos-13]
+        go-version: ["1.23", "1.24"]
+    runs-on: ${{ matrix.os }}
+    permissions:
+      id-token: write
+      contents: read
+    steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1-alpha
+
+      - name: Setup DynamoDB Local
+        if: matrix.library == 'TestVectors'
+        uses: rrainn/dynamodb-action@v4.0.0
+        with:
+          port: 8000
+          cors: "*"
+
+      - name: Support longpaths
+        run: |
+          git config --global core.longpaths true
+
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v4
+        with:
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-DDBEC-Dafny-Role-us-west-2
+          role-session-name: DDBEC-Dafny-Java-Tests
+
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Setup Dafny
+        uses: dafny-lang/setup-dafny-action@v1.8.0
+        with:
+          dafny-version: ${{ inputs.dafny }}
+
+      - 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:
+          distribution: "corretto"
+          java-version: "17"
+
+      - name: Update MPL submodule if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        working-directory: submodules/MaterialProviders
+        run: |
+          git checkout main
+          git pull
+          git submodule update --init --recursive
+          git rev-parse HEAD
+
+      - name: Update project.properties if using MPL HEAD
+        if: ${{ inputs.mpl-head == true }}
+        run: |
+          sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
+
+      - name: Install Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: ${{ matrix.go-version }}
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
+      - uses: actions/checkout@v3
+      - name: Init Submodules
+        shell: bash
+        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
+
+      - name: Install Go imports
+        shell: bash
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
+      - name: Build ${{ matrix.library }} implementation
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_go CORES=$CORES
+
+      - name: Regenerate code using smithy-dafny
+        shell: bash
+        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: |
+          make test_go
+
+      - name: Run and Test Examples
+        if: matrix.library == 'DynamoDbEncryption'
+        working-directory: ./Examples/runtimes/go
+        run: |
+          go run main.go
+          go test ./...

.github/workflows/ci_test_java.yml

@@ -26,6 +26,7 @@ on:
 jobs:
   testJava:
     strategy:
+      fail-fast: false
       matrix:
         library: [DynamoDbEncryption]
         java-version: [8, 11, 16, 17]
@@ -65,6 +66,9 @@ jobs:
         run: |
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_latest_released_mpl_java.yml

@@ -58,6 +58,9 @@ jobs:
         with:
           dafny-version: ${{ needs.getVersion.outputs.version }}
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_net.yml

@@ -60,6 +60,9 @@ jobs:
           git submodule update --init --recursive
           git rev-parse HEAD
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_vector_java.yml

@@ -32,12 +32,17 @@ jobs:
         os: [
             # Run on ubuntu image that comes pre-configured with docker
             ubuntu-22.04,
+            macos-13,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
       contents: read
     steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1.0.0
+
       - name: Setup DynamoDB Local
         uses: rrainn/dynamodb-action@v4.0.0
         with:
@@ -74,6 +79,9 @@ jobs:
         run: |
           sed "s/mplDependencyJavaVersion=.*/mplDependencyJavaVersion=${{inputs.mpl-version}}/g" project.properties > project.properties2; mv project.properties2 project.properties
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen

.github/workflows/ci_test_vector_net.yml

@@ -28,12 +28,17 @@ jobs:
         os: [
             # Run on ubuntu image that comes pre-configured with docker
             ubuntu-22.04,
+            macos-13,
           ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
       contents: read
     steps:
+      - name: Setup Docker
+        if: matrix.os == 'macos-13' && matrix.library == 'TestVectors'
+        uses: douglascamata/setup-docker-macos-action@v1.0.0
+
       - name: Setup DynamoDB Local
         uses: rrainn/dynamodb-action@v4.0.0
         with:
@@ -65,6 +70,9 @@ jobs:
           git submodule update --init --recursive
           git rev-parse HEAD
 
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
       - name: Regenerate code using smithy-dafny if necessary
         if: ${{ inputs.regenerate-code }}
         uses: ./.github/actions/polymorph_codegen
@@ -89,7 +97,6 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json .
-          dotnet run
           cp ../java/*.json .
+          dotnet run
           dotnet run --framework net6.0

.github/workflows/ci_todos.yml

@@ -17,8 +17,8 @@ jobs:
         shell: bash
         # TODOs may be committed as long as the same line contains a link to a Github Issue or refers to a CrypTool SIM.
         run: |
-          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./releases --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml || true; } | wc -l)
-          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)
+          ALL_TODO_COUNT=$( { grep -r "TODO" . --exclude-dir=./releases --exclude-dir=./TestVectors/runtimes --exclude-dir=./submodules --exclude-dir=./.git --exclude=./.github/workflows/ci_todos.yml | grep -v "context\.TODO()" || true; } | wc -l)
+          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 | grep -v "context\.TODO()" || true; } | wc -l)
           if [ "$ALL_TODO_COUNT" != "$GOOD_TODO_COUNT" ]; then
             exit 1;
           fi

.github/workflows/dafny_interop_test_vector_net.yml

@@ -108,7 +108,6 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json .
-          dotnet run
           cp ../java/*.json .
+          dotnet run
           dotnet run --framework net6.0