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