Region leaks: the report, the budget, and what it cannot see

A region frees its memory at its closing brace and not a moment earlier. That is the whole memory model from Memory: regions and references, and it has one failure mode. Each region is backed by an arena: a block of memory that hands out space one allocation after another and has no way to give back a single piece. So if a loop allocates on every pass into a region the loop body did not open, every one of those allocations stays until that outer region closes. The program grows for as long as the region lives.

This is a real bug, not a theoretical one. An HTTP server written in kola started at 2 MB of resident memory (RSS, the memory the OS actually has mapped for the process) and reached 799 MB after 573,000 requests, because each request's buffers were allocated in the connection's region, which lives as long as the connection does. The code was memory-safe throughout: every reference pointed at live, correctly typed memory. The problem was placement, not safety.

kola can see the shape of that bug without running the program, because every allocation names its region (alloc in r, effect !{alloc(r)}) and the compiler's verified IR (the internal form the prover works on) keeps the loop structure. kola report leaks FILE.kl walks that IR and lists the suspicious sites.

The report

Here is the bug in a few lines: a connection handler whose region r belongs to the connection, and one buffer per request.

// `hello` lives in the connection's region `r`, and so does every request buffer.
fn serve[r](hello: &r [u8], n: u64) -> usize !{alloc(r)} {
    let mut total: usize = 0;
    for i in 0..n {
        let buf: &r mut Vec[u8] = alloc in r mut Vec::new();
        buf.push(hello[0]);
        total = total + buf.len;
    }
    total
}

test serves_every_request {
    region conn {
        let hello = alloc in conn [7u8, 8u8];
        assert serve(hello, 3) == 3;
    }
}

The test passes and kola check is silent. Nothing here breaks a rule the checker enforces: r belongs to the caller, so every buffer is alive and every &r reference is valid for as long as it is used. The leak report asks a different question:

$ kola report leaks serve.kl
kola report leaks — candidate region-leak sites inside loops
(a preamble explaining each class, and the rule that a site count must be
 read together with the DE-ANALYZED list)
fn serve
  fresh  Vec::new  [the fn's own region (bound before this loop)]  — repair: open a per-iteration region: `region rq { .. }`
not analyzed `test serves_every_request`: test items run on the interpreter — any allocation inside it (loop or not) is invisible to this report

1 candidate leak site(s): 1 fresh, 0 grow, 0 mint

A finding names the function, the class (fresh here), the site as the compiler sees it, why it is a candidate (the region was bound before this loop), and the repair. You do not have to remember to run the report: kola test prints a hint when there is something to see.

$ kola test --interp serve.kl
serve.kl: test serves_every_request ... ok

1 passed, 0 failed (interpreted, JIT backend)
note: 1 candidate region-leak site(s) inside loops — run `kola report leaks serve.kl` (see `kola help ai`)

The repair

Open a region inside the loop and allocate into that one. It is freed at the end of every pass, which is the lifetime the buffer wanted in the first place:

// The same loop, repaired: the buffer lives in a region opened inside the loop.
fn serve[r](hello: &r [u8], n: u64) -> usize !{alloc(r)} {
    let mut total: usize = 0;
    for i in 0..n {
        region rq {
            let buf: &rq mut Vec[u8] = alloc in rq mut Vec::new();
            buf.push(hello[0]);
            total = total + buf.len;
        }
    }
    total
}

test serves_every_request {
    region conn {
        let hello = alloc in conn [7u8, 8u8];
        assert serve(hello, 3) == 3;
    }
}

0 candidate leak site(s): 0 fresh, 0 grow, 0 mint

The signature, the caller, the test and the result are unchanged. The whole edit is where the bytes live. In a region language a memory-growth bug is a placement bug, and placement is local and visible in review.

A per-iteration region repairs the fresh class, but not every class. The report prints the repair that matches what it found, such as resetting a growing buffer or giving each recursive call its own region, so read the line rather than applying one idiom everywhere.

Four shapes

Class	What it means	How likely a real leak
`fresh`	a new value is created every iteration: an allocation in the loop, or a call to a function that allocates and returns the value	near-certain
`grow`	a `push`, or a call that may push, into a `Vec` bound before the loop and never reset inside it	worth a look
`mint`	an interpolated string (`f"req={i}"`) or `f64::to_str` created every pass into a region the loop did not open, or onto `heap` if none is open	near-certain
recursion	a function in a call cycle that allocates into a region it did not open: a loop with no loop in the source	near-certain

An f"..." passed straight to a parameter of type &str is built in a temporary buffer and allocates nothing, so log::info(f"req={i}") in a loop is not listed. Binding it is: let s: &r str = f"req={i}"; inside the loop is a mint site.

fresh, including through a call

The example above wrote its alloc in the loop body, which you could have found by reading. The HTTP server's bug did not look like that: its loop contained no allocation at all, and its helper functions did. The report follows calls:

fn enc_msg[r](conn: &r [u8], n: u64) -> &r Vec[u8] !{alloc(r)} {
    let v: &r mut Vec[u8] = alloc in r mut Vec::new();
    v.push(wrap[u8](n));
    v
}

fn push64le[r](out: &r mut Vec[u8], v: u64) !{alloc(r)} {
    for i in 0..8u64 {
        out.push(wrap[u8](v >> (i * 8)));
    }
}

// holds no `alloc` of its own
fn frames[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
    let mut total: usize = 0;
    for i in 0..n {
        let msg = enc_msg(conn, i);
        total = total + msg.len;
    }
    total
}

fn stream[r](sink: &r mut Vec[u8], n: u64) -> usize !{alloc(r)} {
    for i in 0..n {
        push64le(sink, i);
    }
    sink.len
}

test both expects 2 {
    region r {
        let conn = alloc in r [0u8; 4];
        assert frames(conn, 3) == 3;
        let s: &r mut Vec[u8] = alloc in r mut Vec::new();
        let n = stream(s, 2);
        assert n == 16;
    }
}

fn frames
  fresh  enc_msg(conn, i)  [the fn's own region (bound before this loop) via call to `enc_msg`]  — repair: open a per-iteration region: `region rq { .. }`
fn stream
  grow  push64le(sink, i)  [the fn's own region (bound before this loop) via call to `push64le`]  — repair: open a per-iteration region: `region rq { .. }`

2 candidate leak site(s): 1 fresh, 1 grow, 0 mint

The two callees are classified by their signatures, not by reading their bodies. enc_msg returns a value in the region, so each call creates something new: fresh. push64le takes a Vec and may extend it: grow. (stream binds the result before asserting on it because an assert expression may not call something that writes through a &mut.)

grow, the quieter class

Accumulating into one buffer is often exactly what the code means to do, so this class is a question rather than an accusation. A direct .push into a Vec the function itself allocated in an outer region, with no .clear() or .truncate() on that handle anywhere in the loop, is flagged. Add the reset and it goes quiet:

// `grow`: a Vec this fn allocated in the connection's region, pushed every pass.
fn collect[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
    let acc: &r mut Vec[u8] = alloc in r mut Vec::new();
    for i in 0..n {
        acc.push(conn[0]);
    }
    acc.len
}

// The same shape with a reset on the same handle: the capacity is reused,
// and the report stays quiet.
fn batched[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
    let acc: &r mut Vec[u8] = alloc in r mut Vec::new();
    let mut total: usize = 0;
    for i in 0..n {
        acc.push(conn[0]);
        total = total + acc.len;
        acc.clear();
    }
    total
}

test both_count_the_same expects 2 {
    region r {
        let conn = alloc in r [1u8];
        let a = collect(conn, 4);
        let b = batched(conn, 4);
        assert a == 4;
        assert b == 4;
    }
}

fn collect
  grow  acc.push(conn[0usize] [checked])  [grows a handle bound before this loop, never cleared/truncated]  — repair: reset the handle each pass (`.clear()`/`.truncate()`) or bound its size

1 candidate leak site(s): 0 fresh, 1 grow, 0 mint

batched is not just unflagged, it is correct. clear() sets the length to zero and keeps the capacity, the space the Vec has already reserved, so refilling it costs the region nothing more. The kola test --sim high-water report described in the Memory chapter shows the same accounting. If a function returns the Vec it filled, the value leaves with the result and the site is not flagged either.

recursion

A recursive walk has no loop for the report to find, and it accumulates just as fast. A function in a call cycle that allocates into a region it did not open, in a block that also makes the recursive call, is reported:

// Recursion is a loop with no loop node.
fn scan[r](depth: u64, out: &r mut Vec[u8]) !{alloc(r)} {
    if depth == 0 {
        return;
    }
    let scratch: &r mut Vec[u8] = alloc in r mut Vec::new();
    scratch.push(1u8);
    out.push(2u8);
    scan(depth - 1, out);
}

test scan_walks {
    region r {
        let out: &r mut Vec[u8] = alloc in r mut Vec::new();
        scan(3, out);
        assert out.len == 3;
    }
}

fn scan
  fresh  Vec::new  [recursion cycle through `scan` — allocates into a region it did not open]  — repair: give each call its OWN region (`region rq { .. }`) or return the value

1 candidate leak site(s): 1 fresh, 0 grow, 0 mint

This is deliberately conservative. A recursive tree builder, such as a parser whose nodes flow into the returned syntax tree, allocates into the caller's region on purpose and is not flagged, because the value escapes. A per-call region rq { .. } is not flagged either. What remains is scratch that is filled, dropped and recursed past: real accumulation.

What the report cannot see

The walk runs over the verified IR, and not every function reaches it. Some constructs have no IR form yet; a domain block is one, and a function that uses one is outside the analysis. Such a function is never silently dropped. It is listed with the reason, and that list is part of the result.

A caller of an unanalysed function loses its own analysis too. This is reported as de-analysed, and the closing line refuses to let a zero look clean:

use std::trap;

// A `domain` block keeps this fn out of the verified IR.
fn guarded[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
    let mut total: usize = 0;
    for i in 0..n {
        let buf: &r mut Vec[u8] = alloc in r mut Vec::new();
        buf.push(conn[0]);
        domain d {
            total = total + buf.len;
        } recover(t: Trap) {
            total = 0;
        }
    }
    total
}

fn serve[r](conn: &r [u8], n: u64) -> usize !{alloc(r)} {
    guarded(conn, n)
}

$ kola report leaks dom.kl
...
de-analyzed `guarded`: `domain`/`recover` has no KIR lowering, so the prover cannot see inside it — ... — its leak sites are UNCHECKED (a reachable body left the IR-v0 subset); NOT counted below
de-analyzed `serve`: call to `guarded` which is outside IR-v0 — its leak sites are UNCHECKED (a reachable body left the IR-v0 subset); NOT counted below
0 candidate leak site(s): 0 fresh, 0 grow, 0 mint — ⛔ 2 fn(s) DE-ANALYZED, their leak sites UNCHECKED, so this count is NOT a clean bill of health

guarded has the same leak as the first example, and the count is zero. The report is not wrong: it says the function was never examined. A zero count next to a non-empty de-analysed or not-analysed list means nothing was checked, not that nothing was found. If you gate a build on this report, gate on the count and the de-analysed list together.

The other limits:

If fn main is skipped, the report says so prominently. A server's accept and serve loops usually live in main, so a report that cannot see it is blind where this class does the most damage.
test items are always listed as not analysed. They run on the interpreter, so allocations inside them are invisible here.
A grow finding names the region in scope at the call site. That is a heuristic: once a Vec handle exists, the IR no longer records which region its storage came from.
A .push into a buffer passed in as a parameter is never flagged. Appending to a buffer the caller owns is what every encoder does, and false alarms would train reviewers to skim past the tool.

The machine-readable form

--format json (or --json) prints the same walk for a script or an agent. The prose and the JSON come from one walk, so they cannot disagree.

$ kola report leaks --format json grow.kl
{"file":"grow.kl","report":"leaks","main_unchecked":null,
 "fns":[{"fn":"collect","sites":[{"class":"grow","site":"acc.push(conn[0usize] [checked])",
   "why":"grows a handle bound before this loop, never cleared/truncated",
   "repair":"reset the handle each pass (`.clear()`/`.truncate()`) or bound its size"}]}],
 "syntactic":[],"de_analyzed":[],
 "not_analyzed":[{"name":"test both_count_the_same","why":"test items run on the interpreter"}],
 "totals":{"fresh":0,"grow":1,"syntactic_loop_alloc":0,"syntactic_aliased_region":0,"mint":0}}

Read de_analyzed and not_analyzed before totals. A script that reads only the totals reproduces exactly the false all-clear the report works to prevent.

Pinning it: the [leaks] budget in kola.pack

A report is something you run; a budget is something that fails the build. A pack opts in by adding a [leaks] section to its kola.pack (see Packages). kola audit then runs the same analysis over the pack's own sources, with the prover fully discharging bounds checks first, and exits with status 1 on any unacknowledged site. That full discharge can take minutes on a large pack, and the audit says so when it starts. Without a [leaks] section the leak lines are informational and never fail.

Audit the pack directory, not a single file. kola audit <file> prints the same lines for that file's closure but says the budget was not enforced, because the budget is a claim about the whole pack.

[pack]
name = "leakdemo"
version = "0.1.0"
src = "src"

[caps]
allowed = []

[leaks]
acknowledged = []

Put the first serve function from this chapter in src/lib.kl and the audit refuses, giving you the exact key to paste:

$ kola audit leakdemo
audit: leaks — proving 1 file(s) under full prover discharge ...
audit: caps within budget — pack `leakdemo` (used=[] ⊆ allowed=[])
...
error[pack leaks budget]: 1 candidate leak site(s) not in [leaks] acknowledged — review EACH (acking a site never covers a new one): fix the code, open a per-iteration region (`region rq { .. }`), or copy the exact key(s) into [leaks] acknowledged: {"serve::fresh::Vec::new"}
audit: FAILED (1 violation(s)) — see the `error[...]` line(s) above; `kola audit` exits 1

There are two legitimate ways forward, and the audit does not care which you choose: fix the code, or accept the site deliberately.

[leaks]
acknowledged = ["serve::fresh::Vec::new"]
not_analyzed_pct_cap = 0

$ kola audit leakdemo
...
audit: leaks within budget (1 fresh, 0 grow acknowledged, 0/1 own non-`test` item(s) not analyzed = 0.0%, cap 0%) — computed under full prover discharge
audit ok: 0 violation(s) — every budget checked in this run is within its declared limits

The key is a site, not a function

An acknowledgement key is fn::class::text, the identity of one site. Acknowledging one site never covers a new one in the same function, and anything that changes the code changes the key. Rename serve to handle and review opens again:

audit: leaks — 1 acknowledged key(s) match NO candidate site: {"serve::fresh::Vec::new"}. Either those sites were FIXED (remove the keys — ...) or their fn LEFT THE ANALYSIS, which is why the de-analyzed count is worth reading beside this: 0 fn(s) de-analyzed here
error[pack leaks budget]: 1 candidate leak site(s) not in [leaks] acknowledged — ...: {"handle::fresh::Vec::new"}

The prover's annotations inside a site's text (such as [checked] in the grow example above) are stripped before matching. They can change when the prover gets better at an unrelated bounds check, and an acknowledgement should survive the compiler getting smarter, not the code changing.

A function outside the analysis that contains a loop and an alloc effect is exactly where a leak could hide, so the audit asks you to acknowledge it by name too, with a key such as "leakdemo::lib::guarded::unchecked-loop". Such a key goes stale, and is reported, the day the function becomes analysable.

not_analyzed_pct_cap: bounding the blind spot

The second key bounds how much of the library may sit outside the analysis: the percentage of the pack's own non-test items that are not in the verified IR. It exists so that coverage can only shrink on purpose. It is a ratio, so a pack can grow without tripping it as long as coverage holds. The older count-based key, not_analyzed_cap, is refused with an explanation.

This number bounds the analyser's blindness; it does not point at something to fix. The audit prints a census by class beside it. param-type and return-type mean a signature the IR cannot express yet, which is ordinary code, not debt. body means a function whose body left the analysable subset, which is where a leak could hide. test items are counted separately and never against the cap, so that adding tests never makes the budget harder to meet.

Pin the number the right way. A pack without a [leaks] section is counted with a quicker structural pass, a pack with one under full prover discharge, and the two percentages can differ. To adopt the cap, add a [leaks] section with no cap, run kola audit, and pin the number that run prints. The audit prints the line to paste.

A verdict may not outlive its coverage

A pack can carry a [leaks] budget, pass its audit and print audit ok while none of the functions that reached the verified IR allocates at all. Such a budget can never fire, yet it looks like protection in review, so the audit refuses it:

error[pack leaks budget]: pack `leakdemo` declares a [leaks] budget, and NOT ONE of the 1 fn(s) that reached the verified IR ALLOCATES, so no region leak this pack could contain is reachable by the analysis and the budget cannot fire (1 further fn(s) are outside the IR-v0 subset). A budget that cannot fire is worse than none: it reads as protection on a review surface. Repair: bring at least one ALLOCATING fn into the IR-v0 subset (`kola report leaks <file>` names why each is outside it), or delete the [leaks] section so the pack claims what is true — nothing

Both repairs are legitimate. A pack that does not allocate in analysable code should say so by carrying no leak budget, rather than one that is green for a reason nobody checked.

What the budget covers

The pack's own sources, its library code. test items are reported on their own line and never counted against the cap.
Not example programs. examples/*.kl get their own labelled census in the audit output, reported and never budgeted, just as [caps] and [caps.examples] are separate.
Not dependencies. Each pack's budget is enforced against its own files. A dependency's budget is checked when that dependency is audited, and is never added into the importer's numbers.