91 What proven is — and getting started

91.1 Why this library exists#

The previous chapter showed, in code that actually runs, five kinds of defect that have been shipping for half a century. From here on we look at an answer to each. But before taking out the tool, it is the right order to say where it came from and where it stops. This section sets down four things in turn: why it was made, what it tries to do differently, what has been verified, and what has not been verified yet.

Why it was made. Because the author, writing C, kept slipping at the same places. Those places are ones this book has already gone through one by one — the limits of representation (chapters 6 and 28), conversions that happen without a sound (chapter 29), the lifetime of memory (chapters 36 and 44), errors that do not arrive as values (chapters 38 and 79), and standard library functions whose contract lives only in the documentation (chapters 69–70). Getting burnt once teaches a habit, but habits fail when a person is tired. So the beginning was to make parts instead of habits.

What it tries to do differently. It takes the direction recent systems programming has moved in — treating errors as values, writing bounds and lifetimes into the type, taking the allocator as a parameter, pinning strings to UTF-8, cutting parts small enough to be checked — and implements it in C23. It is closer to an experiment measuring how much of what a new language gives you can be had in the places you cannot move away from.

Its place in this book. proven does not replace standard C, and it does not withdraw what the preceding eighty-nine chapters taught. The problems were explained earlier without proven; here we look at one solution among others. Choosing a different one, or writing your own, is fine — the earlier knowledge serves you there too.

What has been verified. What this book puts on the page is narrow and clear. All 223 examples in the book, including this part’s 29, are compiled and run on every build, and their output is printed here as captured (GCC as the base, with Clang as a cross-check). The edition shipped alongside is one snapshot, in vendor/proven/. That is to say: the code printed here runs in this environment — and no further.

What has not been verified. Everything beyond that is unverified. proven has not been used in a large project, has not been operated for years, has not passed through many independent users, and has not had an independent security audit. Neither its API nor its ABI (application binary interface) is promised yet. Where words like “modern”, “safe” or “stable” appear in this part, they name the direction the design aims at, not a proof of maturity. The material for deciding whether to use it in real work is tabulated in chapter 99 — what has been confirmed, what has not, and what may still change.

91.2 What the name says — provenance#

The name comes from a word used about art. Provenance is an object’s documented history — where it came from, whose hands it passed through, how it got here. A painting without provenance may be genuine, but nobody can prove it.

Chapter 38 already showed that C’s memory model uses the word in almost that same sense. A pointer carries not only an address but an invisible tag saying which object it was derived from, and the optimiser treats that tag as real. Two pointers can therefore hold the same address, bit for bit, and still refer to different things.

The name was chosen because the library’s answer aims at exactly that place. Writing provenance-clean code “by being careful” is not something a person does reliably — the rule is invisible, and a violation shows up only when the optimisation level goes up. So the choice was to keep raw pointer arithmetic inside one narrow place. A view carries a pointer and a length; a container knows its own extent. Then “walk two buffers as if they were one” becomes a sentence you cannot write by accident.

91.3 What it means to replace#

In one line: to replace the tired parts of the standard library, from the bottom up, without excluding it.

The functions Part XI went through one at a time — strcpy, strtok, sprintf, errno, qsort, rand, atoi — each either does not know a size, carries hidden state, or does not give failure back as a value. proven answers each with something sized, checked, and explicit.

It is not a replacement for libc, though. This library does not want your main.

Use one module or all of them. They sit beside whatever you already link.

91.4 The promises that shaped the design#

Here is the list the nine chapters of this part unfold one by one. Each line is a chapter’s subject.

• Ownership is in the signature. Who allocates and who gives back is written in the parameter list and the return type (chapter 94).
• Failure is in the return type. A function that can fail returns its result as a value, and the important ones are [[nodiscard]], so the compiler stops you from dropping the error (chapter 92).
• It refuses rather than truncates. A path that does not fit is an error, not a shorter path — which is precisely what the strlcpy argument in chapter 70 was about (chapter 95).
• It stays failure-atomic. Where the documentation says so, a failed grow leaves your data intact (chapter 97).
• A borrowed view is a different type from an owning one. The type states the lifetime (chapter 93).
• The platform lives in one layer. Code that calls the operating system does not leave platform/, so a freestanding build drops it whole (chapter 99).

91.5 What it is not#

It is better for both sides to write down the roads not taken.

• Not a libc replacement. Not a garbage collector, not a framework. It does not take your process, your build graph, or your error policy.
• Not a cryptography library. There are hashes (SHA-256 among them) and OS-strength randomness, but signatures, key exchange, password hashing (KDFs), authenticated encryption and TLS are deliberately absent.
• The platform layer does not cover everything. It covers memory, files, time, mapping, environment variables, console I/O and threads. It does not cover process control (fork, exec, pipes), terminal control, or networking — a program whose substance is one of those will call POSIX or Win32 directly, and the “no platform #ifdef” property does not reach that far.
• Not a memory-safe language. This is C. Break a contract and it breaks. The library only makes breaking harder, and being broken more visible.

91.6 The choice of having nothing to install#

proven has no installation procedure. Compile the source you have obtained together with your program and that is all. The source ships inside this book’s repository, github.com/rubidus-api/proven_c_book, under vendor/proven/. There are only two directories that matter.

• src/proven/ — the portable body. The operating system is not called here.
• platform/ — a thin layer that makes system calls. It is the only part that must be changed when moving to a new machine.

In an environment with no operating system (embedded) it is built without platform/. This separation settled the shape of the whole library — the demand “it must run anywhere” becomes the discipline “keep neither hidden allocation nor hidden global state”.

91.7 How this book’s examples are built#

To state it honestly, this book’s proven examples are compiled as follows. The library’s source is made into object files once and linked with the example.

$ cc -std=c23 -O1 -Ivendor/proven/include -c vendor/proven/src/proven/*.c
$ cc -std=c23 -Wall -Wextra -Werror -Ivendor/proven/include \
     hello.c vendor-obj/*.o -lm -o hello

The first line handles the body, the second my program. -I tells it where to find headers (chapter 56), -lm joins the mathematical functions. These two lines are what this book’s verification script really runs every time, and every execution result printed on these pages is the output of a program made that way.

91.8 The first program#

One #include <proven.h> opens the whole library.

#include <proven.h>

int main(void)
{
    const char *name = "world";
    int         count = 3;
    double      ratio = 0.75;
    bool        ready = true;
    char        grade = 'A';

    /* {} is only a placeholder and has no type. The type comes from the argument */
    proven_println("Hello, {}! You have {} messages.",
                   PROVEN_ARG(name), PROVEN_ARG(count));

    /* whatever the type, it goes through the same placeholder */
    proven_println("ratio={} ready={} grade={}",
                   PROVEN_ARG(ratio), PROVEN_ARG(ready), PROVEN_ARG(grade));

    /* the format specification goes after the colon — width, alignment, digits */
    proven_println("|{:>8}|{:<8}|{:.3}|",
                   PROVEN_ARG(name), PROVEN_ARG(name), PROVEN_ARG(ratio));
    return 0;
}

Hello, world! You have 3 messages.
ratio=0.750000 ready=true grade=A
|   world|world   |0.750|

We read it line by line. proven_println takes a format and arguments and prints one line to standard output — so far the same as printf. What differs is the placeholder.

• {} has no type in it. It is neither %d nor %s but simply {}.
• The type comes from the argument. PROVEN_ARG(x) looks at x’s type and wraps the value with a fitting tag attached.
• So chapter 90′s third bug — the mismatch of format and argument — structurally cannot happen. The type is not written twice, so there is no place for them to go out of step.

What is written after the colon, as in {:>8}, corresponds to the width, alignment and precision seen in chapter 66. > is right alignment, < left alignment, .3 is to three decimal places. That the alignment symbol comes first is what differs from printf.

91.9 Three rules — the key to this whole part#

The functions ahead number more than a hundred, but the rules for reading their signatures are only three. Get these three into your hand and you can read half of any function you have never seen, without the documentation.

1. Only a function that takes an allocator as an argument takes memory. If proven_allocator_t appears in the signature it means “this function may allocate”, and if it does not, it takes not one byte. So which functions are usable in embedded work and which are not divide before your eyes (chapter 94).
2. Failure comes as a value. If there is no result to return it gives a single proven_err_t; if there is, an {err, value} bundle. Before checking err you do not look at value (chapter 92).
3. Give a thing back with the allocator you made it with. What was obtained with _create is let go with _destroy, and what has view in its name is borrowed and is not destroyed (chapters 93–94).

The naming rules have almost no exceptions either.

91.10 The life of one object#

Rather than reading three lines of rules, it is quicker to follow one real thing to the end. The program below holds the whole course of making, using and giving back a string object on one screen.

/* The first real program — the whole course of making an object, using it and
   giving it back. The skeleton of a proven program is all in this one file. */
#include <proven.h>

/* (1) Where does the memory come from — the caller decides (the allocator parameter).
   (2) Failure arrives as a value — value is not looked at before err is checked.
   (3) What was made is given back through the allocator it was made with. */
static proven_err_t build_line(proven_allocator_t alloc,
                               proven_u8str_view_t who,
                               int count,
                               proven_u8str_t *out)
{
    /* a string with room for 64 bytes, obtained from alloc */
    proven_result_u8str_t made = proven_u8str_create(alloc, 64);
    if (!proven_is_ok(made.err))
        return made.err;

    proven_u8str_t line = made.value;      /* taken out only after the check */

    /* Appended through a format. On failure the original is left untouched.
       Formatting returns, along with err, "bytes written / bytes needed" */
    proven_fmt_result_t r = proven_u8str_append_fmt(&line, "{} has {} message(s)",
                                                    PROVEN_ARG(who), PROVEN_ARG(count));
    if (!proven_is_ok(r.err)) {
        proven_u8str_destroy(alloc, &line); /* returned on the failure path too */
        return r.err;
    }

    *out = line;                            /* ownership passes to the caller */
    return PROVEN_OK;
}

int main(void)
{
    /* the heap allocator — standard malloc wrapped in the library's interface */
    proven_allocator_t alloc = proven_heap_allocator();

    proven_u8str_t line;
    proven_err_t e = build_line(alloc, PROVEN_LIT("alice"), 3, &line);
    if (!proven_is_ok(e)) {
        proven_println("build failed: {}", PROVEN_ARG((int)e));
        return 1;
    }

    /* an owned string -> a borrowed view. A view is valid only while the original lives */
    proven_u8str_view_t v = proven_u8str_as_view(&line);
    proven_println("line   = {}", PROVEN_ARG(v));
    proven_println("length = {} bytes", PROVEN_ARG(v.size));

    /* the meeting point with old APIs that need NUL termination (no copy, no allocation) */
    proven_println("as C string = {}", PROVEN_ARG(proven_u8str_as_cstr(&line)));

    proven_u8str_destroy(alloc, &line);     /* through the very allocator it was made with */

    /* Destroying empties the struct to zero — so it cannot point at the returned
       buffer again. Hence the length after destroying is 0, and the contract is
       that this object is not used any further. */
    proven_println("after destroy, length = {}",
                   PROVEN_ARG(proven_u8str_as_view(&line).size));
    return 0;
}

line   = alice has 3 message(s)
length = 22 bytes
as C string = alice has 3 message(s)
after destroy, length = 0

Six places to point at.

① It took an allocator as an argument. That build_line’s first argument is an allocator is the declaration that “this function may take memory”. The caller settles whether to give it the heap or an arena (chapter 94).

② Making returns a bundle. proven_u8str_create gives a proven_result_u8str_t (that is, {err, value}). Before checking err you do not take value out — that order is the whole of chapter 92.

③ The capacity is “by content”. The 64 of create(alloc, 64) is the number of bytes of content to hold, and the library internally takes one more byte for the NUL. That is how as_cstr can hand out a C string without copying.

④ The failure path gives back too. If formatting fails, the string taken so far is returned with destroy before the error is raised. Grow this pattern and it becomes chapter 92′s goto cleanup idiom.

⑤ The place where ownership passes is explicit. *out = line; is that place. After this line the string’s owner is the caller, and the responsibility to destroy it is the caller’s too.

⑥ Destroying empties the struct. That the length prints as 0 after destroy is the evidence. It is so that the returned buffer is not still pointed at, and the contract that a destroyed object is not used again stands as it is.

/* ① taking value out without checking */
proven_u8str_t s = proven_u8str_create(alloc, 64).value;   /* rubbish on failure */

/* ② destroying with a different allocator */
proven_u8str_destroy(other_alloc, &s);                     /* contract violation */

/* ③ holding a view longer than its original */
proven_u8str_view_t v = proven_u8str_as_view(&s);
proven_u8str_destroy(alloc, &s);
proven_println("{}", PROVEN_ARG(v));                       /* reads a dead place */

/* ④ forgetting PROVEN_ARG */
proven_println("count={}", count);                         /* does not compile */

91.11 Attaching it to your own project — a minimal Makefile#

To avoid typing the two lines above every time, use chapter 101′s make. Supposing the library has been put whole into vendor/proven, this much suffices.

CC      = cc
CFLAGS  = -std=c23 -Wall -Wextra -Werror -O2 -Ivendor/proven/include
VSRC    = $(wildcard vendor/proven/src/proven/*.c) \
          $(wildcard vendor/proven/platform/*.c)
VOBJ    = $(VSRC:.c=.o)

app: app.o $(VOBJ)
  $(CC) $^ -lm -o $@

clean:
  rm -f app app.o $(VOBJ)

Only three things need be known. -I tells it where to find <proven.h> (chapter 56). platform/ is the thin layer that calls the operating system, so when going to bare metal only this line is removed (chapter 99). -lm joins the mathematical functions that real-number formatting uses — take reals out of the formatter (chapter 99′s PROVEN_FMT_NO_FLOAT) and this is not needed either.

The first program has run. Yet the proven_println just used can in fact fail too — because the band going to the screen may break (chapter 9). This function returns an error but does not compel a check, and that choice itself is a good entrance to understanding this library’s error model. The next chapter is that.