generated-tv #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: generated-tv | |
| # The rotating-seed off-corpus translation-validation job (thermite2-program.md | |
| # REQ-2c / AC-4). `forge tv --generated` discharges the per-clause production-vs- | |
| # reference equivalence obligation over a deterministically GENERATED clause space | |
| # — the off-corpus escape hatch that catches lowering divergences the fixed | |
| # conformance corpus never exercises. The main `ci` gate runs this space at the | |
| # pinned `TV_DEFAULT_SEED` (reproducible); this scheduled job runs it with a | |
| # ROTATING seed (`github.run_number`), so each run walks a different slice of the | |
| # clause space and a seed-dependent divergence eventually surfaces as a red build. | |
| # A DIVERGENT clause exits non-zero (forge's verification-failure exit) and fails | |
| # the job — exactly the signal we want a scheduled lowering-fidelity watchdog to | |
| # raise. (Unverifiable/Skipped never fail the exit — R-HONEST-3.) | |
| on: | |
| schedule: | |
| # Daily at 07:13 UTC (off the hour to dodge the cron stampede). Each run's | |
| # github.run_number is monotonic, so the seed rotates every day. | |
| - cron: '13 7 * * *' | |
| # Manual trigger for on-demand runs (e.g. validating this workflow itself). | |
| workflow_dispatch: | |
| inputs: | |
| seed: | |
| description: 'Override the rotating seed (default: github.run_number)' | |
| required: false | |
| type: string | |
| count: | |
| description: 'Number of generated clauses (default: 200)' | |
| required: false | |
| type: string | |
| jobs: | |
| generated-tv: | |
| 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 | |
| - name: Rust build cache | |
| uses: Swatinem/rust-cache@v2 | |
| with: | |
| key: generated-tv | |
| - name: Cache Verus | |
| uses: actions/cache@v4 | |
| with: | |
| path: ~/verus-dist | |
| key: verus-0.2026.05.24.ecee80a-x86-linux | |
| - name: Install Verus (L3 verification gate — pinned to dev version) | |
| run: | | |
| set -euo pipefail | |
| VERUS_VER="0.2026.05.24.ecee80a" | |
| if ! find "$HOME/verus-dist" -type f -name verus 2>/dev/null | grep -q .; then | |
| 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" | |
| fi | |
| 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: Install elan (Lean toolchain manager) | |
| # The stratified classifier differential battery (REQ-9 check [8]) holds the Rust | |
| # classifier byte-equal to the Lean kernel `admitted` via `lake env lean --run`, so | |
| # the rotating-seed strat-TV needs lake. (The contract-TV step above does not.) | |
| run: | | |
| set -euo pipefail | |
| curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh | |
| bash /tmp/elan-init.sh -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| - name: Cache Lean build (.lake) | |
| uses: actions/cache@v4 | |
| with: | |
| path: | | |
| lean/.lake/packages | |
| lean/.lake/build | |
| key: lean-${{ hashFiles('lean/lake-manifest.json', 'lean/lean-toolchain') }} | |
| restore-keys: | | |
| lean- | |
| - name: Fetch prebuilt Mathlib cache (oleans) | |
| working-directory: lean | |
| run: lake exe cache get | |
| - name: Build the stratified Wire module (the strat-TV Lean driver) | |
| working-directory: lean | |
| run: lake build Thermite.Strat.Cls.Wire | |
| - name: Build forge | |
| run: cargo build -p forge --release | |
| - name: Rotating-seed generated translation-validation | |
| # Seed rotates with the run number (or the manual override); the corpus | |
| # phase rides a representative conformance file. A DIVERGENT clause fails | |
| # the exit and the job — the watchdog signal. | |
| run: | | |
| set -euo pipefail | |
| SEED="${{ github.event.inputs.seed || github.run_number }}" | |
| COUNT="${{ github.event.inputs.count || '200' }}" | |
| echo "::notice::generated TV — seed=$SEED count=$COUNT" | |
| ./target/release/forge tv conformance/binary_search.th \ | |
| --generated "$COUNT" --seed "$SEED" | |
| - name: Rotating-seed stratified classifier differential + two-phase sweep ([8] / [9]) | |
| # REQ-9 check [8]'s rotating-seed half: each scheduled run walks a different slice | |
| # of the well-sorted formula space, holding the Rust admission classifier | |
| # byte-equal to the Lean kernel `Thermite.Strat.Cls.admitted` (`forge strat-tv`), | |
| # plus the two-phase TV sweep over a rotating stratified clause stream | |
| # (`forge strat-faithful-tv`). A classifier disagreement / unknown-on-admitted | |
| # tripwire, or a divergence / withheld clause, exits non-zero and fails the job — | |
| # the seed-dependent admission/lowering-fidelity watchdog (REQ-4 / REQ-8 / AC-9). | |
| run: | | |
| set -euo pipefail | |
| SEED="${{ github.event.inputs.seed || github.run_number }}" | |
| COUNT="${{ github.event.inputs.count || '200' }}" | |
| echo "::notice::strat-TV — seed=$SEED count=$COUNT" | |
| ./target/release/forge strat-tv --generated "$COUNT" --seed "$SEED" | |
| ./target/release/forge strat-faithful-tv --generated "$COUNT" --seed "$SEED" |