tooling: route forge/src/degrade.rs -> degrade-ladder.md (#10) #25
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
| name: ci | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| # The full gauntlet (REQ-5). Each command is a separate, must-pass step: | |
| # a non-zero exit fails CI (R-DEFER-6 — verification is a hard gate). The | |
| # installer is pinned to the SAME version as rust-toolchain.toml (1.95.0) so | |
| # CI runs on exactly the pinned toolchain (R-CODE-5 / design §5.3 determinism); | |
| # rustup also honors rust-toolchain.toml for the cargo invocations below. | |
| # The skill-budget gate (issue #7, REQ-7) runs the `--check-budget` step below: | |
| # `cargo run -p thermite-skill -- --check-budget` fails CI if the generated | |
| # THERMITE.skill.md exceeds the 6,000-token budget (design §2.2 / §10). | |
| # | |
| # Verus is installed below so the L3 verification gate (thermite-lower's | |
| # verus-on-emitted tests) ACTUALLY RUNS in CI, not just locally (R-DEFER-6 — | |
| # verification is a hard gate). The pinned verus 0.2026.05.24.ecee80a bundles | |
| # the matching rust toolchain (1.95.0) + z3. The tests resolve verus via the | |
| # VERUS_BIN env / PATH and skip loudly only if it is genuinely absent. | |
| jobs: | |
| gauntlet: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v4 | |
| - name: Install toolchain (pinned to rust-toolchain.toml channel) | |
| uses: dtolnay/rust-toolchain@1.95.0 | |
| with: | |
| components: rustfmt, clippy | |
| - name: Install Verus (L3 verification gate — pinned to dev version) | |
| run: | | |
| set -euo pipefail | |
| VERUS_VER="0.2026.05.24.ecee80a" | |
| # Asset name is verus-<VER>-x86-linux.zip; the tag path uses a literal | |
| # slash (release/<VER>), NOT %2F (verified against the releases API). | |
| curl -fsSL -o /tmp/verus.zip \ | |
| "https://github.com/verus-lang/verus/releases/download/release/${VERUS_VER}/verus-${VERUS_VER}-x86-linux.zip" | |
| mkdir -p "$HOME/verus-dist" | |
| unzip -q /tmp/verus.zip -d "$HOME/verus-dist" | |
| # Locate the verus binary regardless of the zip's internal dir name. | |
| VERUS_BIN_PATH="$(find "$HOME/verus-dist" -type f -name verus | head -1)" | |
| test -n "$VERUS_BIN_PATH" | |
| echo "VERUS_BIN=$VERUS_BIN_PATH" >> "$GITHUB_ENV" | |
| echo "$(dirname "$VERUS_BIN_PATH")" >> "$GITHUB_PATH" | |
| "$VERUS_BIN_PATH" --version | |
| - name: cargo build | |
| run: cargo build --workspace | |
| - name: cargo test | |
| run: cargo test --workspace | |
| - name: cargo clippy | |
| run: cargo clippy --workspace --all-targets -- -D warnings | |
| - name: cargo fmt | |
| run: cargo fmt --all --check | |
| - name: skill budget gate (issue #7, design §2.2 / §10) | |
| run: cargo run -p thermite-skill -- --check-budget |