| 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 (no example) |
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. For a cast to usize, such as (-1i64) as usize, the program stops at that cast. |
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. (no example) |
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. (no example) |
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. (no example) |
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. (no example) |
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. (no example) |
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. (no example) |
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). (no example) |
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). |
W1035 | A match arm in a loop or while can take Cancelled from a wait and stays in the loop. In a cancelled task each wait gives Cancelled at once, so the loop never ends (F4). |
W1036 | A drop calls send or recv, which wait with no time limit of their own, outside the body of a call of within. A drop runs with cancellation off, so when the other end never acts, the wait holds up the drop until the limit of the drop: its type's wait_limit, 10 seconds by default. Then the wait gives up, as in a cancelled block. A wait_limit that calls them gets the warning too, because it runs before the drop and should only return a time. |
| 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 (no example) |
E3006 | Type mismatch in logical operation (no example) |
E3007 | If branch type mismatch |
E3008 | Enum payload type mismatch (no example) |
E3009 | Enum payload arity mismatch (no example) |
E3010 | Function argument count mismatch |
E3011 | Unsupported cast (no example) |
E3012 | Type mismatch in struct field initialization (no example) |
E3013 | Missing struct field in initialization (no example) |
E3014 | Range type mismatch (no example) |
E3015 | Trait not implemented (no example) |
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 (no example) |
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 Pinned or Ref tensor. A payload tensor is stored as its memref descriptor. Its drop frees a tensor in a memory space through the plugin that the memory's type names. Pinned and Ref give the location outside the tensor type, so the drop does not know it, and such a payload is refused. |
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. (no example) |
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. (no example) |
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 consts. A const table holds a list of number literals, and is read one number at a time, as TABLE[i]. |
E3045 | An integer literal that does not fit its type, such as 300 for a u8. A usize 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. Also a loop over &mut t: the loop gives copies of the elements, so it cannot change them. |
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 of another type than the value matched: a variant of another enum, such as Other::Red in a match on a Color, true in a match on an i32, or 1 in a match on a bool. Write a pattern of the matched value's type. |
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, Sync or Owned, or of no trait at all. Only those three 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 break or continue that leaves a task, a return with a value in a task that has no handle, or a task that joins another task. A return in a task ends the task, and its value is the result of the task. 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. |
E3060 | A task that can fail, used in a way that could lose its failure. A task whose body gives Result<T, E> can fail, and its join() gives the T. When the task failed, the join leaves the tasks block, and the block gives the Err. So the task needs a handle, let h = spawn { .. };, and a join in its own block that always runs after the spawn. The block must give a Result<U, E> with the same E. |
E3061 | An impl of a trait does not write a method that the trait requires: one the trait declares with no default body. A call to that method would otherwise fail where it is called, with "method not found", though the fault is in the impl. |
E3062 | A struct literal that writes its fields in an order other than the struct's declaration. The fields run in the order the source writes them, so P { y : f(), x : g() } would run f before g and store y before x. Write the fields in the order the struct declares them. |
E3063 | A ? that cannot pass its error up. x? takes a Result<T, E>. It gives the T of an Ok, and it passes an Err up unchanged: to the function, which must return a Result<_, E> with the same E, to its closure, which must return one, or to its task or tasks block, which must give one. A ? in a closure needs the closure's type written, |x| -> Result<T, E> { .. }. ? does not convert the error. .map_err(..) converts it. |
E3064 | A break or continue with no loop around it in its own function or closure. A closure body is not inside a loop around the closure, because the closure can run after the loop ends. |
| 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. A closure cannot return a reference to its own parameter, or to the copy it keeps of a variable it uses (|| &x): each call has its own frame. |
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. A match on a reference names parts of the value behind it, so match r { Holder::Full(n) => n } cannot move n either. Through a raw pointer, let b = *p; and let b = p[i]; are refused when the value has something to drop, since its owner drops it too. Only an unsafe fn such as core::ptr::read(p) may take it out. |
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] }), passed to a function that takes the tensor by value (f(q[i])), or returned from a function that returns a tensor by value (return 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(), take the parameter by reference, or return a reference (-> &mut Tensor<..>). |
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();. A return, break or continue that leaves two tasks blocks waits only for the tasks of the inner one, so it cannot drop a value from outside the inner block yet. |
E4015 | A spawn region that moves a value from the code around it: let x = t; or f(t) with a parameter that takes t by value, where t is declared before the region. The region only borrows what it uses, and the function drops t after the region. Borrow it (&t), or clone it (t.clone()). |
E4016 | A borrow clause that is not well formed, or one that the body does not keep. In ensures !points_into(return, *p) the result cannot point into the memory under *p, and in ensures !reaches(return, *p) it also cannot point where a reference in *p points. In ensures !keeps(p) the body stores p, or a reference read through it, nowhere that outlives the call. p is a reference parameter. Each borrow clause is an ensures of its own. |
| 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. A move of a tensor reads no element, so a let, an argument, a store or a return of it is allowed. |
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. (no example) |
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. (no example) |
E6035 | A Memory declaration's within: names a space that is not built in, and that the program and its machine files do not declare. A typo in the name is the usual cause. |
E6036 | A token of transfer_async that the program drops with no .wait(): at the end of its scope, or when an assignment gives its variable a new value. The copy may not be done then, so its target may not hold the data. Call .wait(), which gives the placed tensor. |
E6037 | A placement whose memory is not built in and has no scope:. Such a memory has no address space on the target. Declare the memory with scope: device, sm, cta or thread. |
E6038 | A spawn on body for a device that uses a channel end, a lock, or a value that holds one. The standard library marks these types with the trait HostOnly. A wait on the device for the host can wait forever, because a GPU does not promise that its threads make progress. Send or receive before the spawn on, or after it. A spawn on(Topology::CPU) body runs on the host, so it can use them. |
E6039 | A spawn in a loop of its tasks block, with a count of passes that is not known at compile time, and tasks that use a memory with a capacity. Each pass starts a task, and the tasks run at the same time, so their working set has no bound. Use a for loop over a constant range, or join each task in its pass. Downgraded to W1028 when the space is declared overcommit. |
E6040 | A channel of tensors in a memory with a capacity, with a room that is not known at compile time. The channel can hold that many tensors at once, so the working set has no bound. Downgraded to W1028 when the space is declared overcommit. |
E6041 | A function that makes a channel of tensors in a memory with a capacity, and returns an end of that channel. The room of the channel is counted in the function that calls channel, only until that function returns. |
| 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, a reads_only(t) whose body may write t, or a writes_only() whose body may write memory |
E8008 | A loop invariant that the prover cannot show to hold when the loop starts |
E8009 | A loop invariant that the prover cannot show to hold in the next pass, after the loop body or after a continue |
E8010 | An mlir! block whose dialects list does not match its body: the body uses an operation of a dialect that the list does not name, or the list names something that is not a dialect. The list is what the block says it uses, so it must be right. |
E8011 | A pointer clause that is not well formed: valid(p, n), initialized(p, n) or !overlaps(p, q, n), where p and q are raw pointer parameters, and each clause is a requires or an ensures of its own. In an ensures, return can be the pointer. The fact of an assume is one such clause. A call through a function value or a trait would not prove a requires, so a safe function with one cannot be a function value, and a safe method of a trait impl cannot have one. A frees clause is an ensures of its own, ensures frees(p) or ensures !frees(p) for a parameter p, and a method of a trait impl cannot add a !frees that the trait method does not have. An extern function can also ensure a clause about numbers that names only its integer parameters and return. |
E8012 | A body that breaks a pointer ensures of its function. The facts at a return, or at the end of the body, do not prove a clause such as ensures valid(return, n). Or the body changes a parameter that such a clause names. Or the function says ensures !frees(p), and its body gives p, or a value that it gets from p, to code that can free memory, such as a call without !frees for that parameter, a store or an mlir! block. |
E8013 | A type invariant that is not well formed. An invariant of a struct can use self, the fields of self at any depth, numbers, operators and the pointer clauses valid, initialized and overlaps. It calls no other function. |
E8014 | Code outside the module of a type with an invariant changes a field of the type. Only the module (the .vx file) that declares the type can write a field, take a &mut to a field, call a method that takes &mut self on a field, move a field out of the value, or build the type with a struct literal. Other code calls a function of the module to change a value of the type. Then the invariant holds for each value of the type outside its module. |