Glossary

kola's terms on one page, as the compiler's diagnostics and the two cards use them: SPEC-CARD.md for the language and STD-CARD.md for the standard library (kola help spec-card, kola help std-card).

Values and types

• data: plain copyable values with nothing owning inside: integers, bool, (), char, f64, references, and structs, enums and tuples built from them. Copied freely and compared by value with ==, through references too (by pointee, never by address).

• owning value: a value that moves and is never copied: an owned Vec[T] (a Vec by value), a Map, a value that holds a &mut, and anything that carries one of those in a field or payload. Passing it by value moves it, and reading the source afterwards is an error. Borrow it instead with &v or &mut v.

• resource: a linear value, declared with resource struct: a file, a socket, a thread handle, a capability. It cannot be copied and cannot be silently lost. Many resources wrap an operating-system handle, such as a file descriptor (the small integer the OS uses to name an open file or socket), which must be closed exactly once.

• linearity: the rule that a resource is consumed exactly once on every execution path. Forgetting it is a compile error (resource `t` is not consumed on this return path), and so is using it twice.

• consumption: the ways to finish a resource: pass it to a function that takes it by value (self: T), return it, move it on, or destructure it.

• destructuring: taking a value apart with a pattern, as in let Wal { entries: _ } = self;. For a resource this is how a consuming function ends the value. Every field must be named; there is no ...

• move: handing a value to a new owner. Every position typed by value moves an owning value or a resource: a call argument, a let, a struct-literal field, a variant payload such as Some(v), a channel message, a thread's context, an assignment into a field, a return. Data is copied instead.

• unit (): the type with one value, also written (). A function without -> T returns it.

• literal: a value written in the source: 42, 0x2A, 0o644, 0b1010, 1.5, "text", f"n={n}", b"bytes", r"raw", [1u8, 2u8], Point { x: 1, y: 2 }. _ between digits is a separator. There is no character literal.

• type suffix: 3u64 is the number 3 of type u64. An unsuffixed literal takes its width from context (an annotation, a parameter, the other operand, an index position, which is usize). A width nothing pins is u64, or i64 if a negative value ever enters it.

• widen / narrow / wrap: the only numeric conversions, all explicit. widen[u64](x) is lossless, narrow[u8](x) returns Option[u8], and wrap[i16](x) reinterprets the low bits and never traps. There is no as.

• slice: a view into an array or a Vec, typed &[u64] or &r [u8]. It has .len, indexing xs[i] and subslices xs[a..b]. Nothing is copied.

• view rule: while a view into a place (&v[i], a subslice, a for walk over v) is still used, that place is not written, grown, shrunk or moved through any other name. The repair is to finish the reads first, copy the value out, or keep the index and read again after the change.

• str: a (pointer, length) view of UTF-8 text. .len is its length in bytes and .bytes is the same view as &[u8]. A plain "..." literal is static data and fits any region.

• interpolation: an f"..." literal substitutes expressions into text: f"n={n} sum={a + b}". A plain "..." never interpolates. A bound f-literal allocates; its region is the destination's if the destination's type names one, otherwise the innermost open region, and otherwise the literal is refused. Passed straight to a call-scoped &str parameter, it allocates nothing.

• generic: a parameter in square brackets. Uppercase names bind types and lowercase names bind regions: fn first[T: data](xs: &[T]) -> Option[T]. An unbounded T is treated as linear; T: data makes it copyable; T: move admits data and owning values but no resource. A [const N: usize] parameter binds a compile-time number, usable as an array length. There are no angle brackets.

• monomorphization: compiling a generic by generating one specialized copy per set of type arguments, much as if you had written first_u64 and first_u8 by hand. Every call goes straight to a known function; there is no run-time lookup of which function to call, as there is with C++ virtual methods.

• fn reference: a top-level function name used as a value, as in seq::sort(xs, less_u64). Its type includes the effect row: fn(u64) -> u64 !{}. It captures nothing, because there are no closures.

• module-scoped type: a struct or enum belongs to its module, like a function. Inside the module you name it bare; elsewhere, use M::T; and then T, or M::T in a type position.

Memory

• arena: a block of memory that hands out allocations in order, by moving a pointer forward past each one ("bumping" it), and is freed all at once. That makes allocation very cheap. Nothing in an arena is freed individually.

• region: a lexical block region r { ... } that owns an arena. Everything allocated in it is freed at the closing brace. region r from m { ... } backs the arena with the memory budget m.

• alloc in: allocation into a region: alloc in r mut Vec::new() gives a &r mut Vec[T]. Mutability is chosen where the value is allocated.

• heap: the built-in region that lives as long as the program. There is no garbage collector; heap memory is released when the process ends. A plain string literal is static data and can be typed &heap str. An owned Vec's storage is always on heap, so growing one is alloc(heap).

• region reference &r T: a reference whose type names its region. It can be copied freely but cannot outlive the region, which is checked at compile time.

• call-scoped view &T / &mut T: a reference that exists only as a parameter type. The callee may use it for the duration of the call but cannot store or return it. It is the default parameter form.

• region parameter: a lowercase name in square brackets, as in fn body[r](b: &r [u8]) -> &r [u8]: the function works with whatever region the caller has. A call never writes the region; it is inferred.

• lend: a region-scoped shared view of a resource: let v: &r Wal = lend wal in r;. The resource is frozen until the region closes. There is no lend mut.

• Pool[T]: a slab (a fixed array of equal-sized slots) for long-lived, graph-shaped data, where individual slots can be freed, which a region cannot do. Capacity is reserved at new and charged to the budget in full, but pages are touched only when a slot is first used. insert traps with TrapKind::Capacity when the pool is full; try_insert hands the element back instead. drain_next pops an arbitrary occupied slot for teardown. A Pool may not cross a thread.

• generational handle Gen[T]: the ticket insert returns. It answers two questions: is this slot still the one you were given (after remove, the old handle yields None even if the slot is reused), and is the handle from this pool at all (a handle used on another pool is a deterministic miss).

• owned Vec: Vec::new() bound by value, with storage on heap. Its buffer moves between threads without copying. For memory returned at a brace, allocate the Vec in a region instead.

Effects and capabilities

• effect: what kind of thing a function may do. There are five: alloc(r) (allocates into region r), io (touches the outside world through a capability), hw (a privileged or ordering-sensitive machine operation), block (may block or sleep) and log (writes to the process log). Effects say what kind; capabilities say to what.

• effect row: !{...} at the end of a signature, after the return type: fn f(x: &T) -> u32 !{io}. Every public function states one; a private one may leave it to inference.

• pure function: a function with the row !{}: provably no allocation, no I/O, no blocking.

• hw: the machine effect, for operations a kernel or driver performs on the hardware itself: masking interrupts, maintaining caches and the TLB (the CPU's cache of address translations), memory barriers (instructions that stop the CPU from reordering memory accesses across them), MMIO and atomics. It is forbidden in a ct fn and never reordered or removed. Plain reads and writes through a RamWindow stay on io.

• capability: a value that grants access to one part of the world. There is no ambient authority, so every effectful library operation takes one. Authority tokens such as Clock, Rng, Fs, Dir, Dial, Stdout may be dropped. Mem and linear handles such as File, Conn, Child must be consumed.

• Sys: the root set the runtime passes to main and nothing else: sys.clock, sys.rng, sys.mem, sys.fs, sys.dial, sys.listen, sys.stdout, sys.stdin, sys.stderr, sys.args, sys.env, sys.tty, sys.ping, sys.proc, sys.netlink, sys.raw_ip, sys.mmio, sys.cpu, sys.dev, sys.window and sys.inherited. main takes it by value or takes nothing.

• ambient authority: power available from anywhere, such as a global print, filesystem or clock. kola has none.

• attenuation: narrowing authority as it is passed down. main holds everything and passes a helper only &sys.clock. Some narrowing is typed: dir.ro() gives a DirRo with no write operations, w.atomic() leaves a window only its atomic operations, and dial.to_host(host, port) reaches one endpoint. A capability moves once, so clock.split(), rng.split() and dial.split() hand a worker its own.

• grant: authority beyond the working directory and the process itself (a directory, a binary, a device, a hardware window), bound by name by whoever runs the program. kola run --fs-root db:ro=/abs grants it, and sys.fs.root(b"db") looks it up, returning None if nothing was granted. Each flag has an environment twin, such as KOLA_FS_ROOT_db. Grants come from the operator, never from a parent process.

• log: the one effect that needs no capability, because the sink is write-only: the program cannot read it back, so it cannot steer control flow. The sink and level are chosen once, by --log and --log-level or KOLA_LOG and KOLA_LOG_LEVEL. The functions are std::log::{error, warn, info, debug}.

• memory budget: a part of the Mem capability carved off with sys.mem.split(n). It backs a region with region r from m, and linearity makes you return it with sys.mem.absorb(m). Exceeding a budget traps with TrapKind::Budget.

• window: a granted span of memory or address space with a length and an opaque base. kola works with offsets, never pointers. RamWindow is memory shared with hardware, such as a ring of buffer descriptors a network card reads. MmioWindow is device registers mapped into memory (MMIO, memory-mapped I/O: reading or writing such an address talks to the device instead of RAM). IoWindow is x86 port I/O, an older separate address space for devices. Every access carries a bounds contract that the prover can discharge like an array index.

• device model: under a hosted run or test there is no real device behind a window or device grant, so a model written in kola supplies the behaviour, bound with --sim-mmio, --sim-io or --sim-dev. A grant without a model refuses the test at startup.

• Proc / Child: sys.proc.spawn(bin, argv, env, disp, slots) runs a binary the operator granted by name (--proc-bin ffmpeg=/abs). env is explicit, so nothing ambient crosses. disp: Stdio is Inherit, Piped or Null. Child is linear: wait or kill consumes it. ExitStatus is Code(u8) or Signaled(Signal), and a signal is a name, never a number.

Errors and contracts

• trap: a deterministic halt when an assumption is violated: overflow, out-of-bounds access, a false contract, an unwrap of None, an explicit trap("msg"). No unwinding and no continuing with garbage.

• fault domain: what a trap kills. By default the whole process (in a test, the test). A domain d { ... } recover(t: Trap) { ... } block narrows it to the block: a trap in the body tears d down and runs recover. A domain is a region that also catches. A trap inside recover is fatal.

• Trap: the plain data recover receives. t.kind is one of Bounds, Arith, Req, Ens, Inv, Assert, Unwrap, Explicit, Budget or Capacity, and t.site is module:line, never a filesystem path.

• contract: a checkable condition on a signature. It is always enforced: proven at compile time, in which case the check disappears, or checked at run time with a trap. No build mode removes it.

• req: a precondition, the caller's obligation: req i < xs.len.

• ens: a postcondition, the function's promise; ret names the result: ens ret <= 100.

• inv: an invariant of a resource struct, written as the last item of its body: resource struct Ring { head: usize, inv head < 8 }. Checked at construction and at function boundaries.

• assert: a checked claim inside a body, with the same discharge rule as contracts. Its expression must not change anything.

• Option / Result: expected outcomes as values. Option[T] is present or absent; Result[T, E] is success or an expected error.

• ?: an early return. It takes v out of Ok(v), and on Err returns the error from the current function. A resource live at the ? is a linearity error.

• discarding a Result: a compile error. Handle it with match, ? or .unwrap(), or discard it on purpose with let _ = ...;.

• unwrap: takes the value out of an Option or Result and traps on None or Err. It moves its receiver.

• OS result convention: an operation that reaches the OS answers Result[T, (E, OsErr)], where E is the action family (FsErr, NetErr, IoErr, DevErr, ProcErr, NetlinkErr) and OsErr is the OS's own identity, such as NoEnt. "Nothing yet" is never an error: a try_* operation answers Ok(None).

• layout_assert: a module-level item, layout_assert[Point](8, 4);, that claims a type's C size and alignment. The C backend turns it into a _Static_assert; the interpreter treats it as a no-op. kola has no size_of.

Data you must not trust, data you must not reveal

• untrusted: a parameter marker for attacker-supplied input: wire, file, stdin or IPC bytes. A req, ens or inv may not depend on it, because a contract is a claim about the caller and these bytes have no caller. Check the value at run time and return Result or Option. kola report tainted-reqs finds candidates in existing code.

• Secret[T]: an opaque, linear box for data you must not reveal. Secret::wrap(x) boxes it, Secret::expose(&s) is the only read, Secret::wipe(s) consumes and scrubs it, Secret::eq(&a, &b) compares in constant time, and Secret::wipe_bytes(&mut buf) scrubs a buffer you do not own the box of. A runtime-length secret is Secret[Vec[u8]]. A reference cannot be boxed: scrubbing a pointer would leave the bytes behind it.

• Entropy[[u8; N]]: a box that records where the bytes came from: OS entropy, unpredictable to an adversary. Entropy::draw[[u8; N]](&mut rng) mints one and Entropy::expose(&e) reads it. Entropy::of(x), for test vectors, is refused by kola audit on any path that does not start in a test. It is not linear and not a Secret; a key can want both.

• ct fn: a constant-time function. Its running time and memory-access pattern may depend on the shape of its parameters (widths, lengths) but not on their values. This matters for cryptography: if a comparison of a password or key returns faster when the first byte is wrong, an attacker who can time it can recover the secret byte by byte. Inside one, every parameter is secret unless marked pub, and the checker rejects branching, indexing, division, trapping arithmetic and secret shift amounts on secret-derived values, as well as calls to non-ct functions. See Constant time.

Tools and the project

• SPEC-CARD: the whole language on one card, and the source of truth. Diagnostics cite its sections, as in error[card §8]. What is not on the card is not in the language. Its companion STD-CARD holds the standard library: the types, the capabilities' operations and SIMD.

• golden: the golden/ directory of normative example programs in the repository, from hello world to a sandbox and a VM-exit dispatcher. All of them compile and are tested.

• kola: the compiler, one binary with the standard library embedded. Its commands are check, run, test, build, ir, report, query, audit, pack, security, cc, lsp, mcp and help. See Under the hood.

• interpreter: the executor behind kola run and kola test, and the reference every backend is compared against. It runs with a JIT; --no-jit gives the pure tree-walker.

• differential test: kola test runs every test on the interpreter and on the C backend and compares the answers; a disagreement exits with code 3. --interp or --native runs one side alone.

• KIR: the verified intermediate representation every backend consumes, with each check's proof decision recorded in it. kola ir prints it. See IR-0.

• report checks: the list of every obligation in a file and whether it was proven at compile time or left as a run-time check. "0 runtime" is the bar for kernel-grade code. Siblings include reachable, leaks, regions, effects, secrets, tainted-reqs and stack-frames; kola help report lists them.

• seeded run: a run in which all nondeterminism (randomness, time, I/O order, thread scheduling) derives from one number. kola test --sim --seed N replays the same run bit for bit.

• simulator (--sim): capabilities replaced by deterministic doubles: a virtual clock, a seeded random source, a simulated filesystem and network with fault injection, an empty environment. Proc has no double; a granted spawn really runs.

• kola.pack: the package manifest: name, version, source root, dependencies, and the capability budget [caps] allowed with its per-name lists (fs_roots, proc_bins, devices, dial_hosts, netlink, the window lists and others). [caps.tests] and [caps.examples] widen it for tests and examples only. kola audit fails when code exceeds the budget. The budget limits what a pack may take from the root set; authority it receives as a parameter is listed separately on the audit's reaches: line.

• confusion log: docs/confusion-log.md in the repository, the record of constructs that people or models consistently get wrong. A construct that confuses is treated as a defect in the construct or in the card.