From 98b4b6faffef1b2b76c5b25fbc17074070dd9084 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 26 Aug 2026 02:41:38 +0200 Subject: [PATCH] plan(roadmap): cut v1.135 around PERF-P01 alone; TRACE-P02 -> v1.136 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v1.135 ships the cascade timing baseline and nothing else. WHY: performance was the ONE axis on which this project could make no claim at all. `engine-throughput` guarded the cFS engines since v1.56; the control path that actually flies had no timing baseline of any kind, and the WCET proof in Lean had never been confronted with a measurement. That was the highest-value gap in the standing assessment, and PERF-P01 (#361) closes it: full_cascade_tick 1.2413 us <- all five stages, one tick iekf_propagate 1.1256 us 91 % of the cascade the other four ~108 ns combined Deferred out, each with the reason recorded in the artifact rather than moved silently: TRACE-P02 -> v1.136 next, and now precisely sized MATHF32-P06 -> v1.139 not blocked, just lower value than the four ahead OCI-P03 -> v1.139 parked pending REWRITE, do not implement as written TRACE-P02 is no longer one undifferentiated sweep. Measured 2026-08-25: 155 of 236 verification artifacts have >=1 CI-runnable step -> promotable MECHANICALLY from the gate's own per-artifact result 36 are bench-only -> named waiver or a real step (judgement) 45 have NO steps at all -> cannot be evidence; write steps or demote And ZERO `implemented` requirements lack a verifier — the 22/247 verified figure is entirely UNPROMOTED verifiers, not missing evidence. That makes the bulk of it far cheaper than it looked, and isolates the 45 as the real work. OCI-P03's restated warning matters because it is easy to pick up by release order: upstream wit-bindgen 0.60 already generates `[u8; 8]`, so the fixed-length-list case for the fork is gone; the fork is three minors stale (0.58 vs upstream 0.61.1) and NOTHING in relay depends on it. The drift that actually matters is in the flight path — components pin wit-bindgen-rt 0.41 while the workspace is on 0.60, a 19-minor spread, and 0.41 generates the bindings in every published artifact. Rewrite around that migration; it needs no fork. PERF-P01's criterion (d) — the PX4 head-to-head — is NOT discharged and is now filed as #362 rather than left as an unmet criterion nobody re-reads. We can say what our cascade costs; we cannot yet say it costs less. rivet validate: PASS, exit 0. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-FALCON-MATHF32-P06.yaml | 10 ++++++-- artifacts/swreq/SWREQ-FALCON-OCI-P03.yaml | 19 +++++++++++++-- artifacts/swreq/SWREQ-FALCON-TRACE-P02.yaml | 23 +++++++++++++++++-- 3 files changed, 46 insertions(+), 6 deletions(-) diff --git a/artifacts/swreq/SWREQ-FALCON-MATHF32-P06.yaml b/artifacts/swreq/SWREQ-FALCON-MATHF32-P06.yaml index cac5898..a5d0a61 100644 --- a/artifacts/swreq/SWREQ-FALCON-MATHF32-P06.yaml +++ b/artifacts/swreq/SWREQ-FALCON-MATHF32-P06.yaml @@ -3,7 +3,7 @@ artifacts: type: sw-req title: "MATHF32-P06 — machine-checked Cody-Waite argument-reduction bound → FULL-range sin/cos accuracy" status: proposed - release: falcon-v1.135.0 + release: falcon-v1.139.0 description: > The remaining and HARDEST ingredient: a machine-checked bound on the Cody-Waite argument reduction r = ((x - n*PIO2_HI) - n*PIO2_MID) - @@ -17,7 +17,13 @@ artifacts: slice (the reduction cancellation is the part those references spend most of their pages on — weeks, not days) and deliberately sequenced AFTER P04/P05 so the reduced-range proof lands first. - tags: [falcon, relay-math, f32, gappa, argument-reduction, machine-checked, qualification, v1.130] + Deferred to v1.139 (2026-08-26). Not blocked and not obsolete — simply + lower value than the four releases ahead of it (PERF-P01 measurement, + TRACE-P02 promotion, the trusted-base publication, and the oracle + repairs), each of which moves a claim the project currently cannot + make or cannot defend. + + tags: [falcon, relay-math, f32, gappa, argument-reduction, machine-checked, qualification, v1.139] fields: req-type: non-functional priority: could diff --git a/artifacts/swreq/SWREQ-FALCON-OCI-P03.yaml b/artifacts/swreq/SWREQ-FALCON-OCI-P03.yaml index 779a9bc..9b40ab7 100644 --- a/artifacts/swreq/SWREQ-FALCON-OCI-P03.yaml +++ b/artifacts/swreq/SWREQ-FALCON-OCI-P03.yaml @@ -3,7 +3,7 @@ artifacts: type: sw-req title: "OCI-P03 — bounded messaging payloads: adopt the wit-bindgen fork (fixed-length lists + arena/elision)" status: proposed - release: falcon-v1.135.0 + release: falcon-v1.139.0 description: > Message-carrying seams shall declare BOUNDED payloads, so the work memory they require can be sized and defended rather than being unbounded. @@ -42,7 +42,22 @@ artifacts: justification for adopting the FORK is obsolete; the allocator work (gale-owned arena via cabi-realloc-extern, relay#330) is what remains. Rewrite the requirement around that before implementing it. - tags: [falcon, oci, wasm, wit-bindgen, messaging, embedded, v1.135] + Still parked at v1.139 pending the REWRITE noted above — do not + implement against the current text. Restated because it is easy to + pick up by release order: upstream wit-bindgen 0.60 already generates + `[u8; 8]` for `list`, so the fixed-length-list justification for + adopting the fork is gone. What remains is the gale-owned arena + (relay#330), and measured 2026-08-25 the fork is three minors stale + (synced at upstream 0.58, upstream now 0.61.1) with NOTHING in relay + depending on it. + + The drift that actually matters is different and is in the flight + path: our components pin `wit-bindgen-rt` 0.41.0 while the workspace + is on 0.60.0 — a 19-minor spread in one repo, and 0.41 generates the + bindings baked into every published artifact. Rewrite this requirement + around THAT migration, which needs no fork at all. + + tags: [falcon, oci, wasm, wit-bindgen, messaging, embedded, v1.139] fields: req-type: interface priority: should diff --git a/artifacts/swreq/SWREQ-FALCON-TRACE-P02.yaml b/artifacts/swreq/SWREQ-FALCON-TRACE-P02.yaml index 6f8f57e..b6f8a5e 100644 --- a/artifacts/swreq/SWREQ-FALCON-TRACE-P02.yaml +++ b/artifacts/swreq/SWREQ-FALCON-TRACE-P02.yaml @@ -3,7 +3,7 @@ artifacts: type: sw-req title: "TRACE-P02 — promote the V: drive implemented→verified from the verification gate's own per-artifact result" status: proposed - release: falcon-v1.135.0 + release: falcon-v1.136.0 description: > Artifact status shall reflect executed evidence, so that "verified" means a gate ran the artifact's steps and they passed. @@ -36,7 +36,26 @@ artifacts: a downstream consumer (jess) is BLOCKED on the relocation fix and the published artifact is the only way to hand it to them. Accumulating unrelated scope would make them wait on work they do not need. - tags: [falcon, rivet, traceability, verification, hygiene, v1.135] + Re-scoped to v1.136 (2026-08-26). v1.135 is cut around PERF-P01 alone — + the cascade timing baseline — because performance was the one axis on + which the project could make no claim at all, and that gap was the + highest-value item in the standing assessment. TRACE-P02 follows + immediately and is now precisely sized (see below). + + MEASURED SIZING (2026-08-25), which decomposes this into three + populations with very different costs rather than one sweep: + 155 of 236 verification artifacts carry >=1 CI-runnable step + -> promotable MECHANICALLY from the gate's per-artifact result + 36 are bench-only + -> need a named waiver or a real step; judgement, not bookkeeping + 45 have NO steps at all + -> cannot be evidence as they stand; write steps or demote + Also measured: ZERO `implemented` requirements lack a verifier. The + 22/247 verified figure is entirely UNPROMOTED verifiers, not missing + evidence — which makes this far cheaper than it looks, except for the + 45. + + tags: [falcon, rivet, traceability, verification, hygiene, v1.136] fields: req-type: constraint priority: should