stash

Cargo.lock

@@ -2920,6 +2920,13 @@ dependencies = [
  "uuid",
 ]
 
+[[package]]
+name = "mvp-system"
+version = "0.1.0"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "n0-error"
 version = "0.1.3"
@@ -5370,6 +5377,7 @@ dependencies = [
  "crossbeam-queue",
  "crossbeam-utils",
  "getrandom 0.2.17",
+ "mvp-system",
  "proptest",
  "proptest-state-machine",
  "serde",

Cargo.toml

@@ -10,6 +10,7 @@ members = [
     "crates/distribution",
     "crates/datastream",
     "crates/datastore",
+    "crates/mvp-system",
     "crates/node",
     "tests/docker",
     "tests/integration",
@@ -56,6 +57,11 @@ unexpected_cfgs = { level = "allow", check-cfg = ['cfg(kani)'] }
 criterion = { version = "0.5", features = ["html_reports"] }
 proptest = "1"
 proptest-state-machine = "0.3"
+mvp-system = { path = "crates/mvp-system" }
+
+[[test]]
+name = "arena_manager_guarantees"
+path = "tests/mvp_system/arena_manager_guarantees.rs"
 
 [[bench]]
 name = "runtime_benchmarks"

GPU_WORKER_INTERFACE_SPEC.md

@@ -187,8 +187,6 @@ outside payload ownership. Ring cursors are the authority.
 
 ### 4.4 Device Bridge
 
-USER: If it is determined this is an outsized amount of engineering work, we will defer and require objects to be complete before gpu io.
-
 The worker must have a backend-specific device bridge capable of range copies:
 
 ```text
@@ -445,7 +443,6 @@ may be available. The worker must reload ring cursors from shared memory.
 Duplicate hints may be coalesced.
 
 ### 7.7 ExecuteStep
-USER: Why do we need this explicit? Why doesnt it fall out naturally from the I/O? This whole thing is async message driven, so why do we need a start message?
 
 ```rust
 struct ExecuteStep {
@@ -654,8 +651,6 @@ all copy events for that object have completed.
 committed to the egress ring. It does not mean the remote node received it.
 
 ### 8.5 Step Events
-USER: Why is this here? It seems useless.
-
 
 ```rust
 StepCompleted {

crates/mvp-system/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "mvp-system"
+version = "0.1.0"
+edition = "2024"
+publish = false
+
+[target.'cfg(target_os = "linux")'.dependencies]
+libc = "0.2"

crates/mvp-system/src/lib.rs

@@ -0,0 +1 @@
+pub mod arena_manager;

specs/mvp_system/arena_manager_contract.md

@@ -0,0 +1,58 @@
+# ArenaManager Contract
+
+This document defines the behavioral contract for node-local arena management.
+The `ArenaManager` mints stable arena-relative ring layouts and releases ranges
+only after quiescence proof.
+
+## Arena Formation
+
+- The node constructs one sparse arena.
+- The arena has one reservation ceiling.
+- The arena mapping is stable for the node lifetime.
+- Arena layouts contain offsets, not process-local pointers.
+- Arena boot failure emits a typed arena fault.
+
+## Ring Lease
+
+- `LeaseRing` either emits `RingLeased`, queues the request, or emits
+  `RingLeaseRejected`.
+- A satisfiable request may queue under temporary arena pressure.
+- A request that can never fit within the ceiling is rejected.
+- A live lease has one `RingId`.
+- `RingId` is unique for the node lifetime.
+
+## Layout Safety
+
+- Live leases do not overlap.
+- Every lease lies within the arena ceiling.
+- Every lease satisfies the requested alignment.
+- Header and data offsets are stable for the lease lifetime.
+- A layout never exposes process-local pointers.
+
+## Cancellation
+
+- `CancelLease` removes a queued request that has not been leased.
+- A canceled queued request does not later install worker or pump state.
+- If a fresh lease races with cancellation, it is released without becoming
+  hot-path state.
+
+## Release
+
+- `ReleaseRing` requires quiescence proof.
+- The arena manager does not infer quiescence.
+- Released ranges may be reused after release.
+- Ranges are not reused while a live pump, worker ring, or copy operation still
+  owns them.
+
+## Shutdown
+
+- Shutdown rejects new leases.
+- Shutdown does not corrupt existing live lease records.
+- Shutdown does not release live ranges without proof.
+
+## Test Direction
+
+Tests should issue deterministic lease, cancel, release, and shutdown messages
+and inspect public lease events. Successful tests should assert non-overlap,
+alignment, reuse after release, and queue retry. Failure tests should assert
+oversized rejection, canceled lease suppression, and no release without proof.

specs/mvp_system/device_bridge_contract.md

@@ -0,0 +1,53 @@
+# Device Bridge Contract
+
+This document defines the behavioral contract for the backend-specific device
+bridge used by the GPU worker. The bridge is the worker's boundary between host
+ring memory, device memory, and tinygrad-compatible views.
+
+## Allocation
+
+- `alloc_device(ObjectSpec, extent)` creates a device allocation suitable for
+  the object spec and extent.
+- Allocation failure is reported as device allocation failure.
+- Allocations are tied to the current worker generation.
+- `free_device` releases an allocation after no compute or copy event depends
+  on it.
+
+## Host To Device
+
+- `host_to_device` copies exactly the requested host range to the requested
+  device range.
+- For synchronous copies, return means bytes are safe to release.
+- For asynchronous copies, completion of the copy event means bytes are safe to
+  release.
+- Copy failure is reported as device copy failure.
+
+## Device To Host
+
+- `device_to_host` copies exactly the requested device range to the requested
+  host range.
+- For synchronous copies, return means host bytes are valid.
+- For asynchronous copies, completion of the copy event means host bytes are
+  valid.
+- Copy failure is reported as output copy failure or device copy failure.
+
+## Tinygrad View
+
+- `wrap_for_tinygrad` creates a tinygrad-compatible view over a device
+  allocation.
+- The view matches the tensor view spec used by the role.
+- Invalid view shape or dtype fails the step.
+
+## Lifetime
+
+- Device allocations are not freed while compute uses them.
+- Device allocations are not freed while copy events use them.
+- Worker restart invalidates all prior device handles.
+- Old-generation handles are rejected.
+
+## Test Direction
+
+Tests should use a fake backend to observe allocation, copy, completion, view,
+and free calls. Success tests should assert exact ranges and safe cursor-release
+points. Fault tests should inject allocation failure, copy failure, invalid
+view, and old-generation handles.

specs/mvp_system/driver_pumps_contract.md

@@ -0,0 +1,64 @@
+# Driver And Pump Contract
+
+This document defines the behavioral contract for the iroh driver, edge demux,
+and send/recv pumps. The driver owns tokio, connections, streams, demux, and
+byte-pump tasks.
+
+## Driver Authority
+
+- The driver owns one iroh endpoint.
+- The driver owns connection caching.
+- The driver owns edge ALPN.
+- The driver owns edge-id stream demux.
+- The driver owns send and recv pump tasks.
+- Actors do not poll stream futures directly in the MVP.
+
+## Connection And Stream Shape
+
+- Each edge uses one persistent uni-stream.
+- The stream starts with an `edge_id` preamble.
+- After the preamble, the stream carries object records as bytes.
+- The stream is not opened per object.
+- Connections may be cached per `(peer_node_id, ALPN)`.
+
+## Receive Rendezvous
+
+- `EstablishRecv` may arrive before the stream.
+- The stream may arrive before `EstablishRecv`.
+- The driver stores whichever half arrives first.
+- The recv pump starts only after both receive spec and stream exist.
+- A pending stream is not read before the receive spec exists.
+
+## Recv Pump
+
+- The recv pump is byte-blind after edge demux.
+- It does not parse `ObjectHeader`.
+- It copies QUIC bytes into free ingress ring spans.
+- It advances `commit` after bytes are in the ring.
+- It emits or coalesces `RingReadable`.
+- If no ring space exists, it stops reading and waits for `RingWritable`.
+
+## Send Pump
+
+- The send pump opens one uni-stream for the edge.
+- It writes the `edge_id` preamble once.
+- It writes committed egress ring bytes to QUIC.
+- It advances `consume` only after `write_all` accepts bytes.
+- It emits or coalesces `RingWritable`.
+- If network or QUIC flow control stalls, it keeps ownership of unread ring
+  bytes until the write completes.
+
+## Fault And Stop
+
+- Read error emits `StreamFault`.
+- Write error emits `StreamFault`.
+- Protocol edge failure emits `StreamFault`.
+- `StopEdge` stops the corresponding pump.
+- Stopped pumps emit `PumpStopped`.
+
+## Test Direction
+
+Tests should use mock streams and rings to drive driver messages and pump wake
+events. Successful tests should assert rendezvous in both arrival orders,
+preamble once, byte-blind copying, cursor advancement after I/O acceptance, and
+backpressure. Fault tests should inject read/write errors and stop races.

specs/mvp_system/edge_establisher_contract.md

@@ -0,0 +1,61 @@
+# EdgeEstablisher Contract
+
+This document defines the behavioral contract for local edge establishment. It
+turns `ProvisionTx` or `ProvisionRx` into a local edge actor, arena lease,
+worker ring installation, driver establishment, and ready/fault outcome.
+
+## Provisioning
+
+- Each node has one `EdgeEstablisher`.
+- `ProvisionTx` creates a local send edge record.
+- `ProvisionRx` creates a local receive edge record.
+- The producer needs the consumer `node_id`.
+- The consumer needs the shared `edge_id`.
+- Remote actor addresses are not required for data flow.
+
+## Lease Flow
+
+- Establishment requests one arena lease per edge end.
+- `RingLeased` matching the request advances the edge record.
+- `RingLeaseRejected` matching the request fails the edge record.
+- Stale lease events for stopped records do not install worker or pump state.
+- An unused fresh lease granted after cancellation is released.
+
+## Worker Ring Installation
+
+- The edge establishes driver state only after worker or token endpoint ring
+  installation succeeds.
+- `RingInstalled` matching the edge advances establishment.
+- `RingFault` before readiness stops establishment.
+- Ring installation uses the `ObjectSpec` and `RingSpec` from provisioning.
+
+## Driver Establishment
+
+- Send edges call `EstablishSend` with `edge_id`, consumer `node_id`, and local
+  ring layout.
+- Receive edges call `EstablishRecv` with `edge_id` and local ring layout.
+- `DriverEdgeReady` marks the local edge actor ready.
+- Stream and pump behavior are driver-owned after readiness.
+
+## Ready And Hot Path
+
+- Ready means local actor, arena lease, worker/token ring, and driver state are
+  installed.
+- The hot path runs without `EdgeEstablisher`.
+- The establisher observes coarse ready, stopped, and fault events only.
+
+## Stopping
+
+- `StopEdge` cancels queued leases.
+- `StopEdge` stops pumps if present.
+- `StopEdge` uninstalls worker rings if installed.
+- The arena lease is released only after quiescence proof.
+- `Stopped` is terminal for that edge record.
+
+## Test Direction
+
+Tests should drive the public establishment FSM with lease, worker, driver, and
+stop events. Successful tests should assert the order lease -> install ->
+driver -> ready. Fault tests should inject lease rejection, ring fault, driver
+fault, stale events, and stop races and assert no hot-path state survives
+incorrectly.

specs/mvp_system/gpu_worker_ctl_contract.md

@@ -0,0 +1,55 @@
+# GpuWorkerCtl Contract
+
+This document defines the behavioral contract for the Rust-side GPU worker
+controller. `GpuWorkerCtl` owns the supervised worker process boundary and
+routes worker events to local control components.
+
+## Worker Lifecycle
+
+- `StartWorker` spawns the process actor and process bridge.
+- After process start, `GpuWorkerCtl` sends `InitializeWorker`.
+- `WorkerReady` moves the controller to running.
+- `WorkerFatal`, process exit, or initialization timeout moves the controller
+  to failed or crashed state.
+- Worker generation increments on restart.
+
+## Command Routing
+
+- In running state, valid actor commands are serialized to the worker.
+- `InstallRing` is sent only for the current worker generation.
+- `ExecuteStep` is sent only with current-generation handles.
+- `ReleaseDeviceObject` is sent only for current-generation handles.
+- Payload bytes are never sent through worker control messages.
+
+## Event Routing
+
+- Worker events are parsed from process stdout.
+- `RingInstalled` routes to edge establishment.
+- `ObjectLoaded` routes to Rx or role layer.
+- `ObjectProduced` routes to Tx or role layer.
+- `StepCompleted` and `StepFailed` route to the StageController.
+- Wake events route to the driver or worker side as appropriate.
+
+## Crash Behavior
+
+- Worker crash invalidates old device handles.
+- Worker crash invalidates installed roles, rings, and in-flight steps.
+- The controller synthesizes ring faults for installed rings.
+- The controller asks the driver to stop pumps for affected rings.
+- Old-generation handles are rejected after restart.
+
+## Shutdown
+
+- Graceful shutdown sends `ShutdownWorker`.
+- Timeout escalates according to local process policy.
+- Shutdown marks installed rings faulted or quiesced according to observed
+  worker/process outcome.
+- `WorkerStopped` is observed before terminal stopped when graceful shutdown
+  succeeds.
+
+## Test Direction
+
+Tests should use a fake process adapter and public controller messages. Success
+tests should assert start -> initialize -> ready, command serialization, and
+event routing. Fault tests should inject malformed stdout, worker fatal, process
+exit, restart, and old-generation handles and assert invalidation and fanout.

specs/mvp_system/gpu_worker_egress_producer_contract.md

@@ -0,0 +1,50 @@
+# GPU Worker Egress Producer Contract
+
+This document defines the behavioral contract for worker-side egress
+production. The worker writes object records to an egress ring from explicit
+`ExecuteStep` output bindings.
+
+## Output Admission
+
+- Egress production starts only after `InstallRing(direction = Egress)`.
+- The worker writes output only for an `ExecuteStep` output binding naming that
+  ring.
+- The output binding supplies object id, sequence, extent, and flags.
+- The worker does not invent graph-visible object ids or sequence numbers.
+
+## Header Production
+
+- The worker creates an `ObjectHeader` according to the edge `ObjectSpec`.
+- Header bytes are written before payload bytes.
+- `commit` advances only after header bytes are valid.
+- `RingReadable` is emitted or coalesced after committed header bytes.
+
+## Payload Production
+
+- The worker copies exactly `extent` bytes from device to the egress ring.
+- `commit` advances only after host bytes are valid.
+- Objects larger than the ring may stream through bounded ring spans.
+- If no writable span exists, `ExecuteStep` may block on egress backpressure.
+
+## ObjectProduced
+
+- `ObjectProduced` is emitted after the full output object is committed.
+- `StepCompleted` is emitted only after all declared outputs are produced and
+  role state updates are complete.
+- `ObjectProduced` includes ring id, edge id, port id, object id, sequence, and
+  extent.
+
+## Fault Behavior
+
+- Invalid output ring fails the step.
+- Output extent violation fails the step.
+- Device copy failure fails the step or faults the ring.
+- Worker shutdown rejects or aborts output production according to shutdown
+  mode.
+
+## Test Direction
+
+Tests should drive `ExecuteStep` with fake device outputs and bounded egress
+rings. Success tests should assert header-before-payload, exact extent, cursor
+publication, `ObjectProduced`, and `StepCompleted` ordering. Fault tests should
+cover invalid output ring, invalid extent, backpressure, and copy failure.

specs/mvp_system/gpu_worker_ingress_parser_contract.md

@@ -0,0 +1,53 @@
+# GPU Worker Ingress Parser Contract
+
+This document defines the behavioral contract for worker-side ingress parsing.
+The worker parses object records from an ingress ring and emits `ObjectLoaded`
+only after a complete logical object is available on device.
+
+## Ring Admission
+
+- Ingress parsing starts only after `InstallRing(direction = Ingress)`.
+- The worker reloads cursors after `RingReadable`.
+- The parser consumes committed bytes only.
+- The parser does not read uncommitted bytes.
+
+## Header Validation
+
+- The parser waits until a complete `ObjectHeader` is committed.
+- Unsupported magic rejects the object.
+- Unsupported version rejects the object.
+- Malformed header length rejects the object.
+- `extent > ObjectSpec.max_extent` rejects the object.
+- Extent alignment or layout violation rejects the object.
+- Sequence violation rejects the object.
+
+## Payload Loading
+
+- Payload content values are trusted.
+- The parser copies exactly `extent` payload bytes to device memory.
+- `consume` advances only after copied bytes are safe to release.
+- Objects larger than the ring may stream through bounded ring spans.
+- EOF before the full payload faults the object.
+
+## ObjectLoaded
+
+- `ObjectLoaded` is emitted only after valid header, exact extent copy, copy
+  completion, and device handle creation.
+- `ObjectLoaded` includes ring id, edge id, port id, object id, sequence,
+  extent, and device handle.
+- The emitted handle belongs to the current worker generation.
+
+## Fault Behavior
+
+- Header malformed emits `ObjectFailed`.
+- Extent exceeds max emits `ObjectFailed`.
+- Sequence violation emits `ObjectFailed`.
+- Device allocation or copy failure emits `ObjectFailed` or `RingFault`.
+- After ring fault, the worker stops consuming until uninstall.
+
+## Test Direction
+
+Tests should write object records through the public ring helper and observe
+worker events. Success tests should assert `ObjectLoaded` only after complete
+payload and copy completion. Fault tests should cover malformed headers,
+oversized extent, bad sequence, EOF mid-object, and copy failure.

specs/mvp_system/gpu_worker_process_adapter_contract.md

@@ -0,0 +1,45 @@
+# GPU Worker Process Adapter Contract
+
+This document defines the behavioral contract for the stdin/stdout adapter
+between `GpuWorkerCtl` and the Python/tinygrad worker process. The adapter is
+not a distributed protocol.
+
+## Control Stream Shape
+
+- Commands are one JSON object per stdin line.
+- Events are one JSON object per stdout line.
+- Stderr is reserved for logs and diagnostics.
+- Payload bytes are forbidden in JSON commands.
+- Payload bytes are forbidden in JSON events.
+
+## Initialization
+
+- The worker reads arena environment variables.
+- The worker waits for `InitializeWorker`.
+- The worker maps the arena.
+- The worker initializes the native ring helper.
+- The worker initializes backend/tinygrad.
+- Success emits `WorkerReady`.
+- Failure emits `WorkerFatal` if possible and exits non-zero.
+
+## Parsing
+
+- Invalid JSON is a worker/process fault.
+- Unknown event shape is a worker/process fault.
+- Unsupported helper ABI emits `WorkerFatal`.
+- Stderr output alone is diagnostic and does not define lifecycle state.
+
+## Command Discipline
+
+- `InstallRing` installs worker-side ring state.
+- Wake hints reload ring cursors.
+- `ExecuteStep` runs explicit role compute.
+- `ReleaseDeviceObject` releases handles when safe.
+- `ShutdownWorker` moves the worker toward draining.
+
+## Test Direction
+
+Tests should drive the adapter with fake stdin/stdout lines. Successful tests
+should assert one-line command/event framing and initialization ordering. Fault
+tests should inject malformed JSON, unknown events, ABI mismatch, and payload
+bytes in control messages.

specs/mvp_system/membership_pool_readiness_contract.md

@@ -0,0 +1,46 @@
+# Membership And Pool Readiness Contract
+
+This document defines the behavioral contract for the orchestrator's membership
+gate. SWIM is an input to pool readiness; it is not a distributed graph
+agreement protocol.
+
+## Pool Readiness Formation
+
+- The orchestrator emits `PoolReady` only for the intended candidate pool.
+- `PoolReady` requires every candidate node to be known to the orchestrator.
+- `PoolReady` requires every candidate node to be live in the SWIM view.
+- `PoolReady` requires every candidate node to have emitted `NodeAvailable`.
+- `PoolReady` requires every candidate node to have data-plane identity material.
+- `PoolReady` requires no candidate node to be suspect or faulted.
+- `PoolReady` requires the pool view to remain stable for the configured
+  convergence window.
+
+## Planning Gate
+
+- Run planning starts only after `PoolReady`.
+- If pool readiness is lost before a `RunPlan` is committed, the orchestrator
+  waits or aborts according to local policy.
+- Nodes do not need to agree on graph state before planning.
+- Nodes do not compute placement from SWIM state.
+
+## Loss After Provisioning
+
+- Membership loss for a required node after provisioning begins faults the run.
+- The MVP does not re-place an active run after membership loss.
+- A suspect or faulted required node is treated as unavailable for the active
+  run.
+
+## Authority
+
+- SWIM reports membership and liveness facts.
+- The orchestrator decides pool readiness.
+- The orchestrator owns the candidate pool definition.
+- SWIM does not assign stages, edges, layers, or object specs.
+
+## Test Direction
+
+Tests should feed deterministic membership and node-availability observations
+into the orchestrator readiness gate. Successful tests should assert that
+`PoolReady` appears only after all required facts and the convergence window.
+Failure tests should remove or suspect one candidate node and assert no
+`PoolReady`, or a run fault if provisioning has already begun.

specs/mvp_system/node_boot_lifecycle_contract.md

@@ -0,0 +1,56 @@
+# Node Boot Lifecycle Contract
+
+This document defines the behavioral contract for node boot. It covers the
+observable transition from container start to `NodeAvailable`, and the failure
+cases that keep a node out of the candidate run pool.
+
+## Boot Formation
+
+- A node boot attempt starts when the node process is launched in the intended
+  pool.
+- A boot attempt emits either `NodeAvailable` or a typed node boot fault.
+- It never emits `NodeAvailable` before required local resources are ready.
+- It never allows run provisioning to race ahead of node availability.
+
+## Required Readiness Facts
+
+- The Rust node process is alive.
+- The swactor runtime can receive control messages.
+- The node has a stable `node_id` known to the orchestrator.
+- The arena is created and mapped in the node process.
+- The GPU worker is ready, or the implementation has an explicit deferred
+  worker-start policy with the same run-level readiness guarantee.
+- The iroh endpoint is initialized and bound to the node identity.
+- The SWIM participant has joined or is joining the intended pool.
+- The node can accept run provisioning.
+
+## Non-Readiness Facts
+
+- `NodeAvailable` does not mean weights are present.
+- `NodeAvailable` does not mean a role is configured.
+- `NodeAvailable` does not mean run edges are established.
+- `NodeAvailable` does not mean the node has been selected by a `RunPlan`.
+
+## Failure Behavior
+
+- Arena construction failure rejects node availability.
+- Worker startup failure rejects node availability unless worker startup is
+  explicitly deferred.
+- Transport endpoint failure rejects node availability.
+- Missing or invalid node identity rejects node availability.
+- A node that is boot-faulted is not eligible for run planning.
+
+## Authority
+
+- The node owns local boot resources.
+- The orchestrator owns whether a booted node is part of the intended candidate
+  pool.
+- A node does not self-assign stages, edges, or layer ranges during boot.
+
+## Test Direction
+
+Tests should drive the boot component through public resource outcomes and
+observe emitted lifecycle events. Successful tests should assert that
+`NodeAvailable` appears only after the required readiness facts. Failure tests
+should inject one failed resource at a time and assert a typed boot fault with
+no `NodeAvailable`.

specs/mvp_system/observability_surface_contract.md

@@ -0,0 +1,54 @@
+# Observability Surface Contract
+
+This document defines the behavioral contract for lifecycle and fault events
+used by tests and operators. Observability transport and storage are
+implementation details.
+
+## Event Identity
+
+- Required events include `run_id` when run-scoped.
+- Required events include `node_id` when node-scoped.
+- Required events include `stage_index` when stage-scoped.
+- Required events include `edge_id` when edge-scoped.
+- Required events include `ring_id` when ring-scoped.
+- Object events include `object_id` and `sequence`.
+- Step events include `step_id`.
+- Worker events include `worker_generation`.
+
+## Lifecycle Events
+
+- Node boot emits `node_started` and `node_available` or `node_faulted`.
+- Pool readiness emits `pool_ready`.
+- Planning emits `run_planned`.
+- Stage provisioning emits `stage_provision_started`.
+- Weight work emits `weights_download_started`, `weights_downloaded`, and
+  `weights_loaded` when those phases occur.
+- Edge provisioning emits `edge_provision_started` and `edge_ready`.
+- Stage readiness emits `stage_ready`.
+- The global barrier emits `readiness_barrier_passed`.
+- Prompt injection emits `prompt_injected`.
+- Execution emits `object_loaded`, `execute_step_started`, `object_produced`,
+  `step_completed`, and `token_received`.
+- Terminal run state emits `run_completed` or `run_faulted`.
+- Teardown emits `stop_run_sent`, `stage_stopped`, and `run_torn_down`.
+
+## Fault Events
+
+- Fault events include a stable reason enum.
+- Fault events include the component that detected the fault.
+- Tests do not need to scrape logs to determine lifecycle progress.
+- Free-form logs may add diagnostics but do not replace structured events.
+
+## Ordering
+
+- Events reflect the same ordering guarantees as the component contracts.
+- `prompt_injected` cannot precede `readiness_barrier_passed`.
+- `stage_ready` cannot precede required local readiness.
+- `run_torn_down` cannot precede teardown completion.
+- A run emits exactly one terminal outcome event.
+
+## Test Direction
+
+Tests should subscribe to the stable event stream and assert event identities,
+reason enums, and ordering. Contract tests should not depend on log text,
+transport implementation, storage backend, or event batching policy.

specs/mvp_system/orchestrator_run_fsm_contract.md

@@ -0,0 +1,67 @@
+# Orchestrator Run FSM Contract
+
+This document defines the behavioral contract for the orchestrator run FSM. It
+covers how a valid `RunPlan` becomes provisioning, readiness, prompt injection,
+execution, terminal outcome, and teardown.
+
+## Planning And Provisioning
+
+- The orchestrator plans only after `PoolReady`.
+- It provisions only from a valid `RunPlan`.
+- It sends exactly one `ProvisionStage` to every planned stage.
+- It does not provision unknown stages.
+- It does not provision nodes outside the committed plan.
+- It creates local token-in and token-out endpoints according to the plan.
+
+## Readiness Barrier
+
+- The orchestrator does not inject the prompt before every planned stage reports
+  `StageReady`.
+- The orchestrator does not inject the prompt before local token endpoints are
+  ready.
+- Duplicate `StageReady` does not advance readiness twice.
+- `StageReady` from an unknown stage rejects or faults.
+- `StageReady` for a different run rejects or faults.
+
+## Execution Drive
+
+- Prompt injection is the start signal.
+- There is no separate broadcast start.
+- The orchestrator injects sequence `0` first.
+- It injects sequence `k + 1` only after consuming token sequence `k`.
+- It stops injecting after EOS.
+- It stops injecting after `max_tokens`.
+
+## Fault Behavior
+
+- `StageFault` before readiness faults the run.
+- `StageFault` during execution faults the run.
+- Membership loss for a required node faults the run.
+- Endpoint fault faults the run.
+- Timeout faults the run.
+- The first run-level failure reason is retained.
+- Later failure reasons do not replace the recorded terminal reason.
+
+## Terminal Outcome
+
+- Each run records exactly one terminal outcome.
+- `Completed` and `Faulted` are mutually exclusive.
+- Operator stop before completion records the operator-stopped outcome.
+- After terminal outcome begins, no new prompt or token work is accepted.
+- Teardown is required after success, fault, and operator stop.
+
+## Teardown
+
+- The orchestrator sends `StopRun` to every provisioned stage.
+- It tears down local token endpoints.
+- It waits for `StageStopped` from every provisioned stage or teardown timeout.
+- It emits `run_torn_down` exactly once.
+- `run_torn_down` is emitted only after teardown has reached its terminal state.
+
+## Test Direction
+
+Tests should drive the orchestrator with public events and observe emitted
+commands, lifecycle events, and terminal outcome. Successful tests should prove
+the readiness barrier, sequence injection rule, and teardown after completion.
+Fault tests should inject one fault source at a time and assert exactly one
+run-level terminal outcome and teardown.

specs/mvp_system/orchestrator_token_endpoint_contract.md

@@ -0,0 +1,44 @@
+# Orchestrator Token Endpoint Contract
+
+This document defines the behavioral contract for orchestrator-owned token
+edges. The orchestrator is a data-plane participant for token-in and token-out,
+but it does not run model compute.
+
+## Endpoint Formation
+
+- The orchestrator creates the token-in producer from the committed plan.
+- The orchestrator creates the token-out consumer from the committed plan.
+- Token endpoints use the same edge semantics as stage endpoints.
+- The orchestrator endpoint has a stable `node_id`.
+- Co-location with a GPU node does not change token edge semantics.
+
+## Prompt Injection
+
+- Prompt injection happens only after the global readiness barrier.
+- Prompt injection writes token object sequence `0`.
+- Prompt injection is the only run start signal.
+- The token-in object conforms to the token `ObjectSpec`.
+
+## Token Consumption
+
+- Token-out consumption observes token objects in sequence order.
+- The orchestrator consumes token sequence `k` before deciding whether to inject
+  sequence `k + 1`.
+- EOS stops further injection.
+- `max_tokens` stops further injection.
+- Out-of-order token output faults the run.
+
+## Fault Behavior
+
+- Token-in endpoint fault faults the run.
+- Token-out endpoint fault faults the run.
+- Malformed token object faults the run.
+- Token sequence violation faults the run.
+- Token endpoint teardown failure contributes to run teardown failure.
+
+## Test Direction
+
+Tests should drive the endpoint through prompt injection and token-return
+traces. Successful tests should assert sequence `0` first and `k + 1` only
+after token `k`. Fault tests should inject endpoint fault, malformed token, and
+out-of-order token output and assert run fault.

specs/mvp_system/resource_inventory_contract.md

@@ -0,0 +1,37 @@
+# Resource Inventory Contract
+
+This document defines the behavioral contract for the MVP resource inventory
+used by planning. The inventory is an orchestrator-owned input to `RunPlan`
+formation, not a distributed negotiation protocol.
+
+## Inventory Formation
+
+- The orchestrator owns the intended node pool.
+- The orchestrator owns the resource inventory used for placement.
+- Each inventory entry is tied to a known `node_id`.
+- Inventory facts are available before planning starts.
+- A candidate node may report boot health and readiness, but does not negotiate
+  graph placement after boot.
+
+## Planning Input
+
+- The planner receives a candidate pool and placement input from the
+  orchestrator.
+- The planner rejects placement that names nodes outside the candidate pool.
+- The planner rejects missing or duplicate stage assignments.
+- The planner does not mutate the candidate pool.
+- The planner does not derive hidden nodes outside the inventory.
+
+## Authority
+
+- Resource inventory determines what the planner is allowed to place onto.
+- `RunPlan` determines what actually gets placed.
+- Nodes do not advertise new placement facts during run planning.
+- Stages do not reinterpret inventory after provisioning.
+
+## Test Direction
+
+Tests should treat inventory as public planner input. Successful tests should
+assert that every planned stage node comes from the inventory. Rejection tests
+should name unknown nodes, duplicate stage assignments, or incomplete placement
+facts and assert typed planner rejection.

specs/mvp_system/run_plan_contract.md

@@ -0,0 +1,79 @@
+# RunPlan Contract
+
+This document defines the behavioral contract for MVP `RunPlan` formation and
+projection. It is concerned with externally observable planner behavior: the
+planner inputs, the emitted `RunPlan`, derived provisioning messages, and typed
+rejections.
+
+The planner is the first contract target because the orchestrator is the run
+authority. Every downstream component receives its stage, layer, edge, and
+object obligations from the committed plan.
+
+## RunPlan Formation
+
+- Given model facts, runtime config, intended node pool, stage count, and
+  placement input, the planner either emits exactly one `RunPlan` or a typed
+  rejection.
+- It never emits a partial plan.
+- It never mutates the candidate pool or derives hidden topology outside the
+  plan.
+
+## Layer Assignment
+
+- Stage ranges are contiguous.
+- Stage ranges do not overlap.
+- The union covers the intended GGUF block range.
+- Every stage has exactly one non-empty assigned range unless the spec
+  explicitly allows empty ranges.
+- Stage indices are `0..stage_count-1`.
+
+## Edge Assignment
+
+- Every edge id is unique within the run.
+- Every edge has exactly one producer and one consumer.
+- Token-in edge is `orchestrator -> stage 0`.
+- Activation edge `i` is `stage i -> stage i + 1`.
+- Token-out edge is `stage N-1 -> orchestrator`.
+- Stages do not derive edge ids from names, hashes, layer ranges, or peers.
+
+## Provisioning Projection
+
+- For each `StagePlan`, deriving `ProvisionStage` is deterministic.
+- A stage receives only its own layer range.
+- A stage receives exactly one inbound and one outbound edge provision.
+- Outbound provision contains the consumer `node_id`.
+- Inbound provision does not require producer actor address.
+- No provision message contains remote actor addresses for data flow.
+
+## Object/Ring Spec Consistency
+
+- Every edge has an `ObjectSpec` and `RingSpec`.
+- Activation `max_extent` follows the model facts:
+  `max_seq_len * hidden_dim * dtype_width_bytes`.
+- Token edges use token object specs, activation edges use activation object
+  specs.
+- Specs are copied consistently into stage provisions.
+- Invalid extent, alignment, dtype width, or unsupported shape/layout rejects
+  the plan.
+
+## Authority / Rejection
+
+- Unknown node id rejects.
+- Duplicate stage assignment rejects.
+- Missing stage rejects.
+- Invalid stage count rejects.
+- Edge endpoint mismatch rejects.
+- Model facts inconsistent with requested stage layout reject.
+- The planner is the only source of stage, layer, edge, and object-spec
+  assignment.
+
+## Test Direction
+
+The tests for this contract should assert guarantees over planner inputs,
+planner outputs, derived provisioning messages, and typed rejections. They
+should not assert planner internals, placement heuristics, helper APIs,
+allocation strategy, or private data structures.
+
+Successful-plan tests should inspect the returned `RunPlan` and derived
+`ProvisionStage` values. Rejection tests should feed contradictory inputs and
+assert that no plan is emitted.

specs/mvp_system/shared_ring_helper_abi_contract.md

@@ -0,0 +1,62 @@
+# Shared Ring Helper ABI Contract
+
+This document defines the behavioral contract for the shared ring ABI and native
+helper. Both Rust hot-path code and the Python worker access process-crossing
+rings through this helper.
+
+## Ring Identity
+
+- A ring is a bounded single-producer/single-consumer byte stream.
+- Each ring has exactly one producer and one consumer.
+- `RingId` is unique for the node lifetime.
+- Stale wake events cannot alias replacement rings.
+
+## Cursor Contract
+
+- `commit` is the first byte after the committed readable prefix.
+- `consume` is the first byte not yet released by the consumer.
+- Producer-local `write` does not expose bytes to the consumer.
+- Cursor values are monotonic logical byte positions.
+- Physical indices are derived by `cursor % capacity`.
+
+## Producer Rules
+
+- The producer computes free space from acquired `consume`.
+- The producer does not reserve beyond ring capacity.
+- The producer writes bytes before publishing `commit`.
+- Publishing `commit` uses release ordering.
+- After publishing readable bytes, the producer sends or coalesces
+  `RingReadable`.
+
+## Consumer Rules
+
+- The consumer computes readable bytes from acquired `commit`.
+- The consumer does not read beyond committed bytes.
+- The consumer advances `consume` only after bytes are safe to release.
+- Publishing `consume` uses release ordering.
+- After releasing space, the consumer sends or coalesces `RingWritable`.
+
+## Wake Rules
+
+- Wake hints are edge-trigger hints.
+- Wake hints carry no byte ranges, counts, pointers, or credits.
+- Receivers reload cursors from shared memory.
+- Duplicate wakes may be coalesced only while durable scheduler state still
+  makes the ring discoverable.
+- Losing the only empty-to-readable or full-to-writable transition is a liveness
+  bug.
+
+## Helper ABI
+
+- Python does not implement shared atomics directly.
+- Python does not implement wrap arithmetic directly.
+- Returned pointers are process-local addresses derived from arena base plus
+  arena offsets.
+- Helper operations use acquire/release semantics across the process boundary.
+
+## Test Direction
+
+Tests should use the public helper operations to exercise wraparound, full,
+empty, publish, consume, and wake behavior. Safety tests should assert no
+unwritten reads and no unread overwrite. Liveness tests should assert that wake
+coalescing cannot hide a discoverable readable or writable transition.

specs/mvp_system/stage_controller_contract.md

@@ -0,0 +1,70 @@
+# StageController Contract
+
+This document defines the behavioral contract for a provisioned stage's
+`StageController`. The controller is control-path only: it observes setup,
+worker, edge, and object events, and issues worker commands.
+
+## Provisioning
+
+- A stage starts unprovisioned.
+- It accepts `ProvisionStage` only from the authorized orchestrator.
+- It validates `run_id`, `stage_index`, stage count, layer range, and edge
+  provisions before setup.
+- Invalid provisioning emits `StageFault`.
+- A stage does not rewire inbound or outbound edges.
+
+## Preparation
+
+- The controller configures the local worker role path.
+- It starts assigned weight download, load, or bind work.
+- It establishes the inbound receive edge.
+- It establishes the outbound send edge.
+- It reports `StageReady` only after worker readiness, weight readiness, inbound
+  edge readiness, and outbound edge readiness.
+
+## Execution Admission
+
+- A ready stage executes only after inbound `ObjectLoaded`.
+- The inbound object sequence must equal the next expected sequence.
+- The stage issues exactly one `ExecuteStep` for each accepted inbound object.
+- The output binding uses the same sequence as the input object.
+- The MVP allows one active `ExecuteStep` per stage.
+
+## Sequence Safety
+
+- Sequence `0` is accepted as prefill.
+- Decode sequences are strictly increasing after sequence `0`.
+- Duplicate sequence faults the stage.
+- Skipped sequence faults the stage.
+- Out-of-order sequence faults the stage.
+
+## Completion
+
+- `StepCompleted` returns the stage to ready-for-next-object state.
+- The controller releases per-step input handles according to policy.
+- The stage does not report compute completion before the worker reports
+  `StepCompleted`.
+
+## Fault Behavior
+
+- Worker crash faults the stage.
+- `StepFailed` faults the stage.
+- `ObjectFailed` faults the stage.
+- Output edge fault faults the stage.
+- Sequence violation faults the stage.
+- After fault, the stage rejects new run work until stopped.
+
+## Stopping
+
+- On `StopRun`, the controller stops local edges.
+- It releases per-run device objects.
+- It stops or resets worker role state according to local policy.
+- It emits `StageStopped` once teardown reaches the local terminal state.
+
+## Test Direction
+
+Tests should drive the controller with public setup and worker/edge events.
+Successful tests should assert `StageReady` ordering, one `ExecuteStep` per
+accepted object, and same-sequence output binding. Fault tests should inject
+invalid sequence, setup failure, worker crash, and step failure and assert
+`StageFault` followed by rejection of new work.

specs/mvp_system/tx_rx_edge_actor_contract.md

@@ -0,0 +1,53 @@
+# Tx And Rx Edge Actor Contract
+
+This document defines the behavioral contract for Tx and Rx edge actors. They
+are role-facing lifecycle gates and never carry payload bytes.
+
+## Actor Role
+
+- A Tx actor represents the producer side of one edge.
+- An Rx actor represents the consumer side of one edge.
+- Each edge actor is tied to one `edge_id`.
+- Edge actors receive lifecycle and object events only.
+- Edge actors do not receive bytes, pointers, ranges, credits, or free-space
+  counts.
+
+## Tx Lifecycle
+
+- Tx starts in provisioning.
+- `EdgeReady` moves Tx to ready.
+- Producing is allowed only after ready.
+- `ObjectProduced` reports committed output object identity.
+- Stream fault or object fault moves Tx to faulted.
+- `StopEdge` moves Tx toward stopped.
+
+## Rx Lifecycle
+
+- Rx starts in provisioning.
+- `EdgeReady` moves Rx to ready.
+- `ObjectLoaded` reports complete logical input object identity and handle.
+- Rx exposes loaded objects to the role layer only after `ObjectLoaded`.
+- Object failure or stream fault moves Rx to faulted.
+- `StopEdge` moves Rx toward stopped.
+
+## Payload Isolation
+
+- Payload bytes never travel in edge actor messages.
+- Host pointers never travel in edge actor messages.
+- Flow-control details never travel in edge actor messages.
+- Edge actors traffic only identities, lifecycle events, opaque handles, and
+  coarse faults.
+
+## Fault Behavior
+
+- `ObjectFailed` faults the corresponding edge actor.
+- `StreamFault` faults the corresponding edge actor.
+- Stale events for stopped actors are ignored.
+- Events for a mismatched `edge_id` reject or fault according to local policy.
+
+## Test Direction
+
+Tests should drive Tx and Rx actors with public lifecycle and object events.
+Successful tests should assert readiness before production/loading and payload
+isolation in message types. Fault tests should inject stream and object faults
+and assert no further run work is accepted before stop.

specs/mvp_system/weight_lifecycle_contract.md

@@ -0,0 +1,45 @@
+# Weight Lifecycle Contract
+
+This document defines the behavioral contract for stage-local weight work.
+Weights are persistent run state for a stage and must be usable before the
+stage reports `StageReady`.
+
+## Assignment
+
+- The stage receives its weight source from `ProvisionStage`.
+- The stage receives exactly one assigned layer range.
+- The stage validates the assigned layer range against the run plan.
+- The stage does not load layers outside its assigned range as graph-visible
+  ownership.
+
+## Loading
+
+- A stage may download a whole GGUF and load only its range.
+- A stage may download physical shards containing its range.
+- A stage may use a cached artifact that already exists on the node.
+- The physical loading mechanism is implementation-defined.
+- The system-visible outcome is `WeightsReady` or `StageFault`.
+
+## WeightsReady
+
+- `WeightsReady` requires assigned artifact bytes to be locally available or
+  cached.
+- `WeightsReady` requires the assigned layer range to be validated.
+- `WeightsReady` requires the worker to have loaded or bound the range needed
+  for execution.
+- `WeightsReady` happens before `StageReady`.
+
+## Failure Behavior
+
+- Download failure faults the stage.
+- Parse failure faults the stage.
+- Device allocation failure faults the stage.
+- Binding failure faults the stage.
+- Invalid layer range faults the stage.
+
+## Test Direction
+
+Tests should treat weight loading as a stage-local black box with observable
+events. Successful tests should assert `WeightsReady` before `StageReady`.
+Failure tests should inject download, parse, allocation, and bind failures and
+assert `StageFault` with no `StageReady`.

tests/mvp_system/arena_manager_guarantees.rs

@@ -0,0 +1,266 @@
+//! Black-box contract tests for MVP ArenaManager behavior.
+//!
+//! These tests intentionally know only the public arena-manager surface:
+//!
+//! - arena boot configuration
+//! - lease, cancel, release, quiescence, and shutdown requests in
+//! - lease events, rejected requests, released ranges, and faults out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/arena_manager_contract.md`.
+
+use mvp_system::arena_manager as arena;
+
+// A small deterministic arena makes overlap, alignment, queueing, and reuse
+// proofs easy to inspect. The concrete mmap strategy remains outside the test.
+fn arena_config() -> arena::ArenaConfig {
+    arena::ArenaConfig {
+        node_id: arena::NodeId(10),
+        reservation_ceiling: 4096,
+        base_alignment: 64,
+    }
+}
+
+// Lease requests name size and alignment only. They do not request pointers or
+// private allocator slots, which keeps layout authority inside ArenaManager.
+fn lease_request(request_id: u64, bytes: u64, alignment: u64) -> arena::LeaseRing {
+    arena::LeaseRing {
+        request_id: arena::LeaseRequestId(request_id),
+        ring_spec: arena::RingSpec {
+            header_bytes: 128,
+            data_bytes: bytes,
+            alignment,
+        },
+    }
+}
+
+// The harness exposes public lease events and lease snapshots. Tests use those
+// snapshots only after a RingLeased event, so private allocator state remains
+// unobservable.
+fn new_arena() -> arena::ArenaManagerHarness {
+    arena::ArenaManagerHarness::boot(arena_config()).expect("test arena must boot")
+}
+
+// This helper proves two public layouts are disjoint using half-open ranges.
+// It is more useful than comparing offsets directly because allocator choice is
+// intentionally implementation-defined.
+fn assert_non_overlapping(left: &arena::RingLayout, right: &arena::RingLayout) {
+    let left_range = left.start_offset..left.end_offset;
+    let right_range = right.start_offset..right.end_offset;
+    assert!(
+        left_range.end <= right_range.start || right_range.end <= left_range.start,
+        "live leases overlap: {left:?} and {right:?}"
+    );
+}
+
+// This proves arena boot creates one stable sparse arena with one reservation
+// ceiling, offset-only layouts, and typed boot failure.
+#[test]
+fn arena_boot_creates_stable_offset_only_layout_domain() {
+    // Boot a valid arena.
+    let mut harness = new_arena();
+
+    // Lease one ring so the public layout can be inspected.
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 512, 64)));
+    let lease = harness
+        .events()
+        .iter()
+        .find_map(|event| match event {
+            arena::ArenaEvent::RingLeased { lease } => Some(lease),
+            _ => None,
+        })
+        .expect("valid lease must be granted");
+
+    // Layout facts are arena offsets and stay under the reservation ceiling.
+    assert!(lease.layout.start_offset < arena_config().reservation_ceiling);
+    assert!(lease.layout.end_offset <= arena_config().reservation_ceiling);
+    assert!(matches!(lease.layout.pointer, arena::LayoutPointer::NoProcessPointer));
+
+    // Boot failure is typed and emits no usable arena.
+    let failed = arena::ArenaManagerHarness::boot(arena::ArenaConfig {
+        reservation_ceiling: 0,
+        ..arena_config()
+    });
+    assert!(matches!(
+        failed,
+        Err(arena::ArenaFault::InvalidReservationCeiling)
+    ));
+}
+
+// This proves LeaseRing either leases, queues, or rejects, and that live RingId
+// values are unique for the node lifetime.
+#[test]
+fn lease_requests_grant_queue_or_reject_with_unique_ring_ids() {
+    // Fill most of the arena with one live lease.
+    let mut harness = new_arena();
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 3072, 64)));
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(2, 1024, 64)));
+
+    // A satisfiable request under pressure may queue instead of rejecting.
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            arena::ArenaEvent::RingLeaseQueued {
+                request_id: arena::LeaseRequestId(2)
+            }
+        )
+    }));
+
+    // A request larger than the reservation ceiling must reject.
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(3, 8192, 64)));
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            arena::ArenaEvent::RingLeaseRejected {
+                request_id: arena::LeaseRequestId(3),
+                reason: arena::RingLeaseRejection::CannotFitWithinCeiling,
+            }
+        )
+    }));
+
+    // Granted RingId values must be unique among all live leases.
+    let ids = harness
+        .live_leases()
+        .iter()
+        .map(|lease| lease.ring_id)
+        .collect::<std::collections::BTreeSet<_>>();
+    assert_eq!(ids.len(), harness.live_leases().len());
+}
+
+// This proves live leases are non-overlapping, in-bounds, aligned, and stable
+// for the lease lifetime.
+#[test]
+fn live_layouts_are_non_overlapping_aligned_in_bounds_and_stable() {
+    // Lease two rings with explicit alignment requirements.
+    let mut harness = new_arena();
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 512, 64)));
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(2, 512, 128)));
+
+    // Read the public lease snapshots.
+    let leases = harness.live_leases().to_vec();
+    assert_eq!(leases.len(), 2);
+
+    // Prove non-overlap and in-bounds without constraining allocator placement.
+    assert_non_overlapping(&leases[0].layout, &leases[1].layout);
+    for lease in &leases {
+        assert!(lease.layout.end_offset <= arena_config().reservation_ceiling);
+        assert_eq!(lease.layout.start_offset % lease.requested_alignment, 0);
+    }
+
+    // Re-observing the same live lease must not change offsets.
+    let before = leases[0].layout.clone();
+    let after = harness
+        .lookup_lease(leases[0].ring_id)
+        .expect("live lease must be lookupable")
+        .layout
+        .clone();
+    assert_eq!(after, before);
+}
+
+// This proves CancelLease removes queued work and suppresses later hot-path
+// installation, including a fresh lease that races with cancellation.
+#[test]
+fn cancelled_queued_lease_never_installs_hot_path_state() {
+    // Fill the arena and queue a second satisfiable lease.
+    let mut harness = new_arena();
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 3072, 64)));
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(2, 1024, 64)));
+
+    // Cancel the queued request before it is leased.
+    harness.request(arena::ArenaRequest::CancelLease {
+        request_id: arena::LeaseRequestId(2),
+    });
+
+    // Releasing pressure must not install worker or pump state for the canceled
+    // request.
+    let live = harness.live_leases()[0].ring_id;
+    harness.request(arena::ArenaRequest::ReleaseRing {
+        ring_id: live,
+        proof: arena::QuiescenceProof::verified(),
+    });
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            arena::ArenaCommand::InstallWorkerOrPumpState {
+                request_id: arena::LeaseRequestId(2),
+                ..
+            }
+        )
+    }));
+
+    // If a fresh lease was produced during the race, it must be released instead
+    // of becoming hot-path state.
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            arena::ArenaEvent::CancelledFreshLeaseReleased {
+                request_id: arena::LeaseRequestId(2)
+            }
+        )
+    }));
+}
+
+// This proves ranges are released only with quiescence proof, are not reused
+// while live work owns them, and may be reused after release.
+#[test]
+fn release_requires_quiescence_and_reuse_happens_only_after_release() {
+    // Lease one ring and record its range.
+    let mut harness = new_arena();
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 1024, 64)));
+    let first = harness.live_leases()[0].clone();
+
+    // Release without proof must reject and keep the range live.
+    harness.request(arena::ArenaRequest::ReleaseRing {
+        ring_id: first.ring_id,
+        proof: arena::QuiescenceProof::missing(),
+    });
+    assert!(harness.lookup_lease(first.ring_id).is_some());
+
+    // A second lease while the first is live must not overlap the first range.
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(2, 1024, 64)));
+    let second = harness
+        .live_leases()
+        .iter()
+        .find(|lease| lease.ring_id != first.ring_id)
+        .expect("second live lease must exist")
+        .clone();
+    assert_non_overlapping(&first.layout, &second.layout);
+
+    // Verified quiescence allows release, after which reuse is legal.
+    harness.request(arena::ArenaRequest::ReleaseRing {
+        ring_id: first.ring_id,
+        proof: arena::QuiescenceProof::verified(),
+    });
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(3, 1024, 64)));
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, arena::ArenaEvent::RingLeased { .. })
+    }));
+}
+
+// This proves shutdown rejects new leases, preserves live lease records, and
+// does not release live ranges without quiescence proof.
+#[test]
+fn shutdown_rejects_new_leases_without_corrupting_live_records() {
+    // Create a live lease before shutdown.
+    let mut harness = new_arena();
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(1, 512, 64)));
+    let live_before = harness.live_leases().to_vec();
+
+    // Shut the arena down.
+    harness.request(arena::ArenaRequest::Shutdown);
+
+    // New leases are rejected after shutdown.
+    harness.request(arena::ArenaRequest::LeaseRing(lease_request(2, 512, 64)));
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            arena::ArenaEvent::RingLeaseRejected {
+                request_id: arena::LeaseRequestId(2),
+                reason: arena::RingLeaseRejection::ArenaShuttingDown,
+            }
+        )
+    }));
+
+    // Existing live lease records remain intact until proof-backed release.
+    assert_eq!(harness.live_leases(), live_before.as_slice());
+}

tests/mvp_system/device_bridge_guarantees.rs

@@ -0,0 +1,240 @@
+//! Black-box contract tests for MVP device bridge behavior.
+//!
+//! These tests intentionally know only the public device-bridge surface:
+//!
+//! - allocation, host/device copy, view, compute-use, restart, and free requests
+//!   in
+//! - fake backend calls, completion events, handles, and failures out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/device_bridge_contract.md`.
+
+use mvp_system::device_bridge as device;
+
+// The object spec is small and aligned so exact range checks are readable. The
+// bridge remains free to choose backend-specific allocation details.
+fn object_spec() -> device::ObjectSpec {
+    device::ObjectSpec {
+        max_extent: 16,
+        alignment: 4,
+        dtype: device::DType::U32,
+        shape: device::Shape::Vector,
+    }
+}
+
+// The harness records fake backend calls and public bridge outcomes. Tests do
+// not inspect device memory or tinygrad internals.
+fn new_bridge() -> device::DeviceBridgeHarness {
+    device::DeviceBridgeHarness::new(device::WorkerGeneration(1))
+}
+
+// This helper allocates one current-generation device object for copy and view
+// tests. It keeps tests on the public allocation path.
+fn allocated_bridge() -> (device::DeviceBridgeHarness, device::DeviceHandle) {
+    let mut harness = new_bridge();
+    let handle = harness
+        .alloc_device(object_spec(), 8)
+        .expect("valid allocation must succeed");
+    (harness, handle)
+}
+
+// This proves alloc_device creates a current-generation allocation suitable for
+// the object spec and extent, and allocation failure is reported as device
+// allocation failure.
+#[test]
+fn allocation_creates_current_generation_handle_or_typed_failure() {
+    // Allocate a valid object.
+    let mut harness = new_bridge();
+    let handle = harness
+        .alloc_device(object_spec(), 8)
+        .expect("valid allocation must succeed");
+
+    // The handle is tied to the current worker generation.
+    assert_eq!(handle.generation, device::WorkerGeneration(1));
+    assert!(harness.backend_calls().iter().any(|call| {
+        matches!(
+            call,
+            device::BackendCall::Alloc {
+                spec,
+                extent: 8,
+                ..
+            } if *spec == object_spec()
+        )
+    }));
+
+    // Backend allocation failure becomes typed allocation failure.
+    harness.inject_backend_failure(device::BackendFailure::AllocationFailed);
+    let failure = harness
+        .alloc_device(object_spec(), 8)
+        .expect_err("backend allocation failure must surface");
+    assert_eq!(failure, device::DeviceError::AllocationFailed);
+}
+
+// This proves host_to_device copies exactly the requested host range to the
+// requested device range, and bytes become safe to release only after the copy
+// returns or the asynchronous completion event fires.
+#[test]
+fn host_to_device_copies_exact_range_and_defers_release_until_safe() {
+    // Allocate a device object and request an asynchronous copy.
+    let (mut harness, handle) = allocated_bridge();
+    let copy = harness.host_to_device(
+        device::HostRange { offset: 4, len: 8 },
+        device::DeviceRange { handle, offset: 0, len: 8 },
+        device::CopyMode::Async,
+    ).expect("copy request must be accepted");
+
+    // The backend sees the exact ranges.
+    assert!(harness.backend_calls().iter().any(|call| {
+        matches!(
+            call,
+            device::BackendCall::HostToDevice {
+                host: device::HostRange { offset: 4, len: 8 },
+                device: device::DeviceRange { offset: 0, len: 8, .. },
+                ..
+            }
+        )
+    }));
+
+    // Async copy request alone is not a release proof.
+    assert!(!harness.safe_to_release_host(copy));
+
+    // Completion makes bytes safe to release.
+    harness.observe(device::DeviceEvent::CopyCompleted { copy });
+    assert!(harness.safe_to_release_host(copy));
+}
+
+// This proves device_to_host copies exactly the requested device range to the
+// requested host range, and host bytes become valid only after return or copy
+// completion.
+#[test]
+fn device_to_host_copies_exact_range_and_defers_host_validity_until_safe() {
+    // Allocate a device object and request an asynchronous device-to-host copy.
+    let (mut harness, handle) = allocated_bridge();
+    let copy = harness.device_to_host(
+        device::DeviceRange { handle, offset: 0, len: 8 },
+        device::HostRange { offset: 12, len: 8 },
+        device::CopyMode::Async,
+    ).expect("copy request must be accepted");
+
+    // The backend sees the exact ranges.
+    assert!(harness.backend_calls().iter().any(|call| {
+        matches!(
+            call,
+            device::BackendCall::DeviceToHost {
+                device: device::DeviceRange { offset: 0, len: 8, .. },
+                host: device::HostRange { offset: 12, len: 8 },
+                ..
+            }
+        )
+    }));
+
+    // Host bytes are invalid until completion.
+    assert!(!harness.host_bytes_valid(copy));
+    harness.observe(device::DeviceEvent::CopyCompleted { copy });
+    assert!(harness.host_bytes_valid(copy));
+}
+
+// This proves wrap_for_tinygrad creates a compatible view matching the role
+// tensor spec, and invalid view shape or dtype fails the step.
+#[test]
+fn tinygrad_view_matches_role_tensor_spec_or_fails_step() {
+    // Allocate a valid object and wrap it for a matching role tensor view.
+    let (mut harness, handle) = allocated_bridge();
+    let view = harness
+        .wrap_for_tinygrad(
+            handle,
+            device::TensorViewSpec {
+                dtype: device::DType::U32,
+                shape: device::Shape::Vector,
+            },
+        )
+        .expect("matching tensor view must succeed");
+    assert_eq!(view.dtype, device::DType::U32);
+    assert_eq!(view.shape, device::Shape::Vector);
+
+    // Invalid dtype fails the step at the bridge boundary.
+    let failure = harness
+        .wrap_for_tinygrad(
+            handle,
+            device::TensorViewSpec {
+                dtype: device::DType::F16,
+                shape: device::Shape::Vector,
+            },
+        )
+        .expect_err("invalid dtype must fail");
+    assert_eq!(failure, device::DeviceError::InvalidViewDType);
+}
+
+// This proves allocations are not freed while compute or copy events depend on
+// them, free_device releases after dependencies clear, restart invalidates old
+// handles, and old-generation handles are rejected.
+#[test]
+fn lifetime_blocks_free_until_dependencies_clear_and_rejects_old_generation() {
+    // Allocate a handle and mark it used by compute and copy.
+    let (mut harness, handle) = allocated_bridge();
+    harness.observe(device::DeviceEvent::ComputeStarted {
+        handle,
+        step_id: device::StepId(77),
+    });
+    let copy = harness.host_to_device(
+        device::HostRange { offset: 0, len: 8 },
+        device::DeviceRange { handle, offset: 0, len: 8 },
+        device::CopyMode::Async,
+    ).expect("copy request must be accepted");
+
+    // Free is blocked while compute/copy depends on the allocation.
+    assert_eq!(
+        harness.free_device(handle),
+        Err(device::DeviceError::AllocationStillInUse)
+    );
+
+    // Complete dependencies, then free succeeds.
+    harness.observe(device::DeviceEvent::ComputeCompleted {
+        handle,
+        step_id: device::StepId(77),
+    });
+    harness.observe(device::DeviceEvent::CopyCompleted { copy });
+    assert_eq!(harness.free_device(handle), Ok(()));
+    assert!(harness.backend_calls().iter().any(|call| {
+        matches!(call, device::BackendCall::Free { freed } if *freed == handle)
+    }));
+
+    // Restart invalidates prior handles.
+    harness.observe(device::DeviceEvent::WorkerRestarted {
+        generation: device::WorkerGeneration(2),
+    });
+    assert_eq!(
+        harness.free_device(handle),
+        Err(device::DeviceError::OldGenerationHandle)
+    );
+}
+
+// This proves copy and view backend failures surface as typed copy or step
+// failures rather than ambiguous panics or logs.
+#[test]
+fn backend_copy_and_view_failures_are_typed() {
+    // Copy failure is reported as device copy failure.
+    let (mut harness, handle) = allocated_bridge();
+    harness.inject_backend_failure(device::BackendFailure::CopyFailed);
+    let copy_failure = harness
+        .host_to_device(
+            device::HostRange { offset: 0, len: 8 },
+            device::DeviceRange { handle, offset: 0, len: 8 },
+            device::CopyMode::Sync,
+        )
+        .expect_err("copy failure must surface");
+    assert_eq!(copy_failure, device::DeviceError::DeviceCopyFailed);
+
+    // View failure is reported as a step-visible invalid view.
+    harness.inject_backend_failure(device::BackendFailure::InvalidView);
+    let view_failure = harness
+        .wrap_for_tinygrad(
+            handle,
+            device::TensorViewSpec {
+                dtype: device::DType::U32,
+                shape: device::Shape::Vector,
+            },
+        )
+        .expect_err("invalid backend view must surface");
+    assert_eq!(view_failure, device::DeviceError::InvalidTensorView);
+}

tests/mvp_system/driver_pumps_guarantees.rs

@@ -0,0 +1,259 @@
+//! Black-box contract tests for MVP driver and pump behavior.
+//!
+//! These tests intentionally know only the public driver surface:
+//!
+//! - establish-send/recv, incoming stream, wake, stop, and I/O outcomes in
+//! - stream opens, ring cursor updates, wake hints, faults, and stopped events out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/driver_pumps_contract.md`.
+
+use mvp_system::driver_pumps as driver;
+
+// A driver config names one endpoint and one ALPN. Tests do not expose tokio
+// tasks, connection internals, or stream futures to actors.
+fn driver_config() -> driver::DriverConfig {
+    driver::DriverConfig {
+        local_node_id: driver::NodeId(10),
+        alpn: driver::Alpn("swactor-edge-mvp".into()),
+    }
+}
+
+// A send spec describes one persistent uni-stream for one edge to one peer.
+// The pump still owns when and how bytes leave the egress ring.
+fn send_spec() -> driver::EstablishSend {
+    driver::EstablishSend {
+        edge_id: driver::EdgeId(7001),
+        peer_node_id: driver::NodeId(11),
+        layout: driver::RingLayout::test_egress(),
+    }
+}
+
+// A recv spec describes one edge and one ingress ring. It may arrive before or
+// after the network stream, which is the receive rendezvous guarantee.
+fn recv_spec() -> driver::EstablishRecv {
+    driver::EstablishRecv {
+        edge_id: driver::EdgeId(7001),
+        layout: driver::RingLayout::test_ingress(),
+    }
+}
+
+// The harness gives tests mock stream and ring observations while keeping the
+// driver as the owner of demux and byte-pump behavior.
+fn new_driver() -> driver::DriverHarness {
+    driver::DriverHarness::new(driver_config())
+}
+
+// This helper extracts the byte transcript for a stream. It proves preamble and
+// object bytes by observing writes accepted by the mock stream, not by peeking
+// into pump internals.
+fn written_bytes(harness: &driver::DriverHarness, edge_id: driver::EdgeId) -> Vec<u8> {
+    harness
+        .stream_writes(edge_id)
+        .iter()
+        .flat_map(|write| write.bytes.clone())
+        .collect()
+}
+
+// This proves the driver owns endpoint, connection cache, ALPN, stream demux,
+// and send/recv pump tasks, while actors do not poll stream futures directly.
+#[test]
+fn driver_owns_endpoint_connection_demux_and_pump_tasks() {
+    // Create the driver and establish a send edge.
+    let mut harness = new_driver();
+    harness.observe(driver::DriverEvent::EstablishSend(send_spec()));
+
+    // The driver creates or reuses a connection under its endpoint and ALPN.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            driver::DriverCommand::OpenOrReuseConnection {
+                peer_node_id: driver::NodeId(11),
+                alpn: driver::Alpn(ref value),
+                ..
+            } if value == "swactor-edge-mvp"
+        )
+    }));
+
+    // Pump tasks are driver-owned.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, driver::DriverCommand::SpawnSendPump { edge_id: driver::EdgeId(7001), .. })
+    }));
+
+    // Actor commands must not expose stream polling.
+    assert!(!harness.actor_messages().iter().any(|message| {
+        matches!(message, driver::ActorMessage::PollStreamFuture { .. })
+    }));
+}
+
+// This proves each edge uses one persistent uni-stream, writes an edge-id
+// preamble once, carries object records as bytes after the preamble, and does
+// not open one stream per object.
+#[test]
+fn send_stream_is_persistent_with_single_edge_preamble() {
+    // Establish one send edge and make two committed egress records readable.
+    let mut harness = new_driver();
+    harness.observe(driver::DriverEvent::EstablishSend(send_spec()));
+    harness.observe(driver::DriverEvent::EgressBytesCommitted {
+        edge_id: driver::EdgeId(7001),
+        bytes: b"obj0".to_vec(),
+    });
+    harness.observe(driver::DriverEvent::RingReadable {
+        edge_id: driver::EdgeId(7001),
+    });
+    harness.observe(driver::DriverEvent::EgressBytesCommitted {
+        edge_id: driver::EdgeId(7001),
+        bytes: b"obj1".to_vec(),
+    });
+    harness.observe(driver::DriverEvent::RingReadable {
+        edge_id: driver::EdgeId(7001),
+    });
+
+    // Only one stream is opened for the edge.
+    let stream_opens = harness
+        .commands()
+        .iter()
+        .filter(|command| matches!(command, driver::DriverCommand::OpenUniStream { .. }))
+        .count();
+    assert_eq!(stream_opens, 1);
+
+    // The edge preamble appears once before object bytes.
+    let bytes = written_bytes(&harness, driver::EdgeId(7001));
+    assert!(bytes.starts_with(&driver::encode_edge_preamble(driver::EdgeId(7001))));
+    let preamble_count = driver::count_preamble_occurrences(&bytes, driver::EdgeId(7001));
+    assert_eq!(preamble_count, 1);
+}
+
+// This proves receive rendezvous works in both arrival orders and that a
+// pending stream is not read before the receive spec exists.
+#[test]
+fn recv_rendezvous_starts_pump_only_after_spec_and_stream_exist() {
+    // Spec first, stream second.
+    let mut spec_first = new_driver();
+    spec_first.observe(driver::DriverEvent::EstablishRecv(recv_spec()));
+    assert!(!spec_first.commands().iter().any(|command| {
+        matches!(command, driver::DriverCommand::SpawnRecvPump { .. })
+    }));
+    spec_first.observe(driver::DriverEvent::IncomingUniStream {
+        edge_id: driver::EdgeId(7001),
+        stream_id: driver::StreamId(1),
+    });
+    assert!(spec_first.commands().iter().any(|command| {
+        matches!(command, driver::DriverCommand::SpawnRecvPump { edge_id: driver::EdgeId(7001), .. })
+    }));
+
+    // Stream first, spec second.
+    let mut stream_first = new_driver();
+    stream_first.observe(driver::DriverEvent::IncomingUniStream {
+        edge_id: driver::EdgeId(7001),
+        stream_id: driver::StreamId(2),
+    });
+    assert!(!stream_first.stream_reads_started(driver::StreamId(2)));
+    stream_first.observe(driver::DriverEvent::EstablishRecv(recv_spec()));
+    assert!(stream_first.stream_reads_started(driver::StreamId(2)));
+}
+
+// This proves the recv pump is byte-blind after demux, copies QUIC bytes into
+// ingress ring spans, advances commit after copy, emits readable wakes, and
+// stops reading under backpressure.
+#[test]
+fn recv_pump_copies_bytes_without_parsing_and_respects_backpressure() {
+    // Rendezvous a receive pump.
+    let mut harness = new_driver();
+    harness.observe(driver::DriverEvent::IncomingUniStream {
+        edge_id: driver::EdgeId(7001),
+        stream_id: driver::StreamId(1),
+    });
+    harness.observe(driver::DriverEvent::EstablishRecv(recv_spec()));
+
+    // Deliver bytes that happen to look like an object header. The pump must
+    // copy them blindly, not parse them.
+    harness.observe(driver::DriverEvent::StreamBytesRead {
+        edge_id: driver::EdgeId(7001),
+        bytes: driver::fake_object_header_bytes(),
+    });
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, driver::DriverEventOut::ObjectHeaderParsed { .. })
+    }));
+    assert!(harness.ring_commit(driver::EdgeId(7001)) > 0);
+    assert!(harness.wake_hints().iter().any(|wake| {
+        matches!(wake, driver::WakeHint::RingReadable { edge_id: driver::EdgeId(7001) })
+    }));
+
+    // With no ring space, the pump stops reading and waits for RingWritable.
+    harness.observe(driver::DriverEvent::IngressRingFull {
+        edge_id: driver::EdgeId(7001),
+    });
+    assert!(!harness.is_reading_stream(driver::EdgeId(7001)));
+    harness.observe(driver::DriverEvent::RingWritable {
+        edge_id: driver::EdgeId(7001),
+    });
+    assert!(harness.is_reading_stream(driver::EdgeId(7001)));
+}
+
+// This proves the send pump writes committed egress bytes, advances consume
+// only after write_all accepts bytes, emits writable wakes, and keeps ownership
+// of unread bytes while network flow control stalls.
+#[test]
+fn send_pump_advances_consume_only_after_write_acceptance() {
+    // Establish a send pump and make bytes readable.
+    let mut harness = new_driver();
+    harness.observe(driver::DriverEvent::EstablishSend(send_spec()));
+    harness.observe(driver::DriverEvent::EgressBytesCommitted {
+        edge_id: driver::EdgeId(7001),
+        bytes: b"payload".to_vec(),
+    });
+    harness.observe(driver::DriverEvent::NetworkStalled {
+        edge_id: driver::EdgeId(7001),
+    });
+
+    // Stalled network keeps ownership of unread ring bytes.
+    assert_eq!(harness.ring_consume(driver::EdgeId(7001)), 0);
+
+    // Once write_all accepts the bytes, consume advances and writable is hinted.
+    harness.observe(driver::DriverEvent::WriteAllAccepted {
+        edge_id: driver::EdgeId(7001),
+        byte_count: 7,
+    });
+    assert_eq!(harness.ring_consume(driver::EdgeId(7001)), 7);
+    assert!(harness.wake_hints().iter().any(|wake| {
+        matches!(wake, driver::WakeHint::RingWritable { edge_id: driver::EdgeId(7001) })
+    }));
+}
+
+// This proves read, write, protocol, and stop outcomes are surfaced as
+// StreamFault or PumpStopped events.
+#[test]
+fn driver_faults_and_stop_emit_stream_fault_or_pump_stopped() {
+    // Read error faults the receive edge.
+    let mut recv = new_driver();
+    recv.observe(driver::DriverEvent::IncomingUniStream {
+        edge_id: driver::EdgeId(7001),
+        stream_id: driver::StreamId(1),
+    });
+    recv.observe(driver::DriverEvent::EstablishRecv(recv_spec()));
+    recv.observe(driver::DriverEvent::ReadError {
+        edge_id: driver::EdgeId(7001),
+    });
+    assert!(recv.events().iter().any(|event| {
+        matches!(event, driver::DriverEventOut::StreamFault { edge_id: driver::EdgeId(7001), .. })
+    }));
+
+    // Write error faults the send edge.
+    let mut send = new_driver();
+    send.observe(driver::DriverEvent::EstablishSend(send_spec()));
+    send.observe(driver::DriverEvent::WriteError {
+        edge_id: driver::EdgeId(7001),
+    });
+    assert!(send.events().iter().any(|event| {
+        matches!(event, driver::DriverEventOut::StreamFault { edge_id: driver::EdgeId(7001), .. })
+    }));
+
+    // StopEdge stops the corresponding pump.
+    send.observe(driver::DriverEvent::StopEdge {
+        edge_id: driver::EdgeId(7001),
+    });
+    assert!(send.events().iter().any(|event| {
+        matches!(event, driver::DriverEventOut::PumpStopped { edge_id: driver::EdgeId(7001), .. })
+    }));
+}

tests/mvp_system/edge_establisher_guarantees.rs

@@ -0,0 +1,299 @@
+//! Black-box contract tests for MVP edge establishment.
+//!
+//! These tests intentionally know only the public EdgeEstablisher surface:
+//!
+//! - `ProvisionTx`, `ProvisionRx`, lease, ring-install, driver, stop, and fault
+//!   events in
+//! - arena, worker/token, driver, ready, fault, and release commands out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/edge_establisher_contract.md`.
+
+use mvp_system::edge_establisher as edge;
+
+// A send provision carries the consumer node id because the driver must know
+// where to send. It deliberately carries no remote actor address.
+fn tx_provision() -> edge::ProvisionTx {
+    edge::ProvisionTx {
+        run_id: edge::RunId(7),
+        edge_id: edge::EdgeId(7001),
+        local_node_id: edge::NodeId(10),
+        consumer_node_id: edge::NodeId(11),
+        object_spec: edge::ObjectSpec::test_activation(),
+        ring_spec: edge::RingSpec::test_activation(),
+    }
+}
+
+// A receive provision needs the shared edge id and local layout information
+// after leasing; it does not need producer actor addressing for data flow.
+fn rx_provision() -> edge::ProvisionRx {
+    edge::ProvisionRx {
+        run_id: edge::RunId(7),
+        edge_id: edge::EdgeId(7001),
+        local_node_id: edge::NodeId(11),
+        object_spec: edge::ObjectSpec::test_activation(),
+        ring_spec: edge::RingSpec::test_activation(),
+    }
+}
+
+// The harness records only public establishment outputs. Tests never inspect a
+// private edge record; they infer it from commands and lifecycle events.
+fn new_establisher() -> edge::EdgeEstablisherHarness {
+    edge::EdgeEstablisherHarness::new(edge::NodeId(10))
+}
+
+// This helper drives a successful lease and ring install for the tx edge. It is
+// used by driver and stop tests to stay on the public establishment path.
+fn leased_and_installed_tx() -> edge::EdgeEstablisherHarness {
+    let mut harness = new_establisher();
+    harness.observe(edge::EdgeEvent::ProvisionTx(tx_provision()));
+    harness.observe(edge::EdgeEvent::RingLeased {
+        request_id: edge::LeaseRequestId(1),
+        ring_id: edge::RingId(8001),
+        layout: edge::RingLayout::test_layout(0),
+    });
+    harness.observe(edge::EdgeEvent::RingInstalled {
+        edge_id: edge::EdgeId(7001),
+        ring_id: edge::RingId(8001),
+    });
+    harness
+}
+
+// This proves ProvisionTx and ProvisionRx create local edge records with the
+// required addressing facts and without remote actor addresses.
+#[test]
+fn provisioning_creates_local_edge_records_without_remote_actor_addresses() {
+    // Provision both sides through public messages.
+    let mut tx = new_establisher();
+    tx.observe(edge::EdgeEvent::ProvisionTx(tx_provision()));
+    let mut rx = edge::EdgeEstablisherHarness::new(edge::NodeId(11));
+    rx.observe(edge::EdgeEvent::ProvisionRx(rx_provision()));
+
+    // Tx must request a local lease and remember the consumer node id for the
+    // later driver command.
+    assert!(tx.commands().iter().any(|command| {
+        matches!(
+            command,
+            edge::EdgeCommand::LeaseRing {
+                edge_id: edge::EdgeId(7001),
+                ..
+            }
+        )
+    }));
+    assert_eq!(
+        tx.local_record(edge::EdgeId(7001)).unwrap().peer_node_id,
+        Some(edge::NodeId(11))
+    );
+
+    // Rx must create a receive record keyed by edge id.
+    assert!(rx.local_record(edge::EdgeId(7001)).is_some());
+
+    // Data-flow provisioning must not require remote actor addresses.
+    for record in [tx.local_record(edge::EdgeId(7001)).unwrap(), rx.local_record(edge::EdgeId(7001)).unwrap()] {
+        assert!(record.remote_actor_address.is_none());
+    }
+}
+
+// This proves lease events advance or fail only matching records, stale lease
+// events for stopped records do not install state, and unused fresh leases after
+// cancellation are released.
+#[test]
+fn lease_flow_matches_records_and_suppresses_stale_or_cancelled_leases() {
+    // Start one tx record and send a mismatched lease event.
+    let mut harness = new_establisher();
+    harness.observe(edge::EdgeEvent::ProvisionTx(tx_provision()));
+    harness.observe(edge::EdgeEvent::RingLeased {
+        request_id: edge::LeaseRequestId(99),
+        ring_id: edge::RingId(8999),
+        layout: edge::RingLayout::test_layout(0),
+    });
+
+    // Mismatched lease must not install worker or pump state.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::InstallWorkerRing { .. })
+    }));
+
+    // A matching rejection faults the record.
+    harness.observe(edge::EdgeEvent::RingLeaseRejected {
+        request_id: edge::LeaseRequestId(1),
+        reason: edge::RingLeaseRejection::CannotFit,
+    });
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            edge::EdgeLifecycleEvent::EdgeFaulted {
+                edge_id: edge::EdgeId(7001),
+                ..
+            }
+        )
+    }));
+
+    // Stop and then deliver a fresh lease; it must be released, not installed.
+    harness.observe(edge::EdgeEvent::StopEdge {
+        edge_id: edge::EdgeId(7001),
+    });
+    harness.observe(edge::EdgeEvent::RingLeased {
+        request_id: edge::LeaseRequestId(1),
+        ring_id: edge::RingId(8001),
+        layout: edge::RingLayout::test_layout(0),
+    });
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            edge::EdgeCommand::ReleaseArenaLease {
+                ring_id: edge::RingId(8001),
+                ..
+            }
+        )
+    }));
+}
+
+// This proves driver state is established only after worker or token endpoint
+// ring installation succeeds, using the ObjectSpec and RingSpec from
+// provisioning.
+#[test]
+fn worker_ring_install_precedes_driver_establishment_and_uses_provision_specs() {
+    // Provision and lease a tx edge.
+    let mut harness = new_establisher();
+    let provision = tx_provision();
+    harness.observe(edge::EdgeEvent::ProvisionTx(provision.clone()));
+    harness.observe(edge::EdgeEvent::RingLeased {
+        request_id: edge::LeaseRequestId(1),
+        ring_id: edge::RingId(8001),
+        layout: edge::RingLayout::test_layout(0),
+    });
+
+    // Before ring installation, no driver command may be issued.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::EstablishSend { .. })
+    }));
+
+    // Matching ring installation advances establishment.
+    harness.observe(edge::EdgeEvent::RingInstalled {
+        edge_id: edge::EdgeId(7001),
+        ring_id: edge::RingId(8001),
+    });
+
+    // The worker install command must carry the provisioned object/ring specs.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            edge::EdgeCommand::InstallWorkerRing {
+                object_spec,
+                ring_spec,
+                ..
+            } if *object_spec == provision.object_spec && *ring_spec == provision.ring_spec
+        )
+    }));
+
+    // Now the driver may be established.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::EstablishSend { edge_id: edge::EdgeId(7001), .. })
+    }));
+}
+
+// This proves send and receive driver establishment uses the correct public
+// arguments, and DriverEdgeReady is the readiness boundary for the local actor.
+#[test]
+fn driver_ready_marks_local_edge_actor_ready() {
+    // Drive tx through lease and ring install.
+    let mut tx = leased_and_installed_tx();
+
+    // EstablishSend must include edge id, consumer node id, and local layout.
+    assert!(tx.commands().iter().any(|command| {
+        matches!(
+            command,
+            edge::EdgeCommand::EstablishSend {
+                edge_id: edge::EdgeId(7001),
+                consumer_node_id: edge::NodeId(11),
+                layout,
+            } if *layout == edge::RingLayout::test_layout(0)
+        )
+    }));
+
+    // The edge is not ready until DriverEdgeReady arrives.
+    assert!(!tx.events().iter().any(|event| {
+        matches!(event, edge::EdgeLifecycleEvent::EdgeReady { .. })
+    }));
+    tx.observe(edge::EdgeEvent::DriverEdgeReady {
+        edge_id: edge::EdgeId(7001),
+    });
+    assert!(tx.events().iter().any(|event| {
+        matches!(
+            event,
+            edge::EdgeLifecycleEvent::EdgeReady {
+                edge_id: edge::EdgeId(7001),
+                ..
+            }
+        )
+    }));
+
+    // After readiness, stream and pump behavior belongs to the driver; the
+    // establisher should not emit hot-path byte commands.
+    assert!(!tx.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::CopyHotPathBytes { .. })
+    }));
+}
+
+// This proves StopEdge cancels queued leases, stops pumps, uninstalls worker
+// rings, releases arena lease only after proof, and makes Stopped terminal.
+#[test]
+fn stop_edge_tears_down_local_state_and_terminal_stopped_ignores_late_events() {
+    // Drive an edge to ready.
+    let mut harness = leased_and_installed_tx();
+    harness.observe(edge::EdgeEvent::DriverEdgeReady {
+        edge_id: edge::EdgeId(7001),
+    });
+
+    // Stop the edge.
+    harness.observe(edge::EdgeEvent::StopEdge {
+        edge_id: edge::EdgeId(7001),
+    });
+
+    // Stop commands must cover queued lease, pump, and worker ring cleanup.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::CancelQueuedLease { .. })
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::StopPump { .. })
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::UninstallWorkerRing { .. })
+    }));
+
+    // Arena release is withheld until quiescence proof arrives.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, edge::EdgeCommand::ReleaseArenaLease { .. })
+    }));
+    harness.observe(edge::EdgeEvent::QuiescenceProven {
+        ring_id: edge::RingId(8001),
+    });
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            edge::EdgeCommand::ReleaseArenaLease {
+                ring_id: edge::RingId(8001),
+                ..
+            }
+        )
+    }));
+
+    // Stopped is terminal: later stale events cannot revive readiness.
+    harness.observe(edge::EdgeEvent::Stopped {
+        edge_id: edge::EdgeId(7001),
+    });
+    let ready_before = harness
+        .events()
+        .iter()
+        .filter(|event| matches!(event, edge::EdgeLifecycleEvent::EdgeReady { .. }))
+        .count();
+    harness.observe(edge::EdgeEvent::DriverEdgeReady {
+        edge_id: edge::EdgeId(7001),
+    });
+    let ready_after = harness
+        .events()
+        .iter()
+        .filter(|event| matches!(event, edge::EdgeLifecycleEvent::EdgeReady { .. }))
+        .count();
+    assert_eq!(ready_after, ready_before);
+}

tests/mvp_system/gpu_worker_ctl_guarantees.rs

@@ -0,0 +1,266 @@
+//! Black-box contract tests for MVP GpuWorkerCtl behavior.
+//!
+//! These tests intentionally know only the public controller surface:
+//!
+//! - start, process, stdout event, actor command, crash, restart, and shutdown
+//!   observations in
+//! - serialized worker commands, routed events, faults, and stopped events out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/gpu_worker_ctl_contract.md`.
+
+use mvp_system::gpu_worker_ctl as ctl;
+
+// A test controller config names one worker process boundary. It does not grant
+// tests access to child-process internals or Python implementation details.
+fn worker_config() -> ctl::WorkerConfig {
+    ctl::WorkerConfig {
+        node_id: ctl::NodeId(10),
+        arena_env: ctl::ArenaEnv::test_default(),
+        initialization_timeout_ms: 1_000,
+    }
+}
+
+// The harness uses a fake process adapter at the public boundary. It lets tests
+// observe serialized commands and routed events without inspecting controller
+// state or private supervision tasks.
+fn new_controller() -> ctl::GpuWorkerCtlHarness {
+    ctl::GpuWorkerCtlHarness::new(worker_config())
+}
+
+// This helper starts the worker and drives it to running through public process
+// observations. Tests that need a running worker all use the same path.
+fn running_controller() -> ctl::GpuWorkerCtlHarness {
+    let mut harness = new_controller();
+    harness.observe(ctl::WorkerCtlEvent::StartWorker);
+    harness.observe(ctl::WorkerCtlEvent::ProcessStarted {
+        pid: ctl::ProcessId(1234),
+    });
+    harness.observe(ctl::WorkerCtlEvent::WorkerReady {
+        generation: ctl::WorkerGeneration(1),
+    });
+    harness
+}
+
+// The command fixture carries identities and handles but no payload bytes. It
+// exercises all command families that should be serialized only while running.
+fn current_generation_commands() -> Vec<ctl::ActorCommand> {
+    vec![
+        ctl::ActorCommand::InstallRing {
+            generation: ctl::WorkerGeneration(1),
+            ring_id: ctl::RingId(8001),
+        },
+        ctl::ActorCommand::ExecuteStep {
+            generation: ctl::WorkerGeneration(1),
+            step_id: ctl::StepId(9001),
+            input: ctl::DeviceHandle::new(ctl::WorkerGeneration(1), 42),
+        },
+        ctl::ActorCommand::ReleaseDeviceObject {
+            generation: ctl::WorkerGeneration(1),
+            handle: ctl::DeviceHandle::new(ctl::WorkerGeneration(1), 42),
+        },
+    ]
+}
+
+// This proves StartWorker spawns the process boundary, then sends
+// InitializeWorker, and WorkerReady moves the controller to running. Fatal,
+// process exit, and timeout move it to failed or crashed.
+#[test]
+fn worker_lifecycle_runs_start_initialize_ready_and_fault_paths() {
+    // Start the worker process.
+    let mut harness = new_controller();
+    harness.observe(ctl::WorkerCtlEvent::StartWorker);
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, ctl::WorkerCtlCommand::SpawnProcessActor { .. })
+    }));
+
+    // Process start triggers InitializeWorker.
+    harness.observe(ctl::WorkerCtlEvent::ProcessStarted {
+        pid: ctl::ProcessId(1234),
+    });
+    assert!(harness.serialized_worker_commands().iter().any(|command| {
+        matches!(command, ctl::WorkerCommand::InitializeWorker { .. })
+    }));
+
+    // WorkerReady emits a running lifecycle event.
+    harness.observe(ctl::WorkerCtlEvent::WorkerReady {
+        generation: ctl::WorkerGeneration(1),
+    });
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, ctl::WorkerCtlOut::WorkerRunning { generation: ctl::WorkerGeneration(1) })
+    }));
+
+    // Initialization timeout in a fresh controller is terminal failure.
+    let mut timed_out = new_controller();
+    timed_out.observe(ctl::WorkerCtlEvent::StartWorker);
+    timed_out.advance_time_ms(1_001);
+    assert!(timed_out.events().iter().any(|event| {
+        matches!(event, ctl::WorkerCtlOut::WorkerFailed { reason: ctl::WorkerFailure::InitializationTimeout, .. })
+    }));
+}
+
+// This proves valid actor commands are serialized only in running state, only
+// for the current generation, and never carry payload bytes.
+#[test]
+fn command_routing_requires_running_current_generation_and_is_payload_free() {
+    // Drive the controller to running.
+    let mut harness = running_controller();
+
+    // Send every current-generation command.
+    for command in current_generation_commands() {
+        harness.observe(ctl::WorkerCtlEvent::ActorCommand(command));
+    }
+
+    // All valid commands are serialized to the worker.
+    assert_eq!(harness.serialized_worker_commands().len(), current_generation_commands().len() + 1);
+
+    // Serialized commands must not contain payload bytes.
+    for command in harness.serialized_worker_commands() {
+        match command {
+            ctl::WorkerCommand::InitializeWorker { .. }
+            | ctl::WorkerCommand::InstallRing { .. }
+            | ctl::WorkerCommand::ExecuteStep { .. }
+            | ctl::WorkerCommand::ReleaseDeviceObject { .. }
+            | ctl::WorkerCommand::ShutdownWorker { .. } => {}
+            ctl::WorkerCommand::PayloadBytes { .. } => {
+                panic!("worker control command carried payload bytes: {command:?}")
+            }
+        }
+    }
+
+    // Old-generation handles must be rejected after restart.
+    harness.observe(ctl::WorkerCtlEvent::RestartRequested);
+    harness.observe(ctl::WorkerCtlEvent::ProcessStarted {
+        pid: ctl::ProcessId(1235),
+    });
+    harness.observe(ctl::WorkerCtlEvent::WorkerReady {
+        generation: ctl::WorkerGeneration(2),
+    });
+    harness.observe(ctl::WorkerCtlEvent::ActorCommand(ctl::ActorCommand::ExecuteStep {
+        generation: ctl::WorkerGeneration(1),
+        step_id: ctl::StepId(9002),
+        input: ctl::DeviceHandle::new(ctl::WorkerGeneration(1), 42),
+    }));
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, ctl::WorkerCtlOut::CommandRejected { reason: ctl::CommandRejection::OldGenerationHandle, .. })
+    }));
+}
+
+// This proves worker events parsed from stdout route to the correct local
+// control component.
+#[test]
+fn parsed_worker_events_route_to_their_control_owners() {
+    // Start from a running worker.
+    let mut harness = running_controller();
+
+    // Deliver each worker event family through stdout parsing.
+    harness.observe(ctl::WorkerCtlEvent::StdoutEvent(ctl::WorkerEvent::RingInstalled {
+        ring_id: ctl::RingId(8001),
+    }));
+    harness.observe(ctl::WorkerCtlEvent::StdoutEvent(ctl::WorkerEvent::ObjectLoaded {
+        object_id: ctl::ObjectId(9000),
+        sequence: 0,
+    }));
+    harness.observe(ctl::WorkerCtlEvent::StdoutEvent(ctl::WorkerEvent::ObjectProduced {
+        object_id: ctl::ObjectId(9001),
+        sequence: 0,
+    }));
+    harness.observe(ctl::WorkerCtlEvent::StdoutEvent(ctl::WorkerEvent::StepCompleted {
+        step_id: ctl::StepId(77),
+    }));
+    harness.observe(ctl::WorkerCtlEvent::StdoutEvent(ctl::WorkerEvent::RingReadable {
+        ring_id: ctl::RingId(8001),
+    }));
+
+    // Routing is proven by destination commands/events, not private dispatch
+    // tables.
+    assert!(harness.routed().iter().any(|route| matches!(route, ctl::RoutedEvent::ToEdgeEstablisher(_))));
+    assert!(harness.routed().iter().any(|route| matches!(route, ctl::RoutedEvent::ToRxOrRole(_))));
+    assert!(harness.routed().iter().any(|route| matches!(route, ctl::RoutedEvent::ToTxOrRole(_))));
+    assert!(harness.routed().iter().any(|route| matches!(route, ctl::RoutedEvent::ToStageController(_))));
+    assert!(harness.routed().iter().any(|route| matches!(route, ctl::RoutedEvent::ToDriverOrWorkerSide(_))));
+}
+
+// This proves worker crash invalidates old handles, roles, rings, in-flight
+// steps, synthesizes ring faults, asks the driver to stop pumps, and increments
+// generation on restart.
+#[test]
+fn crash_invalidates_generation_state_and_fans_out_faults() {
+    // Install one ring and start one step in generation 1.
+    let mut harness = running_controller();
+    harness.observe(ctl::WorkerCtlEvent::ActorCommand(ctl::ActorCommand::InstallRing {
+        generation: ctl::WorkerGeneration(1),
+        ring_id: ctl::RingId(8001),
+    }));
+    harness.observe(ctl::WorkerCtlEvent::ActorCommand(ctl::ActorCommand::ExecuteStep {
+        generation: ctl::WorkerGeneration(1),
+        step_id: ctl::StepId(9001),
+        input: ctl::DeviceHandle::new(ctl::WorkerGeneration(1), 42),
+    }));
+
+    // Crash the worker process.
+    harness.observe(ctl::WorkerCtlEvent::ProcessExited {
+        status: ctl::ExitStatus::Signal(9),
+    });
+
+    // Installed rings fault and affected pumps are stopped.
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, ctl::WorkerCtlOut::RingFaulted { ring_id: ctl::RingId(8001), .. })
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, ctl::WorkerCtlCommand::StopDriverPump { ring_id: ctl::RingId(8001), .. })
+    }));
+
+    // Restart increments worker generation.
+    harness.observe(ctl::WorkerCtlEvent::RestartRequested);
+    harness.observe(ctl::WorkerCtlEvent::ProcessStarted {
+        pid: ctl::ProcessId(1235),
+    });
+    harness.observe(ctl::WorkerCtlEvent::WorkerReady {
+        generation: ctl::WorkerGeneration(2),
+    });
+    assert_eq!(harness.current_generation(), ctl::WorkerGeneration(2));
+}
+
+// This proves graceful shutdown sends ShutdownWorker, observes WorkerStopped
+// before terminal stopped, and classifies installed rings according to the
+// observed worker/process outcome.
+#[test]
+fn graceful_shutdown_sends_worker_shutdown_and_reaches_terminal_stopped() {
+    // Start from a running worker with an installed ring.
+    let mut harness = running_controller();
+    harness.observe(ctl::WorkerCtlEvent::ActorCommand(ctl::ActorCommand::InstallRing {
+        generation: ctl::WorkerGeneration(1),
+        ring_id: ctl::RingId(8001),
+    }));
+
+    // Request graceful shutdown.
+    harness.observe(ctl::WorkerCtlEvent::ShutdownRequested);
+    assert!(harness.serialized_worker_commands().iter().any(|command| {
+        matches!(command, ctl::WorkerCommand::ShutdownWorker { .. })
+    }));
+
+    // WorkerStopped must precede terminal stopped.
+    harness.observe(ctl::WorkerCtlEvent::WorkerStopped {
+        generation: ctl::WorkerGeneration(1),
+    });
+    harness.observe(ctl::WorkerCtlEvent::ProcessExited {
+        status: ctl::ExitStatus::Code(0),
+    });
+    let worker_stopped_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, ctl::WorkerCtlOut::WorkerStopped { .. }))
+        .expect("WorkerStopped must be observed");
+    let terminal_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, ctl::WorkerCtlOut::TerminalStopped { .. }))
+        .expect("terminal stopped must be observed");
+    assert!(worker_stopped_pos < terminal_pos);
+
+    // Rings are marked quiesced on graceful stop.
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, ctl::WorkerCtlOut::RingQuiesced { ring_id: ctl::RingId(8001), .. })
+    }));
+}

tests/mvp_system/gpu_worker_egress_producer_guarantees.rs

@@ -0,0 +1,253 @@
+//! Black-box contract tests for MVP GPU worker egress production.
+//!
+//! These tests intentionally know only the public worker egress surface:
+//!
+//! - `InstallRing`, `ExecuteStep` output bindings, device-copy outcomes,
+//!   backpressure, and shutdown events in
+//! - committed ring bytes, cursor publication, `ObjectProduced`,
+//!   `StepCompleted`, and step failures out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/gpu_worker_egress_producer_contract.md`.
+
+use mvp_system::gpu_worker_egress_producer as egress;
+
+// A valid egress ring config supplies the edge object spec and current worker
+// generation. The producer remains free to choose copy scheduling internally.
+fn egress_ring() -> egress::InstallRing {
+    egress::InstallRing {
+        ring_id: egress::RingId(8002),
+        edge_id: egress::EdgeId(7002),
+        port_id: egress::PortId("out".into()),
+        direction: egress::RingDirection::Egress,
+        object_spec: egress::ObjectSpec {
+            max_extent: 16,
+            alignment: 4,
+            layout: egress::ObjectLayout::Token,
+        },
+        generation: egress::WorkerGeneration(1),
+    }
+}
+
+// The harness exposes egress ring writes and worker events, not private output
+// queues, device kernels, or role internals.
+fn new_producer() -> egress::EgressProducerHarness {
+    egress::EgressProducerHarness::new(egress::WorkerGeneration(1))
+}
+
+// This helper installs the output ring through the public worker command path.
+fn installed_producer() -> egress::EgressProducerHarness {
+    let mut harness = new_producer();
+    harness.observe(egress::WorkerEgressEvent::InstallRing(egress_ring()));
+    harness
+}
+
+// A valid output binding carries object identity, sequence, extent, flags, and
+// target ring. The worker must not invent these graph-visible facts.
+fn output_binding(sequence: u64, extent: u64) -> egress::OutputBinding {
+    egress::OutputBinding {
+        ring_id: egress::RingId(8002),
+        object_id: egress::ObjectId(9000 + sequence),
+        sequence,
+        extent,
+        flags: egress::ObjectFlags::default(),
+        device_source: egress::DeviceHandle::new(egress::WorkerGeneration(1), 40 + sequence),
+    }
+}
+
+// This proves egress production starts only after InstallRing, only for
+// ExecuteStep output bindings naming that ring, and never invents object ids or
+// sequence numbers.
+#[test]
+fn output_admission_requires_installed_ring_and_explicit_binding() {
+    // Execute before InstallRing must not write output.
+    let mut not_installed = new_producer();
+    not_installed.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![output_binding(0, 8)],
+    });
+    assert_eq!(not_installed.committed_bytes(egress::RingId(8002)).len(), 0);
+
+    // Install the ring and execute with a binding that names it.
+    let mut harness = installed_producer();
+    harness.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![output_binding(0, 8)],
+    });
+
+    // The pending output identity must match the binding exactly.
+    let pending = harness.pending_outputs();
+    assert_eq!(pending[0].object_id, egress::ObjectId(9000));
+    assert_eq!(pending[0].sequence, 0);
+    assert_eq!(pending[0].extent, 8);
+}
+
+// This proves the worker creates a valid ObjectHeader from ObjectSpec, writes
+// header bytes before payload bytes, advances commit only after valid header
+// bytes, and emits readable wake after committed header bytes.
+#[test]
+fn header_is_written_and_committed_before_payload() {
+    // Start one egress output.
+    let mut harness = installed_producer();
+    harness.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![output_binding(0, 8)],
+    });
+
+    // Complete header production but not payload copy.
+    harness.observe(egress::WorkerEgressEvent::HeaderReady {
+        object_id: egress::ObjectId(9000),
+    });
+
+    // The committed prefix must decode as a header for the configured spec.
+    let committed = harness.committed_bytes(egress::RingId(8002));
+    let header = egress::ObjectHeader::decode(committed).expect("header must decode");
+    assert_eq!(header.object_id, egress::ObjectId(9000));
+    assert_eq!(header.sequence, 0);
+    assert_eq!(header.extent, 8);
+
+    // Payload bytes are not committed before the payload copy is valid.
+    assert_eq!(harness.committed_payload_bytes(egress::RingId(8002)), 0);
+    assert!(harness.wake_hints().iter().any(|wake| {
+        matches!(wake, egress::WakeHint::RingReadable { ring_id: egress::RingId(8002) })
+    }));
+}
+
+// This proves payload production copies exactly extent bytes from device to the
+// egress ring, advances commit only after host bytes are valid, and blocks on
+// egress backpressure without dropping ownership.
+#[test]
+fn payload_copy_is_exact_extent_and_respects_backpressure() {
+    // Start one output with extent 8.
+    let mut harness = installed_producer();
+    harness.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![output_binding(0, 8)],
+    });
+    harness.observe(egress::WorkerEgressEvent::HeaderReady {
+        object_id: egress::ObjectId(9000),
+    });
+
+    // Backpressure prevents committing payload bytes.
+    harness.observe(egress::WorkerEgressEvent::EgressRingFull {
+        ring_id: egress::RingId(8002),
+    });
+    harness.observe(egress::WorkerEgressEvent::DeviceToHostCopyCompleted {
+        object_id: egress::ObjectId(9000),
+        byte_count: 4,
+    });
+    assert_eq!(harness.committed_payload_bytes(egress::RingId(8002)), 0);
+
+    // Once writable, the full exact extent can commit.
+    harness.observe(egress::WorkerEgressEvent::RingWritable {
+        ring_id: egress::RingId(8002),
+    });
+    harness.observe(egress::WorkerEgressEvent::DeviceToHostCopyCompleted {
+        object_id: egress::ObjectId(9000),
+        byte_count: 8,
+    });
+    assert_eq!(harness.committed_payload_bytes(egress::RingId(8002)), 8);
+}
+
+// This proves ObjectProduced is emitted after the full output object is
+// committed, and StepCompleted is emitted only after all declared outputs are
+// produced and role state updates are complete.
+#[test]
+fn object_produced_precedes_step_completed_after_all_outputs() {
+    // Execute a step with two outputs.
+    let mut harness = installed_producer();
+    harness.observe(egress::WorkerEgressEvent::InstallRing(egress::InstallRing {
+        ring_id: egress::RingId(8003),
+        edge_id: egress::EdgeId(7003),
+        port_id: egress::PortId("out2".into()),
+        ..egress_ring()
+    }));
+    harness.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![output_binding(0, 8), egress::OutputBinding {
+            ring_id: egress::RingId(8003),
+            object_id: egress::ObjectId(9100),
+            sequence: 0,
+            extent: 8,
+            flags: egress::ObjectFlags::default(),
+            device_source: egress::DeviceHandle::new(egress::WorkerGeneration(1), 55),
+        }],
+    });
+
+    // Produce only the first output and prove StepCompleted is still absent.
+    harness.complete_output(egress::ObjectId(9000));
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, egress::WorkerEgressOut::StepCompleted { .. })
+    }));
+
+    // Produce the second output and complete role state update.
+    harness.complete_output(egress::ObjectId(9100));
+    harness.observe(egress::WorkerEgressEvent::RoleStateUpdated {
+        step_id: egress::StepId(77),
+    });
+
+    // Both object-produced events precede StepCompleted.
+    let first_object_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, egress::WorkerEgressOut::ObjectProduced { object_id: egress::ObjectId(9000), .. }))
+        .expect("first object produced");
+    let second_object_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, egress::WorkerEgressOut::ObjectProduced { object_id: egress::ObjectId(9100), .. }))
+        .expect("second object produced");
+    let completed_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, egress::WorkerEgressOut::StepCompleted { step_id: egress::StepId(77), .. }))
+        .expect("step completed");
+    assert!(first_object_pos < completed_pos);
+    assert!(second_object_pos < completed_pos);
+}
+
+// This proves invalid output ring, extent violation, device copy failure, and
+// shutdown reject or abort egress production with visible step/ring faults.
+#[test]
+fn egress_faults_are_visible_and_suppress_success_events() {
+    // Invalid output ring fails the step.
+    let mut invalid_ring = installed_producer();
+    invalid_ring.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(77),
+        outputs: vec![egress::OutputBinding {
+            ring_id: egress::RingId(9999),
+            ..output_binding(0, 8)
+        }],
+    });
+    assert!(invalid_ring.events().iter().any(|event| {
+        matches!(event, egress::WorkerEgressOut::StepFailed { reason: egress::StepFailureReason::InvalidOutputRing, .. })
+    }));
+
+    // Extent violation fails the step.
+    let mut bad_extent = installed_producer();
+    bad_extent.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(78),
+        outputs: vec![output_binding(0, 32)],
+    });
+    assert!(bad_extent.events().iter().any(|event| {
+        matches!(event, egress::WorkerEgressOut::StepFailed { reason: egress::StepFailureReason::OutputExtentViolation, .. })
+    }));
+
+    // Copy failure faults the ring or fails the step, but must not emit
+    // ObjectProduced.
+    let mut copy_failed = installed_producer();
+    copy_failed.observe(egress::WorkerEgressEvent::ExecuteStep {
+        step_id: egress::StepId(79),
+        outputs: vec![output_binding(0, 8)],
+    });
+    copy_failed.observe(egress::WorkerEgressEvent::DeviceCopyFailed {
+        object_id: egress::ObjectId(9000),
+    });
+    assert!(copy_failed.events().iter().any(|event| {
+        matches!(event, egress::WorkerEgressOut::StepFailed { .. })
+            || matches!(event, egress::WorkerEgressOut::RingFault { .. })
+    }));
+    assert!(!copy_failed.events().iter().any(|event| {
+        matches!(event, egress::WorkerEgressOut::ObjectProduced { .. })
+    }));
+}

tests/mvp_system/gpu_worker_ingress_parser_guarantees.rs

@@ -0,0 +1,287 @@
+//! Black-box contract tests for MVP GPU worker ingress parsing.
+//!
+//! These tests intentionally know only the public worker ingress surface:
+//!
+//! - `InstallRing`, ring-readable wakes, committed ring bytes, EOF, and device
+//!   copy outcomes in
+//! - cursor changes, `ObjectLoaded`, `ObjectFailed`, and `RingFault` out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/gpu_worker_ingress_parser_contract.md`.
+
+use mvp_system::gpu_worker_ingress_parser as ingress;
+
+// A valid ingress ring config supplies the edge object spec and current worker
+// generation. The parser remains a black box behind ring helper operations.
+fn ingress_ring() -> ingress::InstallRing {
+    ingress::InstallRing {
+        ring_id: ingress::RingId(8001),
+        edge_id: ingress::EdgeId(7001),
+        port_id: ingress::PortId("in".into()),
+        direction: ingress::RingDirection::Ingress,
+        object_spec: ingress::ObjectSpec {
+            max_extent: 16,
+            alignment: 4,
+            layout: ingress::ObjectLayout::Token,
+        },
+        generation: ingress::WorkerGeneration(1),
+    }
+}
+
+// The harness observes only worker-facing ring and device events. Tests do not
+// parse private parser state or device allocation internals.
+fn new_parser() -> ingress::IngressParserHarness {
+    ingress::IngressParserHarness::new(ingress::WorkerGeneration(1))
+}
+
+// A valid object record is constructed through the public helper encoder so the
+// test proves parser behavior rather than hard-coded header bytes.
+fn valid_record(sequence: u64, extent: u64) -> Vec<u8> {
+    ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+        .object_id(ingress::ObjectId(9000 + sequence))
+        .sequence(sequence)
+        .extent(extent)
+        .payload(vec![7; extent as usize])
+        .encode()
+}
+
+// This helper installs the ingress ring through the public command path.
+fn installed_parser() -> ingress::IngressParserHarness {
+    let mut harness = new_parser();
+    harness.observe(ingress::WorkerIngressEvent::InstallRing(ingress_ring()));
+    harness
+}
+
+// This proves ingress parsing starts only after InstallRing, reloads cursors
+// after RingReadable, consumes committed bytes only, and does not read
+// uncommitted bytes.
+#[test]
+fn parser_reads_only_committed_bytes_after_ingress_ring_install() {
+    // Write committed bytes before install; the parser must not consume them.
+    let mut harness = new_parser();
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(0, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    assert_eq!(harness.consume_cursor(ingress::RingId(8001)), 0);
+
+    // Install the ingress ring and make committed bytes readable.
+    harness.observe(ingress::WorkerIngressEvent::InstallRing(ingress_ring()));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    assert!(harness.cursor_reload_count(ingress::RingId(8001)) > 0);
+
+    // Uncommitted bytes must not be read.
+    harness.write_uncommitted_bytes(ingress::RingId(8001), vec![1, 2, 3, 4]);
+    let before = harness.consume_cursor(ingress::RingId(8001));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    assert_eq!(harness.consume_cursor(ingress::RingId(8001)), before);
+}
+
+// This proves malformed or unsupported headers, max-extent violations,
+// alignment/layout violations, and sequence violations emit ObjectFailed.
+#[test]
+fn header_validation_rejects_invalid_object_records() {
+    // Each record corrupts one header fact in an installed parser.
+    let cases = vec![
+        (
+            ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+                .unsupported_magic()
+                .encode(),
+            ingress::ObjectFailureReason::UnsupportedMagic,
+        ),
+        (
+            ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+                .unsupported_version()
+                .encode(),
+            ingress::ObjectFailureReason::UnsupportedVersion,
+        ),
+        (
+            ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+                .malformed_header_length()
+                .encode(),
+            ingress::ObjectFailureReason::MalformedHeaderLength,
+        ),
+        (
+            ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+                .extent(32)
+                .payload(vec![0; 32])
+                .encode(),
+            ingress::ObjectFailureReason::ExtentExceedsMax,
+        ),
+        (
+            ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+                .extent(6)
+                .payload(vec![0; 6])
+                .encode(),
+            ingress::ObjectFailureReason::ExtentAlignmentViolation,
+        ),
+    ];
+
+    for (record, expected_reason) in cases {
+        // Use a fresh installed parser for each invalid object.
+        let mut harness = installed_parser();
+        harness.write_committed_bytes(ingress::RingId(8001), record);
+        harness.observe(ingress::WorkerIngressEvent::RingReadable {
+            ring_id: ingress::RingId(8001),
+        });
+
+        // The parser must emit a typed object failure.
+        assert!(harness.events().iter().any(|event| {
+            matches!(
+                event,
+                ingress::WorkerIngressOut::ObjectFailed {
+                    reason,
+                    ..
+                } if *reason == expected_reason
+            )
+        }));
+    }
+}
+
+// This proves the parser copies exactly extent payload bytes to device memory,
+// advances consume only after bytes are safe to release, can stream objects
+// larger than the ring through bounded spans, and faults EOF before full payload.
+#[test]
+fn payload_loading_is_exact_extent_and_release_after_copy_completion() {
+    // Install the parser and provide a valid record.
+    let mut harness = installed_parser();
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(0, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+
+    // Before device copy completion, consume must not advance past safe bytes.
+    let before_copy_complete = harness.consume_cursor(ingress::RingId(8001));
+    assert_eq!(before_copy_complete, 0);
+
+    // Complete the device copy and prove exact extent was copied.
+    harness.observe(ingress::WorkerIngressEvent::DeviceCopyCompleted {
+        object_id: ingress::ObjectId(9000),
+        byte_count: 8,
+    });
+    assert_eq!(
+        harness.device_copy_log().last().unwrap().byte_count,
+        8
+    );
+    assert!(harness.consume_cursor(ingress::RingId(8001)) > before_copy_complete);
+
+    // EOF mid-object faults the object.
+    let mut eof = installed_parser();
+    eof.write_committed_bytes(
+        ingress::RingId(8001),
+        ingress::ObjectRecordBuilder::new(ingress_ring().object_spec)
+            .object_id(ingress::ObjectId(9010))
+            .sequence(0)
+            .extent(12)
+            .partial_payload(vec![1, 2, 3])
+            .encode(),
+    );
+    eof.observe(ingress::WorkerIngressEvent::Eof {
+        ring_id: ingress::RingId(8001),
+    });
+    assert!(eof.events().iter().any(|event| {
+        matches!(
+            event,
+            ingress::WorkerIngressOut::ObjectFailed {
+                reason: ingress::ObjectFailureReason::EofBeforeFullPayload,
+                ..
+            }
+        )
+    }));
+}
+
+// This proves ObjectLoaded is emitted only after valid header, exact extent
+// copy, copy completion, device handle creation, and with current-generation
+// identity fields.
+#[test]
+fn object_loaded_requires_complete_valid_object_and_current_handle() {
+    // Install and parse one valid record.
+    let mut harness = installed_parser();
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(0, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+
+    // No ObjectLoaded may appear before device copy completion and handle
+    // creation.
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, ingress::WorkerIngressOut::ObjectLoaded { .. })
+    }));
+
+    // Complete device work.
+    harness.observe(ingress::WorkerIngressEvent::DeviceCopyCompleted {
+        object_id: ingress::ObjectId(9000),
+        byte_count: 8,
+    });
+    harness.observe(ingress::WorkerIngressEvent::DeviceHandleCreated {
+        object_id: ingress::ObjectId(9000),
+        handle: ingress::DeviceHandle::new(ingress::WorkerGeneration(1), 42),
+    });
+
+    // ObjectLoaded includes the required identities and current generation.
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            ingress::WorkerIngressOut::ObjectLoaded {
+                ring_id: ingress::RingId(8001),
+                edge_id: ingress::EdgeId(7001),
+                port_id,
+                object_id: ingress::ObjectId(9000),
+                sequence: 0,
+                extent: 8,
+                handle,
+            } if port_id == &ingress::PortId("in".into())
+                && handle.generation == ingress::WorkerGeneration(1)
+        )
+    }));
+}
+
+// This proves parser faults cover sequence violations and device allocation or
+// copy failures, and after RingFault the worker stops consuming until uninstall.
+#[test]
+fn sequence_and_device_failures_fault_and_ring_fault_stops_consumption() {
+    // Parse sequence 0 successfully.
+    let mut harness = installed_parser();
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(0, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    harness.observe(ingress::WorkerIngressEvent::DeviceCopyCompleted {
+        object_id: ingress::ObjectId(9000),
+        byte_count: 8,
+    });
+    harness.observe(ingress::WorkerIngressEvent::DeviceHandleCreated {
+        object_id: ingress::ObjectId(9000),
+        handle: ingress::DeviceHandle::new(ingress::WorkerGeneration(1), 42),
+    });
+
+    // Repeating sequence 0 violates sequence safety.
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(0, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            ingress::WorkerIngressOut::ObjectFailed {
+                reason: ingress::ObjectFailureReason::SequenceViolation,
+                ..
+            }
+        )
+    }));
+
+    // RingFault stops consumption until uninstall.
+    let before_fault = harness.consume_cursor(ingress::RingId(8001));
+    harness.observe(ingress::WorkerIngressEvent::RingFault {
+        ring_id: ingress::RingId(8001),
+    });
+    harness.write_committed_bytes(ingress::RingId(8001), valid_record(1, 8));
+    harness.observe(ingress::WorkerIngressEvent::RingReadable {
+        ring_id: ingress::RingId(8001),
+    });
+    assert_eq!(harness.consume_cursor(ingress::RingId(8001)), before_fault);
+}

tests/mvp_system/gpu_worker_process_adapter_guarantees.rs

@@ -0,0 +1,200 @@
+//! Black-box contract tests for the MVP GPU worker process adapter.
+//!
+//! These tests intentionally know only the public stdin/stdout adapter surface:
+//!
+//! - command JSON lines written to stdin
+//! - stdout JSON event lines and stderr diagnostic lines read back
+//! - adapter events and process faults out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/gpu_worker_process_adapter_contract.md`.
+
+use mvp_system::gpu_worker_process_adapter as adapter;
+
+// The adapter config supplies arena environment variables and an ABI version.
+// Tests do not assume how Python maps the arena or initializes tinygrad.
+fn adapter_config() -> adapter::AdapterConfig {
+    adapter::AdapterConfig {
+        arena_fd: adapter::ArenaFd(3),
+        arena_bytes: 4096,
+        helper_abi_version: adapter::HelperAbiVersion(1),
+    }
+}
+
+// The harness exposes fake stdin/stdout/stderr lines at the process boundary.
+// It does not expose worker internals or controller routing.
+fn new_adapter() -> adapter::ProcessAdapterHarness {
+    adapter::ProcessAdapterHarness::new(adapter_config())
+}
+
+// Valid control commands carry identities and handles, never payload bytes.
+// The command list exercises framing without depending on a specific JSON key
+// order.
+fn valid_commands() -> Vec<adapter::WorkerCommand> {
+    vec![
+        adapter::WorkerCommand::InitializeWorker {
+            helper_abi_version: adapter::HelperAbiVersion(1),
+        },
+        adapter::WorkerCommand::InstallRing {
+            ring_id: adapter::RingId(8001),
+        },
+        adapter::WorkerCommand::ExecuteStep {
+            step_id: adapter::StepId(9001),
+        },
+        adapter::WorkerCommand::ReleaseDeviceObject {
+            handle: adapter::DeviceHandle(42),
+        },
+        adapter::WorkerCommand::ShutdownWorker,
+    ]
+}
+
+// This helper proves payload bytes are absent from JSON values by checking the
+// public command/event representation before it crosses the process boundary.
+fn assert_no_payload_bytes(value: &adapter::JsonLine) {
+    assert!(
+        !value.contains_key("payload")
+            && !value.contains_key("bytes")
+            && !value.contains_key("data"),
+        "control JSON carried payload bytes: {value:?}"
+    );
+}
+
+// This proves commands and events are one JSON object per line, stderr is only
+// diagnostics, and payload bytes are forbidden in control JSON.
+#[test]
+fn control_stream_is_line_framed_json_without_payload_bytes() {
+    // Send every valid command through the adapter.
+    let mut harness = new_adapter();
+    for command in valid_commands() {
+        harness.send_command(command);
+    }
+
+    // Every stdin write must be exactly one JSON object followed by one newline.
+    for line in harness.stdin_lines() {
+        assert!(line.ends_with('\n'));
+        let parsed = adapter::JsonLine::parse(line).expect("stdin line must parse");
+        assert!(parsed.is_object());
+        assert_no_payload_bytes(&parsed);
+    }
+
+    // Stdout events are also one JSON object per line.
+    harness.receive_stdout_line(r#"{"type":"WorkerReady","generation":1}"#);
+    let event = harness.events().last().expect("stdout event must parse");
+    assert!(matches!(event, adapter::AdapterEvent::WorkerReady { .. }));
+
+    // Stderr alone is diagnostic and does not define lifecycle state.
+    harness.receive_stderr_line("loading tinygrad backend");
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::WorkerFatal { .. })
+    }));
+}
+
+// This proves worker initialization reads arena environment, waits for
+// InitializeWorker, maps the arena, initializes the helper and backend, and then
+// emits WorkerReady; failures emit WorkerFatal if possible and exit non-zero.
+#[test]
+fn initialization_order_is_env_initialize_map_helper_backend_ready() {
+    // Start the worker process with arena environment.
+    let mut harness = new_adapter();
+    harness.start_worker_process();
+
+    // Before InitializeWorker, no mapping or backend initialization may occur.
+    assert!(!harness.worker_actions().iter().any(|action| {
+        matches!(action, adapter::WorkerAction::MapArena { .. })
+            || matches!(action, adapter::WorkerAction::InitializeBackend { .. })
+    }));
+
+    // Send InitializeWorker and observe ordered worker actions.
+    harness.send_command(adapter::WorkerCommand::InitializeWorker {
+        helper_abi_version: adapter::HelperAbiVersion(1),
+    });
+    let actions = harness.worker_actions();
+    let env_pos = actions
+        .iter()
+        .position(|action| matches!(action, adapter::WorkerAction::ReadArenaEnvironment { .. }))
+        .expect("worker must read arena env");
+    let map_pos = actions
+        .iter()
+        .position(|action| matches!(action, adapter::WorkerAction::MapArena { .. }))
+        .expect("worker must map arena");
+    let helper_pos = actions
+        .iter()
+        .position(|action| matches!(action, adapter::WorkerAction::InitializeRingHelper { .. }))
+        .expect("worker must init helper");
+    let backend_pos = actions
+        .iter()
+        .position(|action| matches!(action, adapter::WorkerAction::InitializeBackend { .. }))
+        .expect("worker must init backend");
+    assert!(env_pos < map_pos && map_pos < helper_pos && helper_pos < backend_pos);
+
+    // Successful initialization emits WorkerReady.
+    harness.receive_stdout_line(r#"{"type":"WorkerReady","generation":1}"#);
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::WorkerReady { generation: adapter::WorkerGeneration(1) })
+    }));
+
+    // Initialization failure emits WorkerFatal if possible and exits non-zero.
+    let mut failed = new_adapter();
+    failed.start_worker_process();
+    failed.inject_initialization_failure(adapter::InitializationFailure::BackendUnavailable);
+    assert!(failed.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::WorkerFatal { .. })
+    }));
+    assert_ne!(failed.exit_status(), Some(adapter::ExitStatus::Code(0)));
+}
+
+// This proves invalid JSON, unknown event shapes, and unsupported helper ABI are
+// worker/process faults, while stderr output alone is not lifecycle state.
+#[test]
+fn parsing_and_abi_errors_fault_the_worker_process() {
+    // Invalid JSON faults the adapter.
+    let mut invalid_json = new_adapter();
+    invalid_json.receive_stdout_line("{not-json");
+    assert!(invalid_json.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::ProcessFault { reason: adapter::ProcessFaultReason::InvalidJson, .. })
+    }));
+
+    // Unknown event shape faults the adapter.
+    let mut unknown = new_adapter();
+    unknown.receive_stdout_line(r#"{"type":"NotAWorkerEvent"}"#);
+    assert!(unknown.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::ProcessFault { reason: adapter::ProcessFaultReason::UnknownEventShape, .. })
+    }));
+
+    // Unsupported helper ABI emits WorkerFatal.
+    let mut abi = new_adapter();
+    abi.send_command(adapter::WorkerCommand::InitializeWorker {
+        helper_abi_version: adapter::HelperAbiVersion(999),
+    });
+    assert!(abi.events().iter().any(|event| {
+        matches!(event, adapter::AdapterEvent::WorkerFatal { reason: adapter::WorkerFatalReason::UnsupportedHelperAbi, .. })
+    }));
+}
+
+// This proves command discipline: InstallRing, wake hints, ExecuteStep,
+// ReleaseDeviceObject, and ShutdownWorker are accepted only as control messages
+// and payload-bearing control JSON is rejected.
+#[test]
+fn command_discipline_rejects_payload_bearing_control_messages() {
+    // Valid control commands are accepted and framed.
+    let mut harness = new_adapter();
+    for command in valid_commands() {
+        harness.send_command(command);
+    }
+    assert_eq!(harness.command_rejections().len(), 0);
+
+    // Payload bytes in a control command are rejected at the adapter boundary.
+    harness.send_raw_json_command(r#"{"type":"ExecuteStep","step_id":1,"payload":[1,2,3]}"#);
+    assert!(harness.command_rejections().iter().any(|rejection| {
+        matches!(rejection.reason, adapter::CommandRejectionReason::PayloadBytesForbidden)
+    }));
+
+    // Wake hints reload cursors; they do not carry byte ranges or credits.
+    harness.send_command(adapter::WorkerCommand::RingReadable {
+        ring_id: adapter::RingId(8001),
+    });
+    let wake_line = harness.stdin_lines().last().expect("wake command must be written");
+    let parsed = adapter::JsonLine::parse(wake_line).expect("wake line must parse");
+    assert_no_payload_bytes(&parsed);
+    assert!(!parsed.contains_key("range") && !parsed.contains_key("credits"));
+}

tests/mvp_system/membership_pool_readiness_guarantees.rs

@@ -0,0 +1,223 @@
+//! Black-box contract tests for MVP membership and pool readiness.
+//!
+//! These tests intentionally know only the public readiness-gate surface:
+//!
+//! - a fixed orchestrator-owned candidate pool
+//! - membership, availability, and identity observations
+//! - emitted pool readiness, planning, and run fault events
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/membership_pool_readiness_contract.md`.
+
+use mvp_system::membership_pool_readiness as membership;
+
+// Three nodes are enough to prove all-node quantification without hiding behind
+// a single-node special case. The orchestrator owns this pool; SWIM only reports
+// liveness facts about it.
+fn candidate_pool() -> Vec<membership::NodeId> {
+    vec![
+        membership::NodeId(10),
+        membership::NodeId(11),
+        membership::NodeId(12),
+    ]
+}
+
+// The convergence window is short but non-zero so tests can prove PoolReady is
+// not emitted at the instant the last fact arrives.
+fn readiness_config() -> membership::ReadinessConfig {
+    membership::ReadinessConfig {
+        pool_id: membership::PoolId("mvp-test-pool".into()),
+        convergence_window_ms: 500,
+    }
+}
+
+// This helper provides every required public fact for one node. Tests use it to
+// build complete and deliberately incomplete pool views without observing any
+// private readiness bookkeeping.
+fn report_node_ready(
+    gate: &mut membership::ReadinessGateHarness,
+    node_id: membership::NodeId,
+) {
+    gate.observe(membership::Observation::NodeKnown { node_id });
+    gate.observe(membership::Observation::SwimLive { node_id });
+    gate.observe(membership::Observation::NodeAvailable { node_id });
+    gate.observe(membership::Observation::DataPlaneIdentityReady { node_id });
+}
+
+// The test harness records public events as a transcript. This helper counts a
+// specific event so duplicate readiness or duplicate faults are visible at the
+// contract boundary.
+fn count_pool_ready(events: &[membership::ReadinessEvent]) -> usize {
+    events
+        .iter()
+        .filter(|event| matches!(event, membership::ReadinessEvent::PoolReady { .. }))
+        .count()
+}
+
+// This proves PoolReady requires every candidate node, every required fact, no
+// suspect or faulted candidates, and a stable convergence window.
+#[test]
+fn pool_ready_requires_complete_stable_candidate_pool() {
+    // Build the readiness gate with an orchestrator-owned candidate pool.
+    let pool = candidate_pool();
+    let mut gate = membership::ReadinessGateHarness::new(readiness_config(), pool.clone());
+
+    // Report complete facts for every node except the final candidate.
+    report_node_ready(&mut gate, pool[0]);
+    report_node_ready(&mut gate, pool[1]);
+    gate.advance_time_ms(1_000);
+
+    // A partial pool must not become ready, even after time passes.
+    assert_eq!(count_pool_ready(gate.events()), 0);
+
+    // Report the final candidate, then prove the convergence window still
+    // matters by advancing less than the configured duration.
+    report_node_ready(&mut gate, pool[2]);
+    gate.advance_time_ms(499);
+    assert_eq!(count_pool_ready(gate.events()), 0);
+
+    // After the window, PoolReady must describe exactly the intended pool.
+    gate.advance_time_ms(1);
+    let ready = gate
+        .events()
+        .iter()
+        .find_map(|event| match event {
+            membership::ReadinessEvent::PoolReady { pool } => Some(pool),
+            _ => None,
+        })
+        .expect("complete stable pool must emit PoolReady");
+
+    // Compare as sets so ordering is not part of the behavioral contract.
+    let observed = ready.iter().copied().collect::<std::collections::BTreeSet<_>>();
+    let expected = pool.iter().copied().collect::<std::collections::BTreeSet<_>>();
+    assert_eq!(observed, expected);
+}
+
+// This proves suspect, faulted, missing, or identity-less candidates prevent
+// PoolReady rather than being silently ignored.
+#[test]
+fn unavailable_candidate_prevents_pool_ready() {
+    // Each case withholds or poisons one readiness fact for node 12.
+    let cases = [
+        membership::Observation::SwimSuspect {
+            node_id: membership::NodeId(12),
+        },
+        membership::Observation::NodeFaulted {
+            node_id: membership::NodeId(12),
+        },
+        membership::Observation::DataPlaneIdentityMissing {
+            node_id: membership::NodeId(12),
+        },
+    ];
+
+    for poisoned_fact in cases {
+        // Start each run from a fresh gate so one poisoned fact is responsible
+        // for the absence of readiness.
+        let pool = candidate_pool();
+        let mut gate = membership::ReadinessGateHarness::new(readiness_config(), pool.clone());
+
+        // Make every candidate otherwise known and available.
+        for node_id in &pool {
+            report_node_ready(&mut gate, *node_id);
+        }
+
+        // Poison the final candidate and wait past convergence.
+        gate.observe(poisoned_fact.clone());
+        gate.advance_time_ms(1_000);
+
+        // PoolReady must be absent because one required candidate is no longer
+        // available to the intended pool.
+        assert_eq!(count_pool_ready(gate.events()), 0);
+    }
+}
+
+// This proves run planning is gated by PoolReady. SWIM observations alone do
+// not start placement, and loss before a committed RunPlan prevents planning
+// from racing ahead.
+#[test]
+fn planning_starts_only_after_pool_ready_and_stops_if_readiness_is_lost() {
+    // Create a gate and ask the orchestrator to plan before readiness.
+    let pool = candidate_pool();
+    let mut gate = membership::ReadinessGateHarness::new(readiness_config(), pool.clone());
+    gate.request_run_planning(membership::RunRequest::new(membership::RunId(7)));
+
+    // With no PoolReady event, there must be no planning command.
+    assert!(!gate.commands().iter().any(|command| {
+        matches!(command, membership::ReadinessCommand::StartPlanning { .. })
+    }));
+
+    // Satisfy readiness, then immediately lose a required node before plan
+    // commit. The policy may wait or abort, but it must not commit placement.
+    for node_id in &pool {
+        report_node_ready(&mut gate, *node_id);
+    }
+    gate.advance_time_ms(500);
+    gate.observe(membership::Observation::SwimLost { node_id: pool[1] });
+
+    // No plan commitment command may be emitted from an unstable pool view.
+    assert!(!gate.commands().iter().any(|command| {
+        matches!(command, membership::ReadinessCommand::CommitRunPlan { .. })
+    }));
+}
+
+// This proves membership loss after provisioning is a run fault, not active
+// re-placement. The MVP run keeps its committed topology until teardown.
+#[test]
+fn required_node_loss_after_provisioning_faults_without_replacement() {
+    // Drive the pool to ready and mark a run as provisioned from that pool.
+    let pool = candidate_pool();
+    let mut gate = membership::ReadinessGateHarness::new(readiness_config(), pool.clone());
+    for node_id in &pool {
+        report_node_ready(&mut gate, *node_id);
+    }
+    gate.advance_time_ms(500);
+    gate.observe(membership::Observation::RunProvisioned {
+        run_id: membership::RunId(7),
+        required_nodes: pool.clone(),
+    });
+
+    // Lose one required node during the active run.
+    gate.observe(membership::Observation::SwimLost { node_id: pool[1] });
+
+    // The run must fault with a membership reason.
+    assert!(gate.events().contains(&membership::ReadinessEvent::RunFaulted {
+        run_id: membership::RunId(7),
+        reason: membership::RunFaultReason::RequiredNodeLost {
+            node_id: pool[1],
+        },
+    }));
+
+    // Re-placement would violate the committed-plan authority boundary.
+    assert!(!gate.commands().iter().any(|command| {
+        matches!(command, membership::ReadinessCommand::RecomputePlacement { .. })
+    }));
+}
+
+// This proves SWIM authority is limited to membership and liveness. It may
+// report facts, but it must not assign stages, edges, layers, or object specs.
+#[test]
+fn swim_observations_do_not_create_graph_assignments() {
+    // Feed a complete, stable membership view.
+    let pool = candidate_pool();
+    let mut gate = membership::ReadinessGateHarness::new(readiness_config(), pool.clone());
+    for node_id in &pool {
+        report_node_ready(&mut gate, *node_id);
+    }
+    gate.advance_time_ms(500);
+
+    // Walk emitted commands and reject any graph-assignment side effect.
+    for command in gate.commands() {
+        match command {
+            membership::ReadinessCommand::EmitPoolReady { .. }
+            | membership::ReadinessCommand::StartPlanning { .. }
+            | membership::ReadinessCommand::WaitForStability { .. }
+            | membership::ReadinessCommand::AbortPendingRun { .. } => {}
+            membership::ReadinessCommand::AssignStage { .. }
+            | membership::ReadinessCommand::AssignEdge { .. }
+            | membership::ReadinessCommand::AssignLayerRange { .. }
+            | membership::ReadinessCommand::AssignObjectSpec { .. } => {
+                panic!("membership gate emitted graph assignment: {command:?}")
+            }
+        }
+    }
+}

tests/mvp_system/node_boot_lifecycle_guarantees.rs

@@ -0,0 +1,204 @@
+//! Black-box contract tests for MVP node boot lifecycle.
+//!
+//! These tests intentionally know only the public node-boot surface:
+//!
+//! - `BootHarness::launch(config)`
+//! - public resource outcomes delivered into the harness
+//! - lifecycle events and provisioning admission observed from the harness
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/node_boot_lifecycle_contract.md`.
+
+use mvp_system::node_boot_lifecycle as boot;
+
+// A complete boot config lets the tests focus on ordering and failure behavior.
+// The concrete process, transport, arena, worker, and SWIM implementations are
+// outside this contract; the harness exposes only their observable outcomes.
+fn valid_boot_config() -> boot::BootConfig {
+    boot::BootConfig {
+        node_id: boot::NodeId(10),
+        intended_pool_id: boot::PoolId("mvp-test-pool".into()),
+        worker_policy: boot::WorkerStartPolicy::StartBeforeAvailable,
+    }
+}
+
+// The required facts are deliberately listed as public resource outcomes. That
+// makes the proof about the boot barrier rather than about any private boot FSM
+// state or the order in which an implementation happens to initialize resources.
+fn required_readiness_facts() -> Vec<boot::ResourceOutcome> {
+    vec![
+        boot::ResourceOutcome::RustProcessAlive,
+        boot::ResourceOutcome::RuntimeAcceptingControl,
+        boot::ResourceOutcome::StableNodeIdKnown(boot::NodeId(10)),
+        boot::ResourceOutcome::ArenaMapped,
+        boot::ResourceOutcome::GpuWorkerReady,
+        boot::ResourceOutcome::TransportEndpointBound,
+        boot::ResourceOutcome::SwimJoiningPool,
+        boot::ResourceOutcome::ProvisioningReceiverOpen,
+    ]
+}
+
+// Fault injection is one-per-resource so each failure must be explained by the
+// resource that failed. This prevents a broad "boot failed" bucket from hiding
+// which readiness fact was not satisfied.
+fn boot_fault_cases() -> Vec<(boot::ResourceOutcome, boot::BootFaultKind)> {
+    vec![
+        (
+            boot::ResourceOutcome::ArenaFault,
+            boot::BootFaultKind::ArenaConstructionFailed,
+        ),
+        (
+            boot::ResourceOutcome::GpuWorkerFault,
+            boot::BootFaultKind::WorkerStartupFailed,
+        ),
+        (
+            boot::ResourceOutcome::TransportEndpointFault,
+            boot::BootFaultKind::TransportEndpointFailed,
+        ),
+        (
+            boot::ResourceOutcome::InvalidNodeIdentity,
+            boot::BootFaultKind::InvalidNodeIdentity,
+        ),
+    ]
+}
+
+// This proves NodeAvailable is emitted only after every required local boot
+// resource is ready, and that a boot attempt resolves to one availability event
+// rather than a partial intermediate state.
+#[test]
+fn node_available_waits_for_all_required_readiness_facts() {
+    // Launch starts one public boot attempt in the intended pool.
+    let mut harness = boot::BootHarness::launch(valid_boot_config());
+
+    // Drive all but the final readiness fact and prove no prefix is sufficient.
+    let mut facts = required_readiness_facts();
+    let final_fact = facts.pop().expect("fixture has a final fact");
+    for fact in facts {
+        harness.observe(fact);
+        assert!(!harness.events().contains(&boot::LifecycleEvent::NodeAvailable {
+            node_id: boot::NodeId(10),
+        }));
+    }
+
+    // Once the final required fact arrives, availability becomes observable.
+    harness.observe(final_fact);
+
+    // Count the public event, not a private state bit; duplicate availability
+    // would make the boot attempt ambiguous to the orchestrator.
+    let available_count = harness
+        .events()
+        .iter()
+        .filter(|event| {
+            matches!(
+                event,
+                boot::LifecycleEvent::NodeAvailable {
+                    node_id
+                } if *node_id == boot::NodeId(10)
+            )
+        })
+        .count();
+    assert_eq!(available_count, 1);
+}
+
+// This proves run provisioning cannot race ahead of node availability. The
+// orchestrator can use NodeAvailable as the public admission point without
+// inspecting node-local boot state.
+#[test]
+fn provisioning_is_rejected_until_node_available_is_observed() {
+    // Launch the node and create a provision message that would be valid after
+    // boot finishes.
+    let mut harness = boot::BootHarness::launch(valid_boot_config());
+    let provision = boot::ProvisionRequest::for_node(boot::NodeId(10));
+
+    // Before readiness, provisioning must be rejected at the public boundary.
+    assert_eq!(
+        harness.try_accept_provisioning(provision.clone()),
+        Err(boot::ProvisioningAdmissionRejection::NodeNotAvailable)
+    );
+
+    // Complete readiness through observable facts only.
+    for fact in required_readiness_facts() {
+        harness.observe(fact);
+    }
+
+    // After NodeAvailable, the same request may enter run setup.
+    assert_eq!(harness.try_accept_provisioning(provision), Ok(()));
+}
+
+// This proves NodeAvailable is not overloaded with graph or weight meaning. A
+// booted node is eligible for orchestration, but it has not selected itself for
+// any stage, edge, layer range, role, or weight assignment.
+#[test]
+fn node_available_contains_no_run_assignment_or_weight_claims() {
+    // Complete node boot through the same public readiness facts as production.
+    let mut harness = boot::BootHarness::launch(valid_boot_config());
+    for fact in required_readiness_facts() {
+        harness.observe(fact);
+    }
+
+    // Inspect every emitted boot command. The proof is negative: boot may emit
+    // lifecycle facts, but it must not emit graph ownership commands.
+    for command in harness.commands() {
+        assert!(!matches!(command, boot::BootCommand::LoadWeights { .. }));
+        assert!(!matches!(command, boot::BootCommand::ConfigureRole { .. }));
+        assert!(!matches!(command, boot::BootCommand::EstablishEdge { .. }));
+        assert!(!matches!(command, boot::BootCommand::AssignStage { .. }));
+    }
+}
+
+// This proves every boot-blocking resource failure emits a typed boot fault and
+// keeps the node out of the candidate run pool.
+#[test]
+fn boot_resource_failure_faults_without_node_availability() {
+    // Each failure case runs in a fresh boot attempt so outcomes cannot mask
+    // each other.
+    for (failed_resource, expected_kind) in boot_fault_cases() {
+        let mut harness = boot::BootHarness::launch(valid_boot_config());
+
+        // Deliver the failed public resource outcome.
+        harness.observe(failed_resource);
+
+        // The emitted fault must carry the stable reason enum for operators and
+        // tests; logs are not part of the contract.
+        assert!(harness.events().contains(&boot::LifecycleEvent::NodeFaulted {
+            node_id: boot::NodeId(10),
+            kind: expected_kind,
+        }));
+
+        // A faulted boot attempt must not also become available.
+        assert!(!harness.events().iter().any(|event| {
+            matches!(event, boot::LifecycleEvent::NodeAvailable { .. })
+        }));
+
+        // The orchestrator-facing eligibility check must agree with the
+        // lifecycle transcript.
+        assert!(!harness.is_candidate_eligible(boot::NodeId(10)));
+    }
+}
+
+// This proves node boot authority is local-resource authority only. The node
+// may report boot facts, but stage, edge, layer, and object-spec assignment
+// remain absent until the orchestrator provisions a committed plan.
+#[test]
+fn boot_never_self_assigns_run_topology() {
+    // Complete a successful boot attempt.
+    let mut harness = boot::BootHarness::launch(valid_boot_config());
+    for fact in required_readiness_facts() {
+        harness.observe(fact);
+    }
+
+    // Walk every emitted command and require it to stay in the boot domain.
+    for command in harness.commands() {
+        match command {
+            boot::BootCommand::AdvertiseLifecycle { .. }
+            | boot::BootCommand::JoinMembership { .. }
+            | boot::BootCommand::OpenProvisioningInbox { .. } => {}
+            boot::BootCommand::AssignStage { .. }
+            | boot::BootCommand::AssignLayerRange { .. }
+            | boot::BootCommand::AssignEdge { .. }
+            | boot::BootCommand::AssignObjectSpec { .. } => {
+                panic!("boot emitted graph assignment command: {command:?}")
+            }
+        }
+    }
+}

tests/mvp_system/observability_surface_guarantees.rs

@@ -0,0 +1,275 @@
+//! Black-box contract tests for the MVP observability surface.
+//!
+//! These tests intentionally know only the public event stream surface:
+//!
+//! - structured lifecycle and fault events emitted by components
+//! - event identities, reason enums, and ordering observed by subscribers
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/observability_surface_contract.md`.
+
+use mvp_system::observability_surface as obs;
+
+// The trace fixture contains one successful run from boot through teardown.
+// Tests use structured events only; logs, transport, storage, and batching stay
+// outside the contract.
+fn successful_run_trace() -> Vec<obs::Event> {
+    obs::TraceBuilder::new(obs::RunId(7))
+        .node_started(obs::NodeId(10))
+        .node_available(obs::NodeId(10))
+        .pool_ready(vec![obs::NodeId(10)])
+        .run_planned()
+        .stage_provision_started(obs::StageIndex(0), obs::NodeId(10))
+        .weights_download_started(obs::StageIndex(0))
+        .weights_downloaded(obs::StageIndex(0))
+        .weights_loaded(obs::StageIndex(0))
+        .edge_provision_started(obs::EdgeId(7000))
+        .edge_ready(obs::EdgeId(7000))
+        .stage_ready(obs::StageIndex(0))
+        .readiness_barrier_passed()
+        .prompt_injected(obs::Sequence(0))
+        .object_loaded(obs::EdgeId(7000), obs::ObjectId(9000), obs::Sequence(0))
+        .execute_step_started(obs::StepId(77))
+        .object_produced(obs::EdgeId(7001), obs::ObjectId(9001), obs::Sequence(0))
+        .step_completed(obs::StepId(77))
+        .token_received(obs::ObjectId(9002), obs::Sequence(0))
+        .run_completed()
+        .stop_run_sent(obs::StageIndex(0))
+        .stage_stopped(obs::StageIndex(0))
+        .run_torn_down()
+        .finish()
+}
+
+// A fault trace gives the tests one stable reason enum and detecting component
+// without relying on diagnostic log text.
+fn fault_trace() -> Vec<obs::Event> {
+    obs::TraceBuilder::new(obs::RunId(7))
+        .node_started(obs::NodeId(10))
+        .node_available(obs::NodeId(10))
+        .pool_ready(vec![obs::NodeId(10)])
+        .run_planned()
+        .stage_provision_started(obs::StageIndex(0), obs::NodeId(10))
+        .stage_faulted(
+            obs::StageIndex(0),
+            obs::FaultReason::WorkerCrashed,
+            obs::Component::StageController,
+        )
+        .run_faulted(obs::FaultReason::WorkerCrashed, obs::Component::StageController)
+        .stop_run_sent(obs::StageIndex(0))
+        .stage_stopped(obs::StageIndex(0))
+        .run_torn_down()
+        .finish()
+}
+
+// This helper returns the position of an event kind in a trace. Ordering tests
+// use positions so they prove causal ordering without depending on exact event
+// batching or adjacent placement.
+fn position_of_kind(events: &[obs::Event], kind: obs::EventKind) -> usize {
+    events
+        .iter()
+        .position(|event| event.kind() == kind)
+        .expect("event kind missing from trace")
+}
+
+// This helper checks structured identity fields directly. If callers have to
+// scrape logs to recover an id, the event fails this contract test.
+fn assert_required_identity(event: &obs::Event) {
+    match event {
+        obs::Event::RunScoped { run_id, .. } => assert_eq!(*run_id, obs::RunId(7)),
+        obs::Event::NodeScoped { node_id, .. } => assert_eq!(*node_id, obs::NodeId(10)),
+        obs::Event::StageScoped {
+            run_id,
+            stage_index,
+            ..
+        } => {
+            assert_eq!(*run_id, obs::RunId(7));
+            assert_eq!(*stage_index, obs::StageIndex(0));
+        }
+        obs::Event::EdgeScoped { edge_id, .. } => {
+            assert!([obs::EdgeId(7000), obs::EdgeId(7001)].contains(edge_id));
+        }
+        obs::Event::RingScoped { ring_id, .. } => assert_eq!(*ring_id, obs::RingId(8000)),
+        obs::Event::ObjectScoped {
+            object_id,
+            sequence,
+            ..
+        } => {
+            assert!([obs::ObjectId(9000), obs::ObjectId(9001), obs::ObjectId(9002)].contains(object_id));
+            assert_eq!(*sequence, obs::Sequence(0));
+        }
+        obs::Event::StepScoped { step_id, .. } => assert_eq!(*step_id, obs::StepId(77)),
+        obs::Event::WorkerScoped {
+            worker_generation,
+            ..
+        } => assert_eq!(*worker_generation, obs::WorkerGeneration(1)),
+    }
+}
+
+// This proves required event identity fields are structured on the event itself
+// for run, node, stage, edge, ring, object, step, and worker scopes.
+#[test]
+fn required_event_identity_is_structured_not_log_derived() {
+    // Build one trace that includes all required identity scopes.
+    let mut events = successful_run_trace();
+    events.push(obs::Event::RingScoped {
+        kind: obs::EventKind::RingReadable,
+        ring_id: obs::RingId(8000),
+        component: obs::Component::SharedRingHelper,
+    });
+    events.push(obs::Event::WorkerScoped {
+        kind: obs::EventKind::WorkerReady,
+        worker_generation: obs::WorkerGeneration(1),
+        component: obs::Component::GpuWorkerCtl,
+    });
+
+    // Every event exposes its required identity directly.
+    for event in &events {
+        assert_required_identity(event);
+    }
+}
+
+// This proves the lifecycle event stream covers the required successful-run
+// milestones from node boot through run teardown.
+#[test]
+fn lifecycle_events_cover_successful_run_milestones() {
+    // Build the successful trace.
+    let events = successful_run_trace();
+    let observed = events
+        .iter()
+        .map(|event| event.kind())
+        .collect::<std::collections::BTreeSet<_>>();
+
+    // The required lifecycle event kinds must all be present, regardless of
+    // batching or transport.
+    let required = [
+        obs::EventKind::NodeStarted,
+        obs::EventKind::NodeAvailable,
+        obs::EventKind::PoolReady,
+        obs::EventKind::RunPlanned,
+        obs::EventKind::StageProvisionStarted,
+        obs::EventKind::WeightsDownloadStarted,
+        obs::EventKind::WeightsDownloaded,
+        obs::EventKind::WeightsLoaded,
+        obs::EventKind::EdgeProvisionStarted,
+        obs::EventKind::EdgeReady,
+        obs::EventKind::StageReady,
+        obs::EventKind::ReadinessBarrierPassed,
+        obs::EventKind::PromptInjected,
+        obs::EventKind::ObjectLoaded,
+        obs::EventKind::ExecuteStepStarted,
+        obs::EventKind::ObjectProduced,
+        obs::EventKind::StepCompleted,
+        obs::EventKind::TokenReceived,
+        obs::EventKind::RunCompleted,
+        obs::EventKind::StopRunSent,
+        obs::EventKind::StageStopped,
+        obs::EventKind::RunTornDown,
+    ];
+    for kind in required {
+        assert!(observed.contains(&kind), "missing lifecycle event: {kind:?}");
+    }
+}
+
+// This proves fault events carry a stable reason enum and detecting component,
+// and tests do not need free-form log text to determine lifecycle progress.
+#[test]
+fn fault_events_include_stable_reason_and_detecting_component() {
+    // Build a fault trace with a stage-detected worker crash.
+    let events = fault_trace();
+
+    // The structured stage fault carries the reason and detector.
+    assert!(events.iter().any(|event| {
+        matches!(
+            event,
+            obs::Event::StageScoped {
+                kind: obs::EventKind::StageFaulted,
+                reason: Some(obs::FaultReason::WorkerCrashed),
+                component: obs::Component::StageController,
+                ..
+            }
+        )
+    }));
+
+    // The run fault carries the same structured reason.
+    assert!(events.iter().any(|event| {
+        matches!(
+            event,
+            obs::Event::RunScoped {
+                kind: obs::EventKind::RunFaulted,
+                reason: Some(obs::FaultReason::WorkerCrashed),
+                component: obs::Component::StageController,
+                ..
+            }
+        )
+    }));
+
+    // Logs may exist, but they are not required to classify progress.
+    assert!(!obs::requires_log_scraping(&events));
+}
+
+// This proves observability ordering reflects component contracts:
+// prompt_injected follows readiness_barrier_passed, stage_ready follows local
+// readiness, run_torn_down follows teardown completion, and terminal run outcome
+// is emitted exactly once.
+#[test]
+fn event_ordering_reflects_component_contracts_and_one_terminal_outcome() {
+    // Build the successful trace.
+    let events = successful_run_trace();
+
+    // Prompt injection cannot precede the global barrier.
+    assert!(
+        position_of_kind(&events, obs::EventKind::ReadinessBarrierPassed)
+            < position_of_kind(&events, obs::EventKind::PromptInjected)
+    );
+
+    // StageReady cannot precede required local readiness facts.
+    assert!(
+        position_of_kind(&events, obs::EventKind::WeightsLoaded)
+            < position_of_kind(&events, obs::EventKind::StageReady)
+    );
+    assert!(
+        position_of_kind(&events, obs::EventKind::EdgeReady)
+            < position_of_kind(&events, obs::EventKind::StageReady)
+    );
+
+    // RunTornDown cannot precede teardown completion.
+    assert!(
+        position_of_kind(&events, obs::EventKind::StageStopped)
+            < position_of_kind(&events, obs::EventKind::RunTornDown)
+    );
+
+    // Exactly one terminal run outcome is emitted.
+    let terminal_count = events
+        .iter()
+        .filter(|event| {
+            matches!(event.kind(), obs::EventKind::RunCompleted | obs::EventKind::RunFaulted)
+        })
+        .count();
+    assert_eq!(terminal_count, 1);
+}
+
+// This proves observability tests are independent of transport, storage, and
+// batching policy by asserting the same event facts after batching is changed.
+#[test]
+fn event_contract_survives_transport_storage_and_batching_policy() {
+    // Build the same logical events under two batching policies.
+    let unbatched = obs::EventSubscriberHarness::collect(successful_run_trace(), obs::Batching::None);
+    let batched = obs::EventSubscriberHarness::collect(successful_run_trace(), obs::Batching::Fixed(8));
+
+    // Flattened public event facts must match as an ordered stream.
+    let unbatched_kinds = unbatched
+        .flattened_events()
+        .iter()
+        .map(|event| event.kind())
+        .collect::<Vec<_>>();
+    let batched_kinds = batched
+        .flattened_events()
+        .iter()
+        .map(|event| event.kind())
+        .collect::<Vec<_>>();
+    assert_eq!(batched_kinds, unbatched_kinds);
+
+    // Neither subscriber depends on transport or storage implementation names.
+    assert!(!unbatched.used_transport_specific_assertions());
+    assert!(!batched.used_storage_specific_assertions());
+}

tests/mvp_system/orchestrator_run_fsm_guarantees.rs

@@ -0,0 +1,413 @@
+//! Black-box contract tests for the MVP orchestrator run FSM.
+//!
+//! These tests intentionally know only the public orchestrator surface:
+//!
+//! - pool, plan, stage, endpoint, token, fault, stop, and timeout events in
+//! - commands, lifecycle events, and terminal outcome out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/orchestrator_run_fsm_contract.md`.
+
+use mvp_system::orchestrator_run_fsm as fsm;
+
+// A three-stage plan proves multi-stage provisioning and readiness without
+// making tests depend on any placement heuristic. The plan is already valid;
+// these tests are about how the orchestrator consumes it.
+fn committed_plan() -> fsm::RunPlan {
+    fsm::RunPlan::test_linear(
+        fsm::RunId(7),
+        vec![
+            fsm::StageRef {
+                stage_index: 0,
+                node_id: fsm::NodeId(10),
+            },
+            fsm::StageRef {
+                stage_index: 1,
+                node_id: fsm::NodeId(11),
+            },
+            fsm::StageRef {
+                stage_index: 2,
+                node_id: fsm::NodeId(12),
+            },
+        ],
+    )
+}
+
+// The harness is the black-box public boundary for the run FSM. It accepts
+// observable events and records emitted commands/events; tests never inspect an
+// internal FSM enum or private readiness counter.
+fn new_run() -> fsm::OrchestratorHarness {
+    fsm::OrchestratorHarness::new(fsm::RunConfig {
+        run_id: fsm::RunId(7),
+        max_tokens: 4,
+        prompt: vec![101, 102, 103],
+    })
+}
+
+// Stage readiness events are generated from the committed plan so the tests
+// prove readiness by stage identity instead of relying on command ordering.
+fn stage_ready_events(plan: &fsm::RunPlan) -> Vec<fsm::RunEvent> {
+    plan.stages
+        .iter()
+        .map(|stage| fsm::RunEvent::StageReady {
+            run_id: plan.run_id,
+            stage_index: stage.stage_index,
+        })
+        .collect()
+}
+
+// Transcript positions turn ordering claims into proofs over observable output.
+// If an event is missing, the test fails at the boundary where users and other
+// components would also lose the guarantee.
+fn position_of(events: &[fsm::LifecycleEvent], needle: &fsm::LifecycleEvent) -> usize {
+    events
+        .iter()
+        .position(|event| event == needle)
+        .expect("expected lifecycle event missing")
+}
+
+// This proves planning and provisioning are gated by PoolReady, and that the
+// orchestrator provisions exactly the committed stages and local token endpoints
+// from a valid RunPlan.
+#[test]
+fn planning_and_provisioning_start_only_after_pool_ready() {
+    // Start the run and give it a valid plan, but no PoolReady event.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+
+    // Without PoolReady, provisioning must not begin.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::ProvisionStage { .. })
+    }));
+
+    // Once PoolReady is observed, the committed plan may be provisioned.
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+
+    // Every planned stage gets exactly one provision command.
+    let provisioned = harness
+        .commands()
+        .iter()
+        .filter_map(|command| match command {
+            fsm::RunCommand::ProvisionStage { provision } => Some(provision.stage_index),
+            _ => None,
+        })
+        .collect::<std::collections::BTreeSet<_>>();
+    let expected = plan
+        .stages
+        .iter()
+        .map(|stage| stage.stage_index)
+        .collect::<std::collections::BTreeSet<_>>();
+    assert_eq!(provisioned, expected);
+
+    // Provisioning must not mention nodes outside the committed plan.
+    let plan_nodes = plan.stage_nodes().into_iter().collect::<std::collections::BTreeSet<_>>();
+    for command in harness.commands() {
+        if let fsm::RunCommand::ProvisionStage { provision } = command {
+            assert!(plan_nodes.contains(&provision.node_id));
+        }
+    }
+
+    // Token endpoints are created locally from the same committed plan.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::CreateTokenInEndpoint { run_id } if *run_id == fsm::RunId(7))
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::CreateTokenOutEndpoint { run_id } if *run_id == fsm::RunId(7))
+    }));
+}
+
+// This proves prompt injection is blocked until every planned stage and both
+// local token endpoints are ready. Duplicate readiness must not count as a
+// missing stage, and foreign readiness must fault or reject.
+#[test]
+fn readiness_barrier_controls_prompt_injection() {
+    // Provision a valid plan after PoolReady.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+
+    // A duplicate StageReady for stage 0 cannot satisfy stage 1 or 2.
+    harness.observe(fsm::RunEvent::StageReady {
+        run_id: fsm::RunId(7),
+        stage_index: 0,
+    });
+    harness.observe(fsm::RunEvent::StageReady {
+        run_id: fsm::RunId(7),
+        stage_index: 0,
+    });
+    harness.observe(fsm::RunEvent::TokenInEndpointReady);
+    harness.observe(fsm::RunEvent::TokenOutEndpointReady);
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::InjectPrompt { .. })
+    }));
+
+    // Complete the remaining stage readiness facts.
+    for event in stage_ready_events(&plan).into_iter().skip(1) {
+        harness.observe(event);
+    }
+
+    // Prompt injection is the public start signal after the full barrier.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            fsm::RunCommand::InjectPrompt {
+                run_id: fsm::RunId(7),
+                sequence: 0,
+                ..
+            }
+        )
+    }));
+
+    // Unknown stage readiness must not silently advance another run.
+    let mut invalid = new_run();
+    invalid.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    invalid.observe(fsm::RunEvent::PlanAvailable(plan));
+    invalid.observe(fsm::RunEvent::StageReady {
+        run_id: fsm::RunId(7),
+        stage_index: 99,
+    });
+    assert!(invalid.events().iter().any(|event| {
+        matches!(event, fsm::LifecycleEvent::RunFaulted { .. })
+            || matches!(event, fsm::LifecycleEvent::RunRejected { .. })
+    }));
+}
+
+// This proves execution has one start signal and advances by the token feedback
+// rule: inject sequence 0 first, then inject k + 1 only after consuming k.
+#[test]
+fn execution_injects_next_sequence_only_after_consuming_previous_token() {
+    // Drive a run through the complete readiness barrier.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+    harness.observe(fsm::RunEvent::TokenInEndpointReady);
+    harness.observe(fsm::RunEvent::TokenOutEndpointReady);
+    for event in stage_ready_events(&plan) {
+        harness.observe(event);
+    }
+
+    // No separate broadcast start command may exist alongside prompt injection.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::BroadcastStart { .. })
+    }));
+
+    // Sequence 0 must be injected first.
+    assert_eq!(harness.injected_sequences(), vec![0]);
+
+    // Consuming token 0 permits injecting sequence 1.
+    harness.observe(fsm::RunEvent::TokenReceived {
+        sequence: 0,
+        token_id: 201,
+        eos: false,
+    });
+    assert_eq!(harness.injected_sequences(), vec![0, 1]);
+
+    // No additional injection may happen without consuming sequence 1.
+    harness.advance_time_ms(10);
+    assert_eq!(harness.injected_sequences(), vec![0, 1]);
+
+    // EOS stops further injection after the consumed sequence.
+    harness.observe(fsm::RunEvent::TokenReceived {
+        sequence: 1,
+        token_id: 2,
+        eos: true,
+    });
+    assert_eq!(harness.injected_sequences(), vec![0, 1]);
+}
+
+// This proves every run-level fault source records one terminal fault, and the
+// first failure reason is retained if later failures arrive.
+#[test]
+fn first_run_fault_reason_is_terminal_and_sticky() {
+    // Prepare an executing run so both setup and execution-time faults would be
+    // meaningful if observed.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+    harness.observe(fsm::RunEvent::TokenInEndpointReady);
+    harness.observe(fsm::RunEvent::TokenOutEndpointReady);
+    for event in stage_ready_events(&plan) {
+        harness.observe(event);
+    }
+
+    // Inject the first failure source.
+    harness.observe(fsm::RunEvent::StageFault {
+        run_id: fsm::RunId(7),
+        stage_index: 1,
+        reason: fsm::StageFaultReason::WorkerCrashed,
+    });
+
+    // Inject later failures that must not replace the terminal reason.
+    harness.observe(fsm::RunEvent::EndpointFault {
+        run_id: fsm::RunId(7),
+        endpoint: fsm::EndpointKind::TokenOut,
+    });
+    harness.observe(fsm::RunEvent::Timeout {
+        run_id: fsm::RunId(7),
+        kind: fsm::TimeoutKind::Execution,
+    });
+
+    // Exactly one terminal fault is recorded.
+    let faults = harness
+        .events()
+        .iter()
+        .filter_map(|event| match event {
+            fsm::LifecycleEvent::RunFaulted { reason, .. } => Some(reason),
+            _ => None,
+        })
+        .collect::<Vec<_>>();
+    assert_eq!(faults.len(), 1);
+    assert_eq!(
+        *faults[0],
+        fsm::RunFaultReason::StageFault {
+            stage_index: 1,
+            reason: fsm::StageFaultReason::WorkerCrashed,
+        }
+    );
+}
+
+// This proves terminal outcomes are mutually exclusive, reject new work, and
+// always lead into teardown for success, fault, and operator stop.
+#[test]
+fn terminal_outcome_is_single_and_requires_teardown() {
+    // Complete a run by reaching EOS.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+    harness.observe(fsm::RunEvent::TokenInEndpointReady);
+    harness.observe(fsm::RunEvent::TokenOutEndpointReady);
+    for event in stage_ready_events(&plan) {
+        harness.observe(event);
+    }
+    harness.observe(fsm::RunEvent::TokenReceived {
+        sequence: 0,
+        token_id: 2,
+        eos: true,
+    });
+
+    // Completed and Faulted are mutually exclusive public outcomes.
+    let completed = harness
+        .events()
+        .iter()
+        .filter(|event| matches!(event, fsm::LifecycleEvent::RunCompleted { .. }))
+        .count();
+    let faulted = harness
+        .events()
+        .iter()
+        .filter(|event| matches!(event, fsm::LifecycleEvent::RunFaulted { .. }))
+        .count();
+    assert_eq!(completed, 1);
+    assert_eq!(faulted, 0);
+
+    // New token work after terminal outcome begins must be rejected.
+    let before = harness.injected_sequences();
+    harness.observe(fsm::RunEvent::TokenReceived {
+        sequence: 99,
+        token_id: 333,
+        eos: false,
+    });
+    assert_eq!(harness.injected_sequences(), before);
+
+    // Teardown commands must be emitted for every provisioned stage and local
+    // endpoint after the terminal outcome.
+    let stopped_stages = harness
+        .commands()
+        .iter()
+        .filter_map(|command| match command {
+            fsm::RunCommand::StopRun { stage_index, .. } => Some(*stage_index),
+            _ => None,
+        })
+        .collect::<std::collections::BTreeSet<_>>();
+    let expected_stages = plan
+        .stages
+        .iter()
+        .map(|stage| stage.stage_index)
+        .collect::<std::collections::BTreeSet<_>>();
+    assert_eq!(stopped_stages, expected_stages);
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, fsm::RunCommand::TearDownTokenEndpoints { .. })
+    }));
+}
+
+// This proves run_torn_down is emitted exactly once and only after teardown
+// reaches a terminal state by stage stops or timeout.
+#[test]
+fn run_torn_down_is_emitted_once_after_teardown_terminal_state() {
+    // Fault a provisioned run so teardown is required.
+    let plan = committed_plan();
+    let mut harness = new_run();
+    harness.observe(fsm::RunEvent::PoolReady {
+        nodes: plan.stage_nodes(),
+    });
+    harness.observe(fsm::RunEvent::PlanAvailable(plan.clone()));
+    harness.observe(fsm::RunEvent::StageFault {
+        run_id: fsm::RunId(7),
+        stage_index: 0,
+        reason: fsm::StageFaultReason::WorkerCrashed,
+    });
+
+    // StageStopped from only a prefix of stages is not enough to finish
+    // teardown.
+    harness.observe(fsm::RunEvent::StageStopped {
+        run_id: fsm::RunId(7),
+        stage_index: 0,
+    });
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, fsm::LifecycleEvent::RunTornDown { .. })
+    }));
+
+    // Finish teardown through remaining stopped events and local endpoint stop.
+    harness.observe(fsm::RunEvent::StageStopped {
+        run_id: fsm::RunId(7),
+        stage_index: 1,
+    });
+    harness.observe(fsm::RunEvent::StageStopped {
+        run_id: fsm::RunId(7),
+        stage_index: 2,
+    });
+    harness.observe(fsm::RunEvent::TokenEndpointsStopped);
+
+    // The final event may now appear, exactly once.
+    let torn_down_count = harness
+        .events()
+        .iter()
+        .filter(|event| matches!(event, fsm::LifecycleEvent::RunTornDown { .. }))
+        .count();
+    assert_eq!(torn_down_count, 1);
+
+    // Ordering is proven over the lifecycle transcript.
+    let fault_pos = position_of(
+        harness.events(),
+        &fsm::LifecycleEvent::RunFaulted {
+            run_id: fsm::RunId(7),
+            reason: fsm::RunFaultReason::StageFault {
+                stage_index: 0,
+                reason: fsm::StageFaultReason::WorkerCrashed,
+            },
+        },
+    );
+    let torn_down_pos = position_of(
+        harness.events(),
+        &fsm::LifecycleEvent::RunTornDown {
+            run_id: fsm::RunId(7),
+        },
+    );
+    assert!(fault_pos < torn_down_pos);
+}

tests/mvp_system/orchestrator_token_endpoint_guarantees.rs

@@ -0,0 +1,248 @@
+//! Black-box contract tests for MVP orchestrator token endpoints.
+//!
+//! These tests intentionally know only the public token-endpoint surface:
+//!
+//! - committed token edges and endpoint formation in
+//! - readiness, prompt, token, and fault events in
+//! - token writes, lifecycle events, and run faults out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/orchestrator_token_endpoint_contract.md`.
+
+use mvp_system::orchestrator_token_endpoint as token;
+
+// The endpoint plan names the orchestrator and both token edges. Tests use the
+// committed plan as input and do not assume how endpoints allocate local rings
+// or actors.
+fn token_plan() -> token::TokenEndpointPlan {
+    token::TokenEndpointPlan {
+        run_id: token::RunId(7),
+        orchestrator_node_id: token::NodeId(99),
+        token_in_edge: token::EdgePlan::token_in(token::EdgeId(7000), token::NodeId(99), token::NodeId(10)),
+        token_out_edge: token::EdgePlan::token_out(token::EdgeId(7003), token::NodeId(12), token::NodeId(99)),
+        token_spec: token::ObjectSpec::test_tokens(),
+        max_tokens: 4,
+    }
+}
+
+// The harness exposes only endpoint-visible inputs and outputs. It does not
+// reveal pump tasks, local actor addresses, or ring internals.
+fn new_endpoint_harness() -> token::TokenEndpointHarness {
+    token::TokenEndpointHarness::new(token_plan())
+}
+
+// This helper drives the global readiness barrier as the orchestrator would see
+// it. Prompt-injection tests use it to prove the endpoint does not start early.
+fn pass_global_barrier(harness: &mut token::TokenEndpointHarness) {
+    harness.observe(token::EndpointEvent::TokenInReady {
+        edge_id: token::EdgeId(7000),
+    });
+    harness.observe(token::EndpointEvent::TokenOutReady {
+        edge_id: token::EdgeId(7003),
+    });
+    harness.observe(token::EndpointEvent::AllStagesReady);
+    harness.observe(token::EndpointEvent::ReadinessBarrierPassed);
+}
+
+// This proves endpoint formation is derived from the committed plan, uses the
+// same edge semantics as stage endpoints, and keeps a stable orchestrator node
+// identity even when co-located with GPU nodes.
+#[test]
+fn token_endpoints_are_created_from_committed_plan_with_stable_node_id() {
+    // Create endpoints from the committed token plan.
+    let harness = new_endpoint_harness();
+
+    // Token-in and token-out endpoint creation must reference the plan edges.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            token::EndpointCommand::CreateTokenInProducer {
+                edge_id: token::EdgeId(7000),
+                orchestrator_node_id: token::NodeId(99),
+                ..
+            }
+        )
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            token::EndpointCommand::CreateTokenOutConsumer {
+                edge_id: token::EdgeId(7003),
+                orchestrator_node_id: token::NodeId(99),
+                ..
+            }
+        )
+    }));
+
+    // Co-location must not change the edge shape or remove the orchestrator
+    // endpoint identity.
+    for endpoint in harness.local_endpoints() {
+        assert_eq!(endpoint.orchestrator_node_id, token::NodeId(99));
+        assert!(matches!(
+            endpoint.edge_semantics,
+            token::EdgeSemantics::SingleProducerSingleConsumer
+        ));
+    }
+}
+
+// This proves prompt injection waits for the global readiness barrier, writes
+// token object sequence 0, conforms to the token ObjectSpec, and is the only
+// start signal.
+#[test]
+fn prompt_injection_is_barrier_gated_sequence_zero_token_object() {
+    // Build endpoints but do not pass readiness.
+    let mut harness = new_endpoint_harness();
+    harness.request_prompt_injection(vec![101, 102, 103]);
+
+    // No prompt object may be written before the barrier.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, token::EndpointCommand::WriteTokenObject { .. })
+    }));
+
+    // Passing the global barrier permits the first prompt write.
+    pass_global_barrier(&mut harness);
+
+    // The first token-in object must be sequence 0 and match the token spec.
+    let writes = harness
+        .commands()
+        .iter()
+        .filter_map(|command| match command {
+            token::EndpointCommand::WriteTokenObject(write) => Some(write),
+            _ => None,
+        })
+        .collect::<Vec<_>>();
+    assert_eq!(writes.len(), 1);
+    assert_eq!(writes[0].sequence, 0);
+    assert_eq!(writes[0].object_spec, token::ObjectSpec::test_tokens());
+
+    // Prompt injection is the start signal; there must not be a separate
+    // broadcast start command.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, token::EndpointCommand::BroadcastStart { .. })
+    }));
+}
+
+// This proves token-out is consumed in sequence order and sequence k + 1 is
+// injected only after the orchestrator consumes token sequence k.
+#[test]
+fn token_feedback_controls_next_injection() {
+    // Start with prompt sequence 0 injected.
+    let mut harness = new_endpoint_harness();
+    harness.request_prompt_injection(vec![101, 102, 103]);
+    pass_global_barrier(&mut harness);
+    assert_eq!(harness.injected_sequences(), vec![0]);
+
+    // Consuming token sequence 0 authorizes sequence 1.
+    harness.observe(token::EndpointEvent::TokenObjectReceived {
+        edge_id: token::EdgeId(7003),
+        object_id: token::ObjectId(9000),
+        sequence: 0,
+        token_id: 201,
+        eos: false,
+    });
+    assert_eq!(harness.injected_sequences(), vec![0, 1]);
+
+    // Time and readiness events alone do not authorize another decode step.
+    harness.advance_time_ms(100);
+    assert_eq!(harness.injected_sequences(), vec![0, 1]);
+
+    // An out-of-order token faults the run rather than skipping ahead.
+    harness.observe(token::EndpointEvent::TokenObjectReceived {
+        edge_id: token::EdgeId(7003),
+        object_id: token::ObjectId(9002),
+        sequence: 3,
+        token_id: 203,
+        eos: false,
+    });
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            token::EndpointLifecycleEvent::RunFaulted {
+                reason: token::RunFaultReason::TokenSequenceViolation,
+                ..
+            }
+        )
+    }));
+}
+
+// This proves EOS and max_tokens both stop further token-in injection.
+#[test]
+fn eos_and_max_tokens_stop_injection() {
+    // EOS stops immediately after the consumed token.
+    let mut eos_harness = new_endpoint_harness();
+    eos_harness.request_prompt_injection(vec![101]);
+    pass_global_barrier(&mut eos_harness);
+    eos_harness.observe(token::EndpointEvent::TokenObjectReceived {
+        edge_id: token::EdgeId(7003),
+        object_id: token::ObjectId(9000),
+        sequence: 0,
+        token_id: 2,
+        eos: true,
+    });
+    assert_eq!(eos_harness.injected_sequences(), vec![0]);
+
+    // max_tokens stops after the configured number of injections.
+    let mut max_harness = new_endpoint_harness();
+    max_harness.request_prompt_injection(vec![101]);
+    pass_global_barrier(&mut max_harness);
+    for sequence in 0..4 {
+        max_harness.observe(token::EndpointEvent::TokenObjectReceived {
+            edge_id: token::EdgeId(7003),
+            object_id: token::ObjectId(9000 + sequence),
+            sequence,
+            token_id: 300 + sequence as u32,
+            eos: false,
+        });
+    }
+    assert_eq!(max_harness.injected_sequences(), vec![0, 1, 2, 3]);
+}
+
+// This proves token endpoint, malformed object, and sequence faults are
+// surfaced as run faults, while teardown failure contributes to teardown
+// failure rather than being lost in logs.
+#[test]
+fn token_endpoint_failures_fault_the_run_or_teardown() {
+    // Endpoint fault during active run faults the run.
+    let mut harness = new_endpoint_harness();
+    harness.request_prompt_injection(vec![101]);
+    pass_global_barrier(&mut harness);
+    harness.observe(token::EndpointEvent::EndpointFault {
+        edge_id: token::EdgeId(7000),
+        direction: token::EndpointDirection::TokenIn,
+    });
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            token::EndpointLifecycleEvent::RunFaulted {
+                reason: token::RunFaultReason::TokenEndpointFault,
+                ..
+            }
+        )
+    }));
+
+    // Malformed token objects fault the run at the token boundary.
+    let mut malformed = new_endpoint_harness();
+    malformed.request_prompt_injection(vec![101]);
+    pass_global_barrier(&mut malformed);
+    malformed.observe(token::EndpointEvent::MalformedTokenObject {
+        edge_id: token::EdgeId(7003),
+        object_id: token::ObjectId(9999),
+    });
+    assert!(malformed.events().iter().any(|event| {
+        matches!(
+            event,
+            token::EndpointLifecycleEvent::RunFaulted {
+                reason: token::RunFaultReason::MalformedTokenObject,
+                ..
+            }
+        )
+    }));
+
+    // Teardown failure must be visible as teardown failure.
+    malformed.observe(token::EndpointEvent::TeardownFailed {
+        edge_id: token::EdgeId(7003),
+    });
+    assert!(malformed.events().iter().any(|event| {
+        matches!(event, token::EndpointLifecycleEvent::TeardownFailed { .. })
+    }));
+}

tests/mvp_system/resource_inventory_guarantees.rs

@@ -0,0 +1,246 @@
+//! Black-box contract tests for MVP resource inventory.
+//!
+//! These tests intentionally know only the public inventory/planner input
+//! surface:
+//!
+//! - orchestrator-owned inventory entries
+//! - candidate pool and placement input derived from that inventory
+//! - planner acceptance or typed rejection
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/resource_inventory_contract.md`.
+
+use mvp_system::resource_inventory as inventory;
+
+// The inventory fixture has more nodes than the placement needs. That proves
+// the planner may choose among known inventory entries but may not invent hidden
+// nodes or accept nodes that the orchestrator did not provide.
+fn inventory_entries() -> Vec<inventory::InventoryEntry> {
+    vec![
+        inventory::InventoryEntry::ready(inventory::NodeId(10), inventory::GpuClass::TestSmall),
+        inventory::InventoryEntry::ready(inventory::NodeId(11), inventory::GpuClass::TestSmall),
+        inventory::InventoryEntry::ready(inventory::NodeId(12), inventory::GpuClass::TestSmall),
+        inventory::InventoryEntry::ready(inventory::NodeId(13), inventory::GpuClass::TestSmall),
+    ]
+}
+
+// The fixed placement input names stage ownership without giving the planner
+// permission to derive any other topology. The plan still owns the resulting
+// stage records.
+fn fixed_placement() -> inventory::PlacementInput {
+    inventory::PlacementInput::FixedLinear(vec![
+        inventory::StagePlacement {
+            stage_index: 0,
+            node_id: inventory::NodeId(10),
+        },
+        inventory::StagePlacement {
+            stage_index: 1,
+            node_id: inventory::NodeId(11),
+        },
+        inventory::StagePlacement {
+            stage_index: 2,
+            node_id: inventory::NodeId(12),
+        },
+    ])
+}
+
+// This helper builds the public planning request from inventory facts. Tests
+// mutate only the fact under examination so a rejection can be attributed to a
+// specific inventory contract violation.
+fn planning_request() -> inventory::PlanningRequest {
+    inventory::PlanningRequest {
+        run_id: inventory::RunId(7),
+        stage_count: 3,
+        entries: inventory_entries(),
+        placement: fixed_placement(),
+    }
+}
+
+// Node reports after boot are inventory inputs, not placement negotiations.
+// This helper gives tests one post-boot report they can send and then prove did
+// not rewrite the committed planning input.
+fn post_boot_health_report(node_id: inventory::NodeId) -> inventory::NodeReport {
+    inventory::NodeReport::BootHealth {
+        node_id,
+        health: inventory::BootHealth::Ready,
+    }
+}
+
+// This proves inventory formation is orchestrator-owned and available before
+// planning: every entry is tied to a known node id, and node reports do not
+// negotiate placement after boot.
+#[test]
+fn inventory_entries_are_known_before_planning_and_not_negotiated_by_nodes() {
+    // Create the orchestrator-owned inventory and snapshot the public entries.
+    let mut harness = inventory::InventoryHarness::new(inventory_entries());
+    let before_report = harness.entries().to_vec();
+
+    // Let a node report boot health after the inventory already exists.
+    harness.observe_node_report(post_boot_health_report(inventory::NodeId(10)));
+
+    // Boot health may update readiness metadata, but it must not rewrite the
+    // node set or add placement facts.
+    let after_report = harness.entries().to_vec();
+    let before_nodes = before_report
+        .iter()
+        .map(|entry| entry.node_id)
+        .collect::<std::collections::BTreeSet<_>>();
+    let after_nodes = after_report
+        .iter()
+        .map(|entry| entry.node_id)
+        .collect::<std::collections::BTreeSet<_>>();
+    assert_eq!(after_nodes, before_nodes);
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, inventory::InventoryCommand::AcceptPlacementNegotiation { .. })
+    }));
+}
+
+// This proves the planner may place stages only onto nodes present in the
+// orchestrator-owned inventory, and the emitted RunPlan is the sole placement
+// result.
+#[test]
+fn planned_stage_nodes_are_subset_of_inventory_nodes() {
+    // Build a valid public planning request from inventory entries.
+    let request = planning_request();
+    let inventory_nodes = request
+        .entries
+        .iter()
+        .map(|entry| entry.node_id)
+        .collect::<std::collections::BTreeSet<_>>();
+
+    // Plan through the public inventory/planner boundary.
+    let plan = inventory::plan_from_inventory(request).expect("valid inventory must plan");
+
+    // Prove every planned stage node came from the inventory snapshot.
+    for stage in &plan.stages {
+        assert!(
+            inventory_nodes.contains(&stage.node_id),
+            "stage used node outside inventory: {:?}",
+            stage.node_id
+        );
+    }
+}
+
+// This proves unknown nodes, duplicate stage assignments, and missing stage
+// assignments reject as typed planning-input errors.
+#[test]
+fn invalid_inventory_placement_rejects_with_typed_errors() {
+    // Each case corrupts one public placement fact.
+    let cases = vec![
+        (
+            inventory::PlacementInput::FixedLinear(vec![
+                inventory::StagePlacement {
+                    stage_index: 0,
+                    node_id: inventory::NodeId(10),
+                },
+                inventory::StagePlacement {
+                    stage_index: 1,
+                    node_id: inventory::NodeId(99),
+                },
+                inventory::StagePlacement {
+                    stage_index: 2,
+                    node_id: inventory::NodeId(12),
+                },
+            ]),
+            inventory::InventoryRejectionKind::UnknownNode {
+                node_id: inventory::NodeId(99),
+            },
+        ),
+        (
+            inventory::PlacementInput::FixedLinear(vec![
+                inventory::StagePlacement {
+                    stage_index: 0,
+                    node_id: inventory::NodeId(10),
+                },
+                inventory::StagePlacement {
+                    stage_index: 0,
+                    node_id: inventory::NodeId(11),
+                },
+                inventory::StagePlacement {
+                    stage_index: 2,
+                    node_id: inventory::NodeId(12),
+                },
+            ]),
+            inventory::InventoryRejectionKind::DuplicateStage { stage_index: 0 },
+        ),
+        (
+            inventory::PlacementInput::FixedLinear(vec![
+                inventory::StagePlacement {
+                    stage_index: 0,
+                    node_id: inventory::NodeId(10),
+                },
+                inventory::StagePlacement {
+                    stage_index: 2,
+                    node_id: inventory::NodeId(12),
+                },
+            ]),
+            inventory::InventoryRejectionKind::MissingStage { stage_index: 1 },
+        ),
+    ];
+
+    for (placement, expected_kind) in cases {
+        // Replace only the placement fact in an otherwise valid request.
+        let mut request = planning_request();
+        request.placement = placement;
+
+        // The rejection must be typed and no RunPlan may be emitted.
+        let rejection = inventory::plan_from_inventory(request)
+            .expect_err("invalid inventory placement must reject");
+        assert_eq!(rejection.kind, expected_kind);
+    }
+}
+
+// This proves planning does not mutate the candidate pool and does not derive
+// hidden nodes outside the inventory.
+#[test]
+fn planning_preserves_candidate_pool_and_emits_no_hidden_nodes() {
+    // Snapshot the public inventory before planning.
+    let request = planning_request();
+    let original_entries = request.entries.clone();
+    let original_nodes = original_entries
+        .iter()
+        .map(|entry| entry.node_id)
+        .collect::<std::collections::BTreeSet<_>>();
+
+    // Plan using a cloned request so the caller-owned facts remain inspectable.
+    let plan = inventory::plan_from_inventory(request.clone()).expect("valid inventory must plan");
+
+    // The caller's candidate facts must be unchanged.
+    assert_eq!(request.entries, original_entries);
+
+    // Every node mentioned by the plan must be explainable by the original
+    // inventory snapshot.
+    let planned_nodes = plan
+        .stages
+        .iter()
+        .map(|stage| stage.node_id)
+        .collect::<std::collections::BTreeSet<_>>();
+    assert!(planned_nodes.is_subset(&original_nodes));
+}
+
+// This proves inventory authority ends at planner input. After provisioning,
+// stages consume their RunPlan-derived assignment and do not reinterpret
+// inventory reports.
+#[test]
+fn provisioned_stages_do_not_reinterpret_inventory() {
+    // Commit a plan and provision its stages.
+    let plan = inventory::plan_from_inventory(planning_request()).expect("valid inventory must plan");
+    let mut harness = inventory::InventoryHarness::new(inventory_entries());
+    harness.commit_plan(plan.clone());
+    harness.provision_stages();
+
+    // Send a later inventory report that would be dangerous if treated as a
+    // graph rewrite.
+    harness.observe_node_report(inventory::NodeReport::CapacityChanged {
+        node_id: inventory::NodeId(11),
+        gpu_class: inventory::GpuClass::TestLarge,
+    });
+
+    // No provisioned stage may be asked to reinterpret its assignment.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, inventory::InventoryCommand::RewriteStagePlacement { .. })
+    }));
+
+    // The committed plan remains the only graph-visible placement fact.
+    assert_eq!(harness.committed_plan(), Some(&plan));
+}

tests/mvp_system/run_plan_guarantees.rs

@@ -0,0 +1,691 @@
+//! Black-box contract tests for MVP RunPlan formation.
+//!
+//! These tests intentionally know only the public planning surface:
+//!
+//! - `plan_run(input) -> Result<RunPlan, PlanRejection>`
+//! - `derive_stage_provision(&plan, stage_index) -> Result<ProvisionStage, ProjectionRejection>`
+//!
+//! They assert the guarantees in `specs/mvp_system/run_plan_contract.md`.
+//! The planner implementation, placement heuristic, helper APIs, internal graph
+//! representation, and allocation strategy are not observable here.
+
+use mvp_system::run_plan as plan;
+
+// Local aliases keep the test prose readable while the file imports only the
+// public planning module. The aliases do not grant access to planner internals.
+type DTypeFamily = plan::DTypeFamily;
+type EdgeEndpoint = plan::EdgeEndpoint;
+type EdgeId = plan::EdgeId;
+type EdgeKind = plan::EdgeKind;
+type EdgePlan = plan::EdgePlan;
+type InboundEdgeProvision = plan::InboundEdgeProvision;
+type ModelFacts = plan::ModelFacts;
+type NodeId = plan::NodeId;
+type ObjectKind = plan::ObjectKind;
+type OutboundEdgeProvision = plan::OutboundEdgeProvision;
+type PlacementInput = plan::PlacementInput;
+type PlanRejectionKind = plan::PlanRejectionKind;
+type PlannerInput = plan::PlannerInput;
+type RingSpec = plan::RingSpec;
+type RunPlan = plan::RunPlan;
+type RuntimeConfig = plan::RuntimeConfig;
+type StagePlacement = plan::StagePlacement;
+
+// Keep test node ids small and readable. The concrete identity mechanism is
+// outside this contract; these ids exist only so assertions can name topology
+// facts without depending on any address or discovery machinery.
+fn node(id: u64) -> NodeId {
+    NodeId(id)
+}
+
+// The candidate pool is deliberately larger than some test placements. That
+// lets the tests distinguish "known to the orchestrator" from "assigned to a
+// stage", which is one of the planner authority boundaries.
+fn valid_nodes() -> Vec<NodeId> {
+    vec![node(10), node(11), node(12), node(13)]
+}
+
+// Fixed linear placement is the smallest placement input that still exercises
+// the contract. It supplies stage-to-node intent, while the planner remains
+// responsible for validating it and minting the full RunPlan topology.
+fn linear_placement(stage_count: u32) -> PlacementInput {
+    PlacementInput::FixedLinear(
+        (0..stage_count)
+            .map(|stage_index| StagePlacement {
+                stage_index,
+                node_id: node(10 + u64::from(stage_index)),
+            })
+            .collect(),
+    )
+}
+
+// This is the canonical valid fixture for RunPlan guarantees. Each test tweaks
+// only the fact it is trying to prove, so a failure points at the violated
+// contract instead of at accidental fixture drift.
+fn valid_input(stage_count: u32, num_layers: u32) -> PlannerInput {
+    PlannerInput {
+        run_id: 7.into(),
+        orchestrator_node_id: node(99),
+        model: ModelFacts {
+            model_id: "test-gguf".into(),
+            num_layers,
+            hidden_dim: 4096,
+            dtype_family: DTypeFamily::BFloat,
+            dtype_width_bytes: 2,
+            max_seq_len: 2048,
+            eos_token_id: 2,
+        },
+        runtime: RuntimeConfig::test_default(),
+        candidate_pool: valid_nodes(),
+        stage_count,
+        placement: linear_placement(stage_count),
+        activation_ring: RingSpec::test_default_activation(),
+        token_ring: RingSpec::test_default_token(),
+    }
+}
+
+// Tests frequently need to compare a provisioned edge id back to the canonical
+// edge record in the RunPlan. This helper makes that lookup explicit without
+// giving tests access to any planner-private index.
+fn plan_edges_by_id(plan: &RunPlan) -> std::collections::BTreeMap<EdgeId, &EdgePlan> {
+    plan.edges
+        .iter()
+        .map(|edge| (edge.edge_id, edge))
+        .collect::<std::collections::BTreeMap<_, _>>()
+}
+
+// Edge endpoints can be orchestrator or stage endpoints. Tests use this helper
+// when they care only about stage adjacency and want orchestrator endpoints to
+// remain visibly outside the stage index space.
+fn edge_stage_index(endpoint: &EdgeEndpoint) -> Option<u32> {
+    match endpoint {
+        EdgeEndpoint::Orchestrator { .. } => None,
+        EdgeEndpoint::Stage { stage_index, .. } => Some(*stage_index),
+    }
+}
+
+// Provisioning sends concrete node ids across the data-flow boundary. This
+// helper extracts the observable node id from either endpoint shape so tests
+// can compare projection output to plan topology.
+fn edge_node_id(endpoint: &EdgeEndpoint) -> NodeId {
+    match endpoint {
+        EdgeEndpoint::Orchestrator { node_id } => *node_id,
+        EdgeEndpoint::Stage { node_id, .. } => *node_id,
+    }
+}
+
+// This proves RunPlan formation is a total public boundary for valid input:
+// the caller observes one complete plan, not hidden follow-up topology work or
+// a partially initialized result.
+#[test]
+fn valid_input_emits_one_complete_plan() {
+    // Build one ordinary valid planning request.
+    let input = valid_input(3, 36);
+
+    // Planning valid input must produce a usable plan, not a deferred partial.
+    let plan = plan::plan_run(input).expect("valid input must emit a plan");
+
+    // The plan-level identifiers and counts must be complete immediately.
+    assert_eq!(plan.run_id, 7.into());
+    assert_eq!(plan.stages.len(), 3);
+    assert_eq!(plan.edges.len(), 4);
+
+    // Every stage must be bound to this run and know the run's stage count.
+    for stage in &plan.stages {
+        assert_eq!(stage.run_id, plan.run_id);
+        assert_eq!(stage.stage_count, 3);
+    }
+
+    // Every edge must also be bound to this run; no edge can be a loose fact.
+    for edge in &plan.edges {
+        assert_eq!(edge.run_id, plan.run_id);
+    }
+}
+
+// This proves planning does not mutate the candidate pool supplied by the
+// caller. The only topology facts the caller can use after planning are the
+// facts emitted in the RunPlan itself.
+#[test]
+fn planner_does_not_mutate_candidate_pool() {
+    // Keep a copy of the caller-owned pool before the planner sees it.
+    let input = valid_input(3, 36);
+    let original_pool = input.candidate_pool.clone();
+
+    // Run planning through the public API only.
+    let _ = plan::plan_run(input.clone()).expect("valid input must emit a plan");
+
+    // The input pool remains the caller's fact; topology facts must be in the
+    // returned plan, not back-written into the input.
+    assert_eq!(input.candidate_pool, original_pool);
+}
+
+// This proves layer assignment is a contiguous, non-overlapping partition of
+// the intended GGUF block range, with one non-empty range per stage.
+#[test]
+fn stage_ranges_partition_the_model_layers() {
+    // Exercise several deterministic sizes so the check covers one-stage and
+    // multi-stage partitioning without relying on random generation.
+    for (stage_count, num_layers) in [(1, 12), (2, 24), (3, 36), (4, 40)] {
+        // Produce the plan from public inputs.
+        let plan = plan::plan_run(valid_input(stage_count, num_layers)).unwrap();
+
+        // Read only the public stage assignments and sort by stage index.
+        let mut ranges = plan
+            .stages
+            .iter()
+            .map(|stage| {
+                (
+                    stage.stage_index,
+                    stage.layer_start,
+                    stage.layer_end_exclusive,
+                )
+            })
+            .collect::<Vec<_>>();
+        ranges.sort_by_key(|(stage_index, _, _)| *stage_index);
+
+        // Walk the sorted ranges as a proof of contiguity. The next start must
+        // equal the previous end, and every range must consume at least one
+        // layer inside the model range.
+        let mut expected_start = 0;
+        for (_, start, end) in ranges {
+            assert_eq!(start, expected_start, "range gap or overlap");
+            assert!(end > start, "stage range must be non-empty");
+            assert!(end <= num_layers, "stage range exceeds model layer range");
+            expected_start = end;
+        }
+
+        // The final end must cover the whole intended block range.
+        assert_eq!(expected_start, num_layers);
+    }
+}
+
+// This proves stage indices are exactly the dense range required by the
+// contract. Missing, duplicate, or out-of-range stage indices are observable in
+// the returned RunPlan and fail this check.
+#[test]
+fn stage_indices_are_exactly_zero_to_stage_count_minus_one() {
+    // Check several stage counts so the dense-index guarantee is not tied to
+    // the canonical three-stage fixture.
+    for stage_count in 1..=4 {
+        // Produce a valid plan and observe only its public stage indices.
+        let plan = plan::plan_run(valid_input(stage_count, stage_count * 8)).unwrap();
+        let observed = plan
+            .stages
+            .iter()
+            .map(|stage| stage.stage_index)
+            .collect::<std::collections::BTreeSet<_>>();
+
+        // Compare against the contract's exact dense index set.
+        let expected = (0..stage_count).collect::<std::collections::BTreeSet<_>>();
+
+        assert_eq!(observed, expected);
+    }
+}
+
+// This proves every edge has one public producer and one public consumer, and
+// that the returned edge graph is exactly the MVP linear pipeline.
+#[test]
+fn edge_graph_is_exactly_the_linear_pipeline() {
+    // Use four stages so the activation chain has multiple interior edges.
+    let stage_count = 4;
+    let plan = plan::plan_run(valid_input(stage_count, 40)).unwrap();
+
+    // Token-in must be unique and must enter stage 0 from the orchestrator.
+    let token_in = plan
+        .edges
+        .iter()
+        .filter(|edge| edge.kind == EdgeKind::TokenIn)
+        .collect::<Vec<_>>();
+    assert_eq!(token_in.len(), 1);
+    assert!(matches!(
+        token_in[0].producer,
+        EdgeEndpoint::Orchestrator { node_id } if node_id == node(99)
+    ));
+    assert_eq!(
+        token_in[0].consumer,
+        EdgeEndpoint::Stage {
+            node_id: node(10),
+            stage_index: 0,
+        }
+    );
+
+    // Activation edges must be the only stage-to-stage edges, one per adjacent
+    // stage pair.
+    let activation_edges = plan
+        .edges
+        .iter()
+        .filter(|edge| edge.kind == EdgeKind::Activation)
+        .collect::<Vec<_>>();
+    assert_eq!(activation_edges.len(), (stage_count - 1) as usize);
+
+    // Each activation edge produced by stage i must be consumed by stage i+1.
+    for stage_index in 0..stage_count - 1 {
+        let edge = activation_edges
+            .iter()
+            .find(|edge| edge_stage_index(&edge.producer) == Some(stage_index))
+            .expect("activation edge produced by stage");
+
+        assert_eq!(
+            edge.consumer,
+            EdgeEndpoint::Stage {
+                node_id: node(11 + u64::from(stage_index)),
+                stage_index: stage_index + 1,
+            }
+        );
+        assert_ne!(edge.producer, edge.consumer, "self-edge is forbidden");
+    }
+
+    // Token-out must be unique and must leave the final stage for the
+    // orchestrator.
+    let token_out = plan
+        .edges
+        .iter()
+        .filter(|edge| edge.kind == EdgeKind::TokenOut)
+        .collect::<Vec<_>>();
+    assert_eq!(token_out.len(), 1);
+    assert_eq!(edge_stage_index(&token_out[0].producer), Some(stage_count - 1));
+    assert!(matches!(
+        token_out[0].consumer,
+        EdgeEndpoint::Orchestrator { node_id } if node_id == node(99)
+    ));
+}
+
+// This proves edge ids are run-unique and that stage plans refer only to edge
+// ids present in the returned RunPlan, so stages receive assigned ids rather
+// than deriving data-flow identity themselves.
+#[test]
+fn edge_ids_are_unique_and_stage_references_resolve_to_plan_edges() {
+    // Produce a plan with enough edges to make duplicate ids observable.
+    let plan = plan::plan_run(valid_input(4, 40)).unwrap();
+
+    // Insert every public edge id into a set; a duplicate shrinks the set.
+    let edge_ids = plan
+        .edges
+        .iter()
+        .map(|edge| edge.edge_id)
+        .collect::<std::collections::BTreeSet<_>>();
+
+    assert_eq!(edge_ids.len(), plan.edges.len(), "duplicate edge id");
+
+    // Stage plans may reference only ids that the RunPlan itself assigned.
+    for stage in &plan.stages {
+        assert!(
+            edge_ids.contains(&stage.inbound_edge),
+            "stage inbound edge id must come from RunPlan edges"
+        );
+        assert!(
+            edge_ids.contains(&stage.outbound_edge),
+            "stage outbound edge id must come from RunPlan edges"
+        );
+    }
+}
+
+// This proves deriving ProvisionStage is deterministic and stage-local:
+// repeated projection returns the same value, and the projected layer range is
+// exactly the range assigned to that stage in the RunPlan.
+#[test]
+fn provision_stage_projection_is_deterministic_and_stage_local() {
+    // Start from one committed plan; projection is a pure public view of it.
+    let plan = plan::plan_run(valid_input(3, 36)).unwrap();
+
+    // Check every stage projection, not only one representative stage.
+    for stage_index in 0..3 {
+        // Derive twice to prove projection does not depend on hidden mutable
+        // state or call order.
+        let first = plan::derive_stage_provision(&plan, stage_index).unwrap();
+        let second = plan::derive_stage_provision(&plan, stage_index).unwrap();
+
+        // Find the corresponding public stage assignment in the plan.
+        let stage = plan
+            .stages
+            .iter()
+            .find(|stage| stage.stage_index == stage_index)
+            .unwrap();
+
+        // The projected message must be stable and expose only that stage's
+        // assigned run position and layer range.
+        assert_eq!(first, second);
+        assert_eq!(first.stage_index, stage_index);
+        assert_eq!(first.stage_count, 3);
+        assert_eq!(first.layer_start, stage.layer_start);
+        assert_eq!(first.layer_end_exclusive, stage.layer_end_exclusive);
+    }
+}
+
+// This proves each stage receives exactly one inbound and one outbound edge
+// provision, and that the provisioned ids are the ids assigned to that stage by
+// the RunPlan.
+#[test]
+fn provision_stage_contains_exactly_the_assigned_inbound_and_outbound_edges() {
+    // Build a valid plan and test projection for every stage in it.
+    let plan = plan::plan_run(valid_input(3, 36)).unwrap();
+
+    for stage in &plan.stages {
+        // Derive the public provisioning message for this stage.
+        let provision = plan::derive_stage_provision(&plan, stage.stage_index).unwrap();
+
+        // The message exposes exactly the inbound and outbound ids assigned in
+        // that stage's StagePlan.
+        assert_eq!(provision.inbound.edge_id, stage.inbound_edge);
+        assert_eq!(provision.outbound.edge_id, stage.outbound_edge);
+    }
+}
+
+// This proves the data-flow addressing contract of provisioning. The outbound
+// side carries the consumer node id; exhaustive struct destructuring also makes
+// remote actor-address fields a compile-time contract violation.
+#[test]
+fn provision_stage_uses_node_id_addressing_not_remote_actor_addresses() {
+    // Build one plan and an edge lookup using only public edge records.
+    let plan = plan::plan_run(valid_input(3, 36)).unwrap();
+    let edges = plan_edges_by_id(&plan);
+
+    for stage in &plan.stages {
+        // Project the stage-local provisioning message.
+        let provision = plan::derive_stage_provision(&plan, stage.stage_index).unwrap();
+
+        // Destructure the inbound provision exhaustively. If a remote actor
+        // address becomes part of this public type, this test must be updated
+        // consciously instead of silently accepting it.
+        let InboundEdgeProvision {
+            edge_id: inbound_edge_id,
+            kind: _,
+            object_spec: _,
+            ring_spec: _,
+        } = provision.inbound.clone();
+
+        // Destructure the outbound provision exhaustively. The only remote
+        // routing fact it may expose is the consumer node id.
+        let OutboundEdgeProvision {
+            edge_id: outbound_edge_id,
+            kind: _,
+            consumer_node_id,
+            object_spec: _,
+            ring_spec: _,
+        } = provision.outbound.clone();
+
+        assert_eq!(inbound_edge_id, stage.inbound_edge);
+        assert_eq!(outbound_edge_id, stage.outbound_edge);
+
+        // The provisioned consumer node id must match the consumer endpoint of
+        // the canonical RunPlan edge.
+        let outbound_edge = edges.get(&outbound_edge_id).unwrap();
+        assert_eq!(consumer_node_id, edge_node_id(&outbound_edge.consumer));
+    }
+}
+
+// This proves every edge carries object and ring specs, activation capacity is
+// derived from model facts, and edge kind selects the correct object kind.
+#[test]
+fn object_and_ring_specs_are_present_and_match_edge_kind() {
+    // Use the canonical model facts so the expected activation capacity is
+    // known directly from the public input.
+    let plan = plan::plan_run(valid_input(3, 36)).unwrap();
+    let expected_activation_extent = 2048 * 4096 * 2;
+
+    // Every edge must carry complete movement specs; no worker or transport may
+    // invent these later.
+    for edge in &plan.edges {
+        assert!(edge.object_spec.max_extent > 0);
+        assert!(edge.ring_spec.data_capacity > 0);
+
+        // Edge kind selects the object kind, and activation capacity is derived
+        // from model facts.
+        match edge.kind {
+            EdgeKind::Activation => {
+                assert_eq!(edge.object_spec.kind, ObjectKind::Activation);
+                assert_eq!(edge.object_spec.max_extent, expected_activation_extent);
+            }
+            EdgeKind::TokenIn | EdgeKind::TokenOut => {
+                assert_eq!(edge.object_spec.kind, ObjectKind::Token);
+            }
+        }
+    }
+}
+
+// This proves object and ring specs are copied consistently into every stage
+// projection. A stage provision may narrow visibility to its own edges, but it
+// may not revise the specs for those edges.
+#[test]
+fn object_and_ring_specs_are_copied_consistently_into_stage_provisions() {
+    // Build a canonical plan and index its public edge records.
+    let plan = plan::plan_run(valid_input(3, 36)).unwrap();
+    let edges = plan_edges_by_id(&plan);
+
+    for stage in &plan.stages {
+        // Project a stage-local provisioning message.
+        let provision = plan::derive_stage_provision(&plan, stage.stage_index).unwrap();
+
+        // The inbound edge spec must be the plan's exact edge spec.
+        let inbound_edge = edges.get(&provision.inbound.edge_id).unwrap();
+        assert_eq!(provision.inbound.kind, inbound_edge.kind);
+        assert_eq!(provision.inbound.object_spec, inbound_edge.object_spec);
+        assert_eq!(provision.inbound.ring_spec, inbound_edge.ring_spec);
+
+        // The outbound edge spec must also be copied, not recomputed or revised.
+        let outbound_edge = edges.get(&provision.outbound.edge_id).unwrap();
+        assert_eq!(provision.outbound.kind, outbound_edge.kind);
+        assert_eq!(provision.outbound.object_spec, outbound_edge.object_spec);
+        assert_eq!(provision.outbound.ring_spec, outbound_edge.ring_spec);
+    }
+}
+
+// This proves typed rejection is the public behavior for invalid authority and
+// topology inputs. No invalid case is allowed to emit a partial plan.
+#[test]
+fn invalid_authority_and_topology_inputs_reject_without_plan() {
+    // Each case changes one authority/topology fact from the valid fixture and
+    // names the typed rejection the planner must expose.
+    let cases = [
+        (
+            invalid_unknown_node(),
+            PlanRejectionKind::UnknownNode,
+            "unknown node id",
+        ),
+        (
+            invalid_duplicate_stage_assignment(),
+            PlanRejectionKind::DuplicateStageAssignment,
+            "duplicate stage assignment",
+        ),
+        (
+            invalid_missing_stage_assignment(),
+            PlanRejectionKind::MissingStage,
+            "missing stage",
+        ),
+        (
+            invalid_zero_stage_count(),
+            PlanRejectionKind::InvalidStageCount,
+            "invalid stage count",
+        ),
+        (
+            invalid_edge_endpoint_mismatch(),
+            PlanRejectionKind::EdgeEndpointMismatch,
+            "edge endpoint mismatch",
+        ),
+        (
+            invalid_model_stage_layout(),
+            PlanRejectionKind::ModelStageLayoutMismatch,
+            "model/stage layout mismatch",
+        ),
+    ];
+
+    // Invalid inputs must not produce a partial plan. The observable result is
+    // a typed rejection kind.
+    for (input, expected, label) in cases {
+        let err = plan::plan_run(input).expect_err(label);
+        assert_eq!(err.kind(), expected, "{label}");
+    }
+}
+
+// This proves invalid object and ring spec facts reject before provisioning.
+// The planner may choose the exact diagnostic payload, but the rejection kind
+// must be typed and no RunPlan may be emitted.
+#[test]
+fn invalid_object_or_ring_specs_reject_without_plan() {
+    // Each case changes one object/ring fact from the valid fixture and names
+    // the typed rejection expected at the planning boundary.
+    let cases = [
+        (
+            invalid_zero_activation_extent(),
+            PlanRejectionKind::InvalidObjectSpec,
+            "zero activation extent",
+        ),
+        (
+            invalid_dtype_width(),
+            PlanRejectionKind::InvalidObjectSpec,
+            "invalid dtype width",
+        ),
+        (
+            invalid_unsupported_shape_or_layout(),
+            PlanRejectionKind::UnsupportedShapeOrLayout,
+            "unsupported shape/layout",
+        ),
+        (
+            invalid_ring_alignment(),
+            PlanRejectionKind::InvalidRingSpec,
+            "invalid ring alignment",
+        ),
+    ];
+
+    // Rejection happens before provisioning: the only public output is the
+    // typed error, never a RunPlan with invalid specs.
+    for (input, expected, label) in cases {
+        let err = plan::plan_run(input).expect_err(label);
+        assert_eq!(err.kind(), expected, "{label}");
+    }
+}
+
+// Unknown-node rejection needs the placement to name a node outside the
+// orchestrator's candidate pool. The rest of the input stays valid so the
+// expected rejection is isolated to authority over node identity.
+fn invalid_unknown_node() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.placement = PlacementInput::FixedLinear(vec![
+        StagePlacement {
+            stage_index: 0,
+            node_id: node(10),
+        },
+        StagePlacement {
+            stage_index: 1,
+            node_id: node(404),
+        },
+        StagePlacement {
+            stage_index: 2,
+            node_id: node(12),
+        },
+    ]);
+    input
+}
+
+// Duplicate-stage rejection is observable when two placement entries claim the
+// same stage index. This checks that the planner does not silently pick one and
+// continue with ambiguous authority.
+fn invalid_duplicate_stage_assignment() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.placement = PlacementInput::FixedLinear(vec![
+        StagePlacement {
+            stage_index: 0,
+            node_id: node(10),
+        },
+        StagePlacement {
+            stage_index: 1,
+            node_id: node(11),
+        },
+        StagePlacement {
+            stage_index: 1,
+            node_id: node(12),
+        },
+    ]);
+    input
+}
+
+// Missing-stage rejection is observable when placement skips an index inside
+// `0..stage_count`. This checks that the planner does not invent hidden stage
+// ownership to patch an incomplete placement.
+fn invalid_missing_stage_assignment() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.placement = PlacementInput::FixedLinear(vec![
+        StagePlacement {
+            stage_index: 0,
+            node_id: node(10),
+        },
+        StagePlacement {
+            stage_index: 2,
+            node_id: node(12),
+        },
+    ]);
+    input
+}
+
+// Zero stages cannot form the MVP pipeline. This fixture isolates the invalid
+// stage-count path without adding any other contradictory facts.
+fn invalid_zero_stage_count() -> PlannerInput {
+    valid_input(0, 36)
+}
+
+// Endpoint mismatch rejection needs an input that tries to override the linear
+// edge contract. The planner must reject a skipped-stage activation edge rather
+// than accepting a non-MVP topology.
+fn invalid_edge_endpoint_mismatch() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.placement = PlacementInput::FixedLinearWithEdgeOverride {
+        stages: vec![
+            StagePlacement {
+                stage_index: 0,
+                node_id: node(10),
+            },
+            StagePlacement {
+                stage_index: 1,
+                node_id: node(11),
+            },
+            StagePlacement {
+                stage_index: 2,
+                node_id: node(12),
+            },
+        ],
+        forced_activation_edges: vec![(0, 2)],
+    };
+    input
+}
+
+// The current contract requires one non-empty layer range per stage. Fewer
+// layers than stages forces an empty range unless explicitly allowed, so this
+// fixture should reject at the model/stage-layout boundary.
+fn invalid_model_stage_layout() -> PlannerInput {
+    let mut input = valid_input(4, 3);
+    input.placement = linear_placement(4);
+    input
+}
+
+// Zero sequence length makes activation capacity zero. The planner must reject
+// before creating edges whose object specs cannot carry an activation.
+fn invalid_zero_activation_extent() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.model.max_seq_len = 0;
+    input
+}
+
+// Dtype width participates directly in activation extent and object layout.
+// A zero width is not a valid dtype fact and must reject before planning.
+fn invalid_dtype_width() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.model.dtype_width_bytes = 0;
+    input
+}
+
+// Hidden dimension participates directly in activation shape. A zero hidden
+// dimension represents an unsupported shape/layout fact for the MVP contract.
+fn invalid_unsupported_shape_or_layout() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.model.hidden_dim = 0;
+    input
+}
+
+// Ring alignment must be a usable alignment contract for shared memory and
+// device copy boundaries. A non-power-of-two alignment makes the ring spec
+// invalid before any edge can be provisioned.
+fn invalid_ring_alignment() -> PlannerInput {
+    let mut input = valid_input(3, 36);
+    input.activation_ring.alignment = 3;
+    input
+}

tests/mvp_system/shared_ring_helper_abi_guarantees.rs

@@ -0,0 +1,219 @@
+//! Black-box contract tests for the MVP shared ring helper ABI.
+//!
+//! These tests intentionally know only the public helper surface:
+//!
+//! - helper-created bounded SPSC rings
+//! - reserve, write, publish, read, consume, and wake operations
+//! - cursor snapshots and wake hints observed through the helper
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/shared_ring_helper_abi_contract.md`.
+
+use mvp_system::shared_ring_helper_abi as ring;
+
+// A small ring forces wraparound and full/empty transitions quickly. The helper
+// still owns the actual shared-memory atomics and process-local address math.
+fn new_ring() -> ring::RingHelperHarness {
+    ring::RingHelperHarness::create(ring::RingConfig {
+        node_id: ring::NodeId(10),
+        ring_id: ring::RingId(7000),
+        capacity: 8,
+        producer: ring::EndpointId("producer".into()),
+        consumer: ring::EndpointId("consumer".into()),
+    })
+}
+
+// This helper reads all currently committed bytes through the consumer API.
+// It proves visibility through acquire reads instead of peeking at backing
+// memory directly.
+fn drain_committed(helper: &mut ring::RingHelperHarness) -> Vec<u8> {
+    let readable = helper.consumer_readable();
+    let bytes = helper.consumer_read(readable);
+    helper.consumer_consume(readable);
+    bytes
+}
+
+// Wake hints must remain hints. This helper checks the public wake enum without
+// depending on scheduler internals.
+fn assert_wake_is_payload_free(wake: &ring::WakeHint) {
+    match wake {
+        ring::WakeHint::RingReadable { ring_id }
+        | ring::WakeHint::RingWritable { ring_id } => {
+            assert_eq!(*ring_id, ring::RingId(7000));
+        }
+    }
+}
+
+// This proves ring identity is bounded SPSC, has one producer and one consumer,
+// uses unique RingId values, and does not allow stale wakes to alias a
+// replacement ring.
+#[test]
+fn ring_identity_is_unique_bounded_spsc_and_stale_wakes_do_not_alias() {
+    // Create one ring and inspect its public identity.
+    let mut helper = new_ring();
+    let identity = helper.identity();
+    assert_eq!(identity.ring_id, ring::RingId(7000));
+    assert_eq!(identity.capacity, 8);
+    assert_eq!(identity.producer_count, 1);
+    assert_eq!(identity.consumer_count, 1);
+
+    // Retire it and create a replacement with the same numeric id but a new
+    // generation. Stale wake from the retired generation must not wake the new
+    // ring.
+    let stale_wake = helper.retire_and_capture_stale_wake();
+    let mut replacement = ring::RingHelperHarness::create_replacement(identity.ring_id);
+    replacement.deliver_wake(stale_wake);
+    assert!(!replacement.wake_log().iter().any(|wake| wake.was_accepted));
+}
+
+// This proves commit and consume are monotonic logical byte positions, writes
+// are invisible before commit, and physical wrap uses cursor modulo capacity.
+#[test]
+fn cursors_are_monotonic_and_wrap_by_modulo_capacity() {
+    // Reserve and write without publishing.
+    let mut helper = new_ring();
+    let reservation = helper.producer_reserve(6).expect("space must exist");
+    helper.producer_write(&reservation, b"abcdef");
+
+    // Producer-local write is not readable before commit.
+    assert_eq!(helper.consumer_readable(), 0);
+
+    // Publishing makes the prefix readable and advances commit.
+    helper.producer_commit(reservation);
+    assert_eq!(helper.cursor_snapshot().commit, 6);
+    assert_eq!(drain_committed(&mut helper), b"abcdef");
+    assert_eq!(helper.cursor_snapshot().consume, 6);
+
+    // Wrap the physical index while logical cursors keep increasing.
+    let wrapped = helper.producer_reserve(5).expect("space must exist after consume");
+    helper.producer_write(&wrapped, b"ghijk");
+    helper.producer_commit(wrapped);
+    assert_eq!(helper.cursor_snapshot().commit, 11);
+    assert_eq!(helper.cursor_snapshot().commit % helper.identity().capacity, 3);
+    assert_eq!(drain_committed(&mut helper), b"ghijk");
+    assert_eq!(helper.cursor_snapshot().consume, 11);
+}
+
+// This proves the producer computes free space from acquired consume, never
+// reserves beyond capacity, writes before publishing commit, and emits readable
+// wake hints after publication.
+#[test]
+fn producer_respects_free_space_and_publishes_after_writing() {
+    // Reserve the full ring and publish it.
+    let mut helper = new_ring();
+    let reservation = helper.producer_reserve(8).expect("full ring reservation fits");
+    helper.producer_write(&reservation, b"12345678");
+    helper.producer_commit(reservation);
+
+    // With no consumed bytes, producer cannot reserve additional space.
+    assert!(matches!(
+        helper.producer_reserve(1),
+        Err(ring::ReserveError::InsufficientSpace)
+    ));
+
+    // The readable wake must be a payload-free hint.
+    let wake = helper
+        .wake_hints()
+        .iter()
+        .find(|wake| matches!(wake, ring::WakeHint::RingReadable { .. }))
+        .expect("readable wake must be emitted");
+    assert_wake_is_payload_free(wake);
+
+    // Consumer sees the written bytes, proving commit was not published before
+    // the payload became valid.
+    assert_eq!(drain_committed(&mut helper), b"12345678");
+}
+
+// This proves the consumer computes readable bytes from acquired commit, never
+// reads beyond committed data, advances consume only after release, and emits
+// writable wake hints after freeing space.
+#[test]
+fn consumer_reads_only_committed_bytes_and_releases_after_safe_consume() {
+    // Publish three committed bytes.
+    let mut helper = new_ring();
+    let reservation = helper.producer_reserve(3).expect("space must exist");
+    helper.producer_write(&reservation, b"abc");
+    helper.producer_commit(reservation);
+
+    // The consumer cannot read beyond the committed prefix.
+    assert_eq!(helper.consumer_readable(), 3);
+    assert!(matches!(
+        helper.consumer_try_read(4),
+        Err(ring::ReadError::BeyondCommittedBytes)
+    ));
+
+    // Reading alone does not release bytes.
+    assert_eq!(helper.consumer_read(3), b"abc");
+    assert_eq!(helper.cursor_snapshot().consume, 0);
+
+    // Consuming releases space and emits a writable hint.
+    helper.consumer_consume(3);
+    assert_eq!(helper.cursor_snapshot().consume, 3);
+    let wake = helper
+        .wake_hints()
+        .iter()
+        .find(|wake| matches!(wake, ring::WakeHint::RingWritable { .. }))
+        .expect("writable wake must be emitted");
+    assert_wake_is_payload_free(wake);
+}
+
+// This proves wake hints carry no byte ranges, counts, pointers, or credits,
+// and coalescing cannot hide the only readable or writable transition.
+#[test]
+fn wake_hints_are_edge_hints_without_hiding_transitions() {
+    // Create an empty ring and publish one byte, causing empty-to-readable.
+    let mut helper = new_ring();
+    let reservation = helper.producer_reserve(1).expect("space must exist");
+    helper.producer_write(&reservation, b"x");
+    helper.producer_commit(reservation);
+
+    // The readable transition must be discoverable even if duplicate wakes are
+    // coalesced.
+    helper.coalesce_duplicate_wakes();
+    assert!(helper.scheduler_state().readable_rings.contains(&ring::RingId(7000)));
+
+    // Fill then release space to cause full-to-writable.
+    let _ = drain_committed(&mut helper);
+    helper.coalesce_duplicate_wakes();
+    assert!(helper.scheduler_state().writable_rings.contains(&ring::RingId(7000)));
+
+    // Every wake remains a payload-free hint.
+    for wake in helper.wake_hints() {
+        assert_wake_is_payload_free(wake);
+    }
+}
+
+// This proves Python-facing helper operations own shared atomics and wrap math,
+// while returned pointers are process-local addresses derived from arena base
+// plus arena offsets.
+#[test]
+fn helper_abi_owns_atomics_wrap_math_and_process_local_pointers() {
+    // Ask the helper for a process-local view of a layout.
+    let helper = new_ring();
+    let view = helper.map_process_local_view(ring::ArenaBase(0x1000));
+
+    // The helper returns process-local addresses derived from offsets.
+    assert_eq!(
+        view.data_pointer,
+        ring::ProcessLocalPointer::from_base_plus_offset(
+            ring::ArenaBase(0x1000),
+            view.layout.data_offset
+        )
+    );
+
+    // Python operations use helper calls for cursor and wrap behavior instead
+    // of implementing atomics directly.
+    for operation in helper.python_visible_operations() {
+        match operation {
+            ring::PythonOperation::ReserveViaHelper { .. }
+            | ring::PythonOperation::CommitViaHelper { .. }
+            | ring::PythonOperation::ReadableViaHelper { .. }
+            | ring::PythonOperation::ConsumeViaHelper { .. }
+            | ring::PythonOperation::MapPointerViaHelper { .. } => {}
+            ring::PythonOperation::DirectAtomicAccess { .. }
+            | ring::PythonOperation::DirectWrapArithmetic { .. } => {
+                panic!("Python operation bypassed helper ABI: {operation:?}")
+            }
+        }
+    }
+}

tests/mvp_system/stage_controller_guarantees.rs

@@ -0,0 +1,360 @@
+//! Black-box contract tests for MVP StageController behavior.
+//!
+//! These tests intentionally know only the public stage-controller surface:
+//!
+//! - `ProvisionStage`, worker, edge, object, stop, and fault events in
+//! - worker commands, lifecycle events, and teardown events out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/stage_controller_contract.md`.
+
+use mvp_system::stage_controller as stage;
+
+// This provision fixture represents a single middle stage. It has one inbound
+// and one outbound edge so tests can prove the controller uses assigned edges
+// without relying on endpoint internals.
+fn valid_provision() -> stage::ProvisionStage {
+    stage::ProvisionStage {
+        run_id: stage::RunId(7),
+        authorized_orchestrator: stage::NodeId(99),
+        node_id: stage::NodeId(11),
+        stage_index: 1,
+        stage_count: 3,
+        layer_range: stage::LayerRange {
+            start: 12,
+            end_exclusive: 24,
+        },
+        inbound: stage::EdgeProvision::inbound(stage::EdgeId(7001)),
+        outbound: stage::EdgeProvision::outbound(stage::EdgeId(7002)),
+        weight_source: stage::WeightSource::TestArtifact("model.gguf".into()),
+    }
+}
+
+// The harness exposes only public messages. Tests intentionally do not inspect
+// private controller states such as "Preparing" or "Executing"; they infer
+// controller behavior from emitted commands and lifecycle events.
+fn new_controller() -> stage::StageControllerHarness {
+    stage::StageControllerHarness::new(stage::NodeId(11))
+}
+
+// Preparation readiness has four independent prerequisites. Listing them as
+// public observations lets tests prove StageReady is a barrier across worker,
+// weights, inbound edge, and outbound edge readiness.
+fn preparation_ready_events() -> Vec<stage::StageEvent> {
+    vec![
+        stage::StageEvent::WorkerReady,
+        stage::StageEvent::WeightsReady,
+        stage::StageEvent::InboundEdgeReady {
+            edge_id: stage::EdgeId(7001),
+        },
+        stage::StageEvent::OutboundEdgeReady {
+            edge_id: stage::EdgeId(7002),
+        },
+    ]
+}
+
+// This helper provisions and readies a stage through public events. Tests that
+// focus on execution use it to avoid duplicating setup while still going through
+// the same observable path as production.
+fn ready_stage() -> stage::StageControllerHarness {
+    let mut harness = new_controller();
+    harness.observe(stage::StageEvent::ProvisionStage {
+        from: stage::NodeId(99),
+        provision: valid_provision(),
+    });
+    for event in preparation_ready_events() {
+        harness.observe(event);
+    }
+    harness
+}
+
+// This proves provisioning is authorized, validated before setup, and does not
+// allow a stage to rewire its assigned inbound or outbound edge.
+#[test]
+fn provisioning_validates_authority_and_assigned_shape_before_setup() {
+    // Send a valid provision from the authorized orchestrator.
+    let mut harness = new_controller();
+    harness.observe(stage::StageEvent::ProvisionStage {
+        from: stage::NodeId(99),
+        provision: valid_provision(),
+    });
+
+    // Setup commands should be derived from the provided assignment.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            stage::StageCommand::EstablishInboundEdge {
+                edge_id: stage::EdgeId(7001),
+                ..
+            }
+        )
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            stage::StageCommand::EstablishOutboundEdge {
+                edge_id: stage::EdgeId(7002),
+                ..
+            }
+        )
+    }));
+
+    // The controller must not emit any command that replaces the provisioned
+    // edge ids with a locally chosen edge.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(command, stage::StageCommand::RewireEdge { .. })
+    }));
+
+    // An unauthorized provision attempt must fault before setup can begin.
+    let mut unauthorized = new_controller();
+    unauthorized.observe(stage::StageEvent::ProvisionStage {
+        from: stage::NodeId(123),
+        provision: valid_provision(),
+    });
+    assert!(unauthorized.events().iter().any(|event| {
+        matches!(
+            event,
+            stage::StageLifecycleEvent::StageFault {
+                reason: stage::StageFaultReason::UnauthorizedProvision,
+                ..
+            }
+        )
+    }));
+    assert!(!unauthorized.commands().iter().any(|command| {
+        matches!(command, stage::StageCommand::ConfigureWorkerRole { .. })
+    }));
+}
+
+// This proves StageReady is emitted only after worker readiness, weight
+// readiness, inbound edge readiness, and outbound edge readiness are all
+// observed.
+#[test]
+fn stage_ready_waits_for_worker_weights_and_both_edges() {
+    // Provision the stage so preparation can begin.
+    let mut harness = new_controller();
+    harness.observe(stage::StageEvent::ProvisionStage {
+        from: stage::NodeId(99),
+        provision: valid_provision(),
+    });
+
+    // Feed every readiness event except the final one and prove no prefix is
+    // enough for StageReady.
+    let mut events = preparation_ready_events();
+    let final_event = events.pop().expect("fixture has final setup event");
+    for event in events {
+        harness.observe(event);
+        assert!(!harness.events().iter().any(|event| {
+            matches!(event, stage::StageLifecycleEvent::StageReady { .. })
+        }));
+    }
+
+    // The final prerequisite crosses the barrier.
+    harness.observe(final_event);
+
+    // StageReady appears exactly once for the provisioned stage.
+    let ready_count = harness
+        .events()
+        .iter()
+        .filter(|event| {
+            matches!(
+                event,
+                stage::StageLifecycleEvent::StageReady {
+                    run_id: stage::RunId(7),
+                    stage_index: 1,
+                }
+            )
+        })
+        .count();
+    assert_eq!(ready_count, 1);
+}
+
+// This proves a ready stage admits work only from inbound ObjectLoaded, issues
+// one ExecuteStep per accepted object, and binds output with the same sequence.
+#[test]
+fn accepted_inbound_object_creates_one_same_sequence_execute_step() {
+    // Bring the stage to ready state through public setup events.
+    let mut harness = ready_stage();
+
+    // Deliver the first inbound object, sequence 0.
+    harness.observe(stage::StageEvent::ObjectLoaded {
+        edge_id: stage::EdgeId(7001),
+        object_id: stage::ObjectId(9000),
+        sequence: 0,
+        handle: stage::DeviceHandle::new_current(42),
+    });
+
+    // Exactly one ExecuteStep command must result from that accepted object.
+    let execute_steps = harness
+        .commands()
+        .iter()
+        .filter_map(|command| match command {
+            stage::StageCommand::ExecuteStep(step) => Some(step),
+            _ => None,
+        })
+        .collect::<Vec<_>>();
+    assert_eq!(execute_steps.len(), 1);
+
+    // The output binding must preserve the input sequence.
+    assert_eq!(execute_steps[0].input.sequence, 0);
+    assert_eq!(execute_steps[0].outputs[0].sequence, 0);
+
+    // A second object while the first step is active must not create another
+    // active ExecuteStep in the MVP.
+    harness.observe(stage::StageEvent::ObjectLoaded {
+        edge_id: stage::EdgeId(7001),
+        object_id: stage::ObjectId(9001),
+        sequence: 1,
+        handle: stage::DeviceHandle::new_current(43),
+    });
+    let active_steps = harness
+        .commands()
+        .iter()
+        .filter(|command| matches!(command, stage::StageCommand::ExecuteStep(_)))
+        .count();
+    assert_eq!(active_steps, 1);
+}
+
+// This proves the sequence contract: sequence 0 is accepted as prefill, decode
+// sequences must strictly increase, and duplicate, skipped, or out-of-order
+// inputs fault the stage.
+#[test]
+fn duplicate_skipped_and_out_of_order_sequences_fault() {
+    // Each invalid trace starts from a freshly readied stage.
+    let invalid_traces = vec![
+        vec![0, 0],
+        vec![0, 2],
+        vec![0, 1, 0],
+    ];
+
+    for trace in invalid_traces {
+        // Accept the first object and complete its step when needed so the next
+        // object is admitted through the normal public path.
+        let mut harness = ready_stage();
+        for (i, sequence) in trace.iter().enumerate() {
+            harness.observe(stage::StageEvent::ObjectLoaded {
+                edge_id: stage::EdgeId(7001),
+                object_id: stage::ObjectId(9000 + i as u64),
+                sequence: *sequence,
+                handle: stage::DeviceHandle::new_current(100 + i as u64),
+            });
+            if i + 1 < trace.len() {
+                harness.observe(stage::StageEvent::StepCompleted {
+                    step_id: stage::StepId(i as u64),
+                });
+            }
+        }
+
+        // The transcript must contain a sequence fault for the invalid trace.
+        assert!(harness.events().iter().any(|event| {
+            matches!(
+                event,
+                stage::StageLifecycleEvent::StageFault {
+                    reason: stage::StageFaultReason::SequenceViolation,
+                    ..
+                }
+            )
+        }));
+    }
+}
+
+// This proves compute completion is observed only after the worker reports
+// StepCompleted, and completion returns the stage to ready-for-next-object.
+#[test]
+fn step_completed_releases_input_and_admits_next_object() {
+    // Start one accepted step.
+    let mut harness = ready_stage();
+    harness.observe(stage::StageEvent::ObjectLoaded {
+        edge_id: stage::EdgeId(7001),
+        object_id: stage::ObjectId(9000),
+        sequence: 0,
+        handle: stage::DeviceHandle::new_current(42),
+    });
+
+    // Before worker completion, no compute-complete lifecycle event is allowed.
+    assert!(!harness.events().iter().any(|event| {
+        matches!(event, stage::StageLifecycleEvent::StepAccepted { sequence: 1, .. })
+    }));
+
+    // Worker StepCompleted is the public completion signal.
+    harness.observe(stage::StageEvent::StepCompleted {
+        step_id: stage::StepId(0),
+    });
+
+    // The controller releases per-step input according to policy.
+    assert!(harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            stage::StageCommand::ReleaseInputHandle {
+                object_id: stage::ObjectId(9000),
+                ..
+            }
+        )
+    }));
+
+    // The next sequence is now admissible.
+    harness.observe(stage::StageEvent::ObjectLoaded {
+        edge_id: stage::EdgeId(7001),
+        object_id: stage::ObjectId(9001),
+        sequence: 1,
+        handle: stage::DeviceHandle::new_current(43),
+    });
+    let execute_count = harness
+        .commands()
+        .iter()
+        .filter(|command| matches!(command, stage::StageCommand::ExecuteStep(_)))
+        .count();
+    assert_eq!(execute_count, 2);
+}
+
+// This proves worker, object, output-edge, and step failures fault the stage,
+// and after fault no new run work is accepted until StopRun.
+#[test]
+fn stage_fault_rejects_new_work_until_stopped() {
+    // Start from a ready stage and inject a worker crash.
+    let mut harness = ready_stage();
+    harness.observe(stage::StageEvent::WorkerCrashed);
+
+    // Fault must be visible at the stage boundary.
+    assert!(harness.events().iter().any(|event| {
+        matches!(
+            event,
+            stage::StageLifecycleEvent::StageFault {
+                reason: stage::StageFaultReason::WorkerCrashed,
+                ..
+            }
+        )
+    }));
+
+    // New work after fault must not produce ExecuteStep.
+    let before = harness
+        .commands()
+        .iter()
+        .filter(|command| matches!(command, stage::StageCommand::ExecuteStep(_)))
+        .count();
+    harness.observe(stage::StageEvent::ObjectLoaded {
+        edge_id: stage::EdgeId(7001),
+        object_id: stage::ObjectId(9999),
+        sequence: 0,
+        handle: stage::DeviceHandle::new_current(77),
+    });
+    let after = harness
+        .commands()
+        .iter()
+        .filter(|command| matches!(command, stage::StageCommand::ExecuteStep(_)))
+        .count();
+    assert_eq!(after, before);
+
+    // StopRun moves the stage through local teardown and emits StageStopped.
+    harness.observe(stage::StageEvent::StopRun {
+        run_id: stage::RunId(7),
+    });
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, stage::StageCommand::StopLocalEdges { .. })
+    }));
+    assert!(harness.commands().iter().any(|command| {
+        matches!(command, stage::StageCommand::ReleaseRunDeviceObjects { .. })
+    }));
+    assert!(harness.events().iter().any(|event| {
+        matches!(event, stage::StageLifecycleEvent::StageStopped { .. })
+    }));
+}

tests/mvp_system/tx_rx_edge_actor_guarantees.rs

@@ -0,0 +1,247 @@
+//! Black-box contract tests for MVP Tx and Rx edge actors.
+//!
+//! These tests intentionally know only the public edge-actor surface:
+//!
+//! - lifecycle, object identity, stop, stream fault, and object fault events in
+//! - role-facing lifecycle/object events out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/tx_rx_edge_actor_contract.md`.
+
+use mvp_system::tx_rx_edge_actor as edge_actor;
+
+// The edge id fixture gives both actors a shared identity while keeping Tx and
+// Rx lifecycle tests independent from driver and ring internals.
+fn edge_id() -> edge_actor::EdgeId {
+    edge_actor::EdgeId(7001)
+}
+
+// Tx starts in provisioning and represents the producer side of one edge. The
+// harness records only actor messages, not bytes or flow-control details.
+fn new_tx() -> edge_actor::TxActorHarness {
+    edge_actor::TxActorHarness::new(edge_actor::TxConfig {
+        edge_id: edge_id(),
+        role_port: edge_actor::PortId("out".into()),
+    })
+}
+
+// Rx starts in provisioning and represents the consumer side of one edge. It
+// exposes complete object identities and opaque handles to the role layer.
+fn new_rx() -> edge_actor::RxActorHarness {
+    edge_actor::RxActorHarness::new(edge_actor::RxConfig {
+        edge_id: edge_id(),
+        role_port: edge_actor::PortId("in".into()),
+    })
+}
+
+// This helper is a compile-time and runtime guard for payload isolation. If the
+// public actor message enum grows a payload-bearing variant, this exhaustive
+// match has to be updated and the test discussion becomes explicit.
+fn assert_actor_message_is_payload_free(message: &edge_actor::ActorMessage) {
+    match message {
+        edge_actor::ActorMessage::Lifecycle { .. }
+        | edge_actor::ActorMessage::ObjectIdentity { .. }
+        | edge_actor::ActorMessage::OpaqueHandle { .. }
+        | edge_actor::ActorMessage::CoarseFault { .. } => {}
+        edge_actor::ActorMessage::PayloadBytes { .. }
+        | edge_actor::ActorMessage::HostPointer { .. }
+        | edge_actor::ActorMessage::ByteRange { .. }
+        | edge_actor::ActorMessage::CreditCount { .. } => {
+            panic!("edge actor message carried payload or flow-control detail: {message:?}")
+        }
+    }
+}
+
+// This proves Tx and Rx actors are tied to one edge id, receive lifecycle/object
+// events only, and do not traffic payload bytes, pointers, ranges, credits, or
+// free-space counts.
+#[test]
+fn edge_actor_messages_are_lifecycle_identity_and_handle_only() {
+    // Create one Tx and one Rx actor for the same edge id.
+    let mut tx = new_tx();
+    let mut rx = new_rx();
+
+    // Drive typical lifecycle and object events.
+    tx.observe(edge_actor::TxEvent::EdgeReady { edge_id: edge_id() });
+    tx.observe(edge_actor::TxEvent::ObjectProduced {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+    });
+    rx.observe(edge_actor::RxEvent::EdgeReady { edge_id: edge_id() });
+    rx.observe(edge_actor::RxEvent::ObjectLoaded {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+        handle: edge_actor::OpaqueHandle::new(42),
+    });
+
+    // Every emitted actor message must stay payload-free.
+    for message in tx.messages().iter().chain(rx.messages()) {
+        assert_actor_message_is_payload_free(message);
+    }
+
+    // Both actors remain tied to exactly one edge id.
+    assert!(tx.messages().iter().all(|message| message.edge_id() == edge_id()));
+    assert!(rx.messages().iter().all(|message| message.edge_id() == edge_id()));
+}
+
+// This proves Tx starts in provisioning, becomes ready only after EdgeReady,
+// allows producing only after ready, reports produced object identity, and moves
+// to faulted on stream or object faults.
+#[test]
+fn tx_lifecycle_gates_production_and_faults_on_stream_or_object_failure() {
+    // Before EdgeReady, production is rejected.
+    let mut tx = new_tx();
+    tx.observe(edge_actor::TxEvent::ObjectProduced {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+    });
+    assert!(!tx.messages().iter().any(|message| {
+        matches!(message, edge_actor::ActorMessage::ObjectIdentity { .. })
+    }));
+
+    // EdgeReady admits production.
+    tx.observe(edge_actor::TxEvent::EdgeReady { edge_id: edge_id() });
+    tx.observe(edge_actor::TxEvent::ObjectProduced {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+    });
+    assert!(tx.messages().iter().any(|message| {
+        matches!(
+            message,
+            edge_actor::ActorMessage::ObjectIdentity {
+                edge_id: edge_actor::EdgeId(7001),
+                object_id: edge_actor::ObjectId(9000),
+                sequence: 0,
+                ..
+            }
+        )
+    }));
+
+    // Stream fault moves Tx to faulted and suppresses later production.
+    tx.observe(edge_actor::TxEvent::StreamFault { edge_id: edge_id() });
+    let produced_before = tx
+        .messages()
+        .iter()
+        .filter(|message| matches!(message, edge_actor::ActorMessage::ObjectIdentity { .. }))
+        .count();
+    tx.observe(edge_actor::TxEvent::ObjectProduced {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9001),
+        sequence: 1,
+    });
+    let produced_after = tx
+        .messages()
+        .iter()
+        .filter(|message| matches!(message, edge_actor::ActorMessage::ObjectIdentity { .. }))
+        .count();
+    assert_eq!(produced_after, produced_before);
+}
+
+// This proves Rx starts in provisioning, becomes ready only after EdgeReady,
+// exposes loaded objects only after ObjectLoaded, and moves to faulted on stream
+// or object faults.
+#[test]
+fn rx_lifecycle_gates_loaded_objects_and_faults_on_stream_or_object_failure() {
+    // Before EdgeReady, loaded objects are not exposed to the role layer.
+    let mut rx = new_rx();
+    rx.observe(edge_actor::RxEvent::ObjectLoaded {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+        handle: edge_actor::OpaqueHandle::new(42),
+    });
+    assert!(!rx.messages().iter().any(|message| {
+        matches!(message, edge_actor::ActorMessage::OpaqueHandle { .. })
+    }));
+
+    // EdgeReady admits ObjectLoaded exposure.
+    rx.observe(edge_actor::RxEvent::EdgeReady { edge_id: edge_id() });
+    rx.observe(edge_actor::RxEvent::ObjectLoaded {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+        handle: edge_actor::OpaqueHandle::new(42),
+    });
+    assert!(rx.messages().iter().any(|message| {
+        matches!(
+            message,
+            edge_actor::ActorMessage::OpaqueHandle {
+                edge_id: edge_actor::EdgeId(7001),
+                object_id: edge_actor::ObjectId(9000),
+                sequence: 0,
+                ..
+            }
+        )
+    }));
+
+    // Object failure faults Rx and suppresses later loaded objects.
+    rx.observe(edge_actor::RxEvent::ObjectFailed { edge_id: edge_id() });
+    let loaded_before = rx
+        .messages()
+        .iter()
+        .filter(|message| matches!(message, edge_actor::ActorMessage::OpaqueHandle { .. }))
+        .count();
+    rx.observe(edge_actor::RxEvent::ObjectLoaded {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9001),
+        sequence: 1,
+        handle: edge_actor::OpaqueHandle::new(43),
+    });
+    let loaded_after = rx
+        .messages()
+        .iter()
+        .filter(|message| matches!(message, edge_actor::ActorMessage::OpaqueHandle { .. }))
+        .count();
+    assert_eq!(loaded_after, loaded_before);
+}
+
+// This proves StopEdge moves actors toward stopped, stale events after stop are
+// ignored, and mismatched edge ids reject or fault according to policy.
+#[test]
+fn stop_and_mismatched_edge_events_do_not_create_run_work() {
+    // Ready Tx and Rx actors, then stop them.
+    let mut tx = new_tx();
+    let mut rx = new_rx();
+    tx.observe(edge_actor::TxEvent::EdgeReady { edge_id: edge_id() });
+    rx.observe(edge_actor::RxEvent::EdgeReady { edge_id: edge_id() });
+    tx.observe(edge_actor::TxEvent::StopEdge { edge_id: edge_id() });
+    rx.observe(edge_actor::RxEvent::StopEdge { edge_id: edge_id() });
+
+    // Stale post-stop object events must be ignored.
+    tx.observe(edge_actor::TxEvent::ObjectProduced {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+    });
+    rx.observe(edge_actor::RxEvent::ObjectLoaded {
+        edge_id: edge_id(),
+        object_id: edge_actor::ObjectId(9000),
+        sequence: 0,
+        handle: edge_actor::OpaqueHandle::new(42),
+    });
+    assert!(!tx.messages().iter().any(|message| {
+        matches!(message, edge_actor::ActorMessage::ObjectIdentity { .. })
+    }));
+    assert!(!rx.messages().iter().any(|message| {
+        matches!(message, edge_actor::ActorMessage::OpaqueHandle { .. })
+    }));
+
+    // A mismatched edge id must reject or fault, not create work on this actor.
+    let mut mismatched = new_tx();
+    mismatched.observe(edge_actor::TxEvent::EdgeReady {
+        edge_id: edge_actor::EdgeId(9999),
+    });
+    assert!(mismatched.messages().iter().any(|message| {
+        matches!(
+            message,
+            edge_actor::ActorMessage::CoarseFault {
+                reason: edge_actor::ActorFaultReason::MismatchedEdgeId,
+                ..
+            }
+        )
+    }));
+}

tests/mvp_system/weight_lifecycle_guarantees.rs

@@ -0,0 +1,225 @@
+//! Black-box contract tests for MVP stage-local weight lifecycle.
+//!
+//! These tests intentionally know only the public weight-work surface:
+//!
+//! - `ProvisionStage` assignment in
+//! - artifact, parse, allocation, binding, and cache outcomes in
+//! - `WeightsReady`, `StageReady`, and `StageFault` out
+//!
+//! They assert the guarantees in
+//! `specs/mvp_system/weight_lifecycle_contract.md`.
+
+use mvp_system::weight_lifecycle as weights;
+
+// A valid assignment gives the stage exactly one layer range and one source.
+// Tests vary only source or failure outcome so the assignment contract remains
+// visible.
+fn valid_assignment() -> weights::WeightAssignment {
+    weights::WeightAssignment {
+        run_id: weights::RunId(7),
+        stage_index: 1,
+        plan_layer_range: weights::LayerRange {
+            start: 12,
+            end_exclusive: 24,
+        },
+        assigned_layer_range: weights::LayerRange {
+            start: 12,
+            end_exclusive: 24,
+        },
+        source: weights::WeightSource::WholeGguf {
+            uri: "test://model.gguf".into(),
+        },
+    }
+}
+
+// Weight loading is intentionally opaque. The harness accepts public loader and
+// worker outcomes and records only stage-visible events and commands.
+fn new_weight_harness() -> weights::WeightLifecycleHarness {
+    weights::WeightLifecycleHarness::new(weights::NodeId(11))
+}
+
+// The success facts represent the observable prerequisites for WeightsReady:
+// artifact bytes exist, the assigned layer range is valid, and the worker has
+// loaded or bound that range.
+fn successful_load_events() -> Vec<weights::WeightEvent> {
+    vec![
+        weights::WeightEvent::ArtifactAvailable {
+            bytes: weights::ArtifactBytes::Local,
+        },
+        weights::WeightEvent::LayerRangeValidated,
+        weights::WeightEvent::WorkerRangeBound,
+    ]
+}
+
+// Each failure case maps one public loader or worker failure to the stable
+// stage fault reason expected at the control boundary.
+fn failure_cases() -> Vec<(weights::WeightEvent, weights::StageFaultReason)> {
+    vec![
+        (
+            weights::WeightEvent::DownloadFailed,
+            weights::StageFaultReason::WeightDownloadFailed,
+        ),
+        (
+            weights::WeightEvent::ParseFailed,
+            weights::StageFaultReason::WeightParseFailed,
+        ),
+        (
+            weights::WeightEvent::DeviceAllocationFailed,
+            weights::StageFaultReason::DeviceAllocationFailed,
+        ),
+        (
+            weights::WeightEvent::BindingFailed,
+            weights::StageFaultReason::WeightBindingFailed,
+        ),
+        (
+            weights::WeightEvent::InvalidLayerRange,
+            weights::StageFaultReason::InvalidLayerRange,
+        ),
+    ]
+}
+
+// This proves a stage receives weight source and exactly one assigned layer
+// range from provisioning, validates it against the plan, and does not claim
+// graph-visible ownership outside that range.
+#[test]
+fn assignment_is_stage_local_and_range_limited() {
+    // Start weight work from the provisioned assignment.
+    let mut harness = new_weight_harness();
+    harness.observe(weights::WeightEvent::Provisioned(valid_assignment()));
+
+    // The load command may use the physical source, but its graph-visible layer
+    // range must be the assigned range.
+    for command in harness.commands() {
+        if let weights::WeightCommand::LoadOrBindRange { range, .. } = command {
+            assert_eq!(
+                *range,
+                weights::LayerRange {
+                    start: 12,
+                    end_exclusive: 24,
+                }
+            );
+        }
+    }
+
+    // There must be no command claiming ownership of neighboring layers.
+    assert!(!harness.commands().iter().any(|command| {
+        matches!(
+            command,
+            weights::WeightCommand::AdvertiseLoadedLayerRange {
+                range,
+                ..
+            } if range.start < 12 || range.end_exclusive > 24
+        )
+    }));
+}
+
+// This proves whole GGUF download, shard download, and cache use are physical
+// mechanisms with the same public outcome: WeightsReady or StageFault.
+#[test]
+fn supported_physical_sources_have_same_visible_success_contract() {
+    // Exercise every supported source without asserting how bytes are obtained.
+    let sources = vec![
+        weights::WeightSource::WholeGguf {
+            uri: "test://model.gguf".into(),
+        },
+        weights::WeightSource::ShardSet {
+            uris: vec!["test://model.layers.12-24.gguf".into()],
+        },
+        weights::WeightSource::CachedArtifact {
+            cache_key: "model:layers:12-24".into(),
+        },
+    ];
+
+    for source in sources {
+        // Install the source in an otherwise valid assignment.
+        let mut assignment = valid_assignment();
+        assignment.source = source;
+        let mut harness = new_weight_harness();
+        harness.observe(weights::WeightEvent::Provisioned(assignment));
+
+        // Drive the same public success facts for every source.
+        for event in successful_load_events() {
+            harness.observe(event);
+        }
+
+        // The system-visible success outcome is WeightsReady.
+        assert!(harness.events().iter().any(|event| {
+            matches!(
+                event,
+                weights::WeightLifecycleEvent::WeightsReady {
+                    run_id: weights::RunId(7),
+                    stage_index: 1,
+                }
+            )
+        }));
+    }
+}
+
+// This proves WeightsReady requires artifact availability, layer validation,
+// and worker bind/load completion, and that WeightsReady precedes StageReady.
+#[test]
+fn weights_ready_requires_all_weight_facts_and_precedes_stage_ready() {
+    // Start from a valid assignment.
+    let mut harness = new_weight_harness();
+    harness.observe(weights::WeightEvent::Provisioned(valid_assignment()));
+
+    // Feed every success fact except the final one and prove no prefix is
+    // sufficient for WeightsReady.
+    let mut events = successful_load_events();
+    let final_event = events.pop().expect("fixture has final weight event");
+    for event in events {
+        harness.observe(event);
+        assert!(!harness.events().iter().any(|event| {
+            matches!(event, weights::WeightLifecycleEvent::WeightsReady { .. })
+        }));
+    }
+
+    // The final weight prerequisite emits WeightsReady.
+    harness.observe(final_event);
+    let weights_ready_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, weights::WeightLifecycleEvent::WeightsReady { .. }))
+        .expect("WeightsReady must be emitted");
+
+    // StageReady may occur only after the StageController observes WeightsReady
+    // and the other local setup prerequisites.
+    harness.observe(weights::WeightEvent::OtherStagePrerequisitesReady);
+    let stage_ready_pos = harness
+        .events()
+        .iter()
+        .position(|event| matches!(event, weights::WeightLifecycleEvent::StageReady { .. }))
+        .expect("StageReady must be emitted after prerequisites");
+    assert!(weights_ready_pos < stage_ready_pos);
+}
+
+// This proves every weight failure source faults the stage and suppresses both
+// WeightsReady and StageReady.
+#[test]
+fn weight_failures_emit_stage_fault_without_readiness() {
+    // Each failure source gets an isolated attempt.
+    for (failure_event, expected_reason) in failure_cases() {
+        let mut harness = new_weight_harness();
+        harness.observe(weights::WeightEvent::Provisioned(valid_assignment()));
+
+        // Deliver the public failure outcome from weight work.
+        harness.observe(failure_event);
+
+        // The stable fault reason must be observable.
+        assert!(harness.events().iter().any(|event| {
+            matches!(
+                event,
+                weights::WeightLifecycleEvent::StageFault {
+                    reason,
+                    ..
+                } if *reason == expected_reason
+            )
+        }));
+
+        // Readiness cannot also be emitted after a faulted weight attempt.
+        assert!(!harness.events().iter().any(|event| {
+            matches!(event, weights::WeightLifecycleEvent::WeightsReady { .. })
+                || matches!(event, weights::WeightLifecycleEvent::StageReady { .. })
+        }));
+    }
+}