Vow Error Catalog¶

Every Vow error has a machine-readable error_code in the JSON output. This document lists all error codes, their phase, meaning, an example trigger, and how to fix them.

Compile-Time Errors¶

These appear in the diagnostics array of the build output JSON.

UnterminatedString¶

Phase: Lexer Meaning: A string literal was opened with " but never closed before the end of the file, or the file ends with a \ escape that has nothing to escape (unterminated string escape). An escaped quote ("abc\") does not close the literal.

Wrong:

fn f() -> () [io] {
    print_str("hello);
}

Fix: Close the string with a matching ".

Right:

fn f() -> () [io] {
    print_str("hello");
}

InvalidCharacter¶

Phase: Lexer Meaning: The source contains a character the lexer does not recognize. The message is unexpected character '<c>' and the span covers that one byte. Lexing stops at the first lexical error.

Wrong:

fn f() -> i64 {
    x @ y
}

Fix: Remove the invalid character. Vow has no @ operator.

Right:

fn f(x: i64, y: i64) -> i64 {
    x + y
}

A float literal whose decimal magnitude overflows f64 (parses to infinity) is also an InvalidCharacter error, raised at lex time rather than allowed through to produce an uncompilable C inf token later in the pipeline:

Wrong:

fn f() -> f64 {
    999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999.0
}

Fix: Use a literal whose magnitude is within f64::MAX (~1.7976931348623157e308).

Right:

fn f() -> f64 {
    1000000000000000000000.0
}

InvalidIntSuffix¶

Phase: Lexer Meaning: An integer literal carries a type suffix that names a type Vow does not have.

Wrong:

fn f() -> u64 {
    5usize
}

Output: unknown integer suffix `usize`: Vow has no `usize`/`isize` type (fixed-width only)

Fix: Use a fixed-width suffix. Vow's integer widths are pointer-independent by design (see docs/adr/0001-numeric-tower-narrow-ints.md), so there is no usize or isize; write 5u64 for a machine-word-sized unsigned value and 5i64 for a signed one.

Right:

fn f() -> u64 {
    5u64
}

UnexpectedToken¶

Phase: Parser Meaning: The parser encountered a token it did not expect at that position.

Wrong:

module M 123

Fix: Check the syntax around the reported span. Common causes: missing {, }, (, ), or a keyword in the wrong position.

Right:

module M

fn f() -> i64 {
    123
}

MissingDelimiter¶

Phase: Parser Meaning: A matching delimiter (}, ), ]) is missing.

Wrong:

fn f() -> i64 {
    42

Fix: Add the missing closing delimiter. No compiler emits MissingDelimiter today: an unclosed block at end of file is reported as UnexpectedToken.

Right:

fn f() -> i64 {
    42
}

TypeMismatch¶

Phase: Type Checker Meaning: An expression has a different type than expected, or a qualified enum pattern names an enum other than the scrutinee's enum.

Wrong:

fn f() -> i32 {
    true
}

Output: function body has type 'bool' but declared return type is 'i32'

Fix: Change the expression or declared type to match. For an enum pattern, qualify the variant with the scrutinee's enum name.

Right:

fn f() -> bool {
    true
}

A struct literal must name every declared field. Each omitted field is a TypeMismatch in both compilers, reported once per field in declaration order at the literal's span; a field is never zero-initialised:

Wrong:

struct Pair { a: i64, b: i64 }

fn f() -> Pair {
    Pair { a: 1 }
}

Output: struct `Pair` literal is missing field `b`

Fix: Initialise the field explicitly (Pair { a: 1, b: 0 }).

The drop intrinsic also reports TypeMismatch when it is called with an argument count other than one or with a value that is not a linear owner (drop requires a linear value, found `i64`); see Linear Intrinsics.

A Vec index (v[i], v[i] = val) and the Vec::truncate argument must have exactly the type u64. An index of any other integer type (for example an i64 counter) or of a non-integer type is a TypeMismatch in both compilers:

Wrong:

fn f(v: Vec<i64>, i: i64) -> i64 {
    v[i]
}

Output: index has type `i64` but must be `u64`

Fix: Keep index counters u64 (.len() is already u64), or convert at the index site with as u64 (v[i as u64]). Unsuffixed integer literals coerce to u64 without a cast. String offsets (byte_at, substring, string_substr, string_matches_literal_at) follow the same exact-u64 rule, and push_byte takes exactly u8; see String offsets.

Right:

fn f(v: Vec<i64>, i: u64) -> i64 {
    v[i]
}

Only Vec<T> has an index operator. Indexing any other type (HashMap, BTreeMap, String, Option, ...) is a TypeMismatch whose message begins index operation on non-indexable type and prints the full receiver type (for example HashMap<i64, i64> or String, identically in both compilers); read a map entry with m.get(k) and a string byte with s.byte_at(i).

Vec::new(), HashMap::new(), and BTreeMap::new() take their element, key, and value types from the binding's annotation. A method call on a collection whose type was never annotated is a TypeMismatch in both compilers, one per call:

Wrong:

fn f() -> () {
    let m = HashMap::new();
    m.insert(1, 2);
}

Output: cannot infer the collection type of the receiver ofinsert: annotate its binding with a full type

Fix: Annotate the binding: let m: HashMap<i64, i64> = HashMap::new();.

Right:

fn f() -> () {
    let m: HashMap<i64, i64> = HashMap::new();
    m.insert(1, 2);
}

An undefined name is a TypeMismatch whose message begins undefined variable, in both compilers, and the expression then has an error type so it does not cascade into further type errors. A parameter where clause is name-resolved in a scope holding only its own parameter, so a sibling parameter or result is an undefined name there; the hint says to move such a condition to requires/ensures.

Wrong:

fn ordered(a: i64, b: i64 where b > a) -> i64 {
    b
}

Output: undefined variable `a`, hint a `where` clause can only reference its own parameter `b`; put a condition on several parameters in `requires`

Fix: State the condition in requires: b > a.

Right:

fn ordered(a: i64, b: i64) -> i64 vow {
    requires: b > a
} {
    b
}

LiteralOutOfRange¶

Phase: Type Checker Meaning: An integer literal appears in a typed context (annotated let, function argument, struct field, or const declaration) whose target type cannot hold the literal's value. The check runs after context coercion, so the offending literal is the one written in the source, not a widened intermediate.

Wrong:

let x: u8 = 300;
const NEG: u16 = -1;
let y = 256u8;   // a suffixed literal is checked against its suffix type

Output: literal 300 does not fit in u8 (range 0..=255)

Fix: Use a value within the target type's range, change the target type, or write an explicit narrowing intrinsic (i64_to_u8_try, i64_to_u8_wrap, i64_to_u8_sat) if you intend to convert a wider value at runtime.

Right:

let x: u8 = 255;
const NEG: i16 = -1;
let y = 255u8;

NarrowingCastNotAllowed¶

Phase: Type Checker Meaning: The as operator was used to convert a wider integer type to a narrower one. as is widening-only; narrowing must use a named intrinsic so the agent chooses an explicit semantics (range-checked vs. truncating vs. saturating). See grammar.md §Type Cast.

Wrong:

fn f(big: i64) -> u8 {
    big as u8
}

Output: cannot cast 'i64' to 'u8' via 'as'; use 'i64_to_u8_try', 'i64_to_u8_wrap', or 'i64_to_u8_sat' to choose the narrowing semantics

Fix: Replace the cast with the narrowing intrinsic that matches your intent: - i64_to_u8_try(big) -> Option<u8> — reject out-of-range with None - i64_to_u8_wrap(big) -> u8 — truncate (keep low bits) - i64_to_u8_sat(big) -> u8 — clamp to 0..=255

Right:

fn f(big: i64) -> u8 {
    i64_to_u8_wrap(big)
}

i128/u128 to i64/u64 has no narrowing intrinsic family; the diagnostic's hint says so instead of naming one. Narrow through i32 or smaller with i128_to_i32_try-style intrinsics, or keep the value as i128/u128. See grammar.md §Type Cast.

ShiftCountOutOfRange¶

Phase: Type Checker Meaning: A constant-expression shift count is negative or greater than or equal to the bit-width of the left operand. Shifting an N-bit value by >= N bits is undefined in the underlying C model and is rejected at compile time when the count is statically known. Dynamic shift counts (non-const expressions) are checked by the verifier, which requires 0 <= count < width at the shift (a negative signed count is a violation). At runtime only 8-bit shifts trap: an i8/u8 shift whose count is >= 8 aborts with ArithmeticOverflow in every build mode. Wider shifts are not trapped; the hardware shift masks the count to the operand width ((x: i64) << 65 is x << 1), so only verification excludes them.

Wrong:

fn f(x: u8) -> u8 {
    x << 8
}

Output: shift count 8 is out of range for u8 (max 7)

Fix: Use a count less than the LHS bit-width. To shift a narrow value by a larger amount, widen first: (x as u32) << 8 is legal (it shifts the widened u32 value by 8), but the result is u32; to get back to u8, use a narrowing intrinsic such as u32_to_u8_wrap.

Right:

fn f(x: u8) -> u32 {
    (x as u32) << 8
}

TautologicalComparison¶

Phase: Type Checker Meaning: A comparison against a constant 0 can never fail (or can never hold) because the other operand has an unsigned integer type. x >= 0 and 0 <= x are always true for unsigned x; x < 0 and 0 > x are always false. Such a clause admits every implementation while reading like a real bound, so it is rejected rather than warned about — there is no suppression form. The const fold sees through as casts, so x >= 0 as u64 is caught too.

x > 0, x <= 0, x == 0 and x != 0 all constrain an unsigned value and keep compiling. Signed operands are untouched.

Wrong:

fn sum(n: u64) -> u64 vow {
    ensures: result >= 0
} {
    n
}

Output: comparison with 0 is always true for unsigned type `u64`

Widening casts do not launder the tautology. A cast can move the compared type to a signed one while leaving the value provably non-negative, so the rule follows the value, not the printed type. Because as is widening-only plus same-width signedness change (see Type Cast), the condition is exact: the comparison is tautological iff the source is unsigned and the target is strictly wider, i.e. the cast zero-extends.

fn f(x: u32) -> bool { (x as i64) >= 0 }   // error — u32 zero-extends into i64
fn g(x: u64) -> bool { (x as i64) >= 0 }   // ok — same width, `u64::MAX as i64` is -1
fn h(x: i32) -> bool { (x as i64) >= 0 }   // ok — a signed source sign-extends

A chain does not hide it either: (x as i32 as i64) >= 0 with x: u32 is rejected, and the diagnostic names the original unsigned source.

Output: comparison with 0 is always true for `u32` zero-extended to `i64`

Fix: Drop the dead clause, or state the bound you actually meant. An index invariant becomes invariant: i < v.len(); a lower bound that matters on an unsigned counter is i > 0, not i >= 0. If the subject really can be negative, its type should be signed.

Right:

fn sum(n: u64) -> u64 vow {
    ensures: result == n
} {
    n
}

StaticLiteralRequired¶

Phase: Type Checker Meaning: A compiler intrinsic requires a string literal operand so it can be lowered without allocation.

Wrong:

fn f(s: String, key: String) -> i64 {
    string_matches_literal_at(s, 0, key)
}

Output: string_matches_literal_at requires a string literal as its third argument

Fix: Pass a literal directly, for example string_matches_literal_at(s, 0, "name").

Right:

fn f(s: String) -> i64 {
    string_matches_literal_at(s, 0, "name")
}

EffectViolation¶

Phase: Type Checker Meaning: A function calls another function with effects not declared in its own signature, or a requires/ensures/invariant clause or parameter where clause calls a function or builtin method that writes through one of its arguments. The second form is blamed on the callee, even in a requires clause, because the clause itself is at fault for evaluating the write — not the caller.

Wrong:

fn f() -> () {
    print_str("hi");
}

Fix: Add the required effect to the function signature: fn f() -> () [io]. Effects are independent: [io] does not cover read or write, so a function that prints and reads a file declares [io, read].

Right:

fn f() -> () [io] {
    print_str("hi");
}

Wrong:

fn mark(p: Point) -> bool {
    p.x = 1;
    true
}

fn make_point(x: i64, y: i64) -> Point vow {
    ensures: mark(result)
} {
    Point { x: x, y: y }
}

Fix: Move the write out of the clause — contracts may only read, e.g. ensures: result.x == x. See docs/spec/grammar.md → "Contract Purity".

Right:

struct Point { x: i64, y: i64 }

fn make_point(x: i64, y: i64) -> Point vow {
    ensures: result.x == x
} {
    Point { x: x, y: y }
}

LinearTypeViolation¶

Phase: Type Checker Meaning: A linear owner value is used in a way that is immediately invalid, such as consuming it twice, consuming a value declared outside a loop from inside that loop (it may execute more than once), or consuming it after only some control-flow paths already consumed it. A value declared inside the loop body and consumed there is fresh each iteration and is accepted. The error also rejects a struct field whose type owns a linear obligation, because field access has no move-out semantics and repeated reads could expose that obligation more than once. Linear owners include linear struct values and owned enum, Option, or Result wrappers that transitively contain one; matching such a wrapper consumes it and transfers the obligation to the selected payload. An unbound _ catchall also violates the rule while any unhandled enum variant can carry a linear payload.

Wrong:

linear struct Handle { fd: i64 }

fn f(h: Handle) -> () {
    drop(h);
    drop(h);  // h was already consumed
}

Fix: Restructure ownership so each path uses a consumed linear value at most once. Discharge a value that is no longer needed with drop(value). Keep linear owners out of struct fields until move-out field access is supported. In a match, add explicit arms that bind and consume or transfer every linear payload before using _. Obligations that are simply left live at scope exit are reported later as RegionLinear.

Right:

linear struct Handle { fd: i64 }

fn f(h: Handle) -> () {
    drop(h);
}

RegionLinear¶

Phase: Region Inference Meaning: A linear struct value can remain live when its owning region closes. Returning the value transfers the linear obligation to the caller; consuming it before the close satisfies the obligation.

Wrong:

linear struct Handle { fd: i64 }

fn f() -> i64 {
    let h: Handle = Handle { fd: 1 };
    0
}

Fix: Consume the value before the region closes, or return it so the caller receives the obligation.

Right:

linear struct Handle { fd: i64 }

fn f() -> Handle {
    let h: Handle = Handle { fd: 1 };
    h
}

NonExhaustiveMatch¶

Phase: Type Checker Meaning: A match expression does not cover all possible variants.

Wrong:

fn f(o: Option<i64>) -> i64 {
    match o {
        Option::Some(x) => x,
    }
}

Fix: Add a _ => ... wildcard arm or cover all variants (Option::None => ...).

Right:

fn f(o: Option<i64>) -> i64 {
    match o {
        Option::Some(x) => x,
        Option::None => 0,
    }
}

UnsupportedPattern¶

Phase: Type Checker Meaning: A parsed match pattern or scrutinee, or a let pattern, is not in the subset that the compiler can lower safely.

Match currently accepts enum-valued scrutinees, qualified unit variants, qualified tuple variants with _ or immutable identifier payloads, and final catchall _ or immutable identifier arms. A tuple-variant pattern must bind exactly the number of payloads declared by the variant.

Wrong:

fn f(n: i64) -> i64 {
    match n {
        0 => 5,
        _ => 9,
    }
}

Output: literal match patterns are not supported

Fix: Use if/else comparisons for scalar or literal cases. For enum payloads, provide exactly one _ or immutable identifier for each declared payload and inspect bound values separately. Unsupported patterns fail before lowering and never produce an executable.

Right:

fn f(n: i64) -> i64 {
    if n == 0 {
        5
    } else {
        9
    }
}

let only binds identifier, wildcard, and tuple patterns; all other pattern kinds (literals, enum variants, struct patterns, or-patterns) are refutable and rejected outright, since let requires the pattern to always match:

Wrong:

fn f(o: Option<i64>) -> i64 {
    let Option::Some(x) = o;
    x
}

Output: let bindings only support identifier, wildcard, and tuple patterns

Fix: match the value and handle every variant.

Right:

fn f(o: Option<i64>) -> i64 {
    match o {
        Option::Some(x) => x,
        Option::None => 0,
    }
}

A tuple let pattern additionally requires the initializer to be a tuple literal of exactly the same arity, at every nesting level — tuple values have no runtime representation, so let (a, b) = ... is a compile-time desugaring into let a = ...; let b = ...;, never a projection out of a materialized tuple:

Wrong:

fn pair() -> (i64, i64) { (1, 2) }

fn f() -> i64 {
    let (a, b) = pair();
    a + b
}

Output: tuple destructuring requires a tuple literal initializer with matching arity

Fix: Rewrite the pattern as let (a, b) = (expr1, expr2); with one initializer element per pattern slot, or bind a single identifier and access elements once tuples are supported as first-class values (tracked separately; not yet implemented). A tuple let pattern also cannot bind a linear-typed element — bind the whole owner to a single identifier instead.

Right:

fn f() -> i64 {
    let (a, b) = (1, 2);
    a + b
}

ImmutableAssignment¶

Phase: Type Checker Meaning: A binding not declared mut was reassigned. Bindings are immutable by default; mut is required only for whole-binding reassignment x = e. Field writes (s.f = e) and index writes (v[i] = e) are allowed through any binding.

Wrong:

fn f() -> i64 {
    let x: i64 = 1;
    x = 2;
    x
}

Fix: Declare the binding mut: let mut x: i64 = 1;.

Right:

fn f() -> i64 {
    let mut x: i64 = 1;
    x = 2;
    x
}

UnusedMut¶

Phase: Type Checker Meaning: A let mut binding is never reassigned, so the mut is dead. Only whole-binding reassignment counts as a use of mut — a binding mutated solely via s.f = e, v[i] = e, or a method call does not need mut.

Wrong:

fn f() -> i64 {
    let mut x: i64 = 1;
    x
}

Fix: Remove mut: let x: i64 = 1;.

Right:

fn f() -> i64 {
    let x: i64 = 1;
    x
}

UnknownMethod¶

Phase: Type Checker Meaning: A method call uses a name that does not exist on the receiver type.

Wrong:

fn f() -> () {
    let v: Vec<i64> = Vec::new();
    v.psh(42);
}

Output: unknown method `psh` on type `Vec`

Fix: Check the method name for typos. Use --help to see available methods for each type. Vec has no get method: read an element with v[i] (see Indexing), and call HashMap::get or BTreeMap::get for maps. A Vec receiver calling get carries the structured hint use `v[i]` to read an element; `Vec` has no `get` in the diagnostic's hints array, identically in both compilers. Any other unknown method on a String, Vec, HashMap, BTreeMap, Option or Result receiver carries did you mean `push`? for the nearest builtin method within an edit distance of 3 (the earliest in the method list wins a tie; names over 128 bytes get none), and otherwise available methods: len, push, pop, clear, truncate, again identically in both compilers.

Right:

fn f() -> () {
    let v: Vec<i64> = Vec::new();
    v.push(42);
}

UnsupportedFeature¶

Phase: Parser (&expr), Type Checker (everything else) Meaning: A language feature that is not supported in Vow was used, or a HashMap/BTreeMap was written with a key or value type the runtime cannot store (see Map key and value types).

Wrong:

trait Foo {
    fn bar() -> i64;
}

Output: trait blocks are not supported in Vow

Fix: Remove the unsupported construct. Vow does not support traits or impl blocks.

Right:

fn bar() -> i64 {
    0
}

A prefix &expr (or &mut expr, &&expr) borrow expression is rejected by the parser, at the & or && token, with the hint Vow has no borrow expressions: pass the value itself; `&` is only the binary bitwise AND operator; the operand is still parsed, so the diagnostic is reported once:

Wrong:

fn f(x: i64) -> i64 {
    let r: i64 = &x;
    r
}

Output: borrow expressions (`&expr`) are not supported in Vow

Fix: Use the value directly. & is the bitwise AND operator between two operands (x & 1).

Right:

fn f(x: i64) -> i64 {
    let r: i64 = x;
    r
}

A tuple expression, including the empty tuple (), inside a contract clause is also UnsupportedFeature, because tuples have no runtime or verifier representation:

Wrong:

fn f(a: i64, b: i64) -> i64 vow {
    requires: (a, b) != (1, 2)
} {
    a
}

Output: tuple expressions are not supported in contract predicates

Fix: Compare the elements individually, e.g. requires: a != 1 || b != 2.

Right:

fn f(a: i64, b: i64) -> i64 vow {
    requires: a != 1 || b != 2
} {
    a
}

Map key and value types¶

The same code reports a map type whose key or value cannot be stored in the runtime's single 64-bit map slot: a HashMap key that is not an integer type of at most 64 bits or bool, a HashMap or BTreeMap value of type i128, u128, f32, or f64, and a HashMap value that is or contains a linear struct (see HashMap key and value types).

Wrong:

fn f() -> () {
    let m: HashMap<String, i64> = HashMap::new();
}

Output: HashMap key type `String` is not supported: keys are compared by value as a single machine word

Fix: Hash or intern the key to a u64 at the call site and keep a side table for the originals. For a 128-bit value, store the two u64 halves separately. For a linear value, keep it in a local binding and store only an integer handle in the map.

Right:

fn f() -> () {
    let m: HashMap<u64, i64> = HashMap::new();
}

Linear collection elements¶

The same code reports a Vec<T> whose element type is or contains a linear owner (a linear struct, or an Option, Result, or user enum wrapping one). Collections copy and shift elements bitwise, so a stored linear value would be duplicated or would escape the checker's consume-once tracking. A reference element (Vec<&Token>) borrows rather than owns and is accepted; a nested collection is reported once, where the innermost Vec is written, and a type alias once, at its definition.

Wrong:

linear struct Token { id: i64 }

fn f() -> () {
    let v: Vec<Token> = Vec::new();
}

Output: Vec element type must be non-linear; found 'Token'

Fix: Keep the linear value in a local binding and store an integer handle in the Vec. Consume a linear value that is no longer needed with drop(value).

Right:

linear struct Token { id: i64 }

fn f(t: Token) -> () {
    let ids: Vec<i64> = Vec::new();
    drop(t);
}

Slice types¶

The same code reports a slice type [T] (see Slice Types). Each bracket pair is reported once ([[i64]] gives two diagnostics, an alias once at its definition), with the hint use `Vec<T>` to hold a sequence of values.

Wrong:

fn probe(sl: [i64]) -> i64 { 0 }

Output: slice types (`[T]`) are not supported in Vow

Fix: Take a Vec<T> instead.

Right:

fn probe(sl: Vec<i64>) -> i64 { 0 }

Reserved type names¶

The same code reports a struct, enum or type alias named after a builtin type (see User-Defined Types). It is reported once per declaration, at the declaration, with the hint choose a different name for this type.

Wrong:

struct Vec { x: i64 }

Output: `Vec` is a builtin type name and cannot be declared as a user type

Fix: Rename the type.

Right:

struct Coord { x: i64 }

Unit parameters¶

The same code reports a parameter of type () (directly or through a type alias). The unit value carries no information and has no ABI slot, so such a parameter is rejected at the declaration.

Wrong:

fn f(u: ()) -> i64 { 0 }

Output: parameter `u` has type `()`: unit parameters are not supported

Fix: Remove the parameter.

Right:

fn f() -> i64 { 0 }

A 128-bit integer as an Option, Result, or enum payload is supported, so HashMap<i64, Option<u128>> is a valid map type (the map stores a pointer to the payload cell). A bare u128 or i128 map value is still rejected with the error above, because a map value occupies a single 64-bit slot. A 128-bit struct field or Vec element is not a map restriction: aggregates hold 128-bit values in two slots, so only a bare 128-bit map value is rejected.

BTreeMapKeyTypeMustBeI64¶

Phase: Type Checker Meaning: A BTreeMap<K, V> was instantiated with K not equal to i64. Phase 1 of the BTreeMap stdlib only supports i64 keys; the runtime helpers and the verifier's model are hard-coded to i64.

Wrong:

fn f() -> () {
    let m: BTreeMap<bool, i64> = BTreeMap::new();
    m.insert(true, 1);
}

Output: BTreeMap key type must be i64; found 'bool'

Fix: Use BTreeMap<i64, V>. If you need string or struct keys, hash or intern them to i64 at the call site and keep a side-table for the originals.

Right:

fn f() -> () {
    let m: BTreeMap<i64, i64> = BTreeMap::new();
    m.insert(1, 1);
}

BTreeMapValueMustBeNonLinear¶

Phase: Type Checker Meaning: A BTreeMap<K, V> was instantiated with a V that is or transitively contains a linear struct. Non-linear containers like BTreeMap, Vec, and HashMap cannot hold linear values because their internal shift/copy operations are bitwise and would silently duplicate the linear ownership obligation.

Wrong:

linear struct Token { id: i64 }
fn f() -> () {
    let m: BTreeMap<i64, Token> = BTreeMap::new();
}

Output: BTreeMap value type must be non-linear; found 'Token'

Fix: Either drop the linear qualifier on the struct, or keep handles in a Vec<i64> indirection and consume the linear values via direct function calls outside the map.

Right:

linear struct Token { id: i64 }

fn f(t: Token) -> () {
    let m: BTreeMap<i64, i64> = BTreeMap::new();
    drop(t);
}

MissingContract¶

Phase: Type Checker Meaning: An extern "C" block was declared without a vow { ... } contract. Every foreign function call requires a mandatory contract specifying expected behavior.

Wrong:

extern "C" {
    fn write_thing(fd: i32, ptr: i64, len: i64) -> i64 [io];
}

Output: extern block requires a vow contract

Fix: Add a vow { ... } block to the extern declaration with requires and/or ensures clauses.

Right:

extern "C" {
    vow {
        requires: fd >= 0
    }
    fn write_thing(fd: i32, ptr: i64, len: i64) -> i64 [io];
}

ContractTypeMismatch¶

Phase: Type Checker Meaning: A requires, ensures, or invariant clause expression, or a parameter where clause, does not have type bool.

Wrong:

fn add(a: i64, b: i64) -> i64 vow {
    requires: a + b
} {
    a + b
}

Output: `requires` clause has type `i64` but must be `bool`

Fix: Ensure every contract clause is a boolean expression (comparison, logical operator, or a call to a predicate function returning bool).

Right:

fn add(a: i64, b: i64) -> i64 vow {
    requires: a >= 0 && b >= 0
} {
    a + b
}

VowRequiresViolated¶

Phase: Verification Meaning: The verifier found inputs that violate a requires precondition. This is a static verification error — it means the function's callers can reach it with invalid arguments.

Wrong:

fn dec(n: u64) -> u64 vow {
    requires: n > 0
} {
    n - 1
}

fn caller(x: u64) -> u64 {
    dec(x)
}

Fix: Fix the callers to pass valid arguments, or, if the function is correct on a wider domain, state that real domain in the requires clause.

Right: (dec unchanged)

fn caller(x: u64) -> u64 {
    if x > 0 {
        dec(x)
    } else {
        0
    }
}

VowEnsuresViolated¶

Phase: Verification Meaning: The verifier found inputs where the function's return value does not satisfy the ensures postcondition.

Wrong:

fn max(a: i64, b: i64) -> i64 vow {
    ensures: result >= a && result >= b
} {
    a
}

Fix: Fix the function body to satisfy the postcondition, or weaken the ensures clause.

Right:

fn max(a: i64, b: i64) -> i64 vow {
    ensures: result >= a && result >= b
} {
    if a > b { a } else { b }
}

VowInvariantViolated¶

Phase: Verification Meaning: The verifier found a loop iteration where the invariant does not hold.

Wrong:

fn count_up() -> u64 {
    let mut i: u64 = 0;
    while i < 10 vow {
        invariant: i <= 10
    } {
        i = i + 3;
    }
    i
}

Fix: Strengthen the invariant or fix the loop body. No compiler emits VowInvariantViolated today: a loop-invariant counterexample is reported with error_code VowEnsuresViolated, the message reads contract violation in `f`: invariant <predicate>, and the counterexample violation starts with invariant.

Right:

fn count_up() -> u64 {
    let mut i: u64 = 0;
    while i < 10 vow {
        invariant: i <= 10
    } {
        i = i + 1;
    }
    i
}

EsbmcNotFound¶

Phase: Verification Meaning: ESBMC is not installed or not on $PATH. When verification is enabled with the ESBMC backend (the default for vowc build, always for vowc verify), the compiler checks for ESBMC upfront before compilation. If ESBMC is not found, the build aborts immediately with exit code 1. Under --backend native the verifier is Bitwuzla instead: a missing bitwuzla is reported per function as VerifyFailed with verify_status: "tool_not_found" (clause status error in vowc contracts --verify), and ESBMC is never consulted.

Wrong:

vowc build f.vow

Fix: Install ESBMC, or use --no-verify to skip verification: vowc build --no-verify <file>.

Right:

vowc build --no-verify f.vow

RegionConflict¶

Phase: Region Inference (arena-per-scope, Phase 3) Meaning: A heap-typed value's required lifetime cannot be satisfied by the regions the surrounding code provides. This fires when an interprocedural store-effect constraint is unsatisfiable against the inferred region — that is, the value's region(I) = LUB(must_outlive(I)) resolves to a concrete block strictly narrower than the target container's region.

Coverage note (as of issue #314): the check is now semantic, consulting the inferred region populated by §4.1 step 3's LUB pass rather than the raw IR opcode. A fresh allocation routed through a callee's store-effect chain into a parameter container has its inferred region widened to Caller(HiddenRegionIdx(N)) by §4.1 step 2's must-outlive marker propagation, where N is the precise slot index implied by the destination (issue #317 slot-aware inference). Such single-slot routings satisfy the constraint and are accepted. Allocations whose caller-region markers require more than one hidden caller-arena slot (for example, the value is stored into two distinct parameter targets, or returned and also stored into a parameter) have no single caller arena that outlives every destination, so their inferred region widens to the root region (Root) — a strictly wider placement than any one escaped pointer requires, hence sound (leak-but-safe) — and they compile without a blocking error (issue

871). Such a widen-to-root placement is not silent, though: it surfaces a¶

non-blocking RegionRootEscape note (issue #366; see below), so the permanent root-region placement is still visible. RegionConflict therefore fires only when a value's inferred region is a concrete block strictly narrower than the target container's region.

fn store_into(out: Vec<String>, prefix: String) [io] {
    let s: String = String::from(prefix);
    s.push_str(String::from(" world"));
    out.push(s);  // s is allocated in this function's scope but escapes into out's region
}

Fix: Move the allocation to a wider scope, or copy the value into the target region (e.g., String::from(s) into the outer arena). For routings that compile cleanly but you'd like to know about (root-region placement), see RegionRootEscape below. See docs/design/arena_memory.md §4.4 for the full rejection vs. visibility distinction.

Neither compiler rejects the snippet above today: it compiles and carries only a RegionRootEscape note (the self-hosted frontend reaches RegionConflict only through an internal-compiler-error path). Returning the value from the constructing function is the canonical shape and triggers neither:

Right:

fn make_greeting(prefix: String) -> String {
    let s: String = String::from(prefix);
    s.push_str(String::from(" world"));
    s
}

RegionRootEscape¶

Phase: Region Inference (arena-per-scope, Phase 3) Severity: Note (informational — does not fail the build) Meaning: A heap allocation may land in the never-freed root region (__vow_root_arena). The note fires in either of two cases:

1. The allocation's inferred region is Caller and the surrounding function publishes a FreshInCaller return summary or store effect — so the value may flow up the caller chain to main.
2. The allocation's region widens to the root region without an intrinsic root pin (pin_to_root / a literal) — either because it is routed into more than one distinct hidden caller slot (a multi-slot widen), or because it reaches a container through a Phi over caller containers (a Phi widen). Both are sound (leak-but-safe) placements, but the allocation lives for the whole process.

This is a memory-cost decision the compiler surfaces visibly per docs/design/arena_memory.md §4.4: silent root-region placement caused growth-with-no-signal in earlier compiler versions, and the note restores that signal without conflating it with unsoundness (RegionConflict).

The note is conservative — it fires for any qualifying allocation in a function that could route to a caller or that widens to root, even if the actual concrete chain in this program doesn't reach main. False positives are tolerated because the diagnostic is non-blocking. A widen-to-root allocation is flagged even when it is also returned: being returned does not undo a root-region placement.

Wrong:

fn store_into(out: Vec<String>, prefix: String) {
    out.push(String::from(prefix));
}

{
  "error_code": "RegionRootEscape",
  "severity": "note",
  "message": "allocation may live in the root region: routed via store-effect chain to a caller whose target_region ultimately resolves to root",
  "hints": [
    "if intentional (e.g. program-lifetime data), no action needed; if you want this allocation freed earlier, restructure so the value is returned rather than stored into a parameter container"
  ]
}

Fix: Often none — if the program is short-lived (a checker, a CLI tool) or the values are genuinely program-lifetime, the note is informational. To free the allocation earlier, restructure so the value is returned from the constructing function rather than stored into a parameter container; the canonical FreshInCaller return path (fn make_X() -> X) does not trigger the note for the returned value or any allocation installed as a field of the returned struct (e.g. Item { name: String::from("hi") }). The exemption applies only to the currently-installed field initializers — a field overwritten before the return (x.f = A; x.f = B; return x) does not suppress the dead allocation A, which fires the note as expected (per-block last-write dedup, issue #326).

Right:

fn make_name(prefix: String) -> String {
    String::from(prefix)
}

CodegenUnsupported¶

Phase: Code Generation Meaning: The program is valid Vow, but the selected native backend cannot yet lower one of its operations or representations. The build fails closed: status is CompileFailed and executable is null. No new executable is produced — but a file already at the -o path from an earlier successful build is left untouched, so branch on status/executable rather than on the output path existing. The diagnostic currently has a file-level span because backend errors do not carry an instruction origin.

Wrong:

fn remainder(a: f64, b: f64) -> f64 {
    a % b
}

Fix: Restructure the program to avoid the named backend limitation, or use a supported representation until the backend implements it. Agents may branch on CodegenUnsupported without parsing the human-readable message field.

Right:

fn remainder(a: i64, b: i64) -> i64 {
    a % b
}

CodegenFailed¶

Phase: Code Generation Meaning: The native backend failed while declaring, defining, or emitting otherwise-lowered code. This distinguishes an internal backend failure from a source-level parse/type error and from a known unsupported operation.

Fix: Inspect the diagnostic message for backend context. If the program uses only documented supported operations, report a compiler bug with the source and diagnostic; changing source syntax or types may not resolve an internal backend failure.

Right: No source rewrite applies; the program is not at fault. Keep it unchanged and report the bug.

LinkFailed¶

Phase: Linker Meaning: Code generation produced an object, but the native linker could not create the executable. A missing libvow_runtime.a is also reported with this code.

Wrong:

vowc build f.vow   # libvow_runtime.a not found

Fix: Inspect the diagnostic message and verify that the host linker and Vow runtime archive are installed and accessible. When building Vow itself, run cargo build --release --all or set VOW_RUNTIME_PATH to the runtime archive.

Right:

VOW_RUNTIME_PATH=target/release/libvow_runtime.a vowc build f.vow

IoError¶

Phase: Module loading, Code Generation

Meaning: The compiler could not read or write a file. Three build-pipeline sites produce this code: a use declaration naming a module the driver cannot read, a generated object's output directory the backend cannot create, and a generated object file the backend cannot write (full disk, read-only filesystem, or another write failure). The object bytes are already built by the time either the directory creation or the write is attempted, so this is the filesystem's answer rather than a backend defect — which is why it is not CodegenFailed. When this code comes from module loading, compilation stops before type-checking, so diagnostics do not include follow-on errors for names from the missing module.

Wrong:

module Main

use util.mathh

Fix: Check the path in the diagnostic message. For a module load, verify the use path resolves relative to the importing file. For an object write, the compiler creates missing parent directories automatically; verify that no path component is a regular file, that permissions allow creating directories and writing the object, and that the filesystem is writable and has free space. Re-running the same build after fixing the filesystem succeeds; changing the source will not help.

For a module-load failure, the path must resolve to util/math.vow (or util/math.vow.d) next to the importing file:

Right:

module Main

use util.math

VerificationSkipped¶

Phase: Verification (Warning surfaced alongside BuildStatus::Skipped) Meaning: The function carries a vow {} block but the verifier has no model for something its body does, so no proof is attempted. The contract becomes documentary: runtime checks still apply in --mode debug. A function is Skipped only for one of the reasons below; a timeout, a solver unknown, an unwinding failure and an out-of-memory worker are never Skipped (they are timeout / unknown, see docs/spec/cli.md → "Status Values").

The native backend names the reason with a code from a closed list, written after the function name in the message (skipped verification of `f`: <code>: <detail>). detail is free-form (a function, opcode or builtin name) and is not part of the enumerated set; the message text is not a contract. A machine-readable reason_code field is specified additively but not emitted yet, so do not parse for it.

The list is closed: a function that fits no row is a verifier bug, not a new Skipped reason. Under the ESBMC backend the reason is the older free-text non_modelable_reason of the C emitter instead, for example an opcode the C model cannot represent (RegionAlloc and FieldSet from a struct construction the model does not cover, Load/Store, RemF*, LinearBorrow), a 128-bit checked operation or aggregate field, or a call that passes a Vec, String, map or Option argument to a user function (Call target with a collection argument) or uses a user function's result as one (Call target with a collection result). Native verification models the 128-bit cases, so those are Skipped only under ESBMC.

Every non-modelable vowed function is reported, including when another function fails verification in the same run: the set of skipped functions depends only on the program, not on the verify cache or --verify-jobs.

Wrong:

fn len_of(v: Vec<i64>) -> u64 {
    v.len()
}

fn count(v: Vec<i64>) -> u64 vow {
    ensures: result == v.len()
} {
    len_of(v)
}

{
  "error_code": "VerificationSkipped",
  "severity": "warning",
  "message": "skipped verification of `ir_inst_set_region`: function `ir_inst_set_region` is not modelable in the verifier (contains unsupported opcode `RegionAlloc`)",
  "hints": [
    "the contract is documentary; runtime checks still apply in --mode debug"
  ]
}

Why the build fails closed. Per CLAUDE.md's "Contract Authoring" guidance, contracts express semantic correctness and must not be weakened to fit the verifier. When the verifier cannot represent a function's body, the function is skipped with a structured warning instead of tripping a defense-in-depth assertion (under ESBMC, __ESBMC_assert(0, "vow:UNSUPPORTED_OP_VOW_ID"), which historically broke the bootstrap on every vowed struct-builder). But a skipped contract is still an unproved contract, so the build lifts its overall status to Skipped (exit 1). Use --no-verify if you explicitly want a non-failing path that does not invoke a verifier at all (Unverified, exit 0).

Fix: Refactor the function so its body uses only modelable opcodes — typically by splitting allocation/initialisation away from the contract-bearing computation. Alternatively, run with --no-verify if the contract is intentionally documentary.

Right:

fn count(v: Vec<i64>) -> u64 vow {
    ensures: result == v.len()
} {
    v.len()
}

Note form (uncontracted caller). The same code also appears with severity: "note" for a function that has no vow block, cannot be modelled (effects such as [io], unsupported operations, a collection passed to a user function), and calls contracted functions. The callee requires at those call sites are not statically checked, but no contract of its own went unproved, so the build status does not fail closed. This note form is produced by the ESBMC backend; under --backend native the uncontracted-caller selection is shared but a native timeout or unknown for such a caller is a hard VerifyFailed, not a note. The message ends with the reason, and the reasons need different fixes: `f` cannot be modelled (restructure f, or accept that it stays unverified), or the verifier timed out forf/ `the verifier could not decide them for `f (the proof was attempted but not finished — constrain or simplify f, or raise the timeout):

{
  "error_code": "VerificationSkipped",
  "severity": "note",
  "message": "calls from `main` to contracted `divide` were not verified: `main` cannot be modelled",
  "hints": [
    "the callee `requires` at these call sites are checked at runtime in --mode debug only"
  ]
}

ArithOverflowReachable¶

Phase: Verification (Warning; the build status stays Verified) Meaning: The verifier proved that a checked operator (+!, -!, *!, /!, %!) can reach its ArithmeticOverflow abort for some input the function's requires admits. The operand span in primary points at the operator itself.

Wrong:

fn twice(x: i64) -> i64 vow {
    ensures: result == x + x
} {
    x +! x
}

{
  "error_code": "ArithOverflowReachable",
  "severity": "warning",
  "message": "checked arithmetic in `twice` can abort: addition overflows",
  "hints": [
    "the contract is proved for every execution that returns; this abort is a separate runtime outcome",
    "constrain the operands in `requires` to rule the abort out, or use the wrapping operator if wrapping is intended"
  ]
}

The message names the cause: addition overflows, subtraction overflows, multiplication overflows, divisor is zero, or quotient is not representable (MIN / -1).

Why this is a Warning and not a failure. Aborting is the checked operator's specified behaviour (grammar.md), so a reachable abort is not an unproved obligation — unlike VerificationSkipped, nothing went unchecked, and the status does not fail closed. The contract is genuinely proved: the verifier models the abort by pruning the overflowing execution, which never returns and so can never witness an ensures or a loop invariant. The warning exists because an abort is rarely what the author intended and is invisible in the contract verdict — Verified alone would not tell you the program can die at that operator.

Fix: If the abort is unreachable in practice, say so in the contract — a requires that bounds the operands removes the warning, and the bound is then a genuine semantic constraint rather than a verifier appeasement. If wrapping is the intended behaviour, use the wrapping operator (+, -, *, /, %) and state the wrapped result in the contract. If the abort is a real possibility the caller must handle, the warning is informational.

Right:

fn twice(x: i64) -> i64 vow {
    requires: x >= -4611686018427387904 && x <= 4611686018427387903
    ensures: result == x + x
} {
    x +! x
}

Not emitted when: the contract itself fails. The verifier reports one violated property per run, so a contract counterexample takes precedence and no abort claim is made — the counterexample is the actionable finding.

VerifierAssertionUnattributed¶

Phase: Verification Meaning: The verifier found a failed property that Vow cannot attribute to a user-authored requires, ensures, or invariant clause. The build fails closed with VerifyFailed, and the corresponding counterexample uses blame: "None" plus a reserved non-contract vow_id so it cannot collide with the function's real vow 0. Known examples are division or remainder by zero, a dynamic shift count that exceeds the operand's bit width, signed MIN / -1 (native backend only), unwrap() called on None or Err (native backend only) and an out-of-bounds Vec index (native backend only). Under --backend native the native vow_id is 4294967293 and blame is None.

Wrong:

fn remainder(n: u64, d: u64) -> u64 vow {
    ensures: result <= n
} {
    n % d
}

{
  "error_code": "VerifierAssertionUnattributed",
  "severity": "error",
  "message": "verification failed in `remainder` on an unattributed property: division or remainder by zero",
  "span": { "file": "", "offset": 0, "length": 0 }
}

The structured counterexample's violation field carries the stable property description instead of raw verifier text. source may be null when the verifier property has not been mapped back to a Vow source span.

Fix: Inspect counterexamples[0].violation and the reported values. For division or remainder by zero, prevent a zero divisor with a real semantic precondition or a checked branch. For unwrap() called on None, match on the value or require its discriminant instead of unwrapping. For a dynamic shift, keep the count below the left operand's bit width. If the description names an unfamiliar internal assertion, report it as a compiler attribution bug rather than treating the reserved vow_id as a contract clause.

Right:

fn remainder(n: u64, d: u64) -> u64 vow {
    requires: d != 0
    ensures: result <= n
} {
    n % d
}

VerifierBug¶

Phase: Verification (self-hosted vowc verify --backend native --replay-cex only) Meaning: Under the native backend, a counterexample did not replay: the --mode debug harness built from its concrete inputs did not reproduce the predicted VowViolation (same vow_id and blame) or, for a division or remainder abort, the predicted ArithmeticOverflow abort, or, for an unwrap() abort, the predicted UnwrapOnNone abort, or, for a Vec index past the end, the predicted IndexOutOfBounds abort. The counterexample's replay is "diverged" or "aborted" and replay_reason says why. A "skipped" replay (a harness limitation such as an unsupported parameter type) never ran and is not reported. The verifier model and the runtime disagree, so this is a defect in the verifier, not in the program. One diagnostic is emitted per such counterexample; the status stays VerifyFailed and the exit code stays 1.

{
  "error_code": "VerifierBug",
  "severity": "error",
  "message": "native verifier counterexample for `rem` did not replay (diverged: harness exited cleanly; the predicted ArithmeticOverflow abort did not occur)",
  "hints": [
    "a counterexample that does not reproduce at runtime is a bug in the verifier model; report it"
  ]
}

Fix: Report the function, its counterexample values and replay_reason as a verifier bug. Do not weaken the contract to avoid the counterexample on the strength of this diagnostic alone.

Right: No source rewrite applies; the program and its contract are not at fault. Keep both unchanged and report the bug.

ModelCapacityAssumed¶

Phase: Verification (Note; the build status stays Verified). ESBMC backend only: never emitted under --backend native, which models collections with a symbolic length and no capacity. The diagnostic is retired together with the ESBMC backend. Meaning: The function's contracts were proved, but the proof's model restricts at least one capacity to the verifier's model capacity (defaults: Vec<T> 128, String 256, HashMap<K, V> and BTreeMap<K, V> 64, user-struct Heap 1024 slots; the String capacity is raised to the longest string literal in the module, and the note's message reports the capacity actually applied; see contracts.md). A parameter, struct-field collection, String::from_cstr result, or non-constant from_raw_parts_copy length is modelled as nondeterministic within its capacity, and struct allocations stop at the heap capacity, so executions with longer collections or more struct allocations were pruned, not checked: Verified means "verified for executions up to the capacities".

Wrong:

fn first_or_zero(v: Vec<i64>) -> i64 vow {
    requires: v.len() <= 128
    ensures: v.len() > 0 || result == 0
} {
    if v.len() > 0 {
        v[0]
    } else {
        0
    }
}

{
  "error_code": "ModelCapacityAssumed",
  "severity": "note",
  "message": "proof of `first_or_zero` is bounded: only executions within the verifier model capacity were checked (Vec<T>: 128)",
  "hints": [
    "the bound belongs to the bounded model checker, not to the program or its contracts; executions beyond it (longer collections, more struct allocations) were not checked",
    "do not add a length bound to a contract to silence this note; an unbounded verifier removes it without any source change"
  ]
}

The message lists every bounded kind as Kind: capacity, in the fixed order Vec<T>, String, HashMap<K, V>, BTreeMap<K, V>, Heap, one entry per kind. When a model applied several capacities to one kind, the smallest is listed: the proof is claimed only for executions within every bound the model applied. At most one note is emitted per proved function. The span is empty (the note describes the model, not a source location).

Why this is a Note and not a failure. The verdict is genuine for every execution inside the bound and the verifier never changes a verdict because of the note. It is informational so that an agent or CEGIS loop can tell a bounded proof from an unbounded one — for example, to treat a Verified function that handles untrusted-length collections with extra scrutiny, or to test it with the runtime checks of --mode debug.

Fix: None is required. Do not add requires: v.len() <= 128 (or any other capacity) to silence it: that distorts a true contract to fit a prover limitation, and an unbounded backend removes the note without any source change.

Right: Remove the length bound and keep the note; the source needs no other change.

fn first_or_zero(v: Vec<i64>) -> i64 vow {
    ensures: v.len() > 0 || result == 0
} {
    if v.len() > 0 {
        v[0]
    } else {
        0
    }
}

Ordering and presence. Notes describe a completed proof run, so they are emitted only when the overall status is Verified, one per proved function, after every other diagnostic and in function declaration order. A run that ends in a counterexample, unknown, timeout, error, or a fail-closed skip carries no note: a halt cuts the set of verified functions short in a scheduling-dependent way, and a note about one of them would be noise next to the real failure.

Not emitted when: the function's model restricts no capacity (scalar-only functions that allocate no struct, and collections built by the function itself from constant lengths or from a null source), or the overall status is not Verified. The same note is emitted by vow verify and vow build.

Runtime Errors¶

These are emitted to stderr as JSON when a compiled program runs (debug mode for VowViolation).

Exit status. Every runtime abort below terminates the process with the reserved exit status 134 (128 + SIGABRT, the conventional "aborted" status), never a plain 1. A runtime abort is an environment or soundness failure, not an application result. 134 is reserved for aborts by convention: a runtime abort never spontaneously collides with an application's own return N from main, so a program that does not itself return — or process_exit — 134 can treat any 134 exit as a runtime abort (a checker that returns 0/1/2 for accepted/rejected/declined will never mistake an out-of-memory or a contract violation for a genuine "rejected"). The runtime does not enforce the reservation — process_exit(134) and return 134i32 still exit 134 — so a program that deliberately uses 134 opts out of the distinction; applications that care should reserve around it. The JSON envelope on stderr still names the specific abort. This is separate from the compiler exit codes in cli.md, which describe vowc build/vowc verify.

VowViolation¶

When: Debug mode only (--mode debug). A requires, ensures, or invariant predicate evaluates to false at runtime.

{"error":"VowViolation","vow_id":0,"blame":"Caller","description":"y != 0","file":"divide.vow","offset":42,"values":{"y":0}}

file is the source file that defines the violated clause (the module file for a clause in an imported module, not the entry file) and offset is the byte offset at which that clause starts. Both compilers report the same file and offset for the same program, never an empty placeholder.

The blame field indicates who is at fault: - Caller — a requires was violated (the caller passed bad arguments) - Callee — an ensures or invariant was violated (the function has a bug)

Wide integer values. values entries are bare JSON number tokens and are not bounded by i64. A u64, i128, or u128 binding reports its full magnitude, which can exceed the range an IEEE-754 double represents exactly — u128::MAX renders as 340282366920938463463374607431768211455. A consumer that acts on the exact value must read it with an arbitrary-precision JSON number parser; a default double parser silently rounds it.

Wrong:

fn divide(a: i64, b: i64) -> i64 vow {
    requires: b != 0
} {
    a / b
}

fn main() -> i32 {
    let q: i64 = divide(10, 0);
    0
}

Fix: See the description and values fields to understand which predicate failed and with what runtime values.

Right: (divide unchanged)

fn main() -> i32 {
    let q: i64 = divide(10, 2);
    0
}

ArithmeticOverflow¶

Not gated by [panic]: checked operators are modelled as aborting in pure functions.

When: A checked arithmetic operator (+!, -!, *!, /!, %!) overflows at runtime; or checked or unchecked division/remainder encounters a zero divisor; or signed / or /! evaluates MIN / -1.

{"error":"ArithmeticOverflow"}

Fix: For addition, subtraction, or multiplication, use wrapping arithmetic if overflow is acceptable, or add bounds contracts to prevent overflow. For division and remainder, rule out a zero divisor and, for signed division, the MIN / -1 case.

Wrong:

fn main() -> i32 {
    let a: i64 = 9223372036854775807;
    let b: i64 = a +! 1;
    0
}

Right:

fn main() -> i32 {
    let a: i64 = 9223372036854775807;
    if a < 9223372036854775807 {
        let b: i64 = a +! 1;
    }
    0
}

The abort is emitted in every build mode, release included, so this cannot be deferred to a debug run. A checked operator's abort is part of the operator's meaning, not a debug-mode check. Division and remainder also abort when no result exists, regardless of whether their checked or unchecked spelling is used.

UnwrapOnNone¶

When: .unwrap() is called on Option::None or Result::Err.

{"error":"UnwrapOnNone"}

Wrong:

fn main() -> i32 [panic] {
    let o: Option<i64> = Option::None;
    let x: i64 = o.unwrap();
    0
}

Fix: Use match to handle the empty variant — None for Option, Err for Result — or add contracts that guarantee the value is Some/Ok.

Right:

fn main() -> i32 {
    let o: Option<i64> = Option::None;
    match o {
        Option::Some(x) => x,
        Option::None => 0,
    };
    0
}

The abort is emitted in every build mode, release included, so this cannot be deferred to a debug run.

IndexOutOfBounds¶

Not gated by [panic]: the abort is a verification obligation of the (pure) indexing function.

When: A Vec index access (v[i] or v[i] = val) uses an index outside 0..v.len().

{"error":"IndexOutOfBounds"}

Wrong:

fn main() -> i32 {
    let v: Vec<i64> = Vec::new();
    let x: i64 = v[0];
    0
}

Fix: Add a bounds check before indexing, or add a contract: requires: i < v.len(). Do not pair it with requires: i >= 0 — on an unsigned index that clause is always true and is rejected as TautologicalComparison.

Right:

fn main() -> i32 {
    let v: Vec<i64> = Vec::new();
    if v.len() > 0 {
        let x: i64 = v[0];
    }
    0
}

RegionLiteralMutation¶

When: A Vec, String, or HashMap mutation is attempted on a literal-backed container — one whose descriptor carries the VOW_CAP_RODATA sentinel (backing lives in .rodata or was pinned to the root region). Calls that statically trace a mutating target to a literal are rejected during compilation with this code; a runtime fallback emits the JSON shape below if an unchecked mutation reaches a VOW_CAP_RODATA descriptor. See docs/design/arena_memory.md §6.1, §7.3.

{"error":"RegionLiteralMutation","operation":"String::push_str","origin":"rodata"}

A plain-text hint follows on the next line (not a JSON field). The hint text is dispatched on the operation's type prefix:

hint: make an explicit mutable copy with String::from(value) before mutating  # for String::* operations
hint: construct a mutable Vec and copy entries before mutating                # for Vec::*    operations
hint: construct a mutable HashMap and copy entries before mutating  # for HashMap::* operations

The operation field identifies the source-level method that trapped (e.g., Vec::push, Vec::pop, HashMap::insert, String::clear). The origin field identifies the storage class of the immutable backing; today only rodata is emitted.

Wrong:

fn main() -> i32 {
    let s: String = "abc";
    s.push_str("d");
    0
}

Fix: Obtain an explicit mutable copy before mutation: String::from(value), or construct a fresh mutable container and copy the entries you need before mutating.

Right:

fn main() -> i32 {
    let s: String = String::from("abc");
    s.push_str("d");
    0
}

StackOverflow¶

When: The native call stack is exhausted, typically due to unbounded recursion.

{"error":"StackOverflow"}

In debug or sanitize mode, the diagnostic includes call depth and the function that was executing when the overflow occurred:

{"error":"StackOverflow","depth":10693,"function":"recurse"}

The signal handler is installed in all build modes. The depth and function fields are only available in debug/sanitize mode where call-depth instrumentation is emitted.

Wrong:

fn count_down(n: u64) -> u64 {
    count_down(n + 1)
}

fn main() -> i32 {
    let r: u64 = count_down(1);
    0
}

Fix: Add a base case to recursive functions, or restructure the algorithm to use iteration instead of recursion.

Right:

fn count_down(n: u64) -> u64 {
    if n == 0 {
        return 0;
    }
    count_down(n - 1)
}

fn main() -> i32 {
    let r: u64 = count_down(1);
    0
}

OutOfMemory¶

When: A runtime arena operation (__vow_arena_open or __vow_arena_alloc) failed because the underlying malloc returned null. Non-recoverable from within Vow (docs/design/arena_memory.md §3.3, §16).

{"error":"OutOfMemory","operation":"arena_alloc"}

The operation field is arena_open for the initial chunk allocation or arena_alloc for a later fallback chunk allocation.

Like every runtime abort, an OOM exits with the reserved status 134 (see Exit status above), so it is distinguishable from an application's own exit 1.

Fix: Reduce working-set size, raise the process memory limit, or run on a machine with more memory. This is not a Vow program error.

Right: No source rewrite applies; the program is not at fault.

Warnings¶

LoweringWarning¶

Phase: IR Lowering Meaning: The IR lowerer could not resolve a struct type tag or field name, defaulting to index 0. This usually indicates a missing type annotation on a let binding, causing the compiler to lose track of which struct type a pointer refers to.

Fix: Add an explicit type annotation: let x: MyStruct = ...; so the compiler can track struct type tags through the IR.

Right:

struct MyStruct { a: i64 }

fn f() -> i64 {
    let x: MyStruct = MyStruct { a: 1 };
    x.a
}