name: ci-conformance

# Builds and checks the conformance test suite (Tests/Conformance), regenerated from the
# conformance tests of IntersectMBO/plutus.
#
# Trigger with a PR comment, from a maintainer, of the form
#   /run-conformance [<plutus-ref>]
# e.g. `/run-conformance` or `/run-conformance 1.64.0.0`; or run the workflow manually.
# A comment-triggered run reports a `conformance` check on the PR head.
#
# The PR head can change between the comment and the checkout: GitHub does not report when a
# commit was pushed, and commit dates are set by their author. So the job that runs the PR's
# code (`conformance`) gets a read-only token and keeps no credentials, and only the jobs that
# never run it (`authorize`, `report`) can write to the PR. The check is reported on the commit
# that was tested, and names it.

permissions:
  contents: read

on:
  workflow_dispatch:
    inputs:
      plutus_ref:
        description: "IntersectMBO/plutus ref (branch, tag, or commit) to test against"
        required: false
        default: "master"
  issue_comment:
    types: [created]

# Only authorized requests share a concurrency group. Other comments get their own group,
# so an unauthorized /run-conformance comment cannot cancel a run in progress.
concurrency:
  group: >-
    ci-conformance-${{ github.event.issue.number || github.ref }}-${{
      (github.event_name == 'workflow_dispatch' ||
       (github.event_name == 'issue_comment' &&
        github.event.issue.pull_request != null &&
        startsWith(github.event.comment.body, '/run-conformance') &&
        (github.event.comment.author_association == 'OWNER' ||
         github.event.comment.author_association == 'MEMBER' ||
         github.event.comment.author_association == 'COLLABORATOR'))) && 'run' || github.run_id }}
  cancel-in-progress: true

env:
  LEAN_VERSION: "4.24.0"
  Z3_VERSION: "4.15.2"
  GLIBC_Z3: "2.39"

jobs:
  # Checks the trigger and prepares the run. Never runs the PR's code.
  authorize:
    # Run on:
    #   - any workflow_dispatch invocation, OR
    #   - a PR comment whose body starts with the trigger phrase, authored by
    #     a project maintainer (repo owner, org member, or invited collaborator).
    if: |
      github.event_name == 'workflow_dispatch' ||
      (github.event_name == 'issue_comment' &&
       github.event.issue.pull_request != null &&
       startsWith(github.event.comment.body, '/run-conformance') &&
       (github.event.comment.author_association == 'OWNER' ||
        github.event.comment.author_association == 'MEMBER' ||
        github.event.comment.author_association == 'COLLABORATOR'))
    runs-on: ubuntu-latest
    permissions:
      contents: read
      pull-requests: write
      checks: write
    outputs:
      repo: ${{ steps.pr.outputs.repo }}
      sha: ${{ steps.pr.outputs.sha }}
      plutus_ref: ${{ steps.plutus.outputs.ref }}
      check_id: ${{ steps.check.outputs.id }}

    steps:
      - name: Acknowledge comment trigger
        if: github.event_name == 'issue_comment'
        env:
          GH_TOKEN: ${{ github.token }}
        run: |
          # Add an "eyes" reaction to the triggering comment so the author sees
          # the workflow picked it up. Best-effort — failures here don't matter.
          gh api \
            --method POST \
            -H "Accept: application/vnd.github+json" \
            "/repos/${{ github.repository }}/issues/comments/${{ github.event.comment.id }}/reactions" \
            -f content='eyes' || true

      - name: Resolve plutus ref
        id: plutus
        env:
          # Passed via env vars: untrusted input is never interpolated into the script.
          COMMENT_BODY: ${{ github.event.comment.body }}
          DISPATCH_REF: ${{ github.event.inputs.plutus_ref }}
          EVENT_NAME: ${{ github.event_name }}
        run: |
          set -euo pipefail
          if [[ "$EVENT_NAME" == "issue_comment" ]]; then
            # The first whitespace-separated token after the trigger phrase, on the first line
            # of the comment.
            first_line=$(printf '%s\n' "$COMMENT_BODY" | head -n1 | tr -d '\r')
            ref=$(printf '%s\n' "$first_line" | sed -E 's|^/run-conformance[[:space:]]*||' | awk '{print $1}')
          else
            ref=$DISPATCH_REF
          fi
          ref=${ref:-master}
          # Whitelist refs to git-safe characters (alnum, dot, dash, underscore, slash).
          # Tags like v1.2.3 and 40-char SHAs both match.
          if ! [[ "$ref" =~ ^[A-Za-z0-9._/-]+$ ]]; then
            echo "::error::Refusing unsafe plutus ref: $ref"
            exit 1
          fi
          echo "ref=$ref" >> "$GITHUB_OUTPUT"
          echo "Resolved IntersectMBO/plutus ref: $ref"

      - name: Resolve PR head
        if: github.event_name == 'issue_comment'
        id: pr
        env:
          GH_TOKEN: ${{ github.token }}
          REPO_OWNER: ${{ github.event.repository.owner.login }}
          REPO_NAME: ${{ github.event.repository.name }}
          PR_NUMBER: ${{ github.event.issue.number }}
        run: |
          set -euo pipefail
          # The commit the conformance job checks out, by SHA. It is the PR head now, which may be
          # newer than the commit reviewed when the comment was posted (see the note at the top).
          query='query($owner: String!, $repo: String!, $num: Int!) {
            repository(owner: $owner, name: $repo) {
              pullRequest(number: $num) {
                headRefOid
                headRepository { nameWithOwner }
              }
            }
          }'
          result=$(gh api graphql -f query="$query" -F owner="$REPO_OWNER" -F repo="$REPO_NAME" -F num="$PR_NUMBER")
          head_sha=$(echo "$result" | jq -r '.data.repository.pullRequest.headRefOid')
          head_repo=$(echo "$result" | jq -r '.data.repository.pullRequest.headRepository.nameWithOwner')
          echo "PR head: $head_repo@$head_sha"
          echo "sha=$head_sha" >> "$GITHUB_OUTPUT"
          echo "repo=$head_repo" >> "$GITHUB_OUTPUT"

      # The last step, so that once the check run exists, this job succeeds and `report`
      # completes the check run.
      - name: Create check run on PR head
        if: github.event_name == 'issue_comment'
        id: check
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          HEAD_SHA: ${{ steps.pr.outputs.sha }}
          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
        run: |
          set -euo pipefail
          # A Check Run on the PR head SHA makes the conformance run appear in the PR's "Checks"
          # panel; issue_comment-triggered runs otherwise attach to the default branch.
          # Best-effort: without it the report job skips finalizing it and conformance still runs.
          id=$(gh api --method POST \
            -H "Accept: application/vnd.github+json" \
            "/repos/${{ github.repository }}/check-runs" \
            -f name='conformance' \
            -f head_sha="$HEAD_SHA" \
            -f status='in_progress' \
            -f details_url="$RUN_URL" \
            --jq '.id')
          echo "id=$id" >> "$GITHUB_OUTPUT"

  # Builds and runs the PR's code, so it gets a read-only token and keeps no credentials.
  conformance:
    needs: authorize
    runs-on: ubuntu-latest
    permissions:
      contents: read

    steps:
      - name: Setup Lean
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
          echo "/home/runner/.elan/bin" >> $GITHUB_PATH
          chmod +x /home/runner/.elan/bin/*

      - name: Fix Elan version
        run: |
          elan toolchain install ${{ env.LEAN_VERSION }}
          elan default ${{ env.LEAN_VERSION }}

      - name: Install Z3
        run: |
          cd /home/runner/
          wget -q https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}.zip
          unzip -q z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}.zip
          echo "/home/runner/z3-${{ env.Z3_VERSION }}-x64-glibc-${{ env.GLIBC_Z3 }}/bin" >> $GITHUB_PATH

      - name: Tools version
        run: |
          elan --version
          lake --version
          lean --version
          z3 --version

      - name: Checkout PlutusCoreBlaster
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
        with:
          repository: ${{ needs.authorize.outputs.repo || github.repository }}
          ref: ${{ needs.authorize.outputs.sha || github.ref }}
          path: PlutusCoreBlaster
          persist-credentials: false

      - name: Checkout IntersectMBO/plutus
        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
        with:
          repository: IntersectMBO/plutus
          ref: ${{ needs.authorize.outputs.plutus_ref }}
          path: plutus
          persist-credentials: false

      - name: Symlink .plutus-conformance
        run: |
          ln -s "${GITHUB_WORKSPACE}/plutus" "${GITHUB_WORKSPACE}/PlutusCoreBlaster/.plutus-conformance"
          ls -la "${GITHUB_WORKSPACE}/PlutusCoreBlaster/.plutus-conformance/plutus-conformance/test-cases" | head

      - name: Build PlutusCore
        working-directory: PlutusCoreBlaster
        run: make build_plutus_core

      # The plutus checkout is only read as data: the generator refuses test names that are not
      # plain identifiers (`isSafeName` in scripts/GenConformanceTests.lean), and the programs
      # run in the CEK machine.
      - name: Generate conformance test suite
        working-directory: PlutusCoreBlaster
        run: make gen_conformance_tests excludeNotImplemented=1

      - name: Build and validate conformance test suite
        working-directory: PlutusCoreBlaster
        run: make check_conformance

      - name: Upload conformance build log
        if: failure()
        uses: actions/upload-artifact@b7c566a772e6b6bfb58ed0dc250532a479d7789f  # v6.0.0
        with:
          name: conformance-build
          path: PlutusCoreBlaster/build.log

  # Completes the check run. Never runs the PR's code.
  report:
    needs: [authorize, conformance]
    if: always() && needs.authorize.outputs.check_id != ''
    runs-on: ubuntu-latest
    permissions:
      checks: write

    steps:
      - name: Finalize check run
        continue-on-error: true
        env:
          GH_TOKEN: ${{ github.token }}
          CHECK_ID: ${{ needs.authorize.outputs.check_id }}
          HEAD_REPO: ${{ needs.authorize.outputs.repo }}
          HEAD_SHA: ${{ needs.authorize.outputs.sha }}
          PLUTUS_REF: ${{ needs.authorize.outputs.plutus_ref }}
          RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
          # The conformance job's result: success, failure, cancelled or skipped, all valid
          # conclusions for the Checks API.
          CONCLUSION: ${{ needs.conformance.result }}
        run: |
          set -euo pipefail
          summary="Tested commit \`$HEAD_SHA\` (${HEAD_REPO}), the PR head when the run started, against the conformance tests of IntersectMBO/plutus \`$PLUTUS_REF\`: [run ${GITHUB_RUN_ID}]($RUN_URL)."
          jq -n --arg c "$CONCLUSION" --arg t "Conformance tests: $CONCLUSION" --arg s "$summary" \
            '{status: "completed", conclusion: $c, output: {title: $t, summary: $s}}' |
            gh api --method PATCH \
              -H "Accept: application/vnd.github+json" \
              "/repos/${{ github.repository }}/check-runs/$CHECK_ID" \
              --input -