v0.82 lane wave: eight lanes in one change, because runner contention is the binding constraint

.github/workflows/compliance.yml

@@ -79,9 +79,69 @@ jobs:
         with:
           ref: ${{ steps.tag.outputs.tag }}
 
+      # RQ-82-COMPLIANCE2 (#1453): THE TRIGGER WAS FIXED AND THE JOB STILL PRODUCED
+      # NOTHING. v0.81 made this workflow reachable (it ran on the v0.81.0 tag for
+      # the first time ever, 7 steps) and it then FAILED at `Generate compliance
+      # report`, so `Upload report to release` SKIPPED and v0.81.0 carries 13 assets
+      # with no compliance tarball. DERIVED, not inferred: the single `actions/checkout`
+      # above gives the job synth ONLY, while `rivet.yaml` declares SEVEN externals
+      # whose clones live under `.rivet/repos/<prefix>` — a path that is GITIGNORED
+      # (.gitignore:62) and therefore cannot arrive with any checkout. rivet then
+      # reports `could not load externals: IO error` and every cross-repo `traces-to`
+      # target reads as dangling. That is the #1012 signature: link errors BESIDE
+      # unloaded externals mean resolution never ran, not that the links are broken.
+      #
+      # THE PATTERN IS NOT NEW — it is lifted from ci.yml's federated-graph job,
+      # #1143. AUTHENTICATE FOR QUOTA, NOT FOR ACCESS: all seven siblings are PUBLIC,
+      # so no permission is needed, but GitHub rate-limits ANONYMOUS git traffic and
+      # a throttled response makes git fall back to interactive auth, surfacing on a
+      # tty-less runner as `fatal: could not read Username for 'https://github.com'`
+      # — which reads like a permissions failure and is not one. GITHUB_TOKEN is
+      # repo-scoped and that is fine; the authenticated RATE LIMIT is the point. The
+      # rewrite is scoped to this step and removed on exit rather than persisted.
+      - name: Sync rivet externals (network — the 7 PUBLIC sibling repos)
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -euo pipefail
+          git config --global url."https://x-access-token:${GH_TOKEN}@github.com/".insteadOf "https://github.com/"
+          trap 'git config --global --unset-all url."https://x-access-token:${GH_TOKEN}@github.com/".insteadOf || true' EXIT
+          python3 -c 'import yaml' 2>/dev/null || python3 -m pip install --quiet --disable-pip-version-check pyyaml
+          python3 - <<'PYEOF'
+          import pathlib, subprocess, sys, yaml
+
+          # DERIVED from rivet.yaml, so adding an external never needs a second
+          # edit here. A hand-written mirror of this list is the drift the North
+          # Star forbids.
+          ext = (yaml.safe_load(pathlib.Path("rivet.yaml").read_text()) or {}).get("externals") or {}
+          if not ext:
+              sys.exit("REFUSE: rivet.yaml declares NO externals — a zero population "
+                       "here would make this step succeed while syncing nothing, and "
+                       "the report would be generated against an unresolved graph.")
+          root = pathlib.Path(".rivet/repos")
+          root.mkdir(parents=True, exist_ok=True)
+          cloned = []
+          for name, cfg in sorted(ext.items()):
+              dest = root / (cfg.get("prefix") or name)
+              if dest.exists():
+                  cloned.append(name); continue
+              r = subprocess.run(["git", "clone", "--depth", "1", "--branch",
+                                  cfg.get("ref") or "main", cfg["git"], str(dest)],
+                                 capture_output=True, text=True)
+              if r.returncode != 0:
+                  sys.exit(f"REFUSE: clone of {name} failed rc={r.returncode}: "
+                           f"{r.stderr.strip()[-400:]}")
+              cloned.append(name)
+          # NON-VACUITY: every declared external must be present, or the report
+          # would be built on a partially resolved graph and look complete.
+          if len(cloned) != len(ext):
+              sys.exit(f"REFUSE: synced {len(cloned)} of {len(ext)} declared externals")
+          print(f"synced {len(cloned)} of {len(ext)} externals: {', '.join(cloned)}")
+          PYEOF
+
       - name: Generate compliance report
         id: report
-        uses: pulseengine/rivet/.github/actions/compliance@v0.39.0
+        uses: pulseengine/rivet/.github/actions/compliance@v0.40.0
         with:
           theme: dark
           rivet-version: v0.37.0

artifacts/release-v0.82/RQ-82-ARCHMODEL.yaml

@@ -44,4 +44,48 @@ artifacts:
       priority: should
       issue: "#1136"
       verification-track: manual
+      disposition: deferred
+      landed: "PR #1492 — #1136 — the TWENTIETH filing, ordinal DERIVED BY ARTIFACT IDENTITY and stated with its commit; spar issue 445 re-checked STATE-first and still OPEN; the filing shown SEEN by RUNNING the step 1-2 matcher, which reports NA-FILED."
+      verified-by: >
+        DEFERRED — STEPS 1-2 ARE SKIPPED AGAIN AND THE BLOCKER IS UNMOVED. This is the
+        recurring N/A, filed so the skip stays VISIBLE rather than becoming the silent
+        default, and it records an outcome rather than being silent itself.
+
+        THE ORDINAL IS DERIVED BY ARTIFACT IDENTITY AND STATED WITH ITS COMMIT, because the
+        next filing invalidates it and v0.81's artifact had to be corrected for omitting the
+        commit: `ls artifacts/release-v*/RQ-*ARCHMODEL*.yaml | wc -l` returns TWENTY at
+        6034b224, an unbroken run from RQ-63-ARCHMODEL through this one. It is NOT derived by
+        counting releases.
+
+        spar#445 WAS RE-CHECKED STATE-FIRST, which is the #345 lesson — a body is written once
+        and never updated, so the state is the fact: `gh issue view 445 --repo pulseengine/spar`
+        reports STATE=OPEN with no `closedAt`. The blocker stands, so steps 1-2 remain N/A
+        rather than merely unattempted.
+
+        AND THE FILING IS SHOWN SEEN BY RUNNING THE MATCHER, NOT BY READING THE TAGS, which is
+        what the done-when asks for and what RQ-69-ARCHMODEL failed: it lost the `feature-loop`
+        tag, so the filing that exists to keep a deferral visible became invisible to the gate
+        that reads it. `python3 scripts/loop_conformance_check.py v0.82.0` prints
+
+          step 1-2 spar AADL->WIT  filed decision  NA-FILED  decided, artifact scoped, not yet
+          built: RQ-82-ARCHMODEL (#1136, status proposed) [scoped to v0.82, evaluated at checkout]
+
+        Reading the tags would have said the same thing and proved nothing; the matcher
+        requires `feature-loop` AND one of `{aadl, spar}` AND a `fields.issue`, and this
+        artifact carries `process, feature-loop, spar, aadl` and `issue: "#1136"`.
+
+        ONE MEASUREMENT TAKEN WHILE THE MATCHER WAS RUN, recorded because it is about THIS
+        release's tail rather than about #1136: the same gate reports step 3 "reported outcome"
+        as DERIVED-FAIL with 10 of 12 artifacts recording no outcome. That is a TRANSIENT
+        state, not a defect — the gate evaluates at HEAD, and ten of this release's artifacts
+        carry their `disposition`/`verified-by`/`landed` on lane branches that have not merged
+        yet. It clears as the lanes land, and if it does NOT clear by the tag it is a real
+        finding. Step 0 (workspace still 0.81.0), step 7 (no cold-review record yet) and step 8
+        (changelog topmost section still [0.81.0]) are DERIVED-FAIL for the same pre-tag reason.
+
+        WHAT WOULD END THE RECURRENCE, unchanged and not re-litigated: a synth-owned `.aadl`
+        architecture model tracked in-repo, which is what makes the matcher take branch (a)
+        instead of branch (b). The maintainer's recorded decision on #1136 is "not permanently
+        N/A; timing first", so this filing is a deferral with a named blocker rather than an
+        exemption.
       done-when: "manual:2026-12-31 the twentieth filing exists with BOTH the feature-loop tag and a spar/aadl tag, shown SEEN by running the step 1-2 matcher rather than by reading the tags; the ordinal derived by ARTIFACT IDENTITY and stated with the commit it is true at; spar#445's STATE re-checked before its body; and an outcome recorded rather than the artifact being silent"

artifacts/release-v0.82/RQ-82-BAZELPOTENCY.yaml

@@ -45,4 +45,80 @@ artifacts:
       priority: should
       issue: "#1456"
       verification-track: manual
+      disposition: partial
+      landed: "PR #1492 — #1456 — The gap is NARROWED, not closed: this artifact's own cost model was wrong by an order of magnitude — the job runs in 2.0-2.3 min, MEASURED on two commits — so the control is CHEAP and the blocker is SCHEDULING. Recorded UNPROVEN, with the mechanism and the trigger named."
+      verified-by: >
+        PARTIAL — `Bazel Build & Proofs` IS STILL RECORDED UNPROVEN, which is the honest state
+        the gate-potency pass requires, and the gap is materially narrower than v0.81 left it.
+        No paired control was run, so nothing here claims potency.
+
+        THE REFUTING COMMAND RAN FIRST AND DID NOT REFUTE. The protection API still lists nine
+        contexts and `Bazel Build & Proofs` is one of them; `~/.cache/bazel` DOES NOT EXIST, so
+        the cache is cold as recorded; nix answers 2.33.1 after sourcing `nix-daemon.sh` and
+        bazel is at `/opt/homebrew/bin/bazel`. Every stated precondition holds.
+
+        THIS ARTIFACT'S COST MODEL WAS WRONG BY AN ORDER OF MAGNITUDE, and that is the finding.
+        It says a paired control "needs TWO full cold Bazel+Nix+Rocq proof builds". MEASURED
+        from CI's own job records on two separate commits — ee9a9559 (the v0.81 release commit)
+        and 93c5e4b4 — the job completes in 2.3 and 2.0 MINUTES. It is `runs-on: ubuntu-latest`
+        with `bazel-contrib/setup-bazel` restoring a `disk-cache` keyed on the workflow plus a
+        `repository-cache`, so the Rocq toolchain and the compiled libraries come back from
+        cache. The expensive route was never the only route: the cost belongs to the LOCAL
+        reproduction, not to the control.
+
+        AND THE BUILD GRAPH MAKES A ONE-FILE CONTROL CHEAP, read from `coq/BUILD.bazel` rather
+        than assumed: the suite is a chain of per-module `rocq_library` targets with EXPLICIT
+        `deps` over 34 `.v` files, not one monolithic target. Breaking a single proof therefore
+        rebuilds that library and its reverse dependencies only. Breaking `base` would rebuild
+        everything; breaking a leaf rebuilds one. Which targets are leaves needs
+        `bazel query`, which needs a server start and the external repos, so it is NAMED as the
+        next step rather than guessed at here.
+
+        ONE POTENCY SUB-FINDING, BY INSPECTION AND LABELLED AS SUCH. The `Verify Rocq proofs`
+        step is a bare `run: bazel test //coq:verify_proofs` — no `|| true`, no
+        `|| [ $? -eq 4 ]` — so it CANNOT pass vacuously on Bazel exit 4, "no tests matched".
+        That matters because the step DIRECTLY BELOW IT in the same job documents exactly that
+        bug (#945: a tolerated exit 4 made the Renode step "pass while selecting nothing") and
+        guards it deliberately. The proof step is on the right side of that line. This is
+        INSPECTION, not a control: it establishes the step cannot swallow a failure, not that a
+        broken proof produces one.
+
+        THE LOCAL ROUTE IS REFUTED ON MEASURED DISK, a constraint this artifact did not know:
+        the data volume is at 99% with 7.3 GiB available. A cold Bazel+Nix+Rocq build does not
+        fit, and `/nix/store` is already 21 GiB. 16 GiB sits in a SIBLING project's
+        `rivet/target` and was deliberately NOT purged — it belongs to another repository and
+        another session, no compiler was running in it at the time of checking, and buying a
+        rebuild for another project is not this lane's call to make. Nothing in the remaining
+        release path needs a local build, so disk is not blocking.
+
+        SO THE BLOCKER IS SCHEDULING, NOT COST, and it is named precisely. `ci.yml` triggers on
+        `push: branches: [main]` and `pull_request: branches: [main]`, so pushing a scratch
+        BRANCH raises no workflow at all — the control needs a PULL REQUEST. That queues the
+        whole workflow: 73 job keys, of which 46 are `ubuntu-latest`, 18 are
+        `[self-hosted, linux, x64, rust-cpu]` and 3 are `light`. THE BINDING CONSTRAINT IS THE
+        46, NOT THE 18, and an earlier draft of this sentence had it backwards: it blamed the
+        seven-runner rust-cpu partition on a point sample reading 7/7 busy. Measured properly on
+        #1491's CI run via the JOBS api grouped by `labels`: ALL 46 queued jobs were
+        `ubuntu-latest` and ZERO self-hosted jobs were queued — the partition had already
+        finished sixteen rust-cpu jobs across all seven runners. The stall was GitHub-hosted
+        concurrency, consumed org-wide (loom 4 running + 5 queued, rivet 1 + 8, synth 0
+        running) and nothing to do with the label partition.
+        AND THIS REPO HAD ALREADY RECORDED THAT CORRECTION, which is the part worth keeping:
+        RQ-61-CICAP's `landed:` says "a point sample showed rust-cpu 7/7 and I inferred
+        saturation; 10 samples over ~9 minutes with runs queued throughout show all 12
+        self-hosted runners idle ... the bottleneck is the GitHub-hosted quota, not the
+        self-hosted fleet", and RQ-62-CLAIMCHECK calls the same 7/7 reading "a merge-wave
+        transient". A carried artifact family is a strong signal that a decision already
+        exists, and `git grep -n rust-cpu -- artifacts/` would have produced it before the
+        diagnosis rather than after.
+        The CONCLUSION is unchanged and now rests on the right number: a
+        deliberately-broken-proof PR queues 46 GitHub-hosted jobs behind the release's own, so
+        it waits until the queue drains.
+
+        WHAT WOULD SETTLE IT, affordable and unblocked once the queue drains: open a scratch PR
+        that breaks ONE leaf proof (a broken `Qed`, NOT an added `sorry` — this repo has
+        shipped a "fail on sorry" gate where all twelve `sorry`s carried a self-exempting
+        comment), confirm `Bazel Build & Proofs` reds with an attributable diagnostic, record
+        the run link, close the PR without merging, and confirm the unmodified tree passes. Two
+        job runs at ~2 minutes each, both on GitHub-hosted runners, zero local disk.
       done-when: "manual:2026-12-31 `Bazel Build & Proofs` is recorded POTENT with a paired control — a broken proof reds the job, the unmodified tree passes it, both with run links — or the lane states with measured build times why the control remains unaffordable and what would make it affordable"