@cella-lang/c

C11 integer types for the Cella proof checker, as a compiled module pack.

C's integers are not mathematical integers: widths depend on the platform, signed overflow, division by zero and out-of-range shifts are undefined behaviour, and char may be signed or unsigned. This library defines the C semantics directly:

• c.Val t — a C value of integer type t (c.tInt p, c.tUChar, c.tBool, …): an integer plus a proof that it lies in the range of t;
• integer promotions and the usual arithmetic conversions compute the result type (c.addV p a b ok : c.Val (cpp.common p s t));
• every operation that can be undefined takes the condition as an argument — for concrete values (cpp.inT refl) (signed: no overflow), unit (unsigned: wraps modulo 2^N), refl (divisor not zero), (c.shlOk refl) / (c.shrOk refl) (shift amount and, for signed <<, a result that fits the result type);
• comparisons and logical operators yield an int 0 or 1, as in C;
• conversions: to _Bool is "not zero", to unsigned is modulo 2^N, to signed wraps (implementation-defined; as clang);
• platforms: c.lp64P (x86-64 Linux/macOS, char signed), c.aarch64P (AArch64 Linux, char unsigned).

Statements reuse the language-neutral statement model of @cella-lang/cpp (cpp.Stmt, cpp.seq, cpp.breakS, cpp.continueS, cpp.returnS); C adds what differs:

• c.ifC, c.whileC, c.doWhileC, c.forC — the condition is a C scalar, true when it is not zero; loops take fuel and end in cpp.outOfFuel rather than assuming termination;
• c.switchC p e blocks refl — the controlling expression is promoted, case labels are converted to the promoted type before comparing; the last argument proves the converted labels are distinct and there is at most one default (in unsigned int, -1 and 4294967295 are the same label, so refl fails).

Output: c.format p fmt args refl : String and c.printf p fmt args refl st (appends to the stream state shared with the C++ model and returns the number of characters as an int), the integer subset of printf: %d %i %u %o %x %X %c %%, flags - + space # 0, field width and precision (digits or *), length modifiers hh h l ll. Arguments go through the default argument promotions (c.argV p x). Undefined behaviour is the precondition c.printfOkB p fmt args = true: a malformed or unknown conversion, too few arguments, an argument whose type does not match the conversion (a signed/unsigned counterpart is allowed only when the value fits both), # with d i u c, 0 or a precision with c, anything inside %%.

import c
def p : cpp.Platform := c.lp64P
def n (v : Int) (ok : cpp.inTB (c.tInt p) v = true) : c.Arg := c.argV p (c.litV (c.tInt p) v ok)
def s : c.format p "%5d|%-+4d|%#x" [n (pos 42) refl, n (pos 7) refl, n (pos 255) refl] refl = "   42|+7  |0xff" := refl   -- accept
def t : String := c.format p "%d %d" [n (pos 1) refl] refl                                                                   -- reject: too few arguments

Arrays: c.Arr t (fixed length; elements may be uninitialized). c.zerosA t n (static, = {0}), c.uninitA t n (automatic), c.initA t n [x0, …] refl ({…}; missing elements are zero, too many initializers do not check). c.at a i (c.readable refl) reads an element that is in bounds and initialized, c.setAt a i x (c.inBounds refl) writes in bounds; the index is a C value of any integer type. c.sizeofA p a is N * sizeof(T) as a size_t. For loops, c.Full t n carries its length and "all initialized" in its type: c.getK f k h / c.putK f k h x take the h : k < n given by a counting loop, so the body needs no separate proof of bounds.

import c
def p : cpp.Platform := c.lp64P
def a : c.Arr (c.tInt p) := c.initA (c.tInt p) 5 [c.litV (c.tInt p) (pos 1) refl, c.litV (c.tInt p) (pos 2) refl] refl
def s : c.get (c.at a (c.litV (c.tInt p) (pos 3) refl) (c.readable refl)) = pos 0 := refl        -- accept: a[3] is zero
def t : c.Val (c.tInt p) := c.at a (c.litV (c.tInt p) (pos 5) refl) (c.readable refl)             -- reject: a[5] is out of bounds

Memory follows CH2O (Krebbers, The C standard formalized in Coq): a program has one memory c.CMem (c.memNew is empty), every allocation is a tree of values (integers, pointers, arrays, struct and union members), and a pointer c.Ptr is NULL or (allocation, path, index) — the path walks struct members and array cells down to an array (a scalar counts as an array of length 1, 6.5.6p7), and the index is the position in it. So &x, &a[i], &s.k and p->name are the same kind of pointer, and a function taking int * or char * works on all of them. c.addrOf t m x is &x, c.load t m q (c.derefOk refl) is *q (not NULL, allocation alive, in bounds, initialized, and the object has type t — reading an int through a long * is strict aliasing, 6.5p7), c.store t m q v (c.storeOk refl) is *q = v, and c.memberPtr m p "k" is &p->k. Arrays decay with c.arrToMem; c.ptrAdd / c.idx require the result to stay inside the same array or one past its end — pointer arithmetic does not cross into the next member — and c.ptrDiff / c.ptrLt require both pointers to be in the same array. c.malloc ct m n fails takes whether the allocation fails as a parameter (the environment's choice; failure returns NULL), so a verdict must hold for both outcomes — dereferencing without a NULL check does not prove. c.calloc zero-fills; c.free requires NULL or a live block from malloc, pointed at its start. c.toVoid / c.fromVoid convert through void*, back to the original type only. c.loadStore proves that *q = v; *q reads v for any memory and pointer.

import c
def t : cpp.IType := cpp.tInt cpp.lp64P
def r : c.Allocated := c.addrOf t c.memNew (c.litV t (pos 5) refl)                                     -- int x = 5; int *q = &x;
def s : c.get (c.load t (c.amem r) (c.aptr r) (c.derefOk refl)) = pos 5 := refl                        -- accept: *q is 5
def u : c.Val t := c.load t c.memNew c.nullP (c.derefOk refl)                                          -- reject: *NULL

Strings are NUL-terminated char arrays in that memory. c.strArr p m "abc" is char s[] = "abc", c.strArrN p m 10 "abc" refl is char s[10] = "abc" (zero-filled; exactly N bytes leaves no NUL), and c.strLit p m "abc" is char *s = "abc" — a read-only allocation, so writing through it does not prove. <string.h>: c.strlen, c.strcmp, c.strncmp, c.strcpy, c.strncpy (writes no NUL when the source is not shorter than n), c.strcat, c.strchr; their preconditions are c.cstrOk refl (a NUL is reachable), c.cstrNOk refl (the first n bytes or a NUL), and c.strcpyOk refl refl etc. (the destination is writable and large enough, no overlap). They work on whatever array the pointer is in, a member array included (strcpy(p->name, "Ann")). printf takes strings with c.argS t m q for %s (width, -, precision; with a precision the array needs no NUL). <ctype.h>: c.isdigit, isalpha, isspace, isupper, islower, toupper, tolower, whose argument must be an unsigned char value or EOF (c.ctypeArg refl).

import c
def p : cpp.Platform := c.lp64P
def C : cpp.IType := c.tChar p
def r : c.Allocated := c.strLit p c.memNew "hello"
def s : c.format p "[%-7s]" [c.argS C (c.amem r) (c.aptr r)] refl = "[hello  ]" := refl                -- accept
def t : c.CMem := c.store C (c.amem r) (c.aptr r) (c.litV C (pos 72) refl) (c.storeOk refl)             -- reject: writes a string literal

Structs are described by their members, c.mCons "x" (c.ctInt t) (c.mCons "next" c.ctPtr c.mNil), and a struct value has type c.Struct ms; every scalar member may be uninitialized on its own. c.initS ms [c.iInt x, …] refl is an initializer list (missing members are zero), c.member ms "x" s / c.setMember ms "x" v s access by name, and c.scalar … refl reads a member that has been initialized. In memory, c.varOf (c.ctStruct ms) s m allocates a struct and c.malloc (c.ctStruct ms) m n fails allocates n of them; c.arrow ms "v" m q refl is q->v and c.arrowSet ms "v" x m q refl is q->v = x — a malloced struct is initialized member by member, so this needs no other member to be initialized. A member can also be reached through a pointer to it (c.memberPtr), so swap(&s.a, &s.b) is the same swap as for two variables. Arrays of structs: c.structArr. A linked list whose every malloc may fail is in tests/t_linked_list.cella, and pointers to members in tests/t_member_ptr.cella.

import c
def I : cpp.IType := c.tInt c.lp64P
def Point : c.Members := c.mCons "x" (c.ctInt I) (c.mCons "y" (c.ctInt I) c.mNil)
def p : c.Struct Point := c.initS Point [c.iInt (c.litV I (pos 1) refl)] refl
def y : c.get (c.scalar (c.member Point "y" p) refl) = pos 0 := refl                                    -- accept: y is zero-filled
def u : c.Val I := c.scalar (c.member Point "y" (c.uninitS Point)) refl                                  -- unknown: y is uninitialized (stricter than C)
def r : c.Allocated := c.varOf (c.ctStruct Point) p c.memNew                                            -- struct Point s = {1};
def py : c.Ptr := c.memberPtr (c.amem r) (c.aptr r) "y"                                                  -- int *py = &s.y;
def z : c.get (c.load I (c.amem r) py (c.derefOk refl)) = pos 0 := refl                                  -- accept: *py is 0

Array parameters are pointers, so a function does not know the length: int sum(int a[], int n) takes the precondition c.readableNB t m a n = true ("n cells after a are readable"), and c.readK t m a n ok k h reads a[k] for h : k < n — the function is checked once for any memory and pointer, and a caller with a concrete array proves the precondition by refl. Writing is the same with c.writableNB / c.writeK, and c.writableAfterWriteK keeps the precondition through a loop. Pointers can be stored in memory (c.addrOfPtr, c.loadP for *pp), and c.mkArgv p ["prog", "x"] builds argv (NUL-terminated strings, a NULL at argv[argc]).

For a debugger, c.ptrText names m q shows a pointer the way the source would write it — &x, a, &a[2], a + 4, &s.k, NULL (names maps allocations to variable names; an unnamed allocation from malloc shows as heap#b) — and c.varJsonPtr gives a pointer variable for the variables panel in the same JSON shape as the C++ and Python models.

Input: c.scanf p "%d %s" [c.tgtInt t, c.tgtChars 8] st refl reads from the input state shared with the C++ model (cpp.ios "12 abc") and returns what was read: c.scanCount p r (the number of assignments, or EOF), c.assignInt r k t old (the k-th assigned value, or the old value when the conversion failed), c.scannedBytes r k and c.scanSt r (the rest of the input). The precondition rejects a target of the wrong type, a result that does not fit (%d reading 99999999999), and a %s that does not fit its array.

Multi-dimensional arrays: c.arr2ToMem t m R C inits refl declares T a[R][C] (nested or flat initializers), and c.at2 t m a R C i j hi hj ok reads a[i][j] with the bounds checked per dimension — a[0][C] is out of bounds for the inner array even though it is inside the object. A function taking int a[][C] gets c.readable2 t m a n C = true and reads with c.read2K.

Floating point: c.Double and c.Float are IEEE 754 binary64 and binary32 (shared with the C++ model). c.dlit m e is the literal m × 10^e; c.toInt t x (c.truncOk refl) truncates toward zero with the result required to fit; division needs a nonzero divisor. printf takes doubles through c.argF (%f %e %g with flags, width and precision), scanf reads them into c.tgtFloat, and c.sqrt, floor, ceil, round, trunc, pow, fmod, fabs, exp, log, log10, log2, exp2, sin, cos, tan, asin, acos, atan, atan2, expm1, log1p, sinh, cosh, tanh, asinh, acosh, atanh, cbrt, hypot follow <math.h> with correctly rounded results (the standard does not require a correctly rounded libm).

Function pointers: a signature c.sig [c.fInt t, …] r describes the type; C functions return Option (none is undefined behavior in that call, e.g. c.addM overflowing). c.fnOf "f" s f takes &f, c.fnCast converts (the pointer remembers the function it points to), and c.call2 s p x y refl calls through it — the proof says the pointer is not NULL, its type matches the function, and the call is defined. c.qsort and c.bsearch take a comparator c.FnPtr (c.cmpSig p t) that must be a consistent total order on the array.

Memory functions: c.realloc m q n fails ok keeps the first min(old, n) cells and ends the old allocation (failure is a parameter, as with malloc; n = 0 is not in the subset). c.memcpy, c.memmove and c.memset count elements, not bytes; memcpy requires the two ranges not to overlap.

Unions: c.ctUnion ms uses the same member list as a struct. A c.Union ms remembers which member was written last; c.uset writes a member and c.uget ms k u refl reads it only if it is that member (reading another member reinterprets bytes in C, which the model does not represent). c.initU ms [c.iField "k" v] refl is = {.k = v}.

More of <string.h>: c.strstr, c.strrchr, c.strncat (reads at most n bytes of the source), and c.memcmp / c.memchr on character arrays (on int arrays memcmp compares bytes in memory order, so its sign depends on the representation).

Tokens and lines: scanf supports %[...] (scan sets, ^ for the complement); c.strtok makes the hidden state of strtok an explicit value — pass c.tokInit the first time and the previous c.tokState (with a NULL string) afterwards.

Formatting into memory: c.sprintf and c.snprintf write c.format's output into a buffer (the output must fit and must not overlap a %s argument; snprintf truncates to n − 1 bytes and returns the full length); c.sscanf reads from a string in memory.

Character and line I/O: c.putchar, c.puts, c.getchar (EOF at the end of input) and c.fgets (at most n − 1 bytes, keeping the newline) share the cpp.IOS state with printf and scanf.

Number conversions: c.atoi (overflow is undefined, so the result must fit), c.strtol (base 0 or 2–36, clamps to LONG_MAX / LONG_MIN and reports where it stopped), c.abs and c.labs (the most negative value is excluded).

Variable length arrays: c.vla t m n ok declares T a[n] with a run-time length that must be positive, and c.vla2 declares T a[r][c]; the elements start uninitialized.

Const objects: c.constArrToMem and c.constAddrOf allocate read-only storage, so writing through a pointer that cast the const away (or passing the array to a function that writes it) is rejected.

Random numbers: the sequence of rand is implementation-defined, so it is a parameter (c.RandEnv) and a verdict holds for every environment — e.g. rand() % 6 + 1 is between 1 and 6 for any RAND_MAX ≥ 32767 and any sequence.

Files: c.FState is the file system (an environment given by c.fsInit) plus the open files. c.fopen takes a fails parameter like malloc, so the NULL check is required; c.fscanf, c.fgetsF, c.fgetc, c.fprintf, c.fputs and c.fclose require the handle to be open in a suitable mode.

goto: a function body is a table of labeled blocks (c.withLabels); c.gotoS "l" leaves nested loops and ifs like a return and resumes at block l, and c.retJ is the real return. Labels live at the top level of the body.

Length modifiers z, j and t (printf("%zu", strlen(s))) use the LP64 types: size_t is unsigned long, ptrdiff_t and intmax_t are long.

sizeof: c.sizeofV pl ct computes sizes from a type descriptor (struct padding follows the LP64 ABI, which is implementation-defined); c.strspn, c.strcspn and c.strpbrk complete the common <string.h> functions.

The integer core shared by the C family (type descriptors, platforms, promotions) comes from @cella-lang/cpp; C's value type is its own, and its relation to C++'s is a proved path on the fragment where both languages agree.

import c
def p : cpp.Platform := c.lp64P
def x : c.Val (c.tInt p) := c.addV p (c.litV (c.tInt p) (pos 2) refl) (c.litV (c.tInt p) (pos 3) refl) (cpp.inT refl)   -- accept
def y : c.Val (c.tInt p) := c.shlV p (c.litV (c.tInt p) (pos 1) refl) (c.litV (c.tInt p) (pos 31) refl) (c.shlOk refl)   -- reject: 1 << 31 does not fit int

Loading

The pack only loads into the cella-lang build named by index.json (checkerHash, cbfVersion), on top of the packages it depends on (index.requires.packages, here @cella-lang/cpp); the peerDependencies entries pin those versions.

import init, { init_stdlib_cached, load_module_pack, load_library_pack, check } from 'cella-lang';
import assets from 'cella-lang/assets';
// 1. the standard modules it and its dependencies need: index.requires["cella-lang"].modules
for (const m of JSON.parse(index).requires['cella-lang'].modules) load_module_pack(await bytes(assets.module(m)));
// 2. the packages it depends on, in order: index.requires.packages (each with its own index.json)
load_library_pack(cppIndex, 'cpp', await bytes(cppPackUrl));
// 3. the library itself
const r = JSON.parse(load_library_pack(index, 'c', await bytes(new URL('./c.cell', libUrl))));
if (!r.ok) throw new Error(r.error);

Per-definition hashes

index.json lists, for every definition, own (its own content) and merkle (its content plus everything it depends on).