plan(v1.139): the two dark gates, the horizontal hold, and v1.138.0's release notes

.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.

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

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