library_dafny_verification.yml

# This workflow performs static analysis checks.
name: Library 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

jobs:
  verification:
    strategy:
      matrix:
        library: [
          AwsEncryptionSDK,
          TestVectors
        ]
        os: [ macos-13 ]
    runs-on: ${{ matrix.os }}
    env:
      DOTNET_CLI_TELEMETRY_OPTOUT: 1
      DOTNET_NOLOGO: 1
    steps:
      - name: Support longpaths
        run: |
          git config --global core.longpaths true
          
      - uses: actions/checkout@v2
      - name: Init Submodules
        run: |
            git submodule update --init libraries
            git submodule update --init --recursive mpl

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

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

      - name: Regenerate code using smithy-dafny if necessary
        if: ${{ inputs.regenerate-code }}
        uses: ./.github/actions/polymorph_codegen
        with:
          dafny: ${{ env.DAFNY_VERSION }}
          library: ${{ matrix.library }}
          diff-generated-code: false
          update-and-regenerate-mpl: true
            
      - name: Verify ${{ matrix.library }} Dafny code
        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 verify CORES=$CORES

      - name: Check solver resource use
        shell: bash
        working-directory: ./${{ matrix.library }}
        run: |
          make dafny-reportgenerator