Chapter 0: Start Here#

Part I — Start here. No prerequisites beyond one introductory C book. After this chapter you can build a program against proven, read any other chapter, and look up a term you do not recognise.

Table of contents#

1. Who this manual is for
2. Why this library exists
3. Your first program
4. Building and including
5. The five contracts you will meet on every page
6. Intent and design philosophy
7. Build and include model
8. Global contracts
9. Ownership and destruction matrix
10. Operation behavior classes
11. Manual chapters
12. Platform support and verification
13. Appendix B: glossary
14. Appendix C: public header map
15. Appendix D: the libc map
16. Where to go next

1. Who this manual is for#

This manual assumes you have finished one introductory C book. Concretely, it assumes you are comfortable with variables and control flow, functions, arrays, struct, pointers and */&, malloc and free, printf, char * strings with strlen, and compiling a program with gcc main.c -o main. If all of that is familiar, you have enough.

It does not assume you have met ownership as a discipline, borrowed versus owned data, arenas or pools, function-pointer tables used as an interface, C23 attributes, undefined behaviour as something a compiler actively exploits, alignment beyond "it works", atomics, or the idea that a library might refuse an operation instead of doing its best. Every one of those is explained where it is first used, and every one is in the glossary in §13.

This is not a C tutorial. It will not explain what a pointer is. It will explain, at length, why this library hands you a struct containing an error instead of setting errno, because that is a design decision you are entitled to disagree with, and you cannot disagree with a decision nobody explained.

2. Why this library exists#

C gives you almost nothing and trusts you completely. That is its great strength — there is no runtime, no hidden allocation, no cost you did not write — and it is why C is still the language of operating systems, embedded devices and everything that has to be small and predictable.

It is also why the same five bugs have been shipping for fifty years. This library is a set of answers to those five bugs. Each answer costs something, and this section says what.

The string functions do not know how big anything is#

char buf[64];
strcpy(buf, name);            /* wrong: how long is name? strcpy never asks */
strcat(buf, ", welcome!");    /* wrong: and how much room is left now? */

strcpy receives a destination pointer and a source pointer. Nothing in that signature carries the size of the destination, so nothing can check it. The function will happily write the 200th byte into a 64-byte buffer, and what it corrupts is whatever the compiler happened to put next — often the return address. This is not a rare mistake by careless people; it is the single most exploited class of bug in the history of the language, and the API makes it the default behaviour.

strncpy is the traditional answer and it is a trap of its own: it does not always NUL-terminate, so the "safe" version silently produces a string that is not a string.

What this library does instead. A string carries its length. proven_u8str_view_t is a pointer and a size, together, always. An append checks the destination's capacity because it knows the capacity, and when the text does not fit it returns an error and writes nothing — it does not truncate, because a truncated path is a wrong path and a truncated command is a different command. See Chapter 3.

What it costs. Every string is two words instead of one, and you cannot pass a proven string straight to a printf("%s") without asking for a NUL-terminated form.

Nothing makes you check for failure#

char *p = malloc(n);
p[0] = 'x';                   /* wrong: malloc returns NULL when it fails */

malloc reports failure by returning NULL, and C will not say a word if you never look. The same is true of fopen, of realloc, of every function that returns a sentinel. The error is available; noticing it is optional.

errno is worse, because it is a global that survives the call. You must check it at exactly the right moment, before any other library call has a chance to overwrite it, and you must remember that a successful call is allowed to set it to garbage.

What this library does instead. A function that can fail returns its error as a value, and when it also has a result, the two come back together in one struct:

proven_result_u8str_t s = proven_u8str_create(alloc, 64);
if (!proven_is_ok(s.err)) return 1;      /* s.value means nothing until you check */

Functions whose only job can fail are marked [[nodiscard]], which means the compiler refuses to build code that throws the error away. You can still ignore it deliberately — (void) in front of the call — and having to type that is the point. See Chapter 1.

What it costs. More ifs. There is no exception mechanism to jump you out of a deep failure, so error paths are visible in the shape of the code. That visibility is the feature.

printf believes whatever you tell it#

printf("%d\n", 3.0);          /* wrong: %d with a double. This compiles. */
printf("%s\n", 42);           /* wrong: and this one crashes */

The format string is checked by nothing at runtime. Modern compilers warn about literal formats, which helps exactly until the format is a variable, and then you are back to a function that reads whatever bytes the varargs stack happens to hold, in whatever shape the string demanded.

What this library does instead. {} is a placeholder with no type in it, and the type comes from the argument, resolved at compile time by _Generic:

proven_println("{} is {}", PROVEN_ARG(name), PROVEN_ARG(count));

There is no %d-versus-double mismatch available, because you never wrote the type twice. See Chapter 3 §3 for the tutorial and Chapter 8 for the full grammar.

What it costs. PROVEN_ARG around each argument, and a format language that is not the one in your fingers.

Who frees this?#

char *s = build_message();    /* do I free this? the type does not say */

A char * returned from a function might be freshly allocated, might point into a caller's buffer, might be a string literal in read-only memory, or might be a pointer into a static buffer that the next call will overwrite. The type is identical in all four cases. The answer lives in documentation, and documentation drifts.

What this library does instead. Ownership is in the type name and in the signature. A proven_u8str_t is owned — you got it from a _create, and you must _destroy it with the same allocator. A proven_u8str_view_t is borrowed — it points at bytes someone else owns, you never destroy it, and it stops being valid when the owner does. Any function that might allocate takes the allocator as a parameter, so a signature without an allocator cannot allocate.

What it costs. Two types where C has one, and the discipline of asking "who owns this?" at every boundary — which you were paying anyway, just later and in a debugger.

The comparison function nobody can typecheck#

qsort(a, n, sizeof *a, cmp);  /* cmp takes const void*; get it wrong and it is UB */

qsort takes a comparator through a void * interface, so a comparator with the wrong parameter types still compiles. The classic version of this bug is comparing the pointers instead of what they point at, and it produces a program that runs, sorts nothing correctly, and never crashes.

What this library does instead. The same void * shape — this is C, there is no other way — but the library documents the contract precisely, gives you working comparators to copy, and proven_array_sort is an introsort with an O(n log n) guarantee rather than a quicksort that degrades to O(n²) on the input an attacker chooses. See Chapter 4.

The bytes have a type, even when you did not choose one#

You think of memory as bytes. C's abstract machine does not: it treats memory as typed, and reading the same bytes through pointers of two different types is undefined behaviour — which the compiler is allowed to exploit, silently, only when optimisations are on. This is called strict aliasing, and it is the trap under every hand-written parser that reads a byte buffer through pointers of different widths:

void *buf = malloc(8);
uint32_t *w = buf;      /* the same memory, seen as 32-bit — no cast, no warning */
uint16_t *h = buf;      /* the same memory, seen as 16-bit */
*w = 0xAAAAAAAAu;
*h = 0x1234;            /* change the low half */
printf("%08x\n", *w);   /* wrong to expect aaaa1234: at -O2 this prints aaaaaaaa */

Compiled at -O0 it prints aaaa1234; at -O2 it prints aaaaaaaa, because the compiler assumed a uint16_t write and a uint32_t read cannot touch the same memory and dropped the write. No warning is given, and the program passed every test you ran in a debug build. This is the class of bug the Linux kernel avoids by compiling with -fno-strict-aliasing — a whole flag, for one rule.

What this library does instead. Raw memory is proven_byte_t, an alias of unsigned char — the one type the rule explicitly exempts, because the standard lets you inspect any object's bytes through it. The ordinary API never quietly reinterprets your bytes as a wider type, so the bug above cannot be written through it. (Strict aliasing has a subtler sibling, provenance, that the library is named after; Chapter 6 §3 and the project README cover it.)

What this library is not#

It is not a framework, and it does not want to own your main. It has no global state to initialise, starts no threads, registers no atexit handler, and allocates nothing you did not hand it an allocator for. Every module is usable on its own. Most of it runs with no operating system at all — see freestanding mode.

3. Your first program#

This is the whole of it. Every line is one of the contracts in §5, and the build compiles and runs this exact file, so it cannot quietly stop being true.

/*
 * The first program. It is deliberately small, and every line of it is one of
 * the five contracts you will meet on every page of this manual.
 *
 * Compare it with the C you already know:
 *
 *     char buf[64];
 *     strcpy(buf, name);          <- how big is name? strcpy does not ask.
 *     strcat(buf, ", welcome!");  <- and now? strcat does not ask either.
 *     printf("%s\n", buf);
 *
 * That program is correct until the day `name` is longer than you assumed, and
 * then it is a security advisory. The version below cannot do that: every write
 * knows the size of its destination, and every operation that could fail hands
 * you back an error you are not allowed to ignore silently.
 */

int main(void) {
    /* (1) You pass the allocator in. The library never reaches for a global
     *     malloc behind your back, so you always know who allocated what. */
    proven_allocator_t alloc = proven_heap_allocator();

    /* (2) Anything that can fail returns its error WITH its value. There is no
     *     errno to remember to check, and `greeting.value` means nothing until
     *     you have looked at `greeting.err`. */
    proven_result_u8str_t greeting = proven_u8str_create(alloc, 64);
    if (!proven_is_ok(greeting.err)) return 1;

    /* (3) A view is borrowed text that knows its own length. PROVEN_LIT builds
     *     one from a literal at compile time - no strlen scan happens here. */
    proven_u8str_view_t name = PROVEN_LIT("world");

    /* (4) The append refuses rather than truncates. If "hello, " and the name
     *     did not fit in the 64 bytes asked for above, this returns
     *     PROVEN_ERR_OUT_OF_BOUNDS and writes nothing - it never quietly stores
     *     half a word and lets you carry on. */
    proven_err_t err = proven_u8str_append(&greeting.value, PROVEN_LIT("hello, "));
    if (proven_is_ok(err)) err = proven_u8str_append(&greeting.value, name);
    if (proven_is_ok(err)) err = proven_u8str_append(&greeting.value, PROVEN_LIT("!"));

    if (!proven_is_ok(err)) {
        proven_u8str_destroy(alloc, &greeting.value);
        return 1;
    }

    EXAMPLE_REQUIRE(proven_u8str_view_eq(proven_u8str_as_view(&greeting.value),
                                         PROVEN_LIT("hello, world!")),
                    "the three appends should have built the whole greeting");

    proven_println("{}", PROVEN_ARG(proven_u8str_as_view(&greeting.value)));

    /* (5) You created it with `alloc`, so you destroy it with the SAME `alloc`.
     *     Owning things are destroyed exactly once; borrowed things - like
     *     `name` above - are never destroyed at all. */
    proven_u8str_destroy(alloc, &greeting.value);

    return EXAMPLE_OK();
}

EXAMPLE_REQUIRE and EXAMPLE_OK are not part of the library — they come from manual/examples/example.h and exist so the build can check that every example in this manual still does what the text says it does. Your own program would use neither.

Three details worth pausing on, because they recur everywhere:

• proven_u8str_create(alloc, 64) asks for 64 bytes of capacity, and that capacity includes the NUL terminator. It does not grow on its own. proven_u8str_append is the fixed-capacity form: it fails when the text does not fit. When you want growth, you call proven_u8str_append_grow and pass the allocator, and the signature tells you at a glance which one you are using.
• PROVEN_LIT("hello, ") costs nothing at runtime. It is a compile-time sizeof on a string literal. proven_u8str_view_from_cstr(s) exists for the case where the text comes from elsewhere, and that one really does scan for the NUL — the two are spelled differently because one is free and the other is O(n).
• The destroy takes the allocator again. The string does not remember which allocator made it; you must pass the same one. That keeps the string small and makes the dependency visible, and it is a real hazard — see §5.

4. Building and including#

There is one header for everything:

#include "proven.h"

It pulls in the whole public API. If you prefer to include only what you use, every module has its own header under include/proven/ — #include "proven/u8str.h", #include "proven/fs.h" and so on — and §14 below maps every header to the chapter that documents it.

Compiling by hand, which is all this library needs:

gcc -std=c2x -Iinclude -Iplatform your_program.c src/proven/*.c platform/*.c -o your_program

src/proven/ is the portable library. platform/ is the small layer that talks to the operating system — the PAL, or platform abstraction layer. Everything that makes a syscall lives there and nowhere else, which is why the rest of the library can be compiled for a target with no operating system at all.

The repository builds itself with a C program rather than a build system:

cc -std=c2x -o nob nob.c     # build the build driver, once
./nob build                  # compile everything and run the whole test suite
./nob release                # the same, optimised

./nob with no arguments lists the other modes — sanitizers, freestanding, cross-compilation and the benchmark. There is no make, no CMake, and nothing to install.

A C23 compiler is required. The library uses C23 features deliberately, [[nodiscard]] most visibly. GCC 13+, Clang 16+ and recent MSVC all work; the build driver probes for -std=c23 and falls back to -std=c2x for slightly older compilers.

5. The five contracts you will meet on every page#

These five rules explain most of the library's shape. Each is stated once here and assumed everywhere else. §8 below gives the formal versions; these are the plain-language ones.

1. Errors are values#

Every fallible function hands the error back. When there is nothing else to return it is a bare proven_err_t; when there is a value, the value and the error travel together and the value is meaningless until you have checked the error. PROVEN_OK is zero, and proven_is_ok(err) reads better than err == 0.

Wrong — reading the value before the error:

proven_result_u8str_t s = proven_u8str_create(alloc, 64);
proven_u8str_append(&s.value, text);   /* wrong: s.value is garbage if create failed */

The whole point of pairing them is that the value is only valid on the success path. Check first, every time.

2. Views are borrowed#

proven_u8str_view_t is a pointer and a size. It owns nothing, allocates nothing, and is free to copy — but it stops being valid the moment the thing it points into is destroyed or moved.

Wrong — a view that outlives what it points at:

proven_u8str_view_t name;
{
    proven_result_u8str_t owned = proven_u8str_create(alloc, 16);
    (void)proven_u8str_append(&owned.value, PROVEN_LIT("temp"));
    name = proven_u8str_as_view(&owned.value);
    proven_u8str_destroy(alloc, &owned.value);   /* the bytes are gone */
}
use(name);                                       /* wrong: dangling view */

This is the same lifetime bug as a dangling pointer, and it is worth stating separately because a view looks like a value. It is not; it is a pointer wearing a struct.

3. Allocation is a parameter#

Read the signature. proven_u8str_append(str, data) cannot allocate, so it fails when the text does not fit. proven_u8str_append_grow(alloc, str, data) takes an allocator, so it can grow. Nothing in this library calls malloc behind your back, which is what makes it usable in an arena, in a pool, or on a device with no heap.

The corollary is the hazard: you must destroy with the allocator you created with. The object does not remember.

Wrong — mismatched allocators:

proven_result_u8str_t s = proven_u8str_create(arena_alloc, 64);
proven_u8str_destroy(heap_alloc, &s.value);   /* wrong: heap free on arena memory */

Nothing checks this today. It is heap corruption that surfaces later, somewhere else.

4. Caller-owned state must not be copied#

Some objects are structs you own and pass by pointer — buffered writers, line readers, directory iterators. Several of them contain a pointer to one of their own fields, so copying the struct copies a pointer that still points at the original.

Wrong — copying a state struct:

proven_writer_buf_t a = ...;
proven_writer_buf_t b = a;          /* wrong: b's internals still point into a */

§9.2 below lists all sixteen of these types. The rule is simple: create it where it lives, pass &it, and do not assign it.

5. Refuse, never truncate#

When a result does not fit, this library fails the operation and leaves the destination unchanged. It does not write "as much as fits". A truncated path opens the wrong file, a truncated command runs the wrong command, and a truncated number is a different number — and every one of those is worse than an error you can see.

Where truncation genuinely is what you want, there is a separate, differently named function that tells you how much it wrote:

proven_result_size_t r = proven_u8str_append_partial(&s, huge);
/* r.value is how many bytes were actually appended. Reading it is the point. */

Wrong — assuming the two behave alike:

(void)proven_u8str_append_partial(&s, huge);   /* wrong: the count WAS the result */

Everything up to here is the plain-language introduction. The rest of this chapter is the reference the other chapters lean on: the library's intent and build model stated formally, the global contracts, the ownership matrix, the behaviour classes, the reading order, platform support, and the appendices. It used to be a document of its own, the manual's front page; it lives here now so that the front page is nothing but the table of contents.

6. Intent and design philosophy#

proven is a compact C23 systems foundation library. It is intended for C programs that want practical infrastructure without hiding memory ownership, error control flow, or platform access behind global state.

It is not a libc replacement. It provides a focused set of allocator-driven memory tools, byte views, containers, strings, formatting, scanning, hashing (FNV, SipHash, CRC-32, SHA-256), hex/Base64 encoding, OS-strength randomness, filesystem helpers, buffered streams, time helpers, memory mapping, stackless coroutine macros, and a bounded job system.

Core design principles:

• C23 first: the build driver uses -std=c23.
• Explicit errors: fallible functions return proven_err_t or proven_result_*_t.
• Explicit ownership: owned objects have clear destroy functions and allocator rules.
• Failure atomicity: grow/realloc-style APIs preserve the old object on allocation failure unless documented otherwise.
• Pointer provenance discipline: raw object access uses proven_byte_t and bounded views.
• PAL isolation: hosted OS services live under platform/ and are called through public wrappers.
• Core containers do not add hidden locks. Shared mutation requires caller synchronization.
• The build system is a single checked-in nob.c; tests are plain C executables.

7. Build and include model#

There is nothing to install#

This library has no configure, no CMake, no package to fetch, and no shared object to place somewhere. It is C source: you compile it into your program alongside your own files.

That is a deliberate choice and it costs something. You do not get a system package, and updating means pulling new source rather than bumping a version constraint. What you get is that the library cannot be a different version than the one you are looking at, cannot pick up a build flag you did not choose, and cannot fail to link because a distribution built it with different options. For a library that is meant to run on hosted systems and on bare metal, "compile it with your program" is the only model that works in both places.

Two directories matter. src/proven/ is the portable library — no OS calls anywhere. platform/ is the small layer that makes syscalls, and it is the only part a new target has to replace. A freestanding build simply leaves the hosted files out; see the freestanding guide.

The build driver, nob.c, is a C program rather than a build system, and you compile it the same way you compile everything else here. It is checked into the repository, so there is no bootstrap step and no version of it to install either.

A C23 compiler is required — GCC 13+, Clang 16+, or recent MSVC. The driver probes -std=c23 and falls back to -std=c2x for compilers that still use the transitional spelling.

Build and run the hosted test suite:

cc nob.c -o nob
./nob build

Common validation commands:

./nob release
./nob strict
./nob strict-error
./nob asan
./nob ubsan
./nob tsan
./nob regression
./nob regression-asan
./nob regression-ubsan
./nob freestanding
./nob cross -build-root build-out/proven_c_lib

Use the umbrella header when you want the full hosted API:

#include "proven.h"

Use smaller includes when you want a narrower translation unit:

#include "proven/heap.h"
#include "proven/u8str.h"
#include "proven/fmt.h"

A direct hosted application build can follow the same source layout as nob.c:

cc -std=c23 -D_DEFAULT_SOURCE -D_POSIX_C_SOURCE=200809L \
  -Iinclude -Iplatform \
  app.c src/proven/*.c platform/proven_sys_*.c \
  -pthread -o app

8. Global contracts#

8.1 Result contract#

A result value is usable only when err == PROVEN_OK.

Correct:

proven_result_mem_mut_t r = alloc.alloc_fn(alloc.ctx, 128, PROVEN_DEFAULT_ALIGNMENT);
if (proven_is_ok(r.err)) {
    /* only now does r.value mean anything */
    proven_mem_mut_t mem = r.value;
    (void)proven_mem_copy(mem.ptr, mem.size, proven_mem_view_from_u8(PROVEN_LIT("hi")));
    alloc.free_fn(alloc.ctx, mem.ptr);
}

Wrong (does not compile as shown - the value is read before the error is checked):

proven_result_mem_mut_t r = alloc.alloc_fn(alloc.ctx, 128, PROVEN_DEFAULT_ALIGNMENT);
use_bytes(r.value.ptr, r.value.size); /* wrong: r.err was not checked */

8.2 Public struct contract#

Many public structs expose layout for C usability. This does not mean arbitrary field mutation is supported. Treat direct mutation of internal fields as caller misuse unless the header explicitly allows it.

Wrong:

arr.len = 999;      /* wrong: breaks array invariants */
str.internal.cap=0; /* wrong: breaks string invariants */

Use the functions and macros that maintain invariants.

8.3 Borrowed view contract#

Views do not own memory. A proven_u8str_view_t, proven_u16str_view_t, proven_mem_view_t, or proven_mem_mut_t is valid only while the referenced storage remains alive and unmoved.

Wrong:

proven_u8str_view_t v = proven_u8str_as_view(&s);
proven_u8str_append_grow(alloc, &s, PROVEN_LIT("more"));
use_view(v); /* wrong: growth may reallocate s */

8.4 Allocator contract#

A proven_allocator_t is valid only when all three function pointers are present. Reallocation must be failure-atomic: if it fails, the old allocation remains valid.

proven_allocator_t heap = proven_heap_allocator();
if (!proven_alloc_is_valid(heap)) {
    /* no usable allocator here: e.g. the freestanding heap stub */
    proven_panic("no heap allocator on this target");
}

8.5 PAL boundary contract#

Code under src/proven/ should not depend on OS headers directly. Hosted services should route through platform/proven_sys_*.[ch] and public wrappers such as proven_fs_*, proven_sysio_*, proven_time_*, and proven_mmap_*.

Application code should prefer public APIs. Direct PAL calls are for porting and platform integration.

9. Ownership and destruction matrix#

There are two kinds of object in this library, and the difference decides what you must do with them.

Owning objects hold storage they allocated, and you must destroy them. They are the table immediately below.

Caller-owned state objects allocate nothing. They are scratch structs you declare — usually on the stack — and hand to a constructor, which returns a small by-value handle that points into them. They have no destroy function, because there is nothing to free. What they have instead is a rule that owning objects do not have, and it is the one that bites:

A caller-owned state object must not be copied or moved once a handle has been made from it. The handle holds a pointer into the struct. Copy the struct and the handle still addresses the original; let the original go out of scope and the handle points at dead memory.

They are listed in §4.2.

9.1 Owning objects — you must destroy these#

9.2 Caller-owned state — no destroy, do not copy#

These allocate nothing and free nothing. You declare one, pass its address to a constructor, and use the small handle you get back. The struct must outlive the handle, and must not be copied or moved while the handle is alive.

Wrong — the copy looks harmless and is a use-after-free:

proven_sysio_out_t out;
proven_writer_t w = proven_sysio_stdout_buffered(&out, buf);

proven_sysio_out_t saved = out;   /* wrong: `w` still points into `out`, not `saved` */
use_elsewhere(&saved);            /* and if `out` goes out of scope, `w` is dangling */

Wrong — returning the state by value from a factory function does the same thing:

proven_sysio_out_t make_logger(void) {
    proven_sysio_out_t out;
    proven_writer_t w = proven_sysio_stdout_buffered(&out, buf);
    (void)w;
    return out;   /* wrong: any writer made from `out` addresses this dead frame */
}

Correct — the state stays put, and the handle travels:

proven_byte_t buf[512];
proven_sysio_out_t out;                                   /* lives as long as `w` */
proven_writer_t w = proven_sysio_stdout_buffered(&out,
    (proven_mem_mut_t){ .ptr = buf, .size = sizeof buf });

(void)proven_fprintln(w, "one syscall, not {}", PROVEN_ARG(100));
(void)proven_writer_flush(w);                             /* or the bytes never happened */

10. Operation behavior classes#

One operation, three honest answers#

"Append this text to that string" has three defensible behaviours when the text does not fit, and most libraries pick one and hide the choice. This library exposes all three, gives them different names, and puts the difference in the signature — because which one you want depends on what the text is, and only the caller knows that.

Consider appending to a filesystem path:

• If the path does not fit, truncating is catastrophic. documents/report.pdf becomes documents/rep, which is a different, possibly existing, file. The operation must fail and change nothing.
• Now consider appending to a log line. If it does not fit, truncating is fine — you would rather have most of the message than none of it — as long as you are told how much was written.
• And appending to a buffer you are building up, where you would simply like it to grow.

The three classes below are those three answers. The one you get is decided by the function name and the presence of an allocator parameter, never by a flag or a global:

• proven_u8str_append(str, data) — no allocator, so it cannot grow: refuses.
• proven_u8str_append_partial(str, data) — returns a count: truncates and tells you.
• proven_u8str_append_grow(alloc, str, data) — takes an allocator: grows.

The default across the library is the first one, and Chapter 0 §5 explains why: a truncated path opens the wrong file, a truncated command runs the wrong command, and a truncated number is a different number.

Wrong — ignoring the count from the truncating form:

(void)proven_u8str_append_partial(&s, huge);   /* wrong: the count WAS the answer */

Several APIs intentionally expose three behavior classes:

Choose the class deliberately. Do not treat a truncating function as an all-or-nothing function.

Wrong — assuming the truncating and the atomic form behave alike:

/* `_partial` wrote what fit and told you so; the error you did not read is the
   difference between "all of it" and "some of it". */
(void)proven_u8str_append_partial(&s, huge);   /* wrong: the result was the point */

11. Manual chapters#

Just finished an introductory C book? Start with the tutorial. It is nine short programs, each introducing exactly one idea: the sixth is the greeting program from this chapter read line by line, and the last three go on to arenas, containers and files. This chapter shows that program on its first page and it carries five new ideas at once; the tutorial hands them over one at a time.

Otherwise start with this chapter. It is the only chapter that assumes nothing: why the library exists, argued from the C bugs it is answering; a hello-world program; how to build; the five contracts the rest of the manual takes for granted; and a glossary plus a libc-to-proven table. Every other chapter assumes it.

The reading order#

The chapters are grouped into parts, and the parts are ordered so that each one only needs the ones before it. That order is not the same as the header dependency graph, and it is not arbitrary: strings need allocators, containers need allocators, and hosted services need strings, so the sequence below is what the material itself requires.

The chapter numbers are stable identifiers, not a reading sequence. Two of them are out of order on purpose: the alias index is an appendix you look things up in, and Chapter 8 is a reference you read after Chapter 3 has introduced the subject.

The chapters#

• Tutorial: the library in nine short programs, one new idea at a time — Part I, optional on-ramp

1. Start here: why this exists, hello world, the five contracts, glossary, libc map — Part I
2. Foundation: types, errors, memory views, alignment, version, panic — Part II
3. Allocation: heap, arena, pool, byte buffers, and the allocator trait — Part II
4. Strings and text: U8, U16, and an introduction to formatting and scanning — Part II; the tutorial half of the text material
5. Containers and algorithms: array, list, ring, map, sort/search, hashing, encoding — Part III
6. Hosted services: filesystem, tree walk, streams, sysio, environment, randomness, mmap, time — Part V
7. Execution and platform: coroutines, jobs, thread-safety, aliases, PAL, cross builds — Part VI
8. Appendix A — Alias index: every alias_xcv.h spelling — reference only; not reading material
9. Formatting and scanning: the full fmt.h and scan.h reference — Part IV; the reference half of the text material

Chapters 3 and 8 both cover the formatter and the scanner, and the division is deliberate. Chapter 3 introduces them alongside strings, with the everyday cases and enough to be productive. Chapter 8 is the complete reference: the full format grammar, every argument constructor, the scanner's error codes and recovery rules, and how to teach the formatter a type of your own. Read Chapter 3 first; reach for Chapter 8 when you need the exact behaviour of a specifier or a failure.

12. Platform support and verification#

Primary verified hosted target:

• Linux x86_64 with GCC or Clang in C23 mode.

Compile-only cross coverage exists when the corresponding toolchains are installed:

• Linux AArch64.
• Linux ARM hard-float.
• Linux i686 through i686-linux-gnu-gcc or gcc -m32 multilib.
• Windows x86_64 and i686 through MinGW/WinAPI paths.
• ARM Cortex-M freestanding.
• RISC-V ELF freestanding.

The cross matrix checks compilation, public header visibility, and target ABI assumptions. It does not replace runtime validation on the target platform.

Freestanding mode builds a reduced subset with OS-backed services removed. See manual-freestanding.md and Chapter 6 for details.

13. Appendix B: glossary#

Terms this manual uses as if they were ordinary words. They are not ordinary C words, and every one of them is load-bearing.

Two rules the chapters follow, so that nothing here has to be guessed at:

• No private vocabulary. Where a widely used word exists for an idea, the manual uses that word. Where the library has invented something, it is defined here.
• Every abbreviation is written out the first time it appears in a chapter, and every one of them is listed below as well.

The Korean edition adds one more: an English term appears with its original spelling in parentheses the first time each chapter uses it — 뷰(view) — so a reader who learned the idea in English can find it, and a reader who did not is never handed an untranslated word.

14. Appendix C: public header map#

How to find things#

There are 35 public headers and one umbrella. #include "proven.h" pulls in everything and is what the examples in this manual do; including individual headers is for when you care about compile time or want the dependency to be visible in the file.

Two things this table tells you that the file names do not:

• Which chapter documents it. Every header has exactly one chapter that explains it, and the build enforces that every public function is named somewhere under manual/ — so if a symbol is not in the chapter you expect, it is in the manual somewhere and this map says where.
• Whether it survives a freestanding build. The headers assigned to Chapter 5 are the hosted ones: they need a filesystem, standard streams, a clock, virtual memory or threads. Everything else compiles with no operating system. The freestanding guide has the authoritative per-module table.

15. Appendix D: the libc map#

If you already write C, this is the fastest way in. Every row links to the chapter that explains the trade.

16. Where to go next#

The chapters are ordered so that each one only needs the ones before it.

If you are an experienced C programmer in a hurry, read §15 above, then Chapter 1, then whichever chapter covers the thing you need. If you are newer, read Parts I and II in order — they are short, and everything later assumes them.