docs: DSLTrans cutoff analysis + Forge protocol + v0.9.x milestone draft (#215)

Three docs-only deliverables wrapping the v0.9.x cycle:

- docs/research/cutoff-theorem-modal-filtering.md applies Lucio's
  Cutoff Theorem (arXiv 2604.18792) to spar's modal filter, derives
  K_filter = 1 + max(C, E), gives a discharge plan (Kani / proptest),
  and is honest about where the theorem does NOT apply (negatives,
  cartesian-product SOM enumeration, fixed-point downstream passes,
  mode reachability).
- docs/research/forge-replication-protocol.md + the
  forge-replication/ scaffold (descriptor.sexp, descriptor.aadl,
  tasks.json with 24 paired tasks, run_trial.sh, empty RESULTS.md)
  mirror Jin et al. (arXiv 2604.13108) for a self-target replication
  on spar. Pre-registration discipline; no numbers reported.
- docs/blog/v0.9.x-milestone.md recaps v0.9.0..v0.9.3 (MCP +
  spar-insight; gPTP epsilon + frame quantization; RTA->WCTT
  coupling, Context_Switch_Time, sensitivity, ARINC severity;
  piecewise-affine arrival curves + PMOO/LUDB) and previews the
  v0.10.x trace-topology rollout (4 parsers, 5 checks, v1 contract
  URL).

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: avrabe

docs/blog/v0.9.x-milestone.md

@@ -0,0 +1,290 @@
+# v0.9.x milestone: NC kernel honesty, RTA→WCTT coupling, and a peek at v0.10.0 trace-topology
+
+Status: **draft** — milestone wrap-up for the v0.9.x cycle.
+Last update: 2026-05-10.
+Audience: spar users tracking releases, OEMs comparing against
+commercial NC arms, anyone hunting the v0.10.0 trace-topology
+foundation.
+
+> **Why care.** Between 2026-04-29 (v0.9.0) and 2026-05-10 (v0.9.3),
+> spar grew an MCP server, a runtime-trace assistant, and four
+> reviewer-driven tightness passes on the Network-Calculus kernel.
+> The output is byte-identical to v0.8.1 when the new properties are
+> unset — every change is opt-in or only flips a previously
+> optimistic bound. End-state: 2,900+ tests across 19 crates, 131
+> predeclared properties, four Lean theorem-statement skeletons
+> filed for v1.0.0 discharge, and the v0.10.0 trace-topology
+> foundation merged with four runtime-artefact parsers in tree.
+
+---
+
+## What landed in v0.9.x
+
+Four releases, each with a sharp focus.
+
+### v0.9.0 — MCP + spar-insight
+
+(see [CHANGELOG.md](../../CHANGELOG.md#090--2026-04-29))
+
+LLM agents got first-class access to the move-oracle via a JSON-RPC
+2.0 MCP server (`spar mcp serve`, or the standalone `spar-mcp`
+binary). Three tools, all `readOnlyHint: true` and
+`idempotentHint: true`:
+
+- `spar.verify_move` — single hypothetical-rebinding check.
+- `spar.enumerate_moves` — design-space exploration with
+  multi-objective ranking (`max-response | total-load |
+  total-power | total-weight | balanced`).
+- `spar.check_chain` — end-to-end latency breakdown for a flow
+  chain.
+
+The deterministic-apply path stays CLI-exclusive by design: there is
+no `spar.apply_move` over MCP, ever. LLM agents propose, spar
+verifies deterministically, the apply path is replayable from the
+command line. The certification chain stays inside spar.
+
+`spar-insight` (Track G) shipped alongside as the runtime-trace
+discrepancy assistant. Five rules on probe-point CTF traces from
+Zephyr: `WcetViolated`, `BcetUnderestimated`, `MeanDrift`,
+`MissingProbe`, `UnobservedProbe`. Binary CTF and ITM/SWO ingest
+deferred to a v0.9.x follow-up.
+
+### v0.9.1 — NC kernel soundness (Tier-2 reviewer items)
+
+(see [CHANGELOG.md](../../CHANGELOG.md#091--2026-04-29))
+
+The v0.8.1 TSN bounds were *technically optimistic* in two ways. PR
+[#186](https://github.com/pulseengine/spar/pull/186) closed both:
+
+- **gPTP sync-error ε.** The new `Spar_TSN::Sync_Error` property
+  feeds the TAS dispatch in `wctt.rs`: ε subtracts from the
+  effective open time and inflates the worst-case gate latency.
+  Without ε, a frame could miss its window by ε in silicon — an
+  unsound NC reading.
+- **Atomic-frame quantization.** `wctt.rs` now adds
+  `ceil(max_frame_bytes · 8e12 / link_rate_bps)` ps per hop on the
+  TAS and FIFO/Priority arms. Bytes-level NC under-counts by up to
+  one MTU per hop because frames are atomic.
+
+Both changes are byte-identical to v0.8.1 when the new properties
+are unset (ε = 0, default `Max_Frame_Size`). Users who calibrated
+against v0.8.1 numbers will see ≈ +12.144 µs per 1 Gbps hop with
+1518 B MTU — the `WcttFrameQuantization` Info diagnostic flags
+exactly where.
+
+### v0.9.2 — Honesty + tightness, sensitivity, ARINC severity
+
+(see [CHANGELOG.md](../../CHANGELOG.md#092--2026-05-03))
+
+Six PRs. The highlights for users:
+
+- **RTA→WCTT release-jitter coupling
+  ([#199](https://github.com/pulseengine/spar/pull/199)).** When a
+  stream source declares `Timing_Properties::Dispatch_Jitter`,
+  that J is now treated as ingress release-jitter and inflates the
+  arrival burst σ by `ρ·J` bytes. Single biggest credibility lift
+  in the v0.9.x cycle — closes the reviewer's NC top-5 item #4.
+- **WCTT sensitivity output
+  ([#196](https://github.com/pulseengine/spar/pull/196)).** Every
+  `WcttBound` Info is now followed by a `WcttSensitivity` Info
+  carrying worst-hop partial derivatives
+  `∂σ_self / ∂ρ_competing / ∂T_link`. Pure post-processing on the
+  closed-form. Reviewer NC top-5 item #13: cheapest workflow win,
+  turns spar from judge into design partner.
+- **Context_Switch_Time in RTA recurrence
+  ([#198](https://github.com/pulseengine/spar/pull/198)).** v0.8.x
+  emitted a STPA-REQ-022 advisory if `Context_Switch_Time` was
+  unset, then quietly used B=0 when it was set. Now the value
+  inflates each thread's WCET by `2 × Context_Switch_Time` per
+  Buttazzo §7 (one preemption-in + one preemption-out).
+- **CBS user-tunable Hi/Lo Credit
+  ([#195](https://github.com/pulseengine/spar/pull/195)).** v0.8.1
+  hardcoded both credits to `Max_Frame_Size`. Real Qcc/YANG configs
+  carry these per traffic class; now they are honoured.
+- **ARINC-PARTITION-ISOLATION promoted to Error.** Per DO-297
+  spatial-isolation invariant. New `--allow
+  arinc-partition-isolation` for legitimate IMA bypasses.
+
+Tier A reviewer items #5/#6/#8/#9/#13 closed in one release.
+
+### v0.9.3 — Piecewise-affine arrival curves + PMOO/LUDB
+
+(see [CHANGELOG.md](../../CHANGELOG.md#093--2026-05-10))
+
+Two PRs, both reviewer NC top-5 closeouts:
+
+- **Piecewise-affine arrival curves
+  ([#204](https://github.com/pulseengine/spar/pull/204)).** New
+  `PiecewiseAffineArrivalCurve` alongside the affine form.
+  Multi-leaky-bucket `(σ₁, ρ₁) ∧ (σ₂, ρ₂) ∧ …` exactly captures
+  "burst of N frames at line rate, then sustained at 100 Mbps" —
+  the canonical T-SPEC pattern in real ADAS/TSN traffic. Operators
+  take the min over buckets, which is the mathematically tight
+  choice. Reviewer NC top-5 item #1.
+- **PMOO/LUDB tree-shaped multiplexing
+  ([#203](https://github.com/pulseengine/spar/pull/203)).** New
+  `ludb_bound(tagged, competing, services)` for the
+  zonal/automotive pattern. Numerical confirmation: **27.4 %
+  tighter than SFA** on a 3-hop / 3-competing test, **23.7 %
+  tighter** on 5-source zonal aggregation. Closes the "spar says
+  31.7 ms vs RTaW says 8 ms" credibility gap on tree topologies.
+  Reviewer NC top-5 item #2.
+
+That makes 5/5 reviewer NC top-5 items closed across v0.9.1 / v0.9.2
+/ v0.9.3. The post-v0.9.0 reviewer narrative is now: NC arm has
+parity with RTaW-Pegase on the workloads where bounds matter most.
+
+---
+
+## DSLTrans-style cutoff analysis on modal filtering
+
+Lucio's recent Cutoff Theorem (arXiv
+[2604.18792](https://arxiv.org/abs/2604.18792)) proves that bounded
+model checking is *complete* for a precise DSLTrans fragment plus
+positive existence / traceability properties — turning an
+otherwise-infinite search into a finite computable bound. The
+benchmark line in that paper is sharp: 552 properties proved, 345
+counterexamples, 2 undecided across 29 transformations.
+
+We asked: does this apply to spar's **modal filtering** pass — the
+helpers in `crates/spar-analysis/src/modal.rs` that project a
+`SystemInstance` to the components and connections active in a given
+System Operational Mode?
+
+Short answer: **yes for the positive case, no for the rest.** The
+filter is non-recursive, has no negation in matchers, and is
+layered (component filter and connection filter are independent),
+so it fits the fragment. For the property *"every element declared
+`in modes (s)` is preserved in the SOM-projection"*, the cutoff
+bound is concrete and small:
+
+```
+K_filter  =  1  +  max(C, E)
+```
+
+where `C` is the largest `in_modes` list on any component and `E`
+the same for any connection. On `test-data/parser/modes_test.aadl`
+that gives **K = 3** — three mode-name labels per element suffice to
+exhaust the filter's behavioural equivalence classes.
+
+The theorem does **not** apply to: negative properties ("no inactive
+connection appears"); the cartesian-product SOM enumeration itself
+(`|SOMs| = ∏ |modes(c)|` is exponential in the input, not a
+verification artefact); fixed-point downstream passes (RTA
+recurrence, WCTT chain compose); and mode reachability (a graph
+reachability problem, deliberately exported to NuSMV via
+`mode_reachability::export_smv`).
+
+Full analysis with discharge plan (Kani harness vs capped proptest):
+[`docs/research/cutoff-theorem-modal-filtering.md`](../research/cutoff-theorem-modal-filtering.md).
+
+---
+
+## Forge-style navigation evidence — protocol shipped, trials pending
+
+Jin et al. (arXiv
+[2604.13108](https://arxiv.org/abs/2604.13108)) reported that
+conditioning an LLM agent with an architecture descriptor reduces
+navigation steps by **33–44 %** (Wilcoxon p=0.009, Cohen's d=0.92)
+on a controlled 24-task × 4-condition benchmark. Auto-generated
+descriptors hit 100 % accuracy vs 80 % blind on a separate 15-task
+artefact-vs-process arm. S-expressions detected all structural
+completeness errors where JSON failed atomically and YAML silently
+corrupted ~50 % of errors.
+
+We mirror Jin's protocol on spar itself: 24 paired tasks, two arms
+(C0: no descriptor; C1: with `descriptor.sexp`), Wilcoxon
+signed-rank with α=0.05. The scaffolding is in tree:
+
+- `docs/research/forge-replication/descriptor.sexp` — S-expression
+  descriptor of the spar workspace.
+- `docs/research/forge-replication/tasks.json` — 24 code-localization
+  tasks pinned to commit `bad85e6`.
+- `docs/research/forge-replication/run_trial.sh` — bash trial runner
+  that drives `claude --print --output-format stream-json` and
+  scores transcripts.
+- `docs/research/forge-replication/RESULTS.md` — empty results
+  template with pre-registration prompts.
+
+We have not run trials. Numbers will land in `RESULTS.md` once the
+user (or a community contributor) drives the scaffolding. The
+protocol document is honest about deviations from Jin's setup
+(self-target confound, hand-curated descriptor, no field-study arm).
+Pre-registration is the discipline; we record it in `RESULTS.md`
+before any trial fires.
+
+Full protocol:
+[`docs/research/forge-replication-protocol.md`](../research/forge-replication-protocol.md).
+
+---
+
+## What's next: v0.10.0 trace-topology
+
+(design:
+[`docs/designs/v0.10.0-trace-topology.md`](../designs/v0.10.0-trace-topology.md))
+
+v0.10.0 ships the foundation for `spar trace topology`: the
+runtime/declared reconciler that asks *"does the AADL declaration
+match the wire?"* on a real OEM deployment.
+
+Four parsers, all now landed:
+
+- **PCAPNG FrameSource**
+  ([#210](https://github.com/pulseengine/spar/pull/210)) — Tier 1
+  L2 frame ingest from `tcpdump -w` / Wireshark captures.
+- **LLDP JSON TopologySource**
+  ([#208](https://github.com/pulseengine/spar/pull/208)) — neighbor
+  adjacency from `lldpctl -f json`.
+- **Qcc YANG ConfigSource** — TSN switch config from
+  NETCONF/RESTCONF.
+- **gPTP JSON PtpTimeSource**
+  ([#211](https://github.com/pulseengine/spar/pull/211)) —
+  per-port ε from gPTP logs.
+
+Five deterministic checks on the parsed-vs-declared diff:
+
+- `IdentityUnknown` — runtime saw an identity (MAC,
+  chassis-id/port-id, stream-handle, multicast group) the AADL
+  didn't declare.
+- `TopologyMissingWiring` — LLDP saw an adjacency without a
+  corresponding AADL `bus access` connection.
+- `ConfigDrift` — `Spar_TSN::Gate_Control_List` (and 7 sibling
+  properties) on the wire disagree with the declaration.
+- `GptpOutOfBudget` — observed ε exceeds the declared
+  `Spar_TSN::Sync_Error`. This is the soundness guard for v0.9.1's
+  TAS bounds: if it fires, the WCTT readings were optimistic.
+- `BinaryMismatch` — running image digest disagrees with the
+  declared one.
+
+Output: SARIF 2.1.0 + a signed in-toto v1.0 attestation. Predicate
+URL (the integration anchor for rivet, witness, and OEM internal
+certification kits):
+
+```
+https://pulseengine.eu/spar-trace-topology/v1
+```
+
+Phasing: v0.10.0 = foundation + parsers; v0.11.0 = engine + SARIF;
+v1.0 = signed attestation. Estimated total scope ~2 weeks per the
+external reviewer's v1 spec.
+
+---
+
+## Call to action
+
+- **Repo.** [pulseengine/spar](https://github.com/pulseengine/spar).
+- **v0.10.0 design doc.**
+  [`docs/designs/v0.10.0-trace-topology.md`](../designs/v0.10.0-trace-topology.md).
+- **Forge-trial contributors welcome.** The scaffold in
+  `docs/research/forge-replication/` is ready to run. If you have
+  cycles to drive 48 paired trials (24 × 2 arms) on a fresh agent,
+  please file the results.csv + transcripts as a PR against
+  `docs/research/forge-replication/RESULTS.md`.
+- **NC reviewer items.** Five of the post-v0.9.0 top-5 closed; the
+  follow-up list (multi-grouping LUDB LP, full RTA→WCTT
+  auto-propagation, `Interrupt_Overhead` per ISR firing) is logged
+  in the CHANGELOG's "Deferred" sections.
+
+Track the v0.10.x trace-topology rollout via the
+[milestone](https://github.com/pulseengine/spar/milestones) and the
+five-check reconciler engine landing in v0.11.0.