From 1a52863e1797697d2c8182302e1a4dc868862c1e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 06:01:39 +0200 Subject: [PATCH 1/7] fix(stpa): UCA uca-type vocab, host controllers, status enum (#303, v0.36) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drives rivet validate errors 77→39 (oracle-gated with the #570-fixed rivet) on three clearly-correct STPA-hygiene classes — no trace-model judgment: - rfc46-hazards.yaml: UCAs carried an undeclared `type:` field with off-vocabulary values; rename to the schema's required `uca-type:` and remap to the allowed set [not-providing, providing, too-early-too-late] (providing-causes-hazard→providing; too-early/too-late→too-early-too-late). Clears 12 missing-uca-type errors. - control-structure.yaml: model the 3 host/runtime controllers the UCAs issue from — "CM Runtime (embedded)", "Fiber Manager (host intrinsic)", "host-wit-bindgen" — so the `issued-by` links resolve. Clears 24 errors (12 dangling issued-by + 12 missing-controller-link). - loss-scenarios.yaml: status `fixed` is not in the lifecycle enum → LS-M-5 `verified` (cites regression test ls_m_5_*), LS-W-1 `implemented` (fix landed, no cited test). Clears 2 errors. Remaining 39 (GitHub-provenance links + 4 dangling caused-by-uca) follow. Co-Authored-By: Claude Opus 4.8 (1M context) --- safety/stpa/control-structure.yaml | 25 +++++++++++++++++++++++++ safety/stpa/loss-scenarios.yaml | 4 ++-- safety/stpa/rfc46-hazards.yaml | 24 ++++++++++++------------ 3 files changed, 39 insertions(+), 14 deletions(-) diff --git a/safety/stpa/control-structure.yaml b/safety/stpa/control-structure.yaml index 60c4915..e6745a1 100644 --- a/safety/stpa/control-structure.yaml +++ b/safety/stpa/control-structure.yaml @@ -223,6 +223,31 @@ controllers: - cabi_realloc indices in canon lower match importing component's allocator - All import names resolve to valid component instances + # --- Host / runtime controllers outside meld's direct authorship --- + # meld's fusion design must contain the UCAs these issue (RFC-46 resource + # & async hazards, RH-*). They live in the control structure as the + # issuers referenced by safety/stpa/rfc46-hazards.yaml UCA `issued-by`. + - id: "CM Runtime (embedded)" + name: Embedded Component-Model Runtime + type: automated + description: > + The embedded CM runtime that allocates and drops resource handles and + schedules async tasks in the fused module's execution environment. + Issues the RFC-46 resource-lifetime and task-scheduling control actions. + - id: "Fiber Manager (host intrinsic)" + name: Fiber Manager (host intrinsic) + type: automated + description: > + Host intrinsic that creates, suspends, and resumes the fibers backing + stackful async guest execution. Issues fiber lifecycle control actions. + - id: "host-wit-bindgen" + name: Host wit-bindgen (maps to syn/kiln) + type: automated + description: > + Host-side binding generator (syn/kiln in PulseEngine) that emits the + memory/encoding glue at the host/guest boundary. Issues the binding + control actions whose UCAs meld's multi-memory lowering must survive. + controlled-processes: - id: PROC-COMPONENT name: Component Binary Data diff --git a/safety/stpa/loss-scenarios.yaml b/safety/stpa/loss-scenarios.yaml index 28cd670..fdfcfae 100644 --- a/safety/stpa/loss-scenarios.yaml +++ b/safety/stpa/loss-scenarios.yaml @@ -3194,7 +3194,7 @@ loss-scenarios: process-model-flaw: > Wrapper assumes all imports use memory 0 because the original single-component wrapping only had one memory. - status: fixed + status: implemented fix: > Multi-memory WASI import lowering (PR #20). Per-import Memory(N) and Realloc(N) via import_memory_indices/import_realloc_indices. @@ -3290,7 +3290,7 @@ loss-scenarios: instantiation order. The component model spec allows multiple instantiations of the same module (with different import wiring), but the merger's index-space merging model does not account for this. - status: fixed + status: verified priority: critical fix: > Mitigated by detection-and-reject, the same pattern used for diff --git a/safety/stpa/rfc46-hazards.yaml b/safety/stpa/rfc46-hazards.yaml index b375594..7cb33a9 100644 --- a/safety/stpa/rfc46-hazards.yaml +++ b/safety/stpa/rfc46-hazards.yaml @@ -145,7 +145,7 @@ ucas: leaving a dangling reference that subsequent operations dereference. context: "Resource creation during component-to-component call" hazards: [RH-1] - type: not-providing + uca-type: not-providing - id: UCA-RT-2 controller: "CM Runtime (embedded)" @@ -154,7 +154,7 @@ ucas: active stream or future, causing use-after-free on next I/O. context: "Resource cleanup during async task completion" hazards: [RH-1, RH-6] - type: too-early + uca-type: too-early-too-late - id: UCA-RT-3 controller: "CM Runtime (embedded)" @@ -163,7 +163,7 @@ ucas: from multiple tasks without synchronization. context: "Multi-task stream I/O with shared buffer" hazards: [RH-6] - type: providing-causes-hazard + uca-type: providing - id: UCA-RT-4 controller: "CM Runtime (embedded)" @@ -172,7 +172,7 @@ ucas: apparent hang or timeout in the starved component's callers. context: "Task scheduling with multiple async components" hazards: [RH-6] - type: too-late + uca-type: too-early-too-late # --- Fiber Manager (host) --- - id: UCA-FM-1 @@ -182,7 +182,7 @@ ucas: that will execute on it, causing stack overflow during execution. context: "Fiber creation for async component call" hazards: [RH-2] - type: providing-causes-hazard + uca-type: providing - id: UCA-FM-2 controller: "Fiber Manager (host intrinsic)" @@ -191,7 +191,7 @@ ucas: memory or corrupting execution state. context: "Fiber resume after task completion" hazards: [RH-2] - type: providing-causes-hazard + uca-type: providing - id: UCA-FM-3 controller: "Fiber Manager (host intrinsic)" @@ -200,7 +200,7 @@ ucas: completion, causing a permanent resource leak and logical deadlock. context: "Fiber suspension waiting for stream data" hazards: [RH-6] - type: not-providing + uca-type: not-providing - id: UCA-FM-4 controller: "Fiber Manager (host intrinsic)" @@ -209,7 +209,7 @@ ucas: one component to observe another component's internal state. context: "Fiber-local state access during context switch" hazards: [RH-2] - type: providing-causes-hazard + uca-type: providing # --- host-wit-bindgen (maps to syn/kiln in PulseEngine) --- - id: UCA-HB-1 @@ -219,7 +219,7 @@ ucas: module, reading from or writing to the wrong component's memory. context: "Host calling guest export that takes pointer arguments" hazards: [RH-3] - type: providing-causes-hazard + uca-type: providing pulseengine-owner: syn/kiln - id: UCA-HB-2 @@ -229,7 +229,7 @@ ucas: host/guest boundary, passing invalid UTF-8 into guest memory. context: "Host passing string argument to guest function" hazards: [RH-3] - type: not-providing + uca-type: not-providing pulseengine-owner: syn/kiln - id: UCA-HB-3 @@ -239,7 +239,7 @@ ucas: offset, misinterpreting function signatures. context: "Host bindings initialization / module inspection" hazards: [RH-3] - type: providing-causes-hazard + uca-type: providing pulseengine-owner: syn/kiln - id: UCA-HB-4 @@ -250,7 +250,7 @@ ucas: memory 0 regardless of which component owns the data. context: "Host reading return values from guest export" hazards: [RH-3] - type: providing-causes-hazard + uca-type: providing pulseengine-owner: syn/kiln # --------------------------------------------------------------------------- From 2194f11157c8fb872ae97580ca0b18f216f431cc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 06:29:56 +0200 Subject: [PATCH 2/7] feat(aspice): stakeholder+system-req tier foundation (ADR-5, v0.36) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase 1 of the full ASPICE SWE tier migration (maintainer-chosen scope for v0.36). Authors the upstream tier the sw-req migration requires: - ADR-5: the migration plan — target tier (stakeholder-req→system-req→sw-req →sw-verification), the 44-SR→11-system-req map, and the phased, oracle-gated execution order. - system-requirements.yaml: STK-1/2 (stakeholder needs: functional equivalence; functional-safety fitness) + SYS-1..11 (system reqs grouping the SRs by pipeline stage), each deriving from a stakeholder-req. Additive — oracle (the #570-fixed rivet) holds at 39 errors, 0 from the new tier (+13 expected sys2-has-verification warnings). Phase 2 (flip 44 SRs requirement→sw-req + derived-from SYS-n + cited-source for #N provenance) and Phase 3 (typed sw-verification layer) follow. Co-Authored-By: Claude Opus 4.8 (1M context) --- safety/adr/ADR-5-aspice-tier-migration.md | 94 ++++++++++ safety/requirements/system-requirements.yaml | 186 +++++++++++++++++++ 2 files changed, 280 insertions(+) create mode 100644 safety/adr/ADR-5-aspice-tier-migration.md create mode 100644 safety/requirements/system-requirements.yaml diff --git a/safety/adr/ADR-5-aspice-tier-migration.md b/safety/adr/ADR-5-aspice-tier-migration.md new file mode 100644 index 0000000..d4e7d72 --- /dev/null +++ b/safety/adr/ADR-5-aspice-tier-migration.md @@ -0,0 +1,94 @@ +# ADR-5 — ASPICE SWE tier migration for the requirement model (#303, v0.36) + +**Status:** accepted (design) — execution in progress +**Date:** 2026-06-24 +**Supersedes the model choice in:** #303 / SR-44 enforcement discussion + +## Context + +v0.36 enforces requirement→verification traceability. The chosen approach +(maintainer decision, 2026-06-24) is the **full ASPICE SWE tier migration**, +not a generic-`requirement` clean-up. The rivet `aspice@0.2.0` schema models +the V as a typed tier: + +``` +stakeholder-req (SYS.1) + └─derives-from→ system-req (SYS.2) [derived-from REQUIRED] + └─derives-from→ sw-req (SWE.1) [derived-from → system-req REQUIRED] + ←verifies─ sw-verification (SWE.6) [verifies → sw-req REQUIRED on the verification] +``` + +Hard (error-level) constraints from the schema: +- every `system-req` MUST `derives-from` a `stakeholder-req` (one-or-many); +- every `sw-req` MUST `derives-from` a `system-req` (or `system-arch-component`); +- a `sw-verification` MUST `verifies` a `sw-req`. +- `swe1-has-verification` (every sw-req verified) is **warning** severity — so + the verification layer is needed for V-closure but does not block `validate`. + +meld today has 44 `type: requirement` SRs (deriving from STPA `CC-*`/`LS-*`), +no stakeholder/system tier, and verification encoded as free-text +`fields.verification-method` (not typed `sw-verification`). + +## Decision + +Migrate to the ASPICE tier in phases, oracle-gated on `rivet validate` (run +with the #570-fixed rivet) after each phase. + +### Proposed hierarchy + +**Stakeholder requirements (2):** +- `STK-1` — Fused output is functionally equivalent to the composed input. +- `STK-2` — Fused output is fit for functional-safety deployment (traceable, + attested, deterministic, sound-by-construction). + +**System requirements (11)** — each `derives-from` a stakeholder-req; every SR +maps to exactly one: + +| sys-req | theme | SRs | +|---|---|---| +| SYS-1 | Faithful component ingestion (parse) | SR-1,2,3,4,6 | +| SYS-2 | Sound index-space merging | SR-5,7,8,9,10,11,26,31 | +| SYS-3 | Correct Canonical-ABI cross-component adapters | SR-12,13,14,15,16,17,18,22,23,24,25,40,41,42 | +| SYS-4 | Valid component wrapping / output | SR-21 | +| SYS-5 | Async / P3 fusion support | SR-32,33,34,43 | +| SYS-6 | Memory-strategy / isolation soundness | SR-37 | +| SYS-7 | DWARF debug-info preservation | SR-35,36,38 | +| SYS-8 | Cross-input linking (import internalisation) | SR-39 | +| SYS-9 | Deterministic, fail-fast operation | SR-19,20 | +| SYS-10 | Attestation integrity | SR-27,28,29,30 | +| SYS-11 | Traceability / verification governance | SR-44 | + +STK-1 ← SYS-1,2,3,4,5,7,8; STK-2 ← SYS-6,9,10,11 (a sys-req derives from one +stakeholder-req; the split is by "equivalence" vs "safety-fitness"). + +### Phases (each oracle-gated) + +0. **Prerequisite hygiene** (mostly done — 77→39): UCA `uca-type`, host + controllers, status enum (commit 1a52863). Remaining: 4 dangling + `caused-by-uca` (author UCA-F-2/F-3/CP-1 — STPA, tracked separately) and + the GitHub-issue provenance links (handled in Phase 2's per-SR pass). +1. **Foundation** (this ADR's companion commit): author + `safety/requirements/system-requirements.yaml` with STK-1/2 + SYS-1..11. + Additive; adds no errors (only `sys2-has-verification` warnings). +2. **Flip** (per-SR pass over `safety-requirements.yaml`): `type: requirement` + → `type: sw-req`; add `derived-from → SYS-n` per the map; convert the + `tracked-by: "#N"` / `derives-from: "#N"` GitHub refs to `cited-source` + (kind: github) — preserving provenance, removing the dangling/undeclared + links. Drives the remaining errors down; surfaces the sw-req coverage + warnings. +3. **Verification layer** (V-closure): author typed `sw-verification` artifacts + from the existing `verification-matrix` data (`verifies → SR-n`, + `method: automated-test|formal-verification|...`). Clears the + `swe1-has-verification` warnings; closes the right side of the V. +4. **Gate**: wire `rivet validate` (must pass) as the v0.36 enforcement gate + once rivet releases the #570 fix and meld's CI consumes it. + +## Consequences + +- Strongest standards alignment (ASPICE SWE.1/.6); requirement→verification + becomes a typed, enforced trace, not a rendered matrix. +- Largest effort: ~13 new tier artifacts + 44 SR rewrites + ~N verification + artifacts; multi-phase, each verified against the oracle. +- The `cited-source` choice for GitHub issues is deliberate: issues are not + trace-graph artifacts, so provenance belongs in `cited-source`, not in + `derives-from`/`tracked-by` edges. diff --git a/safety/requirements/system-requirements.yaml b/safety/requirements/system-requirements.yaml new file mode 100644 index 0000000..b03bf40 --- /dev/null +++ b/safety/requirements/system-requirements.yaml @@ -0,0 +1,186 @@ +# System & Stakeholder requirements — ASPICE SYS.1 / SYS.2 tier +# +# The upstream tier for meld's software requirements (safety-requirements.yaml, +# being migrated requirement → sw-req per ADR-5). Each system-req derives from a +# stakeholder need; each sw-req (SWE.1) derives from exactly one system-req. +# +# Format: rivet generic-yaml (types from the aspice schema). + +artifacts: + + # ── Stakeholder requirements (SYS.1) ────────────────────────────────────── + - id: STK-1 + type: stakeholder-req + title: Fused output is functionally equivalent to the composed input + description: > + A meld-fused core module shall behave observably identically to the + original composed P2/P3 component graph it was produced from, for every + supported input. + status: approved + fields: + priority: critical + source: PulseEngine toolchain charter (static component fusion, RFC-46) + + - id: STK-2 + type: stakeholder-req + title: Fused output is fit for functional-safety deployment + description: > + A meld-fused module shall be suitable for use in functional-safety + contexts: its construction shall be traceable and attestable, its output + deterministic, and unsafe states shall fail by construction rather than + silently. + status: approved + fields: + priority: critical + source: PulseEngine functional-safety positioning (ASIL/SIL targets) + + # ── System requirements (SYS.2) ─────────────────────────────────────────── + - id: SYS-1 + type: system-req + title: Faithful component ingestion + description: > + meld shall parse composed components completely and correctly — every + core module, import/export, ABI element size, and copy-layout class — and + reject malformed input rather than mis-parse it. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-2 + type: system-req + title: Sound index-space merging + description: > + meld shall merge component index spaces (functions, memories, tables, + types, segments, instantiation order) without collision or mis-offset, + including detection of multiply-instantiated modules. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-3 + type: system-req + title: Correct Canonical-ABI cross-component adapters + description: > + meld shall emit Canonical-ABI adapters that correctly transfer values + across the internalised component boundary — pointer/list/string copies, + transcoding, retptr layouts, realloc/memory targeting, resource handles, + with machine-checked layout invariants. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-4 + type: system-req + title: Valid component wrapping and output + description: > + meld shall wrap the fused core module into a valid output artifact whose + structure matches downstream-tool expectations. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-5 + type: system-req + title: Async / P3 fusion support + description: > + meld shall fuse P3 async constructs — stackful lifting, cross-component + stream bridging, opaque-rep resource drop — preserving their runtime + semantics. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-6 + type: system-req + title: Memory-strategy and isolation soundness + description: > + meld shall select a memory strategy that is sound by construction for the + input, preserving inter-component isolation (multi-memory structural + isolation as the committed model, per ADR-4). + status: approved + fields: + req-type: safety + links: + - type: derives-from + target: STK-2 + + - id: SYS-7 + type: system-req + title: DWARF debug-info preservation + description: > + meld shall preserve and correctly relocate DWARF debug information across + the merge, including multi-source merge and synthesised DIEs for + meld-generated adapter functions. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-8 + type: system-req + title: Cross-input linking (import internalisation) + description: > + meld shall link separately-supplied inputs by internalising cross-input + imports into intra-module calls. + status: approved + fields: + req-type: functional + links: + - type: derives-from + target: STK-1 + + - id: SYS-9 + type: system-req + title: Deterministic, fail-fast operation + description: > + meld shall produce byte-deterministic output for identical input and + shall fail fast on unresolvable state rather than emit a degraded module. + status: approved + fields: + req-type: constraint + links: + - type: derives-from + target: STK-2 + + - id: SYS-10 + type: system-req + title: Attestation integrity + description: > + meld shall record a complete, round-trippable attestation binding the + input hash, configuration, and output hash of each fusion. + status: approved + fields: + req-type: safety + links: + - type: derives-from + target: STK-2 + + - id: SYS-11 + type: system-req + title: Traceability and verification governance + description: > + meld's requirements shall trace to typed verification measures, enforced + mechanically (the ASPICE SWE tier, this migration). + status: approved + fields: + req-type: constraint + links: + - type: derives-from + target: STK-2 From 60d552eb9f811875fa1b7f449dec24e330c62cce Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 12:38:50 +0200 Subject: [PATCH 3/7] =?UTF-8?q?feat(aspice):=20flip=2044=20SRs=20requireme?= =?UTF-8?q?nt=E2=86=92sw-req,=20ASPICE=20tier=20+=20STPA=20trace=20(ADR-5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase 2 of the ASPICE SWE tier migration. Drives rivet validate 38→4 errors (only the 4 caused-by-uca STPA danglers remain). Per ADR-5 + the maintainer's "keep granular STPA trace on sw-reqs" decision: - All 44 SRs: type requirement → sw-req; each gains derived-from → SYS-n (the system-req from system-requirements.yaml) per the ADR map. - STPA links reclassified to schema-valid types, preserving every requirement's exact safety motivation: derives-from CC-*/SC-* → addresses-constraint (declared, meld-local) derives-from LS-* → mitigates (existing) derives-from SR-* → depends-on (existing) - GitHub-issue provenance (derives-from/tracked-by "#N") → cited-source (kind: github) — issues are not trace-graph artifacts. - schemas/meld-local.yaml: declares addresses-constraint + supersedes-default-of link types; registered in rivet.yaml. Verified with the #570-fixed rivet (4 errors, 121 warnings; the 44 swe1-has-verification warnings are Phase 3 — the typed sw-verification layer). Co-Authored-By: Claude Opus 4.8 (1M context) --- rivet.yaml | 1 + safety/requirements/safety-requirements.yaml | 353 +++++++++++++------ schemas/meld-local.yaml | 26 ++ 3 files changed, 263 insertions(+), 117 deletions(-) create mode 100644 schemas/meld-local.yaml diff --git a/rivet.yaml b/rivet.yaml index cc27551..16f70d2 100644 --- a/rivet.yaml +++ b/rivet.yaml @@ -10,6 +10,7 @@ project: - stpa - aspice - dev + - meld-local sources: - path: safety/stpa diff --git a/safety/requirements/safety-requirements.yaml b/safety/requirements/safety-requirements.yaml index 7502144..e679172 100644 --- a/safety/requirements/safety-requirements.yaml +++ b/safety/requirements/safety-requirements.yaml @@ -20,7 +20,7 @@ artifacts: # ========================================================================== - id: SR-1 - type: requirement + type: sw-req title: Complete core module extraction description: > The parser shall extract all core modules from a component, @@ -29,8 +29,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-1 + - type: addresses-constraint target: CC-P-1 - - type: derives-from + - type: mitigates target: LS-P-1 fields: implementation: meld-core/src/parser.rs @@ -41,7 +43,7 @@ artifacts: Parser completeness proof (proofs/parser/). - id: SR-2 - type: requirement + type: sw-req title: Complete import/export extraction description: > The parser shall extract every import and export entry declared @@ -50,6 +52,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-1 + - type: addresses-constraint target: CC-P-2 fields: implementation: meld-core/src/parser.rs @@ -59,7 +63,7 @@ artifacts: match wasmparser's independent count - id: SR-3 - type: requirement + type: sw-req title: Correct Canonical ABI element size computation description: > canonical_abi_element_size shall return the correctly aligned @@ -69,10 +73,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-1 + - type: addresses-constraint target: CC-P-3 - - type: derives-from + - type: addresses-constraint target: CC-P-5 - - type: derives-from + - type: mitigates target: LS-P-2 fields: implementation: meld-core/src/parser.rs @@ -85,7 +91,7 @@ artifacts: spec definition (proofs/parser/ or proofs/adapter/). - id: SR-4 - type: requirement + type: sw-req title: Reject malformed components description: > The parser shall reject components that do not pass wasmparser @@ -95,8 +101,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-1 + - type: addresses-constraint target: CC-P-6 - - type: derives-from + - type: mitigates target: LS-P-3 fields: implementation: meld-core/src/parser.rs @@ -110,7 +118,7 @@ artifacts: # ========================================================================== - id: SR-5 - type: requirement + type: sw-req title: Complete and correct import resolution description: > The resolver shall match every import to exactly one export with @@ -120,10 +128,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-R-1 - - type: derives-from + - type: addresses-constraint target: CC-R-3 - - type: derives-from + - type: mitigates target: LS-R-1 fields: implementation: meld-core/src/resolver.rs @@ -134,7 +144,7 @@ artifacts: Resolver correctness proof (proofs/resolver/). - id: SR-6 - type: requirement + type: sw-req title: Correct CopyLayout classification description: > The resolver shall classify each cross-component call parameter @@ -145,12 +155,14 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-1 + - type: addresses-constraint target: CC-R-2 - - type: derives-from + - type: addresses-constraint target: CC-R-4 - - type: derives-from + - type: addresses-constraint target: CC-R-5 - - type: derives-from + - type: mitigates target: LS-R-2 fields: implementation: meld-core/src/resolver.rs @@ -162,7 +174,7 @@ artifacts: (proofs/transformations/adapter/copy_layout_proofs.v). - id: SR-7 - type: requirement + type: sw-req title: Valid topological instantiation order description: > The resolver shall produce a topological order where every @@ -173,12 +185,14 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-R-6 - - type: derives-from + - type: addresses-constraint target: CC-R-7 - - type: derives-from + - type: mitigates target: LS-R-3 - - type: derives-from + - type: mitigates target: LS-R-4 fields: implementation: meld-core/src/resolver.rs @@ -193,7 +207,7 @@ artifacts: # ========================================================================== - id: SR-8 - type: requirement + type: sw-req title: Correct function base offset calculation description: > The merger shall compute each component's function base offset @@ -203,8 +217,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-M-3 - - type: derives-from + - type: mitigates target: LS-M-1 fields: implementation: meld-core/src/merger.rs @@ -215,7 +231,7 @@ artifacts: Merge layout correctness proof (proofs/transformations/merge/). - id: SR-9 - type: requirement + type: sw-req title: Complete instruction index rewriting description: > The rewriter shall remap indices in all instruction types that @@ -225,14 +241,16 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-M-2 - - type: derives-from + - type: addresses-constraint target: CC-M-4 - - type: derives-from + - type: addresses-constraint target: CC-M-8 - - type: derives-from + - type: mitigates target: LS-M-2 - - type: derives-from + - type: mitigates target: LS-M-3 fields: implementation: meld-core/src/rewriter.rs @@ -243,7 +261,7 @@ artifacts: Rewriter completeness proof (proofs/rewriter/). - id: SR-10 - type: requirement + type: sw-req title: Correct segment reindexing description: > The merger shall reindex data segment memory indices, element @@ -253,8 +271,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-M-5 - - type: derives-from + - type: addresses-constraint target: CC-M-6 fields: implementation: meld-core/src/segments.rs @@ -265,7 +285,7 @@ artifacts: Segment reindexing proof (proofs/segments/). - id: SR-11 - type: requirement + type: sw-req title: Component processing order matches resolver order description: > The merger shall process components in the same order as the @@ -274,6 +294,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-M-7 fields: implementation: meld-core/src/merger.rs @@ -286,7 +308,7 @@ artifacts: # ========================================================================== - id: SR-12 - type: requirement + type: sw-req title: Adapter generation for all pointer-passing cross-component calls description: > The adapter generator shall produce an adapter function for every @@ -297,6 +319,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-1 fields: implementation: meld-core/src/adapter/fact.rs @@ -306,7 +330,7 @@ artifacts: multi-memory mode produces adapter functions - id: SR-13 - type: requirement + type: sw-req title: Correct cabi_realloc targeting description: > The adapter shall call cabi_realloc using the post-merge function @@ -315,10 +339,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-2 - - type: derives-from + - type: addresses-constraint target: CC-A-6 - - type: derives-from + - type: mitigates target: LS-A-1 fields: implementation: meld-core/src/adapter/fact.rs @@ -328,7 +354,7 @@ artifacts: with list argument, verify callee receives correct data - id: SR-14 - type: requirement + type: sw-req title: Correct memory index usage in adapters description: > The adapter shall use the correct source and destination memory @@ -339,12 +365,14 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-4 - - type: derives-from + - type: addresses-constraint target: CC-A-9 - - type: derives-from + - type: mitigates target: LS-A-2 - - type: derives-from + - type: mitigates target: LS-A-4 fields: implementation: meld-core/src/adapter/fact.rs @@ -355,7 +383,7 @@ artifacts: Adapter memory index proof (proofs/adapter/). - id: SR-15 - type: requirement + type: sw-req title: Correct list copy length description: > The adapter shall compute list copy byte length as element_count @@ -364,6 +392,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-5 fields: implementation: meld-core/src/adapter/fact.rs @@ -374,7 +404,7 @@ artifacts: Copy length proof (proofs/adapter/). - id: SR-16 - type: requirement + type: sw-req title: Recursive inner pointer fixup description: > For list types whose elements contain pointer fields, the adapter @@ -386,12 +416,14 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-3 - - type: derives-from + - type: addresses-constraint target: CC-A-7 - - type: derives-from + - type: addresses-constraint target: CC-A-11 - - type: derives-from + - type: mitigates target: LS-A-3 fields: implementation: meld-core/src/adapter/fact.rs @@ -402,7 +434,7 @@ artifacts: Fixup loop termination and correctness proof (proofs/adapter/). - id: SR-17 - type: requirement + type: sw-req title: Correct string transcoding description: > String transcoding adapters shall produce valid output encoding @@ -412,6 +444,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-8 fields: implementation: meld-core/src/adapter/fact.rs @@ -441,7 +475,7 @@ artifacts: tests/async_cross_encoding.rs (#272, post-v0.31.0-audit). - id: SR-18 - type: requirement + type: sw-req title: Adapter instruction ordering description: > The adapter shall emit instructions in the correct order: @@ -451,6 +485,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-10 fields: implementation: meld-core/src/adapter/fact.rs @@ -464,7 +500,7 @@ artifacts: # ========================================================================== - id: SR-19 - type: requirement + type: sw-req title: Deterministic output description: > Given identical input component bytes and identical FuserConfig, @@ -473,8 +509,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-9 + - type: addresses-constraint target: SC-7 - - type: derives-from + - type: mitigates target: LS-CP-2 fields: implementation: meld-core/src/lib.rs @@ -483,7 +521,7 @@ artifacts: Run fusion twice with same inputs; assert byte-equal outputs - id: SR-20 - type: requirement + type: sw-req title: Fail-fast on unresolvable state description: > If any stage encounters an unresolvable error (unresolved import, @@ -494,8 +532,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-9 + - type: addresses-constraint target: SC-8 - - type: derives-from + - type: addresses-constraint target: SC-9 fields: implementation: meld-core/src/error.rs @@ -509,7 +549,7 @@ artifacts: # ========================================================================== - id: SR-21 - type: requirement + type: sw-req title: Valid P2 component wrapping description: > When OutputFormat::Component is selected, the wrapper shall produce @@ -521,12 +561,14 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-4 + - type: addresses-constraint target: CC-W-1 - - type: derives-from + - type: addresses-constraint target: CC-W-2 - - type: derives-from + - type: addresses-constraint target: CC-W-3 - - type: derives-from + - type: mitigates target: LS-W-1 fields: implementation: meld-core/src/component_wrap.rs @@ -536,7 +578,7 @@ artifacts: validate with wasm-tools, run through wasmtime - id: SR-22 - type: requirement + type: sw-req title: Conditional pointer copy for option/result/variant types description: > The adapter shall check the discriminant value of option, result, @@ -548,8 +590,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-12 - - type: derives-from + - type: mitigates target: LS-A-5 fields: implementation: meld-core/src/adapter/fact.rs @@ -559,7 +603,7 @@ artifacts: both Some and None values; verify correct behavior for each - id: SR-23 - type: requirement + type: sw-req title: Import deduplication type safety description: > The merger shall not deduplicate function imports that have the same @@ -570,10 +614,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-M-9 - - type: derives-from + - type: addresses-constraint target: CC-M-10 - - type: derives-from + - type: mitigates target: LS-M-4 fields: implementation: meld-core/src/merger.rs @@ -583,7 +629,7 @@ artifacts: import slots in multi-memory mode - id: SR-24 - type: requirement + type: sw-req title: Correct retptr layout for variant return types description: > The adapter shall copy retptr return values using the correct @@ -595,10 +641,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-13 - - type: derives-from + - type: addresses-constraint target: CC-R-9 - - type: derives-from + - type: mitigates target: LS-A-6 fields: implementation: @@ -611,7 +659,7 @@ artifacts: f64/i64 payloads via retptr; verify correct values - id: SR-25 - type: requirement + type: sw-req title: Resource handle pass-through description: > The adapter shall pass resource handles through cross-component calls @@ -621,6 +669,8 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-3 + - type: addresses-constraint target: CC-A-1 fields: implementation: meld-core/src/adapter/fact.rs @@ -630,7 +680,7 @@ artifacts: are valid after cross-component calls - id: SR-26 - type: requirement + type: sw-req title: Complete component type index tracking description: > The parser shall track all entries in the component type index space @@ -642,8 +692,10 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: CC-P-9 - - type: derives-from + - type: addresses-constraint target: CC-P-10 fields: implementation: meld-core/src/parser.rs @@ -662,7 +714,7 @@ artifacts: # ========================================================================== - id: SR-27 - type: requirement + type: sw-req title: Attestation input hash integrity description: > For every input component added to a fusion, the attestation shall @@ -675,6 +727,8 @@ artifacts: tags: [stpa-derived, attestation, supply-chain] links: - type: derives-from + target: SYS-10 + - type: addresses-constraint target: SC-6 - type: mitigates target: H-6 @@ -688,7 +742,7 @@ artifacts: size equals the actual byte length. - id: SR-28 - type: requirement + type: sw-req title: Attestation configuration completeness description: > The attestation metadata shall record every FuserConfig field @@ -703,6 +757,8 @@ artifacts: tags: [stpa-derived, attestation, supply-chain] links: - type: derives-from + target: SYS-10 + - type: addresses-constraint target: SC-6 - type: mitigates target: H-6 @@ -718,7 +774,7 @@ artifacts: asserting metadata.memory_strategy survives to JSON. - id: SR-29 - type: requirement + type: sw-req title: Attestation serialization round-trip description: > The attestation shall serialize to JSON and deserialize back with @@ -732,6 +788,8 @@ artifacts: tags: [stpa-derived, attestation, supply-chain] links: - type: derives-from + target: SYS-10 + - type: addresses-constraint target: SC-6 - type: mitigates target: H-6 @@ -746,7 +804,7 @@ artifacts: signature, output is valid non-empty JSON). - id: SR-30 - type: requirement + type: sw-req title: Attestation output hash integrity description: > The attestation shall record a SHA-256 hash and byte size of the @@ -758,6 +816,8 @@ artifacts: tags: [stpa-derived, attestation, supply-chain] links: - type: derives-from + target: SYS-10 + - type: addresses-constraint target: SC-6 - type: mitigates target: H-6 @@ -775,7 +835,7 @@ artifacts: # ========================================================================== - id: SR-31 - type: requirement + type: sw-req title: Multiply-instantiated module detection description: > The merger shall detect when the same core module is instantiated @@ -788,10 +848,12 @@ artifacts: tags: [stpa-derived] links: - type: derives-from + target: SYS-2 + - type: addresses-constraint target: SC-8 - - type: derives-from + - type: addresses-constraint target: SC-9 - - type: derives-from + - type: mitigates target: LS-M-5 fields: implementation: meld-core/src/merger.rs @@ -814,7 +876,7 @@ artifacts: # ========================================================================== - id: SR-32 - type: requirement + type: sw-req title: Stackful P3 lifting mode emission description: > In addition to the callback trampoline (shipped #128), meld shall @@ -833,9 +895,14 @@ artifacts: tags: [roadmap, p3-async, v0.8.0] links: - type: derives-from - target: "#94" - - type: tracked-by - target: "#140" + target: SYS-5 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/94" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/140" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/p3_async.rs # ABI foundation (Phase 1) @@ -852,7 +919,7 @@ artifacts: milestone: v0.8.0 - id: SR-33 - type: requirement + type: sw-req title: Cross-component `stream` fusion at merge time description: > When two fused components share a `stream` endpoint, meld shall @@ -872,9 +939,14 @@ artifacts: tags: [roadmap, p3-async, v0.29.0] links: - type: derives-from - target: "#94" - - type: tracked-by - target: "#141" + target: SYS-5 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/94" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/141" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/p3_bridge.rs @@ -911,7 +983,7 @@ artifacts: milestone: v0.29.0 - id: SR-34 - type: requirement + type: sw-req title: Static `stream` validation description: > Build-time validation passes for cross-component streams: @@ -930,11 +1002,16 @@ artifacts: tags: [roadmap, p3-async, v0.12.0, v0.21.0] links: - type: derives-from - target: "#94" - - type: tracked-by - target: "#142" + target: SYS-5 - type: depends-on target: SR-33 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/94" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/142" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/p3_stream.rs @@ -951,7 +1028,7 @@ artifacts: milestone: v0.21.0 - id: SR-35 - type: requirement + type: sw-req title: DWARF address remap into merged code section description: > A new `DwarfHandling::Remap` policy on `FuserConfig` shall rewrite @@ -965,11 +1042,16 @@ artifacts: tags: [roadmap, dwarf, witness-mc-dc, v0.10.0] links: - type: derives-from - target: "#130" - - type: tracked-by - target: "#143" + target: SYS-7 - type: supersedes-default-of target: LS-CP-4 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/130" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/143" + kind: github + last-checked: 2026-06-24 fields: implementation: meld-core/src/dwarf.rs verification-method: test+cross-repo @@ -980,7 +1062,7 @@ artifacts: milestone: v0.10.0 - id: SR-36 - type: requirement + type: sw-req title: Synthesised DWARF DIEs for meld-generated adapter functions description: > For every adapter function meld emits (cross-component lift/lower, @@ -1020,11 +1102,16 @@ artifacts: tags: [roadmap, dwarf, witness-mc-dc, v0.23.0, v0.24.0] links: - type: derives-from - target: "#130" - - type: tracked-by - target: "#144" + target: SYS-7 - type: depends-on target: SR-35 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/130" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/144" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/dwarf.rs @@ -1052,7 +1139,7 @@ artifacts: # verbatim from c50d9d5 in the v0.31.0 traceability audit, with status # upgraded implemented → verified on the recorded evidence. - id: SR-37 - type: requirement + type: sw-req title: Automatic memory-strategy resolution (sound-by-construction default) description: > `MemoryStrategy::Auto` — the default for both `FuserConfig` and the @@ -1072,10 +1159,14 @@ artifacts: status: verified tags: [usability, memory-strategy, v0.22.0] links: - - type: tracked-by - target: "#172" + - type: derives-from + target: SYS-6 - type: mitigates target: LS-M-7 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/172" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/memory_probe.rs @@ -1100,7 +1191,7 @@ artifacts: milestone: v0.22.0 - id: SR-38 - type: requirement + type: sw-req title: Multi-source DWARF merge (bounded relocator) description: > When more than one input core module carries `.debug_*` sections, @@ -1118,13 +1209,18 @@ artifacts: tags: [roadmap, dwarf, witness-mc-dc, v0.26.0] links: - type: derives-from - target: "#130" - - type: tracked-by - target: "#208" + target: SYS-7 - type: depends-on target: SR-35 - type: mitigates target: LS-D-3 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/130" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/208" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/dwarf.rs @@ -1142,7 +1238,7 @@ artifacts: milestone: v0.26.0 - id: SR-39 - type: requirement + type: sw-req title: Separate-input cross-component linking (import internalisation) description: > `meld fuse a.wasm b.wasm --component` shall resolve one input's @@ -1156,11 +1252,16 @@ artifacts: tags: [roadmap, composition, v0.28.0] links: - type: derives-from - target: "#94" - - type: tracked-by - target: "#212" + target: SYS-8 - type: mitigates target: LS-CP-6 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/94" + kind: github + last-checked: 2026-06-24 + - uri: "https://github.com/pulseengine/meld/issues/212" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/component_wrap.rs @@ -1175,7 +1276,7 @@ artifacts: milestone: v0.28.0 - id: SR-40 - type: requirement + type: sw-req title: Machine-checked Canonical-ABI layout invariants (Kani) description: > The canonical-ABI layout functions shall carry machine-checked @@ -1192,9 +1293,11 @@ artifacts: tags: [roadmap, proofs, v0.30.0] links: - type: derives-from - target: "#218" - - type: tracked-by - target: "#218" + target: SYS-3 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/218" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/abi_proofs.rs @@ -1223,7 +1326,7 @@ artifacts: milestone: v0.30.0 - id: SR-41 - type: requirement + type: sw-req title: Async cross-encoding string transcoding description: > Async-lift FACT adapters shall transcode string params and results @@ -1245,11 +1348,15 @@ artifacts: tags: [roadmap, async, transcoding] links: - type: derives-from + target: SYS-3 + - type: depends-on target: SR-17 - - type: tracked-by - target: "#272" - type: mitigates target: LS-F-27 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/272" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/adapter/fact.rs @@ -1290,7 +1397,7 @@ artifacts: milestone: post-v0.31.0 - id: SR-42 - type: requirement + type: sw-req title: Identity-trampoline adapter inlining description: > When a cross-component call edge resolves to a pure identity-trampoline @@ -1305,10 +1412,14 @@ artifacts: status: verified tags: [optimization, adapter, v0.34.0] links: - - type: tracked-by - target: "#304" - type: derives-from + target: SYS-3 + - type: depends-on target: SR-12 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/304" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/adapter/fact.rs @@ -1328,7 +1439,7 @@ artifacts: milestone: v0.34.0 - id: SR-43 - type: requirement + type: sw-req title: Opaque-rep resource drop-teardown soundness description: > A fused 3-component re-exporter chain whose intermediate exports an @@ -1344,10 +1455,14 @@ artifacts: status: verified tags: [bug, resource, opaque-rep, v0.35.0] links: - - type: tracked-by - target: "#305" - type: derives-from + target: SYS-5 + - type: depends-on target: SR-25 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/305" + kind: github + last-checked: 2026-06-24 fields: implementation: - meld-core/src/merger.rs @@ -1362,7 +1477,7 @@ artifacts: milestone: v0.35.0 - id: SR-44 - type: requirement + type: sw-req title: Enforced requirement->verification->test traceability description: > The V-model right side shall be a machine-enforced rivet trace, not inert @@ -1377,8 +1492,12 @@ artifacts: status: proposed tags: [process, traceability, verification, v0.36.0] links: - - type: tracked-by - target: "#303" + - type: derives-from + target: SYS-11 + cited-source: + - uri: "https://github.com/pulseengine/meld/issues/303" + kind: github + last-checked: 2026-06-24 fields: implementation: - safety/requirements/traceability.yaml diff --git a/schemas/meld-local.yaml b/schemas/meld-local.yaml new file mode 100644 index 0000000..36f293e --- /dev/null +++ b/schemas/meld-local.yaml @@ -0,0 +1,26 @@ +# Project-local schema extensions for meld. +# +# Additive (merged on top of common/stpa/aspice/dev). Declares the link types +# meld uses to keep its STPA safety trace on the ASPICE sw-reqs (ADR-5, +# option A): a software requirement that addresses an STPA safety constraint, +# and the one supersedes-default-of relation. Both are unrestricted global +# link types (like `mitigates`) so a sw-req may carry them alongside its +# ASPICE `derived-from`. + +schema: + name: meld-local + version: "0.1.0" + description: Project-local link-type extensions for meld (STPA×ASPICE trace). + +link-types: + - name: addresses-constraint + inverse: constraint-addressed-by + description: > + Source requirement addresses (is the realization of) an STPA controller + or system safety constraint. + - name: supersedes-default-of + inverse: default-superseded-by + description: > + Source requirement supersedes the default behaviour modelled by the + target (e.g. a new sound-by-construction default over a prior loss + scenario's default). From dca146990296f00734d17075c1e80c179ddb27f8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 13:02:57 +0200 Subject: [PATCH 4/7] feat(aspice): typed sw-verification layer for all 44 sw-reqs (ADR-5 Phase 3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the right side of the V — the enforcement payload of v0.36. Authors 44 typed sw-verification (SWE.6) artifacts, one per sw-req, each carrying its required `verifies` backlink and the concrete tests/proofs that discharge it (from traceability.yaml's verification-status block; 40 generated from that data, 4 stragglers — SR-18/42/43/44 — grounded in their actual tests: test_304_identity_direct_adapter_is_inlined, the resource_floats_opaque runtime oracle, the adapter-path runtime suite, and rivet validate itself for the governance req). requirement→verification is now a typed, mechanically-enforced trace, not a rendered matrix. Oracle (the #570-fixed rivet): 4 errors (only the caused-by-uca STPA danglers remain), 0 swe1-has-verification warnings — every sw-req verified. Co-Authored-By: Claude Opus 4.8 (1M context) --- safety/requirements/sw-verifications.yaml | 546 ++++++++++++++++++++++ 1 file changed, 546 insertions(+) create mode 100644 safety/requirements/sw-verifications.yaml diff --git a/safety/requirements/sw-verifications.yaml b/safety/requirements/sw-verifications.yaml new file mode 100644 index 0000000..a249542 --- /dev/null +++ b/safety/requirements/sw-verifications.yaml @@ -0,0 +1,546 @@ +# Software verification measures — ASPICE SWE.6 (sw-verification) +# +# Generated for the v0.36 ASPICE tier migration (ADR-5, Phase 3). One typed +# sw-verification per sw-req, carrying its `verifies` backlink and the +# concrete tests/proofs from traceability.yaml's verification-status block. +# This closes the right side of the V (clears swe1-has-verification). +# +# Format: rivet generic-yaml. + +artifacts: + + - id: SWV-1 + type: sw-verification + title: "Verification of SR-1: Complete core module extraction" + description: > + Verifies SR-1 via: tests `nested_component::test_parse_composed_component_structure`; proofs `proofs/parser/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-1 + + - id: SWV-2 + type: sw-verification + title: "Verification of SR-2: Complete import/export extraction" + description: > + Verifies SR-2 via: tests `release_components::test_no_duplicate_imports`; proofs `proofs/parser/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-2 + + - id: SWV-3 + type: sw-verification + title: "Verification of SR-3: Correct Canonical ABI element size computation" + description: > + Verifies SR-3 via: tests `parser::tests::test_canonical_abi_element_size_primitive_types`, `parser::tests::test_canonical_abi_element_size_string`, `parser::tests::test_canonical_abi_element_size_record_with_padding`, `parser::tests::test_canonical_abi_element_size_record_homogeneous`, `parser::tests::test_canonical_abi_align_values`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-3 + + - id: SWV-4 + type: sw-verification + title: "Verification of SR-4: Reject malformed components" + description: > + Verifies SR-4 via: tests `parser::tests::test_parser_rejects_core_module`, `parser::tests::test_parser_rejects_invalid_wasm`, `tests::test_fuser_rejects_core_module_input`, `tests::test_fuser_rejects_invalid_wasm`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-4 + + - id: SWV-5 + type: sw-verification + title: "Verification of SR-5: Complete and correct import resolution" + description: > + Verifies SR-5 via: tests `resolver::tests::test_resolver_strict_mode`, `resolver::tests::test_resolver_unresolved_import_error`; proofs `proofs/resolver/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-5 + + - id: SWV-6 + type: sw-verification + title: "Verification of SR-6: Correct CopyLayout classification" + description: > + Verifies SR-6 via: tests `resolver::tests::test_copy_layout_flat_list`, `resolver::tests::test_copy_layout_string_list`, `resolver::tests::test_copy_layout_record_with_string`, `resolver::tests::test_copy_layout_nested_list`, `resolver::tests::test_copy_layout_flat_record`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-6 + + - id: SWV-7 + type: sw-verification + title: "Verification of SR-7: Valid topological instantiation order" + description: > + Verifies SR-7 via: tests `resolver::tests::test_topological_sort_linear`, `resolver::tests::test_topological_sort_no_deps`, `resolver::tests::test_topological_sort_circular_fallback`, `resolver::tests::test_topological_sort_diamond`, `resolver::tests::test_resolver_preserves_order_stability`; proofs `proofs/resolver/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-7 + + - id: SWV-8 + type: sw-verification + title: "Verification of SR-8: Correct function base offset calculation" + description: > + Verifies SR-8 via: proofs `proofs/transformations/merge/`. + status: implemented + fields: + method: formal-verification + links: + - type: verifies + target: SR-8 + + - id: SWV-9 + type: sw-verification + title: "Verification of SR-9: Complete instruction index rewriting" + description: > + Verifies SR-9 via: tests `rewriter::tests::test_rewrite_memory_copy_rebased`, `rewriter::tests::test_rewrite_memory_fill_rebased`, `rewriter::tests::test_rewrite_memory_init_rebased`, `rewriter::tests::test_rewrite_memory_size_rebased_const`, `rewriter::tests::test_rewrite_call_remaps_function_index`, `rewriter::tests::test_rewrite_call_indirect_remaps_type_and_table`, `rewriter::tests::test_rewrite_global_get_set_remaps`, `rewriter::tests::test_rewrite_table_ops_remap`, `rewriter::tests::test_rewrite_table_copy_remaps_both`, `rewriter::tests::test_rewrite_memory_copy_remaps_both_memories`, `rewriter::tests::test_rewrite_memory_load_store_remaps_memory`, `rewriter::tests::test_rewrite_ref_func_remaps`; proofs `proofs/rewriter/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-9 + + - id: SWV-10 + type: sw-verification + title: "Verification of SR-10: Correct segment reindexing" + description: > + Verifies SR-10 via: tests `segments::tests::test_reindex_data_segment_rebases_offset`, `segments::tests::test_reindex_const_expr_global_get`, `segments::tests::test_reindex_const_expr_ref_func`, `segments::tests::test_reindex_element_segment_active_remaps_table`, `segments::tests::test_reindex_element_segment_remaps_function_refs`, `segments::tests::test_reindex_data_segment_remaps_memory_index`, `segments::tests::test_reindex_data_segment_global_get_remaps_global`, `segments::tests::test_reindex_element_segment_expression_remaps_ref_null_type`; proofs `proofs/segments/`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-10 + + - id: SWV-11 + type: sw-verification + title: "Verification of SR-11: Component processing order matches resolver order" + description: > + Verifies SR-11 via: tests `resolver::tests::test_topological_sort_linear`, `resolver::tests::test_topological_sort_diamond`, `resolver::tests::test_resolver_preserves_order_stability`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-11 + + - id: SWV-12 + type: sw-verification + title: "Verification of SR-12: Adapter generation for all pointer-passing cross-component calls" + description: > + Verifies SR-12 via: tests `adapter_safety::test_sr12_adapter_generation_for_string_param`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-12 + + - id: SWV-13 + type: sw-verification + title: "Verification of SR-13: Correct cabi_realloc targeting" + description: > + Verifies SR-13 via: tests `adapter_safety::test_sr13_cabi_realloc_targets_correct_memory`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-13 + + - id: SWV-14 + type: sw-verification + title: "Verification of SR-14: Correct memory index usage in adapters" + description: > + Verifies SR-14 via: proofs `proofs/adapter/`. + status: implemented + fields: + method: formal-verification + links: + - type: verifies + target: SR-14 + + - id: SWV-15 + type: sw-verification + title: "Verification of SR-15: Correct list copy length" + description: > + Verifies SR-15 via: tests `adapter_safety::test_sr15_list_copy_length`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-15 + + - id: SWV-16 + type: sw-verification + title: "Verification of SR-16: Recursive inner pointer fixup" + description: > + Verifies SR-16 via: tests `adapter_safety::test_sr16_inner_pointer_fixup_list_string`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-16 + + - id: SWV-17 + type: sw-verification + title: "Verification of SR-17: Correct string transcoding" + description: > + Verifies SR-17 via: tests `adapter_safety::test_sr17_utf8_to_utf16_string_transcoding`, `adapter_safety::test_sr17_utf8_to_utf16_supplementary_plane_transcoding`, `adapter_safety::test_sr17_utf16_to_utf8_supplementary_plane_transcoding`, `adapter_safety::test_sr17_utf16_to_utf8_lone_high_surrogate_replacement`, `adapter_safety::test_sr17_utf16_to_utf8_midstring_lone_surrogate_replacement`, `adapter_safety::test_sr17_utf16_to_utf8_malformed_surrogate_matrix`, `adapter_safety::test_sr17_utf8_to_utf16_malformed_matrix`, `adapter_safety::test_sr17_latin1_to_utf16_transcoding`, `adapter_safety::test_253_read_latin1_tagclear_to_utf16`, `adapter_safety::test_253_read_latin1_tagclear_to_utf8`, `adapter_safety::test_253_read_latin1_tagset_to_utf16`, `adapter_safety::test_253_read_latin1_tagset_to_utf8_supplementary`, `adapter_safety::test_253_write_utf8_to_latin1_fits`, `adapter_safety::test_253_write_utf8_to_latin1_needs_utf16`, `adapter_safety::test_253_write_utf16_to_latin1_fits`, `adapter_safety::test_253_write_utf16_to_latin1_needs_utf16_supplementary`, `adapter_safety::ls_p_21_latin1_utf16_tag_honored_roundtrip`, `resolver::tests::test_sr17_all_encoding_pairs_transcoding_matrix`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-17 + + - id: SWV-19 + type: sw-verification + title: "Verification of SR-19: Deterministic output" + description: > + Verifies SR-19 via: tests `tests::test_deterministic_output`, `resolver::tests::test_resolver_preserves_order_stability`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-19 + + - id: SWV-20 + type: sw-verification + title: "Verification of SR-20: Fail-fast on unresolvable state" + description: > + Verifies SR-20 via: tests `tests::test_fuser_empty_components_error`, `tests::test_fuser_rejects_core_module_input`, `tests::test_fuser_address_rebasing_requires_shared_memory`, `tests::test_fuser_rejects_invalid_wasm`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-20 + + - id: SWV-21 + type: sw-verification + title: "Verification of SR-21: Valid P2 component wrapping" + description: > + Verifies SR-21 via: tests `component_wrap::tests::test_build_stubs_module_multi_memory_exports`, `component_wrap::tests::test_build_stubs_module_single_memory_no_suffix`, `component_wrap::tests::test_build_stubs_module_multi_memory_limits_preserved`, `component_wrap::tests::test_resolve_import_to_instance_strips_suffix`, `component_wrap::tests::test_resolve_import_to_instance_non_numeric_suffix_not_stripped`, `component_wrap::tests::test_resolve_import_to_instance_unknown_module`, `wit_bindgen_runtime::test_fuse_component_wit_bindgen_flavorful`, `wit_bindgen_runtime::test_runtime_wit_bindgen_flavorful`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-21 + + - id: SWV-22 + type: sw-verification + title: "Verification of SR-22: Conditional pointer copy for option/result/variant types" + description: > + Verifies SR-22 via: tests `wit_bindgen_runtime::test_runtime_wit_bindgen_options`, `wit_bindgen_runtime::test_runtime_wit_bindgen_variants`, `wit_bindgen_runtime::test_runtime_wit_bindgen_flavorful`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-22 + + - id: SWV-23 + type: sw-verification + title: "Verification of SR-23: Import deduplication type safety" + description: > + Verifies SR-23 via: tests `merger::tests::test_multi_memory_dedup_separates_components`, `merger::tests::test_shared_memory_dedup_merges_components`, `merger::tests::test_import_memory_and_realloc_indices_populated`, `merger::tests::test_cabi_realloc_suffixed_exports_generated`, `merger::tests::test_shared_memory_no_suffixed_realloc_exports`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-23 + + - id: SWV-24 + type: sw-verification + title: "Verification of SR-24: Correct retptr layout for variant return types" + description: > + Verifies SR-24 via: tests `wit_bindgen_runtime::test_runtime_wit_bindgen_flavorful`, `wit_bindgen_runtime::test_runtime_wit_bindgen_variants`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-24 + + - id: SWV-25 + type: sw-verification + title: "Verification of SR-25: Resource handle pass-through" + description: > + Verifies SR-25 via: tests `wit_bindgen_runtime::test_fuse_wit_bindgen_resources`, `wit_bindgen_runtime::test_fuse_component_wit_bindgen_resources`, `wit_bindgen_runtime::test_runtime_wit_bindgen_resources`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-25 + + - id: SWV-26 + type: sw-verification + title: "Verification of SR-26: Complete component type index tracking" + description: > + Verifies SR-26 via: tests `wit_bindgen_runtime::test_runtime_wit_bindgen_flavorful`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-26 + + - id: SWV-27 + type: sw-verification + title: "Verification of SR-27: Attestation input hash integrity" + description: > + Verifies SR-27 via: tests `attestation::tests::test_sr27_input_hash_integrity`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-27 + + - id: SWV-28 + type: sw-verification + title: "Verification of SR-28: Attestation configuration completeness" + description: > + Verifies SR-28 via: tests `attestation::tests::test_sr28_config_completeness`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-28 + + - id: SWV-29 + type: sw-verification + title: "Verification of SR-29: Attestation serialization round-trip" + description: > + Verifies SR-29 via: tests `attestation::tests::test_sr29_attestation_round_trip`, `attestation::tests::test_to_bytes_returns_result`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-29 + + - id: SWV-30 + type: sw-verification + title: "Verification of SR-30: Attestation output hash integrity" + description: > + Verifies SR-30 via: tests `attestation::tests::test_sr30_output_hash_integrity`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-30 + + - id: SWV-31 + type: sw-verification + title: "Verification of SR-31: Multiply-instantiated module detection" + description: > + Verifies SR-31 via: tests `merger::tests::ls_m_5_multiply_instantiated_module_rejected`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-31 + + - id: SWV-32 + type: sw-verification + title: "Verification of SR-32: Stackful P3 lifting mode emission" + description: > + Verifies SR-32 via: tests `p3_async::tests::stackful_intrinsic_signatures_pinned`, `p3_async::tests::stackful_lift_is_async_without_callback`, `adapter::fact::tests::sr32_has_callback_export_detects_companion`, `adapter::fact::tests::sr32_stackful_emitter_handles_no_shim_with_default_results`, `adapter::fact::tests::sr32_stackful_emitter_shape_pins_call_drop_globalget`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-32 + + - id: SWV-33 + type: sw-verification + title: "Verification of SR-33: Cross-component `stream` fusion at merge time" + description: > + Verifies SR-33 via: tests `p3_bridge_runtime::ls_st_1_round_trip_local_stream_never_crosses_host`, `p3_bridge_runtime::cross_memory_chain_preserves_data_across_distinct_memories`, `p3_bridge_runtime::backpressure_partial_write_then_drain_then_resume`, `p3_bridge_runtime::ls_st_1_eof_only_after_writer_drop_and_drain`, `p3_bridge_runtime::slot_exhaustion_falls_back_to_host_stream`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-33 + + - id: SWV-34 + type: sw-verification + title: "Verification of SR-34: Static `stream` validation" + description: > + Verifies SR-34 via: tests `meld-core/src/p3_stream.rs::tests::ls_r_11_stream_typed_import_with_mismatched_roles_raises`, `meld-core/src/p3_stream.rs::tests::ls_r_11_per_edge_lift_export_mismatch_raises`, `meld-core/src/p3_stream.rs::tests::ls_r_11_sync_only_connection_with_unrelated_streams_does_not_raise`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-34 + + - id: SWV-35 + type: sw-verification + title: "Verification of SR-35: DWARF address remap into merged code section" + description: > + Verifies SR-35 via: tests `meld-core/src/dwarf.rs::tests::ls_d_1_remap_translates_low_pc`, `meld-core/tests/dwarf_remap_witness.rs`, `meld-core/tests/dwarf_strip.rs`, `meld-core/tests/dwarf_passthrough.rs`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-35 + + - id: SWV-36 + type: sw-verification + title: "Verification of SR-36: Synthesised DWARF DIEs for meld-generated adapter functions" + description: > + Verifies SR-36 via: tests `dwarf::tests::adapter_spans_identifies_component_synthetic`, `dwarf::tests::adapter_spans_recognises_fully_synthetic_sentinel`, `dwarf::tests::adapter_spans_empty_when_all_source`, `dwarf::tests::adapter_spans_disjoint_from_source_ranges`, `dwarf::tests::build_adapter_dwarf_attributes_ranges_to_meld_adapter`, `dwarf::tests::ls_d_2_rewrite_emits_source_and_adapter_units_in_one_write`, `adapter_dwarf_e2e::ls_d_2_generated_start_wrapper_is_attributed_to_meld_adapter`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-36 + + - id: SWV-37 + type: sw-verification + title: "Verification of SR-37: Automatic memory-strategy resolution (sound-by-construction default)" + description: > + Verifies SR-37 via: tests `meld-core/tests/auto_memory.rs::auto_selects_shared_for_growfree_inputs`, `meld-core/tests/auto_memory.rs::ls_m_7_auto_keeps_multi_when_input_grows`, `meld-core/tests/auto_memory.rs::ls_m_7_auto_reprobes_after_add_component`, `meld-core/tests/auto_memory.rs::auto_keeps_multi_for_single_memory_input`, `meld-core/tests/auto_memory.rs::explicit_multi_is_not_overridden`, `meld-core/src/memory_probe.rs::tests::ls_m_7_malformed_input_counts_as_grow`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-37 + + - id: SWV-38 + type: sw-verification + title: "Verification of SR-38: Multi-source DWARF merge (bounded relocator)" + description: > + Verifies SR-38 via: tests `dwarf::tests::ls_d_3_multi_source_merge_round_trips_both_units`, `dwarf_passthrough (multi-source policy test on lists.wasm)`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-38 + + - id: SWV-39 + type: sw-verification + title: "Verification of SR-39: Separate-input cross-component linking (import internalisation)" + description: > + Verifies SR-39 via: tests `golden_e2e::ls_cp_6_separate_inputs_internalise_link`, `wit_bindgen_runtime (full suite guards WASI imports staying declared)`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-39 + + - id: SWV-40 + type: sw-verification + title: "Verification of SR-40: Machine-checked Canonical-ABI layout invariants (Kani)" + description: > + Verifies SR-40 via: proofs `abi_proofs::flags_layout_matches_spec (Kani)`, `abi_proofs::total_flat_params_saturating_monotone (Kani)`, `abi_proofs::ring_cursor_invariant_inductive (Kani)`. + status: verified + fields: + method: formal-verification + links: + - type: verifies + target: SR-40 + + - id: SWV-41 + type: sw-verification + title: "Verification of SR-41: Async cross-encoding string transcoding" + description: > + Verifies SR-41 via: tests `async_cross_encoding::inc1_async_utf8_to_utf16_param_transcodes_hello`, `async_cross_encoding::inc1_async_utf8_to_utf16_param_transcodes_supplementary_plane`, `async_cross_encoding::inc2_async_utf16_to_utf8_param_transcodes_supplementary_plane`, `async_cross_encoding::inc4a_async_latin1_to_utf16_tag_set_nihon`, `async_cross_encoding::inc4a_async_latin1_to_utf8_tag_set_nihon`, `async_cross_encoding::inc4b_async_utf8_to_latin1_emoji_surrogate_pair`, `async_cross_encoding::inc4b_async_utf16_to_latin1_nihon_utf16`, `adapter::fact::tests::inc3_async_utf8_to_utf16_top_level_string_result_allowed`, `async_cross_encoding::inc5a_async_nested_list_string_utf8_to_utf16_transcodes`, `async_cross_encoding::inc5a_async_nested_list_u8_result_not_transcoded`, `async_cross_encoding::inc5b_nested_list_string_utf16_to_latin1`, `async_cross_encoding::inc5c_a_async_nested_list_string_param_utf8_to_utf16_transcodes`, `async_cross_encoding::inc5c_b_same_encoding_utf16_nested_param_deep_copies_full_codeunits`, `adapter::fact::tests::inc1_callback_adapter_transcode_locals_within_budget`, `adapter::fact::tests::inc5c_b_callback_adapter_nested_param_dest_latin1_locals_within_budget`, `adapter::fact::tests::inc5c_b_async_deeper_list_nesting_param_fails_loud_all_directions`. + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-41 + - id: SWV-18 + type: sw-verification + title: "Verification of SR-18: Adapter instruction ordering" + description: > + Verifies SR-18 via runtime/e2e tests that exercise the full adapter + instruction path (`meld-core/tests/wit_bindgen_runtime.rs` suite) plus + code inspection of the emission order in `meld-core/src/adapter/fact.rs`. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SR-18 + + - id: SWV-42 + type: sw-verification + title: "Verification of SR-42: Identity-trampoline adapter inlining" + description: > + Verifies SR-42 via test + `meld-core/tests/cross_component_call.rs::test_304_identity_direct_adapter_is_inlined` + (fuses a composed component, asserts adapters_inlined >= 1 and validates). + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-42 + + - id: SWV-43 + type: sw-verification + title: "Verification of SR-43: Opaque-rep resource drop-teardown soundness" + description: > + Verifies SR-43 via runtime oracle + `meld-core/tests/wit_bindgen_runtime.rs::test_runtime_wit_bindgen_resource_floats_opaque` + (construct+drop runs cleanly on the fused opaque-rep chain; skips if the + gitignored fixture is absent). + status: verified + fields: + method: automated-test + links: + - type: verifies + target: SR-43 + + - id: SWV-44 + type: sw-verification + title: "Verification of SR-44: Enforced requirement->verification traceability" + description: > + Verifies SR-44 by static analysis: `rivet validate` mechanically enforces + that every sw-req carries a typed sw-verification backlink (the ASPICE SWE + tier, ADR-5). The passing gate is itself the verification measure. + status: implemented + fields: + method: static-analysis + links: + - type: verifies + target: SR-44 From e6571db2c9b3d36470e6257bb8d1644e51ffbbe0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 13:06:21 +0200 Subject: [PATCH 5/7] =?UTF-8?q?fix(stpa):=20author=20UCA-F-2/F-3/CP-1=20?= =?UTF-8?q?=E2=80=94=20rivet=20validate=20PASSES=20(0=20errors)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The last 4 caused-by-uca danglers: loss scenarios LS-A-9, LS-A-17/18, LS-CP-5 referenced UCAs that were never authored. Authored them in their correct controller groups, grounded in the scenario content: - UCA-F-2 (adapter-ucas / CTRL-ADAPTER, not-providing): resource-graph build drops resource handling — definer-purge/terminal-exporter skip an (iface,rn) pair; [resource-drop] imports dropped for non-pure-consumers. [H-3, H-1] - UCA-F-3 (adapter-ucas, not-providing): async-callback trampoline doesn't dispatch the host poll for a guest POLL return code. [H-3] - UCA-CP-1 (wrapper-ucas / CTRL-WRAPPER, not-providing): composition export dropped or mis-typed when assembling the fused multi-component output. [H-1, H-3] With this, `rivet validate` PASSES (0 errors) on the #570-fixed rivet — the v0.36 traceability graph is clean and gate-able. Remaining 80 warnings are higher-tier V-closure (11 system-reqs need sys-verification; a few inverts-uca notes) — out of v0.36's software scope. Co-Authored-By: Claude Opus 4.8 (1M context) --- safety/stpa/ucas.yaml | 44 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/safety/stpa/ucas.yaml b/safety/stpa/ucas.yaml index 376e49c..32f9467 100644 --- a/safety/stpa/ucas.yaml +++ b/safety/stpa/ucas.yaml @@ -429,6 +429,36 @@ adapter-ucas: Copied list elements retain pointers into source memory. Callee dereferences them and reads garbage or traps. + - id: UCA-F-2 + description: > + Adapter resource-graph construction drops or ignores resource handling + for a component — the definer-purge and terminal-exporter passes skip + an (iface, resource-name) pair, and [resource-drop] imports are dropped + for non-pure-consumer components — so the needed adapter logic is not + emitted. + context: > + Resource-graph build during FACT adapter generation for a component + that defines or re-exports resources across the fused boundary. + hazards: [H-3, H-1] + rationale: > + Omitting resource-drop wiring or an (iface, rn) handler diverges the + fused module from the composed module's resource semantics and can + leak or mis-route handles. + + - id: UCA-F-3 + description: > + Adapter async-callback trampoline does not dispatch the host poll for a + guest POLL return code — it treats POLL (3) as falling through to the + non-WAIT else arm and returns (EVENT_NONE, 0, 0), dropping a ready event. + context: > + Guest legitimately returns callback::POLL on a P3 async export call path + while the host has the polled event ready. + hazards: [H-3] + rationale: > + The guest never observes the event it polls for, so the fused module + diverges from the composed module on P3 async export paths (semantic- + preservation violation). + providing: - id: UCA-A-4 description: > @@ -566,6 +596,20 @@ wrapper-ucas: Non-imported memories are not accessible to the stubs module. Canon lower cannot reference the correct memory for each component. + - id: UCA-CP-1 + description: > + Wrapper does not export, or mis-types, the composition's export when + assembling the fused multi-component output (a re-exported interface or + function from a sub-component is dropped or given the wrong type). + context: > + Multi-component fusion where the composition re-exports an interface or + function originating in one of the fused sub-components. + hazards: [H-1, H-3] + rationale: > + A dropped or mis-typed composition export makes the fused module's + public surface diverge from the composed module — callers see a missing + or wrongly-typed export, breaking semantic preservation. + providing: - id: UCA-W-2 description: > From fdf36b3c40f1314d279fe0dd685d26d6f7ac3c75 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 14:12:05 +0200 Subject: [PATCH 6/7] ci(compliance): bump rivet to v0.19.0 (carries #570 fix + aspice@0.2.0) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The release-time compliance report pinned rivet v0.15.0, which predates both the #570 YAML-parser fix and the aspice@0.2.0 schema — it could neither parse meld's STPA YAML cleanly nor understand the new sw-req/sw-verification tier. rivet v0.19.0 (released 2026-06-24) includes the #570 fix (commit 74aa830 is an ancestor) and ships aspice@0.2.0, so the compliance action + binary are bumped together to v0.19.0. Completes the v0.36 enforcement story: the release pipeline now validates/exports the migrated ASPICE artifacts. Release-only workflow (on: release published) — does not affect PR CI. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/compliance.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/compliance.yml b/.github/workflows/compliance.yml index 29c3403..e019fb4 100644 --- a/.github/workflows/compliance.yml +++ b/.github/workflows/compliance.yml @@ -43,10 +43,10 @@ jobs: - name: Generate compliance report id: report - uses: pulseengine/rivet/.github/actions/compliance@v0.6.0 + uses: pulseengine/rivet/.github/actions/compliance@v0.19.0 with: theme: dark - rivet-version: v0.15.0 + rivet-version: v0.19.0 include-data-formats: true report-label: ${{ steps.tag.outputs.tag }} archive: 'true' From f6da7773dd76a5852f31a540f1000b3b6a9f7ff1 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 24 Jun 2026 20:22:21 +0200 Subject: [PATCH 7/7] =?UTF-8?q?feat(aspice):=20system-tier=20sys-verificat?= =?UTF-8?q?ion=20=E2=80=94=20full=20V-closure=20(ADR-5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the system tier of the V to complete the full ASPICE migration: 11 typed sys-verification (SYS.5) artifacts, one per system-req (SYS-1..11), each carrying its `verifies` backlink and grounded in meld's system-level test evidence — primarily the behavioural-equivalence golden harness (golden_e2e.rs, #213) plus the per-domain e2e/runtime suites (multi_memory, dwarf_*, p3_*, cross_component_call, component_provenance, proptest_fusion), and `rivet validate` itself for the governance req. With this, BOTH tiers are verified: 0 requirement-verification gaps (sw + sys). Oracle (rivet v0.19.0): PASS, 69 warnings (down from 80) — the remainder are unrelated advisory coverage (orphan/prose-mention/EU-AI-Act-risk notes), not requirement→verification gaps. The V-model is closed end to end. Co-Authored-By: Claude Opus 4.8 (1M context) --- safety/requirements/sys-verifications.yaml | 162 +++++++++++++++++++++ 1 file changed, 162 insertions(+) create mode 100644 safety/requirements/sys-verifications.yaml diff --git a/safety/requirements/sys-verifications.yaml b/safety/requirements/sys-verifications.yaml new file mode 100644 index 0000000..9af23d2 --- /dev/null +++ b/safety/requirements/sys-verifications.yaml @@ -0,0 +1,162 @@ +# System verification measures — ASPICE SYS.5 (sys-verification) +# +# Closes the system tier of the V (ADR-5): each system-req (SYS-1..11) is +# verified by meld's system-level test evidence — primarily the behavioural- +# equivalence golden harness (tests/.../golden_e2e.rs, #213) plus the per- +# domain end-to-end / runtime suites. Clears sys2-has-verification. +# +# Format: rivet generic-yaml (sys-verification type from the aspice schema). + +artifacts: + + - id: SYSV-1 + type: sys-verification + title: "System verification of SYS-1: Faithful component ingestion" + description: > + Behavioural-equivalence golden harness (meld-core/tests/golden_e2e.rs, + #213 Tier A+B) plus nested_component.rs and release_components.rs confirm + the fused module ingests and reproduces the composed input faithfully. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-1 + + - id: SYSV-2 + type: sys-verification + title: "System verification of SYS-2: Sound index-space merging" + description: > + proptest_fusion.rs (property-based merge invariants) and + rebasing_end_to_end.rs exercise index-space merging across components; + golden_e2e.rs confirms runtime equivalence of the merged result. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-2 + + - id: SYSV-3 + type: sys-verification + title: "System verification of SYS-3: Canonical-ABI cross-component adapters" + description: > + cross_component_call.rs, runtime_intra_adapter.rs and adapter_safety.rs + exercise the emitted adapters end-to-end; golden_e2e.rs confirms + observable equivalence across the adapted boundary. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-3 + + - id: SYSV-4 + type: sys-verification + title: "System verification of SYS-4: Valid component wrapping and output" + description: > + file_ops_validate.rs and runtime_from_exports.rs validate the wrapped + output artifact's structure and that its exports run. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-4 + + - id: SYSV-5 + type: sys-verification + title: "System verification of SYS-5: Async / P3 fusion support" + description: > + p3_async_abi.rs, p3_async_lowering.rs, p3_bridge_runtime.rs and + async_cross_encoding.rs exercise stackful lifting, stream bridging and + cross-encoding end-to-end. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-5 + + - id: SYSV-6 + type: sys-verification + title: "System verification of SYS-6: Memory-strategy and isolation soundness" + description: > + multi_memory.rs (N distinct memories preserved, cross-memory data + movement) and auto_memory.rs (sound-by-construction strategy selection) + verify inter-component isolation. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-6 + + - id: SYSV-7 + type: sys-verification + title: "System verification of SYS-7: DWARF debug-info preservation" + description: > + dwarf_passthrough.rs, dwarf_remap_witness.rs, dwarf_strip.rs and + adapter_dwarf_e2e.rs verify DWARF is preserved/relocated correctly, + including synthesised adapter DIEs. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-7 + + - id: SYSV-8 + type: sys-verification + title: "System verification of SYS-8: Cross-input linking" + description: > + runtime_from_exports.rs and the separate-input linking e2e path verify + cross-input imports are internalised into intra-module calls and the + linked module runs. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-8 + + - id: SYSV-9 + type: sys-verification + title: "System verification of SYS-9: Deterministic, fail-fast operation" + description: > + proptest_fusion.rs covers byte-determinism over generated inputs; + file_ops_validate.rs and the reject/fail-fast tests confirm unresolvable + state aborts rather than emitting a degraded module. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-9 + + - id: SYSV-10 + type: sys-verification + title: "System verification of SYS-10: Attestation integrity" + description: > + component_provenance.rs verifies the attestation records a complete, + round-trippable binding of input hash, configuration and output hash. + status: implemented + fields: + method: automated-test + links: + - type: verifies + target: SYS-10 + + - id: SYSV-11 + type: sys-verification + title: "System verification of SYS-11: Traceability and verification governance" + description: > + `rivet validate` mechanically enforces the ASPICE SWE/SYS trace (this + migration, ADR-5) — every requirement carries a typed verification + backlink; the passing gate is the verification measure. + status: implemented + fields: + method: static-analysis + links: + - type: verifies + target: SYS-11