docs(release): v0.6.0 plan — 'Reach and Rigor' (breadth × depth)

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.