forjar 1.32.0

# Formal proofs — Kani bounded-model checking + Lean theorem proving.
#
# GH-242: before this workflow, no CI job invoked kani, lean or verus. 32 Kani
# harnesses and 7 Lean proofs sat in the tree, cited by name as evidence in
# contracts/*.yaml, and were never executed by anything.
#
# They were not merely unrun — they did not COMPILE. The first `cargo kani`
# invocation failed with two E0425 errors in kani_proofs.rs (`super::compute_order`
# for a function defined in that same module), so every harness in the crate was
# unbuildable while the contracts referencing them read as verified.
#
# One harness also ran past ten minutes without terminating, because it drove
# `DiskBudget::new` — which allocates Strings — across a 65,536-point input
# space. An intractable proof is indistinguishable from an absent one.
#
# So this gate exists to make "verified" mean the machine checked it.
name: Proofs

# WHEN this runs, and why not on every PR.
#
# Measured on intel 2026-08-17, while this workflow ran on a PR:
#
#   runners executing a job   15 / 16
#   ci.slice cap utilisation  17.99 of 18 cores  (pinned at 100% of quota)
#   cpu.pressure some avg10   40.67%             (full = 0.00 — not wedged)
#
# Judged by pressure and cap utilisation, NOT load average: under a CPUQuota
# throttled tasks stay runnable, so load reads high and means little. intel's
# own ci.slice unit says exactly that, and the first draft of this comment
# ignored it and quoted load 65.6.
#
# The kani job is bare-metal (no `container:`), so it draws from that same
# 18-core budget as every other job, and it holds one of 16 runner slots for
# the duration — 90 minutes under that contention, against ~36 minutes
# measured for the same work on an idle box. Every pull_request paid it.
#
# So: main stays proven post-merge, a nightly catches drift, and a PR that
# actually touches the harnesses opts in with the `proofs` label. This is a
# scheduling change, not a weakening — `proofs` is not a required context
# (the org ruleset requires `gate`), so it never gated a merge anyway.
on:
  push:
    branches: [main]
  schedule:
    - cron: '17 6 * * *'
  pull_request:
    types: [opened, synchronize, reopened, labeled]
  workflow_dispatch:

concurrency:
  group: proofs-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

permissions:
  contents: read

# forjar#447: every job of this workflow may land on the same self-hosted runner
# and, by default, the same _work checkout — so kani, lean and ledger-replay
# compiled in ONE target/release and raced on cargo's dep-info files
# (ENOENT on pmcp-*.d, two jobs red on one run, nothing in the diff). One build
# directory per job name, persistent per runner so the clean-room stays warm.
env:
  CARGO_TARGET_DIR: ${{ github.workspace }}/target-${{ github.job }}

jobs:
  # PMAT-237: ledger-replay builds the binary and replays every recorded
  # ledger defect — 34 minutes, the single most expensive job a PR pays for,
  # and it cannot be affected by a change that touches no code.
  classify:
    runs-on: [self-hosted, clean-room, X64]
    outputs:
      code: ${{ steps.class.outputs.code }}
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
        with:
          fetch-depth: 0
      - id: class
        uses: ./.github/actions/changed-class

  kani:
    name: kani
    # forjar#598 -- PINNED TO BARE METAL, AN INTERIM WITH A NAMED COUPLING.
    #
    # `[self-hosted, clean-room, X64]` matches the intel runners (bare metal,
    # tools present) AND the yoga-build* runners (EPHEMERAL containers --
    # yoga-build, -build2, -build3 all observed running these jobs on
    # 2026-09-20; lean + kani + rsync ABSENT by inventory). So this job was deterministic per runner and
    # a coin flip per run: on commit 537252d3 four runs went fail/pass/fail/pass
    # purely by which runner picked it up. A re-run landing on intel is a green
    # nobody can reconstruct.
    #
    # `intel` here is a HOSTNAME standing in for a CAPABILITY, which this repo
    # otherwise avoids (PMAT-547). Remove it when either lands: a capability
    # label (`provers` / `bare-metal`) declared on the intel runners in infra's
    # fleet declaration, asked for here instead; or yoga's images converging on
    # the declared stack (paiml/infra#813). X64 already excludes gx10 (ARM64,
    # also without the tools).
    runs-on: [self-hosted, clean-room, X64, intel]
    # infra#430: sixteen clean-room runners share one ~/.cargo, and an hourly
    # reaper deletes registry/src entries by mtime -- under a live build, which
    # makes rustc read a source file that has just vanished:
    #   couldn't read .../registry/src/.../<crate>/src/<file>.rs: No such file
    #   error: could not parse/generate dep info at: .../deps/<crate>.d
    # MEASURED on this branch: msrv and coverage both died that way the first
    # time PMAT-547 moved them off GitHub-hosted runners, where each job had a
    # private ~/.cargo by construction. A registry private to this runner takes
    # the job off the shared surface. The path is outside the workspace, so it
    # survives the checkout clean and is a cache rather than a cold download.
    # The host-side fix is paiml/infra's.
    env:
      CARGO_HOME: ${{ github.workspace }}/../cargo-home-${{ github.job }}
    if: >-
      github.event_name != 'pull_request' ||
      contains(github.event.pull_request.labels.*.name, 'proofs')
    # 45 was too short, but NOT because proving is slow — measured 2026-08-16:
    #
    #   proof_applicable_operators_valid   22+ min  -> 2s   (after the fix below)
    #   every other completed harness      0-5s each
    #   9 harnesses in 36 min = ~11s of proving, ~35 min of COMPILATION
    #
    # Kani rebuilds the crate with its own compiler and CI carries no cache for
    # that, so the cost is almost entirely the build. Raising this buys the
    # compile, not slow proofs. If a single harness ever dominates again, that
    # is the disk_budget/applicable_operators shape — an allocating function in
    # the harness — and the fix is to retarget it, not to raise this further.
    timeout-minutes: 150
    steps:
      - uses: actions/checkout@v7

      # Kani is preinstalled in the sovereign-ci image. Asserting it rather than
      # installing it: a runtime toolchain install makes the gate depend on the
      # network and hides a drifted image behind a green run.
      - name: Assert kani is available
        run: |
          if ! command -v cargo-kani >/dev/null 2>&1; then
            echo "cargo-kani is not on runner ${RUNNER_NAME:-unknown} — an absence on ONE runner is not proof it is missing from the image; add it to that runner's image, do not install at runtime (forjar#598)" >&2
            exit 1
          fi
          cargo kani --version

      # A cancelled kani run leaves a half-written `.d` in target/kani, and the
      # NEXT run then dies on it with a message that names no code:
      #
      #   error: could not parse/generate dep info at: .../deps/bashrs-*.d
      #   error: Failed to execute cargo (exit status: 101). Found 0 compilation errors.
      #
      # "0 compilation errors" is the tell — nothing is wrong with the crate.
      # This workflow has cancel-in-progress: true, and a 35-minute build gets
      # cancelled often, so inheriting that state is the normal case rather than
      # the exception. Same dep-info corruption paiml/rmedia#268 documents for
      # concurrent builds; here it comes from cancellation rather than sharing.
      #
      # The earlier version of this step wiped unconditionally, on the reasoning
      # that "kani rebuilds the crate with its own compiler every run
      # regardless, so discarding costs nothing". That reasoning was wrong.
      # These are SELF-HOSTED runners with a persistent workspace, so cargo does
      # reuse target/kani across runs — the unconditional wipe is precisely what
      # guaranteed a cold ~35-minute build every single time. It turned a cache
      # into a cost.
      #
      # The corruption it defended against is real but is specific to a run that
      # was INTERRUPTED mid-build. So: leave a sentinel while a build is in
      # flight and clear it when the job reaches a verdict. Finding the sentinel
      # at startup means the previous run died holding it, and only then is the
      # tree suspect.
      - name: Discard target/kani only if the previous run was interrupted
        run: |
          set -eu
          sentinel=target/kani/.forjar-build-in-flight
          if [ -e "$sentinel" ]; then
            echo "previous kani run did not reach a verdict — discarding target/kani"
            rm -rf target/kani
          else
            echo "previous kani run finished cleanly — reusing target/kani"
          fi
          mkdir -p target/kani
          touch "$sentinel"

      # Compilation is a distinct failure from non-verification, and it is the
      # one that actually happened. Surfacing it separately means a broken
      # harness reports as broken rather than as an opaque proof failure.
      #
      # `nice -n 19` because this job is bare-metal inside the shared 18-core
      # ci.slice: at niceness 19 it still gets the whole box when the box is
      # idle, but yields to interactive PR CI instead of competing with it. It
      # bounds proofs' effect on everyone else's latency, not its own runtime.
      - name: Harnesses must compile
        run: nice -n 19 cargo kani --only-codegen

      - name: Verify all harnesses
        run: nice -n 19 cargo kani --output-format terse

      # Deliberately not `always()`: on cancellation the sentinel must SURVIVE,
      # so the next run knows the tree was left mid-build. success()||failure()
      # covers "reached a verdict" and excludes exactly that case.
      - name: Mark the kani build tree as clean
        if: success() || failure()
        run: rm -f target/kani/.forjar-build-in-flight

  # Deliberately NOT gated behind the `proofs` label the way kani is. Measured
  # 2026-08-17: lean verified all 7 proofs in 67 seconds. The contention this
  # workflow was trimmed for is entirely kani's ~35-minute compile, so every PR
  # keeps real proof coverage at a cost that does not register.
  lean:
    name: lean
    # forjar#598 -- PINNED TO BARE METAL, AN INTERIM WITH A NAMED COUPLING.
    #
    # `[self-hosted, clean-room, X64]` matches the intel runners (bare metal,
    # tools present) AND the yoga-build* runners (EPHEMERAL containers --
    # yoga-build, -build2, -build3 all observed running these jobs on
    # 2026-09-20; lean + kani + rsync ABSENT by inventory). So this job was deterministic per runner and
    # a coin flip per run: on commit 537252d3 four runs went fail/pass/fail/pass
    # purely by which runner picked it up. A re-run landing on intel is a green
    # nobody can reconstruct.
    #
    # `intel` here is a HOSTNAME standing in for a CAPABILITY, which this repo
    # otherwise avoids (PMAT-547). Remove it when either lands: a capability
    # label (`provers` / `bare-metal`) declared on the intel runners in infra's
    # fleet declaration, asked for here instead; or yoga's images converging on
    # the declared stack (paiml/infra#813). X64 already excludes gx10 (ARM64,
    # also without the tools).
    runs-on: [self-hosted, clean-room, X64, intel]
    timeout-minutes: 30
    steps:
      - uses: actions/checkout@v7

      # elan installs into ~/.elan, which is not on the runners' PATH (they get
      # ~/.cargo/bin). Same shape as the existing Rust-toolchain PATH steps.
      # This only exposes it — if it is absent, the assertion below still fails.
      - name: Put the Lean toolchain on PATH
        run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: Assert lean is available
        run: |
          if ! command -v lean >/dev/null 2>&1; then
            echo "lean is not on runner ${RUNNER_NAME:-unknown} — an absence on ONE runner is not proof it is missing from the image; add it to that runner's image, do not install at runtime (forjar#598)" >&2
            exit 1
          fi
          lean --version

      # Every .lean file, and the count is asserted: a proof deleted or renamed
      # out of the glob would otherwise make this job pass by checking nothing,
      # which is the failure mode this whole workflow was written to end.
      - name: Verify Lean proofs
        run: |
          set -euo pipefail
          n=0
          for f in lean/*.lean; do
            echo "--- $f"
            lean "$f"
            n=$((n + 1))
          done
          echo "verified $n Lean proof(s)"
          if [ "$n" -lt 7 ]; then
            echo "expected at least 7 Lean proofs, found $n — a proof was removed" >&2
            exit 1
          fi

  # Aggregator so branch protection can require one context for both.
  ledger-replay:
    if: needs.classify.outputs.code == 'true'
    needs: classify
    name: ledger-replay
    runs-on: [self-hosted, clean-room, X64]
    # forjar#447 (second signature, measured on the host 2026-09-03): all 16
    # clean-room runners share ONE $HOME/.cargo registry, and two sweepers
    # delete extracted crate sources by age (the hourly ci-reaper's
    # `find registry/src -mtime +30 -exec rm -rf`, and cargo's own auto-gc)
    # while other runners are mid-compile — 962 crate dirs re-extracted in
    # 30 minutes right after the 09:01 sweep, bashrs/pmcp dep-info ENOENT on
    # runners 8 and 9 in that window. This job is the only one here that
    # compiles the whole binary from a cold target, so it is the one that dies.
    # A registry private to this runner takes the job off the shared surface;
    # the host-side fix is paiml/infra's (registry sweeps must not run under
    # live builds, or each runner gets its own CARGO_HOME like its toolchain).
    env:
      CARGO_HOME: ${{ github.workspace }}/../cargo-home-${{ github.job }}
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1

      - name: Build the binary under test
        run: cargo build --release

      # WHY THIS LANE EXISTS. docs/cli-defects.json held 85 confirmed defects,
      # each investigated and written down against 1.12.3. A 1.16.0 audit
      # re-ran them and FOURTEEN still reproduced — they had survived 1.13,
      # 1.14, 1.15 and 1.16. Not because they were hard: because nothing ever
      # re-ran the ledger. A defect register written once and never replayed is
      # a list of things you have decided to tolerate, whether or not you
      # decided that. (GH #299, #300.)
      #
      # The harness prints its DENOMINATOR every run ("replayed N of 84 ... M
      # carry no replay script and were NOT tested") and FAILS when it replays
      # zero entries, so growing coverage is visible and an empty sweep can
      # never read as success.
      # ASK CARGO WHERE THE BINARY IS, do not assume `target/`. On this fleet
      # something redirects the target directory to /mnt/nvme-raid0/targets/forjar
      # — not from a repo file, so it is environment-dependent and may or may
      # not apply on a runner. A hardcoded path would make the harness exit 1
      # with "no forjar binary": the right failure DIRECTION (fail-closed), but
      # a lane that is red on arrival for a path bug teaches people to ignore
      # it, which is the failure this whole release is about.
      - name: Every replayable ledger defect must stay fixed
        run: |
          TARGET_DIR=$(cargo metadata --format-version 1 --no-deps \
            | python3 -c 'import sys,json; print(json.load(sys.stdin)["target_directory"])')
          BIN="$TARGET_DIR/release/forjar"
          [ -x "$BIN" ] || { echo "::error::no binary at $BIN"; exit 1; }
          FORJAR="$BIN" bash scripts/ledger-replay.sh

  contracts:
    name: contracts
    runs-on: [self-hosted, clean-room, X64]
    # UNCONDITIONAL, unlike kani/lean. Those are label-gated because they cost
    # ~35 min of compilation; this is a YAML parse over 30 files and costs
    # seconds. A validator that only runs on labelled PRs is absent on the PRs
    # that need it most.
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1

      # AN ABSENT VERIFIER IS A NO-GO, NEVER A PASS. This repo has that rule and
      # was not applying it to its own contracts: `if command -v pv` would have
      # made every run green on a machine without pv, which is exactly the
      # defect class the contracts exist to catch.
      - name: pv must be present
        run: |
          command -v pv >/dev/null || {
            echo "::error::pv is not installed — the contract corpus is unvalidatable, which is a NO-GO not a skip"
            exit 1
          }
          pv --version

      # WHY THIS JOB EXISTS. contracts/verified-effect-v1.yaml shipped INVALID
      # on the 1.16.0 release branch — a duplicate falsifier id, created when
      # three blocker fixes each appended a clause and the merge kept both
      # sides. Nothing caught it: no CI job ran `pv validate` at all, so the
      # only signal was a human running it by hand during an audit. See #298.
      - name: Every contract must validate
        run: |
          set -u
          fail=0
          for c in contracts/*.yaml; do
            case "$c" in */binding.yaml) continue ;;   # a registry, not a contract
            esac
            OUT=$(pv validate "$c" 2>&1); EC=$?
            if [ "$EC" -ne 0 ]; then
              echo "::error file=$c::$(printf '%s' "$OUT" | grep -i error | head -1)"
              fail=$((fail+1))
            fi
          done
          n=$(ls contracts/*.yaml | grep -vc 'binding.yaml')
          echo "validated $n contract(s), $fail invalid"
          # A sweep that validated nothing must not report success — the empty
          # loop is the vacuous pass this whole corpus is about.
          [ "$n" -gt 0 ] || { echo "::error::no contracts found to validate"; exit 1; }
          [ "$fail" -eq 0 ]

      # CITATIONS ARE RESOLVED IN RUST, NOT HERE.
      #
      # This step used to be a Python heredoc that grepped for each falsifier's
      # function name. It was the defect #298 is about, one level up from the
      # corpus it was checking. Its rule was
      #
      #     re.fullmatch(r"([\w./-]+\.rs)::(\w+)", cite.strip())
      #
      # and the corpus writes citations in four shapes, of which that accepts
      # one. Everything else fell through a `continue` and was reported as
      # "not resolvable" rather than "not resolved", so the job printed
      # "every resolvable falsifier citation resolves" and exited 0 over
      # verb-surface-v1.yaml's seven dangling citations. It also grepped
      # src/ tests/ benches/ GLOBALLY, so all 28 wrong-FILE citations passed,
      # and it read only falsification_tests[].test, so 104 `enforced_by` and
      # 12 `discharged_by` citations were never resolved at all.
      #
      # The rule now lives in tests/falsification_contract_citations_resolve.rs
      # and runs in `ci / examples-validate`. Keeping a second, weaker copy
      # here is what let the rule narrow without anyone deciding to narrow it.

  proofs:
    name: proofs
    runs-on: [self-hosted, clean-room, X64]
    needs: [classify, kani, lean, contracts, ledger-replay]
    if: always()
    steps:
      # `skipped` is a PASS here and nothing else is. On an unlabelled PR the
      # proof jobs do not run at all, and treating that as failure would make
      # every such PR red — the shape that trains people to ignore a red check.
      # A genuine failure, cancellation or timeout is still `failure`/`cancelled`
      # and still fails this gate.
      - name: Check proof jobs
        env:
          CODE: ${{ needs.classify.outputs.code }}
        run: |
          set -eu
          rc=0
          for job in kani:"${{ needs.kani.result }}" lean:"${{ needs.lean.result }}" contracts:"${{ needs.contracts.result }}" ledger-replay:"${{ needs['ledger-replay'].result }}"; do
            name=${job%%:*}
            result=${job#*:}
            case "$result" in
              success) echo "$name: verified" ;;
              skipped)
                # PMAT-237: a skip is a pass only when the change could not
                # reach the job. kani is skipped by event; ledger-replay is
                # skipped by class, and if the class says `code` then a skip
                # there is a hole, not a saving.
                # An EMPTY class means classify did not run, so nothing knows
                # what this change can break: treat it as code (PMAT-237).
                if [ "$name" = "ledger-replay" ] && [ "${CODE:-true}" != "false" ]; then
                  echo "$name FAILED: skipped on a change the classifier called code" >&2
                  rc=1
                else
                  echo "$name: skipped (not selected for this change)"
                fi
                ;;
              *)       echo "$name FAILED: $result" >&2; rc=1 ;;
            esac
          done
          [ "$rc" -eq 0 ] && echo "All proofs accounted for"
          exit "$rc"