diff --git a/dag/extdeps/systems/types.dag b/dag/extdeps/systems/types.dag
index 93bece90d35..4bbad8a5190 100644
--- a/dag/extdeps/systems/types.dag
+++ b/dag/extdeps/systems/types.dag
@@ -1,7 +1,7 @@
 module extdeps.systems.types
 
 import v2.std.algebra { filter }
-import std.types { NonEmptyStr, List, Int, Bool }
+import std.types { NonEmptyStr, List, Int, Bool, String }
 import std.measure { ByteSize, Bandwidth, Watt, BitWidth, Hertz, HardwareThreadCount, hardware_thread_count_value, byte_size, byte_size_count, Millimeter, Celsius, watt, watt_count, Volt }
 import std.nat { Nat }
 import extdeps.storage.types { PcieLink }
@@ -112,6 +112,79 @@ fn coherent_superchip_coherent_capacity(row: CoherentSuperchipCatalogRow) -> Byt
   byte_size(count: byte_size_count(b: row.gpu.memory.capacity) + byte_size_count(b: row.cpu_memory.memory.capacity))
 }
 
+// ── A SYSTEM'S MEMORY COMPONENTS, ADDRESSABLE ────────────────────────────────────────────────────
+//
+// The rows above carry each memory's FACTS but give no way to name "this memory of this system", so
+// a consumer that places bytes on one memory and not another had nothing to point at. These are
+// derived projections over the existing fields and add no figures. A component's identity is the
+// system's own catalog name plus how its GPU reaches that memory.
+//
+// Addressability is a physical fact about the package, not a deployment choice:
+// - the integrated SoC's one pool serves CPU and GPU alike;
+// - a superchip's GPU memory is reached directly;
+// - its CPU memory is reached across the coherent chip-to-chip link at that link's per-direction
+//   rate.
+// A new system shape adds its own projection here. No generic enum of memories grows an arm.
+type GpuMemoryAddressability
+  = GpuAndCpuShareOnePool
+  | GpuAddressesDirectly
+  | GpuAddressesAcrossCoherentLink { per_direction: Bandwidth }
+
+// SEALED: the row-shape projections below are the only constructors, so a component always carries
+// facts copied from a catalog row and never hand-assembled ones.
+type SystemMemoryComponent sole_constructor {
+  system: NonEmptyStr
+  memory: MemoryFacts
+  addressability: GpuMemoryAddressability
+}
+
+fn integrated_system_unified_memory(row: IntegratedComputeSystemCatalogRow) -> SystemMemoryComponent {
+  SystemMemoryComponent { system: row.soc_model, memory: row.memory, addressability: GpuAndCpuShareOnePool }
+}
+
+fn integrated_system_memory_components(row: IntegratedComputeSystemCatalogRow) -> List<SystemMemoryComponent> {
+  [integrated_system_unified_memory(row: row)]
+}
+
+fn coherent_superchip_memory_components(row: CoherentSuperchipCatalogRow) -> List<SystemMemoryComponent> {
+  [
+    SystemMemoryComponent { system: row.model, memory: row.gpu.memory, addressability: GpuAddressesDirectly },
+    SystemMemoryComponent {
+      system: row.model,
+      memory: row.cpu_memory.memory,
+      addressability: GpuAddressesAcrossCoherentLink { per_direction: row.chip_to_chip_bandwidth_per_direction },
+    },
+  ]
+}
+
+fn gpu_memory_addressability_wire(a: GpuMemoryAddressability) -> NonEmptyStr {
+  match a {
+    GpuAndCpuShareOnePool => "unified" as NonEmptyStr
+    GpuAddressesDirectly => "gpu-local" as NonEmptyStr
+    GpuAddressesAcrossCoherentLink { per_direction: _ } => "across-coherent-link" as NonEmptyStr
+  }
+}
+
+// IDENTITY IS THE WHOLE FACT, not a name:
+// - the system;
+// - the memory's capacity and kind;
+// - the complete addressability, including a coherent link's rate.
+// Equality on the two coproducts is the derived structural equality (DESIGN §4: operations come
+// from inhabitance), so a new arm needs no table here.
+// Two components agree only when every fact agrees. A row edited to different memory, or to a
+// different link rate, under the same system name projects a component that is NOT the original's,
+// so a tier join can never alias them.
+fn system_memory_component_same(a: SystemMemoryComponent, b: SystemMemoryComponent) -> Bool {
+  (a.system as String) == (b.system as String)
+    && byte_size_count(b: a.memory.capacity) == byte_size_count(b: b.memory.capacity)
+    && a.memory.memory_kind == b.memory.memory_kind
+    && a.addressability == b.addressability
+}
+
+fn system_memory_component_wire(c: SystemMemoryComponent) -> NonEmptyStr {
+  join([c.system as String, "/", gpu_memory_addressability_wire(a: c.addressability) as String], "") as NonEmptyStr
+}
+
 // ── COMPLETE SUPERCHIP SERVERS ───────────────────────────────────────────────────────────────
 //
 // A COMPLETE SERVER IS THE THIRD SHAPE, beside the sealed integrated system and the bare superchip: an
diff --git a/dag/extdeps/vllm/weight_offload.dag b/dag/extdeps/vllm/weight_offload.dag
new file mode 100644
index 00000000000..b16b28188c3
--- /dev/null
+++ b/dag/extdeps/vllm/weight_offload.dag
@@ -0,0 +1,207 @@
+module extdeps.vllm.weight_offload
+
+import std.types { String, NonEmptyStr, Bool, List }
+import v2.std.optional { Present, Absent }
+import std.nat { Nat }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef }
+import extdeps.uri { Uri, Https }
+import extdeps.vllm.runtime_defaults { defaults_source_revision, Vllm8d09804 }
+
+// The revision is read from its one minting row rather than re-spelled here (extdeps.vllm.environment
+// does the same).
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: join(["github.com/vllm-project/vllm/blob/", defaults_source_revision(r: Vllm8d09804).full_revision as String, "/vllm/model_executor/offloader"], "")
+  }
+}
+
+data extdeps_model_scope: ExternalModelScope = ExternalModelScope {
+  subject: ExternalSubjectRef {
+    declaration: DeclarationRef {
+      module_path: "extdeps.vllm.weight_offload",
+      decl_name: "VllmWeightOffloadSplitLaw",
+      field: WholeDeclaration
+    }
+  },
+  first_citation: extdeps_external_authority_anchor,
+  further_citations: []
+}
+
+// ── HOW THE ENGINE SPLITS A CHECKPOINT BETWEEN DEVICE AND HOST MEMORY ───────────────────────────
+//
+// vLLM's weight offloaders (vllm.config.offload OffloadConfig, chosen by
+// vllm.model_executor.offloader.base create_offloader) move whole named PARAMETERS. They never move
+// part of a tensor. The wrap is in vllm.model_executor.models.utils make_layers, so only the
+// decoder-layer stack is eligible, and the unit of a split is one parameter of one layer. On a
+// FusedMoE model all routed experts of a layer are one tensor per projection, so a layer's whole
+// expert store moves or stays together.
+//
+// A CONFIGURED BACKEND IS NOT A REALIZATION. What the device actually holds depends on facts the
+// configuration does not fix, so the law is minted only from a reading of them:
+//
+// - UVA (UVAOffloader). It hands kernels a device view of pinned host memory ONLY when
+//   uva_offloading = is_uva_available() and not VLLM_WEIGHT_OFFLOADING_DISABLE_UVA.
+//   Otherwise it falls back to plain CPU parameters. Each offloaded module's forward then moves its
+//   whole state_dict to the device with .to(device) and runs functional_call, so one module's
+//   offloaded parameters are device-resident while it runs.
+// - The zero-copy view also survives loading only if the FP8 MoE backend leaves the weights in
+//   place. convert_to_fp8_moe_kernel_format allocates NEW tensors for the relayout arms, and
+//   replace_parameter re-registers them on the device, which undoes the offload with no warning.
+// - Prefetch (PrefetchOffloader) keeps the host copy and, in post_init, a StaticBufferPool with
+//   slot_capacity = prefetch_step. So the device holds prefetch_step copies of each distinct
+//   offloaded parameter. It re-reads CPU storage after loading (sync_cpu_storage), so a relayout
+//   backend does not undo it. OffloadConfig.validate_offload_config refuses an enabled prefetch with
+//   offload_prefetch_step below one.
+
+// THE FP8 MoE BACKENDS AT THE PINNED REVISION (vllm.model_executor.layers.fused_moe.oracle.fp8
+// Fp8MoeBackend), each with what convert_to_fp8_moe_kernel_format does to its weights. A backend
+// added upstream has no row here, so it cannot be read as preserving.
+type VllmFp8MoeBackend
+  = Fp8MoeTriton
+  | Fp8MoeBatchedTriton
+  | Fp8MoeVllmCutlass
+  | Fp8MoeBatchedVllmCutlass
+  | Fp8MoeHpc
+  | Fp8MoeEmulation
+  | Fp8MoeTritonMxfp8
+  | Fp8MoeDeepGemm
+  | Fp8MoeBatchedDeepGemm
+  | Fp8MoeFlashInferCutlass
+  | Fp8MoeFlashInferTrtllm
+  | Fp8MoeMarlin
+  | Fp8MoeAiter
+  | Fp8MoeAiterMxfp8
+  | Fp8MoeHumming
+  | Fp8MoeXpu
+  | Fp8MoeCpu
+
+// True for the arms that allocate new weight tensors after loading:
+// - prepare_fp8_moe_layer_for_deepgemm
+// - prepare_fp8_moe_layer_for_fi
+// - the marlin preparers
+// - rocm_aiter_ops shuffles
+// - convert_to_humming_moe_kernel_format
+// - prepare_fp8_moe_layer_for_xpu / _for_cpu
+// False for the arms the converter returns unchanged (TRITON, BATCHED_TRITON, VLLM_CUTLASS,
+// BATCHED_VLLM_CUTLASS, HPC, EMULATION, TRITON_MXFP8).
+fn vllm_fp8_moe_backend_relays_out_weights(b: VllmFp8MoeBackend) -> Bool {
+  match b {
+    Fp8MoeTriton => false
+    Fp8MoeBatchedTriton => false
+    Fp8MoeVllmCutlass => false
+    Fp8MoeBatchedVllmCutlass => false
+    Fp8MoeHpc => false
+    Fp8MoeEmulation => false
+    Fp8MoeTritonMxfp8 => false
+    Fp8MoeDeepGemm => true
+    Fp8MoeBatchedDeepGemm => true
+    Fp8MoeFlashInferCutlass => true
+    Fp8MoeFlashInferTrtllm => true
+    Fp8MoeMarlin => true
+    Fp8MoeAiter => true
+    Fp8MoeAiterMxfp8 => true
+    Fp8MoeHumming => true
+    Fp8MoeXpu => true
+    Fp8MoeCpu => true
+  }
+}
+
+// THE PREFETCH STEP IS POSITIVE BY CONSTRUCTION: the only constructor is the refusing mint below.
+type VllmPrefetchStep sole_constructor {
+  count: Nat
+}
+
+type VllmPrefetchStepMint
+  = VllmPrefetchStepAdmitted { step: VllmPrefetchStep }
+  | VllmPrefetchStepRefused { cause: NonEmptyStr }
+
+fn vllm_prefetch_step(count: Nat) -> VllmPrefetchStepMint {
+  if count == 0 {
+    VllmPrefetchStepRefused { cause: "offload_prefetch_step must be at least one when prefetch offloading is enabled (vllm.config.offload OffloadConfig.validate_offload_config refuses it)" as NonEmptyStr }
+  } else {
+    VllmPrefetchStepAdmitted { step: VllmPrefetchStep { count: count } }
+  }
+}
+
+// WHAT A UVA LAUNCH MUST READ. An unread fact is Absent, never a default. The readings come from the
+// host and the engine's own log; this row only names them.
+type VllmUvaOffloadReading {
+  uva_available: Bool?
+  disable_uva_env_set: Bool?
+  realized_moe_backend: VllmFp8MoeBackend?
+}
+
+type VllmWeightOffloadBackend
+  = VllmUvaOffload { reading: VllmUvaOffloadReading }
+  | VllmPrefetchOffload { step: VllmPrefetchStep }
+
+// THE REALIZATION THE READING ESTABLISHES, and the device copies each keeps per distinct offloaded
+// parameter. The functional_call fallback's copy is transient: one module's parameters are moved in
+// while it runs, then released to the caching allocator. The device still has to hold that layer's
+// bytes, which is the cost.
+type VllmWeightOffloadRealization
+  = UvaZeroCopyView
+  | UvaFunctionalCallFallback
+  | PrefetchStaticBuffers { step: VllmPrefetchStep }
+
+type VllmWeightOffloadSplitLaw sole_constructor {
+  realization: VllmWeightOffloadRealization
+  device_copies_per_offloaded_parameter: Nat
+}
+
+// THREE STANDINGS:
+// - Established carries a law only a reading can mint.
+// - Unestablished names each fact still unread.
+// - Refused is a reading under which no split exists: a relayout backend re-materialises every
+//   offloaded store on the device.
+type VllmWeightOffloadSplitStanding
+  = WeightOffloadSplitEstablished { law: VllmWeightOffloadSplitLaw }
+  | WeightOffloadSplitUnestablished { obligations: List<NonEmptyStr> }
+  | WeightOffloadSplitRefused { cause: NonEmptyStr }
+
+fn unread_obligation(present: Bool, what: String) -> List<NonEmptyStr> {
+  if present { [] as List<NonEmptyStr> } else { [join(["unread: ", what], "") as NonEmptyStr] }
+}
+
+fn vllm_uva_split_standing(r: VllmUvaOffloadReading) -> VllmWeightOffloadSplitStanding {
+  let available_read = match r.uva_available { Present { value: _ } => true Absent => false }
+  let disable_read = match r.disable_uva_env_set { Present { value: _ } => true Absent => false }
+  let backend_read = match r.realized_moe_backend { Present { value: _ } => true Absent => false }
+  let obligations = concat(
+    unread_obligation(present: available_read, what: "is_uva_available() on the serving host (pinned memory available)"),
+    concat(
+      unread_obligation(present: disable_read, what: "whether VLLM_WEIGHT_OFFLOADING_DISABLE_UVA is set in the engine environment"),
+      unread_obligation(present: backend_read, what: "the FP8 MoE backend the engine selected (its logged Fp8MoeBackend)")))
+  if count(obligations) > 0 {
+    WeightOffloadSplitUnestablished { obligations: obligations }
+  } else {
+    let zero_copy = (match r.uva_available { Present { value: v } => v Absent => false })
+      && !(match r.disable_uva_env_set { Present { value: v } => v Absent => true })
+    let relays_out = match r.realized_moe_backend { Present { value: b } => vllm_fp8_moe_backend_relays_out_weights(b: b) Absent => true }
+    if relays_out {
+      WeightOffloadSplitRefused { cause: "the engine selected an FP8 MoE backend whose load-time conversion allocates new weight tensors on the device (convert_to_fp8_moe_kernel_format), so every offloaded expert store is re-materialised there and no device/host split exists" as NonEmptyStr }
+    } else if zero_copy {
+      WeightOffloadSplitEstablished { law: VllmWeightOffloadSplitLaw { realization: UvaZeroCopyView, device_copies_per_offloaded_parameter: 0 } }
+    } else {
+      WeightOffloadSplitEstablished { law: VllmWeightOffloadSplitLaw { realization: UvaFunctionalCallFallback, device_copies_per_offloaded_parameter: 1 } }
+    }
+  }
+}
+
+fn vllm_weight_offload_split_standing(backend: VllmWeightOffloadBackend) -> VllmWeightOffloadSplitStanding {
+  match backend {
+    VllmUvaOffload { reading: r } => vllm_uva_split_standing(r: r)
+    VllmPrefetchOffload { step: s } =>
+      WeightOffloadSplitEstablished { law: VllmWeightOffloadSplitLaw { realization: PrefetchStaticBuffers { step: s }, device_copies_per_offloaded_parameter: s.count } }
+  }
+}
+
+fn vllm_weight_offload_realization_wire(r: VllmWeightOffloadRealization) -> NonEmptyStr {
+  match r {
+    UvaZeroCopyView => "uva-zero-copy" as NonEmptyStr
+    UvaFunctionalCallFallback => "uva-functional-call-fallback" as NonEmptyStr
+    PrefetchStaticBuffers { step: _ } => "prefetch" as NonEmptyStr
+  }
+}
diff --git a/dag/test/claim/system_memory_component_witness_test.dag b/dag/test/claim/system_memory_component_witness_test.dag
new file mode 100644
index 00000000000..733bfe2706c
--- /dev/null
+++ b/dag/test/claim/system_memory_component_witness_test.dag
@@ -0,0 +1,114 @@
+module test.claim.system_memory_component_witness
+
+import std.types { Bool, List }
+import std.nat { Nat }
+import v2.std.algebra { filter }
+import v2.std.optional { Present, Absent }
+import std.measure { bandwidth, gibibyte, gibibyte_to_byte_size }
+import extdeps.memory.types { MemoryFacts, Hbm }
+import extdeps.gpu.types { GpuModelCatalogRow }
+import extdeps.systems.types {
+  CoherentSuperchipCatalogRow, CoherentMemoryTier, SystemMemoryComponent,
+  GpuAndCpuShareOnePool, GpuAddressesDirectly, GpuAddressesAcrossCoherentLink,
+  coherent_superchip_memory_components, integrated_system_memory_components, system_memory_component_same,
+}
+import extdeps.systems.nvidia { nvidia_dgx_spark_1tb_catalog, nvidia_dgx_spark_4tb_catalog }
+import extdeps.systems.nvidia_gh200 { nvidia_gh200_480gb_catalog }
+
+// THE IDENTITY UNDER TEST is extdeps.systems.types system_memory_component_same, over components
+// that only the row projections can construct. The aliasing reds edit a CATALOG ROW, which is a
+// public record. That is the one route by which same-system, same-arm components with different
+// facts could reach a tier join. Each edit must project a component that is not the original's.
+
+fn gh200_components(row: CoherentSuperchipCatalogRow) -> List<SystemMemoryComponent> {
+  coherent_superchip_memory_components(row: row)
+}
+
+// The component reached a given way, or Absent. Claims require Present, so a missing component can
+// never satisfy a "does not alias" red by default.
+fn reached(xs: List<SystemMemoryComponent>, link: Bool) -> SystemMemoryComponent? {
+  first(filter(xs, c => match c.addressability {
+    GpuAddressesAcrossCoherentLink { per_direction: _ } => link
+    GpuAddressesDirectly => !link
+    GpuAndCpuShareOnePool => !link
+  }))
+}
+
+fn both_present_and(a: SystemMemoryComponent?, b: SystemMemoryComponent?, same_expected: Bool) -> Bool {
+  match a {
+    Absent => false
+    Present { value: x } =>
+      match b {
+        Absent => false
+        Present { value: y } => system_memory_component_same(a: x, b: y) == same_expected
+      }
+  }
+}
+
+data larger_hbm_gpu: GpuModelCatalogRow = GpuModelCatalogRow {
+  vendor: nvidia_gh200_480gb_catalog.gpu.vendor,
+  model: nvidia_gh200_480gb_catalog.gpu.model,
+  microarchitecture: nvidia_gh200_480gb_catalog.gpu.microarchitecture,
+  execution_lane_count: nvidia_gh200_480gb_catalog.gpu.execution_lane_count,
+  memory: MemoryFacts { capacity: gibibyte_to_byte_size(g: gibibyte(count: 144)), memory_kind: Hbm },
+  memory_bandwidth: nvidia_gh200_480gb_catalog.gpu.memory_bandwidth,
+  boost_clock: nvidia_gh200_480gb_catalog.gpu.boost_clock,
+  tdp_watts: nvidia_gh200_480gb_catalog.gpu.tdp_watts,
+  compute_capability: nvidia_gh200_480gb_catalog.gpu.compute_capability,
+  supported_runtimes: nvidia_gh200_480gb_catalog.gpu.supported_runtimes,
+  interconnect: nvidia_gh200_480gb_catalog.gpu.interconnect,
+  sm_cache: nvidia_gh200_480gb_catalog.gpu.sm_cache,
+  sm_cache_citations: nvidia_gh200_480gb_catalog.gpu.sm_cache_citations,
+}
+
+fn edited_row(gpu: GpuModelCatalogRow, link_rate_bytes_per_second: Nat) -> CoherentSuperchipCatalogRow {
+  CoherentSuperchipCatalogRow {
+    vendor: nvidia_gh200_480gb_catalog.vendor,
+    model: nvidia_gh200_480gb_catalog.model,
+    board_designation: nvidia_gh200_480gb_catalog.board_designation,
+    cpu_architecture: nvidia_gh200_480gb_catalog.cpu_architecture,
+    cpu_core_clusters: nvidia_gh200_480gb_catalog.cpu_core_clusters,
+    gpu: gpu,
+    cpu_memory: nvidia_gh200_480gb_catalog.cpu_memory,
+    chip_to_chip_bandwidth_per_direction: bandwidth(count: link_rate_bytes_per_second),
+    module_power_floor: nvidia_gh200_480gb_catalog.module_power_floor,
+    module_power_ceiling: nvidia_gh200_480gb_catalog.module_power_ceiling,
+    figure_standing: nvidia_gh200_480gb_catalog.figure_standing,
+  }
+}
+
+// Positive control: the same row projected twice names the same components, and its two memories
+// are distinct.
+test fn w_a_row_projects_one_identity_per_memory() -> Bool {
+  let a = gh200_components(row: nvidia_gh200_480gb_catalog)
+  let b = gh200_components(row: nvidia_gh200_480gb_catalog)
+  count(a) == 2
+    && both_present_and(a: reached(xs: a, link: false), b: reached(xs: b, link: false), same_expected: true)
+    && both_present_and(a: reached(xs: a, link: true), b: reached(xs: b, link: true), same_expected: true)
+    && both_present_and(a: reached(xs: a, link: false), b: reached(xs: a, link: true), same_expected: false)
+}
+
+// RED: same system, same arm, different memory. A GPU-local component whose capacity differs is
+// not the original's.
+test fn w_same_system_and_arm_with_different_memory_does_not_alias() -> Bool {
+  both_present_and(
+    a: reached(xs: gh200_components(row: nvidia_gh200_480gb_catalog), link: false),
+    b: reached(xs: gh200_components(row: edited_row(gpu: larger_hbm_gpu, link_rate_bytes_per_second: 450000000000)), link: false),
+    same_expected: false)
+}
+
+// RED: same system, same coherent-link arm, different link rate. The link components do not alias.
+test fn w_same_system_and_link_arm_with_a_different_rate_does_not_alias() -> Bool {
+  both_present_and(
+    a: reached(xs: gh200_components(row: nvidia_gh200_480gb_catalog), link: true),
+    b: reached(xs: gh200_components(row: edited_row(gpu: nvidia_gh200_480gb_catalog.gpu, link_rate_bytes_per_second: 900000000000)), link: true),
+    same_expected: false)
+}
+
+// The two DGX Spark SKUs differ only in storage, so their one memory is one identity.
+test fn w_spark_skus_share_their_one_memory_identity() -> Bool {
+  both_present_and(
+    a: reached(xs: integrated_system_memory_components(row: nvidia_dgx_spark_1tb_catalog), link: false),
+    b: reached(xs: integrated_system_memory_components(row: nvidia_dgx_spark_4tb_catalog), link: false),
+    same_expected: true)
+}
diff --git a/dag/test/claim/vllm_weight_offload_witness_test.dag b/dag/test/claim/vllm_weight_offload_witness_test.dag
new file mode 100644
index 00000000000..68e4fd461b6
--- /dev/null
+++ b/dag/test/claim/vllm_weight_offload_witness_test.dag
@@ -0,0 +1,109 @@
+module test.claim.vllm_weight_offload_witness
+
+import std.types { Bool, NonEmptyStr }
+import std.nat { Nat }
+import v2.std.optional { Present, Absent }
+import extdeps.vllm.weight_offload {
+  VllmFp8MoeBackend, Fp8MoeTriton, Fp8MoeDeepGemm, Fp8MoeMarlin,
+  VllmUvaOffloadReading, VllmUvaOffload, VllmPrefetchOffload,
+  VllmPrefetchStepAdmitted, VllmPrefetchStepRefused, vllm_prefetch_step,
+  VllmWeightOffloadSplitStanding, WeightOffloadSplitEstablished, WeightOffloadSplitUnestablished, WeightOffloadSplitRefused,
+  UvaZeroCopyView, UvaFunctionalCallFallback, PrefetchStaticBuffers,
+  vllm_weight_offload_split_standing,
+}
+
+fn uva(available: Bool?, disabled: Bool?, backend: VllmFp8MoeBackend?) -> VllmWeightOffloadSplitStanding {
+  vllm_weight_offload_split_standing(backend: VllmUvaOffload { reading: VllmUvaOffloadReading {
+    uva_available: available, disable_uva_env_set: disabled, realized_moe_backend: backend,
+  } })
+}
+
+fn is_zero_copy(s: VllmWeightOffloadSplitStanding) -> Bool {
+  match s {
+    WeightOffloadSplitEstablished { law: l } =>
+      l.device_copies_per_offloaded_parameter == 0 && match l.realization {
+        UvaZeroCopyView => true
+        UvaFunctionalCallFallback => false
+        PrefetchStaticBuffers { step: _ } => false
+      }
+    WeightOffloadSplitUnestablished { obligations: _ } => false
+    WeightOffloadSplitRefused { cause: _ } => false
+  }
+}
+
+fn is_fallback(s: VllmWeightOffloadSplitStanding) -> Bool {
+  match s {
+    WeightOffloadSplitEstablished { law: l } =>
+      l.device_copies_per_offloaded_parameter == 1 && match l.realization {
+        UvaZeroCopyView => false
+        UvaFunctionalCallFallback => true
+        PrefetchStaticBuffers { step: _ } => false
+      }
+    WeightOffloadSplitUnestablished { obligations: _ } => false
+    WeightOffloadSplitRefused { cause: _ } => false
+  }
+}
+
+fn is_refused(s: VllmWeightOffloadSplitStanding) -> Bool {
+  match s {
+    WeightOffloadSplitRefused { cause: _ } => true
+    WeightOffloadSplitEstablished { law: _ } => false
+    WeightOffloadSplitUnestablished { obligations: _ } => false
+  }
+}
+
+fn unestablished_count(s: VllmWeightOffloadSplitStanding) -> Nat {
+  match s {
+    WeightOffloadSplitUnestablished { obligations: os } => count(os)
+    WeightOffloadSplitEstablished { law: _ } => 0
+    WeightOffloadSplitRefused { cause: _ } => 0
+  }
+}
+
+// Positive control: every fact read, UVA live, an in-place backend. This is the only zero-copy route.
+test fn w_read_uva_with_an_in_place_backend_is_the_zero_copy_law() -> Bool {
+  is_zero_copy(s: uva(available: Present { value: true }, disabled: Present { value: false }, backend: Present { value: Fp8MoeTriton }))
+}
+
+// RED: UVA unavailable on the host. The engine falls back to functional_call and materialises one
+// module's offloaded parameters on the device. That is not zero-copy.
+test fn w_uva_unavailable_is_the_device_materialising_fallback() -> Bool {
+  let s = uva(available: Present { value: false }, disabled: Present { value: false }, backend: Present { value: Fp8MoeTriton })
+  is_fallback(s: s) && !is_zero_copy(s: s)
+}
+
+// RED: VLLM_WEIGHT_OFFLOADING_DISABLE_UVA set. Same fallback.
+test fn w_uva_disabled_by_env_is_the_device_materialising_fallback() -> Bool {
+  let s = uva(available: Present { value: true }, disabled: Present { value: true }, backend: Present { value: Fp8MoeTriton })
+  is_fallback(s: s) && !is_zero_copy(s: s)
+}
+
+// RED: a relayout backend allocates device tensors after loading, so no split exists.
+test fn w_a_relayout_moe_backend_refuses_the_split() -> Bool {
+  is_refused(s: uva(available: Present { value: true }, disabled: Present { value: false }, backend: Present { value: Fp8MoeDeepGemm }))
+    && is_refused(s: uva(available: Present { value: true }, disabled: Present { value: false }, backend: Present { value: Fp8MoeMarlin }))
+}
+
+// RED: an unread fact is unestablished, and each unread fact is named once.
+test fn w_unread_facts_leave_the_split_unestablished() -> Bool {
+  unestablished_count(s: uva(available: Absent, disabled: Absent, backend: Absent)) == 3
+    && unestablished_count(s: uva(available: Present { value: true }, disabled: Present { value: false }, backend: Absent)) == 1
+    && !is_zero_copy(s: uva(available: Present { value: true }, disabled: Absent, backend: Present { value: Fp8MoeTriton }))
+}
+
+// RED: an enabled prefetch with step zero has no constructor. Step two keeps two device copies.
+test fn w_prefetch_step_is_positive_and_prices_its_device_copies() -> Bool {
+  (match vllm_prefetch_step(count: 0) {
+    VllmPrefetchStepRefused { cause: _ } => true
+    VllmPrefetchStepAdmitted { step: _ } => false
+  })
+    && (match vllm_prefetch_step(count: 2) {
+      VllmPrefetchStepAdmitted { step: st } =>
+        match vllm_weight_offload_split_standing(backend: VllmPrefetchOffload { step: st }) {
+          WeightOffloadSplitEstablished { law: l } => l.device_copies_per_offloaded_parameter == 2
+          WeightOffloadSplitUnestablished { obligations: _ } => false
+          WeightOffloadSplitRefused { cause: _ } => false
+        }
+      VllmPrefetchStepRefused { cause: _ } => false
+    })
+}