chore(rivet): close the V's right side + migrate to rivet 0.17 (canonical statuses + aspice)

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(

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() {

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

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

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

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: