docs(planning): category-leadership programme — beyond completion #139
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: MPL-2.0 | |
| # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | |
| # | |
| # Backend-Assurance Harness (epic #87 Tier C) | |
| # | |
| # Runs the BEAM-native property tests that validate the backend | |
| # operations underlying the 5 class-(J) believe_me axioms in | |
| # src/abi/Boj/SafetyLemmas.idr. See docs/backend-assurance/ and | |
| # PROOF-NEEDS.md for the campaign framing. | |
| # | |
| # This is *external* evidence — it does not change the in-language | |
| # proof; the believe_me sites stay in source. The harness shrinks the | |
| # trusted base from "we trust the backend" to "we read the lowering and | |
| # randomly tested the operation". | |
| # | |
| # Triggers only on changes that could affect the harness or the | |
| # proof contract it backs. | |
| name: Backend-Assurance Harness | |
| # Was workflow-level path-filtered: a required check that never ran on PRs | |
| # touching none of its paths, leaving the check "Expected" and the PR blocked. | |
| # Now always runs; the `changes` job gates the heavy job, which when skipped | |
| # reports SUCCESS to required checks. | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| workflow_dispatch: | |
| concurrency: | |
| group: backend-assurance-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: ${{ github.event_name == 'pull_request' }} | |
| permissions: | |
| contents: read | |
| jobs: | |
| changes: | |
| name: Detect relevant changes | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 5 | |
| outputs: | |
| run: ${{ steps.detect.outputs.run }} | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| with: | |
| fetch-depth: 0 | |
| - id: detect | |
| env: | |
| EVENT: ${{ github.event_name }} | |
| BASE: ${{ github.base_ref }} | |
| BEFORE: ${{ github.event.before }} | |
| run: | | |
| set -uo pipefail | |
| run=true | |
| if [ "$EVENT" = pull_request ]; then | |
| git fetch --no-tags --depth=200 origin "$BASE" 2>/dev/null \ | |
| && changed=$(git diff --name-only "origin/${BASE}...HEAD" 2>/dev/null) \ | |
| && { printf '%s\n' "$changed" | grep -qE '^src/abi/Boj/SafetyLemmas\.idr$|^elixir/test/backend_assurance/|^elixir/mix\.(exs|lock)$|^docs/backend-assurance/' && run=true || run=false; } | |
| elif [ "$EVENT" = push ] && [ -n "$BEFORE" ] && [ "$BEFORE" != 0000000000000000000000000000000000000000 ]; then | |
| changed=$(git diff --name-only "${BEFORE}...${GITHUB_SHA}" 2>/dev/null) \ | |
| && { printf '%s\n' "$changed" | grep -qE '^src/abi/Boj/SafetyLemmas\.idr$|^elixir/test/backend_assurance/|^elixir/mix\.(exs|lock)$|^docs/backend-assurance/' && run=true || run=false; } | |
| fi | |
| printf 'run=%s\n' "$run" >> "$GITHUB_OUTPUT" | |
| echo "relevant=$run; changed files:"; printf '%s\n' "${changed:-<none computed>}" | |
| property-test: | |
| name: BEAM property tests | |
| needs: changes | |
| if: needs.changes.outputs.run == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 10 | |
| defaults: | |
| run: | |
| working-directory: elixir | |
| steps: | |
| - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 | |
| - name: Set up BEAM (Elixir + OTP) | |
| uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.24.0 | |
| with: | |
| elixir-version: '1.18.4' | |
| otp-version: '27.0' | |
| - name: Cache deps + _build | |
| uses: actions/cache@d4323d4df104b026a6aa633fdb11d772146be0bf # v4.2.2 | |
| with: | |
| path: | | |
| elixir/deps | |
| elixir/_build | |
| key: backend-assurance-${{ runner.os }}-${{ hashFiles('elixir/mix.lock') }} | |
| restore-keys: | | |
| backend-assurance-${{ runner.os }}- | |
| - name: Fetch deps | |
| run: mix deps.get | |
| - name: Compile | |
| run: mix compile --warnings-as-errors | |
| - name: Run backend-assurance property tests | |
| run: mix test --only backend_assurance --color |