test_vector_verification.yml

# This workflow performs static analysis checks.
name: Test Vectors Dafny verification

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:
  verification:
    # Don't run the nightly build on forks
    if: github.event_name != 'schedule' || github.repository_owner == 'aws'
    strategy:
      matrix:
        os: [macos-12]
    runs-on: ${{ matrix.os }}
    defaults:
      run:
        shell: bash
    env:
      DOTNET_CLI_TELEMETRY_OPTOUT: 1
      DOTNET_NOLOGO: 1
    steps:
      - uses: actions/checkout@v3
        with:
          submodules: recursive

      - name: Setup Dafny
        uses: dafny-lang/setup-dafny-action@v1.7.0
        with:
          dafny-version: ${{ inputs.dafny }}

      - 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

      # dafny-reportgenerator requires next6
      # but only 7.0 is installed on macos-12-large
      - name: Setup .NET Core SDK '6.0.x'
        uses: actions/setup-dotnet@v4
        with:
          dotnet-version: "6.0.x"

      - name: Regenerate code using smithy-dafny if necessary
        if: ${{ inputs.regenerate-code }}
        uses: ./.github/actions/polymorph_codegen
        with:
          dafny: ${{ env.DAFNY_VERSION }}
          library: TestVectors
          diff-generated-code: false

      - name: Verify TestVectors
        working-directory: ./TestVectors
        run: |
          # This works because `node` is installed by default on GHA runners
          CORES=$(node -e 'console.log(os.cpus().length)')
          make verify CORES=$CORES

      - name: Check solver resource use
        if: success() || failure()
        working-directory: ./TestVectors
        run: |
          make dafny-reportgenerator