Embedding kola in a C program: the header, the symbols, and the seam

Most of this guide treats kola as the whole program. In a real system it usually arrives as a part of one: an object file linked into an existing C image, called by C code that was there first. A hypervisor, a router firmware or a kernel module will not be rewritten and will not hand over main. What it wants is one function, written in kola, carrying kola's proofs, reachable by an ordinary C call. This chapter describes that boundary as it exists on disk: what kola build writes, what the generated header declares, which symbols leave the object, what a bare-metal host must supply, and what the boundary refuses to do.

A library to embed

Everything below is generated from this one file. It parses an eight-byte frame header out of wire bytes. It is small, but it has every shape the boundary cares about: a struct that crosses, a slice parameter, an Option return, a contract, a byte-string literal and a private helper.

// frame.kl: a library. There is no `fn main`, so the object exports
// its non-std `pub` surface and nothing else.
use std::encoding::bytes;
use std::num::bits;

/// The parsed header: plain data a C caller can name and read.
pub struct Header {
    magic: u16,
    len: u16,
    crc: u32,
}

layout_assert[Header](8, 4);

const MAGIC: u16 = 0x4B4Cu16;

/// Not `pub`: every caller is inside this object, so it is emitted `static`.
fn crc_of(buf: &[u8]) -> u32 !{} {
    let mut acc = 2166136261u32;
    for b in buf {
        acc = bits::rotl32(acc ^ widen[u32](b), 7u32);
    }
    acc
}

/// The exported entry. kola cannot see a C caller, so this contract is
/// enforced at run time inside the exported symbol.
pub fn parse(buf: &[u8]) -> Option[Header] !{}
    req buf.len >= 8
{
    let m = bytes::rd16(buf, 0);
    if m != MAGIC {
        return None;
    }
    Some(Header {
        magic: m,
        len: bytes::rd16(buf, 2),
        crc: bytes::rd32(buf, 4),
    })
}

pub fn body_ok(buf: &[u8], h: &Header) -> bool !{} {
    if buf.len < 8 {
        return false;
    }
    crc_of(buf) == h.crc
}

/// A byte-string literal, so this library carries a blob of its own.
pub fn name() -> &heap [u8] !{} {
    &b"kola/frame"
}

test parses_a_good_header {
    let wire = b"\x4b\x4c\x00\x03\xde\xad\xbe\xef";
    let h = parse(&wire);
    assert h.is_some();
}

The fields of Header carry no pub. In kola a field is readable wherever its struct type is, and writing pub on a field is an error. The struct's own visibility decides everything, which is what lets pub struct mean "this layout is part of my ABI".

What kola build puts on disk

$ kola build -o out frame.kl
build ok: 7 native fn(s), 4 exported item(s) (3 fn, 0 const, 1 type) → out/frame.o
  crc_of
  parse
  body_ok
  name
  std::num::bits::rotl32
  std::encoding::bytes::rd16
  std::encoding::bytes::rd32
note: 1 exported fn(s) return a by-value aggregate in the SysV-vs-MS x64 return-mechanism divergence window (sizes 3,5,6,7 and 9-16). `sizeof` AGREES across those ABIs, so a `_Static_assert` cannot see it: SysV returns the value in RAX:RDX, MS x64 through a hidden pointer.
  KOpt_struct_k_frame__Header (12 bytes) — parse
  = note: harmless if every consumer of this `.kh` uses ONE psABI. If a C consumer tests on host SysV and ships to MS x64, run that leg on the real target ABI — the size pins in the header will not catch it.

$ ls out
frame.c  frame.kh  frame.o  kola.h  kola_asm.S

An ABI (application binary interface) is the set of rules compiled code on one platform agrees on: how structs are laid out in memory, which registers carry arguments and return values, how symbols are named. The note is the compiler flagging an ABI question discussed below: parse returns a 12-byte Option struct by value, inside the size range where two x64 ABIs agree on the struct's size but return it by different mechanisms.

The files each have one job:

• frame.c is the generated C. It is a build artifact, not a source to edit, but it is meant to be readable. When you want to know what a construct costs, look here.

• frame.kh is the generated header. This is the seam: it declares the types and the exported functions, and it is what your C code includes.

• frame.o is the object.

• kola.h is the runtime (the support code every kola program needs: memory allocation, trap handling and so on), copied beside the output and included by every generated header. It is a single self-contained header with no library to link, holding the heap, the trap path, slice helpers and per-architecture tables. kola_asm.S holds the assembly legs some std functions use.

The flags that shape this:

• -o <dir> writes the files into that directory instead of build/ beside the source. Two builds with different -o directories do not interfere, even on the same source file. Use it first.

• --freestanding builds for bare metal: no libc, a static heap, hooks you supply. Covered below.

• --target <triple> passes --target=<triple> to the same C compiler (which must accept it; clang does). A build is compile-only, so a foreign-target object goes as far as a native one.

• --link <path> also produces an executable. It needs a fn main. On x86-64 and AArch64 it tries kola's own backend and linker first, with no C compiler at all; a program the own backend refuses is built through cc with kola's own flags, so no hand-copied cc line can drift from them. The .o beside it stays free of an entry point. It is refused with --freestanding and with --cross, each with the reason.

Without --link, kola build never links. It compiles with -c and stops. In an embedded build the host owns the linker script, the entry point and the section layout, and a compiler that tried to own them would be in the way.

The header

out/frame.kh is about 830 lines, almost all of it the shared std error enums (OsErr, NetErr, FsErr, DevErr and others), which every header re-emits whether or not the library uses them. They are guarded, so this costs nothing but reading time. Here are the top and the part that belongs to this library:

/* kola-provenance 1: what this file was generated FROM.
 *
 * Generated by kola; do not edit. Deterministic: the same inputs produce
 * this block byte for byte on any machine, from any directory. UNPINNED
 * marks a source that has no version by construction (a working tree);
 * the sha256 beside it is of the source that was actually compiled.
 *
 * compiler  kola 0.1.0  card v0.234  std sha256:10be4338…
 * closure   sha256:2f4b969b…  (3 module(s), 0 embedded file(s))
 *
 * root      std            embedded in kola - covered by the `compiler` line above
 *
 * module    frame.kl                               <entry>        sha256:eb18b335…
 * module    std::encoding::bytes                   std            sha256:b71b8427…
 * module    std::num::bits                         std            sha256:ad31cce2…
 */
#ifndef KOLA_KH_6D8947763A893BF7
#define KOLA_KH_6D8947763A893BF7
#include "kola.h"
struct OsErr;
struct NetErr;
/* ... forward declarations, then each std enum: a guarded body,
   its layout pins, and a guard per variant macro ... */

#ifndef KOLA_T_struct_k_frame__Header
#define KOLA_T_struct_k_frame__Header
struct k_frame__Header {
    uint16_t magic;
    uint16_t len;
    uint32_t crc;
};
#endif /* KOLA_T_struct_k_frame__Header */
_Static_assert(sizeof(struct k_frame__Header) == 8, "kola ABI: sizeof(struct k_frame__Header) -- the target C compiler disagrees with kola layout");
_Static_assert(_Alignof(struct k_frame__Header) == 4, "kola ABI: _Alignof(struct k_frame__Header)");
_Static_assert(offsetof(struct k_frame__Header, magic) == 0, "kola ABI: k_frame__Header.magic moved");
_Static_assert(offsetof(struct k_frame__Header, len) == 2, "kola ABI: k_frame__Header.len moved");
_Static_assert(offsetof(struct k_frame__Header, crc) == 4, "kola ABI: k_frame__Header.crc moved");
#ifndef KOLA_T_KOpt_struct_k_frame__Header
#define KOLA_T_KOpt_struct_k_frame__Header
typedef struct { bool some; struct k_frame__Header val; } KOpt_struct_k_frame__Header;
#endif /* KOLA_T_KOpt_struct_k_frame__Header */
#ifndef KOLA_T_KSlice_uint8_t
#define KOLA_T_KSlice_uint8_t
typedef struct { uint8_t* ptr; size_t len; } KSlice_uint8_t;
#endif /* KOLA_T_KSlice_uint8_t */
#ifndef KOLA_BSTR_10_25B55AA00F3C6B36
#define KOLA_BSTR_10_25B55AA00F3C6B36
static KOLA_UNUSED const KArr_uint8_t_10 k_bstr_10_25B55AA00F3C6B36 = /* the 10 bytes of "kola/frame" */;
#endif /* KOLA_BSTR_10_25B55AA00F3C6B36 */
_Static_assert(sizeof(struct k_frame__Header) == 8, "kola layout_assert[Header]: claimed sizeof == 8");
_Static_assert(_Alignof(struct k_frame__Header) == 4, "kola layout_assert[Header]: claimed _Alignof == 4");
KOpt_struct_k_frame__Header k_frame__parse(KSlice_uint8_t buf);
bool k_frame__body_ok(KSlice_uint8_t buf, struct k_frame__Header* h);
KSlice_uint8_t k_frame__name(void);
#endif /* KOLA_KH_6D8947763A893BF7 */

The #ifndef/#define/#endif lines are include guards, the standard C trick that makes a header's contents count only once even if it is included several times; the section on two libraries explains why kola emits so many. The last three declarations are the whole public surface. crc_of is not in the file because it is not pub, and neither is MAGIC. A non-pub module constant is defined only in the .c; in a header it would be a static const that two libraries could collide on in one translation unit. If a C consumer needs a constant, mark it pub.

The comment at the top is a provenance record. Every emitted .c and .kh opens with one: the compiler's version, the card version it implements and a hash of its embedded std, one line per module with the sha256 of its source, and a single closure sha256: over the whole record. If you commit generated C into your repository, the file itself can answer what it was made from, and two builds compare on the closure line. The block contains no timestamp, hostname or absolute path, so the same inputs give byte-identical output on any machine. A root marked UNPINNED (a working tree named in kola.work, for instance) has no version, so it carries a content hash instead; grep UNPINNED over a committed .c shows which inputs nothing pins. There is no flag to turn the record off.

Which kola types a C caller can name

kola's compound types lower to C structs with mechanical names, so you can predict a signature before you look:

kola's owned things do not cross well. A slice crosses because it is a view of memory the caller already owns. A Vec lives in a region or in heap, and the C caller has no way to reason about that lifetime. If you want to hand a C caller data, the shape that works is for kola to fill a buffer the caller supplied.

A region parameter does not disappear at the seam either. (A region is a block of memory that kola frees all at once at a known point; see Memory: regions and references.) A function that allocates into its caller's region must name that region in a parameter type, and in C the region becomes an extra argument:

// The caller's region crosses the seam as an extra parameter.
pub fn fill[r](out: &r mut Vec[u64], n: usize) !{alloc(r)}
    req n <= 1000usize
{
    for i in 0..n { out.push(widen[u64](i)); }
}

// The region stays inside: a plain C signature.
pub fn build(n: usize) -> usize !{}
    req n <= 1000usize
{
    let mut out = 0usize;
    region r {
        let v: &r mut Vec[u64] = alloc in r mut Vec::new();
        for i in 0..n { v.push(widen[u64](i)); }
        out = v.len;
    }
    out
}

/* pool.kh */
void k_pool__fill(KOLA_UNUSED KRegion* k_rgn_r, KVec* out, size_t n);
size_t k_pool__build(size_t n);

fill makes the C side responsible for a kola region and a kola Vec, which is rarely what you want at a seam. build keeps the region inside the exported function, and its signature is one a C programmer can hold in their head.

Synthesised return types and the ABI

Nobody declared KOpt_struct_k_frame__Header. kola synthesised it, C compiles it, and how a small struct is returned by value is decided by the target ABI, not by kola or the header. When both sides are compiled by the same compiler for the same target, that is invisible. When they are not, it can bite. A fieldless enum once lowered to a struct containing an empty union, which is 0 bytes under SysV and 1 byte under the Microsoft ABI, so any struct with an enum field had a different layout per target; a test harness that only compiled SysV could not see it. The note kola build printed above exists for the same class of problem. If you embed kola, know which types cross your boundary: list them.

layout_assert is how you pin a layout a C caller depends on. It is a module-level item that claims a type's size and alignment, and the C backend turns it into _Static_assert, visible above as the two layout_assert[Header] lines. The interpreter treats it as a no-op, since it has no C layout. Bare metal: device nodes, freestanding builds and layout claims covers it in full.

The symbols

A kola function's C name is k_, then the compilation unit, then the name, with every non-alphanumeric character replaced by _. The unit is what you pointed kola at: a pack's declared [pack] entry is <pack>, any other file of a pack is <pack>::<module path>, and a .kl with no manifest above it is its file stem. So parse in frame.kl becomes k_frame__parse, and std::encoding::bytes::rd16 becomes k_std__encoding__bytes__rd16. The unit depends on the source, not on where it sits in your filesystem: a pack vendored through a symlink produces the same symbols as one in a real directory.

What actually leaves the object is much shorter (a Linux ELF object; Mach-O adds a leading underscore):

$ nm -g out/frame.o
                 U exit
                 U __fprintf_chk
                 U free
                 U _GLOBAL_OFFSET_TABLE_
00000000000001f0 T k_frame__body_ok
0000000000000240 T k_frame__name
0000000000000170 T k_frame__parse
                 U __longjmp_chk
                 U stderr

T marks a symbol this object defines and exports; U marks one it uses and expects the linker to find elsewhere (here, a few libc functions the hosted runtime calls). Three exported functions, exactly the pub surface. crc_of and the std helpers are compiled in with internal linkage (C static: visible only inside this object) and do not appear. One rule produces this: linkage follows visibility. Its consequences:

1. A non-pub function is emitted static.

2. Imported std functions are emitted static in each translation unit that uses them, so two separately built kola objects that both use std::encoding::bytes link together without multiple definition errors.

3. Emission is pruned to what is reachable. A library object is the closure of its non-std pub surface. A program, a file with fn main, is the closure of main plus the entry file's pub functions.

You can watch the pruning:

use std::log;
pub fn reachable(x: u32) -> u32 !{} { x + 1u32 }
pub fn also_pub_never_called(x: u32) -> u32 !{} { x + 2u32 }
fn private_and_dead(x: u32) -> u32 !{} { x + 3u32 }
fn main(sys: Sys) -> u8 !{log} {
    let v = reachable(41u32);
    log::info(f"v={v}");
    0
}

$ kola build -o outprog prog.kl
build ok: 4 native fn(s), 2 exported item(s) (2 fn, 0 const, 0 type) → outprog/prog.o
  reachable
  also_pub_never_called
  main
  std::log::info

$ nm -g outprog/prog.o | grep ' T '
0000000000000190 T k_prog__also_pub_never_called
0000000000000170 T k_prog__reachable

private_and_dead was never lowered: it is neither reachable from main nor pub. also_pub_never_called survives with no caller, because the entry file's pub surface is the ABI you published.

Every exported name carries its unit, so two separately built packs that each declare pub fn header_sane emit k_a__header_sane and k_b__header_sane and link together. There is no manifest key to choose this. main is exempt, and so are the shared std enums (NetErr, FsErr and the rest), which keep one name precisely so that two headers in one translation unit can share them. Two compilation units with the same name, such as two files called cfg.kl in different directories, still produce the same prefix; give your units distinct names.

Who owns main

k_main is not in that list either. kola's entry point is emitted static, and a real C main is behind a macro:

static KOLA_UNUSED uint8_t k_main(KOLA_UNUSED KSys sys) { /* ... */ }
#ifdef KOLA_MAIN
int main(int argc, char** argv){ (void)argc; (void)argv;
 /* ... */
 KSys s=k_sys_new(0, k_run_seed()); return (int)k_main(s); }
#endif

So one object serves both cases, and you choose at link time:

# the host keeps its own main and calls kola as a library
$ cc -I. -o drive drive.c prog.c && ./drive
42

# or take kola's entry point
$ kola build --link outprog/kmain prog.kl
build ok: 1 native fn(s) → outprog/kmain (own Linux-x64 executable, 6064 bytes)
backend: own LIR/x86-64; linker: own ELF; no external compiler
$ ./outprog/kmain
[info] v=42

The contract is the boundary

This is what earns kola its place in someone else's image. A req is a precondition: something the caller must guarantee, such as a minimum buffer length. A pub fn with a req checks it at the top of its exported symbol. Inside kola, call sites that prove a precondition skip the check: the compiler emits a check-free __nr body for them. You can see both halves on the std helper rd16, which parse calls after proving its bounds:

KOpt_struct_k_frame__Header k_frame__parse(KSlice_uint8_t buf) {
    if (!(/* buf.len >= 8 */)) k_trap_k(K_TRAP_REQ, "error[card §8]: req violated calling `parse`\n  --> frame.kl:29");
    uint16_t m = k_std__encoding__bytes__rd16__nr(buf, (size_t)0ull);
    /* ... */
}

static uint16_t k_std__encoding__bytes__rd16__nr(KSlice_uint8_t buf, size_t off) { /* no check */ }
static uint16_t k_std__encoding__bytes__rd16(KSlice_uint8_t buf, size_t off) {
    if (!(/* off + 2 <= buf.len */)) k_trap_k(K_TRAP_REQ, "error[card §8]: req violated calling `std::encoding::bytes::rd16`\n  --> std::encoding::bytes:79");
    return k_std__encoding__bytes__rd16__nr(buf, off);
}

A C caller proves nothing, so it always enters through the check. Here is a C program that is wrong about the length:

#include <stdio.h>
#include "frame.kh"

int main(void) {
    uint8_t wire[4] = { 0x4b, 0x4c, 0x00, 0x03 };
    KSlice_uint8_t s = { .ptr = wire, .len = sizeof wire };   /* 4, not 8 */
    KOpt_struct_k_frame__Header h = k_frame__parse(s);
    printf("returned some=%d  (we never get here)\n", (int)h.some);
    return 0;
}

$ cc -I. -o short short.c frame.o && ./short
trap: error[card §8]: req violated calling `parse`
  --> frame.kl:29
$ echo $?
101

Without the check, the call would read four bytes past the end of a stack array and return a plausible-looking Header. With it, the program stops deterministically and names the function and the rule. This is the same req as in Contracts, traps and tests; it does not disappear at the language boundary.

There is no flag to remove the check. Such a flag would mean "trust external C to respect a contract nobody checks", which is exactly what req exists to prevent. If you write pub, you get the check. The corollary: there is no way to export a function without making it pub. If a C test harness needs to call something your kola callers should not, put it in its own module, pub there and imported by nothing.

Two libraries in one translation unit

A translation unit is one .c file plus everything it includes; the C compiler sees each one separately. Once a C program embeds one kola library, it tends to embed a second, and then some header includes both, or includes one twice through a chain nobody drew. Both work:

#include <stdio.h>
#include "frame.kh"
#include "tag.kh"
#include "frame.kh"      /* again, as a transitive chain would */

int main(void) {
    uint8_t wire[8] = { 0x4b, 0x4c, 0x00, 0x03, 0xde, 0xad, 0xbe, 0xef };
    KSlice_uint8_t s = { .ptr = wire, .len = sizeof wire };
    KOpt_struct_k_frame__Header h = k_frame__parse(s);
    struct k_tag__Tag t = k_tag__read_tag(s);
    printf("header magic=%04x  tag kind=%u slot=%u\n", h.val.magic, t.kind, t.slot);
    return 0;
}

$ cc -I. -o both both.c frame.o tag.o && ./both
header magic=4b4c  tag kind=75 slot=76

Two mechanisms make this work, because they solve different problems:

• A per-type include guard, #ifndef KOLA_T_<cname>, around each type's body. A whole-block guard would also suppress the second library's own types; the collision is per type. Forward declarations stay unguarded, since struct X; may repeat.

• A whole-file guard, #ifndef KOLA_KH_<hash>, keyed on content, for the same header included twice. It is keyed on content because the emitter does not know what you will name the file, and two headers with one basename from different packs must not suppress each other. It uses #ifndef/#define, since #pragma once is not ISO C.

Why the layout pins sit outside the guard

A guard keyed on a type's name has a failure mode worse than the problem it solves. If two units each define a Cfg with different fields (two files named cfg.kl in different directories, say), the guard makes the second definition vanish, and the second library's calls then run against the first library's layout: a silent ABI mismatch.

So every _Static_assert in the header sits outside its type's guard. The guard suppresses the duplicate definition, and the pins still run against whichever definition won:

# a/cfg.kl:  pub struct Cfg { a: u64, b: u64 }     -> 16 bytes
# b/cfg.kl:  pub struct Cfg { a: u32 }              ->  4 bytes
$ cc -I. -c clash.c
In file included from clash.c:2:
cfg_b.kh:796:1: error: static assertion failed: "kola ABI: sizeof(struct k_cfg__Cfg) -- the target C compiler disagrees with kola layout"

That fails at the include site and names the type. (Clang adds expression evaluates to '16 == 4'.)

Byte-string literals

A &b"..." literal becomes a static const array in the header, named by its content: k_bstr_<len>_<fnv1a64-hex>. The length is part of the name so that two different byte strings could only share an identifier if a 64-bit hash collided and their lengths agreed too. Each definition has its own #ifndef KOLA_BSTR_<key> guard, so two libraries that both contain b"kola/frame" emit the same declaration and one translation unit keeps one copy. Unlike a type, a byte string cannot disagree with itself, so this guard needs no pins beside it. Separately compiled objects still carry their own copies, which costs a few bytes.

Bare metal: what the host supplies

--freestanding builds for an image with no libc: no stdio, no malloc, no C runtime. The runtime is still kola.h, but its freestanding branch provides a static heap and calls hooks you supply. Each hook is referenced only when the program needs it:

• void k_panic(const char *msg), when a trap edge survives the prover. It is the non-returning trap handler (log and halt, or fault the guest), where every contract, bounds or overflow violation lands.

• uint64_t k_now_ns(void) and int64_t k_now_wall_us(void), when the program reads Clock.

• void k_io_write(const char *s), when the unit is compiled with -DKOLA_LOG_HOOK and the program logs. Without the macro, log lines are dropped.

• -DKOLA_HEAP_BYTES=<n> sizes the static pool (16 MiB by default) and -DKOLA_REGION_DEFAULT=<n> the first slab of each region (1 MiB by default). Both must be the same on every translation unit of the image.

The acceptance test is nm -u

Every object file lists the symbols it uses but does not define, and the linker must supply each of them when it builds the final image. nm -u prints that list. For a hypervisor there is no process to kill, so the useful question is whether the object has an edge to the panic path at all. That is a question for the linker's view of the object, and nm -u answers it. The frame library keeps one edge, because parse is pub with a req:

$ kola build --freestanding -o outfs frame.kl
$ nm -u outfs/frame.o
                 U k_panic

That is the only undefined symbol, and nothing comes from libc. A module with no runtime obligation left references nothing:

pub fn mix(a: u32, b: u32) -> u32 !{} {
    (a ^ b) | 1u32
}

$ kola build --freestanding -o outp pure.kl
$ nm -u outp/pure.o
                                   (nothing)

A module whose req is discharged at every call site also comes out empty: its checked entry is then dead static code that the optimiser removes along with its k_panic edge, and imported std functions are local to the unit. Make the undefined set a check in your build: run nm -u on every kola object that enters the image and fail on anything not on your allowlist. A C compiler may synthesise a memcpy or memset call from a loop (kola.h defines both for freestanding builds), so verify per object rather than assuming.

Measuring the heap

A freestanding program allocates from one static pool per image: a fixed block of memory reserved at link time, from which allocations are handed out by moving a pointer forward. Each region carves slabs from it, and a region that closes rewinds the pool when everything above its mark is its own. The host can read the ledger:

size_t used  = k_heap_used_bytes();   /* region slabs and growth chunks taken */
size_t total = k_heap_total_bytes();  /* the linked pool size                 */

Here is a host reading a pool the kola library allocated from, using build from earlier:

/* board.c: a separate translation unit from the generated pool.c */
#include <stdio.h>
#include <stdlib.h>
#include "pool.kh"

void k_panic(const char *msg) { fprintf(stderr, "PANIC: %s\n", msg); exit(1); }

int main(void) {
    printf("pool total = %zu bytes, used before = %zu\n",
           k_heap_total_bytes(), k_heap_used_bytes());
    size_t n = k_pool__build(200);
    printf("built %zu elements; used after = %zu bytes\n", n, k_heap_used_bytes());
    return 0;
}

$ kola build --freestanding -o ofs pool.kl
$ cd ofs
$ cc -O2 -DKOLA_FREESTANDING -DKOLA_HEAP_BYTES=65536 -I. -o board board.c pool.c && ./board
pool total = 65536 bytes, used before = 0
PANIC: bare heap exhausted

Two hundred u64s are 1600 bytes of data, but each region asks the pool for a whole slab, and the default slab is 1 MiB. One region block already exceeds a 64 KiB pool. Size the slab for the target and it fits:

$ cc -O2 -DKOLA_FREESTANDING -DKOLA_HEAP_BYTES=65536 -DKOLA_REGION_DEFAULT=8192 -I. -o board board.c pool.c && ./board
pool total = 65536 bytes, used before = 0
built 200 elements; used after = 0 bytes

used after is zero because the region inside build closed and the pool rewound behind it. Compile with optimisation, as here: at -O0 unused clock helpers in kola.h stay alive and the link asks for k_now_ns even though the program never reads a clock.

Cross-compiling the seam

--target <triple> passes the triple to the C compiler. Nothing about the seam changes; the object is for another machine:

$ KOLA_CC=clang kola build --freestanding --target aarch64-unknown-linux-gnu -o outx frame.kl
build ok (freestanding, cross --target=aarch64-unknown-linux-gnu, compile-only): 7 native fn(s), 4 exported item(s) (3 fn, 0 const, 1 type) → outx/frame.o
$ file outx/frame.o
outx/frame.o: ELF 64-bit LSB relocatable, ARM aarch64, version 1 (SYSV), not stripped
$ nm -u outx/frame.o
                 U k_panic

On ELF (the object format of Linux and most bare-metal toolchains) the 16 MiB default pool sits in .bss, the section for zero-initialised data that the loader allocates at start-up rather than storing in the file, so it costs memory at run time but no bytes in the object file (frame.o above is about 3 KB). The pool is a weak definition (one the linker may merge with other definitions of the same name), and Mach-O, the macOS format, cannot place a weak definition in bss, so there the array becomes real bytes in the object; pass a small -DKOLA_HEAP_BYTES if you build freestanding on a Mac.

kola build --cross --target <arch> is a different path, named here so you do not reach for it by mistake. It uses kola's own backend to write an object with no C compiler, which is useful where no cc exists. It writes no .kh, because there is no C, and its reach is narrower:

$ kola build --cross --target x86_64 --format elf -o outc/frame.o frame.kl
build ok: 25 native fn(s), 9 skipped → outc/frame.o (x86_64/elf, 13200 bytes)
  skipped `parse`: return `Option[struct#0]` is outside native-m2
  skipped `body_ok`: slot `h`: `&struct#0` is outside native-m2
  skipped `name`: return `&[u8]` is outside native-m2
  ...

The whole pub surface of this library was skipped. For embedding in C, the C backend is the path.

The direction that does not exist

kola cannot call into C. There is no syntax for it:

extern "C" fn host_tick() -> u64;

error[card §1]: expected an item, found identifier `extern`
  --> ffi.kl:1:1
   |
 1 | extern "C" fn host_tick() -> u64;
   | ^^^^^^
   = help: items: fn, struct, resource struct, enum, impl, const, test, use, mod, layout_assert

extern is not a reserved word held back for later, and there is no raw pointer type either. Every kola function is inside the checked world, which is what lets a reviewer trust a signature: an FFI edge would be a place where effects, regions and contracts stop meaning anything.

The question of whether kola needs a C FFI or inline assembly to be fast has been examined against measurements, in media codecs and in TLS. In both cases the gap turned out to be fixable inside kola: missing SIMD intrinsics were ordinary compiler work, and a large TLS handshake gap came down to one field-multiply routine that a loop rewrite repaired.

That leaves three sanctioned shapes:

• C calls kola, as in this chapter.

• kola runs another program as a process (sys.proc, see Command-line programs). Reusing an existing encoder goes through a spawned process, not a linked call.

• For a hot function that needs a specific instruction sequence, an hw clause names a per-architecture C or assembly symbol for that one function. The kola body remains the definition: it is what the interpreter runs and what the checker proves, kola test --native compares the two, and --no-hw drops the leg. The symbol must be a leaf, and only scalars, arrays and slices of scalars cross. SPEC-CARD §8 has the rules.

If you think you need to call out of kola for testing, for instance to build a differential test against a C implementation, consider whether a corpus of inputs and expected outputs can serve as the oracle instead. It usually can, with no foreign code in the path.

A checklist for embedding kola

1. Build with -o <dir> and keep generated files out of your source tree.

2. Include the .kh, never the .c. Compile the .c (or link the .o) as one more unit of your build.

3. List the types on your pub surface and pin each with layout_assert. Assume nothing about a synthesised KOpt_ or KRes_ return until you have checked it on the real target ABI.

4. Check nm -u in your build against an explicit allowlist.

5. Keep regions inside kola. A KRegion* in an exported signature makes the C side responsible for a kola lifetime.

6. Size the heap from the peak: sample k_heap_used_bytes() under real load, set KOLA_HEAP_BYTES from that, and set KOLA_REGION_DEFAULT deliberately.

7. Give compilation units distinct names. Two files with one stem, or two packs with one name, share every exported symbol's prefix.