From 5f35807aec7f29f3eaeb30f3d6eb67adda8aa539 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 28 Jul 2026 21:27:43 +0200 Subject: [PATCH] =?UTF-8?q?docs(release):=20v0.6.0=20plan=20=E2=80=94=20'R?= =?UTF-8?q?each=20and=20Rigor'=20(breadth=20x=20depth,=20full=20scope)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Plans the next release along both north-star axes. Grounded on measured state: T2 (object-code verification) and T3 (schedulability) are UNTOUCHED (req+V both proposed); T4's V was never closed; and 12 requirements have a closed V but a lagging status, so the release-completeness gate currently misreports them. Scope committed in full: D1 close T4's V, D2 object-code first light, D3 traceability promotion + a CI gate so the drift cannot recur, D4 schedulability bridge; B1 fused gale-nano gust:os component (gale#224), B2 a third target family through the AADL model, B3 a new capability class. Sequenced D3 first (until the gate tells the truth, cuttability is unanswerable) with the two research-shaped tracks late. Claims are not committed with the scope: any workstream that cannot close honestly ships WITH ITS GAP STATED rather than inflated. Kill-criteria retained for the two overclaimable items (T2 first light, the component's gust:hal-only residual). Co-Authored-By: Claude Opus 4.8 --- docs/releases/v0.6.0-breadth-depth.md | 141 ++++++++++++++++++++++++++ 1 file changed, 141 insertions(+) create mode 100644 docs/releases/v0.6.0-breadth-depth.md diff --git a/docs/releases/v0.6.0-breadth-depth.md b/docs/releases/v0.6.0-breadth-depth.md new file mode 100644 index 00000000..5df7cf58 --- /dev/null +++ b/docs/releases/v0.6.0-breadth-depth.md @@ -0,0 +1,141 @@ +# gust v0.6.0 — "Reach and Rigor" (breadth × depth) + +**Status:** planning. Each workstream lands as its own PR and closes its rivet scope +before the tag is cut. Scope is stated honestly: what is *verified*, what is +*demonstrated*, what is *deferred*. + +## Why this shape + +v0.5.0 was consolidation — it shipped the accumulated merged work and took the leap +the upstream blockers were gating. v0.6.0 is the first release planned along the two +north-star axes deliberately: + +- **BREADTH** — how far the OS reaches: more targets, more consumers, more capability + surface. gust is a *composable* OS; breadth is the claim that the seam generalizes. +- **DEPTH** — how well the claims hold: the safety release line defined four + cross-cutting verification tracks (T1–T4) and **two are still untouched**. Depth is + the claim that the certificates are real. + +Breadth without depth is a demo; depth without breadth is a lab result. v0.6.0 does +both, and the traceability machinery is fixed so the release gate tells the truth. + +## Grounded starting state (measured, not assumed) + +| Track | Requirement | V (verification) | Reality | +|---|---|---|---| +| T1 tri-track | `REQ-OS-TRITRACK-001` implemented | `VER-OS-TRITRACK-001` **verified** | V closed, REQ status lags | +| T2 object-code verification | `REQ-OS-OBJVERIFY-001` **proposed** | `VER-OS-OBJVERIFY-001` **proposed** | **untouched** | +| T3 schedulability | `REQ-OS-SCHED-001` **proposed** | `VER-OS-SCHED-001` **proposed** | **untouched** | +| T4 static WCET | `REQ-OS-WCET-001` implemented | `VER-OS-WCET-001` **proposed** | **V open** | +| I-ISO keystone | `REQ-OS-ISO-001` implemented | `VER-OS-ISO-001` **verified** | V closed, REQ status lags | + +**Traceability machinery gap (found while planning):** **12 requirements** whose +`VER-*` is `verified` but whose own status still reads `implemented`/`proposed` — +including the whole verified driver suite (adc/can/dac/i2c/pwm/spi/wdg/dma/breadth), +`REQ-DRV-GPIO-001`, `REQ-DRV-TIMER-001` and `REQ-OS-SYSCALL-001`. The release +completeness gate reads those as *not done* when their V is in fact closed. That is a +gate that lies in the safe direction, but it still lies — and nothing prevents the +drift recurring. + +## Scope + +### DEPTH — close the tracks the safety case rests on + +**D1. T4: close the static-WCET V (`VER-OS-WCET-001`).** +`REQ-OS-WCET-001` is implemented (synth sound static WCET on gale objects, "T4 first +light", #197) but its V was never closed. Produce the WCET evidence artifact over the +trusted sliver (switch + MPU program + HM), state the soundness argument and its +assumptions honestly, and record what is *bound* vs *measured* (DWT high-water-mark is +**not** cert-grade WCET — that distinction stays explicit). + +**D2. T2: object-code verification first light (`REQ-OS-OBJVERIFY-001`).** +The premise of the whole BUILD decision (DD-OS-BUILD-001) is *checkable certificates at +every layer* — including codegen. Today the wasm→native dissolve is **differentially +trusted, not proven equivalent**. First light = pick the smallest trusted object (the +dissolved switch or an MPU-program core), and produce a per-rule or +binary-translation-level check that the emitted object refutes-or-confirms against the +wasm semantics, with the residual gap stated. Upstream synth has been maturing exactly +this (WasmCert-Coq anchor, Rocq ISA model, VCR-VER); this workstream is gale's side of +that seam. + +**D3. Traceability completeness + a gate that keeps it true.** +Promote the 12 lagging requirements whose V is closed, then add a **CI gate** that fails +when a requirement's `VER-*` is `verified` while the requirement itself is not — the +same shape as the gale#214 WIT-drift gate, so this class of drift cannot recur silently. +This is the cheapest high-value item in the release and it makes every other claim +auditable. + +**D4 (stretch). T3: compositional schedulability bridge (`REQ-OS-SCHED-001`).** +Machine-checked inner-responsiveness under the outer partition schedule, via the spar +modal-filtered scheduling analysis already in the toolchain. Stretch because it needs +the spar bridge wired, not just a proof written. + +### BREADTH — how far the seam reaches + +**B1. Fused gale-nano `gust:os` component (gale#224) — consumer breadth.** +The v0.5.1 demonstrator publishes a *provider* component (time) as signed OCI + +wasm.directory. B1 generalizes it to the real deliverable: one self-contained component +(executor + capability providers + msgq/mutex/sem) that **exports `gust:os`** with +residual imports **exactly `gust:hal`**, per DD-OS-DELIVERY-001. Acceptance is the +delivery invariant, mechanically checked. This is the multi-consumer story — the first +consumer is already waiting, more follow. + +**B2. A third target family — retarget breadth.** +The AADL target model is silicon-validated on STM32G474 + STM32F100 (same vendor, two +families). B2 proves the *retarget* claim by adding a genuinely different target through +the model (a Cortex-M7-class or RISC-V part), with generated constants/`memory.x`/WIT and +no firmware edits. Silicon if a board is at hand; honestly scoped as model+build-only if +not. + +**B3 (stretch). Capability breadth: secure-boot on-ramp (gale#164) or on-target +loading (gale#161).** One new capability class beyond the current iodev set — chosen by +which unblocks the most downstream, not by novelty. + +## Committed scope: all seven workstreams + +D1–D4 and B1–B3 are all **in scope** for v0.6.0 — the full breadth × depth cut. The +stretch labels above are retained only as *risk markers*, not as permission to drop the +item. + +**The discipline that makes "everything" safe:** scope is committed, but *claims are +not*. Each workstream closes with whatever it actually established — and where the +honest result is "first light with a residual gap" or "model-only, no silicon", that is +what the notes say. An item is never dropped silently, and never inflated to look +closed. If a workstream cannot close honestly by tag time, it ships **with its gap +stated** and its rivet artifact left at the status the evidence supports. + +## Sequence + +`D3` (traceability gate — makes everything else auditable) → `D1` (close T4's V) → +`B1` (fused component) → `B2` (third target) → `D2` (object-code first light) → +`D4` (schedulability bridge) → `B3` (new capability class) → consolidate + tag. + +D3 first is deliberate: until the gate tells the truth, "is v0.6.0 cuttable?" is not a +question rivet can answer. D2 and D4 are sequenced late because they are the two +research-shaped tracks — if either runs long, it is visible as a gap in a release that +is already carrying five closed workstreams, rather than blocking the tag. + +## Exit criteria (the tag is cut only when all hold) + +1. All workstream PRs merged green — never over a real red; infra flakes re-run with a + root-cause, not dismissed. +2. `rivet validate` clean; **no requirement whose V is closed is left un-promoted** (D3's + gate green), and every artifact claimed in the notes traces to a verified V. +3. T4's V closed (D1). T2 has first light with its residual gap **stated, not implied** + (D2). +4. The fused component satisfies the delivery invariant mechanically (exports `gust:os`, + residual imports exactly `gust:hal`) — checked in CI, not by inspection. +5. Silicon claims name the board and the captured value; anything emulated is labelled + emulated. +6. Dissolves ≠ verified: every dissolved artifact is Kani-, probe-, gate- or + silicon-anchored, and the wasm→native trust residual is stated wherever it applies. + +## Kill-criteria + +- **D2:** if object-code verification on the smallest trusted object cannot produce a + *checkable* artifact (only a re-assertion of the differential test), it is NOT first + light — say so, keep the differential-trust wording, and carry T2 forward rather than + claiming a layer that does not exist. +- **B1:** if the fused component cannot reach residual-`gust:hal`-only (a scheduler or + heap import leaks), it is not the consumable unit — publish nothing and report the + leak, rather than shipping a component that only looks self-contained.