diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 86efee38..9e4508b5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -546,6 +546,76 @@ jobs: - name: Check coverage run: rivet coverage + # --------------------------------------------------------------------------- + # Rivet Federated Graph — ADVISORY (deliberately NOT in the required set). + # + # #1012: the required job above validates ONLY the synth-local half (it strips + # the externals block), so the entire federated half of the trace graph was + # unchecked — six dead `path: /Volumes/Home/...` entries poisoned resolution + # for months and nothing noticed. This job owns the federated half: it syncs + # the sibling repos and validates every cross-repo traces-to link. + # + # WHY ADVISORY, stated as the tradeoff it is: resolving the federated graph + # makes network access AND seven sibling repos' current heads a CI dependency + # (`rivet sync` tracks `ref: main` — rivet has no `sync --locked` mode, so the + # committed rivet.lock pins for reproducibility/impact tooling but does not + # pin what CI fetches). A sibling deleting an artifact synth links to SHOULD + # turn this red — that is a real broken trace — but it must not block synth + # merges that didn't cause it, and a GitHub/network hiccup must not deadlock + # the queue. So: visible red, non-blocking. Promote to required only if it + # stays quiet long enough to earn it (and then only with a lock-pinned sync). + # + # WHY rivet v0.32.0 HERE while the job above stays on v0.23.0: this is a NEW + # pin for a NEW job, not a silent bump of the existing gate — sync/lock and + # the broken-cross-ref accounting this job exists to exercise are what + # matured after 0.23.0, and the in-tree rivet.lock was written by 0.32.0. + # Installed under its OWN --root: both jobs share self-hosted runners, and + # ~/.cargo/bin/rivet is shared machine state — clobbering versions would make + # the two jobs re-build rivet-cli (HiGHS C++) on alternating runs, the exact + # disk-filling failure the binary cache above exists to prevent. + # --------------------------------------------------------------------------- + rivet-federated: + name: Rivet Federated Graph (advisory) + runs-on: [self-hosted, linux, x64, rust-cpu] + timeout-minutes: 30 + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache rivet-cli 0.32.0 binary + uses: actions/cache@v6 + with: + path: ~/.cargo/rivet-0.32/bin/rivet + key: ${{ runner.os }}-rivet-cli-v0.32.0 + - name: Install rivet 0.32.0 (own root — never clobbers the 0.23.0 at ~/.cargo/bin) + run: | + if ! ~/.cargo/rivet-0.32/bin/rivet --version 2>/dev/null | grep -q "0.32.0"; then + cargo install --force --git https://github.com/pulseengine/rivet --tag v0.32.0 --root ~/.cargo/rivet-0.32 rivet-cli + fi + - name: Sync externals (network — clones the 7 sibling repos) + run: ~/.cargo/rivet-0.32/bin/rivet sync + - name: Validate the federated graph + # Exit code IS the gate (rivet validate exits non-zero on FAIL). tee'd + # under pipefail so the log keeps the full diagnostic list. + run: | + set -o pipefail + ~/.cargo/rivet-0.32/bin/rivet validate 2>&1 | tee /tmp/rivet-federated.txt + - name: Non-vacuity guard — resolution must actually have run + # The #1012 signature was "FAIL (50 errors, ..., 0 broken cross-refs)": + # zero broken cross-refs beside dozens of link errors because rivet + # never RESOLVED the graph (dead paths), not because it was clean. A + # validator reporting N errors and 0 has + # usually not gotten far enough to look. Guard: a resolved graph loads + # external artifacts that link back to synth ("Cross-repo backlinks: + # N"), and N was 1032 at authoring — if resolution ever silently stops + # again, N reads 0 and this step goes red even though validate PASSed. + run: | + BACKLINKS=$(grep -oE 'Cross-repo backlinks: [0-9]+' /tmp/rivet-federated.txt | grep -oE '[0-9]+' | head -1) + echo "Cross-repo backlinks: ${BACKLINKS:-0}" + if [ "${BACKLINKS:-0}" -eq 0 ]; then + echo "::error::Federated resolution appears NOT to have run (0 cross-repo backlinks loaded) — the #1012 poisoned-resolution signature. A green validate above is vacuous in this state." + exit 1 + fi + bazel: name: Bazel Build & Proofs # Stays on ubuntu-latest: needs Nix + Bazel + Rocq via Bazel diff --git a/artifacts/component-model.yaml b/artifacts/component-model.yaml index d865bdcf..5b807780 100644 --- a/artifacts/component-model.yaml +++ b/artifacts/component-model.yaml @@ -226,8 +226,12 @@ artifacts: target: CM-002 - type: traces-to target: CM-005 - - type: traces-to - target: kiln:FR-P3-ASYNC-BUILTINS + # A traces-to link to kiln:FR-P3-ASYNC-BUILTINS was removed in #1012: + # kiln's artifact store has no such id (never did — zero hits in the + # synced repo), and retargeting to the nearest live kiln P3 artifacts + # (REQ_P3_CALLBACK / REQ_P3_LIBCOMP, both about async lifting rather + # than the 'recursive' reentrance effect) would fabricate a trace. + # Re-add the link if kiln lands a matching requirement. fields: req-type: functional priority: should diff --git a/artifacts/gale-integration.yaml b/artifacts/gale-integration.yaml index a5282897..72517d35 100644 --- a/artifacts/gale-integration.yaml +++ b/artifacts/gale-integration.yaml @@ -558,8 +558,6 @@ artifacts: links: - type: derives-from target: GI-NPA-001 - - type: traces-to - target: gale:354 fields: req-type: functional priority: must @@ -616,8 +614,6 @@ artifacts: links: - type: derives-from target: GI-002 - - type: traces-to - target: gale:369 fields: req-type: functional priority: must @@ -706,8 +702,6 @@ artifacts: links: - type: derives-from target: GI-002 - - type: traces-to - target: gale:369 fields: req-type: functional priority: must @@ -837,8 +831,6 @@ artifacts: links: - type: derives-from target: GI-005 - - type: traces-to - target: gale:372 fields: req-type: functional priority: must @@ -894,8 +886,6 @@ artifacts: links: - type: derives-from target: GI-NPA-001 - - type: traces-to - target: gale:359 fields: req-type: functional priority: must @@ -938,8 +928,6 @@ artifacts: links: - type: derives-from target: GI-005 - - type: traces-to - target: gale:374 - type: traces-to target: jess:TEST-PIX-013 fields: @@ -1012,8 +1000,6 @@ artifacts: links: - type: derives-from target: GI-005 - - type: traces-to - target: gale:382 fields: req-type: functional priority: must diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 406ee538..11d159be 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -2752,8 +2752,6 @@ artifacts: target: VCR-RA-001 - type: refines target: VCR-DEC-001 - - type: traces-to - target: gale:209 fields: req-type: constraint priority: should @@ -2862,8 +2860,6 @@ artifacts: # the title/tags where it is a reference rather than a resolvable target. - type: traces-to target: VCR-COV-001 - - type: traces-to - target: witness:130 fields: req-type: constraint priority: should diff --git a/rivet.lock b/rivet.lock new file mode 100644 index 00000000..ac96b58d --- /dev/null +++ b/rivet.lock @@ -0,0 +1,29 @@ +pins: + gale: + git: https://github.com/pulseengine/gale.git + commit: 52d00eb7da7c4cbb42d6fab16bad09abd6d12b55 + prefix: gale + jess: + git: https://github.com/pulseengine/jess.git + commit: d3211dd8ede1854dd461931f146e63ab76dbdca1 + prefix: jess + kiln: + git: https://github.com/pulseengine/kiln.git + commit: cbfd1b538c49461195e920e4aff8925232623d68 + prefix: kiln + loom: + git: https://github.com/pulseengine/loom.git + commit: 5168f935054f8b0e96e8612fc04fdc4f61eb85d0 + prefix: loom + meld: + git: https://github.com/pulseengine/meld.git + commit: c6e51a3ac02a85a003ce7168c2b0f9b9239d7394 + prefix: meld + scry: + git: https://github.com/pulseengine/scry.git + commit: 35aed0fe60639766988a4dd6918fefec7e4c2bf0 + prefix: scry + sigil: + git: https://github.com/pulseengine/sigil.git + commit: 1e9ec54d529cc7371a540fa1598070289e2ef4ef + prefix: sigil diff --git a/rivet.yaml b/rivet.yaml index e63d7425..46201456 100644 --- a/rivet.yaml +++ b/rivet.yaml @@ -42,36 +42,44 @@ commits: externals: kiln: git: https://github.com/pulseengine/kiln.git - path: /Volumes/Home/git/pulseengine/kiln ref: main prefix: kiln meld: git: https://github.com/pulseengine/meld.git - path: /Volumes/Home/git/pulseengine/meld ref: main prefix: meld sigil: git: https://github.com/pulseengine/sigil.git - path: /Volumes/Home/git/pulseengine/sigil ref: main prefix: sigil loom: git: https://github.com/pulseengine/loom.git - path: /Volumes/Home/git/pulseengine/loom ref: main prefix: loom gale: git: https://github.com/pulseengine/gale.git - path: /Volumes/Home/git/pulseengine/gale ref: main prefix: gale scry: git: https://github.com/pulseengine/scry.git - path: /Volumes/Home/git/pulseengine/scry ref: main prefix: scry + + # jess hosts the hermetic Renode silicon oracles synth artifacts trace to + # (e.g. TEST-PIX-013, GI-MEM-002's OOB-trap verification). Declared in #1012 + # when federated resolution was repaired — it had been referenced by + # traces-to links but never declared, so the refs could not resolve. + # NOTE (#1012): externals deliberately carry NO `path:` — a declared local + # path takes precedence over `git:`, and a dead one (the /Volumes/Home + # entries removed in #1012) poisons resolution for everyone else: rivet + # reports "0 broken cross-refs" beside dozens of link errors because it + # never resolves the graph at all. Sync via `rivet sync` (git fallback). + jess: + git: https://github.com/pulseengine/jess.git + ref: main + prefix: jess