core.sys — V-LLSI kernel bootstrap

sys is the lowest-level module, the one and only FFI boundary. All higher-level stdlib modules (io, net, async, mem) sit on top.

V-LLSI = Verum Low-Level System Interface. No libc dependency:

• 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.

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

---

Conformance baseline (2026-06-11)

✅ Update (later same day): Bug A and Bug B below are CLOSED (cee79ec03, 08ede3518). On the fixed build: durability 3/8-fail → 11/11, darwin/libsystem TIMEOUT(hang) → 51/0, linux/time TIMEOUT → 20/0, no regressions — 39/51 leaf modules now fully green. Remaining failures are a heterogeneous tail (umbrella re-export Bug C, method-on-newtype dispatch, assorted assertion failures, codegen/data cluster), tracked in core-tests/sys/SYS_SPECTRUM_AUDIT.md §F. The original root-cause writeup is kept below as the fix record.

A full per-module --interp sweep (one process per leaf module, so a single interpreter hang/crash isolates instead of aborting the suite) puts 37 of 51 core/sys leaf modules fully green (~2010 of ~2150 @test). Every pure-data module — constants, ADTs, bit layouts, error enums — passes on both the native (Linux/macOS) and cross-target (Windows-on-host) data surfaces. The remaining failures concentrate entirely in modules that drive real platform/FFI operations, and trace to two live compiler defects in the stdlib precompile + archive path:

• Bug A — cross-module stdlib calls stubbed to nil at precompile. A call from one stdlib module into another (e.g. sys.common.full_fsync → sys.darwin.libsystem.safe_full_fsync) is silently replaced with a LOAD_NIL; RET stub during the stdlib bootstrap precompile (function-id ordering / two-pass gap). The wrapper then returns Ok(())/nil for every input — it never reports Err on an invalid fd, and umbrella re-exports of non-zero constants collapse to 0. This is the dominant cause: durability (8), darwin/mod umbrella (30), and the FFI-routed single-test failures in locking/darwin/io/file_ops/fs_watch/init/io_engine/signal. A fresh user compile of the same call resolves correctly, so the defect is confined to the archive precompile.

• Bug B — archive FFI symbols not carried into the consuming module. merge_archive_function_bodies remaps func_id / type_id / const_id / string_id references in copied archive bodies but not the ffi_symbols table or the CallFfiC symbol-index operand, so a body that does reach an FFI call indexes the wrong symbol table (FFI symbol not found: FfiSymbolId(N)).

• AOT is blocked suite-wide by a separate pre-existing defect: verum build --aot reports E402: module core.sys.common not found for any program that mounts a stdlib submodule, so the --aot half of the interp+aot CI contract cannot yet be met for sys (or any module).

Full per-module table, VBC evidence, reproductions, and fix surfaces: core-tests/sys/SYS_SPECTRUM_AUDIT.md. The single highest-leverage fix is Bug A (two-pass precompile cross-module resolution): it alone clears the durability + darwin/mod clusters (38 tests) plus most of the single-test FFI failures; Bug B is the necessary follow-on so the un-stubbed calls execute.

---

Common types

type OSError is { code: Int, message: Text };
type FileDesc is (Int);                // type-safe file descriptor wrapper
type IOVec is { base: *mut 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(&self, op: CompletionOp) -> Result<SubmissionId, IoError>;
    fn poll(&self, timeout: Maybe<Duration>) -> List<CompletionResult>;
    fn shutdown(&self);
}

type CompletionOp is
    | Read  { fd: FileDesc, buf: *mut Byte, len: Int, offset: Int }
    | Write { fd: FileDesc, buf: *const Byte, len: Int, offset: Int }
    | Accept { fd: FileDesc, addr: *mut Byte, addrlen: *mut Int }
    | Connect { fd: FileDesc, addr: *const Byte, addrlen: Int }
    | Send { fd: FileDesc, buf: *const Byte, len: Int, flags: Int }
    | Recv { fd: FileDesc, buf: *mut Byte, len: Int, flags: Int }
    | Timeout { duration: Duration }
    | Close { fd: FileDesc };

type CompletionResult is {
    submission_id: SubmissionId,
    result: Int,                    // negative = errno
    flags: Int,
};

fn create_io_engine(config: IoEngineConfig) -> Result<Heap<IOEngine>, IoError>

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 {
    public fn new() -> Result<FsWatcher, Text>
    // .watch(path) — add a target to the watcher
    // .recv()      — block for the next FsEvent
    // .recv_with_timeout(d) — bounded wait
}

---

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>)
    | IoError(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
    | AlreadyInitialized
    | InvalidConfig(Text)
    | PlatformError(OSError);

type PanicInfo is {
    message: Text,
    location: SourceLocation,
    thread_id: Int,
};
fn panic_impl(info: &PanicInfo) -> !
fn set_panic_handler(h: fn(&PanicInfo) -> !)

---

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 task #5 — 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 (#75) — pre-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
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.

Module	Status	Conformance suite
common.vr	partial	core-tests/sys/common — 70+ type-level tests green: PAGE_SIZE / page_align_* / OSError / FileDesc / IOVec / MemProt / MapFlags / SysContextError / FcntlLockKind / ACCESS_* / SEEK_SET / F_*LCK / MAX_CONTEXT_SLOTS / CONTEXT_STACK_DEPTH. Mount re-export defect (mount core.sys.{PAGE_SIZE} resolving to wrong sibling) closed by parent-prefix scan in process_import_tree. Two fundamental fixes landed 2026-05-16 (commits 0b17c7579 + c8e39850c): (a) sized-integer ==/!= (Int8/Int16/Int32/Int64/UInt8..UInt128/USize/ISize/Byte) on cross-module-const operands no longer infinite-recurses through method dispatch — compile_binary's is_primitive extended to consult is_numeric_type registry + extract_expr_type_name(Path) propagates const declared types; (b) EqG protocol_id=0 (blanket-impl <T: Eq> Eq dispatch like Maybe<OSError>.eq) now reads runtime ObjectHeader.type_id and dispatches through <TypeName>.eq instead of falling through to structural deep_value_eq (OSError.eq compares only code, so structural pre-fix returned false for two same-code different-message records). FileDesc.STDIN/INVALID const-method access deferred (typechecker __newtype_inner_X gap for archive-loaded transparent-wrapper records). FFI-adjacent surface (os_alloc / pread / pwrite / fsync / try_lock_region / file_size / access / random_bytes / init_process_args) deferred to per-platform integration.
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	complete	core-tests/sys/bitfield — 56 unit + 31 property + 22 integration + 3 regression. Cross-module free-fn dispatch defect closed (audit §3.2 — task #121); regression_dispatch_returns_real_bool flipped GREEN under --interp. Property suite sweeps single-bit / mask / field-mask / extract-insert round-trip algebraic laws; integration suite exercises BitfieldElement<{Bool,UInt8,UInt16,UInt32,UInt64}> round-trip + Endianness 3-variant + List-iter-filter test_bit partition + popcount-via-test_bit loop.
mmio.vr	partial	core-tests/sys/mmio — 8/8 BarrierKind + compiler_barrier/dmb green + 12 algebraic-law sweeps (BarrierKind 5-variant exhaustive + dispatch-tag pairwise distinctness; MemoryFlags single-bit power-of-two + pairwise disjointness + OR-combines-to-union + self-OR-idempotent; MemoryRegion.end + contains start/middle/exclude-end/exclude-below-start + every-addr-in-range sweep). MemoryFlags const access + MemoryRegion methods consuming MemoryFlags const gated by typechecker __newtype_inner_X gap (same as FileDesc.STDIN). MmioRegister<T, MODE> generic + VerifiedRegister ghost-state deferred — require runtime MMIO fixture.
interrupt.vr	complete	core-tests/sys/interrupt — 3 unit + 8 property + 7 integration + 2 regression. Kernel-intrinsic registry gap CLOSED 2026-05-27: replaced 5 @intrinsic(…) externs in core/intrinsics/lowlevel/kernel.vr (disable_interrupts, enable_interrupts, interrupts_enabled, restore_interrupts, save_and_disable_interrupts) with safe-default Verum bodies for the host target (return true / 0 / no-op). Kernel/embedded targets override via @cfg(no_runtime) / per-platform module. The previously-failing CriticalSection.is_active chain now compiles cleanly and runs deterministically; full surface (CriticalSection ∘ InterruptCell<T> ∘ disable_interrupts ∘ context_switch) is pinned in the conformance suite. Privileged ring-0 paths (@interrupt(vector = N), exception-frame I/O, context_switch) remain VCS-specs domain.
time_ops.vr	partial	core-tests/sys/time_ops — Arithmetic API (SysTimeOpsDuration.from_*/as_*/zero) GREEN in both --interp and --aot. Clock API (SysTimeOpsInstant.now/elapsed/duration_since) GREEN post-fix. Task #5 CLOSED in commit 51ecc3bc9 — fundamental architectural fix: replaced the hardcoded dependency-graph HashMap in core_compiler.rs with augment_dependencies_from_mounts — a regex-based mount scan that auto-derives the implied module dep edges from every stdlib .vr file's mount <path> declarations. A FOUNDATION_DEPS_TO_FORCE const force-orders core.intrinsics + core.intrinsics.runtime before their 20+ consumers (sys/base/mem/async/io/text/runtime/net/sync subdirs). The fix transitively closes the panic-stub class across the entire stdlib — every @intrinsic-decorated raw-syscall declaration is now reliably visible to its consumers' mount-resolution path at codegen time. 2 residual defects: §C Child.read_stdout silent-empty data-loss (separate stub-body class); §D wall_clock_ms() returns < post-2000 ms (runtime SystemTime dispatch — exposed by §A close, distinct defect).
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. Task #FUNDAMENTAL-SYS-RAW CLOSED in this branch — 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. Task #FUNDAMENTAL-SYS-RAW CLOSED — same architectural fix as file_ops. Live socket round-trip deferred (needs fixture pair).
process_ops.vr	partial	core-tests/sys/process_ops — ProcessExitStatus.success ↔ code==0 + Child invalid-fd short-circuit + args/arg_count coherence pinned. Task #FUNDAMENTAL-SYS-RAW CLOSED — same architectural fix. spawn / run happy path deferred (needs CI-portable fixture).
process_native.vr	partial	core-tests/sys/process_native — 8 unit + 6 property + 6 integration + 2 regression tests. 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=256 + tls_set/get round-trip + context_provide/get/end DI scope + defer_depth tracking pinned end-to-end. Two fundamental fixes landed in this branch: (a) Task #FUNDAMENTAL-SYS-RAW — replaced stale mount super.raw.* with canonical mount core.intrinsics.runtime.os.{__ctx_*_raw, __defer_*_raw}; (b) Task #FUNDAMENTAL-CTX-INTRINSICS — wired interpreter __ctx_get_raw / __ctx_provide_raw / __ctx_end_raw / __defer_*_raw to the real state.context_stack + new state.defer_stack (pre-fix every TLS/DI/defer raw intrinsic returned constant 0/nil; the interpreter's existing ContextStack opcode-level wiring at 0xB0/0xB1/0xB2 was correct but the raw-function dispatch arm was completely inert). defer_execute callback invocation deferred to Tier-1 (interpreter can't synthesise indirect fn(Int)->Int dispatch).
signal.vr	regression-only	core-tests/sys/signal — 14/52 green. Pre-existing stdlib defects in Signal: variant-tag drift on @cfg-aware match arms, atomic_load/atomic_store intrinsic registration missing for SignalFlag. Architectural — drift is in stdlib Signal implementation, not test infrastructure.
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() / .watch() / event-stream surface deferred (needs per-platform fixture).
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 Shared/Exclusive (#160 rename from LockKind to avoid SQLite VFS shadow) + LockRegion start/length with -1 EOF sentinel + LockError Conflict(Maybe<Int>)/IoError(OSError) variant payload shapes pinned. Integration suite adds exhaustive 2-variant dispatch + LockRegion "spans EOF" predicate + LockError.Conflict dispatch table funnelling through a custom 3-state ErrorOutcome ADT + LockRegion overlap classification with EOF-as-+∞ semantics. Round-16 extension 2026-05-28: +11 algebraic laws for LockRegion constructors (.new/.to_eof/.byte) + .overlaps predicate (reflexive / symmetric / disjoint / overlapping / adjacent-exclusive / EOF-as-+∞ / single-byte overlaps single-point). try_lock / unlock live round-trip deferred (needs 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	complete	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 (2026-06-01). 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	complete	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 — 22u + 5p + 6i + 5r (full triad, 2026-06-01). MapType ADT (30 variants matching enum bpf_map_type) with exhaustive discriminant-injectivity law (total match → Int dense over [0,30), ordinal-ordered wire-tag pin); MapConfig boundary round-trip; per-variant MapDescriptor preservation; create_map Result shape + value-buffer geometry + per-class count + Maybe lift; D6/field-drift/high-ordinal regressions. bpf() syscall CRUD deferred to Linux runner. AOT umbrella resolution unblocked by D1 (see below).
linux/bpf/program	partial	core-tests/sys/linux/bpf/program — 27u + 6p + 8i + 6r (full triad, 2026-06-01). EXHAUSTIVE discriminant injectivity over ALL 32 ProgramType + ALL 40 AttachType variants (dense, ordinal-ordered — the source declares 40 AttachType, not the 39 an earlier note claimed); ProgramBytecode / ProgramDescriptor / Link round-trip (link.fd != link.program_fd; GPL + dual BSD/GPL license); load Result shape with verifier/EPERM paths + attach-point compatibility + Link bookkeeping; D6 + 3-field no-drift + ordinal-39/31 dispatch regressions. load_program / attach_* deferred to Linux runner.
linux/bpf/mod	partial	core-tests/sys/linux/bpf/mod — 9u + 6p + 3i + 4r (full triad, 2026-06-01). Umbrella-only surface laws (every re-exported name constructs / dispatches / round-trips via the umbrella path ALONE) + whole XDP-firewall assembly (program + LPM-trie map + link) + D1 umbrella-resolution + D6 regressions. Function re-exports (load_program / attach_* / create_map / map_*) deferred to Linux runner; their AOT umbrella resolution is unblocked by D1.
windows/ntstatus	complete	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	partial	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	partial	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	partial	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	partial	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	partial	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	partial	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	partial	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	complete	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 — 19 unit + 13 property + 8 integration + 4 regression tests. 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	complete	core-tests/sys/no_runtime — 18 unit + 13 property + 8 integration + 4 regression tests. 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 — 17 unit + 10 property + 8 integration + 4 regression tests. 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 as of 2026-05-27 — the cross-module free-function dispatch defect was closed by task #121 (see core-tests/sys/bitfield/audit.md §3.2). 56 unit + 31 property + 22 integration + 3 regression tests are all green under --interp.

AOT (2026-06-01): 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 returns Unit/nil at --interp runtime — affects every mount X.{free_fn} and module.fn(args) call site (workspace-wide; core.base.glob.matches exhibits the same shape).	closed in task #121
2	mount X.{public_const} does not register the name in the codegen's global symbol table; cross-module imports of public const items report UndefinedVariable("CONST_NAME") at codegen. Workaround: mount X; X.CONST.	partial — bare-mount form mount X.Y.Z; Z.CONST closed; selective mount X.{CONST} form still falls through (task #15)
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 eager-compile path surfaces [VBC codegen error (user bodies)] undefined variable: <VariantName> for every stdlib function that returns a bare-name variant in expression position (e.g. resolution_for in core/database/sqlite/native/vfs_xcurrenttime_api/clock.vr). Same defect class as 8f0ee3d6 (qualify Maybe.Some/None across 8 collection files). Workaround: source-level qualification (Resolution.RsSeconds etc.) per call site.	tracked — multi-day codegen surface (compile_function should propagate declared return-type into expression-position variant lookup; the WRITE-site at register_impl_function already does this for Self → concrete substitution per the 2026-05-27 fix).

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

type AccessMode is Volatile | Sync | Relaxed;

type Register<T, const ADDR: UInt64> is { mode: AccessMode };
type MemoryRegion is { base: *mut Byte, length: Int, cacheable: Bool };

fn volatile_load<T>(addr: UInt64) -> T
fn volatile_store<T>(addr: UInt64, value: T)
fn barrier(order: MemoryOrdering)
fn dmb()                                        // data memory barrier (arm64)
fn dsb()                                        // data sync barrier
fn isb()                                        // instruction sync barrier

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
    | IoError(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.