proof.yml

# =============================================================================
# LadybugDB — Integration Proof Suite
# =============================================================================
# Runs the mathematical proof tests that verify ladybug-rs architectural
# claims against the published literature (Berry-Esseen, NARS, Pearl, etc.)
#
# Four test suites:
#   proof_foundation       — 13 proofs (F-1 through F-7c)
#   proof_reasoning_ladder — 8 proofs  (RL-1 through RL-8)
#   proof_tactics          — 12 proofs (T-01 through T-34)
#   proof_level_a_gaps     — 6 proofs  (A.1.4 through A.6.2)
#
# Total: 39 proofs verifying cognitive substrate invariants.
#
# Rust version: pinned to 1.93.0 to match Dockerfile build environment.
# RUSTFLAGS: -D warnings with targeted -A for noise lints in evolving codebase.
# =============================================================================

name: Proof Suite

on:
  push:
    branches: [main]
    paths:
      - 'src/**'
      - 'tests/proof_*.rs'
      - 'Cargo.toml'
      - 'Cargo.lock'
      - '.github/workflows/proof.yml'
  pull_request:
    branches: [main]
    paths:
      - 'src/**'
      - 'tests/proof_*.rs'
      - 'Cargo.toml'
      - 'Cargo.lock'
  workflow_dispatch:

env:
  CARGO_TERM_COLOR: always
  # Allow specific lints that are noise in a 115K-line evolving codebase.
  # Actual logic errors still fail. Remove allows as cleanup progresses.
  # Categories: unused-* (imports, vars, mut, assignments, parens),
  # edition 2024 (unsafe-op-in-unsafe-fn, mismatched-lifetime-syntaxes),
  # visibility (private-interfaces), and minor (dead-code, unexpected-cfgs,
  # ambiguous-glob-reexports, overlapping-range-endpoints, confusable-idents).
  RUSTFLAGS: "-D warnings -A unused -A dead-code -A private-interfaces -A mismatched-lifetime-syntaxes -A unsafe-op-in-unsafe-fn -A unexpected-cfgs -A ambiguous-glob-reexports -A overlapping-range-endpoints -A confusable-idents"

jobs:
  # ---------------------------------------------------------------------------
  # Quick check: does it compile at all?
  # ---------------------------------------------------------------------------
  compile-check:
    name: Compile Check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: cargo check
        run: cargo check --lib --tests

  # ---------------------------------------------------------------------------
  # Foundation Proofs (Berry-Esseen, XOR algebra, NARS truth values)
  # ---------------------------------------------------------------------------
  proof-foundation:
    name: Foundation Proofs (F-1 through F-7)
    needs: compile-check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: Run foundation proofs
        run: cargo test --test proof_foundation -- --test-threads=1 --show-output

  # ---------------------------------------------------------------------------
  # Reasoning Ladder Proofs (Sun et al. 2025 tier verification)
  # ---------------------------------------------------------------------------
  proof-reasoning-ladder:
    name: Reasoning Ladder Proofs (RL-1 through RL-8)
    needs: compile-check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: Run reasoning ladder proofs
        run: cargo test --test proof_reasoning_ladder -- --test-threads=1 --show-output

  # ---------------------------------------------------------------------------
  # Tactics Proofs (34 cognitive tactics structural verification)
  # ---------------------------------------------------------------------------
  proof-tactics:
    name: Tactics Proofs (T-01 through T-34)
    needs: compile-check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: Run tactics proofs
        run: cargo test --test proof_tactics -- --test-threads=1 --show-output

  # ---------------------------------------------------------------------------
  # Level A Gap Proofs (hardening / race condition coverage)
  # ---------------------------------------------------------------------------
  proof-level-a-gaps:
    name: Level A Gap Proofs (A.1.4 through A.6.2)
    needs: compile-check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: Run level A gap proofs
        run: cargo test --test proof_level_a_gaps -- --test-threads=1

  # ---------------------------------------------------------------------------
  # Full unit test suite (all 884 #[test] in src/)
  # ---------------------------------------------------------------------------
  unit-tests:
    name: Unit Tests (all modules)
    needs: compile-check
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: dtolnay/rust-toolchain@master
        with:
          toolchain: "1.93.0"
      - uses: Swatinem/rust-cache@v2
      - name: Run all unit tests
        run: cargo test --lib -- --test-threads=4

  # ---------------------------------------------------------------------------
  # Summary
  # ---------------------------------------------------------------------------
  proof-summary:
    name: Proof Summary
    needs: [compile-check, proof-foundation, proof-reasoning-ladder, proof-tactics, proof-level-a-gaps, unit-tests]
    runs-on: ubuntu-latest
    if: always()
    steps:
      - name: Check results
        run: |
          echo "============================================"
          echo "  LADYBUG-RS PROOF SUITE RESULTS"
          echo "============================================"
          echo ""
          echo "  Compile:          ${{ needs.compile-check.result }}"
          echo "  Foundation:       ${{ needs.proof-foundation.result }}"
          echo "  Reasoning Ladder: ${{ needs.proof-reasoning-ladder.result }}"
          echo "  Tactics:          ${{ needs.proof-tactics.result }}"
          echo "  Level A Gaps:     ${{ needs.proof-level-a-gaps.result }}"
          echo "  Unit Tests:       ${{ needs.unit-tests.result }}"
          echo ""
          PASS=true
          for result in \
            "${{ needs.compile-check.result }}" \
            "${{ needs.proof-foundation.result }}" \
            "${{ needs.proof-reasoning-ladder.result }}" \
            "${{ needs.proof-tactics.result }}" \
            "${{ needs.proof-level-a-gaps.result }}" \
            "${{ needs.unit-tests.result }}"; do
            if [ "$result" != "success" ]; then
              PASS=false
            fi
          done
          if [ "$PASS" = true ]; then
            echo "  ✅ ALL PROOF SUITES PASSED"
          else
            echo "  ❌ SOME PROOF SUITES FAILED"
            exit 1
          fi
          echo "============================================"