ubt 0.4.2

name: Proof Verification

on:
  push:
    branches: [main, master]
    paths:
      - 'formal/**'
      - '.github/workflows/proofs.yml'
  pull_request:
    branches: [main, master]
    paths:
      - 'formal/**'
      - '.github/workflows/proofs.yml'
  workflow_dispatch:

jobs:
  verify-proofs:
    runs-on: ubuntu-latest
    
    env:
      OPAMYES: 1
      OPAMJOBS: 2
    
    steps:
      - name: Checkout repository
        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4

      # NOTE: Linking layer requires RocqOfRust library
      # RocqOfRust requires cloning and building from https://github.com/formal-land/rocq-of-rust
      # The linking layer can be verified locally with: make linking
      # For CI, we skip linking to avoid the long RocqOfRust build time

      - name: Install opam
        run: |
          sudo apt-get update
          sudo apt-get install -y opam

      - name: Cache opam
        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
        id: cache-opam
        with:
          path: ~/.opam
          key: opam-rocq9-${{ runner.os }}-v2-${{ hashFiles('formal/Makefile') }}
          restore-keys: |
            opam-rocq9-${{ runner.os }}-v1-

      - name: Initialize opam
        if: steps.cache-opam.outputs.cache-hit != 'true'
        run: |
          opam init --bare --disable-sandboxing

      - name: Create Rocq switch
        if: steps.cache-opam.outputs.cache-hit != 'true'
        run: |
          # Create switch with OCaml 4.14.2 (or use existing)
          opam switch create rocq-9 ocaml-base-compiler.4.14.2 || opam switch rocq-9
          eval "$(opam env --switch=rocq-9)"
          
          # Add Rocq released repo (contains rocq-prover 9.0.0)
          opam repo add rocq-released https://rocq-prover.org/opam/released --set-default || true
          # Add Coq released repo (contains coq-quickchick)
          opam repo add coq-released https://coq.inria.fr/opam/released || true
          opam update
          
          # Debug: show available packages
          opam search rocq-prover || true
          
          # Install Coq 9.0 (compatibility package that provides coqc binary)
          # rocq-prover alone doesn't provide coqc, we need the coq compat package
          opam pin add coq 9.0.0 -y || opam install coq -y
          
          # Verify installation
          eval "$(opam env --switch=rocq-9)"
          echo "PATH=$PATH"
          ls -la ~/.opam/rocq-9/bin/ | grep -E "coq|rocq" || true
          coqc --version

      - name: Build core proofs (without QuickChick)
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          coqc --version
          make clean
          # Build specs, simulations, and core proofs (skip quickchick_tests.v)
          make specs
          make simulations
          make proofs-core

      - name: Install QuickChick
        run: |
          eval "$(opam env --switch=rocq-9)"
          # Add coq-released repo (contains coq-quickchick)
          opam repo add coq-released https://coq.inria.fr/opam/released --set-default 2>/dev/null || true
          opam update --quiet || true
          opam install coq-quickchick -y

      - name: Run QuickChick tests (CI - reduced count)
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          # Use quickchick-ci target: 1000 tests/property (5000 total)
          # Full tests (10000/property) can be run locally with `make quickchick`
          make quickchick-ci

      - name: OCaml extraction verification
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          make extract
          # Verify extracted files exist and have content
          if [ ! -f extraction/extracted.ml ]; then
            echo "::error::OCaml extraction failed - extracted.ml not generated"
            exit 1
          fi
          if [ ! -s extraction/extracted.ml ]; then
            echo "::error::OCaml extraction failed - extracted.ml is empty"
            exit 1
          fi
          echo "Extracted OCaml file size: $(wc -c < extraction/extracted.ml) bytes"

      - name: Documentation generation check
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          make docs || true  # Don't fail on doc generation issues
          # Verify docs were generated
          if [ ! -d docs/html ] || [ -z "$(ls -A docs/html 2>/dev/null)" ]; then
            echo "::warning::Documentation generation produced no output"
          else
            echo "Generated $(find docs/html -name '*.html' | wc -l) HTML files"
          fi

      - name: Generate audit report
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          make audit

      - name: Verify axiom count
        working-directory: formal
        run: |
          eval "$(opam env --switch=rocq-9)"
          make verify-axioms

      - name: Check admit threshold
        working-directory: formal
        run: |
          # Set threshold - allows for Admitted theorems in generated code (src/)
          # Note: This checks for 'Admitted.' theorems, not 'admit.' tactics
          # See formal/docs/ADMITS_TRACKING.md for detailed breakdown
          make check-admits ADMIT_THRESHOLD=100

      - name: Upload audit report
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
        with:
          name: proof-audit
          path: formal/audit-report.txt
          retention-days: 30

      - name: Upload extracted OCaml
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
        with:
          name: extracted-ocaml
          path: |
            formal/extraction/extracted.ml
            formal/extraction/extracted.mli
          retention-days: 30

      - name: Upload documentation
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
        if: always()
        continue-on-error: true
        with:
          name: coqdoc-html
          path: formal/docs/html/
          retention-days: 30

      - name: Build Summary
        run: |
          echo "## Proof Verification Summary" >> $GITHUB_STEP_SUMMARY
          echo "" >> $GITHUB_STEP_SUMMARY
          echo "| Check | Status |" >> $GITHUB_STEP_SUMMARY
          echo "|-------|--------|" >> $GITHUB_STEP_SUMMARY
          echo "| Core Proofs | ✅ |" >> $GITHUB_STEP_SUMMARY
          echo "| QuickChick Tests | ✅ |" >> $GITHUB_STEP_SUMMARY
          echo "| Linking Layer | ⏭️ Skipped (requires RocqOfRust) |" >> $GITHUB_STEP_SUMMARY
          echo "| OCaml Extraction | ✅ |" >> $GITHUB_STEP_SUMMARY
          echo "| Documentation | ✅ |" >> $GITHUB_STEP_SUMMARY
          echo "" >> $GITHUB_STEP_SUMMARY
          echo "### Audit Report" >> $GITHUB_STEP_SUMMARY
          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
          tail -20 formal/audit-report.txt >> $GITHUB_STEP_SUMMARY
          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY