rocq/glibc/ZsysWrite.v
A contract at libpizlo's boundary: zsys_write, the pizlonated write(2) that user glibc's write calls (docs/zsys.md, docs/glibc-ir.md). The contract zsys_write_contract is trusted; its native counterexample probe is rocq/glibc/zsys-write.c.
At the pin, libpizlo's filc_native_zsys_write(fd, buf, size) (libpas/src/libpas/filc_runtime.c) is three steps:
check_fd(fd): a Fil-C assertion that fd is not libpizlo's own log descriptor, which exists only when libpizlo logs to a file;filc_check_read(buf, size): the capability check, a Fil-C panic when buf cannot be read for size bytes;FILC_SYSCALL(write(fd, ptr, size)): leave the Fil-C world, make the system call, come back, and on failure hand errno tofilc_set_errno, which calls user glibc's errno handler, Fil-C code that stores the number in the thread's errno.
The contract's world, fd_world, keeps what no Fil-C code of the module owns: where that errno store lands and which descriptor is libpizlo's log. The errno handler is not proved here; the contract names its effect, a store into the 4-byte errno_span, as the call's only writable root, so every other byte of memory is kept by the machine's effects rule.
The world is trusted to be the real one: errno_ptr is the calling thread's user glibc errno (thread_local int errno, csu/errno.c), already allocated (Fil-C allocates a thread-local on first use, and the contract allows no allocation); glibc's errno_handler is registered (__libc_start_main does it; filc_set_errno panics without one); FILC_DUMP_ERRNOS is unset, so a failure logs nothing; and log_fd is libpizlo's log descriptor. The observation reuses ExternalCalls.v's StreamBytes event, read at this layer as bytes the kernel accepted for the descriptor, not bytes stdio buffered.
Over a Logic instance, fd_wi interprets the world: the errno cell writable and apart from every object the program owns, and the program's descriptors not the log's. wp_zsys_write is the contract's rule for a caller owning the buffer's pieces.
The world
What a descriptor call needs that no Fil-C code of the module owns: the thread's errno, where user glibc's errno handler stores a failure's number, and libpizlo's log descriptor, if it logs to a file.
The 4 bytes of the world's errno.
The k bytes of memory m from p's address.
The contract
zsys_write returns a long (class L), or its result is discarded, and takes an int, a pointer and a size_t.
The precondition: the buffer is readable for its n bytes through a live object's capability (readable_bytes, the check filc_check_read makes), fd is not libpizlo's log descriptor (the check check_fd makes), and errno is a live, writable, aligned int (errno_cell).
A finite prefix: nothing born, the world kept, errno still a writable int, and either nothing observed or the first k bytes of the buffer, k at most n, accepted for fd.
The postcondition: as the prefix, and either the kernel accepted the first k bytes, k at most n and below 2^31 (Linux writes at most MAX_RW_COUNT at once), and the call returns k; or it accepted none and the call returns -1, 2^64 - 1 as a long's bits. Only a failure stores errno (FILC_SYSCALL calls the handler only on a nonzero native errno); the contract allows the store either way.
The capability checks a call outside the precondition reaches: the buffer's null or out-of-bounds capability, and argument or return size mismatch. A log descriptor fails libpizlo's own assertion, which is no capability reason.
The trusted contract of zsys_write: a long, zsys_write_abi, zsys_write_pre, no capability sources (it returns an integer), errno's 4 bytes as its one writable root, no releases, no allocation, zsys_write_prefix, zsys_write_post, no resource ending, and zsys_write_panic.
Boundary checks
A call that returns anything but -1 accepted exactly that many of the buffer's first bytes for fd.
Proof 6 steps Qed
A failed call observed nothing.
Proof 4 steps Qed
Over a Logic instance
The world interpretation, the rule and its lemmas over the runtime R and the Logic instance LG.
The world interpretation of a program that writes to the descriptors fds: errno is a writable int apart from every live object owning a piece of h, and no descriptor of fds is libpizlo's log.
A safepoint keeps fd_wi: no region changes (collector_live), and writability and apartness read only regions.
Proof 20 steps Qed
A zsys_write call that returns returns one long: a count no more than its size, or -1.
Proof 5 steps Qed
After a zsys_write call that returns, from a state interpreted with the ghost heap h, the state is interpreted with h again: the prefix keeps the runtime ready, the frame keeps h agreeing and live objects apart, since the one writable root, errno, is apart from h, and the world and errno's writability are kept.
Proof 10 steps Qed
The Iris instance of the registry and fd_wi.
The expressions of the language.
zsys_write's triple, from zsys_write_contract: a call whose arguments read as fd, one of fds, the pointer p and the size n, owning pieces ps that show p readable for n bytes, binds d to a count no more than n, or -1, and the pieces are still owned.