refactor: migrate Markdown to AsciiDoc (#366) #34
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: AGPL-3.0-or-later | |
| # This workflow is managed by gh actions-lock. | |
| # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | |
| # | |
| # formal-verification.yml — Creusot formal verification of the trust-pipeline kernel. | |
| # | |
| # Stage 8c of the ECHIDNA ROADMAP. Both jobs are merge gates as of Stage 8c-M3. | |
| # | |
| # stable-tests — `cargo test -p echidna-core-spark` on stable Rust. | |
| # Exercises every proof obligation as a `#[test]` function. | |
| # Fast (~10 s); always passes on a correct Rust installation. | |
| # | |
| # creusot-verify — `cargo +nightly creusot` with Why3 + Z3 discharge. | |
| # Hard gate as of Stage 8c-M3. Requires Why3 in the runner; | |
| # `apt-get install why3` covers Ubuntu 22.04+. | |
| # If Why3 availability changes, re-evaluate whether to keep | |
| # this as a required check or move to a scheduled/manual job. | |
| # | |
| # See crates/echidna-core-spark/CREUSOT-SETUP.md for local setup. | |
| name: Formal Verification (Stage 8c) | |
| on: | |
| pull_request: | |
| paths: | |
| - 'crates/echidna-core-spark/**' | |
| - '.github/workflows/formal-verification.yml' | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'crates/echidna-core-spark/**' | |
| # Cause-B mitigation (#77): cancel superseded runs so stacked pushes | |
| # to the same ref don't pile up identical jobs in the queue. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| # ── Job 1: invariant tests on stable Rust ──────────────────────────────── | |
| stable-tests: | |
| name: Trust-pipeline invariant tests (stable) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v7.0.1 | |
| - name: Install stable Rust toolchain | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| toolchain: stable | |
| - name: Cache Rust build artefacts | |
| uses: Swatinem/rust-cache@v2.9.2 | |
| with: | |
| workspaces: ". -> target" | |
| - name: Run trust-pipeline invariant tests | |
| run: cargo test -p echidna-core-spark --verbose | |
| env: | |
| RUST_BACKTRACE: 1 | |
| # ── Job 2: Creusot formal verification (hard gate — Stage 8c-M3) ───────── | |
| creusot-verify: | |
| name: Creusot formal verification | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| # No continue-on-error — this is a hard merge gate as of Stage 8c-M3. | |
| # The outer-loop invariant for compute is now live; all obligations | |
| # (PO-1..P8, PO-A1..A12) must discharge under Why3+Z3. | |
| # | |
| # If this job becomes flaky due to nightly drift, update the pin in | |
| # rust-toolchain.toml and the `toolchain:` field below together. | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v7.0.1 | |
| - name: Install nightly Rust toolchain (Creusot pin) | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| # Pin matches crates/echidna-core-spark/rust-toolchain.toml. | |
| # Update both files together when bumping. | |
| toolchain: nightly-2024-05-01 | |
| components: rustc, cargo, rust-src | |
| - name: Install Why3 and SMT solvers | |
| run: | | |
| set -euo pipefail | |
| sudo apt-get update -qq | |
| sudo apt-get install -y --no-install-recommends why3 z3 | |
| # alt-ergo has no installation candidate in the Ubuntu 24.04 | |
| # (noble) apt repos (#250). Install the prebuilt musl static | |
| # binary pinned from OCamlPro's GitHub releases instead — same | |
| # provisioning pattern as live-provers.yml. | |
| curl -sSL --max-time 120 -o /tmp/alt-ergo \ | |
| https://github.com/OCamlPro/alt-ergo/releases/download/v2.6.3/alt-ergo-v2.6.3-x86_64-linux-musl | |
| sudo install -m 0755 /tmp/alt-ergo /usr/local/bin/alt-ergo | |
| # why3 + z3 cover all current obligations. alt-ergo is included | |
| # as a fallback solver for obligations z3 times out on. | |
| - name: Verify Why3 installation | |
| run: | | |
| why3 --version | |
| z3 --version | |
| alt-ergo --version | |
| why3 config detect | |
| - name: Install Creusot | |
| run: cargo +nightly-2024-05-01 install creusot | |
| # Hard failure: if the nightly drifts from what Creusot supports, | |
| # this step will fail and the PR is blocked. Fix: bump the pin. | |
| - name: Run Creusot verification | |
| run: | | |
| cargo +nightly-2024-05-01 creusot \ | |
| -p echidna-core-spark \ | |
| -- \ | |
| --features creusot \ | |
| --why3 "$(which why3)" | |
| # All obligations must be Valid. Unknown/Timeout indicates either | |
| # a contract error or a solver timeout (raise --timeout if needed). | |
| # Invalid means the contract is wrong — check the Why3 obligation. |