The standard library

Every module of the standard library, in the order of its name, with the head of its interface: what it is for, what it guarantees, and an example. The modules named Bindings bind a C library and are unsafe; which safe module stands on each is in the unsafe modules.

Bindings.Account

Binds the lookup of an account in the password database and the effective user of the process, from the runtime.

let user: Int64 := accountNumber("_notes", false);

Bindings.Arena

Binds the arena of the runtime, which takes memory with mmap and hands out pieces.

let made: Option[Arena] := createArena(65536);
let got: Option[Span![Int32, R]] := arenaSpan(r, 100);

Bindings.Argon2

Binds libargon2, the reference implementation of Argon2, through Bindings.C.Argon2.

let tag: Option[String] := argon2id(asSpan(&password), asSpan(&salt), 3, 65536, 4, 32);

Bindings.Array

Binds the reading and writing of numbers in little endian bytes, with @embed in plain C.

let x: Float64 := loadFloat64(bytes, 8);

Bindings.Bcrypt

Binds the check of a bcrypt hash through the system's own library, by a function of the runtime.

let verdict: Int32 := bcryptCheck(asSpan(&password), asSpan(&stored));

Bindings.Bits

Binds the reading of the bits of a number as a number of another type of the same width, in C.

let bits: Nat64 := float64Bits(1.0);

Bindings.BuildInfo

Binds what the compiler writes into the C of the programme about its build.

let hash: Span[Nat8, Static] := commitText();

Bindings.Context

Binds what Standard.Context needs of the kernel and the runtime: pipes and a chain to wait on.

let root: Node := emptyNode();
let ready: Int32 := nodeReady(&root, 0);
releaseNode(root);

Bindings.Database

Binds nothing outside: it holds a driver's value in a box whose type does not name the driver.

let box: Erased := erase(connection);

Bindings.DuckDB

Binds libduckdb, DuckDB's release build, through the declarations of Bindings.C.Duckdb.

let opened: Either[DuckError, Connection] := connect("/var/db/stats.duckdb", false);
let changed: Either[DuckError, Nat64] := execute(&!db, "DELETE FROM hits", noValues());

Bindings.Entropy

Binds getentropy, the system's call for a few bytes of secure random, for the keys of hash maps.

let seed: Nat64 := entropyWord();

Bindings.File

Binds the file, directory, process, environment and socket calls of the C library, through the runtime.

let number: Int32 := openRead(&path);
let read: Int64 := readInto(number, &!buffer, 0, 4096);
let closed: Bool := closeNumber(number);

Bindings.Libcrypto

Binds libcrypto through the declarations in Bindings.C.Libcrypto.

let digest: Option[String] := sha256(asSpan(&message));
let sealed: Option[String] := sealAes256Gcm(asSpan(&key), asSpan(&nonce), asSpan(&text), "");

Bindings.MariaDB

Binds libmariadb, MariaDB Connector/C, through the declarations of Bindings.C.Mariadb.

let opened: Either[MariaError, Connection] := connect("db.example.org", 3306, "shop", "app",
    asSpan(&password), "/etc/ssl/cert.pem", false);
let changed: Either[MariaError, Nat64] := execute(&!db, "DELETE FROM carts", noValues());

Bindings.MlDsa

Binds ML-DSA of FIPS 204 from the libcrux code the compiler carries, the backend of Standard.MlDsa.

let made: Option[KeyBytes] := keypair(44, asSpan(&seed));

Bindings.Pcre

Binds the 8-bit library of PCRE2, libpcre2-8, through the declarations in Bindings.C.Pcre2.

let compiled: Either[String, Code] := compileCode("[a-z]+", 1000000);
let found: Either[Int32, Option[Buffer[Index]]] := search(&regex, asSpan(&text), 0);

Bindings.Platform

Binds the names of the system and the machine the programme was compiled for, and of its host, from the runtime.

let system: Span[Nat8, Static] := systemText();

Bindings.Poller

Binds the poller of the runtime, which waits on many descriptors at once.

let added: Bool := addDescriptor(&!handle, listener, 1);
let ready: Int32 := waitHandle(&!handle, 1000);
let first: Int32 := eventDescriptorAt(&handle, 0);

Bindings.Postgres

Binds libpq, the client library of PostgreSQL, through the declarations of Bindings.C.Libpq.

let values: Values := withInt64(noValues(), 42);
let changed: Either[PgError, Nat64] := execute(&!db, "DELETE FROM cart WHERE id = $1", values);

Bindings.Resolve

Binds the resolver of the C library, getaddrinfo, for Standard.Resolve.

let found: Either[Int32, String] := resolveRecords("example.org");

Bindings.Resource

Binds the resource calls of the runtime: limits, usage and the boot clock.

let files: Option[LimitPair] := limitOf(1);
let raised: Bool := setLimitOf(1, 4096, 4096);

Bindings.Sandbox

Binds the calls that confine the process, through the functions of the runtime.

if platform() = 1 then
    let pledged: Int32 := pledge(&promises);
end if;

Bindings.Secret

Binds the reading of a secret from the terminal or a descriptor, into memory that is wiped before it is given back.

case allocateRaw() of
    when Some(value as raw: RawSecret) do
        destroyRaw(raw);
    when None do
        skip;
end case;

Bindings.Serial

Binds a count shared by the whole process, for numbers that must never repeat.

let serial: Nat64 := nextSerial();

Bindings.Shared

Binds the mutexes of the runtime and the atomic operations of the C compiler.

let { value: Nat64, key: Key } := acquire(&mutex);
release(&mutex, value + 1, key);

Bindings.Signal

Binds the signal handling of the runtime, with alarm(2), getpid(2) and kill(2).

if watchMask(7) then
    let woken: Bool := waitPipe(1000);
    let stops: Nat32 := arrivals(2);
end if;

Bindings.SqlCipher

Binds libsqlcipher, the C library of SQLCipher, through the declarations in Bindings.C.SqlCipher.

case openWriter("app.db", makeKey(secret)) of
    when Right(right as db: Connection) do
        closeDatabase(db);
    when Left(left as error: SqlError) do
        printLn(describe(error));
end case;

Bindings.Sqlite

Binds libsqlite3, the C library of SQLite, through the declarations in Bindings.C.Sqlite3.

case openWriter("app.db") of
    when Right(right as db: Connection) do
        closeDatabase(db);
    when Left(left as error: SqlError) do
        printLn(describe(error));
end case;

Bindings.SqliteReplica

Binds libsqlite3 through the declarations in Bindings.C.Sqlite3, for statements whose text is known only when they run.

let opened: Either[String, Database] := openDatabase("data.db");

Bindings.SystemLog

Binds the system log, openlog(3), syslog(3) and closelog(3), through the runtime.

openSystemLog("shop", 1);
writeSystemLog(1, "started");
closeSystemLog();

Bindings.Task

Binds the fibers, scopes and channels of the runtime, which run tasks on threads.

let started: Either[Nat64, Task[Nat64]] := spawn(&!scope, double, 21);

Bindings.Terminal

Binds the standard streams of libc, stdin, stdout and stderr, through the runtime.

if isTerminalNumber(0) then
    let quiet: Bool := setEcho(0, false);
end if;

Bindings.Testing

Binds what Standard.Testing asks the runtime: whether the programme runs under valgrind.

let underValgrind: Bool := runningUnderValgrind();

Bindings.Time

Binds the clocks of libc through the runtime, which calls clock_gettime.

if hasMonotonic() then
    let now: Int64 := monotonicReading();
end if;

Bindings.Tls

Binds libtls, the TLS library of OpenBSD and, as libretls over OpenSSL, of Debian.

let client: Either[String, Client] := connect("example.org", "443", "/etc/ssl/cert.pem");

Bindings.Watch

Binds the watching of files in the runtime: inotify on Linux, kqueue on the BSDs.

let watcher: Int32 := watchOpen();
let watch: Int32 := watchAdd(watcher, &path, true);
let changed: Int32 := watchWait(watcher, 5000);

Bindings.X509

Binds the X.509 and key functions of libcrypto that Standard.X509 needs.

let key: Option[Key] := newKey(1);

Standard.About

The full version text and the info text of a programme, from its build and its platform.

setFullVersion(&!command, fullVersion("1.2.0", "2026 Example Corp"));

Standard.Account

The accounts of the system: the numbers of an account by its name, and who the process runs as.

case lookupAccount("_notes") of
    when AccountFound(numbers as n: AccountNumbers) do
        useOwner(n.user, n.group);
    when NoAccount do
        refuse();
    when LookupFailed do
        refuse();
end case;

Standard.Acme

A client of the ACME protocol of RFC 8555, by which a CA issues certificates for DNS names.

let opened: Either[AcmeError, Account] := openAccount(directory, key, "", caFile, limits);
let order: Either[AcmeError, Order] := newOrder(&!account, "example.org,www.example.org");
let challenge: Either[AcmeError, Challenge] := challengeOf(&!account, authorization, "dns-01");
let record: String := dnsChallengeValue(&!account, asSpan(&token));
let ready: Either[AcmeError, Unit] := respond(&!account, challengeUrl);

Standard.Archive

Archives in tar, tar with gzip and zip, read whole and written in memory.

case readArchive(asSpan(&bytes), TarGz(), defaultBudget()) of
    when Right(right as archive: Archive) do
        let unpacked: Either[Failure, Unit] := extractArchive(&archive, "/var/www/site");
        destroyArchive(archive);
    when Left(left as failure: Failure) do
        report(failure);
end case;

Standard.Arena

A bump allocator behind a linear handle, for the memory of one unit of work such as one request.

case createArena(65536) of
    when Some(value as made: Arena) do
        var arena: Arena := made;
        borrow r: &![Arena, R] := &!arena do
            let got: Option[Span![Int32, R]] := arenaSpan(r, 100);
        end borrow;
        arena := resetArena(arena);
        freeArena(arena);
    when None do
        abort("No memory for the arena.");
end case;

Standard.Arguments

Reading a programme's command line against a declared command, its options and subcommands.

var command: Command := makeCommand("fetch", "Fetches a file.");
let verbose: FlagKey := addVerbose(&!command, "Say more.");
let output: PathKey := addPath(&!command, option("output", 0, "Where to write."));
let arguments: Buffer[String] := processArguments();
let parsed: Either[ArgumentError, Outcome] := parse(&command, &arguments);

Standard.Array

Arrays of numbers with a shape, strides and an element type, and views that share their bytes.

var a: Array := zeros(float64Type(), shape2(2, 3));
setFloat64(&!a, 4, 2.5);
let n: Index := size(&a);
destroy(a);

Standard.ArrayWire

The binary form of an owning array: a header with magic, version, element type, rank and shape, then the elements.

let written: Index := encode(&a, &!out);
case decode(received) of
    when Right(right as b: Array) do
        destroy(b);
    when Left(left as e: DecodeError) do
        skip;
end case;

Standard.ArrayCompute

Arithmetic over arrays: elementwise operations with broadcasting, reductions over the whole array and along one axis, and the joining of partial results.

var a: Array := zeros(float64Type(), shape2(2, 3));
setFloat64(&!a, 4, 2.5);
let total: Array := sum(view(&a));
destroy(total);
destroy(a);

Standard.AtomicFile

Writing a file so that whoever opens it finds the old content or the new, never a part.

let mode: Nat32 := 420;
let written: Either[AtomicFailure, Bool] := writeWithBackup("app.conf", asSpan(&text), mode);
let change: Either[AtomicFailure, Change] := writeIfChanged("app.conf", asSpan(&text), mode);

Standard.Base32

Base32 after RFC 4648, section 6, the form in which the secrets of one-time passwords are written.

let secret: String := encodeBase32Unpadded(asSpan(&key));
let back: Option[String] := decodeBase32(asSpan(&secret));

Standard.Base64

Base64 after RFC 4648, section 4, padded or unpadded.

let text: String := encode(asSpan(&bytes));
let back: Option[String] := decode(asSpan(&text));
let salt: Option[String] := decodeUnpadded("c2FsdHNhbHQ");

Standard.Bits

Reads the bits of a number as an unsigned number of the same width, and back, for formats that store numbers as bytes.

let one: Float64 := float64FromBits(float64Bits(1.0));

Standard.Bounded

A typeclass for the smallest and the largest value of a type.

let top: Nat32 := maxBound();
let bottom: Int64 := minBound();

Standard.Box

One value on the heap, owned by a linear handle.

case makeBox(7) of
    when Right(right as box: Box[Nat64]) do
        let seven: Nat64 := unbox(box);
    when Left(left as value: Nat64) do
        skip;
end case;

Standard.Buffer

A linear, growable array on the heap.

var prices: Buffer[Nat64] := allocateEmpty();
insertBack(&!prices, 250);
let first: Nat64 := nth(&prices, 0);
destroyFree(prices);

Standard.BuildInfo

What a programme knows about its own build: commit, state of the work tree, time, compiler and its own values.

printLn(commit());
case value("channel") of
    when Some(value as channel: Span[Nat8, Static]) do
        printLn(channel);
    when None do
        printLn("no channel");
end case;

Standard.Cache

A cache of values under keys, with a lifetime per entry and limits on count and total size.

var cache: Cache[Nat64, Nat64] := makeCache(1000, 1048576, 60000000000);
let price: Option[Nat64] := getWith(&!cache, item, nowNanos(), lookUpPrice);

Standard.Calendar

Dates and times of day in the Gregorian calendar, time zones from zone files, and RFC 3339 text.

let zone: Either[ZoneFailure, Zone] := loadZone("Europe/Berlin");
let stamp: Option[Stamp] := parseRfc3339("2026-09-27T01:10:00+02:00");

Standard.Cbor

CBOR as RFC 8949 defines it, read strictly into a document and looked into by items.

case readCbor(asSpan(&coseKey)) of
    when Right(right as key: Cbor) do
        let top: CborItem := rootOf(&key);
        let entries: Option[Index] := countOf(&key, top);
        destroyCbor(key);
    when Left(left as refused: CborError) do
        printLn(refused.offset);
end case;

Standard.CompositeSig

Signs and verifies with the composite of ML-DSA-44 and Ed25519 of the IETF draft for composite signatures.

let signed: Option[String] := sign(&key, openSshLabel(), asSpan(&message), "");

Standard.Context

Cancellation and deadlines that reach a whole chain of calls and tasks.

let root: Context := background();
case withTimeout(&root, 5000) of
    when Some(value as made: Derived) do
        let { context: Context, canceller: Canceller } := made;
        let budget: Nat32 := remainingMilliseconds(&context, 1000);
        cancel(canceller);
        destroyContext(context);
    when None do
        skip;
end case;
destroyContext(root);

HTTP cookies after RFC 6265: one cookie read out of a Cookie header, a Set-Cookie value written.

let header: Option[String] := setCookie("session", token, "/", strictOptions());
let sent: Option[String] := cookieValue(asSpan(&cookieHeader), "session");

Standard.Cose

COSE keys of RFC 9052 and RFC 9053 turned into the DER public keys that Standard.X509 verifies with.

case publicKeyFromCose(asSpan(&credentialKey)) of
    when Some(value as der: String) do
        let good: Bool := verifyMessage(asSpan(&der), asSpan(&signed), asSpan(&signature));
        destroyString(der);
    when None do
        printLn("not a key");
end case;

Standard.Csrf

Protection against cross-site request forgery: a token bound to the session, and origin headers.

let token: Option[String] := csrfToken(serverKey, sessionToken);
if changingMethod(verb) and not csrfValid(serverKey, sessionToken, submitted) then
    refuse();
end if;

Standard.Csv

Tables in CSV, as RFC 4180 describes them, read and written.

case readCsv(text) of
    when Right(right as table: CsvTable) do
        let rows: Index := rowCount(&table);
        destroyCsv(table);
    when Left(left as error: CsvError) do
        report(error.line, error.offset);
end case;

Standard.Database

One interface over SQLite, SQLCipher, PostgreSQL and MariaDB, the backend chosen at open.

case openSqlite("app.db") of
    when Right(right as opened: Database[Writing]) do
        var db: Database[Writing] := opened;
        let values: Values := withText(withInt64(noValues(), 7), "Ada");
        case execute(&!db, "INSERT INTO people (id, name) VALUES (?, ?)", values) of
            ...
        end case;
        closeDatabase(db);
    ...
end case;

Standard.Database.MariaDB

The MariaDB driver of Standard.Database: a programme that imports it can open a MariaDB connection.

case openMariaDB("db.example", 3306, "app", "app", password, "/etc/ssl/ca.pem") of
    when Right(right as opened: Database[Writing]) do
        ...
end case;

Standard.Database.Postgres

The PostgreSQL driver of Standard.Database: a programme that imports it can open a PostgreSQL connection.

case openPostgres("db.example", 5432, "app", "app", password, "/etc/ssl/ca.pem") of
    when Right(right as opened: Database[Writing]) do
        ...
end case;

Standard.Database.Sqlite

The SQLite and SQLCipher driver of Standard.Database: a programme that imports it can open those files.

case openSqlite("app.db") of
    when Right(right as opened: Database[Writing]) do
        ...
end case;

Standard.DatabaseUsers

A store for Standard.Users in a database of Standard.Database, on every backend it has.

case openDatabaseUsers(db) of
    when Right(right as opened: DatabaseUsers) do
        var users: DatabaseUsers := opened;
        let added: Either[UserError, Bool] := addUser(&!users, "alice", asSpan(&password));
        closeDatabase(closeDatabaseUsers(users));
    when Left(left as failed: DatabaseUsersFailed) do
        let { db: Database[Writing], error: UserError } := failed;
        closeDatabase(db);
end case;

Standard.Decimal

Decimal numbers for money: exact, with at most 18 digits and at most 18 of them after the point.

case parseDecimal("19.99") of
    when Some(value as price: Decimal) do
        let total: Option[Decimal] := multiplyDecimal(price, quantity);
    when None do
        skip;
end case;

Standard.Doctor

Checks that the files, directories, socket and account a programme declares are there as they should be, and makes what is not there.

var checkup: Checkup := makeCheckup("notes", Service());
expectPath(&!checkup, DataDirectory(), "/var/notes");
var out: StringBuilder := makeStringBuilder();
let missing: Index := runCheckup(&checkup, false, &!out);
destroyCheckup(checkup);

Standard.DuckDB

DuckDB, the database for analysis that runs inside the programme over a file of its own.

case openWriter("facts.duckdb") of
    when Right(right as opened: Connection[Writing]) do
        var db: Connection[Writing] := opened;
        let values: Values := withText(withInt64(noValues(), 7), "Ada");
        case execute(&!db, "INSERT INTO people VALUES (?, ?)", values) of
            ...
        end case;
        closeDatabase(db);
    ...
end case;

Standard.Equality

Type classes for partial and total equivalence relations.

let same: Bool := equal(&left, &right);

Standard.Failure

A failure for the Left of an Either: its operation, its kind, its message and the failure behind it.

let failure: Failure := makeFailure("file.write", Unclassified(), "disk full");
let outer: Failure := wrapFailure("store.save", failure);
let line: String := describeFailure(&outer);
destroyFailure(outer);

Standard.Fcgi

The FastCGI record protocol, from the responding side: records read from bytes and built into bytes.

case readHeader(bytes, 0) of
    when Some(value as header: RecordHeader) do
        let content: Option[String] := readContent(bytes, 0, header);
        let next: Index := recordLength(header);
    when None do
        skip;
end case;

Standard.FcgiServer

A FastCGI responder: the loop that serves the requests of a web server through a handler.

function hello(request: Request): String is
    destroyRequest(request);
    return cgiResponse(200, "text/plain", "hello");
end;

let accepted: Option[Index] := serveUnix(&listener, hello, defaultLimits(), &!signals);

Standard.File

Files, pipes, directories, child processes, the environment and sockets of Unix and TCP.

case openRead("notes.txt") of
    when Some(value as opened: FileDescriptor) do
        var file: FileDescriptor := opened;
        let text: Option[String] := readAll(&!file);
        let closed: Bool := closeFile(file);
    when None do
        skip;
end case;

Standard.FileHelpers

Helpers over Standard.File for copying, measuring, naming and removing files and trees.

case copyDirectory("site", "site-backup") of
    when Right(right as done: Unit) do
        skip;
    when Left(left as failure: Failure) do
        let line: String := describeFailure(&failure);
        destroyFailure(failure);
end case;

Standard.Graph

A directed graph whose nodes and edges each carry a value.

var graph: Graph[Nat32, Nat64] := makeGraph();
let from: NodeId := addNode(&!graph, 1);
let to: NodeId := addNode(&!graph, 2);
let added: Either[Nat64, EdgeId] := addEdge(&!graph, from, to, 5);
let reached: Bool := hasPath(&graph, from, to);

Standard.Grapheme

Grapheme clusters, the characters a reader sees, by the rules of Unicode's Standard Annex 29.

let clusters: Option[Index] := countClusters(asSpan(&name));
let firstEnd: Option[Index] := clusterEnd(asSpan(&name), 0);

Standard.Gzip

Compression in the formats of gzip: DEFLATE of RFC 1951, raw or in a gzip member of RFC 1952.

let packed: String := gzip(asSpan(&page));
case gunzip(asSpan(&packed), 1048576) of
    when Right(right as unpacked: String) do
        skip;
    when Left(left as failure: GzipFailure) do
        skip;
end case;

Standard.Hash

Keyed hashing with SipHash, and the type class Hashable that a hash map needs of its keys.

let tag: Nat64 := sipHash24(key0, key1, asSpan(&message));
let slot: Nat64 := hashOf(&name, key0, key1);

Standard.HashMap

A hash map whose keys are hashed with SipHash-1-3 under a key of its own.

var ages: HashMap[Nat64, Nat32] := makeHashMap();
let replaced: Option[Pair[Nat64, Nat32]] := put(&!ages, id, 36);
let age: Option[Nat32] := get(&ages, &id);
destroyFree(ages);

Standard.Html

HTML read into tokens after the tokenizer of the HTML standard, its text taken out, or cleaned.

let clean: String := sanitize(asSpan(&comment), basicPolicy());
let plain: String := textOf(asSpan(&page));

Standard.Htmx

The server side of htmx: its requests told apart, its response headers written, its script served.

if isHtmxRequest(asSpan(&hxRequest)) then
    let line: String := redirectHeader("/done");
    let answer: String := htmlResponse(200, asSpan(&line), "");
end if;

Standard.Http

Questions about an HTTP header block, answered from the text of the block as it stands.

let length: Option[String] := headerValue(asSpan(&headers), "Content-Length");
let upgrade: Bool := valueHasToken(asSpan(&connection), "upgrade");

Standard.HttpClient

An HTTPS client: one request, one answer, then the connection is closed.

let answer: Either[Failure, Response] :=
    request(Get(), "https://example.org/status", "", "", "/etc/ssl/cert.pem", defaultLimits());

Standard.I18n

Translated texts from a catalog that is part of the programme, for templates and for code.

var arguments: Arguments := makeArguments();
addText(&!arguments, "name", "Ada");
let greeting: String := translate(messages(), "de", Greeting(), None(), &arguments);
destroyArguments(arguments);

Standard.IO

The capability to reach the terminal, and the type classes of byte streams.

var terminal: TerminalCapability := acquireTerminal(&!root);
var output: StandardOutput := acquireOutput(&!terminal);
writeByte(&!output, 10);
releaseOutput(output);
releaseTerminal(terminal);

Standard.IO.Terminal

The standard output, the standard error and the standard input of a programme.

var terminal: TerminalCapability := acquireTerminal(&!root);
var input: StandardInput := acquireInput(&!terminal);
let line: String := readLine(&!input);
releaseInput(input);
releaseTerminal(terminal);

Standard.Ini

Configuration files in the INI form: lines of name = value grouped under [section] headers.

let file: IniFile := readIni(asSpan(&text));
let defaults: IniFile := readIni(asSpan(&shipped));
let port: Option[String] := iniValueWith(&file, &defaults, "server", "port");
let verbose: Bool := iniSwitch(&file, "log", "verbose");
destroyIni(defaults);
destroyIni(file);

Standard.Ip

IP addresses, IPv4 and IPv6: parse, render, mask, match and anonymise.

case parseIp(asSpan(&peer)) of
    when Some(value as address: IpAddress) do
        let inside: Bool := inSubnet(address, office, 24);
        let logged: String := ipToString(anonymise(address));
    when None do
        printLn("not an address");
end case;

Standard.Json

JSON as RFC 8259 defines it, read strictly into a document and written through a writer.

var writer: JsonWriter := makeJsonWriter();
beginObject(&!writer);
writeName(&!writer, "id");
writeInteger(&!writer, 42);
endObject(&!writer);
let text: Option[String] := finishJson(writer);

case readJson(asSpan(&body)) of
    when Right(right as document: Json) do
        let id: Option[Int64] := integerAt(&document, "/id");
        destroyJson(document);
    when Left(left as refused: JsonError) do
        printLn(refused.offset);
end case;

Standard.Jws

JSON Web Signatures in the compact form of RFC 7515, JSON Web Keys and OpenID Connect claims.

case verifyWithJwks(asSpan(&token), asSpan(&keySet)) of
    when Some(value as payload: String) do
        let problem: Option[String] :=
            claimsProblem(asSpan(&payload), issuer, clientId, asSpan(&nonce), now, 60);
    when None do
        printLn("token refused");
end case;

Standard.Libcrypto

Authenticated encryption, key agreement, signatures, hashes and secure random bytes.

case randomBytes(12) of
    when Some(value as nonce: String) do
        let sealed: Option[String] :=
            sealChaCha20Poly1305(asSpan(&key), asSpan(&nonce), asSpan(&message), "");
        destroyString(nonce);
    when None do
        printLn("no random bytes");
end case;

Standard.Log

Log entries with a level, a message and named fields, one line each.

var log: Log := logToError(acquireError(&!terminal), Info(), TextLines());
let entry: Entry := addInteger(makeEntry(Warning(), "slow request"), "millis", millis);
let written: Bool := writeEntry(&!log, entry);
let closed: Bool := closeLog(log);

Standard.Map

A map from keys to values, ordered by the TotalOrder of the keys from Standard.Order.

var stock: Map[Nat64, Nat64] := makeMap();
let old: Option[Pair[Nat64, Nat64]] := put(&!stock, item, 12);
let count: Option[Nat64] := get(&stock, &item);
destroyFree(stock);

Standard.MariaDB

A client for MariaDB through the system's libmariadb, in the form of Standard.Postgres.

case openWriter("db.local", 3306, "shop", "app", asSpan(&password), "ca.pem") of
    when Right(right as db: Connection[Writing]) do
        let values: Values := withText(withInt64(noValues(), 7), "apple");
        let changed: Either[MariaError, Nat64] :=
            execute(&!db, "insert into stock (id, name) values (?, ?)", values);
        closeDatabase(db);
    when Left(left as failed: MariaError) do
        printLn(describe(failed));
end case;

Standard.MlDsa

Signs and verifies with ML-DSA of FIPS 204 at the levels 44, 65 and 87.

let key: Option[MlDsaKey] := generateKeyPair(Level44());

Standard.Normalization

The four normalization forms of Unicode for UTF-8 text, NFD, NFC, NFKD and NFKC.

case toNfc(asSpan(&typed)) of
    when Some(value as normal: String) do
        printLn(asSpan(&normal));
        destroyString(normal);
    when None do
        printLn("not UTF-8");
end case;

Standard.Order

Type classes for partial and total orders, with the total orders of integers and strings.

case compare(&left, &right) of
    when LessThan do
        printLn("before");
    when Equal do
        printLn("same");
    when GreaterThan do
        printLn("after");
end case;

Standard.Otp

One-time passwords, HOTP after RFC 4226 and TOTP after RFC 6238, as authenticator apps make them.

let accepted: Bool :=
    verifyTotp(asSpan(&secret), asSpan(&code), nowSeconds, 30, 6, OtpSha1(), 1);

Standard.Password

Passwords stored as Argon2id hashes in the PHC string form, and checked against them.

let stored: Option[String] := hashPassword(asSpan(&typed));
let check: PasswordCheck := checkPassword(asSpan(&typed), asSpan(&saved));

Standard.Path

Taking a path apart and putting one together, as text.

if hasParentComponent(asSpan(&upload)) then
    printLn("refused");
else
    let target: String := joinPath("/var/spool/in", asSpan(&upload));
    let suffix: Option[String] := extension(asSpan(&target));
end if;

Standard.Paths

Where a service or a user tool keeps its configuration, secrets, data, logs and socket on each system.

case choosePath("notes", Service(), PepperFile(), flag, configured) of
    when Some(value as path: String) do
        usePepper(asSpan(&path));
    when None do
        refuse();
end case;

Standard.Pcre

Regular expressions through PCRE2, with its syntax and its engine.

case compile("([a-z]+)@([a-z.]+)", 100000) of
    when Right(right as regex: Regex) do
        let hits: Either[String, Buffer[Hit]] := find_all(&regex, asSpan(&text));
        destroyRegex(regex);
    when Left(left as message: String) do
        printLn(asSpan(&message));
end case;

Standard.PcreJit

Patterns of Standard.Pcre compiled to machine code by the JIT of PCRE2.

case compile("[0-9]{4}-[0-9]{2}-[0-9]{2}", 100000) of
    when Right(right as compiled: Compiled) do
        let { regex: Regex, fallBack: Option[String] } := compiled;
        let found: Either[String, Bool] := match(&regex, asSpan(&line));
        destroyRegex(regex);
    when Left(left as message: String) do
        printLn(asSpan(&message));
end case;

Standard.Platform

The system and the machine the programme was compiled for, and the host it runs on.

print(systemName());
print("/");
printLn(machineName());

Standard.Png

PNG images of 8 bits per channel, written and read.

case decodePng(asSpan(&data), 4194304) of
    when Right(right as image: Image) do
        let file: String := encodePng(&image);
        destroyImage(image);
    when Left(left as error: PngError) do
        reportBadImage(error);
end case;

Standard.Poller

Waiting on many descriptors at once.

case createPoller() of
    when Some(value as made: Poller) do
        var poller: Poller := made;
        let watched: Bool := watchFile(&!poller, &socket, interestRead);
        let ready: Option[Index] := waitFor(&!poller, 1000);
        let first: Option[Event] := nthEvent(&poller, 0);
        destroyPoller(poller);
    when None do
        useBlockingReads();
end case;

Standard.Postgres

PostgreSQL through the system's libpq, with the types and the shape of Standard.Sqlite.

case openWriter(host, 5432, "app", "app", asSpan(&password), caFile) of
    when Right(right as made: Connection[Writing]) do
        var db: Connection[Writing] := made;
        let values: Values := withText(withInt64(noValues(), 42), "Ada");
        let insert: Span[Nat8, Static] := "INSERT INTO people (id, name) VALUES ($1, $2)";
        let changed: Either[PgError, Nat64] := execute(&!db, insert, values);
        closeDatabase(db);
    when Left(left as error: PgError) do
        logLine(describe(error));
end case;

Standard.Qr

QR codes of ISO/IEC 18004, model 2, made from text in Hilde.

case encodeQr("https://example.org/ticket/4711", QrMedium()) of
    when Some(value as code: QrCode) do
        let image: Option[Image] := qrToImage(&code, 8, 4);
        destroyQr(code);
        showImage(image);
    when None do
        reportTooLong();
end case;

Standard.Raft

Raft consensus as a state machine of its own: messages and ticks go in, messages and committed entries come out.

var node: Node := newNode(Config(id => 1, electionTicks => 10, heartbeatTicks => 2, seed => 7, quorum => majority), members);
tick(&!node);
let outgoing: Buffer[Message] := takeMessages(&!node);

Standard.RaftTcp

The messages of Standard.Raft over TCP: each one as bytes behind a length of four bytes.

let sent: Bool := sendMessage(&!socket, &message);
let next: Option[Message] := receiveMessage(&!socket);

Standard.Regex

Regular expressions in linear time.

case compile("^[0-9]+-[0-9]+$") of
    when Right(right as regex: Regex) do
        let isRange: Bool := match(&regex, asSpan(&text));
        destroyRegex(regex);
    when Left(left as message: String) do
        reportPattern(message);
end case;

Standard.Resolve

Host names resolved to addresses through the hosts file and DNS, as the system sets them up.

case resolveHost("mail.example.org", AnyFamily()) of
    when Right(right as addresses: Buffer[IpAddress]) do
        connectToFirst(addresses);
    when Left(left as failure: ResolveFailure) do
        reportFailure(failure);
end case;

Standard.Resource

The resource limits of the process, what it has used, and how long the system has been up.

let cores: Bool := disableCoreDumps();
case readLimit(OpenFiles()) of
    when Some(value as limit: Limit) do
        let wide: Limit := Limit(soft => limit.hard, hard => limit.hard);
        let raised: Bool := setLimit(OpenFiles(), wide);
    when None do
        skip;
end case;

Standard.Sandbox

Confines the running process to what a policy allows, and says what really confines it.

let promised: Policy := allowPromises(makePolicy(), "stdio rpath inet");
let policy: Policy := allowPath(promised, "/var/www", "r");
let report: Report := applyPolicy(policy);
printLine(describeReport(report));

Full-text search in a database of Standard.Database, with the FTS5 module of SQLite.

case search(&!db, asSpan(&typed), 10, 0, "<mark>", "</mark>") of
    when Right(right as hits: Buffer[SearchHit]) do
        renderHits(&hits);
        destroyHits(hits);
    when Left(left as error: SearchError) do
        showNoResults(error);
end case;

Standard.Secret

Passwords and other secrets read from the terminal without echo, held in memory that is wiped when they go.

case readNewSecret("New password: ", "Again: ") of
    when Right(right as secret: Secret) do
        store(secretBytes(&secret));
        destroySecret(secret);
    when Left(left as error: SecretError) do
        refuse(error);
end case;

Standard.Semver

Release versions of the form vX.Y.Z, as git tags carry them, read, written and ordered.

case parseVersion("v1.4.2") of
    when Some(value as version: Version) do
        let text: String := formatVersion(version);
        printLn(asSpan(&text));

Standard.Session

Server-side sessions in a database of Standard.Database, with an idle and an absolute time limit.

let limits: SessionLimits := defaultSessionLimits();
case loadSession(&!db, asSpan(&cookieToken), limits, now) of
    when Right(right as found: Option[String]) do
        serveWith(found);
    when Left(left as error: SessionError) do
        reportFailure(error);
end case;

Standard.Setup

The subcommands setup and user of a programme: its vault of secrets, its completion and manual, and its users.

let setup: SetupKeys := addSetup(&!root);
case parse(&root, &arguments) of
    when Right(right as outcome: Outcome) do
        useOutcome(outcome);
    when Left(left as error: ArgumentError) do
        useError(error);
end case;

Standard.Sftp

SFTP version 3 over the pipes of a child process.

case startSession(command, 30000) of
    when Some(value as opened: Session) do
        var session: Session := opened;
        let content: Either[SftpError, String] := readFile(&!session, "/srv/data/report.csv");
        let status: ProcessStatus := endSession(session);
        store(content);
    when None do
        reportNoServer();
end case;

Standard.Shared

State that tasks share: a mutex that guards a value, and an atomic word of 64 bits.

let { value as count: Int64, key: Key } := acquire(counter);
release(counter, count + 1, key);
let total: Int64 := atomicAdd(requests, 1);

Standard.SharedCache

A Standard.Cache that tasks share, with one fill per key.

case makeSharedCache(1000, 1048576, 60000000000) of
    when Some(value as cache: SharedCache[Nat64, Nat64]) do
        servePrices(cache);
    when None do
        reportNoMemory();
end case;

let price: Option[Nat64] := getWith(prices, item, nowNanos(), lookUpPrice);

Standard.Signal

Signals taken as events, a time limit for shutting down, and PID files.

let wanted: Wanted := Wanted(hangup => true, interrupt => true, terminate => true,
                             user1 => false, user2 => false);
case watchSignals(wanted) of
    when Some(value as watch: Signals) do
        var signals: Signals := watch;
        while not shutdownRequested(&!signals) do
            let woken: Bool := waitSignal(&!signals, 1000);
        end while;
        let left: Nat32 := limitShutdown(10);
        let restored: Bool := stopWatching(signals);
    when None do
        reportNoWatch();
end case;

Standard.Signify

Keys and signatures in the files of OpenBSD's signify(1): Ed25519, base64, one comment line.

case generateKeys("demo") of
    when Some(value as keys: KeyPair) do
        let { publicKey: String, secretKey: String } := keys;
        case signMessage(asSpan(&secretKey), "text", "verify with demo.pub") of
            when Some(value as signature: String) do
                let good: Bool := verifyMessage(asSpan(&publicKey), "text", asSpan(&signature));

Standard.Smtp

Sending mail through a relay, by the dialogue of RFC 5321 over TLS, with plain messages of RFC 5322.

case makeRelay("mail.example.org", 587, StartTls(), "/etc/ssl/cert.pem", 30000) of
    when Some(value as relay: Relay) do
        let sent: Either[MailFailure, Unit] := sendMail(&relay, "app", asSpan(&password),
                                                        &envelope, asSpan(&message));
        reportMail(sent);
        destroyRelay(relay);
    when None do
        reportBadHost();
end case;

Standard.Sort

Sorting and searching a buffer whose elements have a total order of Standard.Order.TotalOrder.

let sorted: Buffer[String] := sort(names);
case binarySearch(&sorted, &wanted) of
    when Found(position: Index) do
        showAt(position);
    when Missing(insertAt: Index) do
        offerToAdd(insertAt);
end case;

Standard.Sperli

A job of ranks that send each other messages over TLS 1.3, with the semantics of message passing and none of its interface.

let started: Either[Int32, Comm] := init(job);
let sent: Int32 := send(&!comm, 1, 7, message);
let arrived: Int32 := barrier(&!comm);

Standard.SperliCkpt

The files and frame payloads of a Sperli checkpoint: rank files, signed COMMIT files and their place on disk.

let file: Option[String] := rankFile(job, 1, 0, 2, asSpan(&state));
let verdict: Int32 := checkCommit(asSpan(&commit), publicKey, job, 1, 2);

Standard.SperliCollective

The bytes of the collective frames of Sperli and the reduction of two arrays of numbers.

let payload: String := collectivePayload(bcastOperation(), bytesType(), noReduction(), resultPhase(), 0, 1, "data");
let verdict: Int32 := checkCollective(asSpan(&payload), bcastOperation(), bytesType(), noReduction(), resultPhase(), 0, 1);

Standard.SperliError

The codes with which a Sperli job refuses a peer, a frame or a token, and their words.

let why: Span[Nat8, Static] := describe(badToken());

Standard.SperliExport

The calls of Standard.Sperli in the shape a C library can export: one session that holds the comm and the last result, and codes instead of Either.

let session: Session := openSession(text);
let sent: Int32 := sessionSend(&!session, 1, 7, message);

Standard.SperliLaunch

The launcher of a Sperli job: reads the host list, makes the keys and certificates of the job, and starts the ranks.

let hosts: Either[Int32, HostList] := parseHostList(text, "");

Standard.SperliWire

The bytes of Sperli, the cluster layer: frame headers, hello payloads and join tokens.

let header: String := frameHeader(dataKind(), 5, job, 1, 0, 0, 1, 7);
let verdict: Int32 := checkHeader(asSpan(&header), job, 1, 1, 0);

Standard.SqlCipher

SQLCipher through the system's libsqlcipher: Standard.Sqlite with the database file encrypted.

case openWriter("app.db", makeKey(secret)) of
    when Right(right as db: Connection[Writing]) do
        closeDatabase(db);
    when Left(left as error: SqlError) do
        printLn(describe(error));
end case;

Standard.Sqlite

SQLite through the system's libsqlite3, with every query checked against the schema at compile time.

@query(&!db, "SELECT id, name FROM users WHERE age > ?", age)
    for row: User[R] do
        printLn(row.name);
    else error do
        printLn(describe(error));
    end for;

Standard.SqliteReplica

SQLite replicated through Standard.Raft: every write is an entry of the log, applied by every node in the same order.

case proposeWrite(&!node, &store, "INSERT INTO kv (k, v) VALUES (?, ?)", &values) of
    when Right(right as index: Nat64) do
        skip;
    when Left(left as refusal: Nat8) do
        skip;
end case;

Standard.SqliteUsers

A store for Standard.Users in an SQLite database of Standard.Sqlite.

case openSqliteUsers(db) of
    when Right(right as opened: SqliteUsers) do
        var users: SqliteUsers := opened;
        let added: Either[UserError, Bool] := addUser(&!users, "alice", asSpan(&password));
        closeDatabase(closeSqliteUsers(users));
    when Left(left as failed: SqliteUsersFailed) do
        let { db: Connection[Writing], error: UserError } := failed;
        closeDatabase(db);
end case;

Standard.Ssh

Commands run on another host by the ssh client of OpenSSH, and any child run within a time and size.

case sshCommand("/usr/bin/ssh", "backup.example.org", "deploy", 22, 10) of
    when Right(right as base: Command) do
        let command: Command := addRemoteWord(addRemoteWord(base, "df"), "-h");
        case runCommand(command, 30000, 65536) of
            when Right(right as result: CommandResult) do
                showResult(result);
            when Left(left as error: SshError) do
                reportFailure(error);
        end case;
    when Left(left as error: SshError) do
        reportFailure(error);
end case;

Standard.String

The String type, a linear byte string on the heap that owns its bytes.

var line: String := fromLiteral("hello, world");
storeNth(&!line, 0, 72);
let head: String := fromSpan(getSpan(&line, 0, 4));
let size: Index := length(&line);
destroyString(head);
destroyString(line);

Standard.StringBuilder

A builder that collects bytes at its end and hands them over as one String.

var builder: StringBuilder := makeStringBuilder();
writeString(&!builder, "id=");
writeByte(&!builder, 52);
let line: String := finalize(builder);

Standard.Task

Structured concurrency: tasks that belong to a scope, and channels with two linear ends.

var scope: Scope := opened;
case spawn(&!scope, work, 21) of
    when Right(right as task: Task[Int32]) do
        printLn(join(task));
    when Left(left as unused: Int32) do
        printLn(-1);
end case;
closeScope(scope);

Standard.TaskArena

A task that is handed an arena of its own, which ends with the task.

case spawnWithArena(&!scope, work, request, 65536) of
    when Right(right as task: Task[Reply]) do
        answer(join(task));
    when Left(left as unused: Request) do
        refuse(unused);
end case;

Standard.Template

Jinja2 templates, checked when the programme is compiled, and what their generated code calls.

var out: StringBuilder := makeStringBuilder();
@template("page.jinja", page, out);
return finalize(out);

Standard.Testing

Assertions for tests run by hilde test.

assertTrue(isLeapYear(2024), "2024 is a leap year");
assertFalse(isLeapYear(1900), "1900, divided by 100 but not by 400, is not");

Standard.Text

What one does with text: parse it, encode it, compare it and take it apart.

let port: Option[Nat64] := parseNat(trim(asSpan(&field)));
let parts: Buffer[Span[Nat8, Static]] := split("a,b,c", ",");

Standard.Time

A wall clock that says what time it is, and a monotonic clock that says how much time has passed.

let stamp: Nat64 := wallNanos();
case monotonicNanos() of
    when Some(value as start: Nat64) do
        work();
        report(start);
    when None do
        work();
end case;

Standard.Tls

A TLS client and server, through libtls on OpenBSD and libretls on Debian.

let made: Either[String, Client] := connect("example.org", "443", "/etc/ssl/cert.pem");
let sent: Either[String, Unit] := send(&!client, asSpan(&request));

Standard.Toml

TOML as version 1.0.0 of its specification defines it, read strictly and then asked by path.

case readToml(asSpan(&text)) of
    when Right(right as parsed: Toml) do
        let port: Option[Int64] := integerAt(&parsed, "servers[1].port");
        destroyToml(parsed);
    when Left(left as error: TomlError) do
        report(error.line, error.column);
end case;

Standard.Tuples

Records of two to six values of any types, with fields named by their position.

let old: Pair[String, Nat64] := Pair(first => word, second => seen);
let { first: String, second: Nat64 } := old;

Standard.Unicode

Upper and lower case of UTF-8 text, and comparison without regard to case.

let shout: Option[String] := toUpper("Gruesse aus Koeln");
let same: Bool := equalIgnoringCase("STRASSE", asSpan(&street));

Standard.UnicodeProperties

Properties of code points from the Unicode Character Database, version 17.0.0.

let category: Span[Nat8, Static] := generalCategory(65);
var ranges: Buffer[Index] := allocateEmpty();
let known: Bool := appendProperty("Greek", &!ranges);

Standard.Users

User accounts with Argon2id passwords, locks and a limit on failed attempts, over a store the programme chooses.

case verify(&!users, "alice", asSpan(&typed), asSpan(&address), limits, now) of
    when Right(right as verdict: Verdict) do
        answer(verdict);
    when Left(left as error: UserError) do
        reportFailure(error);
end case;

Standard.Utf8

UTF-8: decoding it, validating it and building it.

case makeCodePoint(233) of
    when Some(value as point: CodePoint) do
        appendCodePoint(&!builder, point);
    when None do
        skip;
end case;
let count: Option[Index] := countCodePoints(asSpan(&text));

Standard.Vault

Encrypted secrets in a .env file, readable only with the key in that file and a pepper in a file of its own.

case openVault("/etc/app/secret/.app.env", "/var/lib/app/.app.pepper", "VAULT_KEY") of
    when Right(right as opened: Vault) do
        var vault: Vault := opened;
        let stored: Either[VaultError, Unit] := setSecret(&!vault, "DB_PASSWORD", "s3cret");
        closeVault(vault);
    when Left(left as error: VaultError) do
        skip;
end case;

Standard.Watch

Watching files and directories for changes: inotify on Linux, kqueue on OpenBSD and FreeBSD.

var watcher: Watcher := made;
let config: Option[Index] := watchFile(&!watcher, "/etc/app.conf");
case waitForChange(&!watcher, 5000) of
    when Changed(watch as changed: Index) do
        reload();
    when WaitedOut do
        skip;
    when WatchFailed do
        skip;
end case;
destroyWatcher(watcher);

Standard.X509

Keys and X.509 certificates: made, written, read, signed and verified.

let key: Option[PrivateKey] := generateKey(EcP256());
let made: Option[Certificate] := selfSigned(&signer, "web", "example.org", 90, false);

Standard.Xml

XML 1.0 read into tokens, without a document type, and text escaped for it.

case parseXml(asSpan(&text)) of
    when Right(right as parsed: XmlDocument) do
        let feed: Option[Index] := xmlFindStart(&parsed, 0, "feed");
        destroyXmlDocument(parsed);
    when Left(left as error: XmlError) do
        report(error.offset);
end case;

Standard.Yaml

The part of YAML that configuration files use, read into the values of Standard.Json.

case readYaml(asSpan(&text)) of
    when Right(right as config: Json) do
        apply(config);
    when Left(left as error: YamlError) do
        report(error.line);
end case;