diff --git a/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml new file mode 100644 index 00000000..062af9c0 --- /dev/null +++ b/.github/workflows/checkerboard-alln-proofplaygrond-audit.yml @@ -0,0 +1,91 @@ +# Copyright 2026 Dominic Dabish +# Licensed under the Apache License, Version 2.0. +# Focused 6×6 production-module audit for source commit 913adfd724cbedd5c47b52a2c538a94a7c7cf785. + +name: Checkerboard all-n ProofPlaygrond audit + +on: + pull_request: + branches: [main] + paths: + - '.github/workflows/checkerboard-alln-proofplaygrond-audit.yml' + - 'audits/checkerboard-alln-proofplaygrond.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + audit: + runs-on: ubuntu-latest + timeout-minutes: 120 + steps: + - name: Checkout exact checkerboard certificate source + uses: actions/checkout@v6 + with: + repository: DomTheDeveloper/ProofPlaygrond + ref: 913adfd724cbedd5c47b52a2c538a94a7c7cf785 + fetch-depth: 1 + + - name: Record exact commit + run: git rev-parse HEAD | tee "$RUNNER_TEMP/resolved-sha.txt" + + - name: Install repository-pinned Lean + run: | + set -euo pipefail + curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ + | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + + - name: Resolve pinned Mathlib and cache + run: | + set -euo pipefail + "$HOME/.elan/bin/lake" update + "$HOME/.elan/bin/lake" exe cache get + + - name: Reject proof holes and trust shortcuts + run: | + set -euo pipefail + files=(Checkerboard/N6SATTest.lean Checkerboard/N6Explicit.lean) + if grep -nE '\b(sorry|admit|native_decide|unsafe)\b|(^|[^A-Za-z])axiom([^A-Za-z]|$)|bv_decide|bv_check|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "${files[@]}"; then + echo 'Forbidden placeholder or trust shortcut found in checkerboard certificate.' >&2 + exit 1 + fi + + - name: Build production 6x6 proof + run: | + set -o pipefail + "$HOME/.elan/bin/lake" build Checkerboard.N6Explicit \ + 2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-build.log" + + - name: Print public base-case axioms + run: | + set -euo pipefail + cat > "$RUNNER_TEMP/CheckerboardN6AxiomAudit.lean" <<'EOF' + import Checkerboard.N6Explicit + #print axioms Checkerboard.n6_zero_upper + #print axioms Checkerboard.n6_one_upper + EOF + set -o pipefail + "$HOME/.elan/bin/lake" env lean "$RUNNER_TEMP/CheckerboardN6AxiomAudit.lean" \ + 2>&1 | tee "$RUNNER_TEMP/checkerboard-n6-axioms.log" + + - name: Enforce axiom policy + run: | + set -euo pipefail + cat "$RUNNER_TEMP/checkerboard-n6-build.log" "$RUNNER_TEMP/checkerboard-n6-axioms.log" > "$RUNNER_TEMP/checkerboard-n6-all.log" + if grep -E 'sorryAx|_native\.bv_decide|Lean\.(trustCompiler|ofReduce|ofReduceBool)' "$RUNNER_TEMP/checkerboard-n6-all.log"; then + echo 'Forbidden axiom or compiler-trust dependency detected.' >&2 + exit 1 + fi + + - name: Upload certificate transcripts + if: ${{ always() }} + uses: actions/upload-artifact@v4 + with: + name: checkerboard-n6-certificate-${{ github.run_id }} + path: | + ${{ runner.temp }}/resolved-sha.txt + ${{ runner.temp }}/checkerboard-n6-build.log + ${{ runner.temp }}/checkerboard-n6-axioms.log + if-no-files-found: warn