Skip to content

ci: batch — genuine setup-bazel pin, fail-closed gates, taiki bump, dependabot grouping, merge_group triggers - #588

Merged
avrabe merged 7 commits into
mainfrom
ci/batch-gates-pins-grouping
Oct 22, 2026
Merged

avrabe merged 7 commits into
mainfrom
ci/batch-gates-pins-grouping

Conversation

@avrabe

@avrabe avrabe commented Oct 21, 2026

Copy link
Copy Markdown
Contributor

Why one PR: main is strict — every merge sends every other open PR through a full CI cycle on a saturated rust-cpu pool (#514). These four are all CI configuration and none is in Kani's scope regex (0 hits), so batching them costs one cycle instead of three or four.

Each commit is the exact reviewed commit, cherry-picked (-x records the source):

commit was what
45223e9 #583 release.yml: repin setup-bazel from 5483a91 (not in the action's history — fork-network object, used by every release since v1.77) to the genuine v0.14.0 e8776f5. Measured tree-identical (20 files, same content hash; 0.19.1 control differs) → no executed-code change. Signing-path review: maintainer approved merging (2026-10-21).
a54e61e #584 spar analyze honours spar's exit code (passed on a missing .aadl); float-discipline gate fails closed on a missing crate and reports its denominator (22/22, 52 files). Both negative-controlled old vs new.
06b880b #579 taiki-e/install-action 2.87.27 → 2.87.29 (tag verified to exist).
e63109e new dependabot grouping: one weekly PR per ecosystem for minor/patch; majors stay separate. The five cargo entries become one multi-directories entry — #576 and #578 were the same line of root Cargo.toml.

Closed as part of this consolidation: #569 (superseded by #574), #580 (deliberate version jump on the signing path), #576 (duplicate of #578).

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

avrabe and others added 4 commits October 21, 2026 17:03
…as not in the action's history

`release.yml` pinned `bazel-contrib/setup-bazel@5483a91b6e3ffac6092848f1dd7eafcfad203d80`
with the comment `# v0.14.0 pinned`. That SHA is not v0.14.0 — tag 0.14.0 is
e8776f58fb6a6e9055cbaf1b38c52ccc5247e9c4 — and it is not in the action
repository's history at all:

  commits/<sha>              422 "No commit found"
  commits/<sha>/branches-where-head   422
  github.com/.../commit/<sha>.patch   Not Found
  search/commits?q=hash:<sha>         0 results
  tarball/<sha>              HTTP 200   <- still served

GitHub resolves `owner/repo@<sha>` across the whole fork network, so an object
that exists only in a fork, or was orphaned, still downloads under the
upstream name. That is the "imposter commit" class, and it sat on the release
job since #205 (2026-06-17, v1.77). The signed falcon-v1.140.0 run's log
records `Download action repository 'bazel-contrib/setup-bazel@5483a91…'`.

IT WAS BENIGN — MEASURED. Extracted into an isolated directory and never
executed, its tree is byte-identical to the genuine v0.14.0:

  5483a91 (pinned)   20 files   content tree-hash d9249affa4edfd11
  e8776f5 (v0.14.0)  20 files   content tree-hash d9249affa4edfd11
  104e3ee (v0.19.1)  24 files   content tree-hash 24710fabad65c309   <- control

The control proves the comparison discriminates. So no release ran anything but
v0.14.0's code; what was wrong is that nobody could have SHOWN that from the pin,
and the object could vanish (breaking a release mid-tag) or — had it differed —
run arbitrary code on the job that produces signed artifacts.

This repin changes NO executed code, only provenance: from "an object nobody can
locate" to "the release tag's own commit". It is deliberately NOT the 0.19.1 bump
in #580: that is a version change on the signing path and should be judged on its
own. (#580's new SHA 104e3ee IS genuinely 0.19.1 — but it kept the stale
"# v0.14.0 pinned" comment, which is how this surfaced.)

AUDIT, so this is not one of several: every SHA-pinned `uses:` in .github/ was
checked for existence upstream, with a negative control (a fabricated SHA must
read NOT-IN-UPSTREAM) and a positive one (real 0.19.1 must read IN-UPSTREAM).
3 distinct SHA pins; this was the ONLY one not in its repository. The first run of
that audit was vacuous — `--jq '.sha[0:7]'` prints the string "null" on a 422 and
read as present — and the controls are what exposed it.

Not in scope, named: ~every other action in this repo is pinned by mutable TAG,
not SHA. That is a broader posture question, not this defect.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
(cherry picked from commit 5854e39)
…fail closed

Prompted by jess#292, which found an absence-assertion in jess's CI that
passed on an EMPTY log ("a gate that asserted the absence of a skip, read no
evidence, and said 0"). A read-only audit of relay's workflows and the scripts
they call found the same class twice here. Each is now proven both ways with
negative controls run against the old and the new gate.

1. spar.yml "Analyze system roots" — VACUOUS on missing input (not required).
   `out=$(spar analyze ...) || true` then decided on `grep -qE ERROR` alone.
   Measured with spar itself: an unreadable/missing .aadl makes spar EXIT 1 and
   print "Cannot read <path>: No such file or directory" — no ERROR line — so
   the gate passed having analysed nothing. Same for a `spar/*.aadl` glob that
   stops matching, or a missing binary. Now the exit code is the verdict and the
   grep a second opinion. `|| rc=$?` (not a bare call) because `shell: bash`
   runs with -e and every root should still report.

     case                         old   new
     real models (spar/*.aadl)    pass  pass
     missing input file           PASS  fail
     glob matching nothing        PASS  fail

   No false-failure risk, measured: all five real roots exit 0 while printing
   10-22 WARNINGs each.

2. scripts/check-float-discipline.sh — LATENT in the REQUIRED Clippy check.
   `[ -d "$src" ] || continue` dropped a listed flight crate silently when it
   had no source, and nothing counted what was scanned; run in an empty tree
   the script printed "float discipline: OK" and exited 0. Every listed crate
   must now contribute a scanned file (else CANNOT DETERMINE, fail), and OK
   reports its denominator.

     case                               old       new
     real tree                          pass      pass — "scanned 22/22 flight crates, 52 .rs files"
     empty tree                         PASS      fail (22 crates flagged)
     a listed crate renamed away        skipped   fail
     f64 injected in flight code        fail      fail   (detection preserved)

   The f64 control was itself wrong the first time — appended at end-of-file,
   it landed inside the gate's deliberate cfg(test)-to-EOF exemption and read
   as "0 hits" for BOTH versions. Placed in real code (line 40, before the
   first cfg(test) at 354) both catch it. Recorded because a control that
   cannot fail looks exactly like a gate that cannot fail.

   This script's own comment already records one earlier vacuous incident (BSD
   awk has no \y); this is the second, of a different mechanism.

NAMED, NOT FIXED (assessed as guarded or out of scope for this change):
  - verification-gate.yml:349 detects "verified nothing" by grepping for the
    literal "# 0 artifact(s) matched". Guarded in practice (pipefail + the
    runner fails on 0 tests), but wording-coupled: renaming the print silences
    it. A positive-count assertion would be sturdier.
  - check-verification-independence.sh prints OK on an unresolvable base ref
    (git diff errors to stderr, `|| true`). The workflow's merge-base fallback
    makes that need two bad sources, so mostly guarded.
  - gazebo.yml's BIT-IDENTICAL check only fires if a DIFFERENTIAL line exists;
    a run with the differential off passes it (the LOOP CLOSES/^PASS checks
    still bound the empty-log case).

Refs pulseengine/jess#292

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
(cherry picked from commit 530ea6f)
Bumps [taiki-e/install-action](https://github.com/taiki-e/install-action) from 2.87.27 to 2.87.29.
- [Release notes](https://github.com/taiki-e/install-action/releases)
- [Changelog](https://github.com/taiki-e/install-action/blob/main/CHANGELOG.md)
- [Commits](taiki-e/install-action@v2.87.27...v2.87.29)

---
updated-dependencies:
- dependency-name: taiki-e/install-action
  dependency-version: 2.87.29
  dependency-type: direct:production
  update-type: version-update:semver-patch
...

Signed-off-by: dependabot[bot] <support@github.com>
(cherry picked from commit 0bcd445)
Ungrouped, one upstream release arrived as several PRs: the wit-bindgen
0.62 -> 0.63 bump came twice (#576 and #578 edit the SAME line, root
Cargo.toml:90 — the /fuzz entry resolves to the workspace manifest, and #576
omitted the Cargo.lock change), and three action bumps arrived as three.

main's protection is `strict`, so every merge sends every other open PR back
through a full CI cycle, Kani matrix included. N small PRs therefore cost N
SERIAL cycles on a shared, saturated rust-cpu pool (#514). One grouped weekly PR
per ecosystem collapses that to one cycle.

The five cargo entries become one multi-`directories` entry so the duplicate
cannot recur. MAJOR bumps stay ungrouped — an API break gets its own PR and its
own review, never buried in a batch of patch bumps. The github-actions entry
keeps the per-pin existence check as a documented obligation (#583).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
…n be enabled

The maintainer chose a merge queue (2026-10-21) to replace `strict`
protection, under which every merge sends every other open PR back through a
full CI cycle on a saturated rust-cpu pool (#514).

ORDER MATTERS, and is why this lands before the setting flips: a queue can only
merge a PR whose required checks are reported on the `merge_group` event. Enable
the queue first and nothing — including the PR that adds these triggers — could
ever pass it.

The four workflows that produce the nine required contexts all gain
`merge_group:` —
  ci.yml                Format, Clippy, Test (linux/macos/windows),
                        Closed-loop simulation + Monte-Carlo campaigns
  verification-gate.yml Verification gate (rivet-driven)
  kani.yml              Kani gate
  gazebo.yml            Gazebo SITL (real gz bridge)

TWO SCOPE CHECKS NEEDED THE QUEUE'S BASE, or they would have thrown away most of
the speed-up without failing anything:
  - kani.yml read `pull_request.base.sha || event.before`; a merge_group run has
    neither, so it took the "no base sha" backstop and ran all 47 legs on every
    queue entry. Now `|| merge_group.base_sha` sits between them.
  - verification-gate.yml's scope step read only `pull_request.base.sha`, so
    every entry fell to the full ~45-min sweep. Same fix. The Verify-Filter
    override is NOT available in a queue run (no PR body), so a relevant change
    runs the default full filter — the intended trade: the queue tests the
    COMBINED tree that will land and must not inherit one PR's narrowing.
Both still fail SAFE to the full run if the base is unusable.

NOT VACUOUS IN THE QUEUE, checked: the only event-gated steps in these four are
the two-commit-rule step (already run on the PR), and the cosmetic setup-gh +
sticky-comment steps in the verification gate. The verdict step is not gated.
Concurrency keys are safe as written: a queue run has an empty head_ref and a
unique `gh-readonly-queue/main/pr-N-<sha>` ref, so it gets its own group and
cannot be cancelled by its PR's own run.

actionlint: clean.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
@avrabe
avrabe enabled auto-merge (squash) October 21, 2026 15:51
@avrabe avrabe changed the title ci: batch — genuine setup-bazel pin, fail-closed gates, taiki bump, and dependabot grouping (supersedes #583 #584 #579) ci: batch — genuine setup-bazel pin, fail-closed gates, taiki bump, dependabot grouping, merge_group triggers Oct 21, 2026
@github-actions

github-actions Bot commented Oct 21, 2026 •

Copy link
Copy Markdown
Contributor

✅ Rivet verification gate — falcon

176/176 passed

count
Passed 176
Failed 0
Skipped (bench-only — needs hardware / sim) 21
Skipped (no steps) 12

Bench-only artifacts (not run by CI)

  • FV-FALCON-ARCH-001 — spar AADL architectural model — falcon cascade (v0.13)
  • FV-FALCON-ARCH-002 — spar codegen --format wit recheck — works at v0.10.0 (v0.15.0)
  • FV-FALCON-COV-001 — witness MC/DC structural coverage — falcon pipeline wired (v0.13)
  • FV-FALCON-COV-002 — cargo-llvm-cov statement coverage — workspace-wide (v0.14.0)
  • FV-FALCON-COV-003 — witness MC/DC on real Rust source — Geofence subject (v0.14.1)
  • FV-FALCON-GEO-003 — Geofence safety path — miri UB/overflow check (v0.12, AI substitute)
  • FV-FALCON-LYAP-002 — Strict (cross-term) Lyapunov — exponential-decay inequality + CI-gated Lean proofs (v1.105)
  • FV-FALCON-LYAP-004 — Lyapunov exponential convergence — the deferred 'trajectory ⇒ converges' step, discharged (v1.107)
  • FV-FALCON-MATHF32-003 — MATHF32-P03 — machine-checked (Gappa→Flocq→coqc) rounding bound for the f32 sin polynomial (v1.127)
  • FV-FALCON-MATHF32-004 — MATHF32-P04 — machine-checked (Coq-Interval) approximation bound for the f32 sin polynomial (v1.128)
  • FV-FALCON-MATHF32-005 — MATHF32-P05 — machine-checked rounding + approximation bounds for the f32 cosine kernel (v1.129)
  • FV-FALCON-MELD-001 — meld-fuse the verified cascade into a single module (v1.5.0)
  • FV-FALCON-OCI-001 — OCI-P01 — signed per-component publish, WASI-free build, and through-wasm closed-loop proof (v1.129)
  • FV-FALCON-SIM-001 — PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)
  • FV-FALCON-SIM-005 — gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)
  • FV-FALCON-TARGET-001 — Verified flight core as a bare-metal ARM Cortex-M ELF + sim backend (v1.6.0)
  • FV-FALCON-WASMCM-001 — Verified flight core runs in wasmtime as a CM component (v1.26.0)
  • FV-FALCON-WASMCM-002 — All 8 falcon CM components build and bundle script emits versioned dist/ (v1.56)
  • FV-FALCON-WCET-001 — Compositional WCET + flight-cascade schedulability, kernel-checked (v1.10.0)
  • FV-FALCON-WIT-001 — Verified IEKF componentized + plugged into the composed cascade (v1.4.0)
  • FV-RELAY-KANICI-003 — Orphaned-proof sweep completed — flight-support + HAL + infra Kani harnesses enforced in CI (v1.108)

Source of truth: artifacts/verification/FV-FALCON-*.yaml.

@temper-pulseengine

Copy link
Copy Markdown
Contributor

Automated review for PR #588

pulseengine/relay:ci/batch-gates-pins-grouping → pulseengine/relay:main

Verdict: 💬 Comment

Summary: The workflow updates the merge_group event to ensure that REQUIRED checks are run on the queue's merge_group event, which prevents queued PRs from waiting forever for a check that is never reported. Additionally, it ensures that the base SHA is correctly identified in merge_group runs.

Findings: 0 mechanical (rivet) · 5 from local AI model.

Findings (5):

  1. .github/workflows/ci.yml:9

      merge_group:
    

    The merge_group event is used to ensure that REQUIRED checks are run on the queue's merge_group event.

  2. .github/workflows/gazebo.yml:15

      merge_group:
    

    The merge_group event is used to ensure that REQUIRED checks are run on the queue's merge_group event.

  3. .github/workflows/kani.yml:11

      merge_group:
    

    The merge_group event is used to ensure that REQUIRED checks are run on the queue's merge_group event.

  4. .github/workflows/spar.yml:67

              BASE_SHA: ${{ github.event.pull_request.base.sha || github.event.merge_group.base_sha }}
    

    The base SHA is correctly identified in merge_group runs.

  5. .github/workflows/verification-gate.yml:14

      merge_group:
    

    The merge_group event is used to ensure that REQUIRED checks are run on the queue's merge_group event.


Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at 0d32da0

@avrabe
avrabe merged commit 588f680 into main Oct 22, 2026
60 checks passed
@avrabe
avrabe deleted the ci/batch-gates-pins-grouping branch October 22, 2026 11:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant