/
Search
EN

Effects and capabilities

kola is designed so that a reviewer can answer "what can this function do?" from its signature, without reading the body. Two parts of the type system make that possible. Effects say what kind of thing can happen ("it touches the outside world"). Capabilities say exactly what it can happen to ("this one directory and nothing else").

Effects: what kind

There are five effects, and the set is closed on purpose; the end of this section explains the test a new one would have to pass. The effect row goes after the return type and before any contracts.

row

means

reached through

!{}

pure: provably no allocation, no I/O, no blocking

nothing

alloc(r)

allocates into the region r

a region (and its Mem budget, if it has one)

io

touches the outside world through the operating system: files, sockets, streams, threads, the environment

a capability (Fs, Stdout, Dial, …)

hw

a privileged or ordering-sensitive machine operation: interrupt state, cache or TLB maintenance, a memory barrier, MMIO

Cpu or Mmio

block

may block or sleep

usually a capability

log

appends a diagnostic line to the process log

nothing; this is the one exception

ct is not on the list. It qualifies the function itself (ct fn ...) and takes freedom away rather than granting it; io and hw are both forbidden inside one. See Constant time.

use std::log;
use std::stdio;

// The effect row goes after the return type.
fn report(label: &str, value: u64) !{log} {
    log::info(f"{label}: {value}");
}

// A program's output is a different channel: bytes another program reads.
fn emit(out: &Stdout, line: &[u8]) -> Result[usize, (IoErr, OsErr)] !{io} {
    out.write(line)
}

fn main(sys: Sys) -> u8 !{io, log} {
    report("answer", 42);
    match emit(&sys.stdout, &b"42\n") {
        Ok(_) => 0,
        Err(_) => 1,
    }
}

A public function must declare its effects. For a private function the row may be left out, and the compiler infers it.

The checking rule is a single sentence, and it explains every refusal you will meet: a callee's effects must be a subset of the caller's. A function cannot get someone else to do what it is not allowed to do itself.

Caller

may call !{}

may call !{io}

may call !{io, block}

!{}

yes

no

no

!{io}

yes

yes

no: block is not declared

!{io, block}

yes

yes

yes

block deserves its strictness. A !{io} signature promises "I touch the world, but I do not wait". Code on a hot path, such as an interrupt handler or a dispatcher, can call such a function knowing it will not stall. Letting it make a blocking call would break that promise without anyone noticing. Here a pure function calls one that reads the clock:

error[card §6]: `pure_wants_io` performs `io` (call to `tick`) but does not declare it
  --> subset.kl:3:5
   |
 3 |     tick(c)
   |     ^^^^^^^
   = help: add `io` to the effect clause, or hand the work to a caller that has it

Changing what you were handed is not an effect. A pure function may modify whatever it receives through a &mut parameter. rng.weak_u64() advances the generator's state and is still !{}. Effects describe influence on the world beyond the arguments, the part you cannot see at the call site. If you pass a function a &mut, the possibility of change is already in the signature in front of you. (assert draws this line differently, for reasons covered in Contracts, traps, and tests.)

When does a concern earn an effect?

Effects are not a clean partition of everything a function might do. They overlap on purpose: log is a weak form of io, block usually comes with io but a non-blocking write is io without block, and hw is io restricted to the machine. The test for a new row is whether naming it separately tells a reviewer something they could not already read from the capabilities or the types. hw passes: Cpu and Mmio grant the right to touch hardware, but only the row says "this must not be reordered across a barrier". Other candidates have homes elsewhere. Nondeterminism is already marked by a Clock or Rng parameter. Fallibility belongs to contracts and Result, since nearly anything can trap. Secrecy and taint are types (Secret[T], untrusted). A finer split of io into network and filesystem would add nothing, because the capability already names the resource.

Talking and output are two channels

kola has no print. Instead it separates two things that most languages run together: the program talking, and the program's output.

Talking means a trace, a warning, "connected to 10.0.0.4". It goes to the log: use std::log; and then log::info(f"x={v}"). The effect is !{log}, and no capability is needed. There are four levels: error, warn, info and debug. A log call takes a &str; a plain "..." literal is text, and only an f"..." literal interpolates its {...} holes. Each hole is one expression, such as f"sum={a + b} point=({p.x},{p.y})"; there is no separate format-specifier syntax.

Output means bytes another program consumes, and it goes to a stream: sys.stdout.write(&bytes) returns Result[usize, (IoErr, OsErr)] with !{io}, and needs the Stdout capability. Its counterpart for input is sys.stdin.read_line(&mut buf), which returns Result[bool, (IoErr, OsErr)] with !{io, block} (Ok(false) is end of input). They are separate capabilities because "may this code read the console" and "may it write to it" are different questions for a reviewer. Diagnostics meant for whoever called the program, such as a compiler's file:line:col messages, go to sys.stderr, which has the same Stdout type.

The reason for the split is that stdout is a protocol. When you run prog | other, the shell connects prog's standard output to other's standard input, and other parses every byte it receives. A stray diagnostic in it does more than clutter the output: it corrupts the data for whatever is parsing the other end of the pipe. Run the program above and you can see the two channels separate:

$ kola run two-channels.kl
[info] answer: 42        <- stderr: the program talking (the default sink)
42                       <- stdout: the program's output

$ kola run two-channels.kl --log off > answer.txt
$ cat answer.txt
42                       <- only the output went through the pipe

The same flag can also send the log into the stream it was kept out of. With --log stdout the diagnostic lands inside the bytes a consumer parses:

$ kola run two-channels.kl --log stdout > answer.txt
$ cat answer.txt
[info] answer: 42
42

Which lines reach the sink at all is a separate setting: --log-level error | warn | info | debug (or KOLA_LOG_LEVEL). A level keeps itself and everything more severe. --log-level warn keeps error and warn; with no setting, the default is debug and everything gets through.

$ kola run level-demo.kl --log-level warn
[error] disk full
[warn] retrying connection

A level filter does not make a log call free. The line is built at the call site before the filter runs, so a log line inside a hot loop is formatted on every iteration whatever the level. Use static literals on hot paths.

hw: the machine, not the system call

io covers interaction with the world through the operating system: your program asks the kernel to do something with a system call (a syscall), such as read or write. Kernel and driver code also does something of a different kind, directly on the hardware. It masks interrupts, so the CPU will not jump to an interrupt handler in the middle of a critical step. It flushes a cache line, so that data the CPU wrote reaches main memory where a device can see it. It issues a memory barrier, an instruction that stops the CPU from reordering memory accesses across it. And it writes device registers through MMIO (memory-mapped I/O), where a device's control registers appear at memory addresses and a load or store talks to the device rather than to RAM. A cache flush performs no input and no output; what it means is coherence and ordering. Telling a kernel reviewer "this function does io" would say nothing about whether it touches the interrupt flag, so these operations have their own effect, hw.

// A device driver: `hw`, not `io`. Nothing here talks to the OS.
// These are register accesses whose order the device depends on.
const UART_DR: usize = 0x00;   // data register
const UART_FR: usize = 0x18;   // flags: bit 0 = receive FIFO not empty

pub fn uart_put(w: &MmioWindow, b: u8) !{hw}
    req w.len >= 0x20
{
    w.write8(UART_DR, b);
}

pub fn uart_ready(w: &MmioWindow) -> bool !{hw}
    req w.len >= 0x20
{
    (w.read32(UART_FR) & 1u32) != 0u32
}

hw is a separate effect, not a synonym. Declaring !{io} on uart_put is refused:

error[card §6]: `uart_put` performs `hw` (mmio write) but does not declare it
  --> uart.kl:7:5
   |
 7 |     w.write8(UART_DR, b);
   |     ^^^^^^^^^^^^^^^^^^^^
   = help: add `hw` to the effect clause, or hand the work to a caller that has it

One type uses both rows, which shows that the split follows consequences rather than the capability. A RamWindow is memory shared with hardware, such as the descriptor ring a network card reads to find out which packets to send. The card fetches that memory by DMA (direct memory access), without going through the CPU. Its ordinary reads and writes are !{io}, because they are just memory. Its DMA cache operations, dma_writeback and dma_invalidate, and its release-ordered writes are !{hw}, because only the row can say that another core or device depends on the ordering.

Capabilities: exactly what

A capability is a value with no public constructor; you cannot create a Clock from nothing. The runtime hands the root set to main and to nothing else. Here is all of it, as a program that takes each piece out of sys:

use std::log;

fn main(sys: Sys) -> u8 !{io, block, hw, log, alloc(heap)} {
    let _t: u64       = sys.clock.now();   // Clock: time
    let _r: Rng       = sys.rng;           // randomness
    let _f: Fs        = sys.fs;            // files under the working directory
    let _o: Stdout    = sys.stdout;        // the program's output
    let _e2: Stdout   = sys.stderr;        // diagnostics for the caller
    let _i: Stdin     = sys.stdin;         // the program's input
    let _a: Args      = sys.args;          // argv
    let _e: Env       = sys.env;           // the environment
    let _y: Tty       = sys.tty;           // the controlling terminal
    let _l: Dial      = sys.dial;          // outbound connections
    let _s: Listen    = sys.listen;        // inbound connections
    let _p: Ping      = sys.ping;          // unprivileged ICMP echo
    let _x: Proc      = sys.proc;          // spawning granted binaries
    let _w: Mmio      = sys.mmio;          // hardware windows
    let _c: Cpu       = sys.cpu;           // the CPU's privileged operations
    let _d: Dev       = sys.dev;           // device nodes
    let _g: Window    = sys.window;        // desktop windows and input
    let _n: Netlink   = sys.netlink;       // the kernel routing channel
    let _q: RawIp     = sys.raw_ip;        // raw IP egress (Linux)
    let _h: Inherited = sys.inherited;     // descriptors handed over by a parent

    // sys.mem: Mem is here too, but binding it like this does not compile.
    // The section on dropping capabilities explains why.
    log::info("that is the whole root set");
    0
}

sys also has two methods: sys.cores() answers how many cores this process may use, and sys.perturb(b"name") is a test hook that is false outside a test run that grants it. STD-CARD has a section on the operations of each capability.

From main, capabilities are passed down the call tree explicitly, usually as call-scoped views (&sys.clock), and each function gets exactly as much of the world as it was given:

use std::log;

enum Verdict { Clean, Suspicious }

// Hostile bytes in, a verdict out. No capabilities, and !{} is checked.
pub fn scan[r](payload: &r [u8]) -> Verdict !{} {
    let mut zeros = 0;
    for i in 0..payload.len {
        if payload[i] == 0 { zeros = zeros + 1; }
    }
    if zeros * 4 > payload.len { Verdict::Suspicious } else { Verdict::Clean }
}

// The only part that can say anything, and all it can do is log.
fn report(v: Verdict) !{log} {
    match v {
        Verdict::Clean => log::info("payload: clean"),
        Verdict::Suspicious => log::info("payload: suspicious"),
    }
}

fn main(sys: Sys) -> u8 !{io, block, alloc(heap), log} {
    region r {
        let good = alloc in r [1u8, 2u8, 3u8, 4u8];
        let bad  = alloc in r [0u8, 0u8, 7u8, 0u8];
        report(scan(good));    // report may log; scan gets nothing
        report(scan(bad));
    }
    0
}

This is attenuation: authority narrows at each step down. main holds the whole root set, report can append a line to a write-only log, and scan gets nothing. Capabilities also narrow themselves. Because a capability moves rather than copies, you mint a narrower one from the one you hold and keep the original: dial.to_host(host, port) reaches one endpoint, dir.ro() only the read operations, and clock.split(), rng.split() and dial.split() hand a worker its own.

Who does this protect against? Usually not a malicious colleague. The common cases are a function body generated by a model that nobody reads line by line, or a third-party parsing library upgraded together with its transitive dependencies. In both, a !{} signature with no capabilities means that whatever the body turns out to contain, it has nothing to send the parsed data with: no channel out, no allocation, no way to wait. An attacker who wants a function that does have a capability runs into the same property from the other side: such functions are few, and they can be listed. kola query attack-surface lists every capability a function is handed, including handles carried inside your own types (a &Session holding a Conn), along with the function values that cross the boundary and the returns that escape a region. Those signatures plus the package manifest are a small review surface.

If a program does not need randomness, do not pass sys.rng to anyone. Unused capabilities stay inside sys until main returns and are reclaimed by the runtime. A package can also be barred from whole classes of capability: a manifest with [caps] allowed = [] declares a pure-data pack, which may not hold a Clock, Rng, Fs or any other world capability anywhere in its code (see Packages). The list describes what the pack itself may take from the root bundle. An already-open handle that a caller passes in, such as a Conn, is accounted to the caller who opened it, and kola audit lists such values on the pack's public signatures separately.

Grants: the operator decides

Some things a program may need are, by design, not something the program can name: a directory outside the working directory, a window of physical memory, a range of x86 I/O ports (a separate address space older devices such as serial ports use), a device node (a file under /dev that stands for a driver), a device minted from a mounted filesystem, an external binary to run. All of them use one pattern.

  1. The operator names the grant when launching the program, outside the source: --fs-root db:ro=/srv/db, --ram-window ring0=0x1000:0x100, --mmio-window uart0=0x0900_0000:0x1000, --io-window uart=0x3f8:8, --device widget=/dev/widget:map=4096:ioctl=0x80384b01, --dev-mint vol0=/mnt/data:mint=0x80384b01:map=4096, --proc-bin ffmpeg=/usr/bin/ffmpeg. Each flag has an environment twin (KOLA_FS_ROOT_db, KOLA_PROC_BIN_ffmpeg, and so on). Grants come only from the operator. An environment key with one of these prefixes, passed to a child through sys.proc.spawn, traps, so a program cannot create authority for its child.

  2. The program looks the grant up by name and gets an Option: sys.fs.root(b"db"), sys.mmio.ram(b"ring0"), sys.mmio.window(b"uart0"), sys.mmio.io_window(b"uart"), sys.dev.open(b"widget"). An unknown name is None, not an error, so "I was not granted this" is an ordinary branch. An operation that does the work itself answers with its error family instead: sys.dev.mint(..) returns a Result, and spawning an ungranted binary is Err(NotGranted).

  3. A package declares which names it may ask for, per kind: [caps] fs_roots, ram_windows, mmio_windows, io_windows, devices, proc_bins. kola audit checks it, so for a shipped image you can say exactly which nodes each pack opens.

  4. Read-only access is a separate type, never a flag: DirRo beside Dir, RamWindowRo beside RamWindow. The write operations do not exist on the narrow type, so a read-only consumer that tries to write fails to compile.

use std::fs;
use std::log;

// An unknown grant name is None, so a program that was not granted
// `db` takes a branch rather than a failure path.
fn main(sys: Sys) -> u8 !{io, block, log, alloc(heap)} {
    match sys.fs.root_ro(b"db") {
        Some(d) => {
            match d.open_read("index") {
                Ok(fh) => {
                    log::info("db/index opened");
                    let _ = fh.close();
                }
                Err(_) => log::warn("db/index missing"),
            }
            0
        }
        None => { log::warn("no db grant, running without it"); 0 }
    }
}

The same binary behaves two ways, and the choice is made by whoever runs it:

$ kola run grant.kl --fs-root db:ro=/tmp/demo/db
[info] db/index opened

$ kola run grant.kl
[warn] no db grant, running without it

Point 4 in practice: w.ro() narrows a RAM window to its read half. Taking less authority is always safe, so it needs no grant. The result is a type on which the write operations do not exist:

error[card §7]: `RamWindowRo` is the READ-ONLY half of a RAM window — `write32` writes, and the write half does not exist on this type
  --> ro.kl:3:5
   |
 3 |     ro.write32(0, 1u32);
   |     ^^^^^^^^^^^^^^^^^^^
   = help: `w.ro()` ATTENUATES a `RamWindow`: the result carries `read8/16/32/64`, `copy_out`, `.len` and `snapshot`, and nothing that mutates — so a seqlock reader that writes cannot compile. Write through the full window `w` instead, or if this code should not hold one, take a `&RamWindowRo` parameter and let the caller keep the writable half

A few details about the hardware grants. In a hosted run, an MMIO or I/O-port window is backed by a simulated device model (--sim-mmio, --sim-io): a few pure kola functions over your own state struct, so the device's behaviour is the function body. A window granted without a model is refused at startup rather than reading zeros. A RAM window needs no model, since plain memory is its own model. A --device grant without a model (--sim-dev) opens the real node under kola run and is refused under kola test, where a real ioctl would read the host. A Device is a linear handle whose operations are limited by its grant. Drivers are mostly controlled through ioctl, a system call that sends a numbered command to a device; an ioctl code that is not on the grant's allowlist is Err(Denied) before the device is touched. A device can also be minted from a granted mount with sys.dev.mint(b"vol0"), which performs the open, ioctl and close inside the runtime; the mint operation belongs to the grant and does not exist on a handle. Proc applies the same pattern to programs: sys.proc.spawn(b"ffmpeg", argv, env, disp, slots) runs the binary the operator bound to that name, and nothing crosses into the child (environment, open descriptors) beyond what the call passes. The command-line chapter works through it.

Which capabilities may be dropped

Capabilities are resources, and the resource rule (see Resources and linearity) says a resource must be consumed exactly once on every path. Some capabilities are exempt, and which ones follows from a single question: does the capability own anything?

  • An authority token owns nothing but permission: Clock, Rng, Fs, Dir, DirRo, Dial, Listen, Stdout, Stdin, Args, Env, Tty, Ping, Proc, Mmio and its windows, Cpu, Dev, Window, and sys itself. Drop one on any path; the runtime reclaims it.

  • A quantity (Mem) or a linear handle (File, Conn, Device, Child, RawMode, …) may not be dropped. Losing one would lose budget or leak a descriptor, so the ordinary rule applies.

The compiler answers this from one registry of capabilities, so a capability added later lands on the correct side without anyone updating a list. Two tests show the rule:

// Authority tokens may be dropped: there is nothing to reconcile.
test tokens_may_simply_be_dropped(mut sim: Sim) {
    let clock = sim.clock;
    let rng   = sim.rng;
    let env   = sim.env;
    let term  = sim.tty;
    assert true;              // none of the four is consumed, and that is legal
}

// A budget is a quantity: dropping a Mem split would lose memory.
test a_budget_must_come_back(mut sim: Sim) {
    let m: Mem = sim.mem.split(4096);
    sim.mem.absorb(m);        // delete this line and the test does not compile
    assert true;
}
error[card §2]: resource `m` is not consumed on this path
  --> rule.kl:13:5
    |
 13 |     let m: Mem = sim.mem.split(4096);
    |     ^^^
    = help: no implicit destructors: move it on, return it, destructure it, or pass it to a consuming fn

Memory budgets

use std::log;

fn main(mut sys: Sys) -> u8 !{io, block, alloc(heap), log} {
    let small: Mem = sys.mem.split(1048576);
    region r from small {
        let v: &r mut Vec[u64] = alloc in r mut Vec::new();
        v.push(42);
        log::info(f"v[0]={v[0]}");
    }   // r is closed and its charge is refunded to small
    sys.mem.absorb(small);
    0
}

Budgets make a memory-hungry component fail where the problem is. Without them, when the machine runs out of memory, the operating system's OOM (out-of-memory) killer picks a process and ends it, often somewhere far from the cause. With them, exceeding a budget is a deterministic trap that points at the culprit. There are two ways to exceed one, and both are checked:

$ kola run overdraw.kl                       # carving more than you hold
trap: error[card §7]: memory budget exceeded in split
  --> overdraw.kl:3:21
   |
 3 |     let tiny: Mem = small.split(4096);
   |                     ^^^^^^^^^^^^^^^^^

$ kola run overshoot.kl                      # outgrowing it inside the region
trap: error[card §7]: memory budget exceeded in region
  --> overshoot.kl:7:13
   |
 7 |             v.push(1u64);
   |             ^^^^^^^^^^^^

Forgetting absorb is caught at compile time by linearity. A plain region r with no from is unbounded and draws from whatever backs the enclosing region, so a plain region nested in a budgeted one is charged to the same budget. The interpreter charges simulated sizes and a native build charges its real arena's bytes, so the two agree on whether a budget is exceeded at a comfortable margin, not on the exact byte. kola test --sim reports each region's peak (see Memory: regions and references).

Determinism

All of a program's nondeterminism (time, randomness, I/O order, thread scheduling) flows through capabilities, so it can be replaced wholesale. kola test --sim --seed N gives tests a seeded set of capabilities: every source of randomness starts from one number, the seed, and produces the same sequence on every run. The same seed gives the same run. A failing test prints its seed, FAILED (seed 1802464353), and passing that to --seed reproduces the failure on your machine.

Capabilities that read the outside of the process follow the same substitution. sys.env is empty under test and --sim, so a test cannot depend on the shell that ran it, and sys.rng is seeded per test rather than drawing OS entropy. One capability has no simulator: a granted sys.proc.spawn really runs the binary, under test too.

A seeded generator is what a test wants and what a key must never come from. Rng::weak_u64 is a fast stream seeded once, and anyone who sees one output can predict the rest. A value an adversary must not guess (a key, a token, a salt, an ephemeral secret) comes from Entropy::draw[[u8; 32]](&mut rng) or rng.fill_os(&mut buf), which read OS entropy (unpredictable bits the kernel collects from hardware events) on every call; Entropy::draw also records that origin in its type. Under test and --seed they fall back to the seeded stream on purpose, so a pinned run replays exactly and its keys are test keys. Cryptography has the full rule.

// Exponential backoff with jitter. Jitter does not need to be unpredictable.
pub fn retry_after(rng: &mut Rng, attempt: u32) -> u64 !{}
    req attempt < 16
    ens ret < 1024
{
    let exp: u64 = if attempt < 9 { 1u64 << attempt } else { 512 };
    let jitter = rng.weak_u64() % exp;
    exp + jitter
}

// (mut sim: Sim) gives the test a seeded capability set:
// sim.rng is seeded, sim.clock is virtual, sim.env is empty.
test backoff_is_bounded(mut sim: Sim) {
    let mut attempt: u32 = 0;
    while attempt < 16 {
        let d = retry_after(&mut sim.rng, attempt);
        assert d < 1024;
        attempt = attempt + 1;
    }
}

test env_is_empty_under_test(mut sim: Sim) {
    assert sim.env.get(b"HOME").is_none();
}

The normative reference is SPEC-CARD §6 and §7 (kola help spec-card); each capability's operations are in STD-CARD.