|
| 1 | +# SPDX-License-Identifier: MPL-2.0 |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# Proofs Gate — type-check the Idris2 contract layer (src/abi/) and enforce |
| 5 | +# the empty trusted base (no believe_me / postulate / assert_total). |
| 6 | +# |
| 7 | +# FeedbackOTron.Contract is the verified CONTRACT SPEC for the Elixir |
| 8 | +# FormValidator (see ABI-FFI-README.md). This gate keeps it honestly |
| 9 | +# compiling: every push/PR touching src/abi/** re-checks the package under |
| 10 | +# a pinned Idris2 toolchain (same asdf+Chez install pattern as boj-server's |
| 11 | +# proofs gate). |
| 12 | +# |
| 13 | +# NOTE: this workflow is path-filtered because it is NOT a required status |
| 14 | +# check. If it is ever promoted to required, the `on.*.paths` filters MUST |
| 15 | +# be removed and replaced with an always-run `changes` detector job (see |
| 16 | +# boj-server .github/workflows/proofs.yml and the estate CI conventions: |
| 17 | +# a path-filtered required check that never triggers reports as permanently |
| 18 | +# "Expected" and deadlocks the PR). |
| 19 | +name: Proofs Gate |
| 20 | + |
| 21 | +on: |
| 22 | + push: |
| 23 | + branches: [main] |
| 24 | + paths: |
| 25 | + - 'src/abi/**' |
| 26 | + - '.github/workflows/proofs.yml' |
| 27 | + pull_request: |
| 28 | + branches: [main] |
| 29 | + paths: |
| 30 | + - 'src/abi/**' |
| 31 | + - '.github/workflows/proofs.yml' |
| 32 | + workflow_dispatch: |
| 33 | + |
| 34 | +permissions: |
| 35 | + contents: read |
| 36 | + |
| 37 | +concurrency: |
| 38 | + group: proofs-${{ github.ref }} |
| 39 | + cancel-in-progress: ${{ github.event_name == 'pull_request' }} |
| 40 | + |
| 41 | +env: |
| 42 | + IDRIS2_VERSION: '0.7.0' |
| 43 | + |
| 44 | +jobs: |
| 45 | + # Cheap, dependency-free gate: the contract layer claims an EMPTY trusted |
| 46 | + # base — no believe_me, no postulate, no assert_total anywhere in src/abi. |
| 47 | + trusted-base: |
| 48 | + name: Trusted-base audit (empty — no axioms) |
| 49 | + runs-on: ubuntu-latest |
| 50 | + timeout-minutes: 5 |
| 51 | + steps: |
| 52 | + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 |
| 53 | + - name: Enforce empty trusted base |
| 54 | + run: | |
| 55 | + set -euo pipefail |
| 56 | + found=0 |
| 57 | + while IFS= read -r -d '' f; do |
| 58 | + # Strip `--` and `|||` comments so documentation may mention the |
| 59 | + # banned constructs without tripping the audit. |
| 60 | + if sed -e 's/--.*$//' -e 's/|||.*$//' "$f" \ |
| 61 | + | grep -nE 'believe_me|postulate|assert_total'; then |
| 62 | + echo "::error file=$f::Unsound construct in $f — the contract layer must stay axiom-free." |
| 63 | + found=1 |
| 64 | + fi |
| 65 | + done < <(find src/abi -name '*.idr' -print0) |
| 66 | + if [ "$found" -eq 0 ]; then echo "Trusted base is empty."; fi |
| 67 | + exit "$found" |
| 68 | +
|
| 69 | + typecheck: |
| 70 | + name: Idris2 type-check (contract layer) |
| 71 | + runs-on: ubuntu-latest |
| 72 | + timeout-minutes: 45 |
| 73 | + steps: |
| 74 | + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 |
| 75 | + |
| 76 | + - name: Install build deps (Chez Scheme + GMP) |
| 77 | + run: sudo apt-get update && sudo apt-get install -y chezscheme libgmp-dev build-essential |
| 78 | + |
| 79 | + - name: Cache asdf + Idris2 toolchain |
| 80 | + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 |
| 81 | + with: |
| 82 | + path: ~/.asdf |
| 83 | + key: idris2-asdf-${{ runner.os }}-${{ env.IDRIS2_VERSION }} |
| 84 | + |
| 85 | + - name: Install asdf + Idris2 ${{ env.IDRIS2_VERSION }} |
| 86 | + env: |
| 87 | + # Ubuntu's chezscheme package installs the interpreter as `scheme`; |
| 88 | + # Idris2's bootstrap Makefile reads $SCHEME (defaults to `chez`). |
| 89 | + SCHEME: scheme |
| 90 | + run: | |
| 91 | + set -euo pipefail |
| 92 | + if [ ! -f "$HOME/.asdf/asdf.sh" ]; then |
| 93 | + git clone --depth 1 --branch v0.14.0 https://github.com/asdf-vm/asdf.git "$HOME/.asdf" |
| 94 | + fi |
| 95 | + . "$HOME/.asdf/asdf.sh" |
| 96 | + asdf plugin add idris2 || true |
| 97 | + asdf install idris2 "$IDRIS2_VERSION" |
| 98 | + asdf global idris2 "$IDRIS2_VERSION" |
| 99 | +
|
| 100 | + - name: Put Idris2 on PATH |
| 101 | + run: echo "$HOME/.asdf/shims" >> "$GITHUB_PATH" |
| 102 | + |
| 103 | + - name: Idris2 version |
| 104 | + run: idris2 --version |
| 105 | + |
| 106 | + - name: Type-check the contract package |
| 107 | + working-directory: src/abi |
| 108 | + run: idris2 --typecheck feedback-o-tron.ipkg |
0 commit comments