The filesystem

Status: settled, and built. Shorter than strings.md because most of it is an application of decisions already made: Fs(prefix) narrows by §7.4’s prefix extension exactly as Ffi(library) does, and the file operations reach libc the way putchar and the arena already do. Two things here are genuinely new, and §2 and §4 are those two.

This is the last mile to M3’s acceptance criterion (#1): a real CLI tool doing file IO and parsing.

1. Fs(prefix) is a capability carrying a path

linearity-and-effects.md §8.1 listed it, and §7.4’s worked example is literally this one:

let logs = narrow(fs, "/var/log/app");   // Fs("/var") -> Fs("/var/log/app")

So it is the machinery Ffi already uses, pointed at a different kind of name. split hands out Fs("") — the unnarrowed root, authority over nothing until it names somewhere — and narrowing is prefix extension, one way only. A program cannot grant itself what it was not given.

The effect labels carry the prefix too: fs_read("/var/log") and fs_write("/tmp"). A function’s row therefore says which part of the filesystem it can touch, and a caller reads that without opening the body.

1.1 A path prefix is not a byte prefix

One place Fs is not the same as Ffi, found while building it and worth stating rather than leaving implicit.

libc is a byte prefix of libcrypto, and that is the right answer for a library name: attenuation there is textual because a library name has no structure. A path does have structure. /tmp is a byte prefix of /tmpevil, and /tmpevil is not in /tmp — it is the directory next door, and a purely textual check would hand it over.

A path prefix extends at a /, or not at all. target is inside prefix when it starts with those bytes and either is exactly the prefix, or continues from it at a separator.

Exactly the prefix is allowed on purpose: Fs("/tmp/app.log") naming one file is an ordinary and useful point in the lattice, and a rule that refused it would make single-file authority unexpressible.

The empty prefix contains everything, which is what makes the capability split hands out the root rather than a special case. The rule is checked twice, because the two halves are known at different times: narrow checks it at compile time against the literal, and the operations check it at run time against the path (§4).

The effect row uses the same rule. Owning an Fs("/tmp") discharges fs_read/fs_write labels inside /tmp, and Label::covers decides that with extends_path, the function narrow calls: /tmp covers /tmp, /tmp/x and /tmp/x/y, a trailing slash (/tmp/) covers what is beneath it and not /tmp itself, the empty path covers every path, and /tmpevil is covered by none of them. Exec’s exec(p) label follows the same rule (processes.md §4.1). . and .. are not interpreted: the label is its literal’s text, as for narrow, and .. is refused when a path reaches an operation (§4). Until the correcting change covers compared these by byte prefix, so a function owning Fs("/tmp") could declare [] for a body that read /tmpevil: an inexact row (narrowing-into-several.md §6; no accepted program relied on it). net_out/net_in keep a plain text prefix on their "host:port" bound, as narrow does for a Net (net.md §4).

More than one path. narrow(fs, "a", "b", ...) spends the Fs and answers a tuple, one Fs per literal, each checked as above and against each other (no two equal, none inside another). A program that holds /dev/urandom and a certificate directory at once reports fs_read("/dev/urandom") and fs_read("/etc/cancho/tls_echo"), and not fs_read(""). Each operation is still checked at run time against the prefix of the capability it borrowed, so a read of one child’s file through the other traps (narrowing-into-several.md, built in PR #364, conformance/narrow_many.rs).

2. Why the operations are builtins and not extern fn

This is the first of the two new decisions, and it is the one that decides whether Fs means anything at all.

File operations reach libc from the backend, the way putchar, malloc and free already do. They are not extern fn declarations.

If they were, they would be gated by Ffi("libc") — and then holding the FFI capability would let a program open any path, with Fs contributing nothing. The authority that guards the filesystem has to be the one that names the filesystem.

2.1 What Fs does not do

Fs is not a sandbox, and this document will not pretend otherwise.

A program that narrows its Ffi to "libc" can declare extern fn open(...) and reach any path it likes. Nothing in the type system stops that, because §8.4 deliberately makes C reachable and C has the whole filesystem in it.

What the design actually claims is narrower and still worth having:

• a program’s authority is visible in its types. Reaching the filesystem through the language costs an Fs narrowed to a prefix; reaching it around the language costs an Ffi("libc") and an extern declaration, and both are in the signature of every frame that carries them;
• main chooses. It is handed one World, and what it narrows and what it releases is the whole story — a main that releases its ffi and narrows its fs to /tmp has given the rest of the program exactly that, and the rest of the program cannot widen it.

Containment against a hostile program is a sandbox’s job — lex-os runs one, and this language is what runs inside it. Containment against an honest program’s mistakes is what types do, and that is what this is.

2.2 And they do not call open

A note from building it, because it cost a CI cycle and the reason is not obvious.

open is variadic — int open(const char *, int, ...) — and on Apple ARM64 a variadic argument is passed on the stack while a fixed one is passed in a register. Declaring it with three fixed arguments therefore put the mode somewhere the callee never looked: the write succeeded and returned the right byte count, and the file was created with whatever happened to be on the stack, usually unreadable. Linux x86-64 cannot show this, because there varargs and fixed arguments share the same registers — so it passed locally and failed on the other CI target, which is what the second target is for.

So the backend calls two non-variadic functions instead:

• creat(path, mode) to write, which is exactly open(path, O_WRONLY|O_CREAT|O_TRUNC, mode) — and which also deletes the platform-dependent flag constants, the other thing here a portable language should not be guessing at;
• open(path, O_RDONLY) to read, declared with two arguments. That is the non-variadic prefix, so no argument lands anywhere the callee is not looking, and O_RDONLY is zero on both platforms.

The rule this generalises to: the backend does not call variadic C functions, because their ABI differs from the fixed one and Cranelift signatures do not express the difference. A conformance test checks the mode of a file a program wrote, from outside the program, rather than inferring it from a read that happens to succeed.

Corrected (processes.md §4.5). The rule was overtaken twice, and both opens have changed. fcntl and then openat (directory-handles.md) needed variadic calls, and the backends learned to make them correctly: LLVM declares the callee variadic, and Cranelift shapes the call on Apple ARM64 the way the callee reads it, with the variadic argument in the first stack slot. Then every descriptor a builtin opens had to be close-on-exec, which creat cannot ask for. So both opens are now openat(AT_FDCWD, path, flags, mode) with O_CLOEXEC: O_WRONLY|O_CREAT|O_TRUNC and 0644 to write, O_RDONLY to read. The per-target flag values live once, in cancho_ir::open_flags. The mode test above still holds, and still checks the variadic mode from outside the program.

3. Two operations, whole-file

fs_read(fs: &f Fs(p), path: &a [byte], into: &!b [byte]) -> [fs_read(p)] int
fs_write(fs: &f Fs(p), path: &a [byte], bytes: &c [byte]) -> [fs_write(p)] int

The capability is borrowed shared, like Ffi and unlike Io: holding it is a key, not a conversation, and two frames holding the same key at once changes nothing about what either may open. into is unique because fs_read writes through it; bytes and path are shared because nothing here writes through them.

fs_read fills as much of into as the file has and returns the byte count; fs_write writes the whole slice and returns what it wrote. Both return -1 on failure rather than trapping: a missing file is an ordinary outcome a program should handle, not a bug in the program.

No handles, no streaming, no seek. A file handle is a linear resource — it is precisely the thing this language exists to track — and giving it a type means deciding what close consumes, what a half-read file is, and what happens to a handle at the end of a region. That is a milestone, not a paragraph, and whole-file operations are what M3 needs to read its own source and write its own output.

Built (#66), and the milestone was smaller than this paragraph says — file-handles.md. Two of the three questions were already answered by machinery that existed: close consumes the handle because that is what res means, and a handle at the end of a region is a compile error because a linear value that nothing consumes already is. Only the third — what a half-read file is — needed a decision, and the answer is a three-constructor Read rather than a fourth meaning for -1.

fs_read and fs_write are unchanged and stay the right call for a file whose size is known. What the handle adds is the case that could not be written correctly at all: reading a file whose size you do not know.

4. The path is checked at runtime, and .. is refused

The second new decision, and the one with the sharp edge.

The prefix lives in the type and is therefore known at compile time. The path is a runtime slice — it has to be, or a program could not open a file named on its command line. So:

The operation emits a check that the path starts with the capability’s prefix, and traps if it does not.

A trap rather than -1, because a path outside the granted prefix is not a missing file: it is a program doing something its type said it would not. That is the same distinction defined-behaviour.md draws everywhere — -1 for an outcome, a trap for a broken promise.

Corrected: the check was undefined behaviour in the LLVM backend. Both backends compared byte i of the path with byte i of the prefix for every i in the path, reading the prefix’s data past its end once the path was longer. Cranelift read whatever lay next to it, which was harmless by luck. LLVM folds a load past the end of a global to poison, and the mask that was meant to discard it does not: false && poison is still poison, and a branch on it is undefined behaviour. At -O2, where the check’s loop is unrolled for a short path, the optimiser therefore deleted every path through the call: fs_read("/tmp/q/f") on Fs("/tmp") trapped with SIGILL (measured: paths of 11 bytes and fewer, not 15 and more). connect’s host check had the same shape and answered garbage (48 for a connect that should have been refused). The prefix’s byte is now read at i only while i is inside it, and an empty prefix is not read at all; a_short_path_under_a_narrowed_prefix_is_read_on_both_backends and a_host_inside_a_shorter_bound_is_dialled_on_both_backends pin both.

4.1 .. is refused rather than normalised

A prefix check on bytes is defeated by /tmp/../etc/passwd. There are two honest responses and one dishonest one:

• normalise the path before checking — which is a security function with a long history of being got wrong, and would need its own design, its own fixtures and a decision about symlinks;
• refuse any path containing .. — a trap, like the prefix check;
• pretend the prefix check is sufficient, which is the dishonest one.

M3 takes the second. It is a real restriction and it is stated rather than hidden: a program that needs .. is a program that needs path normalisation, and path normalisation arrives with a design document of its own.

5. What this unblocks

M3’s acceptance criterion. examples/lines.cho writes a log, reads it back off disk, counts and filters it, writes a report, and reads the report back to print it — four file operations, one capability narrowed once in main, and a row on every frame that carries it. The bytes come from disk; everything done to them is the slice machinery wordcount.cho already used.

There are no command-line arguments yet (§6), so the tool lays down its own input rather than being handed a path. That is the one place the example is a demonstration rather than a tool, and it is a missing runtime feature rather than a missing language one.

6. Open

7. The must-reject suite

And the accepting counterparts:

Plus four conformance tests, because these are runtime rules and a fixture that only compiles would not reach them: