core.sys — V-LLSI kernel bootstrap

partial

A subset of the API has conformance coverage. Consult the documented backend and API limitations.

sys is the lowest-level OS interface used by higher-level modules such as io, net, async and mem.

V-LLSI = Verum Low-Level System Interface. Its generated AOT runtime boundaries are:

• Linux: direct syscall instructions via syscall6.
• macOS: Apple's stable ABI via libSystem.B.dylib (Mach + Darwin).
• Windows: kernel32.dll + ntdll.dll.
• Embedded / no_runtime: stack allocator, no syscalls, stubs for async.

These are requirements for generated code, not a claim that every current AOT path conforms. The host interpreter may use libc/system libraries, subject to CLI portability and consistent API semantics. See the AOT no-libc status and host compatibility boundary.

Most user code never imports sys directly. This page is for runtime authors, driver writers, and kernel engineers.

Area	Files
Common types	common.vr
Raw syscall bindings	core/intrinsics/runtime/os.vr (post-migration canonical home; core/sys/raw.vr no longer exists).
Wrapped operations	file_ops.vr, time_ops.vr, net_ops.vr, process_ops.vr, context_ops.vr (each mounts the raw intrinsics from core.intrinsics.runtime.os.{...}).
I/O abstraction	io_engine.vr
Initialization	init.vr
Signals	signal.vr
Hardware control	bitfield.vr, mmio.vr, interrupt.vr
Byte-range file locking	locking/mod.vr (LockHandle affine RAII)
Crash-safe persistence	durability.vr (full_fsync, sync_directory)
Alternative runtimes	embedded.vr, no_runtime.vr
Linux (@cfg(target_os="linux"))	syscall.vr, arch.vr, errno.vr, auxv.vr, io.vr, mem.vr, thread.vr, time.vr, tls.vr, bpf/ (eBPF map+program loader). Supports both x86_64 and aarch64 — architecture-specific syscall numbers live in arch.vr and are re-exported by syscall.vr; x86_64-only legacy syscalls (open, stat, mkdir, …) are gated behind @cfg(target_arch="x86_64"), with the portable *at variants (openat, newfstatat, mkdirat, …) available on both.
macOS (@cfg(target_os="macos"))	libsystem.vr, mach.vr, io.vr, errno.vr, thread.vr, time.vr, tls.vr
Windows (@cfg(target_os="windows"))	kernel32.vr, ntdll.vr, io.vr, errno.vr, thread.vr, time.vr, tls.vr, ntstatus.vr, winsock2.vr

---

Platform coverage

core.sys is the lowest layer in the library: thin wrappers over the operating system, gated per platform. What is available to you depends on which platform you build for, and the gap between platforms is wide enough to plan around.

Coverage is specific to the module and target

The table below summarizes recorded module audits; it is not a fresh cross-platform revalidation. Read each row alongside its module page and linked audit. A passing interpreter suite does not establish native or Windows support. In particular:

• There is no Windows file layer. Not a partial one. The two modules that would carry it mount, on Windows, a total of two functions — checked, and the whole finding fits on a screen:

  for f in core/io/file.vr core/io/fs.vr; do
      awk '/@cfg\(target_os = "windows"\)/{p=1} p{print} p&&/};/{exit}' "$f"
  done

  (The loop is not decoration. Handing both files to one awk prints only the first: exit ends the program, not the file.)

  file.vr brings in safe_close and ten constants; fs.vr brings in GetFileAttributesW and nothing else. Run the same command with "linux" and the two files answer with ten and eighteen functions — open, read, write, lseek, fstat, mkdir, unlink, rename and the rest. Anything on this page describing Windows file behaviour describes an intention. See also the file I/O page.

• Several core.sys surfaces are reachable only through the interpreter; the ahead-of-time path for programmes that mount a standard-library submodule is a separate question this page does not answer.

Common types

type OSError is { code: Int, message: Text };
type FileDesc is (Int);                // type-safe file descriptor wrapper
type IOVec is { base: &unsafe Byte, len: Int };
type PageSize is Int;

type MemProt is bitflags {
    None   = 0x0,
    Read   = 0x1,
    Write  = 0x2,
    Exec   = 0x4
};

type MapFlags is bitflags {
    Shared  = 0x01,
    Private = 0x02,
    Anon    = 0x20,
    Fixed   = 0x10,
    Stack   = 0x20000,
    HugeTlb = 0x40000
};

type MemoryOrdering is Relaxed | Acquire | Release | AcqRel | SeqCst;

Constants

const PAGE_SIZE: Int = 4096;                 // or 16384 on aarch64
const PAGE_SHIFT: Int = 12;
const MAX_CONTEXT_SLOTS: Int = 32;
const CONTEXT_STACK_DEPTH: Int = 256;

---

Cross-platform file & random helpers — sys.common

Platform-agnostic syscall wrappers that dispatch to sys.linux / sys.darwin / sys.windows under a single signature. These are the shape that pure-Verum stdlib modules (core.database.sqlite, core.security.aead, core.io.file) actually call.

// File I/O — all positional, do not perturb fd offset
fn pread(fd: FileDesc, buf: &mut [Byte], offset: Int) -> Result<Int, OSError>
fn pwrite(fd: FileDesc, buf: &[Byte], offset: Int) -> Result<Int, OSError>

// File metadata
fn file_size(fd: FileDesc) -> Result<Int, OSError>
fn truncate(fd: FileDesc, length: Int) -> Result<(), OSError>
fn access(path: &[Byte], mode: Int) -> Result<Bool, OSError>   // F_OK / R_OK / W_OK / X_OK

// Durability
fn full_fsync(fd: FileDesc) -> Result<(), OSError>            // F_FULLFSYNC on macOS, fdatasync on Linux
fn sync_directory(path: &[Byte]) -> Result<(), OSError>

// Byte-range advisory file locks (POSIX fcntl / Win LockFileEx)
fn try_lock_region(fd: FileDesc, kind: FcntlLockKind, start: Int, len: Int) -> Result<(), OSError>
fn unlock_region(fd: FileDesc, start: Int, len: Int) -> Result<(), OSError>

// Cryptographic randomness — getrandom / SecRandomCopyBytes / BCryptGenRandom
fn random_bytes(buf: &mut [Byte]) -> Result<(), OSError>

All wrappers carry IntrinsicHint.RequiresPermission; capability checking is the caller's responsibility (typically via sys.permissions). Errors are typed OSError with raw errno plus localised message.

Page alignment

fn page_align_up(x: Int) -> Int
fn page_align_down(x: Int) -> Int
fn is_page_aligned(x: Int) -> Bool

---

OS memory

Direct mmap / VirtualAlloc (bypassing CBGR):

unsafe fn os_alloc(size: Int) -> Int                           // returns virtual addr
unsafe fn os_free(addr: Int, size: Int)
unsafe fn os_alloc_aligned(size: Int, align: Int) -> Int
unsafe fn os_alloc_huge(size: Int, huge_page_size: Int) -> Int
unsafe fn os_protect(addr: Int, size: Int, prot: MemProt)
unsafe fn os_advise(addr: Int, size: Int, advice: MemAdvice)   // madvise

type MemAdvice is
    | Normal | Random | Sequential
    | WillNeed | DontNeed
    | Free | Remove | DontFork
    | HugePage | NoHugePage;

These back the segment allocator in mem.

---

Threads

fn get_thread_id() -> Int                          // OS-native TID
fn thread_self() -> ThreadHandle
fn thread_yield()                                   // sched_yield / Sleep(0)
fn thread_spawn(entry: fn(*mut Byte), arg: *mut Byte, stack_size: Int) -> Result<ThreadHandle, OSError>
fn thread_join(handle: ThreadHandle) -> Result<(), OSError>
fn thread_detach(handle: ThreadHandle) -> Result<(), OSError>
fn num_online_cpus() -> Int

TLS (thread-local storage)

unsafe fn tls_get_base() -> *mut Byte              // TCB base
unsafe fn tls_slot_get(slot: Int) -> Maybe<Int>
unsafe fn tls_slot_set(slot: Int, value: Int)
unsafe fn tls_slot_clear(slot: Int)
unsafe fn tls_slot_has(slot: Int) -> Bool

unsafe fn tls_frame_push() -> Result<(), ContextError>
unsafe fn tls_frame_pop() -> Result<(), ContextError>

unsafe fn tls_read_ptr<T>(slot: Int) -> *const T
unsafe fn tls_write_ptr<T>(slot: Int, value: *const T)
unsafe fn tls_read_i32(slot: Int) -> Int32
unsafe fn tls_write_i32(slot: Int, value: Int32)
unsafe fn tls_read_usize(slot: Int) -> USize
unsafe fn tls_write_usize(slot: Int, value: USize)

---

Context system (V-LLSI storage)

The dynamic using / provide system stores its stack in TLS slots.

type ContextError is
    | StackOverflow
    | StackUnderflow
    | SlotOccupied
    | SlotEmpty
    | InvalidSlot;

fn ctx_get(slot: Int) -> Maybe<Int>;
fn ctx_get_mut(slot: Int) -> Maybe<&mut Int>;
fn ctx_set(slot: Int, value: Int);
fn ctx_has(slot: Int) -> Bool;
fn ctx_clear(slot: Int);
fn ctx_push_frame() -> Result<(), ContextError>;
fn ctx_pop_frame() -> Result<(), ContextError>;

User code interacts with this via provide / using — see Language → context system.

core.sys.context_ops — raw V-LLSI TLS + DI surface

The thin wrappers in core.sys.context_ops sit one layer below the typed ctx_* API above. They take a raw Int-keyed slot or type_id and pass it straight through to the underlying interpreter / AOT intrinsic. Use this surface only from runtime-implementation code; user code should reach for the typed ctx_* family instead.

public let TLS_SLOT_COUNT: Int = 256;                  // V-LLSI per-thread arena ceiling

public fn tls_get(slot: Int) -> Int                    // read TLS slot
public fn tls_set(slot: Int, value: Int)               // write TLS slot

public fn context_provide(type_id: Int, value: Int)    // push DI value
public fn context_get(type_id: Int) -> Int             // most-recent provide for type_id
public fn context_end(type_id: Int)                    // pop the most-recent provide

public fn defer_register(cleanup_fn: fn(Int) -> Int, arg: Int)
public fn defer_execute()                              // pop top (Tier-1 invokes callback)
public fn defer_depth() -> Int
public fn defer_run_to(depth: Int)                     // truncate stack to depth

Tier-0 vs Tier-1 contract

Operation	Tier 0 (interpreter)	Tier 1 (AOT)
tls_set / tls_get	round-trip via state.context_stack	round-trip via per-thread TCB
context_provide / context_get / context_end	round-trip via state.context_stack	round-trip via per-thread TCB
defer_register / defer_run_to / defer_depth	maintains (fn_id, arg) stack — depth tracking accurate	maintains stack + cleanup-callback dispatch
defer_execute (callback invocation)	not invoked — interpreter cannot synthesise indirect fn(Int) -> Int dispatch	invoked via call-frame machinery

The interpreter wiring closed in this branch — pre-fix every raw intrinsic above returned constant 0/nil, leaving the V-LLSI context arena entirely inert under Tier 0. See core-tests/sys/context_ops/audit.md for the conformance report.

---

Value types — sys.io_engine

Refinement-typed value types used by the I/O engine protocol below.

public type Port is UInt16;
public type BoundPort is Port where |p| p > 0;

public type EngineDuration is (UInt64);           // always non-negative
public type NonZeroDuration is EngineDuration where |d| d.0 > 0;

public type TimeSpec is { tv_sec: Int64, tv_nsec: Int64 };

public type Fd is (Int32);
public type ValidFd is Fd where |fd| fd.0 >= 0;

EngineDuration constructors and accessors

Constructor	Returns
EngineDuration.from_nanos(n: UInt64)	EngineDuration
EngineDuration.from_micros(n: UInt64)	n * 1_000 ns
EngineDuration.from_millis(n: UInt64)	n * 1_000_000 ns
EngineDuration.from_secs(n: UInt64)	n * 1_000_000_000 ns
EngineDuration.ZERO	0 ns
EngineDuration.MAX	UInt64.MAX ns (≈ 584 years)
MAX_PRACTICAL_DURATION	365 * 86400 * 1_000_000_000 (1 year cap)

Accessor	Returns
d.as_nanos()	d.0 (identity)
d.as_millis()	d.0 / 1_000_000
d.as_secs()	d.0 / 1_000_000_000
d.is_zero()	d.0 == 0
d.saturating_add(other)	caps at EngineDuration.MAX
d.saturating_sub(other)	floors at EngineDuration.ZERO
d.to_timespec()	POSIX timespec projection

Fd predicates

Method	Semantics
Fd.INVALID	sentinel Fd(-1)
f.as_raw()	Int32 accessor
f.is_valid()	f.0 >= 0
f.try_as_valid()	Maybe<ValidFd>
f.as_valid()	ValidFd (panics on invalid)

Standard descriptors

public const STDIN_FD: ValidFd = Fd(0) as ValidFd;
public const STDOUT_FD: ValidFd = Fd(1) as ValidFd;
public const STDERR_FD: ValidFd = Fd(2) as ValidFd;

---

I/O engine

type IOEngine is protocol {
    fn submit(&mut self, ops: &[(CompletionOp, UInt64)])
        -> Result<Int{>= 0}, EngineIoError>;
    fn submit_one(&mut self, op: CompletionOp, user_data: UInt64)
        -> Result<(), EngineIoError>;          // default impl over `submit`
    fn poll(&mut self, results: &mut [CompletionResult])
        -> Result<Int{>= 0}, EngineIoError>;   // default impl over `wait`
    fn wait(&mut self, results: &mut [CompletionResult],
            min_complete: UInt32, timeout: Maybe<EngineDuration>)
        -> Result<Int{>= 0}, EngineIoError>;
    fn wake(&self) -> Result<(), EngineIoError>;
    fn flush(&mut self) -> Result<(), EngineIoError>;
    fn shutdown(&mut self) -> Result<(), EngineIoError>;
}

type CompletionOp is
    | Read  { fd: ValidFd, buf: &mut [Byte], offset: Int64{>= 0} }
    | Write { fd: ValidFd, buf: &[Byte], offset: Int64{>= 0} }
    | ReadV { fd: ValidFd, iovecs: &[IOVec] }
    | WriteV { fd: ValidFd, iovecs: &[IOVec] }
    | Accept { fd: ValidFd, addr: &mut RawSocketAddr }
    | Connect { fd: ValidFd, addr: &RawSocketAddr }
    | Recv { fd: ValidFd, buf: &mut [Byte], flags: Int32 }
    | Send { fd: ValidFd, buf: &[Byte], flags: Int32 }
    | RecvMsg { fd: ValidFd, msg: &mut MsgHdr, flags: Int32 }
    | SendMsg { fd: ValidFd, msg: &MsgHdr, flags: Int32 }
    | Close { fd: Fd }              // Fd, not ValidFd — may be closed already
    | Timeout { ts: &TimeSpec }
    | Cancel { user_data: UInt64 }
    | Fsync { fd: ValidFd, datasync: Bool }
    | Poll { fd: ValidFd, events: UInt32 };

type CompletionResult is {
    user_data: UInt64,              // the caller's own token, echoed back
    result: Int32,                  // negative = errno
    flags: UInt32,
};

implement CompletionResult {
    pure fn success(user_data: UInt64, bytes: BytesTransferred) -> CompletionResult;
    pure fn error(user_data: UInt64, errno: ErrnoCode) -> CompletionResult;
    pure fn is_success(&self) -> Bool;
    pure fn is_error(&self) -> Bool;
}

type BytesTransferred is UInt32;
type ErrnoCode is Int32 { > 0 };    // refined: an errno is never <= 0

fn create_io_engine(sq_entries: UInt32) -> Result<some E: IOEngine, EngineIoError>;

There is no SubmissionId and no IoEngineConfig: a submission carries an opaque user_data: UInt64 that the completion echoes back, and the engine is created from a queue depth. IOEngine is a protocol, so create_io_engine returns an opaque some E: IOEngine rather than a Heap.

Platform picks:

• Linux: IoUringDriver (fallback: EpollDriver)
• macOS: KqueueDriver
• Windows: IocpDriver

---

Filesystem watcher — sys.fs_watch

Native, event-driven filesystem monitoring on top of the per-platform kernel facility:

Platform	Backend
macOS	kqueue EVFILT_VNODE
Linux	inotify (inotify_init1 + inotify_add_watch direct syscalls)
Windows	ReadDirectoryChangesW (overlapped + WaitForMultipleObjects)

Sub-millisecond latency, kernel-driven; no polling overhead.

public type FsEventKind is
    | Created
    | Modified
    | Deleted
    | Renamed
    | AttribChanged;

public type FsEvent is {
    path: Text,
    kind: FsEventKind,
}

@must_consume
public type FsWatcher is { inner: FsWatcherImpl };

implement FsWatcher {
    /// Open a fresh watcher. `Err` where the native backend is
    /// unavailable or could not be initialised.
    public fn new() -> Result<FsWatcher, Text>;

    /// Add a path to the watch set. The same path may be added more
    /// than once; events fire once per registration.
    public fn add(&mut self, path: &Text) -> Result<(), Text>;

    /// Remove a previously-added watch. Removing a path that was never
    /// added is `Ok`.
    public fn remove(&mut self, path: &Text) -> Result<(), Text>;

    /// Wait for the next event(s). An EMPTY LIST means the timeout
    /// elapsed, not an error. Timeout in milliseconds; `-1` blocks
    /// forever.
    public fn wait(&mut self, timeout_ms: Int) -> Result<List<FsEvent>, Text>;
}

There is no .watch(), no .recv() and no .recv_with_timeout() — the watch set is managed with add/remove and events are drained by wait, which returns a LIST because one kernel wake-up can carry several. A bounded wait is wait(ms); a blocking one is wait(-1).

Does not run yet on Tier 0

FsWatcher.new() panics under the interpreter before any filesystem activity is involved:

Panic: [lenient] stage-5 qualified cross-module fn stub never resolved

The types are fine — FsEventKind and FsEvent construct, match and round-trip — and so is the rest of the sys layer around it, which is what makes the failure easy to miss: reading and writing files through io.file works in the same programme. The signature above is what core/ declares, and it is what an AOT build compiles against; treat the runtime behaviour as unverified until this box goes away.

---

Byte-range file locks — sys.locking

High-level, typed wrapper around the per-platform fcntl / LockFileEx primitives in sys.common. The user-facing surface expresses the lifecycle through an affine LockHandle that consumes its receiver on .unlock() — releasing without explicit unlock is also safe (handled by Drop).

public type FileLockKind is Shared | Exclusive;

public type LockRegion is {
    start: Int,
    length: Int,    // -1 = "from start to EOF"
};

public type LockError is
    | Conflict(owner_pid: Maybe<Int>)
    | IoFailure(err: OSError);

The 5-state SQLite locking protocol (SHARED / RESERVED / PENDING / EXCLUSIVE) is built on top of these primitives in core.database.sqlite.native.l0_vfs.locking. Advisory-only on POSIX; mandatory on Windows; NFS not supported.

---

Crash-safe persistence — sys.durability

Intent-named re-export surface over the durability primitives in sys.common. Callers prefer mount core.sys.durability.{full_fsync, sync_directory} over reaching into the catch-all common namespace, so the intent is visible at the import site.

public mount core.sys.common.full_fsync;
public mount core.sys.common.data_only_fsync;
public mount core.sys.common.sync_directory;
public mount core.sys.common.pread;
public mount core.sys.common.pwrite;

Per-platform backends:

Platform	full_fsync	sync_directory
Linux	fsync(fd) direct syscall	fsync(dirfd)
macOS	fcntl(fd, F_FULLFSYNC) (stronger than fsync)	fsync(dirfd)
Windows	FlushFileBuffers(handle)	no-op (NTFS journals dir updates)

---

Initialization

fn verum_init(cfg: InitConfig) -> Result<(), InitError>;
fn verum_shutdown();
fn is_initialized() -> Bool;

fn init_thread() -> Result<(), InitError>;
fn cleanup_thread();

type InitError is
    | TlsFailed { reason: Text }
    | ContextFailed { reason: Text }
    | AllocatorFailed { reason: Text }
    | PanicHandlerFailed { reason: Text }
    | AlreadyInitialized
    | NotInitialized
    ;

implement InitError { fn message(&self) -> Text; }

// `SysInitPanicInfo`, and it carries the location as three plain
// fields rather than a `SourceLocation`. There is no thread id.
type SysInitPanicInfo is {
    public message: Text,
    public file:    Text,
    public line:    Int,
    public column:  Int,
};

fn panic_impl(message: Text, file: Text, line: Int, column: Int) -> !;
unsafe fn set_panic_handler(handler: fn(&SysInitPanicInfo));

The error arms name the subsystem that failed to come up, each with a reason — there is no InvalidConfig or PlatformError. The handler passed to set_panic_handler returns (), not !; panic_impl is the diverging one.

---

Time operations — sys.time_ops

core.sys.time_ops is the syscall-level layer that core.time sits on top of. Two record types and a small free-function surface route into three @intrinsic-decorated raw functions (__time_monotonic_nanos_raw, __time_sleep_nanos_raw, __time_now_ms_raw) whose runtime is implemented in crates/verum_vbc/src/interpreter/dispatch_table/handlers/calls.rs:1492-1514 (interpreter / Tier 0) and crates/verum_codegen/src/llvm/platform_ir.rs:15605-15732 (AOT / Tier 1).

type SysTimeOpsInstant is { nanos: Int };
type SysTimeOpsDuration is { nanos: Int };

SysTimeOpsInstant

Method	Returns	Semantics
SysTimeOpsInstant.now()	SysTimeOpsInstant	Monotonic clock read — non-negative, non-decreasing across sequential calls. POSIX clock_gettime(CLOCK_MONOTONIC) / equivalent.
t.elapsed()	SysTimeOpsDuration	now() - t.nanos, expressed as Duration.
t.duration_since(earlier)	SysTimeOpsDuration	t.nanos - earlier.nanos.

SysTimeOpsDuration

Constructor	Returns
SysTimeOpsDuration.from_nanos(n: Int)	SysTimeOpsDuration
SysTimeOpsDuration.from_micros(n: Int)	n * 1_000 ns
SysTimeOpsDuration.from_millis(n: Int)	n * 1_000_000 ns
SysTimeOpsDuration.from_secs(n: Int)	n * 1_000_000_000 ns
SysTimeOpsDuration.zero()	0 ns

Accessor	Returns
d.as_nanos()	d.nanos (identity)
d.as_micros()	d.nanos / 1_000 (integer truncation toward zero)
d.as_millis()	d.nanos / 1_000_000
d.as_secs()	d.nanos / 1_000_000_000

The accessor chain forms a refinement: d.as_secs() <= d.as_millis() / 1000 <= d.as_micros() / 1000 <= d.as_nanos() / 1000.

Free functions

public fn sleep(d: SysTimeOpsDuration)   // sleep for d.nanos
public fn sleep_ms(ms: Int)              // sleep for ms milliseconds
public fn sleep_secs(s: Int)             // sleep for s seconds
public fn wall_clock_ms() -> Int         // milliseconds since Unix epoch (wall clock)

Conformance & open defects

See the module-status table below for the current green-test count and the gating defects. Arithmetic API surface (SysTimeOpsDuration.from_* / as_* / zero) is stable in both interpreter and AOT. Every clock-touching API (SysTimeOpsInstant.now, sleep_*, wall_clock_ms) is currently gated by the intrinsic-mount propagation defect surfaced by this module's suite, audited in core-tests/sys/time_ops/audit.md.

---

File operations — sys.file_ops

Thin Verum-side shim over the canonical POSIX file syscalls. The OpenMode newtype packs the canonical O_* flag bit-patterns so callers don't have to import platform-specific constants directly.

public type OpenMode is { flags: Int };

implement OpenMode {
    public fn read() -> OpenMode        // O_RDONLY = 0
    public fn write() -> OpenMode       // O_WRONLY | O_CREAT | O_TRUNC = 0x301
    public fn read_write() -> OpenMode  // O_RDWR = 2
    public fn append() -> OpenMode      // O_WRONLY | O_CREAT | O_APPEND = 0x409
    public fn create() -> OpenMode      // O_WRONLY | O_CREAT | O_EXCL = 0x241
}

public fn read_file(path: Text) -> Maybe<Text>           // None on ENOENT
public fn write_file(path: Text, content: Text) -> Bool  // true on success
public fn append_file(path: Text, content: Text) -> Bool
public fn delete_file(path: Text) -> Bool                // false on missing
public fn file_exists(path: Text) -> Bool
public fn file_size(path: Text) -> Int                   // -1 sentinel

The error contract is intentionally lossy at this layer — the caller gets a Maybe or Bool and is expected to consult errno separately if structured error propagation is required. core.io.fs is the higher-level shape that funnels through Result<T, OSError>.

---

Process operations — sys.process_ops

public type ProcessExitStatus is { code: Int };
implement ProcessExitStatus {
    public fn success(&self) -> Bool   // code == 0
    public fn code(&self) -> Int
}

public type Child is { pid: Int, stdout_fd: Int, stderr_fd: Int };
implement Child {
    public fn wait(&self) -> ProcessExitStatus
    public fn read_stdout(&self) -> Text  // "" when stdout_fd < 0
}

public fn spawn(program: Text, args: List<Text>) -> Maybe<Child>
public fn run(program: Text, args: List<Text>) -> ProcessExitStatus
public fn args() -> List<Text>
public fn arg_count() -> Int
public fn arg_unchecked(index: Int) -> Text

The arg_unchecked(i) form is the canonical path for core.cli.*'s argv parser — user code should reach for core.base.env.arg(i) -> Maybe<Text> which performs the bounds check internally.

---

Raw TCP / UDP — sys.net_ops

FFI-only fallback socket types. The user-facing rich API lives in core.net.tcp / core.net.udp — RawTcpStream, RawTcpListener, RawUdpSocket here are the raw shapes user code should NOT reach for unless explicitly working around the IoEngine async boundary (e.g. in low-level test harnesses).

public type RawTcpStream is { fd: Int };
implement RawTcpStream {
    public fn connect(host: Text, port: Int) -> Maybe<RawTcpStream>;
    public fn send(&self, data: Text) -> Int;
    public fn recv(&self, max_len: Int) -> Text;
    public fn close(&self);
    public fn raw_fd(&self) -> Int;
}

public type RawTcpListener is { fd: Int };
implement RawTcpListener {
    public fn bind(port: Int) -> Maybe<RawTcpListener>;
    public fn accept(&self) -> Maybe<RawTcpStream>;
    public fn close(&self);
    public fn raw_fd(&self) -> Int;
}

public type RawUdpSocket is { fd: Int };
implement RawUdpSocket {
    public fn bind(port: Int) -> Maybe<RawUdpSocket>;
    public fn send_to(&self, data: Text, host: Text, port: Int) -> Int;
    public fn recv(&self, max_len: Int) -> Text;
    public fn close(&self);
}

The Raw* name prefix is mandatory — before the rename, the bare TcpStream / TcpListener / UdpSocket names silently shadowed the rich core.net.* API and broke addr.port() method lookup.

---

Module status

Each core.sys.* module carries an explicit conformance status so you know what you can rely on today versus what is still in flight. The status is the truth-table over the module's API surface as exercised by core-tests/sys/<module>/ under both verum test --interp (Tier 0 VBC interpreter) and verum test --aot (Tier 2 LLVM AOT).

Status	Meaning
complete	Everything stable requires, plus the coverage bar the conformance inventory sets for its top mark: algebraic laws pinned by property tests, cross-stdlib integration verified, and the module's audit findings landed or routed. A stable module graduates to complete when those land — the two are not synonyms.
stable	Every public method conformance-tested. Algebraic laws pinned by exhaustive or large-domain property tests. Cross-stdlib integration verified. Interpreter and AOT agree on every test. Safe to depend on in production.
partial	Subset of the public API is conformance-tested. The rest is exercised in regression_test.vr via @ignored (or workaround-style) tests pinning the specific defects that block coverage. The non-ignored API surface is safe; everything else is documented per-module under "Open defects".
regression-only	Module is gated by upstream stdlib / language-level defects. Public-API tests do not pass yet — only @ignored regressions exist to lock the bug shapes. Avoid in production until promoted.
undocumented	Documentation in this reference is authoritative, but the module has not yet been routed through the core-tests/ conformance suite. The current page is a best-effort snapshot of the source; it may drift from runtime behaviour.
unverified	The conformance suite has not been run against this module, so nothing on its row is a measurement. Distinct from undocumented: the module IS routed into core-tests/, but no result has been recorded since the liveness check that began demanding one.

Module	Status	Conformance suite
common.vr	partial	core-tests/sys/common — the type-level surface is covered: PAGE_SIZE, the page-alignment helpers, OSError, FileDesc, IOVec, MemProt, MapFlags, SysContextError, FcntlLockKind and the ACCESS_* / SEEK_* / F_*LCK constant families, plus the context-slot limits.
cabi.vr	complete	core-tests/sys/cabi — 22 unit + 9 property + 5 regression all green. Every alias (CInt / CUInt / CLong / CULong / CSize / CSSize / COff / CMode / CPid / CUid / CGid / CClockId / CSockLen / CFd) round-trips through tuple-newtype construction; CFD_STDIN / CFD_STDOUT / CFD_STDERR sentinel triple pinned. Transparent-wrapper newtype constructor registration fix in archive_ctx_loader.rs Pass 5 closed every CFD_* / direct-CFd-construction test.
bitfield.vr	partial	core-tests/sys/bitfield — unit, property, integration and regression suites all covered. The property suite sweeps single-bit, mask, field-mask and extract-insert round trips. Calling a free function across a module boundary returns a real value here, which it did not before.
mmio.vr	partial	core-tests/sys/mmio — BarrierKind's five variants and their dispatch, compiler_barrier/dmb, the MemoryFlags bitfield laws (single-bit power-of-two, pairwise disjointness, OR combines to the union, self-OR idempotent) and MemoryRegion.end/.contains over start, middle, the excluded end and below-start, all green under --interp. The BarrierKind half was silently wrong until recently and the way it was wrong is worth knowing: a match whose arms never matched fell through to the LAST arm, so a check that only ever constructed one variant passed. The pin now asserts the pair — the same value against its arm first and against its arm last — because only that pair distinguishes a real tag match from a fall-through. MemoryFlags constants and the MemoryRegion helpers that consume them remain gated by the TypeName.CONST.0 typechecker gap, the same one FileDesc.STDIN hits. MmioRegister<T, MODE> and the VerifiedRegister ghost state are deferred: they need a real memory-mapped fixture.
interrupt.vr	partial	core-tests/sys/interrupt — CriticalSection (enter / is_active / nesting), InterruptCell<T> construction and read-back over Int, Text, Bool, the integer extremes and a user record, and the @const no-side-effect pin, all green under --interp. InterruptCell was unusable until recently for a reason worth stating plainly: its field named a type the standard library does not define, so the constructor never compiled and every InterruptCell.new(v) was read as a method call on v itself. The field holds the value directly now, and the raw pointer comes from the same address-of idiom the rest of the library uses. Privileged ring-0 paths — @interrupt vector handlers, exception-frame I/O and context switching — are exercised by the conformance specs rather than here.
time_ops.vr	partial	core-tests/sys/time_ops — the arithmetic API (SysTimeOpsDuration.from_*, as_*, zero) is green under both the interpreter and ahead-of-time compilation, and the clock API (SysTimeOpsInstant.now, elapsed, duration_since) is green after a fix that replaced a hardcoded dependency with real propagation.
file_ops.vr	partial	core-tests/sys/file_ops — OpenMode bit-patterns (read=0 / write=0x301 / append=0x409 / create=0x241 / read_write=2) + error-sentinel paths (missing path → None / -1 / false) pinned end-to-end. replaced stale mount super.raw.* (pointed at deleted core/sys/raw.vr post-migration) with canonical mount core.intrinsics.runtime.os.{__file_*_raw}. Pre-fix every __file_*_raw call silently compiled to a lenient panic-stub. Happy-path round-trip (write→read of same content) deferred to integration suite with tmpdir fixture.
net_ops.vr	partial	core-tests/sys/net_ops — Raw* canonical-name (RawTcpStream / RawTcpListener / RawUdpSocket; #75 shadow-break) + fd round-trip + connect→None on unroutable-port sweep pinned. same architectural fix as file_ops. Live socket round-trip deferred (needs fixture pair).
process_ops.vr	unverified	core-tests/sys/process_ops — ProcessExitStatus.success ↔ code==0 + Child invalid-fd short-circuit + args/arg_count coherence pinned. same architectural fix. spawn / run happy path deferred (needs CI-portable fixture).
process_native.vr	partial	core-tests/sys/process_native — Unit, property, integration and regression suites. SpawnResult record construction + every-field projection identity across 8 capture configurations (2^3 Bool triples); -1 fd sentinel disjointness from valid fds; fork(2) pid trichotomy via custom ForkOutcome ADT; SpawnResult × List fleet iteration + Result<SpawnResult, Text> error funnel + 4-variant CaptureMode dispatch + Maybe lift. Live syscall surface (native_spawn / native_kill / native_fd_write_all / native_fd_read_chunk) + Windows path deferred.
context_ops.vr	partial	core-tests/sys/context_ops — TLS_SLOT_COUNT, the tls_set/tls_get round-trip, the context_provide/context_get/context_end DI triple and defer_depth tracking are pinned end-to-end and green under --interp. The round-trip is checked at both polarities: a slot written through the wrapper reads back its value, and a slot nothing wrote still reads absent. That second half matters because the whole surface used to be a no-op for its callers — the value was recorded against the stack frame of the stdlib wrapper that called the intrinsic, not the scope the user wrote the call in, so returning from tls_set discarded it. A context written through this surface now lives until it is explicitly ended or overwritten, which is what the platform TLS slot table does under AOT, where returning from a function does not clear a slot. defer_execute callback invocation remains deferred to Tier-1: the interpreter would have to synthesise indirect dispatch for an arbitrary fn(Int) -> Int pointer.
signal.vr	partial	core-tests/sys/signal — Not usable yet. The signal implementation in the library drifts on two counts: variant tags shift across configuration-gated match arms, and the atomic load and store intrinsics are not registered for the flag type. This is a library defect, not a gap in coverage.
fs_watch.vr	partial	core-tests/sys/fs_watch — FsEventKind 5-variant (Created/Modified/Deleted/Renamed/AttribChanged) + Clone impl + FsEvent record round-trip pinned. Integration suite adds exhaustive 5-variant dispatch + is_content_mutation predicate (Created/Modified/Deleted vs Renamed/AttribChanged) + events.iter().filter(content_mutation).count() reduction over List + variant pattern round-trip identity. FsWatcher.new() / add / remove / wait are NOT covered, and the reason is not a missing fixture: FsWatcher.new() panics under the interpreter with an unresolved cross-module stub before any filesystem activity is reached. Measured; see the caution box above.
io_engine.vr	partial	core-tests/sys/io_engine — EngineDuration ring algebra (from/as scaling, saturating add/sub, identity laws) + Fd partition (valid ↔ raw >= 0) + Fd.INVALID = -1 + TimeSpec record pinned end-to-end. Integration suite adds saturating_add at MAX clamp + EngineDuration ↔ TimeSpec round-trip across compound sub-second values + Fd × Maybe open(2) funnel + EngineDuration max-via-fold pattern over List + TimeSpec lift through Maybe pattern-match. IOEngine protocol round-trip + CompletionOp 18-variant + Port/BoundPort refinement validation + RawSocketAddr V4/V6 deferred.
init.vr	partial	core-tests/sys/init — InitError 6-variant (TlsFailed/ContextFailed/AllocatorFailed/PanicHandlerFailed/AlreadyInitialized/NotInitialized) + Eq laws (reflexivity / symmetry / payload-aware) + .message contents pinned. verum_init / verum_shutdown / panic_impl deferred (bootstrap-time + termination-time; out of scope for in-process tests).
durability.vr	partial	core-tests/sys/durability — Intent-named re-exports (full_fsync / data_only_fsync / sync_directory / pread / pwrite) resolve via the public mount core.sys.common.X chain. Error-funnel (Result<(), OSError> on invalid fd) pinned across full_fsync + data_only_fsync with the invalid-fd sweep. Happy-path round-trip + pread/pwrite/sync_directory CBGR-byte-slice deferred.
locking/mod.vr	partial	core-tests/sys/locking — FileLockKind, LockRegion and LockError data contracts are covered. Region laws include reflexivity, symmetry, disjointness, adjacency, single-byte overlap and the -1 EOF sentinel. Live try_lock/unlock round-trips require an fd fixture.
darwin/errno	complete	core-tests/sys/darwin/errno — 38 unit + 11 property + 6 integration + 4 regression. Canonical BSD errno values (EAGAIN=35, EWOULDBLOCK aliased, ENOENT=2 universal); 6 classifier predicates with predicate disjointness; total-over-Int sweep.
darwin/libsystem	partial	core-tests/sys/darwin/libsystem — 27u + 9p + 8i + 4r. POSIX/BSD constants (O_, PROT_, MAP_, SEEK_, MADV_, CLOCK_); PROT_* power-of-two algebra; SEEK partition of {0,1,2}; Darwin-specific O_CREAT=0x200, MAP_ANON=0x1000, O_CLOEXEC=0x1000000. Live FFI deferred.
darwin/mach	partial	core-tests/sys/darwin/mach — 17u + 7p + 3r. KERN_* 0..=14 + KERN_ABORTED=14; VM_PROT_* 3-bit power-of-two (DEFAULT=READ|WRITE=3, ALL=7); KernReturn(Int32) width-pin (regression class from T0.4.2 Phase 3). Live Mach FFI deferred.
darwin/thread	partial	core-tests/sys/darwin/thread — 14u + 5p + 3r. DarwinThreadError 10-variant + ONCE_INIT/RUNNING/COMPLETE lifecycle; Eq reflexive + payload-sensitive + variant-disjoint; monotone-increasing-lifecycle defect pin. Live thread.spawn deferred.
darwin/time	partial	core-tests/sys/darwin/time — 6u + 3p + 2r. CLOCK_*_ID constants (MONOTONIC=6 NOT Linux's 1); pairwise distinctness; kernel-range bound. Live clock readers deferred.
darwin/tls	partial	core-tests/sys/darwin/tls — 17u + 7p + 4r. MAX_CONTEXT_SLOTS=256, CONTEXT_STACK_DEPTH=8, TCB_MAGIC=0x5645525_5_4D5F_5443 ("VERUM_TC"); 8-variant SysTlsError with payload-sensitive Eq + is_retryable always-false. Live TCB allocation deferred.
darwin/io	partial	core-tests/sys/darwin/io — 30u + 5p + 4r. DarwinIoDriverError 13-variant ADT + DarwinIoOpKind 9-variant + from_errno mapper + is_retryable classifier + MAX_EVENTS=256/DEFAULT_TIMEOUT_NS=1e9. Live kqueue deferred.
darwin/mod	partial	core-tests/sys/darwin/mod — 23u + 11p + 7i + 5r. Umbrella path-equivalence: every umbrella ↔ direct submodule value preserved across libsystem/mach/errno/tls/io/thread/time.
linux/errno	complete	core-tests/sys/linux/errno — 25u + 8p + 4r. EAGAIN=11 NOT Darwin's 35; EWOULDBLOCK≡EAGAIN; 30-element low-POSIX 1..=30 pairwise distinct + consecutive sequence; predicate disjointness.
linux/mem	complete	core-tests/sys/linux/mem — 17u + 6p + 3r. PROT_* universal (1/2/4); MAP_* Linux-specific (MAP_ANON=0x20 NOT Darwin's 0x1000; MAP_ANONYMOUS≡MAP_ANON); MAP_* pairwise distinct sweep.
linux/time	partial	core-tests/sys/linux/time — 13u + 3p + 4r. 11 Linux clock IDs (REALTIME=0, MONOTONIC=1 NOT Darwin's 6, BOOTTIME=7, TAI=11); pairwise distinctness.
linux/auxv	complete	core-tests/sys/linux/auxv — 15u + 3p + 4r. AT_* auxv constants (NULL=0 terminator, PAGESZ=6, RANDOM=25, SYSINFO_EHDR=33 vDSO); UID/EUID/GID/EGID quartet consecutive.
linux/thread	partial	core-tests/sys/linux/thread — 16u + 3p + 4r. CLONE_* flags (VM=0x100 .. NEWPID=0x20000000); SIGCHLD=17 NOT Darwin's 20; pairwise disjoint + power-of-two. Live clone(2) deferred.
linux/tls	partial	core-tests/sys/linux/tls — 10u + 7p + 2r. arch_prctl ops (SET_GS=0x1001..GET_GS=0x1004 consecutive); TLS_ALIGN=64 power-of-two; STACK_GUARD_MAGIC=0xDEAD_BEEF_CAFE_BABE; MAX_CONTEXT_SLOTS=256 cross-platform invariant with Darwin. Live TCB deferred.
linux/io	partial	core-tests/sys/linux/io — 18u + 4p + 4r. io_uring SETUP/ENTER/REGISTER constants; SETUP bits 0..=7 consecutive; ENTER flags power-of-two; REGISTER opcode sequence. Live io_uring ring deferred.
linux/syscall	partial	core-tests/sys/linux/syscall — 23u + 5p + 5r. Architecture-invariant ABI constants: termios ioctls (TIOCGWINSZ=0x5413), fcntl ops (F_GETFD..F_SETFL=1..=4 consecutive), FD_CLOEXEC=1, O_NONBLOCK=0o4000, wait flags (power-of-two), futex ops (PRIVATE = base | 128). SYS_* numbers + raw syscall6 deferred.
linux/arch	partial	core-tests/sys/linux/arch — 15u + 4p + 3r. aarch64 SYS_* numbers (READ=63 NOT x86_64's 0, WRITE=64 NOT 1, CLOSE=57, OPENAT2=437 universal); consecutive read/write block 62..=67; SYS_FSYNC+1=SYS_FDATASYNC. x86_64 values gated.
linux/mod	partial	core-tests/sys/linux/mod — 7u + property/integration/regression triad. PROT_/MAP_ single-bit disjointness + MAP_ANON≡MAP_ANONYMOUS + errno distinct-positive + CLOCK_* distinct enumeration; mmap-flag composition + errno classification; cross-platform divergence pins (EAGAIN=11 NOT Darwin's 35, MAP_ANON=0x20, CLOCK_MONOTONIC=1, CLOCK_BOOTTIME=7 Linux-only). AOT validation needs a Linux target (@cfg(target_os="linux")) — deferred to a Linux runner.
linux/bpf/error	partial	core-tests/sys/linux/bpf/error — 20u + 22p + 1r + 12i. BpfError 8-variant ADT (OsError / VerifierRejected / InvalidAttachType / FeatureNotSupported / MapTypeMismatch / SizeMismatch / NotFound / UnsupportedHelper); Display textual stability; Eq reflexivity + symmetry + payload-sensitivity + cross-variant inequality; Result<T, BpfError> + List aggregation funnels; error-class dispatch table (Permission/Resource/Verifier/Compat/NotFound/Helper/Other) with errno-aware classification.
linux/bpf/map	partial	core-tests/sys/linux/bpf/map — MapType discriminant injectivity and wire tags, MapConfig boundaries, descriptor fields and result/value-buffer shapes are covered. bpf() syscall CRUD requires the Linux runner.
linux/bpf/program	partial	core-tests/sys/linux/bpf/program — ProgramType and AttachType discriminants, bytecode and descriptor round-trips, distinct link/program fds, license fields and verifier/error result shapes are covered. Live loading and attachment require the Linux runner.
linux/bpf/mod	partial	core-tests/sys/linux/bpf/mod — umbrella re-export data contracts and XDP program/map/link assembly are covered. Live load_program, attachment and map operations require the Linux runner.
windows/ntstatus	unverified	core-tests/sys/windows/ntstatus — 50u + 11p + 12r + 15i. 50+ NTSTATUS constants (STATUS_SUCCESS / PENDING / TIMEOUT / INVALID_HANDLE / ACCESS_DENIED / NO_MEMORY / OBJECT_NAME_NOT_FOUND / …) spanning all four severity domains; severity-bit dispatch (is_success / is_information / is_warning / is_error); bit-field accessors (code / facility / status_code); to_win32_error round-trip; name() lookup table on every documented arm; classifier helpers (is_retryable for STATUS_PENDING / is_not_found for the 4-arm not-found set / is_access_denied); pairwise disjointness of severity dispatch over the documented arm set. FUNDAMENTAL FIX LANDED: stdlib is_success rewritten to use NT_SUCCESS bit-31 form ((self.0 as UInt32) >> 31) == 0 instead of signed self.0 >= 0, avoiding the VBC UInt32 → Int32 cast signedness drift in the compile_cast passthrough arm. The defect (and the deferred VBC codegen fix) is pinned in regression_test.vr §A with the full isolation chain — see audit.md for details.
windows/kernel32	unverified	core-tests/sys/windows/kernel32 — 75u + 17p + 9r + 27i. 150+ Win32 constants (MEM_* / PAGE_* / FILE_ATTRIBUTE_* / FILE_FLAG_* / CREATE_* / OPEN_* / TRUNCATE_* / ERROR_* / WAIT_* / INFINITE / FILE_NOTIFY_CHANGE_* / FILE_ACTION_* / FILE_BEGIN/CURRENT/END / LOCKFILE_* / STARTF_USESTDHANDLES / CREATE_NO_WINDOW / HANDLE_FLAG_INHERIT / STILL_ACTIVE / CREATE_SUSPENDED / TLS_OUT_OF_INDEXES); bitmask-safety contract pinned (MEM_* / PAGE_* / FILE_FLAG_* / FILE_NOTIFY_CHANGE_* are powers of two + pairwise distinct); standard handles as documented two's-complement negatives (STD_INPUT=-10/STD_OUTPUT=-11/STD_ERROR=-12 as UInt32 0xFFFFFFF6/0xFFFFFFF5/0xFFFFFFF4); WAIT_FAILED ≡ INFINITE both 0xFFFFFFFF (disambiguated by call context). FFI bindings (CreateFileW / ReadFile / WaitForSingleObject / …) deferred to Windows runner.
windows/ntdll	unverified	core-tests/sys/windows/ntdll — 32u. Handle newtype (NULL.raw()==0, INVALID.raw()==-1, is_valid for NULL/INVALID/arbitrary, raw round-trip); OBJ_* object-attribute flags (8 constants including OBJ_VALID_ATTRIBUTES=0x7F2 bit-union); standard rights (GENERIC_READ/WRITE/EXECUTE/ALL + DELETE/READ_CONTROL/WRITE_DAC/WRITE_OWNER/SYNCHRONIZE); 13 FILE_* access-mask constants (FILE_READ_DATA/WRITE_DATA/APPEND_DATA/READ_EA/WRITE_EA/EXECUTE/DELETE_CHILD/READ_ATTRIBUTES/WRITE_ATTRIBUTES + FILE_ALL_ACCESS/FILE_GENERIC_READ/WRITE/EXECUTE composites); NtCreateFile disposition codes (FILE_SUPERSEDE/OPEN/CREATE/OPEN_IF). Nt* FFI bindings deferred to Windows runner.
windows/tls	unverified	core-tests/sys/windows/tls — 15u. MAX_CONTEXT_SLOTS=256 + CONTEXT_STACK_DEPTH=8 (cross-platform invariants matching Linux/Darwin); TCB_MAGIC=0x5645_5255_4D5F_5443 ("VERUM_TC", 16 hex digits / 64-bit); DEFAULT_STACK_SIZE=1 MiB; GUARD_PAGE_SIZE=4 KiB; WindowsTlsError 8-variant ADT (NotInitialized / AlreadyInitialized / AllocationFailed{code,size} / InvalidSlot{slot} / StackOverflow{slot} / StackUnderflow{slot} / InvalidTcb / TlsIndexExhausted) with payload round-trip + Display textual stability. TCB allocation / TlsAlloc / ctx_push / ctx_pop / ctx_get / ctx_set deferred to Windows runner.
windows/time	unverified	core-tests/sys/windows/time — 27u. Scale-ladder constants (NANOS_PER_SEC=10^9, NANOS_PER_MILLI=10^6, NANOS_PER_MICRO=10^3, MILLIS_PER_SEC=10^3, MICROS_PER_SEC=10^6, FILETIME_UNITS_PER_SEC=10^7, WINDOWS_EPOCH_OFFSET=116444736000000000) + cross-unit equivalence laws (NANOS_PER_SEC == NANOS_PER_MILLI × MILLIS_PER_SEC; NANOS_PER_MILLI == NANOS_PER_MICRO × 1000); WindowsDuration newtype — from_nanos/micros/millis/secs + as_* round-trip + zero/is_zero + add/sub (saturating at zero) / mul / div + subsec_nanos / subsec_millis on whole-second and fractional inputs + 1s/1ms/1µs cross-scale equivalence. WindowsInstant (QueryPerformanceCounter) + sleep + system_time deferred to Windows runner.
windows/thread	unverified	core-tests/sys/windows/thread — 19u. DEFAULT_THREAD_STACK_SIZE=1 MiB; Once state machine constants (ONCE_INIT=0, ONCE_RUNNING=1, ONCE_COMPLETE=2 — pairwise distinct sentinels for the 3-state CAS pattern); WindowsThreadError 11-variant ADT (CreateFailed/JoinFailed/SuspendFailed/ResumeFailed/MutexInitFailed/MutexLockFailed/CondInitFailed/CondWaitFailed each with code:UInt32 + TlsInitFailed/AlreadyJoined/AlreadyDetached) with payload round-trip + message() textual stability for the unit-payload variants. spawn/join/Mutex/Condvar/SpinLock/Once/futex_wait/wake deferred to Windows runner.
windows/winsock2	unverified	core-tests/sys/windows/winsock2 — 22u. POSIX-compat socket constants with cross-platform divergence catalogue pinned: AF_INET=2 (POSIX) / AF_INET6=23 (Windows-specific, NOT Linux's 10); SOCK_STREAM=1 / SOCK_DGRAM=2 (POSIX); SOCK_NONBLOCK=0 / SOCK_CLOEXEC=0 (Windows uses ioctlsocket(FIONBIO) + SetHandleInformation, NOT socket() type flags); IPPROTO_TCP=6 / IPPROTO_UDP=17 (IANA); SOL_SOCKET=0xFFFF (Windows-specific, NOT Linux's 1); SO_ERROR=0x1007 (Windows-specific); SHUT_RD/WR/RDWR=0/1/2 (POSIX); MSG_PEEK=2 (POSIX); MSG_DONTWAIT=0 (Windows lacks MSG_DONTWAIT); SOCKET_ERROR=-1 (POSIX-compat); INVALID_SOCKET=0xFFFFFFFFFFFFFFFF_u64 (Windows-specific, SOCKET is unsigned UINT_PTR); WindowsSockaddrIn / WindowsSockaddrIn6 record-shape round-trip with 16-byte IPv6 addr buffer. ws2_32.dll FFI bindings deferred to Windows runner.
windows/io	unverified	core-tests/sys/windows/io — 7u. MAX_EVENTS=256 (IOCP dequeue cap); DEFAULT_TIMEOUT_MS=1000 / DEFAULT_TIMEOUT_NS=10^9 with cross-unit equivalence NS / 10^6 == MS; WindowsIoToken newtype round-trip with 0 and 0xFF..FF sentinels. IocpDriver / async_read / async_write / IocpEventIter deferred to Windows runner.
windows/mod	unverified	core-tests/sys/windows/mod — 21u. Umbrella reachability + value preservation across the 8 windows submodules — every documented re-export (NtStatus + STATUS_* / kernel32 Handle constants + GENERIC_/CREATE_/INFINITE/WAIT_/STD_*/INVALID_HANDLE_VALUE / TLS constants / time scale ladder / winsock POSIX-compat divergence catalogue) resolves at compile time and produces the expected value at runtime.
embedded.vr	partial	core-tests/sys/embedded — Unit, property, integration and regression suites. StackAllocator bump arithmetic (alignment rounding, sequential allocs, OOM sentinel returns 0, reset semantics) + used() + remaining() == capacity() invariant + remaining monotone-decreasing + alignment-relative-to-buffer-base contract + OOM-does-NOT-advance-offset defect-class pin. RingBuffer empty/full/len invariants over positive + zero capacities. PanicAction 3-variant exhaustive dispatch. Integration: Maybe OOM funnel + bootloader struct-table pattern + two-independent-allocators coexistence + List pointer-collection ascending-order. Volatile MMIO push/pop + @cfg(runtime="embedded") gated paths (set_panic_action / embedded_panic / Custom handler) deferred to vcs/specs/L0-critical/embedded/.
no_runtime.vr	partial	core-tests/sys/no_runtime — Unit, property, integration and regression suites. block_on identity over Int/Text/Bool/Int.max/Int.min boundaries; spawn_sync inline-execution identity over 3 function shapes; SyncChannel two-state lifecycle (Empty → Full(T) → Empty) + send-on-Full preserves existing (defect-class pin) + recv-on-Empty is None + N-cycle alternation returns to Empty; NoOpMutex payload-identity sweep over Int domain + lock/unlock preserves value. Integration: SyncChannel producer/consumer pipeline draining List into accumulator + collecting received back into List + 8-cycle retransmit pattern; NoOpMutex custom-record payload. @cfg(runtime="none") build-mode gate verification + compile-time select!/channels rejection deferred to vcs/specs/L0-critical/.
mod.vr (umbrella)	complete	core-tests/sys/mod — Unit, property, integration and regression suites. Path-equivalence laws: PAGE_SIZE ↔ common.PAGE_SIZE / MAX_CONTEXT_SLOTS ↔ common.MAX_CONTEXT_SLOTS / CONTEXT_STACK_DEPTH ↔ common.CONTEXT_STACK_DEPTH / USIZE_BITS ↔ bitfield.USIZE_BITS. Constant invariants (PAGE_SIZE positive + power-of-two + ≥ 4096; MAX_CONTEXT_SLOTS positive + power-of-two; USIZE_BITS byte-multiple + ≥ 32). Type-identity preservation across umbrella + direct submodule paths for OSError, Fd, MemoryRegion, BarrierKind, MemoryFlags, InitError, TimeSpec, SysContextError, MemProt, MemoryOrdering, MapFlags. Platform-conditional re-exports (linux/darwin/windows) + @cfg(runtime=*) umbrella mounts deferred to per-platform vcs specs.

---

Bitfields and MMIO

core.sys.bitfield — bit-manipulation primitives

Status: regression-only.

The 8 free functions plus field_mask and USIZE_BITS are landed in core/sys/bitfield.vr and route through core/sys/mod.vr's bitfield.{...} re-export. Implementation is pure, @inline(always), branchless except at the documented width == 0 / width >= USIZE_BITS boundaries — under monomorphisation each call collapses to one or two CPU instructions and is eligible for constant folding when the arguments are compile-time constants.

The conformance suite is complete — the cross-module free-function dispatch defect is closed (see core-tests/sys/bitfield/audit.md §3.2). Unit, property, integration and regression suites are all green under --interp.

AOT: two AOT-specific compiler defects that blocked the bitfield module under verum test --aot were closed — D1 (AOT-UMBRELLA-REEXPORT-1): the bitfield free functions are re-exported through the core.sys umbrella, and strict (AOT) compilation failed to resolve mount core.sys.{extract_bits} (E100 unbound variable); and D7 (AOT-NOT-USIZE-1): bitwise-NOT !mask on a USize was rejected by the typechecker. Both are fixed in verum_types (see defect-class-catalogue §21/§22 — verum repo, docs/architecture/defect-class-catalogue.md). The AOT failure histogram collapsed from ~2000 unbound + 147 NOT errors to zero of those classes; a full sustained AOT green run is pending a stable build environment.

Canonical API surface

All operations work over USize — the platform-native bitfield word that pairs with the BitfieldElement protocol's to_bits / from_bits lingua franca. On any 64-bit target the LLVM lowering is bit-identical to UInt64; on 32-bit embedded targets USize narrows to 32 bits and the operations follow.

mount core.sys.bitfield;

// --- Bit-width constant ----------------------------------------
public const USIZE_BITS: USize = USize.bits;

// --- Single-bit operations -------------------------------------
public pure fn test_bit(value: USize, n: USize) -> Bool;
public pure fn set_bit(value: USize, n: USize) -> USize;
public pure fn clear_bit(value: USize, n: USize) -> USize;
public pure fn toggle_bit(value: USize, n: USize) -> USize;

// --- Mask operations -------------------------------------------
public pure fn set_bits(value: USize, mask: USize) -> USize;
public pure fn clear_bits(value: USize, mask: USize) -> USize;

// --- Field operations ------------------------------------------
public pure fn field_mask(offset: USize, width: USize) -> USize;
public pure fn extract_bits(value: USize, offset: USize, width: USize) -> USize;
public pure fn insert_bits(value: USize, bits: USize, offset: USize, width: USize) -> USize;

Boundary table

Let N = USIZE_BITS. Every field operation lifts the boundary cases out of the hot path so the call is total over 0..=N regardless of host-instruction-set quirks.

width	extract_bits(v, o, w)	insert_bits(v, b, o, w)	field_mask(o, w)
0	0	value (no field, no change)	0
1..N-1	(v >> o) & ((1 << w) - 1)	(v & !field) | ((b & low_mask) << o)	((1 << w) - 1) << o
N (full)	value (full read-through)	bits (full overwrite)	!0 (all ones)

The width >= USIZE_BITS lift exists because LLVM defines shl ?, N as poison when N >= bit_width; on x86_64 the silicon further masks the shift count to N-1, producing 1 << 0 = 1 instead of "all ones". Without the lift the hot-path expression would yield UB at the boundary; with it, every call is defined.

Algebraic laws

Every operation carries an algebraic contract:

Operation	Law
set_bit / clear_bit / set_bits / clear_bits	Idempotent: applying twice with the same mask/index is the same as applying once.
toggle_bit	Self-inverse: toggle_bit(toggle_bit(v, n), n) == v.
extract_bits ∘ insert_bits	Round-trip: extract_bits(insert_bits(v, b, o, w), o, w) == b & field_mask(0, w) for any o + w ≤ USIZE_BITS.
field_mask	Disjoint-union: field_mask(o, w) | field_mask(o + w, k) == field_mask(o, w + k) when o + w + k ≤ USIZE_BITS.
insert_bits	Adjacent-field independence: leaves every bit outside [o, o + w) unchanged.
test_bit ↔ extract_bits	test_bit(v, n) == (extract_bits(v, n, 1) == 1) for every n < USIZE_BITS.
set_bit ↔ set_bits	set_bit(v, n) == set_bits(v, 1 << n) (single-bit form is the mask form specialised to a unit mask). Same for clear_bit ↔ clear_bits.

Caller contracts (NOT runtime-enforced)

n < USIZE_BITS                  for *_bit operations
offset + width <= USIZE_BITS    for *_bits / extract / insert
width <= USIZE_BITS             for field_mask / extract / insert

Violating these silently yields the LLVM-poison value of the underlying shift; downstream computations remain defined-but-garbage. Bitfield-codegen call sites prove these invariants from the surrounding @bits(N) annotations, so the runtime checks would be pure overhead.

Example — packed sensor sample

mount core.sys.bitfield;

// 16-bit packed sample: 4-bit channel | 12-bit value
fn pack_sample(channel: USize, value: USize) -> USize {
    let raw = bitfield.insert_bits(0 as USize, channel, 0 as USize, 4 as USize);
    bitfield.insert_bits(raw, value, 4 as USize, 12 as USize)
}

fn unpack_sample(raw: USize) -> (USize, USize) {
    let channel = bitfield.extract_bits(raw, 0 as USize, 4 as USize);
    let value   = bitfield.extract_bits(raw, 4 as USize, 12 as USize);
    (channel, value)
}

BitfieldElement and Bitfield protocols

The protocols underlie compiler-generated @bitfield types (see @bitfield attribute below):

public type BitfieldElement is protocol {
    const BIT_WIDTH: USize;
    fn from_bits(bits: USize) -> Self;
    fn to_bits(self) -> USize;
};

implement BitfieldElement for Bool   { const BIT_WIDTH: USize = 1;  ... }
implement BitfieldElement for UInt8  { const BIT_WIDTH: USize = 8;  ... }
implement BitfieldElement for UInt16 { const BIT_WIDTH: USize = 16; ... }
implement BitfieldElement for UInt32 { const BIT_WIDTH: USize = 32; ... }
implement BitfieldElement for UInt64 { const BIT_WIDTH: USize = 64; ... }

public type Bitfield is protocol {
    const SIZE_BYTES: USize;
    const SIZE_BITS:  USize;
    fn zero() -> Self;
    fn as_bytes(&self)        -> &[UInt8];
    fn as_bytes_mut(&mut self) -> &mut [UInt8];
};

The compiler auto-derives Bitfield for any type annotated with @bitfield. Bitfield fields have one absolute restriction: their address cannot be taken (&field is forbidden). Total bits must align to byte boundaries (or use explicit @padding).

@bitfield attribute and derived types

@repr(C)
@bitfield
@endian(little)
public type TcpFlags is {
    @bits(1) fin: Bool,
    @bits(1) syn: Bool,
    @bits(1) rst: Bool,
    @bits(1) psh: Bool,
    @bits(1) ack: Bool,
    @bits(1) urg: Bool,
    @bits(2) reserved: UInt8,
};

let flags = TcpFlags { fin: true, syn: true, ..TcpFlags.zero() };
assert(flags.fin);
assert(flags.syn);

Compile-time verification helpers (used by @bitfield lowering):

@const public fn verify_byte_alignment<TOTAL_BITS: meta USize>() -> Bool
    where TOTAL_BITS % 8 == 0;

@const public fn verify_field_width<FIELD_BITS: meta USize, TYPE_BITS: meta USize>() -> Bool
    where FIELD_BITS <= TYPE_BITS;

@const public fn verify_enum_fits<MAX_VARIANT: meta USize, BITS: meta USize>() -> Bool
    where MAX_VARIANT < (1 << BITS);

Open defects

The conformance suite under core-tests/sys/bitfield/ pins three language-level defects that block the suite from turning green at runtime; each has its own task on the language-implementation track.

#	Defect	Status
1	Cross-module free-function dispatch silently returned Unit/nil at run time under the interpreter — it affected every mount X.{free_fn} and module.fn(args) call site.	closed
2	mount X.{public_const} does not register the name for code generation, so a cross-module import of a public const reports an undefined variable. Workaround: mount X; X.CONST.	partial — the bare-mount form works; the selective form does not
3	Parallel UInt64 implementations in core.math.bits previously caused codegen to dispatch to the wrong implementation under monomorphisation. Eliminated by collapsing to the single canonical home (core.sys.bitfield); pinned in regression_test.vr to prevent re-introduction.	closed
4	AOT compilation can report undefined variable: <VariantName> for a bare variant in a stdlib return expression, such as resolution_for in core/database/sqlite/native/vfs_xcurrenttime_api/clock.vr. Qualifying the variant (Resolution.RsSeconds) is the documented workaround.	Open: declaration return types must reach expression-position variant lookup.

These defects are NOT specific to core.sys.bitfield — they are foundational language-level gaps that cascade into every module that exercises cross-module free-function calls. Closing any of them unlocks coverage in many downstream modules at once.

MMIO — memory-mapped I/O

// The mode says what the hardware permits, not how the access is
// ordered — every MMIO access is volatile by construction.
type AccessMode is
    ReadOnly | WriteOnly | ReadWrite | ReadWriteOnce
    | WriteOneToClear | WriteOneToSet;

// `MmioRegister`, parameterised by the mode rather than storing it,
// and built from an address at compile time.
type MmioRegister<T: Copy, MODE> is { addr: *volatile mut T };

implement<T: Copy, MODE> MmioRegister<T, MODE> {
    @const fn at(addr: USize) -> MmioRegister<T, MODE>;
}

type MemoryRegion is { start: USize, size: USize, flags: MemoryFlags };
type MemoryFlags  is (UInt32);          // READ | WRITE | EXEC | DMA

implement MemoryRegion { fn contains(&self, addr: USize) -> Bool; }

// From core.intrinsics.lowlevel.mmio, re-exported here.
fn volatile_load<T>(ptr: *volatile T) -> T;
fn volatile_store<T>(ptr: *volatile mut T, value: T);
fn volatile_load_acquire<T>(ptr: *volatile T) -> T;
fn volatile_store_release<T>(ptr: *volatile mut T, value: T);

fn dmb();                                        // data memory barrier
fn compiler_barrier();                           // reorder fence only

There is no Register, no barrier(order), no dsb and no isb, and MemoryOrdering is not a type in this module — acquire/release ordering is chosen by picking the _acquire / _release accessor. The volatile intrinsics take a *volatile pointer, not a bare address.

Interrupts

type ExceptionFrame is { ... };                 // CPU context at exception
type CriticalSection is { ... };

fn disable_interrupts() -> CriticalSection       // RAII guard
fn enable_interrupts()
cs.release()                                     // re-enables on drop

---

Byte-range file locking — sys.locking

Advisory byte-range locking, typed and capability-safe. Wraps fcntl(F_OFD_SETLK) on Linux, fcntl(F_SETLK) on macOS, and LockFileEx on Windows. Used by core.database to implement SQLite's 5-state locking protocol.

mount core.sys.locking.{LockRegion, FileLockKind, LockHandle, try_lock, unlock};

public type LockKind is Shared | Exclusive;     // no Unlock variant — unlock consumes
public type LockRegion is { start: Int, length: Int };  // length == -1 ⇒ to EOF
public type LockError is
      Conflict(owner_pid: Maybe<Int>)           // EAGAIN / EWOULDBLOCK
    | IoFailure(OSError);

public type affine LockHandle is { /* ... */ }; // RAII; must be consumed

Core surface

public fn try_lock(fd: FileDesc, region: LockRegion, kind: LockKind)
    -> Result<LockHandle, LockError>;

public fn unlock(handle: LockHandle) -> Result<(), LockError>;

// Convenience for single-byte locks (SQLite PENDING_BYTE / RESERVED_BYTE)
public fn try_lock_byte_exclusive(fd: FileDesc, offset: Int)
    -> Result<LockHandle, LockError>;
public fn try_lock_byte_shared(fd: FileDesc, offset: Int)
    -> Result<LockHandle, LockError>;

The affine annotation on LockHandle is the safety surface: the handle may be moved but not copied, and dropping without calling unlock is a compile error. The lock cannot leak on the underlying fd.

Advisory on POSIX, mandatory on Windows. NFS is not supported — try_lock on an NFS fd surfaces as IoError(OSError) rather than silently returning "success".

Crash-safe persistence — sys.durability

Named re-exports of the durability primitives inside sys.common. The dedicated module lets callers declare their intent at the import site:

mount core.sys.durability.{full_fsync, sync_directory};

Function	Behaviour
full_fsync(fd)	Linux: fsync(fd). macOS: fcntl(fd, F_FULLFSYNC). Windows: FlushFileBuffers(handle). Returns only after the data is on stable storage — not just in the OS page cache.
sync_directory(path)	Open directory read-only, fsync it, close. Required on POSIX after rename/unlink/creat for the name change to survive power loss. No-op on Windows (NTFS journals directory updates synchronously).

Used by core.database between WAL frame flush and checkpoint; by core.io.atomic_write for the rename-after-write pattern; by file-backed caches anywhere. The F_FULLFSYNC distinction matters on macOS — ordinary fsync() on Darwin does not flush the disk's write cache.

---

Permission gating (#12 / P3.2)

Every raw-syscall intrinsic (syscall0..=syscall6, IntrinsicCategory.Syscall) is registered with the IntrinsicHint.RequiresPermission marker. Codegen consults the marker to insert a __permission_check(scope, target) -> Result<(), PermissionDenied> gate before the intrinsic body so deny-listed contexts (sandboxed scripts, capability-attenuated subroutines) get a typed refusal instead of silent OS-resource access.

The marker is enforced at the intrinsic-registry level by two pin checks:

• Every Syscall-category intrinsic carries the hint; new ones added without it fail loudly at registry-build time.
• Time, Platform, and Logging intrinsics that happen to carry IoEffect MUST NOT carry RequiresPermission. Gating those would force every print() and monotonic_nanos() through the permission router for no security benefit (no caller- controlled resource targets).

The codegen-side check insertion (with per-(scope, target) caching for ≤2 ns warm overhead) is the follow-up phase.

Platform-specific modules

Linux (@cfg(target_os = "linux"))

mount sys.linux;

// Direct syscalls (gated — all 7 carry IntrinsicHint.RequiresPermission)
unsafe fn syscall_raw(num: Int, a0..a5: Int) -> Int
unsafe fn syscall6(num: Int, a0..a5: Int) -> Int

// Common wrappers
unsafe fn read(fd: Int, buf: *mut Byte, count: Int) -> Int
unsafe fn write(fd: Int, buf: *const Byte, count: Int) -> Int
unsafe fn close(fd: Int) -> Int
unsafe fn mmap(addr: *mut Byte, len: Int, prot: Int, flags: Int, fd: Int, offset: Int) -> *mut Byte
unsafe fn munmap(addr: *mut Byte, len: Int) -> Int
unsafe fn mprotect(addr: *mut Byte, len: Int, prot: Int) -> Int

// Processes
fn getpid() -> Int           fn gettid() -> Int
fn exit(code: Int) -> !      fn exit_group(code: Int) -> !

// Synchronisation
unsafe fn futex_wait(uaddr: *mut Int32, expected: Int32, timeout: *const Timespec) -> Int
unsafe fn futex_wake(uaddr: *mut Int32, n: Int) -> Int

// Time
fn clock_gettime(clk_id: Int) -> Timespec
type Timespec is { tv_sec: Int64, tv_nsec: Int64 };

// I/O drivers
type IoUringDriver is { ... };
type EpollDriver   is { ... };

// Sync primitives (futex-based)
type Thread  is { ... };
type Mutex   is { ... };
type Condvar is { ... };
type SpinLock is { ... };

macOS (@cfg(target_os = "macos"))

mount sys.darwin;

// libSystem.B FFI
@extern("C") fn malloc(size: Int) -> *mut Byte
@extern("C") fn free(ptr: *mut Byte)
@extern("C") fn read(fd: Int, buf: *mut Byte, n: Int) -> Int

// Mach
type mach_port_t = UInt32;
fn mach_task_self() -> mach_port_t
fn mach_vm_allocate(task, addr, size, flags) -> KernReturn
fn mach_vm_deallocate(task, addr, size) -> KernReturn

Windows (@cfg(target_os = "windows"))

mount sys.windows;

// kernel32
@extern("C") fn VirtualAlloc(lp: *mut Byte, size: Int, type: UInt32, protect: UInt32) -> *mut Byte
@extern("C") fn VirtualFree(lp: *mut Byte, size: Int, type: UInt32) -> Int32
@extern("C") fn ReadFile(h: Handle, buf: *mut Byte, count: UInt32, read: *mut UInt32, overlapped: *mut Overlapped) -> Int32
@extern("C") fn CreateFileW(...)

// ntdll
@extern("stdcall") fn NtCreateFile(...) -> NtStatus

// I/O driver
type IocpDriver is { ... };

---

Alternative runtimes

Embedded (@cfg(runtime = "embedded"))

mount sys.embedded;

// Stack allocator (no heap)
fn stack_alloc(size: Int, align: Int) -> Maybe<*mut Byte>
fn stack_reset()                                // reset to mark

// Async stubs (sync shim)
// async {...}.await   compiles to blocking execution

no_runtime (@cfg(runtime = "no_runtime"))

mount sys.no_runtime;

// All heap operations return None / error
// Async compiled away
// Used for kernel startup, bootloaders

---

Cross-references

• mem — os_alloc feeds the segment allocator.
• io — file operations call through sys.file_ops.
• net — TCP/UDP uses sys.net_ops and the IO engine.
• async — executor uses the IO engine for readiness.
• intrinsics → runtime — low-level time, TLS, syscall intrinsics.