verify-proofs.yml

# SPDX-License-Identifier: MPL-2.0
# This workflow is managed by gh actions-lock.
# Consolidated workflow (behaviour-preserving merge).
# Merged from: verify-idris.yml, verify-lean.yml, verify-tlaplus.yml
name: Verify Proofs (Idris / Lean / TLA+)

on:
  push:
    paths:
    - .github/workflows/verify-proofs.yml
    - Justfile
    - pack.toml
    - verification/proofs/idris2/**
    - verification/proofs/lean4/**
    - verification/proofs/tlaplus/**
    - src/abi/**
    - src/Hypatia/ABI/**
    - verify/**
    branches:
    - main
  pull_request:
    paths:
    - .github/workflows/verify-proofs.yml
    - Justfile
    - pack.toml
    - verification/proofs/idris2/**
    - verification/proofs/lean4/**
    - verification/proofs/tlaplus/**
    - src/abi/**
    - src/Hypatia/ABI/**
    - verify/**
    branches:
    - main
  schedule:
  # Weekly Monday 04:00 UTC — single trigger. The three crons (04:00,
  # 04:30, 05:00) were inherited from the pre-consolidation
  # verify-{idris,lean,tlaplus}.yml workflows and fired the now-merged
  # workflow three times every Monday. Collapsed to one.
  - cron: '0 4 * * 1'
  workflow_dispatch:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

permissions: read-all

jobs:
  type-check:
    name: idris2 --check
    runs-on: ubuntu-latest
    timeout-minutes: 25
    permissions:
      contents: read

    env:
      IDRIS2_VERSION: v0.7.0

    steps:
      - name: Checkout
        uses: actions/checkout@v7.0.1

      - name: Install Chez Scheme
        run: |
          set -euo pipefail
          sudo apt-get update
          sudo apt-get install -y chezscheme

      - name: Cache Idris 2 install
        id: cache-idris
        uses: actions/cache@v6.1.0
        with:
          path: |
            /usr/local/bin/idris2
            /usr/local/bin/idris2_app
            /usr/local/lib/idris2
            ~/.idris2
          # `idris2` is only a launcher script; it execs its sibling
          # idris2_app/idris2.so. The previous cache omitted idris2_app/, so
          # every cache *hit* restored a launcher with no image and died with
          # `idris2_app/idris2.so: not found` (exit 127) before any proof ran.
          # Key bumped to -2 to discard those poisoned caches.
          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-2

      - name: Build Idris 2 from source
        if: steps.cache-idris.outputs.cache-hit != 'true'
        run: |
          set -euo pipefail
          git clone --depth 1 --branch "${IDRIS2_VERSION}" \
            https://github.com/idris-lang/Idris2 /tmp/idris2
          cd /tmp/idris2
          make bootstrap SCHEME=chezscheme
          sudo make install PREFIX=/usr/local
          idris2 --version

      - name: Verify Idris is on PATH
        run: idris2 --version

      - name: Type-check every .idr proof file
        working-directory: verification/proofs/idris2
        run: |
          set -euo pipefail
          failed=0
          for f in *.idr; do
            echo "── $f ─────────────────────────────────────────────"
            if idris2 --check "$f"; then
              echo "✓ $f"
            else
              echo "✗ $f"
              failed=$((failed + 1))
            fi
          done
          if [ "$failed" -gt 0 ]; then
            echo "::error::$failed Idris proof file(s) failed to type-check"
            exit 1
          fi

      # The standalone files above are only half the Idris proof surface. The
      # richest proofs (RuleEngine's safety-triangle / dispatch / Bayesian
      # monotonicity, the FFI ApiResponse proof, the pipeline state machine)
      # live in the ABI and verify *packages*, which the per-file --check loop
      # never builds. Gate them here so they can't silently rot again.
      - name: Build the ABI proof package (Types, GraphQL, gRPC, REST, FFI, RuleEngine)
        run: idris2 --build src/abi/hypatia-abi.ipkg

      - name: Build the verify package (PipelineState, Verify.Fuel)
        run: idris2 --build verify/hypatia-verify.ipkg

      - name: Summary
        if: always()
        run: |
          {
            echo "## Idris 2 proof verification"
            echo ""
            echo "- Toolchain: Idris 2 \`${IDRIS2_VERSION}\` (from source, Chez Scheme backend)"
            echo "- Proof files checked:"
            for f in verification/proofs/idris2/*.idr; do
              echo "  - \`$(basename "$f")\`"
            done
          } >> "$GITHUB_STEP_SUMMARY"

  lake-build:
    name: lake build
    runs-on: ubuntu-latest
    timeout-minutes: 20
    permissions:
      contents: read

    env:
      ELAN_VERSION: v4.0.0
      # Pinned (not :stable) so the proofs are checked against the exact Lean
      # they were verified with. Matches verification/proofs/lean4/lean-toolchain;
      # bump both together. A moving :stable can break version-sensitive lemmas.
      LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0

    steps:
      - name: Checkout
        uses: actions/checkout@v7.0.1

      - name: Cache Lean toolchain and build
        id: cache-lean
        uses: actions/cache@v6.1.0
        with:
          path: |
            ~/.elan
            verification/proofs/lean4/.lake
          key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-${{ hashFiles('verification/proofs/lean4/lakefile.lean', 'verification/proofs/lean4/*.lean') }}
          restore-keys: |
            lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-

      - name: Install elan + Lean 4
        if: steps.cache-lean.outputs.cache-hit != 'true'
        run: |
          set -euo pipefail
          curl -fL -o /tmp/elan-init.sh "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh"
          sh /tmp/elan-init.sh -y --default-toolchain "${LEAN_TOOLCHAIN}" --no-modify-path

      - name: Put elan on PATH
        run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: lake build
        working-directory: verification/proofs/lean4
        run: |
          set -euo pipefail
          lean --version
          lake --version
          lake build

      - name: Summary
        if: always()
        run: |
          {
            echo "## Lean proof verification"
            echo ""
            echo "- Toolchain: \`${LEAN_TOOLCHAIN}\` via elan \`${ELAN_VERSION}\`"
            echo "- Proof files:"
            for f in verification/proofs/lean4/*.lean; do
              [ "$(basename "$f")" = "lakefile.lean" ] && continue
              echo "  - \`$(basename "$f")\`"
            done
          } >> "$GITHUB_STEP_SUMMARY"

  tlc:
    name: TLC model-check
    runs-on: ubuntu-latest
    permissions:
      contents: read
    timeout-minutes: 15

    steps:
      - name: Checkout
        uses: actions/checkout@v7.0.1

      - name: Set up Eclipse Temurin 21 JRE
        uses: actions/setup-java@v6.0.0
        with:
          distribution: temurin
          java-version: '21'

      - name: Cache tla2tools.jar
        id: cache-tla
        uses: actions/cache@v6.1.0
        with:
          path: ~/.local/share/tla2tools.jar
          key: tla2tools-v1.8.0

      - name: Fetch tla2tools.jar
        if: steps.cache-tla.outputs.cache-hit != 'true'
        run: |
          mkdir -p ~/.local/share
          curl -sSL -o ~/.local/share/tla2tools.jar \
            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
          ls -la ~/.local/share/tla2tools.jar

      - name: Model-check KinGate (H8)
        working-directory: verification/proofs/tlaplus
        run: |
          java -XX:+UseParallelGC \
            -cp "$HOME/.local/share/tla2tools.jar" tlc2.TLC \
            -workers auto -config KinGate.cfg KinGate.tla \
            | tee tlc.log
          # Fail if TLC printed an error or didn't declare completion.
          if grep -q "Error:" tlc.log; then
            echo "::error::TLC found an invariant / property violation"
            exit 1
          fi
          if ! grep -q "Model checking completed. No error has been found." tlc.log; then
            echo "::error::TLC did not report clean completion"
            exit 1
          fi

      - name: Upload TLC log on failure
        if: failure()
        uses: actions/upload-artifact@v7.0.1
        with:
          name: tlc-log
          path: verification/proofs/tlaplus/tlc.log
          retention-days: 14