plan(v1.139): the two dark gates, the horizontal hold, and v1.138.0's release notes - #406
Merged
Merged
Conversation
…0's notes SCOPE ADDED TO falcon-v1.139.0 (both `proposed`): SWREQ-RELAY-VGATE-P04 — a verification track that CANNOT RUN shall block the release, not merely go red. At v1.138.0 two tracks were dark and the release went out anyway: Verus failed all 19 targets in 0.1 s each with "can't find crate for core/std" (#405, red on six consecutive main commits), and //:falcon-cascade has not built since #393 so the witness MC/DC coverage it feeds has produced nothing (#397). Neither is a required context, so neither blocked a merge — and the release-execution traceability gate did not catch them either, because it audits artifact status and trace links, and both tracks' artifacts were already `verified` from when the tracks last ran. VGATE-P01/P02/P03 all assume the track EXECUTES; this is the fourth case, where it is wired correctly, cited correctly, and cannot run at all. From the evidence's point of view that is indistinguishable from never having had the proofs. Worth being blunt about: both gates WERE red, visibly, for days. Redness that blocks nothing decays into background noise. v1.138.0 recorded the darkness in its release notes by hand; the requirement exists so that stops depending on the operator remembering. SWREQ-FALCON-HOLD-P01 — a stationary hold shall stay bounded for 60 s, HORIZONTALLY as well as vertically (#403). v1.138.0 fixed the altitude half and uncovered a horizontal divergence underneath it; the excursion comes first and the altitude loss follows as tilt steals vertical thrust. It carries the measurement gap as part of the requirement rather than as a follow-up: the flightcore scenario's `final_dist` is the ALTITUDE error alone, so every native gz verdict to date has reported horizontal drift as zero by construction. It also records what NOT to do — the altitude anti-windup condition was tried here and reverted, because there is no horizontal transient to wind up from and it breaks three verified wind-rejection tests — and names the first diagnostic job: separate "the controller is unstable" from "the estimate has gone bad", since the traced excursions imply ~12 m/s at a tilt that can only produce 0.34 m/s^2. ALSO: .github/release-notes/v1.138.0.md, the body release.yml looks for. It answers the two synth questions the embedded track asked — floats DO lower on synth 0.66.0 (verified vmul/vadd/vdiv/vsqrt, hard-float ABI), the real blocker is GI-FPU-002 register pressure on the one big tick (synth#1267), and `--relocatable` does emit ET_REL for the PX4-module route. It also carries the warning that cost the most to find: a STALE synth silently emits wrong code with exit 0 — ours returned an argument instead of computing anything, and we nearly reported "floats don't lower" on the strength of it. Refs #397, #398, #403, #405. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
added a commit
that referenced
this pull request
Sep 16, 2026
…#425) (#426) The required `Kani gate` went red on main and blocked every merge in the repo. 45 engine legs failing at once. ROOT CAUSE, with the timeline: kani-0.68.0 released 2026-09-16T03:43:14Z first failing CI run 2026-09-16T03:55:44Z <- 12 minutes later last passing CI run 2026-09-15T19:49 <- the v1.138.0 tag commit `model-checking/kani-github-action@v1` has a `kani-version` input that defaults to `latest`. We never set it, so every run installed whatever Kani had most recently published. Upstream shipped 0.68.0 and our required gate fell over twelve minutes later. IT IS NOT THE PROOFS, established rather than assumed. Every failing leg completed in about 11 s, which is far too fast for model checking, and the only change to the tree between the last green run and the first red one was PR #406 — artifacts and release notes, no Rust. Running the same thing locally on 0.67.0 settles it: crates/relay-lc $ cargo kani ** 0 of 75 failed VERIFICATION:- SUCCESSFUL Complete - 9 successfully verified harnesses, 0 failures, 9 total. 0.67.0 is exactly what `latest` resolved to for the whole period the gate was green (it was released 2026-01-16), so this pins the known-good state rather than picking a new one. Moving to 0.68.0 is a deliberate change with its own validation — not something an upstream release gets to do to us at 03:43 on a required gate. THE GENERAL LESSON, which this repo has now paid for twice. An unpinned tool in a REQUIRED gate is an unreviewed dependency on someone else's release schedule. The same class already bit us on the other side: a stale, four-month-old local synth binary silently emitted wrong float code with exit 0. Floating means "whatever, whenever", in both directions. Also worth recording: this was visible for hours as "the Kani gate is red" and read as a proof problem. The 11-second job duration was the tell, and duration is not something anyone looks at when a verification gate goes red. Closes #425. Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verify-Filter: (or (has-tag "verification-gate") (has-tag "hold") (has-tag "wasm"))
Refs #397, #398, #403, #405.
Scope added to
falcon-v1.139.0(bothproposed)SWREQ-RELAY-VGATE-P04 — a track that cannot run must block the release
At v1.138.0 two verification tracks were dark and the release went out anyway:
can't find crate for core/std//:falcon-cascadehas not built, so witness MC/DC coverage produces nothingNeither is a required context, so neither blocked a merge. And the
release-execution traceability gate did not catch them either — it audits
artifact status and trace links, and both tracks' artifacts were already
verifiedfrom when the tracks last ran.VGATE-P01 (no orphaned proofs), P02 (no untraced proofs) and P03 (a cited
enforcer must be observed to pass) all assume the track executes. This is
the fourth case: wired correctly, cited correctly, cannot run. From the
evidence's point of view that is indistinguishable from never having had the
proofs — the exact state #364 was created to end.
Being blunt about the lesson: both gates were red, visibly, for days. Redness
that blocks nothing decays into background noise. v1.138.0 recorded the darkness
in its release notes by hand; this requirement exists so that stops depending on
the operator remembering.
SWREQ-FALCON-HOLD-P01 — a hold must stay bounded for 60 s, horizontally too
v1.138.0 fixed the altitude half of the swing and uncovered a horizontal
divergence underneath it (#403). The excursion comes first; the altitude loss
follows as tilt steals the vertical thrust component.
The requirement carries the measurement gap rather than deferring it: the
flightcorescenario'sfinal_distis the altitude error alone, so everynative gz verdict to date has reported horizontal drift as zero by
construction.
It also records what not to do — the altitude anti-windup condition was tried
here and reverted (no horizontal transient to wind up from; it breaks three
verified wind-rejection tests) — and names the first diagnostic job: separate
"the controller is unstable" from "the estimate has gone bad", since the traced
excursions imply ~12 m/s at a tilt that can only produce 0.34 m/s².
Also:
.github/release-notes/v1.138.0.mdThe body
release.ymllooks for. It answers the two questions from the embeddedtrack:
vmul.f32/vadd.f32/vdiv.f32/vsqrt.f32, hard-float ABI.#369/#708are closed; those noteswere stale. The real blocker is GI-FPU-002 register pressure on the one large
tick — 21 of 22 cascade functions lower on cortex-m7dp (synth#1267).
--relocatableemits ET_REL, so the PX4-module route is not gated onoutput format.
wrong code with exit 0 — ours returned an argument instead of computing
anything, and we nearly reported "floats don't lower" on the strength of it.
🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG