From 7c42172c97f06775dd38a1a3dd001b9f72020524 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 15 Sep 2026 22:13:30 +0200 Subject: [PATCH] plan(v1.139): the two dark gates and the horizontal hold; and v1.138.0's notes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- .github/release-notes/v1.138.0.md | 160 +++++++++++++++++++++ artifacts/swreq/SWREQ-FALCON-HOLD-P01.yaml | 55 +++++++ artifacts/swreq/SWREQ-RELAY-VGATE-P04.yaml | 49 +++++++ 3 files changed, 264 insertions(+) create mode 100644 .github/release-notes/v1.138.0.md create mode 100644 artifacts/swreq/SWREQ-FALCON-HOLD-P01.yaml create mode 100644 artifacts/swreq/SWREQ-RELAY-VGATE-P04.yaml diff --git a/.github/release-notes/v1.138.0.md b/.github/release-notes/v1.138.0.md new file mode 100644 index 00000000..0f0e4f5c --- /dev/null +++ b/.github/release-notes/v1.138.0.md @@ -0,0 +1,160 @@ +# falcon v1.138.0 — the wasm cascade flies Gazebo, and the 15-second swing is fixed + +The published wasm cascade now **flies real Gazebo**, and the "it starts +swinging after about fifteen seconds" report is fixed at the root. + +This bundles the **v1.136 → v1.138** arc; those tags were never cut. + +## The swing + +Reported from a Windows/WSL2 bench: *"es fängt nach etwa 15 sekunden an zu +schwingen."* Reproduced, and it is not drift — it is a limit cycle driven by the +altitude integral, which charged through the entire climb and then spent that +charge as overshoot (NED, negative is up): + +``` +t=7.9s true_z -2.14 (target reached) alt_int -6.26 <- peak charge +t=13.9 true_z -2.64 (overshoot) alt_int -3.45 +t=39.9 true_z -0.08 (nearly aground) alt_int -5.72 +``` + +At `ki 0.03`, ±6 is a ±0.19 thrust swing on a 0.585 hover. The integral now +charges only when the vehicle is **not already converging**. + +Before: 0.62 m error at 16 s, and a 40 s hold ends near the ground. After: four +25 s holds measured **0.02, 0.04, 0.21 and 0.10 m** — and `alt_int` sits at +−0.040 for the whole hold instead of swinging ±6. (Four runs rather than one +because a single green gz run has already fooled us once this cycle.) + +Both obvious fixes were measured and rejected: a velocity gate cannot separate +the cases (the climb runs at only 0.1–0.29 m/s), and an error band cannot either +(the thrust-lapse sag the integral must reject is ~1.5 m, *larger* than the band +that would block the climb). Their product does separate them. + +## Also in this release + +- **`configure(vehicle-config)`** — nine airframe values a host can install. + Before it, every number was frozen inside the component and no host could + correct them from outside. +- **ESC telemetry on the seam** — `read_motor_rpm` had no field at all, so the + rotor-out FDI in the published component was inert by construction. +- **Gazebo runs in CI** for the first time, with video recorded every run and a + hard gate on the hold error. The wasm and native paths are bit-identical + per-motor across every tick. + +--- + +# Answers to two questions from the embedded track + +## 1. "synth float poles are WIP (#708/#369). Was fehlt dafür noch?" + +**Those notes are stale, and floats lower fine.** `#369` (soft-float for all +f32/f64) and `#708` (`f32.load` + `i32.reinterpret_f32`) were both **closed +10–11 July 2026**. Verified on **synth 0.66.0**, `--target cortex-m7dp`: + +``` +vmul.f32 s3, s0, s1 +vadd.f32 s4, s3, s2 +vdiv.f32 s2, s0, s1 +vsqrt.f32 s1, s0 +``` + +Real hardware FPU, hard-float ABI. So the trivial float path you asked us to +validate **passes**. + +### One warning that matters more than the answer + +A **stale synth silently emits wrong code**. Our first attempt used a +four-month-old binary, which compiled the same module with **exit 0** and +emitted: + +| export | emitted | meaning | +|---|---|---| +| `faxpy(a,b,c)` | `mov r0,r2 ; bx lr` | returns `c` — no multiply, no add | +| `fdiv(a,b)` | `mov r0,r1 ; bx lr` | returns `b` | +| `fsqrt(x)` | `bx lr` | returns `x` | + +No FPU instructions, no error, no warning. We nearly reported "floats don't +lower, your route stalls" on the strength of it. So your instinct to validate a +trivial float path is exactly right — and **the first thing to validate is the +version**. Pin synth through varve rather than a `cargo install` binary, and +disassemble the result once; an integer function of the same shape is a good +control (ours lowered to a correct `mul.w`/`adds` in 10 bytes while the float +one was 4). + +### What is actually still missing, for our cascade + +On **synth 0.66.0 / cortex-m7dp**, **21 of the cascade's 22 functions lower**, +including 1408- and 1468-byte ones. Exactly one declines — the tick itself: + +``` +GI-FPU-002: VFP register file exhausted (S0..S15 all live) — f32/f64 register +pressure exceeds the file; the backend retries with VFP spilling (#881) and +this surfaces only if that also fails +``` + +Target sensitivity, same input: + +| target | functions skipped of 22 | +|---|---| +| **cortex-m7dp** | **1** (the tick only) | +| cortex-m4f | 3 | +| cortex-m7 | 3 | +| cortex-m3 (no FPU) | 16 | + +We tried reducing the pressure from our side by splitting the export into a +forwarder plus an `#[inline(never)]` body. **It does not help** — the decline +moves with the body, so the pressure is inherent to the tick (where +`FlightCore::step` inlines the whole cascade), not to the export boundary. +Filed as **synth#1267**, including the question of whether per-stage +`#[inline(never)]` in the guest is the intended remedy. + +**So: floats are not the blocker. Register pressure in one large tick is.** +That is a much narrower risk than "the whole meld+synth route stalls", and it +is visible on day one exactly as you suggested. + +**Not validated here:** the `→ Renode` half. Renode is not installed on this +machine, so we confirmed `synth compile --cortex-m` only. Someone with Renode +should close that loop before the firmware rewrite goes on the schedule. + +## 2. "Can synth emit a relocatable object or static archive, rather than a linked ELF?" + +**Yes — a relocatable object.** `synth compile --relocatable`: + +``` +int_rel.o: ELF 32-bit LSB relocatable, ARM, EABI5 version 1 — not stripped +00000000 g F .text 0000000a iaxpy +``` + +`ET_REL`, with global function symbols in `.text` that a linker can see. The +flag's own help is explicit: *"Force relocatable object (.o, ET_REL) output even +when wasm has no imports — for linking into a host build system."* `--link` is +the opposite direction (links to firmware ELF via `arm-none-eabi-gcc`), and +`--builtins` takes a kiln-builtins `.o`. + +**A static archive is not emitted directly** — that is `arm-none-eabi-ar rcs +libfoo.a out.o`. One gotcha we hit: use the **cross** `ar`. The macOS host `ar` +accepts the file and produces a malformed archive (`ranlib: warning: archive +member not a mach-o file`). + +**So the PX4-module route is not gated on output format.** It is gated on +GI-FPU-002 for the tick, above. + +--- + +## Known, filed, not fixed + +- **#403** — the horizontal loop diverges after ~26 s of hold; it was hidden + under the altitude oscillation until that was fixed. This is why a 40 s hold + still ends badly even though the altitude loop is now clean. +- **#398** — rotor-out recovery does not hold on the gz plant. +- **#397** — `//:falcon-cascade` has not built under Bazel since #393, so the + cascade's witness MC/DC coverage is not being produced. +- **synth#1267** — the cascade tick declines on cortex-m7dp. + +## Falsification + +This release is wrong if a 25 s stationary 2 m hold on the gz `falcon-quad`, +driven by the published component through the Component Model seam, leaves the +vehicle more than 0.5 m from the commanded altitude — or if the wasm and native +paths ever differ by a single per-motor bit. diff --git a/artifacts/swreq/SWREQ-FALCON-HOLD-P01.yaml b/artifacts/swreq/SWREQ-FALCON-HOLD-P01.yaml new file mode 100644 index 00000000..a0fb9405 --- /dev/null +++ b/artifacts/swreq/SWREQ-FALCON-HOLD-P01.yaml @@ -0,0 +1,55 @@ +artifacts: + - id: SWREQ-FALCON-HOLD-P01 + type: sw-req + title: "HOLD-P01 — a stationary position hold shall stay bounded for at least 60 s, horizontally as well as vertically" + status: proposed + release: falcon-v1.139.0 + description: > + Commanded to hold a fixed NED position, the vehicle shall remain within + 0.5 m vertically and 1.0 m horizontally of the setpoint for at least 60 s + on the reference Gazebo plant. + + WHY IT EXISTS. v1.138.0 fixed the ALTITUDE half: the altitude integral + charged through the climb and spent it as overshoot, producing a limit + cycle a colleague reported as "es fängt nach etwa 15 sekunden an zu + schwingen". With that fixed the altitude holds cleanly — and a SECOND + instability became visible underneath it. Measured over 40 s after the + fix: + + t=21.9 true_z -1.98 xy=[+0.41,-0.64] tilt 0 deg + t=25.9 true_z -1.97 xy=[-1.55,+2.01] tilt 1 deg + t=31.9 true_z -1.41 xy=[+11.21,-5.02] tilt 2 deg + t=39.9 true_z -0.04 xy=[-22.95,-2.58] tilt 6 deg + + The horizontal excursion comes FIRST; the altitude loss follows it as tilt + steals the vertical thrust component (#403). + + WHY IT WAS INVISIBLE. The `flightcore` scenario's `final_dist` is the + ALTITUDE error alone (`alt_err = -target_alt_m - last_true[2]`), not 3D + distance, so every native gz verdict to date has reported horizontal drift + as zero BY CONSTRUCTION. A hold gate that cannot see horizontal error is + the empty-scope-passes shape again, and closing that measurement gap is + part of this requirement, not a follow-up to it. + + NOT THE SAME DEFECT as the altitude one, and deliberately not fixed the + same way. There is no horizontal transient to wind up from — the setpoint + is the launch point and `perr` starts at zero — and applying the altitude + anti-windup condition here breaks three verified wind-rejection tests + (`holds_position_under_steady_wind`, `rejects_wind_gusts`, and the + `f100_passthrough` fixture). It was tried and reverted. + + FIRST JOB, BEFORE ANY FIX: separate "the controller is unstable" from "the + estimate has gone bad". The traced `xy` samples move up to 25 m in 2 s, + about 12 m/s, which the observed 1-2 deg tilt cannot produce + (`g*tan(2deg) ~ 0.34 m/s^2`). Either the vehicle thrashes far harder + between samples than the 0.1 s-sampled tilt suggests, or the position and + velocity the loop acts on are not trustworthy late in the run — + `est_z` and `true_z` also separate from about t=31. A per-tick trace of + both true and estimated horizontal position and velocity settles it. + + FALSIFICATION: wrong if a 60 s stationary 2 m gz hold leaves the vehicle + more than 1.0 m horizontally or 0.5 m vertically from the setpoint. + tags: [requirement, falcon, control, gazebo, hold, v1.139] + links: + - type: derives-from + target: SYSREQ-FALCON-010 diff --git a/artifacts/swreq/SWREQ-RELAY-VGATE-P04.yaml b/artifacts/swreq/SWREQ-RELAY-VGATE-P04.yaml new file mode 100644 index 00000000..68623bab --- /dev/null +++ b/artifacts/swreq/SWREQ-RELAY-VGATE-P04.yaml @@ -0,0 +1,49 @@ +artifacts: + - id: SWREQ-RELAY-VGATE-P04 + type: sw-req + title: "VGATE-P04 — a verification track that CANNOT RUN shall block the release, not merely go red" + status: proposed + release: falcon-v1.139.0 + description: > + A verification track whose toolchain fails to execute shall be treated as + a release blocker, distinguishable in the release gate from a track that + ran and passed. + + WHY IT EXISTS. At falcon-v1.138.0 two tracks were dark and the release + went out anyway: + + Verus — all 19 proof targets failed in 0.1 s each with + `error[E0463]: can't find crate for core/std`. They never ran. + Red on six consecutive main commits, 2026-09-11 to 2026-09-15 + (#405). + Bazel — `//:falcon-cascade` has not built since #393, so the fused + image and the witness MC/DC coverage it feeds have produced + nothing for four days (#397). + + Neither is in the required-contexts set, so neither blocked a merge, and + the release-execution traceability gate did not surface them either: it + audits artifact status and trace links, and both tracks' artifacts were + already `verified` from when the tracks last ran. + + THE DISTINCTION THIS REQUIREMENT ADDS. VGATE-P01 forbids orphaned proofs, + P02 forbids untraced ones, P03 requires a cited enforcer to be OBSERVED to + pass. All three assume the track executes. This is the fourth case: the + track is wired correctly, is cited correctly, and cannot run at all. From + the evidence's point of view that is indistinguishable from never having + had the proofs — which is exactly the state #364 was created to end + ("19 proofs were defined and NONE ever ran"). + + A RED GATE IS NOT ENOUGH ON ITS OWN. Both tracks WERE red, visibly, for + days. Redness that blocks nothing decays into background noise; what + matters is that the release cannot be cut while a track is dark, or that + cutting it records the darkness explicitly in the release notes. v1.138.0 + did the latter by hand — this requirement is to stop relying on the + operator remembering. + + FALSIFICATION: wrong if a release can be tagged while any verification + track fails to execute, without that fact being recorded in the release + as a known gap. + tags: [requirement, relay, verification-gate, release, v1.139] + links: + - type: derives-from + target: SYSREQ-FALCON-010