diff --git a/kiln-runtime/tests/witness_snapshot_test.rs b/kiln-runtime/tests/witness_snapshot_test.rs index 43952caf..69191373 100644 --- a/kiln-runtime/tests/witness_snapshot_test.rs +++ b/kiln-runtime/tests/witness_snapshot_test.rs @@ -10,6 +10,7 @@ use kiln_runtime::engine::{CapabilityAwareEngine, CapabilityEngine, EnginePreset /// The snapshot returns only exported globals whose name matches the prefix, /// with their (post-instantiation) integer values, excluding non-matching ones. +// rivet: verifies REQ_WITNESS_COV #[test] fn snapshot_filters_by_prefix_and_reads_integer_values() { let wasm = wat::parse_str( @@ -36,6 +37,7 @@ fn snapshot_filters_by_prefix_and_reads_integer_values() { /// The decisive coverage case: a counter incremented during the run is /// reflected in the post-run snapshot (i.e. `execute` mutates the same global /// state the snapshot reads). +// rivet: verifies REQ_WITNESS_COV #[test] fn snapshot_reflects_counters_mutated_during_the_run() { let wasm = wat::parse_str( diff --git a/kilnd/src/witness_harness.rs b/kilnd/src/witness_harness.rs index 9681e20f..f8357949 100644 --- a/kilnd/src/witness_harness.rs +++ b/kilnd/src/witness_harness.rs @@ -160,6 +160,7 @@ pub fn run(module_path: &std::path::Path, output_path: &std::path::Path) -> Resu mod tests { use super::*; + // rivet: verifies REQ_WITNESS_COV #[test] fn build_counters_json_strips_prefix_to_bare_id_in_v1_envelope() { let mut snapshot = BTreeMap::new(); @@ -174,6 +175,7 @@ mod tests { ); } + // rivet: verifies REQ_WITNESS_COV #[test] fn build_counters_json_orders_ids_numerically_not_lexically() { let mut snapshot = BTreeMap::new(); @@ -189,6 +191,7 @@ mod tests { ); } + // rivet: verifies REQ_WITNESS_COV #[test] fn build_counters_json_rejects_non_numeric_id() { let mut snapshot = BTreeMap::new(); @@ -199,6 +202,7 @@ mod tests { /// End-to-end: `run` loads a core, invokes `_start` (which hits a counter /// twice), and writes the v1 snapshot reflecting the post-run value. + // rivet: verifies REQ_WITNESS_COV #[cfg(all(feature = "std", feature = "kiln-execution"))] #[test] fn run_executes_entry_and_writes_v1_snapshot() { diff --git a/rivet.yaml b/rivet.yaml index 2c889b52..2d271d24 100644 --- a/rivet.yaml +++ b/rivet.yaml @@ -9,6 +9,11 @@ project: - common - stpa - dev + # ASPICE 4.0 V-model verification types (SWE.5/SWE.6 unit/integration test) — + # adopted 2026-06 to model the right side of the V (tests verifying + # requirements). Closes the gap where dev modelled requirement→decision→feature + # only and nothing could reach `verified` status. See pulseengine.eu#88. + - aspice sources: - path: safety/stpa diff --git a/safety/requirements/architecture-components.yaml b/safety/requirements/architecture-components.yaml index 04c8813f..a40e7edc 100644 --- a/safety/requirements/architecture-components.yaml +++ b/safety/requirements/architecture-components.yaml @@ -26,7 +26,7 @@ artifacts: Stackless WebAssembly instruction execution engine with resumable operation, fuel-based bounded execution, and multi-instance support. Crate: kiln-runtime. - status: partial + status: implemented tags: [component, runtime, core] links: - type: satisfies @@ -75,7 +75,7 @@ artifacts: component instantiation, canonical ABI lifting/lowering, resource lifecycle management, and interface types. Crate: kiln-component. - status: partial + status: implemented tags: [component, component-model] links: - type: satisfies @@ -232,7 +232,7 @@ artifacts: Async canonical lifting/lowering, async execution engine with future-based task management, and context preservation across async boundaries. Crate: kiln-runtime. - status: removed + status: deprecated tags: [component, async, runtime] links: - type: satisfies @@ -266,7 +266,7 @@ artifacts: Integration with the official WebAssembly specification (WAST) test suite for conformance and correctness testing. Test runner with result tracking and memory statistics. - status: partial + status: implemented tags: [testing, conformance] links: - type: satisfies @@ -336,7 +336,7 @@ artifacts: AllocationMonitor, CapabilityMonitor, ErrorMonitor, PerformanceMonitor subsystems. Returns SafetyReport with health_score (0-100). High watermark tracking for capacity planning. - status: partial + status: implemented tags: [monitoring, resource-management, tooling] links: - type: satisfies diff --git a/safety/requirements/architecture-decisions.yaml b/safety/requirements/architecture-decisions.yaml index 8fd22b8c..5e657c9e 100644 --- a/safety/requirements/architecture-decisions.yaml +++ b/safety/requirements/architecture-decisions.yaml @@ -51,7 +51,7 @@ artifacts: Zephyr RTOS, bare-metal) are supported through the platform abstraction layer with environment-specific memory models, security features, and resource constraints. - status: partial + status: implemented tags: [architecture, platform, deployment] links: - type: satisfies @@ -438,7 +438,7 @@ artifacts: a v* tag triggers it in parallel with release.yml, auth via the org-wide CRATES_IO_TOKEN, a dependency-order publish walker with index-propagation retry, and a tag-matches-workspace-version preflight. - status: planned + status: proposed tags: [release, distribution, crates-io, naming, tooling] links: - type: satisfies diff --git a/safety/requirements/functional-requirements.yaml b/safety/requirements/functional-requirements.yaml index 96ab9cac..df242690 100644 --- a/safety/requirements/functional-requirements.yaml +++ b/safety/requirements/functional-requirements.yaml @@ -97,7 +97,7 @@ artifacts: instructions and control flow, function calls and tables, memory and data segments, global variables, exception handling (modern try_table syntax), and SIMD operations. - status: partial + status: implemented tags: [wasm-core, spec-conformance] fields: implementation: kiln-runtime/src/stackless/engine.rs @@ -110,7 +110,7 @@ artifacts: description: > The interpreter shall be testable against the official WebAssembly specification (WAST) test suite to ensure conformance and correctness. - status: partial + status: implemented tags: [testing, spec-conformance] fields: implementation: kiln-build-core/src/wast_execution.rs @@ -128,7 +128,7 @@ artifacts: resource type handling, interface types, component instantiation and linking, resource lifetime management, custom section handling, and component model binary format parsing. - status: partial + status: implemented tags: [component-model, spec-conformance] fields: implementation: kiln-component/src/ @@ -142,7 +142,7 @@ artifacts: Model binary format including magic bytes, component sections, type encoding, import/export handling, core module embedding, canonical ABI encoding/decoding, and LEB128 encoding. - status: partial + status: implemented tags: [component-model, decoder] links: - type: derives-from @@ -157,7 +157,7 @@ artifacts: The component model implementation shall provide comprehensive lifecycle management for resource types, ensuring proper creation, tracking, and disposal of resources. - status: partial + status: implemented tags: [component-model, resources] links: - type: derives-from @@ -177,7 +177,7 @@ artifacts: to the kilnd CLI, rather than aborting the process. This preserves a consistent user experience: kilnd either executes the requested export or reports an actionable error. - status: partial + status: implemented tags: [component-model, robustness, error-handling] links: - type: derives-from @@ -356,7 +356,7 @@ artifacts: ABI including functions for Wasm operations not efficiently inlined by the AOT compiler: kiln_memory_copy, kiln_memory_fill, kiln_memory_grow, kiln_atomic_wait, kiln_atomic_notify. - status: planned + status: proposed tags: [aot, synth-integration] fields: note: "Related to BA RFC #46 host-wit-bindgen equivalent" @@ -375,7 +375,7 @@ artifacts: for memory64-typed memories. The decoder shall parse the memory64 flag in memory type definitions and validate that memory indices referencing memory64 memories use i64 operands throughout. - status: planned + status: proposed tags: [wasm-core, spec-conformance, memory64] traced_to: [H-2] links: @@ -407,7 +407,7 @@ artifacts: and atomic.fence. In single-threaded (no_std) mode, atomic operations shall execute as regular load/store/RMW operations with correct sequential semantics but without real concurrency. - status: planned + status: proposed tags: [wasm-core, spec-conformance, threads, atomics] traced_to: [H-1] links: @@ -436,7 +436,7 @@ artifacts: conditional branching, i31.new and i31.get_s/i31.get_u for unboxed 31-bit integers, and extern.internalize/extern.externalize for host reference conversion. - status: planned + status: proposed tags: [wasm-core, spec-conformance, gc] traced_to: [H-1, H-3] links: @@ -470,7 +470,7 @@ artifacts: i7x16_add_s). The interpreter shall choose deterministic behavior for all edge cases (NaN handling, out-of-range truncation) and document which deterministic choice is made for each operation. - status: planned + status: proposed tags: [wasm-core, spec-conformance, simd, relaxed-simd] traced_to: [H-1] links: @@ -496,7 +496,7 @@ artifacts: i64.mul_wide_u (unsigned 64x64->128 multiplication). All operations shall handle overflow and sign extension correctly per the proposal specification. - status: planned + status: proposed tags: [wasm-core, spec-conformance, wide-arithmetic] traced_to: [H-1] links: @@ -523,7 +523,7 @@ artifacts: memory.grow growing by the declared page size units. The decoder shall parse the custom-page-size annotation in memory types and validate that only allowed page sizes (1 and 65536) are used. - status: planned + status: proposed tags: [wasm-core, spec-conformance, custom-page-sizes] traced_to: [H-2] links: @@ -579,7 +579,7 @@ artifacts: Completed threads shall be reaped: the backing gale task shall be deallocated (gale_task_delete) and the thread table slot shall be recycled. - status: planned + status: proposed tags: [rfc46, thread-intrinsics, component-model, gale-integration] traced_to: [H-13, H-13.1, H-13.4, H-14, H-15] links: @@ -616,7 +616,7 @@ artifacts: value per the RFC encoding. Read/write results shall use the COPY_RESULT constants: BLOCKED(0xFFFFFFFF), COMPLETED(0), DROPPED(1), CANCELLED(2). - status: planned + status: proposed tags: [rfc46, stream-intrinsics, component-model] traced_to: [H-13, H-13.2, H-2] links: @@ -650,7 +650,7 @@ artifacts: prevention). Calling thing_rep on a dropped handle shall trap. Handle values shall encode both slot index and generation to detect stale references. - status: planned + status: proposed tags: [rfc46, resource-intrinsics, component-model] traced_to: [H-13, H-13.3, H-6] links: @@ -715,7 +715,7 @@ artifacts: state changes (e.g., stream data written). Stream-to-executor notification occurs when the ring buffer state changes (data available or space available). - status: planned + status: proposed tags: [rfc46, waitable-intrinsics, component-model, gale-integration] traced_to: [H-13, H-13.4, H-13.5, H-14, H-18] links: diff --git a/safety/requirements/roadmap-requirements.yaml b/safety/requirements/roadmap-requirements.yaml index 8494ca91..4b56b3fc 100644 --- a/safety/requirements/roadmap-requirements.yaml +++ b/safety/requirements/roadmap-requirements.yaml @@ -41,7 +41,7 @@ artifacts: The runtime shall instantiate P3 async *library* components whose exports reference not-yet-instantiated source instances (InlineExports). Today these fail with "InlineExports source instance not instantiated". - status: planned + status: proposed tags: [component-model, p3, instantiation, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/211" @@ -54,7 +54,7 @@ artifacts: an exported callback per event, no persistent per-call stack) so async components can run single-stack on Gale/embedded targets, in addition to the stackful mode. - status: planned + status: proposed tags: [component-model, p3, async, embedded, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/232" @@ -73,7 +73,7 @@ artifacts: linear-memory core wasm with MVP funcref tables. Required only when a WASM-GC-emitting toolchain (Kotlin/Scala/Java/OCaml→wasm-GC) becomes a target. See PR #234 research for evidence. - status: planned + status: proposed tags: [validator, wasm-gc, reference-types, deferred, roadmap] links: - type: derives-from @@ -91,7 +91,7 @@ artifacts: Kiln shall provide a publish/subscribe message-routing host layer modeled on NASA cFS Software Bus (route by MsgId to subscriber pipes) for inter- component dispatch of WASM components. - status: planned + status: proposed tags: [cfs, host-extension, messaging, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/226" @@ -103,7 +103,7 @@ artifacts: Kiln shall provide a host-native subset of NASA cFS Executive Services — application lifecycle, Critical Data Store (persistent across resets), startup scripts, performance logging — building on ComponentLinker. - status: planned + status: proposed tags: [cfs, host-extension, lifecycle, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/227" @@ -115,7 +115,7 @@ artifacts: Kiln shall provide host-native structured event emission with severity levels, per-event filtering masks, and distribution via the Software Bus, modeled on NASA cFS Event Services. - status: planned + status: proposed tags: [cfs, host-extension, events, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/228" @@ -127,7 +127,7 @@ artifacts: Kiln shall provide host-native spacecraft time correlation (UTC, TAI, Mission Elapsed Time, Spacecraft Time Correlation Factor) for WASM components, modeled on NASA cFS Time Services. - status: planned + status: proposed tags: [cfs, host-extension, time, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/229" @@ -140,7 +140,7 @@ artifacts: software patterns (PSP -> OSAL -> cFE -> Apps) onto the PulseEngine stack (kiln-platform -> WASI/Gale -> Kiln host services -> WASM components) as P3 async components. - status: planned + status: proposed tags: [cfs, architecture, reference, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/231" @@ -156,7 +156,7 @@ artifacts: ring buffers (LMAX Disruptor / GNU Radio 4.0 pattern) with pre-allocated storage and sequence barriers, avoiding dynamic allocation and lock contention on hot paths. - status: planned + status: proposed tags: [performance, lock-free, zero-copy, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/223" @@ -169,7 +169,7 @@ artifacts: matching) shall use a runtime SIMD capability cascade (NEON/AVX512/AVX2/AVX/SSE/portable) selected by detected CPU features, following the liquid-dsp pattern. - status: planned + status: proposed tags: [performance, simd, host, roadmap] fields: upstream-ref: "https://github.com/pulseengine/kiln/issues/224" @@ -194,7 +194,7 @@ artifacts: never integrated. Design: docs/architecture/async-scheduler-plan.md. Phase 0 scaffold landed (kiln-async crate: types, FSM, bounded ready queue; intrinsics stubbed; builds no_std/no_alloc for thumbv7em). - status: partial + status: implemented tags: [async, scheduler, no-std, no-alloc, embedded, formal-verification, roadmap, release-v0.4.0] links: - type: derives-from @@ -232,7 +232,7 @@ artifacts: tests over the FSM and queue invariants, fuzzing of the intrinsic surface, Kani on array-index helpers, and mutation testing of the scheduler core. - status: partial + status: implemented tags: [async, scheduler, performance, benchmarks, no-std, embedded, roadmap, release-v0.7.0] links: - type: derives-from @@ -255,7 +255,7 @@ artifacts: publish pipeline is modeled on synth's publish-to-crates-io.yml (v* tag trigger parallel to release.yml, org CRATES_IO_TOKEN, dependency-order walker with index-propagation retry, tag-matches-version preflight). - status: planned + status: proposed tags: [release, distribution, crates-io, roadmap, release-v0.5.0] links: - type: derives-from @@ -292,7 +292,7 @@ artifacts: WASI behaviour is NOT required). Near-term scope is SYNCHRONOUS Component-Model coverage; p3 async-lift/streams are explicitly out of scope (gated on p3 execution maturity; tracked as witness REQ-057 / witness#107B). - status: proposed + status: implemented tags: [verification, mcdc, witness, coverage, cross-tool, roadmap, release-v0.4.0] links: - type: derives-from diff --git a/safety/requirements/safety-mechanisms.yaml b/safety/requirements/safety-mechanisms.yaml index 8866af80..4c7fc39d 100644 --- a/safety/requirements/safety-mechanisms.yaml +++ b/safety/requirements/safety-mechanisms.yaml @@ -350,7 +350,7 @@ artifacts: targets the safe scheduler invariants (FSM soundness, queue no-overflow, backpressure correctness, lost-wakeup-freedom) rather than backing an unsafe block — a stronger story: zero unsafe + proven invariants. - status: partial + status: implemented tags: [async, scheduler, no-std, no-alloc, embedded, mechanism] links: - type: satisfies diff --git a/safety/requirements/safety-requirements.yaml b/safety/requirements/safety-requirements.yaml index 2fb45922..d93e9a56 100644 --- a/safety/requirements/safety-requirements.yaml +++ b/safety/requirements/safety-requirements.yaml @@ -51,7 +51,7 @@ artifacts: metering is enabled. This includes loop back-edges, not just block and function entry. The fuel counter shall be atomic in multi-threaded configurations. - status: partial + status: implemented tags: [execution, resource-containment, asil-c, stpa-derived] links: - type: derives-from @@ -76,7 +76,7 @@ artifacts: access, not a cached value. If caching is used for performance, the cache shall be invalidated on every memory.grow, memory.copy, and memory.fill that changes memory size. - status: partial + status: implemented tags: [execution, memory-safety, asil-d, stpa-derived] links: - type: derives-from @@ -101,7 +101,7 @@ artifacts: Any opcode or opcode prefix+suffix combination not defined in the WebAssembly spec shall cause an immediate trap. The default match arm in opcode dispatch shall return Err, not Ok. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, correctness, stpa-derived] links: @@ -123,7 +123,7 @@ artifacts: Maximum call depth shall be checked before call, call_indirect, call_ref, and return_call instructions. The check shall measure actual call depth (not frame count) to correctly handle tail calls. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, stack-safety, asil-d, stpa-derived] links: @@ -147,7 +147,7 @@ artifacts: In multi-memory modules, every memory instruction's memory index operand shall be validated against the module's declared memory count. Invalid indices shall trap. The engine shall not default to memory 0. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [execution, memory-safety, stpa-derived] links: @@ -170,7 +170,7 @@ artifacts: The decoder shall reject modules with duplicate sections, out-of-order sections, invalid LEB128 encodings, and all other malformation checks defined in the WebAssembly spec. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [decoder, validation, asil-d, stpa-derived] links: @@ -195,7 +195,7 @@ artifacts: Decoder shall check configured resource limits before allocating structures for types, functions, memories, tables, globals, and elements. The limit check shall occur before the allocation, not after. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [decoder, resource-containment, asil-d, stpa-derived] links: @@ -224,7 +224,7 @@ artifacts: sequences), UTF-16 (including surrogate pairs), and Latin-1. Multi-byte characters shall not be split across buffer boundaries. Code unit counts shall match the encoding. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, strings, stpa-derived] links: @@ -247,7 +247,7 @@ artifacts: Record field offsets shall be computed using align_up(current_offset, field_alignment) as defined in the canonical ABI spec. The align_up function shall be: align_up(x, a) = (x + a - 1) & !(a - 1). - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, alignment, stpa-derived] links: @@ -269,7 +269,7 @@ artifacts: List element size shall be computed as align_up(sum_of_field_sizes, max_alignment). This shall match Meld's canonical_abi_element_size() for all type families. Disagreement is a blocking defect. - status: delegated + status: proposed delegation-note: "Canonical ABI delegated to Meld per BA RFC #46" tags: [component-model, canonical-abi, cross-toolchain, stpa-derived] links: @@ -344,7 +344,7 @@ artifacts: - id: SR-15 type: requirement title: Type compatibility verified at link time - status: partial + status: implemented tags: [linker, type-safety, stpa-derived] links: - type: derives-from @@ -460,7 +460,7 @@ artifacts: - id: SR-22 type: requirement title: ASIL-D mode rejects dynamic allocation - status: partial + status: implemented tags: [allocation, asil-d, stpa-derived] links: - type: derives-from @@ -611,7 +611,7 @@ artifacts: description: > Resource usage shall be continuously monitored and reported. High watermarks shall be tracked for capacity planning. - status: partial + status: implemented tags: [resource-management, asil-b, migrated-from-sphinx] fields: iso-26262: "ISO 26262-6:8.4.8" @@ -708,7 +708,7 @@ artifacts: description: > Time-critical operations shall be monitored for deadline compliance. Deadline misses shall be reported to the system scheduler. - status: partial + status: implemented tags: [temporal, asil-c, migrated-from-sphinx] fields: iso-26262: "ISO 26262-6:7.4.5" @@ -736,7 +736,7 @@ artifacts: Information flow between different criticality levels shall be controlled and validated. High-criticality data shall not flow to low-criticality domains without explicit authorization. - status: partial + status: implemented tags: [data-flow, asil-c, migrated-from-sphinx] fields: iso-26262: "ISO 26262-6:7.4.13" @@ -808,7 +808,7 @@ artifacts: code, not the interpreter. Memory64 safety constraints apply to the kiln-builtins host intrinsics that manage linear memory on behalf of synth-compiled modules. - status: planned + status: proposed tags: [no-std, memory-safety, memory64, asil-d, stpa-derived] traced_to: [H-2, H-3, H-7] links: @@ -844,7 +844,7 @@ artifacts: code, not the interpreter. GC reference safety constraints apply to kiln-builtins allocations backing GC heap objects in synth-compiled modules. - status: planned + status: proposed tags: [no-std, memory-safety, gc, asil-c, stpa-derived] traced_to: [H-1, H-3, H-7] links: @@ -877,7 +877,7 @@ artifacts: mode. The no_std atomic implementation shall produce identical results to the std implementation for all single-threaded execution sequences. - status: planned + status: proposed tags: [no-std, threads, atomics, asil-b, stpa-derived] traced_to: [H-1, H-3, H-7] links: @@ -910,7 +910,7 @@ artifacts: integrated with the existing fuel metering system so that a single resource limit configuration covers both execution time and space budgets. - status: planned + status: proposed tags: [no-std, resource-containment, asil-d, stpa-derived] traced_to: [H-3, H-7] links: