Repository navigation
fix(boundary): isolate unsafe Rust under ffi/rust; forbid it in src/ (#49) #223
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> | |
| # | |
| # proof-corpus.yml — Machine-checks the VclTotal Idris2 proof corpus. | |
| # | |
| # vcl-ut is the doubly-trusted hypatia<->verisim interface. This gate | |
| # fails the build if the corpus (ABI.{Types, Layout, LayoutProofs} + Core.* | |
| # + Interface.Wire*, 12 modules) stops typechecking under idris2 0.8.0, or | |
| # if a proof-escape symbol is introduced. Tracked: hyperpolymath/standards#124. | |
| # | |
| # Scope note: VclTotal.ABI.Layout is now sound and IS in | |
| # verification/proofs/vclut-core.ipkg (LayoutProofs discharges its | |
| # theorems). Only the Foreign bindings (module Foreign, VclTotal.Legacy. | |
| # Foreign) remain excluded — see verification/proofs/VERIFICATION-STANCE.adoc. | |
| name: Proof Corpus | |
| on: | |
| pull_request: | |
| branches: ['**'] | |
| push: | |
| branches: [main, master] | |
| permissions: | |
| contents: read | |
| # Concurrency-cancel guard (repo convention for canonical check workflows). | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| machine-check: | |
| name: idris2 0.8.0 --build vclut-core | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| # Idris2 0.8.0 is built from PINNED official source. The former | |
| # `idris-community/setup-idris` action's repository no longer | |
| # resolves (404), and no maintained equivalent exists; a | |
| # SHA-pinned source build is deterministic, version-exact, and | |
| # depends on no third-party action (matches the repo's pin | |
| # posture). `idris-lang/Idris2` tag v0.8.0 == commit | |
| # 15a3e4e70843f7a34100f6470c04b791330788df. | |
| - name: Build & install Idris2 0.8.0 from pinned source | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update -qq | |
| sudo apt-get install -y --no-install-recommends chezscheme make gcc | |
| git clone --no-checkout https://github.com/idris-lang/Idris2.git /tmp/Idris2 | |
| git -C /tmp/Idris2 checkout 15a3e4e70843f7a34100f6470c04b791330788df | |
| make -C /tmp/Idris2 bootstrap SCHEME=chezscheme | |
| make -C /tmp/Idris2 install PREFIX="$HOME/.idris2" | |
| echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" | |
| echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV" | |
| - name: Proof-escape audit (honesty guard) | |
| run: | | |
| set -euo pipefail | |
| # Robust, comment-aware scan (line --, doc |||, nested {- -}, and | |
| # string-literal-aware): scripts/honesty-guard.sh. Scoped to the | |
| # Phase-1 corpus sources — the same module set vclut-core.ipkg builds | |
| # below. Exits 1 on any believe_me / really_believe_me / postulate / | |
| # assert_total / assert_smaller / idris_crash / sorry / ?hole / | |
| # partial appearing outside a comment. | |
| sh scripts/honesty-guard.sh \ | |
| src/core/Grammar.idr src/core/Schema.idr src/core/Decide.idr \ | |
| src/core/Levels.idr src/core/Checker.idr \ | |
| src/core/Composition.idr src/core/Epistemic.idr \ | |
| src/core/Transition.idr \ | |
| src/interface/abi/Types.idr src/interface/abi/Layout.idr \ | |
| src/interface/abi/LayoutProofs.idr \ | |
| src/interface/WireDecode.idr src/interface/WireConformance.idr | |
| - name: Build the proof corpus | |
| run: | | |
| set -euo pipefail | |
| idris2 --version | |
| idris2 --build verification/proofs/vclut-core.ipkg | |
| - name: Build the self-contained L4 model (Phase 0) | |
| # `module SafetyL4Model` must be checked from its own directory so | |
| # the module name matches the file path. | |
| run: | | |
| set -euo pipefail | |
| cd verification/proofs && idris2 --check SafetyL4Model.idr |