semantics.md

Vx Operational Semantics & Memory Model

This document specifies the runtime evaluation, spatial computing execution model, and memory rules of the Vx language.

1. Spatial Computing Model

Vx does not assume a single, flat instruction stream executing on a monolithic CPU. The language intrinsically models distributed, heterogeneous topologies (e.g., CPU, GPU, NPU, AccCore).

1.1 The spawn on(Topology) Operation

The spawn on(Topology) expression transitions the execution context from the current hardware unit to the specified hardware topology.

Operational Rule: Let $E[ \text{spawn on}(\tau) { B } ]$ be a program state evaluated on an active hardware unit $\rho$.

1. The runtime checks if the topology $\tau$ is reachable from $\rho$.
2. The runtime reserves resources on $\tau$.
3. The block $B$ runs on $\tau$ and produces a value $v$.
4. The spawning unit $\rho$ continues with $v$, which lives on $\tau$ (type Pinned<T, τ>). Everything after the spawn observes $B$ as complete. The runtime may overlap $B$ with later work on $\rho$ as long as $\rho$ cannot tell the difference; see ../spawn_on.md.
5. All variables captured within $B$ that are not in a shared or transferred memory space relative to $\tau$ will result in a compiler error.
6. Index scope rule: If $\tau$ contains an index expression (e.g., NPU[i] or NPU[0..4]), the index expression is evaluated in the calling scope $\rho$, not in $\tau$. This ensures loop variables and other outer-scope identifiers are accessible.

1.2 The unroll across(Topology) Operation

unroll across is a spatial loop parallelizer. It takes a physical or logical topology slice (e.g., Topology::NPU[0..4]) and spatially duplicates the inner block $B$.

Operational Rule: unroll across(Topology::Unit[A..B]) { |id| B } evaluates to parallel spawn on instances: spawn on(Topology::Unit[A]) { let id = A; B } || ... || spawn on(Topology::Unit[B-1]) { let id = B-1; B }.

---

2. Memory Model & Transfers

Standard languages employ a flat memory model (*mut T). Vx uses a partitioned address space memory model: a value's memory space is part of its type. For a tensor that is the placement slot, Tensor<f32, [4, 4], Memory::CPU_DRAM>, which may equally be written as the device that holds the space, Topology::NPU[0]. Ref<T, MemorySpace> says the same thing for values that are not tensors.

2.1 Spatial Isolation

If variable $v$ is of type Tensor<f32, [4, 4], Memory::CPU_DRAM> and execution context is Topology::NPU[0], attempting to dereference $v$ triggers a spatial fault (caught statically at compile-time by the Semantic Analyzer).

2.2 The transfer Primitive

Data movement across distinct memory hierarchies is explicit. let local_data = transfer(host_data, Memory::NPUHBM);

Operational Rule:

1. Given source reference $S$ residing in space $M_1$.
2. Evaluates to a target reference $T$ in space $M_2$.
3. The runtime schedules an asynchronous or synchronous DMA transfer from $M_1$ to $M_2$.
4. Linearity: If $S$ represents uniquely owned data, the transfer consumes $S$. Future use of $S$ in space $M_1$ is invalid.

2.3 Declared Memory Spaces & Sub-space Scheduling

A Memory declaration gives a space real semantics beyond a bare name — its place in the hierarchy, its size, and how it is allocated:

Memory SMEM {
  within:    Memory::GPU_HBM,   // containment: SMEM ⊂ GPU_HBM
  capacity:  228 KB,            // the space is bounded
  bandwidth: 128 B/cyc,         // feeds the roofline transfer cost
  granule:   16 KB,             // allocation granularity (a TMEM/SMEM sub-scratchpad)
  scope:     sm,                // the execution level the space is private to
}

Placement checking. A statically-shaped tensor placed into a space (by transfer) must fit:

• Per-tile (E6009): a single tile larger than capacity is rejected.
• Cumulative (E6010): the working set — the sum over all tiles placed in the space — must fit capacity. When the space declares a granule, each tile is rounded up to the granule first (a tile smaller than a granule still occupies a whole one), so the quantity checked is the granule-rounded working set. Declaring the space overcommit downgrades E6010 to a warning (W1028): the programmer asserts the tiles do not all coexist.
• Coherence: within: forms a containment tree; a sub-space may not exceed its parent's capacity (E6007) nor widen its scope below the parent (E6011); a within: cycle is rejected (E6006).

Sub-space reachability. A sub-space (SMEM/TMEM) has no hardware transfer edges of its own; a transfer into or between sub-spaces is reachable through their enclosing spaces — each endpoint is resolved to itself-or-a-within:-ancestor, and a sibling→sibling move (e.g. TMEM→SMEM) meets at their nearest common ancestor and is costed on both legs. A value already resident in a sub-space is recognized as starting there when re-transferred.

Sub-space scheduling. For a space with a granule, the compiler assigns each placed tile a concrete position via a granule-rounded bump allocator — a byte offset and a slots (granule) count within the space — and preserves the full sub-space descriptor together with this assignment as metadata on the IR (vx.transfer).

Design choices (why it takes this shape):

• Metadata, not the memref type. The sub-space identity and schedule ride as op-attributes, not as a memref memory-space / address space. This keeps the description available to later passes and a device backend with zero effect on the lowering — a typed memory space would break the CPU-fallback address computation. Promoting the identity into the memref type is deferred to a real device backend.
• Scoped to granule'd sub-spaces. Scheduling and granule-rounding apply only to spaces that declare a granule (the sub-scratchpads — TMEM/SMEM); device-global spaces (HBM/DRAM) are unaffected.
• One budget, two granularities. The capacity check and the scheduler share a single notion of the working set; the granule-rounded sum is the allocation-accurate refinement of the raw sum, and overcommit relaxes both.

Which spaces exist at all is decided by the machine and host models a compilation is given: see hosts_and_machines.md. No host is assumed — a program that stages through Memory::CPU_DRAM while a machine model is in force must name one (E6014), because --machine describes an accelerator and says nothing about the machine it hangs off.

---

3. Typestates and Hardware Fallibility

Because computations map to physical hardware, availability is non-deterministic.

3.1 Verified<T> vs Pinned<T, Topology>

• Verified<T>: A lazily evaluated computation graph. The compiler has verified memory and type safety, but the physical location is deferred to the runtime cost model.
• Pinned<T, Topology>: An eagerly bound computation locked to a specific physical unit.

3.2 Monadic Transitions (HardwareState)

The transition Verified<T> -> try_pin(T) -> HardwareState<Pinned<T>, Verified<T>> acts as a failible monad. The runtime attempts to acquire the lock on the Topology. If successful, it returns Available(Pinned), else Saturated(Verified).

---

4. Compile-Time Evaluation (comptime)

Vx supports deterministic ahead-of-time evaluation via comptime blocks.

• Execution within a comptime block happens during the Semantic Analysis compiler pass.
• Operations inside comptime are guaranteed to have zero runtime overhead.
• Used predominantly for layout calculation, array sizing, and topological assertion (assert(...)).
• An assert over a placement query (x.topology() == Some(Topology::T), see the type system document) is decided by the checker: a true one is removed, a false one fails the compile (E8002).

Operational Rule: If $E[\text{comptime} { B }]$ evaluates to $v$, the AST is strictly replaced by the literal or reduced expression $v$ before lowering to the intermediate representation (MLIR).

A block in statement position produces no value and is removed outright. Neither back end ever sees a comptime block, because the replacement happens in the checker.

The block must be able to run, and must leave nothing behind. These follow from the rule above rather than adding to it, and each is refused rather than quietly lowered as run-time code, which is what used to happen:

• A block the evaluator cannot finish is an error (E3033). There is no half-running it: a block that was emitted as ordinary code instead is how a loop or a call the evaluator skipped stayed invisible, and a build could pass while proving nothing.
• A block that writes to a variable declared outside it is an error (E3033). The block disappears, so the write would disappear with it.
• A block inside another block is an error (E3034). The outer block already runs while compiling, so the inner one asks for nothing more.
• A block may read a value known only when the program runs, when neither its value nor its effects depend on that value.
• The compiler decides, while compiling, every check that the program makes while it runs: an assert, and an integer / or %. The division stops the program on a divisor of zero, and on the minimum value divided by -1. A check left for run time would never run, because the block disappears.
  • A false assert on a path that always runs is an error (E8002).
  • Any other check that the compiler cannot show to pass is an error (E3033). This is a check that fails on a path that runs only for some run-time values, such as one branch of an if on a run-time value. It is also a check that depends on a run-time value.
• An integer result outside its type has no compile-time value, so a block whose value depends on it is an error (E3033). At run time the program wraps the result and does not stop, so a block whose value does not depend on it still folds.
• The evaluator runs at most 1,000,000 loop iterations in a block, in all, and at most 256 nested calls. More is an error (E8005, E8004).

Comptime lambdas. comptime { .. } is also Vx's block-expression form, so it is how a closure with more than one statement is written. Such a lambda is a function that runs while compiling — nearer C++'s consteval than its constexpr:

• Its body is not folded where the lambda is written. Its parameters have no values yet.
• Every call to it must fold. A call whose arguments are not all known while compiling is an error; there is no falling back to a run-time call, which is where this is stricter than constexpr.
• Once every call has folded, nothing refers to the lambda, so its binding and its generated body are both dropped and it leaves no trace. A lambda nobody calls is an ordinary unused variable.

A closure body starts a fresh compile-time context, so a lambda whose body is a comptime block, written inside another such block, is two functions rather than a nested block.

The lineage is Zig's comptime rather than C++'s constexpr. A constexpr function only may be evaluated while compiling and silently becomes an ordinary call when it cannot be, which is the reason C++ later grew consteval. Vx refuses instead, so a block that did not run while compiling can never be mistaken for one that did.

---

5. Automatic Differentiation

Vx provides semantic primitives for program transformations related to calculus.

• grad(f): Yields a new function $f'$ which computes the gradients of $f$.
• vjp(f): Vector-Jacobian Product. Propagates gradients backwards (Reverse-Mode AD).
• jvp(f): Jacobian-Vector Product. Propagates tangents forwards (Forward-Mode AD).

Operational Rule: When $g = \text{grad}(f)$ is evaluated, the compiler generates an adjoint computation graph for $f$, tracing linear data consumption (as verified by the borrow checker). Linear variables are consumed exactly once in the forward pass and uniquely referenced in the reverse pass.