Diagnostic index

Every diagnostic the Vx compiler can emit, with the code it reports and what it means.

Codes are grouped by the compilation stage that raises them, and the group is readable off the number: E1xxx is the parser, E3xxx the type checker, E6xxx the placement and capacity rules, and so on. A W prefix is a warning rather than an error.

This file is generated from src/diagnostic.rs by scripts/tools/gen_error_index.py. Edit the doc comments on the codes there, not this file.

Every code below links to its own page, which carries the message the compiler emits and, where the test suite has one, a program that triggers it.

Warnings — W1001–W1034 (25 codes)
Parser Errors — E1001–E1013 (13 codes)
Name Resolution Errors — E2001–E2007 (7 codes)
Type Errors — E3001–E3059 (58 codes)
Borrow/Ownership Errors — E4001–E4014 (14 codes)
Safety Errors — E5001–E5002 (2 codes)
Topology/Hardware Errors — E6001–E6034 (34 codes)
Tensor/Math Errors — E7001–E7004 (4 codes)
Contract/Verification Errors — E8001–E8007 (7 codes)

Warnings

Reported without stopping the compile. A warning means the program is accepted but something in it is probably not what was intended.

Code	Meaning
`W1001`	Unused variable binding
`W1002`	A function in the program’s own file that nothing calls, directly or through other functions, starting from `main`.
`W1003`	Unreachable code after return, break, or continue
`W1004`	`let mut x` where `x` never changes: it is never assigned, never borrowed `&mut`, and no method that changes it is called on it. The `mut` can go.
`W1005`	A `let` that reuses a name already declared in the same block, so the first value can no longer be named.
`W1006`	`&&x`, a borrow of a borrow, where `&x` was probably meant.
`W1007`	An `as` cast that widens, such as `x as i64` when `x` is an `i32`. It cannot lose a value, and `i64::from(x)` says so.
`W1008`	A match arm whose body is empty, such as `1 => {}`.
`W1009`	Unused function parameter
`W1010`	An `unsafe` block with nothing inside it that needs `unsafe`.
`W1013`	An `as` cast to the type the value already has, such as `x as i32` when `x` is an `i32`.
`W1014`	An `as` cast of a number known while compiling that does not fit the target type, such as `100000 as i8`, which gives -96.
`W1020`	`*&x`, a borrow that is dereferenced at once. It is the same as `x`.
`W1022`	A `transfer` into the memory the value is already in. It only makes a copy.
`W1023`	`spawn on(Topology::Current)`: the region runs where the code around it already runs.
`W1024`	Implicit cross-topology transfer inserted via a `Relocatable` impl (a real data movement happens silently at the use site; write the transfer explicitly to silence). `Relocatable` answers “may this value move implicitly?” and is keyed on a user type. That is a different question from “what code moves bytes across this hardware edge?”, which is `impl Transfer<Memory::A, Memory::B> for Topology::X`. Both were called `Transfer` before Vx#353.
`W1025`	Use of a user-defined topology with no registered descriptor (not declared via `Topology <Name> { ... }` and not registered by a plugin). Often a typo of a built-in; defaults to host-like placement.
`W1026`	A user-defined topology’s memory is unreachable from the host (no transfer path), so data can never be moved to it. See the topology coherence check.
`W1027`	A declared `relaxed` transfer edge does not preserve visibility (the seam engine shows a consumer may read stale data). See the topology coherence check.
`W1028`	The working set of a memory space exceeds `capacity`, but the space is declared `overcommit`, so the cumulative-budget errors (E6010, and the cross-call E6027/E6028) are downgraded to this warning.
`W1029`	A tensor placed in a memory space that declares a `capacity` has a dynamic (non- literal) shape, so the capacity check (E6009/E6010) could not run — the placement is unverified. Silence by making the shape static, or bounding it. Emitted only when the destination space actually declares a capacity.
`W1030`	A topology’s device index is not a compile-time constant (`GPU[i]` for a runtime `i`), so it cannot be resolved to a device instance and falls back to index 0. Every such spawn therefore targets the same device. Vx models one representative device per declared kind (#284), so a fleet program should index with constants or const generics.
`W1031`	A proof obligation could not be discharged because no SMT solver was available, so the property is unverified rather than proved. Distinct from W1027, which means the solver ran and found a violation. Emitted only under `VX_ALLOW_UNVERIFIED`; without it a missing solver is an error, because silence used to be indistinguishable from success (Vx#374).
`W1033`	The loop of a `spawn` region runs on one thread although each pass writes only memory of its own, so its passes could run at the same time. The warning points at what stops it: a call the compiler cannot show writes nothing, inline MLIR, a read of a row another pass writes, bounds not known when compiling, and the like. A region that calls `barrier()` asks for blocks and threads, so it is warned about whenever it runs on one thread, with the first thing that stopped the split: two threads that may write the same element, a `break` out of a loop that holds a `barrier()`, a write to block-shared memory with no `barrier()` after it, and the like.
`W1034`	The program writes a variable that a closure copied, and uses the closure after the write. The closure keeps the value that it copied, so it does not see the write. A later release makes this an error (K4).

Parser Errors

Raised while turning source text into an AST. The program is not syntactically valid Vx.

Code	Meaning
`E1001`	Unexpected token
`E1002`	Unexpected end of file
`E1003`	Expected identifier
`E1004`	Expected type
`E1005`	Expected expression
`E1006`	Unclosed delimiter (paren/brace/bracket)
`E1007`	Missing semicolon
`E1008`	Missing comma
`E1009`	Invalid operator
`E1010`	Unknown topology variant
`E1011`	Unknown memory space
`E1012`	Unknown element type
`E1013`	Invalid macro invocation syntax

Name Resolution Errors

Raised when a name cannot be resolved to a declaration, or resolves to something of the wrong kind.

Code	Meaning
`E2001`	Undefined variable
`E2002`	Undefined function
`E2003`	Unknown enum
`E2004`	Unknown enum variant
`E2005`	Unknown struct field
`E2006`	Module does not export function
`E2007`	Method not found on type

Type Errors

Raised by the type checker. Vx performs no implicit numeric conversion, so many of these are mismatches that a language with coercion would have silently accepted.

Code	Meaning
`E3001`	Type mismatch in variable declaration
`E3002`	Type mismatch in return
`E3003`	Type mismatch in function argument
`E3004`	Type mismatch in binary operation
`E3005`	Type mismatch in relational operation
`E3006`	Type mismatch in logical operation
`E3007`	If branch type mismatch
`E3008`	Enum payload type mismatch
`E3009`	Enum payload arity mismatch
`E3010`	Function argument count mismatch
`E3011`	Unsupported cast
`E3012`	Type mismatch in struct field initialization
`E3013`	Missing struct field in initialization
`E3014`	Range type mismatch
`E3015`	Trait not implemented
`E3016`	A generic call that leaves one of the callee’s type parameters unbound: no argument fixes it, and no type declared for the result does either. Left alone, the parameter travelled into the instance’s symbol name as its bare letter and `sizeof<T>()` folded to 8, so a buffer was sized for an element type that was never chosen. Spell the type argument out, as `Vec<i32>::new()`, or give the result a type, as `let v : Vec<i32> = Vec::new();`.
`E3017`	Closure argument count or type mismatch
`E3018`	An array literal whose elements are not scalars, are not all of one type, or which is empty. A number literal takes the type of the other elements; a typed value needs `as`. An array literal lowers to `tensor.from_elements`, whose element type must be a scalar, so `[a, b]` for tensors – placed or not – has nothing to lower to, and an empty literal has no element type to give it. Both used to be accepted by the checker (the element type silently stayed at its `f32` default) and then crash codegen with an internal error rather than a diagnostic. See Vx#354.
`E3019`	A `match` arm whose integer literal cannot be represented in the scrutinee’s type. The arm can never be selected, so the program does not mean what it says. Codegen used to parse the literal with a zero fallback, which turned an unrepresentable arm into a comparison against 0 – so the arm fired for scrutinee 0, the most common value there is, with no diagnostic.
`E3036`	A static call to a method several traits supply, where no impl takes the argument types written. Reported instead of an ambiguity (E3035), because ambiguity is not what went wrong: the call named one thing and the arguments ruled every candidate out. The message lists the impls that do exist, which is the edit.
`E3020`	A `match` that no arm is guaranteed to match. A match over an enum must name every variant or carry a wildcard arm, wherever it sits. The uncovered value falls through, and when every written arm returns, the function falls off its end and hands back whatever was in the return slot. A scrutinee that is not an enum cannot be enumerated, so it is only asked for a wildcard in value position, where the fall-through edge would otherwise have no value to carry – codegen used to paper over that by evaluating the whole match to a constant zero.
`E3021`	An enum variant whose payload is a tensor. A payload is stored into the variant’s tagged-union slot with `llvm.insertvalue`, which takes primitive operands, and a tensor is a memref descriptor. The AST path dropped such a payload silently: the construction emitted the tag and nothing else, so a program carrying a tensor through an enum compiled, ran, and lost it with no diagnostic. A struct field holding a tensor is the same representational gap in another position.
`E3022`	An `extern` function whose signature mentions a tensor. A tensor is a memref, and lowering expands a memref parameter into the seven scalars of its descriptor – allocated pointer, aligned pointer, offset, and a size and stride per rank. So `fn c_take(t : Tensor<f32, [?, ?]>) -> i32` declares a C symbol taking seven arguments, which is not a signature anyone writes on the C side; the call links by name and passes something the callee never agreed to. Take a raw pointer and build the tensor in Vx (`Tensor<f32, [?, ?]>::from_ptr_2d`), which is what the corpus already does.
`E3023`	A shaped tensor initialized from a scalar. `let a : Tensor<f32, [128, 64]> = 1.0` allocated and filled a whole buffer from something that reads as an assignment, and the two codegen paths disagreed about it: the AST path emitted the allocation and a `linalg.fill`, the flat path kept the bare constant and handed an `f32` to a call expecting a memref. `Tensor<T, [..]>::fill(v)` is the spelling. The rank-0 wrap (`Tensor<f32, []> = 1.0`) is a different thing and stays legal.
`E3024`	`.shape[i]` on a tensor. It answered on any value, not only a tensor, and typed its answer as a rank-0 tensor. `extent(i)` is the read of a run-time extent.
`E3025`	`extent(i)` with an index that is not a literal below the tensor’s rank. Rank is static, so the index is checked here rather than read past the descriptor at run time.
`E3026`	A placement query (`.topology()`) the checker cannot decide. Placement is a fact of the receiver’s type, compared with `Some(Topology::..)` or `None`; it has no run-time value.
`E3028`	A function with a non-void return type whose body can complete without returning. Reported here rather than left to codegen, where it surfaced as an MLIR verifier message naming an operation, with no source location.
`E3029`	A type name in a signature that names no declaration. An unknown name in type position parses as a user nominal, so without this a typo – or a type constructor removed from the language – compiled silently and did nothing.
`E3030`	An operator applied to operand types it is not defined on – `%` on a shaped tensor or on a `bool`. Refused here because the alternative is worse in both directions: the flat emitter would decline and fall back to a path that cannot lower it either, and an `i1` operand would reach `arith.remsi` and verify.
`E3031`	`impl Copy for X` where one of `X`’s fields is a type that moves. `Copy` promises a value survives being assigned elsewhere, and a field that does not survive it breaks that promise for the whole type – which would be a way to duplicate a tensor, or any other placed value, without saying so.
`E3032`	A chain of generic instantiations that does not end – `f<N - 1>()` whose base case is never reached. Reported here rather than left to run out of stack, which gave no file, no line and no message.
`E3033`	A `comptime` block the evaluator could not finish. The block runs during compilation and leaves nothing behind, so one that cannot be run has no meaning – and used to be emitted as ordinary run-time code, which hid the fact entirely.
`E3034`	A `comptime` block inside another one. The outer block already runs at compile time, so the inner one asks for nothing extra, and nesting them is what made a block’s value depend on evaluating a closure defined inside another block.
`E3035`	A method name that more than one `impl` block defines for the same type. The impls are kept in a hash map, so which body a call reached used to change from one run of the compiler to the next; refusing the call is the only answer that is the same twice. Naming the trait, as in `Display::fmt(&x, f)`, chooses one impl.
`E3037`	An impl of a trait that declares an associated type does not bind it. The trait’s signatures are written against `Self::Item`, so with no binding there is nothing to put in their place, and the method’s type becomes whatever the impl happened to write.
`E3038`	`type Item = ..` in an impl whose trait declares no `Item`. Usually a misspelling: nothing reads the binding, so it would go on meaning nothing, in silence.
`E3039`	`I::Item` disagrees with the impl for what `I` is: an argument bound it to one type and that impl binds `Item` to another.
`E3040`	`I::Item` where no impl for what `I` is binds an associated type named `Item`: `I` has no such bound, or the name is misspelled.
`E3041`	A struct field that names `I::Item`. Fields are laid out from the struct’s parameters alone, so the projection is made a parameter instead, as `Map<I, F>` does with its closure.
`E3042`	A bound on a type parameter, `T : Name`, where no trait called `Name` is declared or imported. Usually a misspelling or a missing `import`.
`E3043`	A `for` loop over a reference to a type with no method to iterate it by. The loop calls `iter()` for `for x in &c` and `iter_mut()` for `for x in &mut c`, as Rust’s collections do, so the type needs the one the loop asks for.
`E3044`	A top-level `const` whose value is not known while compiling, or does not fit its declared type. A `const` holds a number or a `bool`: a literal, or arithmetic on literals and other `const`s. A `const` table holds a list of number literals, and is read one number at a time, as `TABLE[i]`.
`E3045`	A number literal that does not fit `usize`, which holds 0 up to the largest `i64`.
`E3046`	A `for` loop over a tensor that is not a variable or a flat array literal, such as one a function call returns, or a nested array literal. The loop reads the tensor by index, so it needs a name: bind the tensor with `let` first.
`E3047`	A `reshape` call the compiler cannot check: the new shape has a different number of elements than the tensor (without `PadMode::Pad` or `PadMode::Trim`), a size is not known while compiling, or the arguments are not a shape such as `[4, 4]` and an optional `PadMode`.
`E3048`	An `if` with no `else` whose value is used, as in `let u = if c { .. };`. When the condition is false there is no branch to give a value. Add an `else`, or use the `if` as a statement.
`E3049`	Two impls of the same trait for the same type: `impl Describe for Point` written twice, in one module or in two. A type has one impl of a trait, so a call could not choose between them. Remove one.
`E3050`	A pattern inside a variant’s payload that is not a name or `_`, such as the `3` in `Val(3)` or the `Inner::A(v)` in `Wrap(Inner::A(v))`. The compiler does not test such a pattern when it chooses an arm, so the arm would be taken for any payload. Bind the payload to a name and test it in the arm, with an `if` or another `match`.
`E3051`	A `match` pattern that names a variant of another enum than the value matched, such as `Other::Red` in a `match` on a `Color`. Write the variant with the matched value’s enum.
`E3052`	Arithmetic on fp8 or fp4 values (`f8e4m3`, `f8e5m2` or `f4e2m1`) with no written result type, as in `print(a * b)`. The compiler computes in f32 and rounds once to the written type, so the program must write it: `let c : f32 = a * b;`. Also `+=` and the other compound operators on these values, and any operator on tensors of them.
`E3053`	An impl of `Send` or `Sync` with no `unsafe`, as in `impl Send for Handle {}`. The compiler derives both from the fields, and a raw pointer is neither. An impl claims one for a type that holds a raw pointer, and the compiler cannot check the claim. Write `unsafe impl Send for Handle {}`.
`E3054`	`unsafe impl` of a trait other than `Send` or `Sync`, or of no trait at all. Only those two traits make a claim that the compiler cannot check. Remove `unsafe`.
`E3055`	A task takes a value that is not `Send`, or reads a variable whose type is not `Sync`. A task that moves a value, copies it or writes it needs `Send`. A task that reads a variable in place shares it with the code around the task, so it needs `Sync`. The error names the field that makes the type fail.
`E3056`	`spawn { .. }` outside a `tasks { .. }` block. The end of the `tasks` block waits for each task, so a task cannot outlive the variables it uses. A `spawn` in a closure, or directly in another task, is outside the block too. Put the `spawn` in a `tasks` block of its own.
`E3057`	A task handle used in a way other than `h.join()`, or a `spawn` that is not the value of a `let` or a statement of its own. A task must not leave its `tasks` block, so the program cannot return a handle, store it, or pass it to a function. Write `let h = spawn { .. };` and later `h.join()`.
`E3058`	A `return`, `break` or `continue` that leaves a task, or a task that joins another task. The last expression of a task body is its result. A task cannot join another task yet. Join both tasks in the `tasks` block.
`E3059`	An `extern` declaration of `malloc`, `calloc`, `realloc`, `aligned_alloc` or `free` whose type is not C’s. The compiler calls these functions too, and it can share only a declaration of C’s type. A size is a 64-bit integer: `usize`, `i64` or `u64`. A pointer is a raw pointer to host memory. `free` returns nothing.

Borrow/Ownership Errors

Raised by the borrow checker and the linear-type rules. These rule out use-after-move, aliasing violations and lifetimes that outlive what they point at.

Code	Meaning
`E4001`	Use of moved or consumed linear variable
`E4002`	Cannot access mutably borrowed variable
`E4003`	Cannot borrow as mutable (already immutably borrowed)
`E4004`	Cannot borrow (already mutably borrowed)
`E4005`	A value that points into this function’s stack frame would outlive the function: a reference to a local, or a closure that uses one, returned (on its own or inside a struct), stored through a reference, or passed to a call that could store it there. What it points at is gone once the function returns. The same holds inside a function for a block: a variable declared outside a block cannot be given a value that points at a variable declared inside it. Nor can a variable keep a reference into a value with no name, such as `make_vec()` in `let r = &make_vec();`, when that value is dropped at the end of its statement.
`E4006`	An assignment through a shared reference: `*r = v`, `r.f = v` or `r[i] = v` where `r` is a `&T`. A shared reference only reads; writing needs a `&mut T`.
`E4007`	A value moved while a borrow of it is still used afterwards: `let r = &a; let b = a;` followed by a use of `r`. The borrow would point at a value that has moved away.
`E4008`	A value moved out from behind a reference: `let b = *r;` where `r` is a reference to a type that is not `Copy`. The reference does not own the value, so it cannot give it away; copy or clone it instead.
`E4009`	An assignment to a variable, or a field or element of it, while a `&` borrow of it is still used afterwards: `let r = &x; x = 2;` and then a use of `r`. The borrow would see the value change under it.
`E4010`	A change to a variable declared without `mut`: assigning it, or a field or element of it, borrowing it `&mut`, or calling a method that takes `&mut self` on it. Declare it `let mut x`, or for a parameter `mut x : T`.
`E4011`	A view of a tensor (a row `q[i]` or a field `h.t`) used where a tensor of its own is held: stored in a variable that already exists (`t = q[i]`) or a struct field (`h.t = q[i]`, `Holder { t : q[i] }`), or passed to a function that takes the tensor by value (`f(q[i])`). A view shares its owner’s memory and is not a copy. Bind it to a new variable with `let`, pass `q[i].clone()`, or take the parameter by reference.
`E4012`	A call to the `drop` method of a `Drop` impl by hand: `x.drop()`. `drop` runs when the value is dropped, so calling it as well would run it twice. Write `drop(x)`, from `core::mem`, to drop a value early.
`E4013`	A field moved out of a value that must keep it: `let x = p.a` where `p`’s type implements `Drop`, whose `drop` needs every field, or `let x = make().a`, where the value has no name and drops all its fields at the end of the statement. Borrow the field (`&p.a`), clone it, or bind the value to a variable first.
`E4014`	A task that can still run when a variable that it uses ends or changes. A task in a loop that the same pass does not join runs at the same time as the next pass, so it must not write a variable from outside the loop, or read one that the loop writes. A task must not use a variable that ends before its `tasks` block, such as one of the loop body. Join the task in the same block: `let h = spawn { .. };` and then `h.join();`.

Safety Errors

Raised where an operation needs an unsafe context and does not have one.

Code	Meaning
`E5001`	Unsafe function call outside unsafe block. `Tensor<..>::uninit()` is one: its elements hold whatever the memory held, so the program says with `unsafe` that it writes each one before reading it.
`E5002`	Unsafe memory operation outside unsafe block

Topology/Hardware Errors

Raised by the placement and capacity rules — the checks that make Vx different from a single-address-space language. A value in the wrong memory space, a region on the wrong device, a working set that does not fit, or a transfer with no declared route.

Code	Meaning
`E6001`	Topology mismatch in function call
`E6002`	Cannot transfer between memory spaces (no hardware path)
`E6003`	A value is used from a topology that cannot see the memory space it lives in. The diagnostic names the value’s space, the visible set of the topology reading it, and the cost of the transfer that would fix it – so a misplaced handoff (an un-transferred KV cache in a disaggregated prefill/decode split, say) is a compile error that carries its own remedy. A `managed: cached` space the topology can reach across a declared seam is coherent in hardware and is not reported here.
`E6004`	Transfer violates the boundary contract at a seam (per-seam local-completeness / soundness obligation is `sat`; a stale read can violate the contract).
`E6005`	A user-defined topology declaration is incoherent: it cannot see its own default memory space (`default_space ∉ visibility`). See the topology coherence check.
`E6006`	A `Memory` declaration’s `within:` hierarchy forms a cycle (a space contains itself).
`E6007`	A `Memory` sub-space’s `capacity` exceeds its parent’s capacity (a child cannot be larger than what contains it).
`E6008`	A `Memory` declaration has a non-positive `capacity`, `bandwidth`, or `granule`.
`E6009`	A statically-shaped tensor placed in a memory space exceeds that space’s `capacity`.
`E6010`	The working set placed in a memory space (the sum of its tiles) exceeds `capacity`. Downgraded to W1028 when the space is declared `overcommit`.
`E6011`	A sub-space’s `scope` is broader than its parent’s (locality must narrow down `within:`).
`E6012`	The same `Memory` or `Topology` name is declared by two compilation inputs (e.g. a `--machine` file and the program). Declarations are name-keyed, so one would silently shadow the other and the machine model in force would depend on load order (#281).
`E6013`	A declared `transfer` edge carries an explicit cost and has one derivable from its endpoints’ `bandwidth:` figures. An edge gets exactly one cost source, because two answers to “what does this hop cost” is not a model: the compiler routed by the declared number and reported the derived one, and nothing detected the disagreement.
`E6014`	A program stages through host memory while a machine model is in force, and no host was declared. `--machine` describes an accelerator and says nothing about the machine it hangs off, so the host end of that seam was being reasoned about without anything describing it. `--host <file>` names one; `--host default` names the machine compiling the program. A host declares no capacity – host memory is virtual, and a hard limit would reject programs that page rather than fail – so this is about the host being stated rather than assumed, not about a budget.
`E6015`	A structurally invalid transfer lowering (`impl transfer A -> B { ... }`): the same edge implemented twice in one compilation (which one is in force would be load order), or a lowering with no functions (an empty body cannot move anything, and accepting it would make `impl transfer` an inert annotation rather than code).
`E6016`	A `Topology` or `Memory` declaration whose identity cannot be relied on. Two forms: the declared name shadows a built-in topology (every use of `Topology::<Name>` resolves to the built-in, so the declaration is silently ignored – including its `arch:`); or two declared names collide on one dispatch id (custom ids are derived from the name by hashing), in which case which declaration is in force would be hash-iteration order – observed as the same program getting a device image on some runs and not others for a topology, and as a `transfer` carrying the other space’s capacity and granule for a memory space.
`E6017`	A misuse of the `raw::` transfer-lowering primitives (Vx#353): a `raw::` call outside an `impl transfer` body, an unknown primitive name, a tile argument that is not a bare parameter name (the primitives are indexed, not addressed), a store into a tile not held by `&mut`, or a wrongly typed index/value.
`E6018`	A `raw::` bounds obligation (`0 <= index < extent`) that could not be proven. Prove it with a loop bound or invariant the SMT prover can see, or assert it in an `unsafe` block – which records the obligation as asserted-not-proven, the same standing an unverified `spec:` figure has.
`E6019`	`raw::barrier()` anywhere but a top-level statement of the lowering body. The barrier’s contract requires every lane to reach it; under a conditional or a loop that cannot be guaranteed syntactically, so it is rejected outright (conservative by design – restructure the body so the barrier is unconditional).
`E6020`	`raw::async_copy` in a lowering for an edge no declared topology equips with a copy engine. The capability lives in the machine file (`transfer A -> B copy_engine`); using an absent primitive is a compile error, not a fallback.
`E6021`	A violation of the async/synchronization discipline in a lowering body: a destination read while an `async_copy` into it is still outstanding, a body that ends with copies no `async_wait` covers, or a lowering for a synchronizing edge whose body does not end with `raw::barrier()` (the seam obligation of `hir/seam.rs`: a relaxed publication makes a stale read reachable).
`E6022`	An `impl transfer` lowering whose edge endpoints are not visible to a topology that declares the edge – the lowering would execute on a part that cannot address the spaces it moves bytes between, which the transfer contract’s space-visibility constraint forbids.
`E6023`	An `impl transfer` lowering whose declared tile shape is not the shape the transfer at hand actually moves. A lowering is selected by edge, so nothing else relates the two, and the `raw::` primitives take their extents from the declaration: a smaller declaration copies part of the tile and leaves the rest uninitialised, a larger one stores past the end (observed as a SIGSEGV).
`E6024`	A proof obligation could not be discharged because no SMT solver was available. Fails the compilation by default: an undischarged obligation is not a proved one, and treating the two alike is what let a missing z3 certify every seam in silence (Vx#374). Set `VX_ALLOW_UNVERIFIED=1` to downgrade this to W1031 and compile anyway.
`E6025`	A placement naming a location the machine does not have: a memory space no declared topology holds, written either as the space or as the device that would hold it. The derivation between the two spellings has a like-named fallback, so an undeclared name resolves to a space that exists only in the placement that mentions it.
`E6026`	A tensor whose element type the target hardware cannot represent, placed on it anyway. The machine model states what a device has (`dtypes: [f32, f16, ...]`); this is the check that a placement stays inside it. An H100 has no fp4, so an fp4 tensor placed on one asks for silicon that is not there – and the placement is in the type, so the question is answerable here rather than at a kernel launch on the machine that lacks the type. Only fires against a topology that declares `dtypes:`. An undeclared machine constrains nothing, which is what keeps every machine file written before the field kept working.
`E6027`	A working set that overflows a space only across call boundaries: the peak along some call path – what each caller still holds when it calls, plus the deepest callee’s own peak – exceeds the space’s declared capacity, while every function on the path fits by itself (that case is E6010’s). Computed by folding per-function capacity summaries over the call graph, after the per-function checks. Downgraded to W1028 when the space is declared `overcommit`.
`E6028`	A recursive cycle that places tiles in a space with a declared capacity. The recursion depth is not known at compile time, so the true peak is unbounded and the placement is refused conservatively. Downgraded to W1028 when the space is declared `overcommit`.
`E6029`	A pointer argument into one memory passed to a parameter that wants a pointer into another: a host `mut f32` where `mut f32 in Memory::GPU_HBM` is declared, or the reverse. The two are different types, and the C library or kernel behind the parameter reads the memory the declaration names, so the spaces must match exactly.
`E6030`	A `spawn` region on a device hands out a tensor it makes, which the host could not free. The compiler makes such a tensor before the region instead, in the device’s memory, when the region hands it out as a variable created with `Tensor<..>(..)`, `::new()` or `unsafe { ..::uninit() }`, with no type annotation, a size that uses nothing the region computes, and a name nothing outside the region already uses.
`E6031`	A tensor shape that folds to a negative extent, or whose size is more than 2^63 - 1 bytes, the most an allocation can ask for. The size is known, and it is not one the generated code can allocate: it would wrap.
`E6032`	An `across` loop that the topology or its place cannot have: a topology with no `levels:` or one whose arch cannot launch them (without `-fauto-schedule-levels`), a level the topology does not name, a loop outside a `spawn on` region or in the wrong order, a size that is not known when the kernel is compiled or is over the limit, or a jump out of the loop. Also a lane reduction (`lanes::sum` and the others) outside the code of a loop of blocks or subgroups, or with a tensor that is too large.
`E6033`	An index into a tensor in a `scope: thread` space that is not known when compiling. Such a tensor stays in registers, and a register has no address. So each index must be a constant, or made of constants and the variables of `for` loops with constant bounds, at most 1024 passes each. The code generator unrolls those loops.
`E6034`	An `aligned(N)` in a tensor type that the compiler cannot give: the space is not one whose storage the compiler lays out (`scope: sm`, `cta` or `thread`), or N is less than the `alignment:` of the space, which every tensor there has.

Tensor/Math Errors

Raised on tensor shapes and numeric operations, including shape mismatches that are decided at compile time.

Code	Meaning
`E7001`	Matmul dimension mismatch
`E7002`	Matmul element type mismatch
`E7003`	Reshape arithmetic mismatch
`E7004`	Non-differentiable return type (autodiff)

Contract/Verification Errors

Raised when a requires, ensures or invariant clause cannot be discharged, or when a seam obligation is left unproven.

Code	Meaning
`E8001`	Cannot prove postcondition
`E8002`	Comptime assert failed
`E8003`	Compile-time index out of range
`E8004`	Compile-time evaluation exceeded the call-depth limit
`E8005`	Compile-time evaluation ran more loop iterations than the budget allows. A loop whose end condition is never reached is the usual cause; without this it hung the compiler.
`E8006`	A call does not meet the called function’s precondition (`requires`)
`E8007`	An access clause that does not hold: an `atomic(t)` whose body uses `t` without an atomic operation, or a `writes_only()` whose body may write memory

164 diagnostics.

The Vx Book