/
Search
EN
ENRU

Contracts, traps, and tests

kola separates two kinds of failure and never lets them mix. Expected failures (bad input, a busy port, a short frame) are values: Result and Option, handled by ordinary code. A violated assumption of the program itself (an overflow, an out-of-bounds index, a false contract) is a trap, a deterministic halt. There are no exceptions, no null and no stack unwinding (the mechanism by which C++ exceptions and Rust panics run cleanup code in every function on the way up the call stack).

Result, Option and the ? operator

enum ParseErr { Short }

fn rd16_manual[r](b: &r [u8]) -> Result[u16, ParseErr] !{} {
    if b.len < 2 { return Err(ParseErr::Short); }
    Ok((widen[u16](b[0]) << 8) | widen[u16](b[1]))
}

fn parse_pair[r](b: &r [u8]) -> Result[(u16, u16), ParseErr] !{} {
    if b.len < 4 { return Err(ParseErr::Short); }
    let x = rd16_manual(b[0..2])?;
    let y = rd16_manual(b[2..4])?;
    Ok((x, y))
}

e? looks at a Result. On Ok(v) the expression's value is v; on Err(e) the current function returns Err(e) at once. So ? works only on a Result, inside a function that returns a Result with a compatible error type:

error[card §3]: `?` applies to Result, found `u64`
  --> q.kl:2:13
   |
 2 |     let y = x?;
   |             ^

Because ? is an early return, a resource still live at the ? is a compile error: the Err path would lose it (see Resources and linearity). Consume it first, or use an explicit match.

Ignoring a Result is also a compile error. Handle it with match, ? or .unwrap(), or discard it on purpose with let _ = ...;. Option is exempt: a None is an answer, while an ignored Err is a failure nobody looked at.

unwrap: a deliberate "this cannot happen here"

.unwrap() takes the value out of an Option or Result and traps on None or Err. It is a claim in the code: the author states that the other case is impossible and accepts a loud halt if they are wrong. Like any by-value use, it moves its receiver.

test unwrap_when_proven {
    let v: Option[u64] = narrow[u64](12u64 * 5);
    // 60 always fits in a u64, so None cannot happen here
    assert v.unwrap() == 60;
}

If the impossible happens anyway, the trap names the spot:

trap: error[card §3]: unwrap on `None`
  --> u.kl:3:13
   |
 3 |     let v = o.unwrap();
   |             ^^^^^^^^^^

Over external data, use match or ?. Keep unwrap for cases that are provably impossible (say why in a comment) and for tests, where a failure is the signal you want.

What a trap is and what it kills

A trap happens on arithmetic overflow, division by zero, a shift by the operand's width or more, an out-of-bounds access, a violated contract or invariant, an exhausted memory budget, or an explicit trap("msg"). A program whose assumption turned out false does not keep running with bad data in hand.

trap: error[card §3]: explicit trap: n out of range
  --> t.kl:3:16
   |
 3 |     if n > 2 { trap("n out of range"); }
   |                ^^^^^^^^^^^^^^^^^^^^^^

What halts is the fault domain, by default the whole process. The operating system then reclaims what the process held, such as its file descriptors (the small integers the OS uses to name open files and sockets), which is sound because linearity only promised consumption on normal paths. Under kola test a trap fails only its own test, which prints FAILED (seed N). A program can also narrow the domain itself.

domain and recover

Recall that a region is a block that owns a private pool of memory (an arena); everything allocated in it is freed at once at the closing brace. domain d { … } recover(t: Trap) { … } is a region that also catches. It is a region in the full sense of Memory: regions and references, with the same escape rules and the same from m backing. That is what makes catching sound: tearing down the arena is the cleanup, and there is no unwinding to stop halfway.

use std::log;

// A request handler whose fault domain is one request, not the process.
pub fn serve(payload: &[u8]) -> u32 !{log} {
    let mut status: u32 = 200u32;
    domain d {
        // a deliberate bug: the caller may send fewer bytes than this reads
        let b = payload[7];
        status = widen[u32](b);
    } recover(t: Trap) {
        status = 500u32;
        log::error(f"request died: {t.kind} at {t.site}");
    }
    status
}

test a_trap_kills_the_request_not_the_process {
    assert serve(&b"short") == 500u32;    // the domain caught it
    assert serve(&b"long enough.") == 111u32;
    // and the process is still here to run this line
}

Under kola test --sim, which prints the log lines of passing tests, the first call logs:

log[error] request died: Bounds at serve.kl:8

The rules:

  • recover is mandatory, and it runs only on a trap. A return or break leaves the block like a plain region and does not trigger it.

  • Trap is plain data. t.kind is a TrapKind: Bounds, Arith, Req, Ens, Inv, Assert, Unwrap, Explicit, Budget or Capacity. Budget means a memory budget ran out; Capacity means a fixed bound was reached, such as a Pool with every slot live. (shed load, or refuse this one item). t.site is a module:line string such as serve.kl:8, never a filesystem path of the build machine.

  • A trap inside recover is fatal. No domain catches it, not even an outer one.

  • A linear resource may not live inside a domain (authority tokens such as Clock are exempt): a trap would strand it, and there are no destructors. Domains compute over data.

error[card §3]: `m`: a linear resource may not live inside a `domain` — a trap would strand it
  --> dom.kl:3:9
   |
 3 |         let m: Mem = sys.mem.split(1024);
   |         ^^^
   = help: domains compute over data; move this resource outside the domain, or consume it before entering

Contracts: req and ens

A contract is a checkable condition written into the signature. req is a precondition, the caller's obligation: "call me only like this". ens is a postcondition, the function's promise about its result, which it names ret. Each keyword takes a comma-separated list of conditions:

fn sum_range(xs: &[u64], a: usize, b: usize) -> u64 !{}
    req a <= b, b <= xs.len
{
    let mut s: u64 = 0;
    let mut i = a;
    while i < b {
        s = s +% xs[i];
        i = i + 1;
    }
    s
}

fn clamp100(x: u64) -> u64 !{}
    ens ret <= 100
{
    if x > 100 { 100 } else { x }
}

A contract is always enforced. If the compiler can prove it, the check disappears from the generated code; if not, a run-time check that traps stays in. No build mode turns contracts off, unlike C's assert or Rust's debug_assert. A violated req:

trap: error[card §8]: req violated calling `sum_range`
  --> rq.kl:2:17
   |
 2 |     req a <= b, b <= xs.len
   |                 ^^^^^^^^^^^
   = help: contracts are always enforced: proven statically or trapped at runtime

Indexing xs[i] and slicing xs[a..b] carry built-in req bounds contracts, so an out-of-bounds access is one more violated contract. A guard upstream (if i < xs.len) discharges it statically. In sum_range, the loop condition i < b together with req b <= xs.len proves i < xs.len, and the compiled code has no bounds check in the loop. The compiler contains a small prover, a component that tries to show from the code itself that a condition can never be false; this is such a proof, not a heuristic (see Under the hood).

report checks: what is left at run time

"Proven or trapped" is useful only if you can see which one you got. kola report checks lists every obligation in a file and how it was discharged. Here it is on the two functions above:

$ kola report checks contracts.kl
fn sum_range
  proven   xs[i]  [proved i < xs.len from req+guards]
  proven   i + 1usize  [sum bounded by width]
fn clamp100
  proven   ens at tail  [ens discharged at this exit]

1 index site(s): 1 proven at compile time, 0 runtime
1 arith site(s): 1 proven at compile time, 0 runtime
1 ens exit(s): 1 proven at compile time, 0 runtime

(The header and the two closing lines of the real output are trimmed here.) Now remove the req line and ask again. The program still works and is still memory-safe, but the proof is gone, so the bounds check runs on every iteration:

$ kola report checks unguarded.kl
fn sum_range_weak
  RUNTIME  xs[i]
  proven   i + 1usize  [sum bounded by width]

1 index site(s): 0 proven at compile time, 1 runtime
1 arith site(s): 1 proven at compile time, 0 runtime

This is the working method for hot paths: strengthen the req and add guards until the runtime column reads 0. The bounds checks are then absent from the emitted code, because the compiler proved they can never fire. A kernel datapath or a cipher's inner loop gets fast this way, by earning the removal of each check rather than switching checks off.

assert, and why it must be repeatable

assert EXPR; is a checkable claim in the middle of code, with the same discharge rule as a contract: proven and removed, or checked and trapping. Invariants of resource structs (inv) are covered in Resources and linearity.

The rule that catches people: the expression must not mutate anything. Bind the result first, as in let ok = q.push(1); assert ok;. It looks like an effect rule, but it is not one, and the diagnostic says so:

error[card §8]: assert expression mutates state (calls `bump`, which writes through `g.level`)
  --> as.kl:5:5
   |
 5 |     assert bump(&mut v);
   |     ^^^^^^
   = help: `mutates` is not the effect row's sense — a write through a `&mut` param is effect-PURE (§6) and this rule still refuses it. A PROVEN assert is ELIDED, so its expression must be repeatable and must mean the same thing in the build where it never runs. Bind first — let ok = x.f(); assert ok;

For the effect row, writing through a &mut parameter is pure, because the caller can see it in the signature (see Effects and capabilities). But an assert that the prover discharges is deleted, so a mutating one would make the program's meaning depend on how much the prover managed to prove. The rule follows what the callee's body does, not how its parameters are declared.

untrusted: a contract may not depend on attacker bytes

A req lowers to a trap, so a req that an attacker can falsify is a remote kill switch. Take a packet decoder with req packet.len >= 32, where packet is a UDP payload. A crafted 20-byte datagram violates the contract and traps, and on a freestanding build (a program running without an operating system, such as a router's packet path) one packet halts the whole router before any authentication.

A req is a claim about the caller, and bytes off the wire have no caller. Mark such a parameter untrusted and the checker enforces the distinction:

// A packet off the wire. This does not compile.
pub fn decap(untrusted packet: &[u8]) -> Option[u64] !{}
    req packet.len >= 32
{
    Some(widen[u64](packet[0]))
}
error[card §8]: `req` depends on untrusted input `packet`
  --> un.kl:2:9
   |
 2 |     req packet.len >= 32
   |         ^^^^^^^^^^^^^^^^
   = help: this `req` depends on untrusted input `packet`; return `Result`/`Option` and check at runtime, or remove the `untrusted` marker if this param is not attacker-controlled
// The repair: check the length at run time and answer with a value.
pub fn decap(untrusted packet: &[u8]) -> Option[u64] !{} {
    if packet.len < 32 { return None; }
    Some(widen[u64](packet[0]))
}

test a_short_packet_is_refused_not_fatal {
    assert decap(&b"too short").is_none();
}

The repair weakens nothing: the length is still checked before the first byte is read, and the function answers with a value instead of killing the process. untrusted sits beside Secret[T] and ct (see Constant time) as kola's ways of marking how far data can be trusted. For code not yet marked up, kola report tainted-reqs lists every req that constrains a shared slice or array parameter. It is a triage list: the compiler cannot tell an inbound packet from your own outbound buffer by type alone.

Tests

enum ParseErr { Short }

fn rd16_manual(b: &[u8]) -> Result[u16, ParseErr] !{} {
    if b.len < 2 { return Err(ParseErr::Short); }
    Ok((widen[u16](b[0]) << 8) | widen[u16](b[1]))
}

test parse_short_frame {
    region r {
        let b = alloc in r [1u8];
        assert rd16_manual(b) == Err(ParseErr::Short);
    }
}

// seeded capabilities: sim.rng, sim.clock, sim.fs, ...
test seeded_rng(mut sim: Sim) {
    let a = sim.rng.weak_u64();
    let b = sim.rng.weak_u64();
    assert a != b;
}

Tests live next to the code and run with kola test file.kl (a directory is walked recursively). --test <substring> selects tests by name; a substring that matches nothing is an error listing the names. A test that needs capabilities declares (mut sim: Sim) and receives a seeded set with the same fields as Sys: a virtual clock, a deterministic random source, a simulated filesystem. A failing test prints its seed, and --seed N reproduces the failure exactly. A test may instead declare (mut sys: Sys); it is then live, with real sockets and a real clock, and only sys.rng stays seeded.

--sim adds fault injection and reports each region's peak memory:

$ kola test --interp --sim --seed 7 tests.kl
tests.kl: test parse_short_frame ... ok
    region r: 1 bytes region-charged high-water (arena-faithful)
tests.kl: test seeded_rng ... ok

2 passed, 0 failed (interpreted, JIT backend)

kola has two ways to execute a program. The interpreter runs the source directly and is the reference for what a program means. The C backend translates the program to C and compiles it with a C compiler, which is how you build what you ship. By default kola test runs every test on both, compares them file by file and exits with status 3 if they disagree. --interp runs the interpreter alone and needs no C compiler: the fast loop while you work. --native runs only the C build, each test in its own process.

A test that asserts nothing passes whether or not anything ran, so kola check warns about it; write expects 0 when "it does not trap" is the whole claim. In general test name expects N { … } requires exactly N asserts to execute (including those in functions it calls), so a clause that an empty input skipped turns the test red:

test three_claims expects 3 {
    let xs = [1u64, 2u64, 3u64];
    assert xs[0] == 1;
    assert xs[1] == 2;
    assert xs.len == 3;
}

The normative reference is SPEC-CARD §3, §8 and §10 (kola help spec-card).