Read what runs

Lim has explicit types, named call arguments, visible control flow, and explicit returns. Arithmetic names its type and overflow behavior. Builtins begin with #; your declarations use ordinary names. A small surface notation makes handwritten code lighter while reducing to the same parenthesized trees that code generators manipulate.

#fn add {
  #params = { left = #u64; right = #u64; };
  #returns = #u64;
  #body: #return [#u64 #wrap; left + right];
}

#fn main {
  #params = {};
  #returns = #u64;
  #body: #return add { left = 40; right = 2; };
}

The result is the process exit status, 42. Braces contain named pairs; the colon groups the rest of its line; brackets contain typed infix arithmetic. The tutorial develops these rules step by step.

Why a new language?

Generated programs still need human review. Following a call becomes harder when its meaning depends on implicit conversions, receiver lookup, hidden cleanup, or distant generic instantiations. Lim explores a deliberately smaller design: make those decisions visible in source, give generators a simple tree to produce, and check ownership and API requirements before emitting code.

The goal is to shorten the path from an idea to code you can understand and run. The name evokes a limit as time approaches zero: less waiting to build, less overhead to execute, less time reconstructing intent. These are engineering targets, not benchmark results or a claim that Lim replaces established languages for every project. Lim is experimental and unreleased; syntax, semantics, backend coverage, and tooling can still change.

Why these design choices?

What the compiler checks

Ownership and borrowing checks track moves, exclusive access, returned references and retained loans across functions, without user-written lifetime annotations. Linear values need explicit consumption; destruction is visible rather than silently inserted. Raw pointers and unsafe operations have an explicit boundary and still need an audit. These checks target specific classes of mistakes; they do not establish that every program is correct.

Predicate contracts let an API say what evidence a caller must supply. A #if-valid branch runs a predicate and makes that exact fact available in its true branch. #requires, #ensures and #preserves make function boundaries explicit; mutations invalidate facts that depend on changed storage. There is no automatic theorem search. Programmer-written promises in #ensures and #preserves, and assertions through #assume, are trust boundaries. Optional runtime contract audits check exercised paths; they are not mathematical proofs. See the contract tutorial and verification notes.

Read, try, build

• Start with the tutorial, then use the language reference for precise rules and builtin forms.
• Open the browser playground to edit and compile toy examples locally. Only the playground loads JavaScript and the compiler; this handbook requires neither. Runnable browser programs currently use a scalar subset; browser support and limits describe the boundary.
• From a repository checkout, build and run the native example:

nix develop
cargo build --release
./target/release/lim docs/answer.lim -o answer
./answer
# Exit status: 42

The complete handbook is this page. Use Ctrl+F / Cmd+F for a keyword or error code, or save the HTML file for offline reading. Nothing is hidden in collapsed panels.

1. Return a value

This entire program returns 42:

#fn main {
  #params = {};
  #returns = #u64;
  #body: #return 42;
}

#fn declares a function. #params is a record of parameter names and types; this function has none. #returns is always explicit. #body contains the function’s forms. #u64 is an unsigned 64-bit integer. An unsuffixed literal gets its type from this explicitly declared context; 42u64 spells it directly.

For a function that returns no value, use #returns = (); and #return ();. Empty #requires, #ensures and #preserves fields may be omitted.

Run this natively from a checkout:

nix develop
cargo build
./target/debug/lim example.lim -o /tmp/example
/tmp/example
echo $?  # 42: the program's exit status, not printed output

The playground displays the returned value directly. Native exit statuses are limited by the operating system; returning a number is different from printing.

2. Read the tree beneath the sugar

Each surface form has a local, mechanical interpretation:

Inline colons consume through a newline, semicolon, or enclosing closing delimiter. Consecutive colons nest to the right. Semicolons inside explicit parentheses or an indented group belong to that group. Use spaces for layout.

Curly braces contain only key = value; entries, with key: available when the value is colon-grouped. Parentheses delimit ordinary forms; square brackets select infix parsing. Nested square brackets inherit their arithmetic header only through direct bracket nesting. A function-call parenthesis ends that inheritance, so brackets inside the call need their own header.

Canonical S-expressions remain useful for generators and fully explicit code:

(#fn main () #u64
  (#return (#u64::add-wrap 40u64 2u64)))

3. Declare and call a function

Calls name their arguments. Their written order can differ from the declaration; expressions are evaluated once, in parameter declaration order.

#fn subtract {
  #params = { left = #u64; right = #u64; };
  #returns = #u64;
  #body: #return [#u64 #wrap; left - right];
}

#fn main {
  #params = {};
  #returns = #u64;
  #body: #return subtract { right = 2; left = 44; };
}

#wrap states overflow behavior. Integer arithmetic must choose the required wrapping or saturation behavior explicitly; comparisons use a type header without an arithmetic mode, such as [#u64; value < 100].

#call remains a canonical form understood by the compiler and generators. Handwritten code can call an ordinary function with its name and an argument record. Functions are free-standing declarations; there is no method lookup.

4. Mutate a local and write a loop

#let binds an immutable value. #let-mut permits assignment with #set. A range is half-open: 1 through 11 means the numbers 1 through 10.

#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let-mut total #u64 0;
    #for-range (number #u64) 1 11:
      #set total [#u64 #wrap; total + number];
    #return total;
}

The loop’s colon opens its body. Dedent closes it; the final return belongs to the function. #while, #for and #loop cover other iteration shapes. #break exits a loop; #continue starts its next iteration. In a #for loop, continuing still executes the step. Names cannot shadow existing bindings.

For actual printed output, see the working 1-through-10 native printing example. The browser’s initial scalar backend reports return values instead of host I/O.

5. Validate an API argument once

A predicate is an ordinary pure Boolean function. A function that requires it can be called only where the checker already has matching evidence.

#fn positive {
  #params = { value = #u64; };
  #returns = #bool;
  #body: #return [#u64; value > 0];
}

#fn accept {
  #params = { value = #u64; };
  #returns = #u64;
  #requires: positive { value = value; };
  #ensures: positive { value = (#result); };
  #body: #return value;
}

#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let input #u64 42;
    #return (#if-valid positive { value = input; }
      accept { value = input; }
      0u64);
}

#if-valid runs the predicate. Its successful branch carries the evidence into the call. Ordinary #if does not grant this evidence. Removing the validation branch makes the call fail to check, even though this particular literal is 42. The checker follows explicit claims; it does not unfold predicates or solve arithmetic implications.

Use --check-contracts when testing native programs. It audits requirements, postconditions and preservation, but does not prove a programmer’s promise for all inputs. Production can omit these extra audits. The playground enables them.

6. Borrow storage explicitly

A mutable reference grants exclusive access. End it before using the owner again:

(#fn main () #u64
  (#let-mut number #u64 40u64)
  (#let view (#ref-mut #u64) (#borrow-mut number))
  (#deref-set view 42u64)
  (#forget view)
  (#return number))

#forget explicitly consumes this handle. Ownership and borrow checking remain active inside #unsafe. Linear values must be consumed; Copy values may be reused. Destruction is explicit. Returned references retain the source storage’s lifetime obligations.

Evidence is tied to the storage read by a predicate. A relevant write can revoke a temporary fact. Fixed constraints in stored types must instead be restored before an exclusive borrow returns access to the owner. See constrained types for the detailed restoration rules. A valid property of an unrelated field can remain available.

This example can use Check only in the browser; reference code generation currently belongs to the native backend.

7. Prove an array index

This checks the exact comparison needed by the access, then uses its evidence:

(#fn main () #u64
  (#let items (#array #u64 2)
    (#array-of (#array #u64 2) 20u64 42u64))
  (#let view (#ref (#array #u64 2)) (#borrow items))
  (#let index #usize 1usize)
  (#return (#if-valid (#usize::lt index 2usize)
    (#index-proven view index)
    0u64)))

The index must be #usize, and the comparison must mention this index and this array length. A fact about another index or bound does not match. A named validator with the same implementation is still a distinct predicate.

To connect claims, call an ordinary helper with explicit #requires and #ensures. The generated fixed-array API supplies such a helper. The checker does not discover the conversion on its own. Proven access omits the bounds check in production; instrumented compilation audits the access. This example is available through Check only in the browser.

8. Generate a concrete type

Generators produce concrete declarations instead of hidden runtime dispatch:

(#generate #optional ((type #u64) (name MaybeNumber)))
(#fn main () #u64
  (#let value MaybeNumber
    (#call MaybeNumber::construct ((value 42u64))))
  (#return (#match value
    (#case (MaybeNumber.Some number) number)
    (#case MaybeNumber.None 0u64))))

Generated source is inspectable in .lim/generated/. Builtin and library generators use reserved names such as #optional; user generators use ordinary names. The pure generator language uses #gn, #gn-fn and the restricted #gn-* operations. All emitted runtime code still passes ordinary validation.

Use the generator reference for syntax bundles, quoting, generated declarations, validation witnesses and file authority. Generating a type does not make it an opaque mathematical proof.

9. Follow a diagnostic

The compiler distinguishes parsing, generation, types, borrows, linearity, unsafe use, contracts, code generation and linking. A failed check gives a source location and, where available, related locations.

#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let answer #u64 false;
    #return answer;
}

Here the declared type is #u64 and the value is #bool. Change false to 42. For contract errors, first compare the required predicate and argument identities with the available evidence. For borrow errors, inspect which owner or reference still has access. For unsupported WebAssembly code generation, use Check only or run the example natively.

10. Keep the compiler stages in view

Surface syntax changes how a tree is written. Generators change which concrete program is checked. Type, ownership, borrow and contract checking decide whether that program is accepted. A backend then emits code for its supported operations. An unsupported backend feature is an error, not permission to skip validation.

The rest of this page is the full language reference. Its examples are checked against the native compiler. The WebAssembly notes describe the smaller runnable browser subset, build command and versioned compiler interface.

Design and scope

#fn increment {
  #params = { value = #u64; };
  #returns = #u64;
  #requires:
    [#u64; value < 99];
  #ensures:
    [#u64; (#result) < 100];
  #body:
    #return [#u64 #wrap; value + 1];
}
#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let input #u64 41;
    #return (#if-valid [#u64; input < 99]
      (increment { value = input; })
      0u64);
}

#fn main {
  #params = {};
  #returns = #u64;
  #body: #return : #u64::add-wrap 20u64 22u64;
}

Shared allocator state and cells

Dynamic allocation follows the concrete allocator ABI in allocator.md. Allocator values are passed explicitly and generated collections retain an immutable allocator reference; interior mutability belongs to the allocator implementation.

#generate #cell is a standard-library generator in library/cell.lim, not a builtin type. Each invocation explicitly names the concrete type and three free-standing functions. It currently accepts the integer widths supported by #atomic (#i8/#i16/#i32/#i64, #u8/#u16/#u32/#u64, and #usize); it does not support floats, pointers, or enums. The generated get/set functions take a shared reference to the concrete cell and never return a reference to its contents:

(#alias cell-generator = ../library/cell.lim::#cell)
(#generate cell-generator #u64 CellU64 CellU64::create CellU64::get CellU64::set)
(#struct Arena () ((cursor CellU64)))
(#fn advance ((cursor (#ref CellU64))) #u64
  (#let next #u64 (#u64::add-wrap
    (#call CellU64::get ((cell (#clone cursor)))) 1u64))
  (#call CellU64::set ((cell (#clone cursor)) (value next)))
  (#return next))

An aggregate that stores a reference retains a borrow of its owner for the rest of the containing function. It cannot be returned if that borrow points to a local, and reference-bearing fields cannot be replaced. Mutable references may be stored in structs and enum payloads; they retain an exclusive borrow of their source and cannot be cloned. The generated cell is linear, but its relaxed atomic storage makes it both Send and Sync. A read-modify-write sequence such as advance is not an atomic increment; use #atomic-fetch-add when multiple threads must update one counter.

For coordinated shared mutable state, use explicit atomic operations. The atomic API supports #i8/#i16/#i32/#i64, #u8/#u16/#u32/#u64, and #usize. Each operation uses the width's naturally aligned x86 memory access; Lim's current local and aggregate storage is at least eight-byte aligned:

(#let-mut counter (#atomic #u64) (#atomic-init #u64 0u64))
(#atomic-fetch-add (#borrow counter) 1u64 #memory-acq-rel)
(#let observed #u64 (#atomic-load (#borrow counter) #memory-acquire))
(#atomic-store (#borrow counter) observed #memory-release)

(#atomic-exchange reference desired #memory-order) replaces the value and returns the old scalar. Compare-exchange has these explicit forms:

(#atomic-compare-exchange reference expected desired #memory-acq-rel #memory-acquire)
(#atomic-compare-exchange-weak reference expected desired #memory-release #memory-relaxed)

Both return (#tuple #bool ScalarType): success followed by the observed old value. On failure memory is unchanged; the observed value can be used for an explicit retry. Expected and desired must match the atomic scalar. Success accepts every #memory-* order; failure accepts relaxed, acquire, or seq-cst, and cannot be stronger than success. In particular, release success permits only relaxed failure; acquire failure requires acquire, acq-rel, or seq-cst success. Release/acq-rel failure orders are invalid.

The x86-64 backend emits memory xchg for exchange (implicitly locked), and lock cmpxchg for both compare-exchange forms. Narrow observed values are sign- or zero-extended according to the scalar type. These instructions provide stronger hardware ordering than relaxed operations require. Weak compare-exchange is currently implemented without spurious failure; callers must still allow spurious failure for future backends. Atomic operations provide no scheduling fairness or starvation guarantee. See examples/atomic_claim.lim for two workers claiming the same state; both tasks are spawned before either is joined.

Loads accept #memory-relaxed, #memory-acquire, or #memory-seq-cst; stores accept #memory-relaxed, #memory-release, or #memory-seq-cst. Fetch-add accepts any of those plus #memory-acq-rel. Invalid order/operation combinations are compile-time errors. The native x86_64-sysv backend relies on aligned 8-bit, 16-bit, 32-bit, and 64-bit x86 atomic accesses; acquire and release loads/stores use x86 TSO ordering, seq-cst stores use an exchanging instruction, and read-modify-write uses a locked instruction. This API is not available for #i128 or #u128. Unsafe #send/#sync overrides remain the author's soundness promise and do not replace atomic operations.

Borrows of struct fields are tracked as places. While point.x is borrowed, an access to point.y is allowed, but an access to point.x or to the whole point is rejected. A field reference derived through a mutable reference temporarily suspends that parent reference; #drop releases the derived loan and restores the parent borrow.

Send and Sync properties

Send means a value may be transferred to another thread; Sync means a shared reference to the value may be used from another thread. The compiler derives both properties recursively for structs, enums, tuples, and arrays:

• Scalar types are Send + Sync.
• Raw pointers are neither Send nor Sync.
• Generated #generate #cell types use relaxed atomic storage and are Send + Sync for their supported integer widths.
• (#atomic T) is both Send and Sync only for the supported atomic integer widths listed below.
• (#ref T) is Send when T is Sync, and is Sync when T is Sync.
• (#ref-mut T) is Send when T is Send, and Sync when T is Sync.
• An aggregate has a property only when all of its stored fields/payloads have that property.

Unsafe native or opaque types may opt in explicitly:

(#struct NativeResource () ((handle (#ptr #u8))))
(#unsafe-impl #send NativeResource)
(#unsafe-impl #sync NativeResource)

These declarations are promises by the author and override the structural result for that property. They must only be used when the type's invariants make cross-thread transfer or shared access sound. Generic-type overrides are currently rejected; duplicate or undeclared targets are errors. The #generate #thread-spawn with ((task TaskType) (worker worker-function)) validates a monomorphic worker's parameter and return types against Send. It generates TaskType-spawn and TaskType-join functions and a private native thread entry point; user code never passes a function pointer. Spawn arguments are copied into a private task packet before the worker starts. Scalar and aggregate arguments/results use the compiler's native calling convention. Spawn returns TaskType-spawn-result: TaskType-spawn-ok carries the opaque task handle and TaskType-spawn-error carries an allocation or thread-creation error. Join returns TaskType-join-result: TaskType-join-ok carries the worker result; TaskType-join-error carries the still-owned task handle and native error code. This distinguishes runtime failure from valid zero-valued results and allows the caller to retry a failed join. A failed join does not release captured borrows or free the task packet.

On the Linux x86-64 backend, generated threads use direct kernel calls, not libc or pthreads. mmap reserves a stack and task packet; mprotect leaves the bottom page inaccessible. The compiler sizes each worker's stack from its emitted call graph, rounded to pages with a 64-KiB minimum and allowances for the entry trampoline and red zone. An unknown or unbounded worker call path is a compilation error rather than a guessed stack size.

The native clone trampoline starts execution on the new stack. The parent and child share a kernel-managed TID word: parent-TID publication avoids an immediate-exit race, and child-TID clearing wakes a shared futex after exit. Join waits for that clearing before copying the result and unmapping the stack/packet. EINTR and EAGAIN retry internally; other futex errors retain the task handle in the join-error result. Allocation/protection and creation failures keep the existing distinct spawn-error variants. See the Linux clone contract and clear-child-TID contract.

Workers have no libc TLS: their FS base is explicitly zero, and reachable foreign or indirect callees are rejected, including calls through Lim helper functions. Explicit FFI outside worker call graphs remains available. Unsafe worker assembly must obey the same no-foreign-runtime and stack contracts; it must not terminate the thread early or change its clear-child-TID address. Installing custom signal handlers is also an unsafe responsibility: block their signals before spawning, arrange a worker-owned alternate signal stack, then unblock them. The computed Lim stack bound does not cover arbitrary signal-handler frames. The backend provides no pthread cancellation or TLS destructor behavior.

examples/kernel_threads.lim exercises concurrent parent/worker progress, shared PID/distinct TIDs, the worker TLS boundary, repeated joining, and stdout. tests/kernel_threads.rs checks static ELF linkage, argument/result layouts, nested workers, large stack frames, and an actual guard-page fault. Its opt-in ptrace tests also verify kernel calls and inject spawn/join failures.

For inspection, (#generate #thread-spawn ((task TaskType) (worker worker))) materializes in .lim/ as a #thread-task declaration containing explicit #thread-task-spawn and #thread-task-join builtin signatures, followed by #enum declarations for their results. The spawn signature exposes TaskType-spawn; its result enum contains TaskType-spawn-ok and TaskType-spawn-error. The join signature exposes TaskType-join, and its result enum contains TaskType-join-ok and TaskType-join-error. The compiler validates and reuses matching signatures and enums rather than synthesizing duplicates.

Task handles are affine: match spawn results, and join each successful task handle exactly once. The join error arm must retain or retry the returned handle; discarding either generated result is rejected. References captured by a worker remain borrowed until a successful join; shared captures require Sync, mutable captures exclude parent access until join. These restrictions are checked statically. Unsafe #send/#sync overrides are promises, not synchronization: the author must ensure the underlying resource remains sound under concurrent access.

Inferred lexical borrows

Lim's initial borrow model checks lexical borrow scopes without lifetime annotations. A shared borrow is written as:

(#borrow value (#u64::add-wrap value 2))

and a mutable borrow as:

(#borrow-mut value (#block (#set value 42) value))

The three-expression form borrows the owner for the duration of the body. The two-expression form produces a reference:

(#fn first ((value (#ref #u64))) (#ref #u64)
  (#return value))

Multiple shared borrows may overlap, but a mutable borrow cannot overlap any other borrow, and a shared borrow cannot overlap a mutation. References to locals cannot escape their function; incoming reference referents and globals may be returned. A by-value parameter's own storage is local too: returning (#borrow parameter) is invalid even if the parameter itself contains references. Loading one of those incoming references preserves its external referent instead. #deref reads through a reference, and #deref-set writes through a mutable reference when the target fits the native value registers. The known target type is used for aggregate RHS values, including one-word structs. Writing a zero-sized aggregate evaluates both operands but writes no bytes. A field reference can be derived from a named reference to a struct with (#borrow (#get reference field)) or #borrow-mut for an exclusive field reference. The derived reference retains the original referent's borrow: it cannot escape when that referent is local, and a mutable parent reference is suspended while its derived field reference remains live. Tuple and array projections use #get and #index; enum payload fields use (#get-payload reference Variant index). Each variant has zero or one payload. Use a named struct as the payload when a variant needs multiple fields. Projections may also start at an owned local, without borrowing the entire aggregate first: (#borrow (#get owner field)). Nested struct, tuple, array, and enum-payload projections address the original storage; a dynamic index is evaluated once before the borrow's body. Mutable borrowing requires a mutable local or an exclusive reference root. The same rules apply to #pin-borrow and #pin-borrow-mut, and reborrowing through a pinned reference preserves pinning. A projection cannot borrow a computed aggregate temporary. When crossing a reference-valued field, bind that reference first so the next borrow has an explicit reference root. See examples/owned_field_borrow.lim.

Reference-valued fields may be projected through nested aggregates; their original source borrow remains active for as long as the containing aggregate is live.

(#struct Point () ((x #u64) (y #u64)))
(#fn main () #u64
  (#let-mut point Point (#struct-literal Point ((x 1) (y 2))))
  (#let point-ref (#ref-mut Point) (#borrow-mut point))
  (#let y-ref (#ref-mut #u64) (#borrow-mut (#get point-ref y)))
  (#deref-set y-ref 42)
  (#return (#deref y-ref)))

Raw pointers and unsafe blocks

Raw pointers are explicit and distinct from references. (#ptr T) is an immutable raw pointer and (#ptr-mut T) is a mutable raw pointer. Taking an address and reading or writing through a raw pointer must occur inside an #unsafe block:

(#fn main () #u64
  (#let-mut value #u64 40)
  (#return
    (#unsafe
      (#block
        (#let pointer (#ptr-mut #u64) (#addr-of-mut value))
        (#ptr-write pointer 42)
        (#ptr-read pointer)))))

Functions with caller safety obligations use #unsafe-fn instead of #fn. Their signatures otherwise have the same shape. Every call uses #unsafe-call inside #unsafe, including calls from another unsafe function. #call rejects unsafe functions even inside #unsafe, and #unsafe-call rejects safe functions. The declaration does not make its body implicitly unsafe: raw operations and unsafe calls still need an explicit block.

(#unsafe-fn read-byte ((pointer (#ptr #u8))) #u8
  (#return (#unsafe (#ptr-read pointer))))
(#fn main () #u64
  (#let value #u8 42u8)
  (#return (#as (#unsafe
    (#unsafe-call read-byte ((pointer (#addr-of value))))) #u64)))

Imports and generated declarations preserve the calling requirement. Implicit entry points (main, aggregate clone hooks, and thread workers) must be safe; use a safe wrapper that explicitly discharges the unsafe function's obligations. Generator capability contracts currently describe safe operations, so an unsafe operation does not satisfy one. The Linux library uses this contract for all raw-pointer wrappers and integer-only APIs with hidden memory or execution-state obligations. Reference-bounded byte/time helpers remain safe. See the syscall caller contracts.

The operations are #addr-of, #addr-of-mut, #ptr-read, #ptr-write, and (#ptr-offset pointer element-index). (#ptr-null (#ptr-mut T)) or (#ptr-null (#ptr T)) constructs a typed null pointer; constructing one is safe, but dereferencing it is not. (#ptr-is-null pointer) safely tests whether a raw pointer is null without consuming it. (#ptr-address pointer) returns the machine address as #usize without dereferencing it; it can check Linux error-pointer returns before any access. The offset consumes a raw pointer and returns a pointer with the same mutability and pointee type; its index must be #usize. Offsets use the pointee's byte width (for example, *mut u8 advances one byte). Byte-offset multiplication and address addition are checked for overflow and trap on overflow. Reads and writes access only the pointee's width. Writing requires (#ptr-mut T). Reads and writes do not check allocation bounds, and raw-pointer operations are rejected outside #unsafe; callers must uphold pointer validity and bounds themselves. #ptr-borrow and #ptr-borrow-mut also require #unsafe; their first argument is a reference used as the inferred lifetime anchor, and the second is the pointer to the referenced value. The #pin-ptr-borrow variants require a pinned-reference anchor and preserve the pinned-reference type/provenance. The caller must ensure the pointer is valid, stable, and uniquely accessible as required for the full anchor lifetime. These forms do not make allocation or pointer validity safe by themselves.

Pinning is exposed through generated opaque objects rather than a special binding statement. Import library/pin.lim and declare a concrete API:

(#generate #pin ((type Frame) (name PinnedFrame) (fields ((value #u64)))))
(#generate #pin-scope ((type Frame) (pin PinnedFrame) (name with-pinned-frame)
  (run drive-frame) (destroy destroy-frame) (result #u64)))

#generate #pin emits opaque PinnedFrame and PinnedFrame::Shared handles, unsafe constructors, and PinnedFrame::Read::value / PinnedFrame::Write::value free functions (plus the shared reader). Field types are literal generator inputs; ordinary checking verifies them and rejects moving linear fields or replacing fields that do not satisfy the pinned-field restrictions. Optional copy true emits whole-value readers and a writer only after checking a structural Copy proof. All implementation functions are inspectable in the generated cache. For linear fields, projections ((child PinnedChild)) generates PinnedFrame::Project::child and PinnedFrame::ProjectMut::child, returning the existing concrete child pin handles without moving the field. Shared handles also get a shared projection. Projection consumes the parent handle; it does not leave a second mutable handle to the same storage. Derived handles retain their source's borrow and cannot outlive it. Unsafe PinnedFrame::into-view consumes a handle and exposes its low-level pinned reference for trusted implementations; it does not unpin or move the referent.

The same declarations also generate PinnedFrame::BorrowMut::child, taking ((pin (#ref-mut PinnedFrame))), and PinnedFrame::Borrow::child, taking ((pin (#ref PinnedFrame))). Shared wrappers have their own shared ::borrow function. These reborrow the child without consuming the parent handle. Disjoint mutable child fields can coexist, as can overlapping shared views; overlapping exclusive access is rejected at the offending call argument. Callee footprints follow the wrapper's actual pinned pointer slot, including helper calls and transferred child arguments, not just its stack address. Forgetting a wrapper does not unpin or destroy its referent: child views still retain that referent, and prevent scope escape or heap release. See examples/pin_projection_borrows.lim for two independently writable children.

with-pinned-frame takes value Frame, initializes private stack storage, and calls drive-frame with pin PinnedFrame. It then calls destroy-frame with a fresh pin handle before retiring that storage in place. The run function returns the specified result type; the destruction function returns unit. Both functions must consume their handles explicitly. The original storage is inaccessible to callbacks, even if they forget their handles. Returned borrows cannot escape the scope, and cancellation/resource cleanup must be implemented in the destruction callback. No function pointers, lambdas, #let-pin, or #pin-end are needed. See examples/stationary_pin.lim.

For an initialized local, (#pin local) creates an exclusive (#pin-ref-mut T) and requires a #let-mut binding. (#pin-shared local) creates a shared (#pin-ref T) and also accepts immutable locals. Neither accepts a temporary, projection, reference variable, top-level constant, or static: use #pin-borrow/#pin-borrow-mut for projection reborrows. Both local operations permanently freeze the original storage, including Copy locals. Forgetting the reference ends its loan, but does not allow moving or assigning the original local again. A branch that may pin a local also freezes it after the branch joins. Copy values can still be read or copied from frozen storage when normal loan rules permit: copying a Copy value does not move the storage itself. Whole-local assignment remains forbidden. Each new loop iteration initializes fresh local storage; explicitly end the previous iteration's local after its views end.

(#struct LocalJob (#linear) ((state #u64)))

(#fn main () #u64
  (#let-mut job LocalJob (#struct-literal LocalJob ((state 0u64))))
  (#let view (#pin-ref-mut LocalJob) (#pin job))
  (#pin-set-field view state 42u64)
  (#let answer #u64 (#get view state))
  (#forget view)
  (#forget job)
  (#return answer))

Ordinary named functions can take pinned references, so multiple local pins can be selected and polled in branches without callbacks or generated wrappers. An ordinary reference does not satisfy a pinned-reference parameter. Local pins cannot escape their storage scope, and overlapping mutable loans are rejected. After all references end, explicit #forget owner ends the local in place; it is not a destructor and performs no resource cleanup. Perform any required in-place cleanup first. Local pinning does not change #pin-own: that heap owner remains movable because its allocation stays stationary.

Low-level pinned-reference operations remain compiler primitives for generated code and unsafe implementations. Ordinary #pin-borrow permanently prevents moving a linear local after its first pin, even after its last view is forgotten; explicit #forget/#drop ends that local's lifetime. Plain Copy referents retain short-lived borrow rules. Nonmoving Copy field operations on pinned linear locals remain allowed, subject to the existing field-loan checks.

(#pin-own T) is a linear, movable owner of stationary heap storage. Unsafe #pin-own-of pointer value initializes uniquely owned writable allocation storage using Lim's native value layout and adopts it; safe #pin-own-borrow and #pin-own-borrow-mut borrow the allocation identity, not the handle's address. Views remain valid across handle moves, aggregate moves, and function returns. An optional allocator-reference argument keeps the allocator borrowed for the entire view lifetime. Forgetting an owner leaks the allocation rather than moving, freeing, or unpinning its contents. In-place cleanup precedes unsafe #pin-release, which returns the pointer for deallocation. Retained views block release, including release in called helpers. Calls that obtain conflicting pointee access also reject retained views; a pure owner-forwarding function does not. The opaque owner generated by #generate #pin-box exposes native pinned references; its destruction callback accepts pin with type (#pin-ref-mut T) for in-place cleanup. Transferring an owning allocation to a thread requires retirement of its existing pointee views. The caller still guarantees validity, alignment, unique raw ownership, and retirement of untracked raw pointers. Reference-bearing and nested owning-pin pointees retain their contents' loans through owner moves, return summaries, and field projections. Allocating storage does not extend a referent's lifetime. Heap writes, including helper-call writes, update retained loans in the owning allocation. A definite write to one concrete field retires that field's old loan and records its replacement; uncertain writes and control-flow joins keep all possible referents. A reference already loaded from the old field remains an independent live loan. library/pin_box.lim defines the #generate #pin-box generator, which takes exactly the named options type, allocator, name, and destroy. allocator is a literal bundle root exposing ::State, ::Error, byte-pointer ::Allocation, safe ::allocate, and unsafe ::deallocate. Its private typed adapter converts the byte pointers. It generates an opaque named linear heap-owner type and create, shared-borrow, mutable-borrow, and destroy functions. Its borrow functions return native #pin-ref and #pin-ref-mut values. examples/pin_box.lim demonstrates moving a handle while a view stays live. For an owner Box, generated symbols include Box::CreateResult, Box::created, Box::allocation-failed, and Box::create / Box::borrow / Box::borrow-mut / Box::destroy.

library/pin_rc.lim defines #generate #pin-rc with the same named options and allocator bundle convention, and generates named linear reference-counted owners with create, clone, shared-borrow, mutable-borrow, and destroy functions. This Rc is single-threaded and is neither Send nor Sync; it has no weak-reference handles. Mutable borrowing is available only while the handle is the unique strong owner. Destroy every borrowed view before destroying a handle, because the final handle destruction runs the pointee destructor in place and releases the allocation. For an owner Shared, generated symbols include Shared::Allocation, Shared::CreateResult, Shared::MutResult, and Shared::create / Shared::clone / Shared::borrow / Shared::borrow-mut / Shared::destroy; enum cases include Shared::unique and Shared::Shared.

For an owner named PinnedFrameRc, a private adapter converts the bundle's (#ptr-mut #u8) success payload to a pointer to the generated PinnedFrameRc::Allocation control block. The generated functions pass that block's size and alignment to the allocator and deallocator. Both Box and Rc request only allocate and deallocate adapters; their bundles may omit grow. Destruction hooks are explicit safe functions taking ((allocator (#ref Root::State)) (pin (#pin-ref-mut Element))) and must perform explicit in-place cleanup. examples/pinned_box_async.lim and examples/pinned_rc_async.lim poll generated futures through these native pinned references, including after moving the owning handle.

An async function can initialize an owner containing an external reference after an await and retain it across later suspension. Its source remains borrowed through Pending; Ready or explicit state-specific cancellation must consume the owner before the source can be modified. Structural reference tracking includes references inside nested owning pins, not just inline fields. examples/async_heap_reference.lim demonstrates this case. It is not a frame-local self-reference: general delayed frame-owner initialization and named pinned poll-handle recycling remain separate checked-analysis work.

#pin-read and #pin-write are lower-level unsafe operations for compiler- generated pinned state machines. They access aggregate referents at their existing storage address. A read can duplicate a linear value, and a write can invalidate references derived from the pinned value; callers must prove exclusive access, preserve any displaced ownership they need, and ensure no derived references remain. Ordinary code should use safe field operations instead; safe code cannot replace a pinned referent.

For a pinned handle proven to address one whole owned local value, the compiler tracks a linear #pin-read as a move: the original value's cleanup obligation is satisfied, and repeated loads, alias reads, and reborrows of that uninitialized storage are rejected. A matching #pin-write requires prior consumption before replacing a linear value and restores its cleanup obligation. The loaded value keeps its own retained reference slots, not the container address. Moving a reference-bearing holder transfers its loans; copying one retains both sets until the corresponding values are released. See examples/pinned_local_move.lim for local move/restoration and returning a loaded reference-bearing value from a branch-local holder.

For #deref-set and unsafe #pin-write, a destination proven to be one whole owned local value retains the RHS's reference fields and their original referent loans. Replacing a holder releases its previous stored loans; moving an exclusive-reference holder transfers its loans and keeps derived-reference parents suspended until the restored holder is consumed. Shared copies keep their respective loans. A local reference cannot be stored in external storage or survive its referent's scope, even when the write is indirect. See examples/borrowed_variant.lim and examples/pinned_holder_restore.lim. This whole-local registration rule does not enable projected, ambiguous, parameter, global, or lifetime-only destinations.

Whole ordinary #deref loads from borrowed parameters preserve the retained reference fields of the loaded value. Each field remains tied to its original input slot through function returns and caller substitution, rather than to the address of the container. A shared container cannot grant exclusive access through a stored mutable reference. See examples/borrowed_whole_load.lim. Parameter #pin-read loads preserve those retained value slots as well; see examples/pinned_parameter_load.lim. This provenance rule does not supply a complete parameter move/restore contract or prove variant-conditioned async frame accesses. The operation remains unsafe.

This local rule does not establish complete contracts for parameter-loaded frames, projected/ambiguous storage, or lifetime-anchored raw pointers. Those unsafe protocols still require the caller's guarantees; full referent and variant-conditioned async ownership analysis remains under development.

#pin-set-field is the checked field-wise operation for scalar/fieldless-enum and shared-reference struct fields. It writes only that field, so a state tag can change independently and an immutable reference can be established after the struct is pinned without moving the referent. The borrow checker tracks the stored reference as part of the owner: it rejects overlapping field replacement and keeps the owner pinned and borrowed until the reference field is cleared. This operation is not a way to make a movable async frame self-referential; generated frames still need stable storage slots and cancellation-aware internal-loan handling.

Ordinary calls also check statically resolved internal owner loans against the callee's writes and destructive accesses, including nested calls and paths that trap instead of returning. A disjoint field update is allowed; overwriting the internally borrowed field reports E4100 at the caller's argument and labels the callee access. Checked enum tests and assertions retain entry-tag constraints for conditional initialization, rather than treating a tag written by the initializer as an incoming constructor. See examples/pinned_self_reference.lim for an ordinary-call example. This additional rejection check is not permission to reborrow a whole parent while its children remain live. Context-sensitive exclusive loans in conditional enum payloads still require incoming/fresh-family correlation and remain subject to the existing conservative borrow checks.

#asm embeds target assembler at an expression site. Its form is (#asm ResultType ((register value) ...) "instructions"): each value is evaluated and loaded into its named 64-bit general-purpose register, and the result is read from rax (or discarded for ()). The current backend uses GNU Intel-syntax x86-64 assembly. #asm is unsafe and must be inside #unsafe. The assembly must leave rsp and rbp unchanged, must not return or jump out of the surrounding function, and must obey the platform ABI for any registers it changes; the compiler preserves callee-saved GPRs but cannot verify raw instructions. Syscall numbers and register conventions are OS/architecture specific, so select implementations with #cfg rather than assuming one assembly sequence is portable.

For Linux x86-64 kernel entry without hand-written register shuffling, unsafe #linux-syscall takes an explicit result type, syscall number, and up to six arguments. It emits the syscall instruction directly; no libc wrapper is called. Integer arguments are passed as machine words, raw pointers as-is, and Lim references have their internal low-bit tag removed before being passed as addresses. Raw syscall failures are returned as negative errno values. The primitive is deliberately unsafe because the kernel interprets syscall numbers, flags, descriptors, and pointer/length pairs according to Linux ABI contracts.

(#fn process-id () #i64
  (#return (#unsafe (#linux-syscall #i64 39usize ()))))

library/linux_x86_64.lim builds byte input/output, process helpers, and file-descriptor operations (openat, positional and sequential IO, metadata, directory queries, resource limits and usage, advice, locking, allocation, descriptor duplication, anonymous files, wall-clock/process-time queries, and private futex operations) on this primitive. The low-level pointer wrappers do not validate kernel buffer ranges; callers must uphold pointer validity and length preconditions. These wrappers are #unsafe-fn: the compiler requires #unsafe-call inside #unsafe, even for null pointers or zero-length buffers. Safe reference-bounded helpers use #call. For example, this unsafe forwarding function passes its caller's buffer contract through to the low-level read wrapper:

(#alias linux-read = ../library/linux_x86_64.lim::linux-read)
(#unsafe-fn read-buffer ((fd #i64) (destination (#ptr-mut #u8)) (count #usize)) #i64
  (#return (#unsafe
    (#unsafe-call linux-read ((fd fd) (destination destination) (count count))))))

The raw syscall operation remains available for the rest of the Linux syscall table. examples/linux_syscalls.lim and examples/linux_sockets.lim exercise direct socket syscalls, while examples/linux_socket_listener.lim binds an automatically named abstract UNIX socket, listens, connects, and exchanges bytes through both accept and accept4. It checks returned peer addresses, nonblocking and close-on-exec flags, empty accept queues, invalid arguments, and exact stdout; examples/linux_socket_messages.lim transfers datagrams with sendmsg, recvmsg, sendmmsg, and recvmmsg, checks each batched message length, and verifies nonblocking empty-queue errors and exact received output; examples/linux_select.lim checks select and raw pselect6 readiness before and after draining an eventfd, validates the kernel signal-mask argument size, and exercises legacy epoll/inotify descriptor creation; examples/linux_shared_memory.lim creates a private System V segment with shmget, checks shared bytes through writable and read-only shmat attachments, marks it for removal with shmctl, and verifies destruction after the last shmdt; examples/linux_message_queue.lim creates a private queue with msgget, sends typed messages with msgsnd, verifies msgrcv type selection and buffer-size/empty-queue errors, removes the queue with msgctl, and checks the received payloads through exact stdout; examples/linux_semaphores.lim creates and removes a private semaphore set with semget/semctl, verifies atomic semop failure without partial changes, and exercises successful and expired semtimedop calls; examples/linux_posix_mq.lim exercises mq_open, mq_unlink, mq_timedsend, mq_timedreceive, mq_getsetattr, and mq_notify. It immediately unlinks its unique queue, verifies priority ordering, oversized-message rejection, queue counts, expired deadlines, nonblocking mode changes, and exclusive SIGEV_NONE notification registration. It also blocks SIGUSR1 and verifies actual SIGEV_SIGNAL delivery, the SI_MESGQ code, sender PID/UID, and notification payload, then checks one-shot delivery, rearming, cancellation, and restoration of the original signal mask. Exact stdout checks both the received messages and the notification payload; see mq_notify(3). Raw queue names omit the leading slash required by libc, deadlines are absolute CLOCK_REALTIME values, and descriptors close with linux-close; see mq_open(3). examples/linux_robust_futex.lim registers and queries a robust-futex list, restores the original thread registration, and checks invalid sizes, missing threads, and invalid output pointers. A child then exits while owning a futex in shared memory; the parent verifies that Linux clears its owner ID and sets FUTEX_OWNER_DIED. A second owner is held behind a pipe while a waiter blocks directly on its robust futex. A second run blocks on a staging word and moves that waiter to the robust futex with FUTEX_CMP_REQUEUE before the owner exits. The controller checks each child's /proc/PID/wchan for a futex wait before releasing the owner, rather than guessing readiness with a sleep. This test requires readable procfs wait symbols; see proc_pid_wchan(5). The waiter requires a successful wake and verifies both owner-death and waiters bits before printing W; the parent reaps both children and prints R. The requeue wrapper uses an explicit #u32 count in the fourth syscall argument, rather than pretending it is a timeout pointer. The example tests an empty requeue, an expected-value mismatch, and successful blocked requeue cleanup on the supported host. See FUTEX_CMP_REQUEUE(2). These raw registrations require the caller to keep the list storage valid until replacement or thread exit; see get_robust_list(2). examples/linux_process_vectors.lim transfers bytes within its own address space using process_vm_readv and process_vm_writev, then through a pipe using vmsplice, checking byte counts, error paths, and exact payload output; examples/linux_mseal.lim exercises linux-mseal, whose flags are #usize (Linux unsigned long). It verifies invalid inputs, page rounding, idempotence, and rejected permission changes, discard, and unmapping while preserving the payload. Sealed mappings cannot be unsealed; this example's page is released only when its process exits. See the kernel mseal documentation. examples/linux_secret_memory.lim exercises linux-memfd-secret with #u32 flags. It verifies O_CLOEXEC (524288, not MFD_CLOEXEC), initial sizing, rejected resizing, shared mappings, and rejected process_vm_readv access. Mappings remain usable after descriptor close. The example deliberately copies its synthetic test bytes into ordinary memory for stdout, then unmaps all storage. Kernel secret-memory support and sufficient locked-memory allowance are required; unsupported hosts do not count as passing. See memfd_secret(2). examples/linux_io_uring.lim uses linux-io-uring-setup, linux-io-uring-enter, and linux-io-uring-register without liburing. The wrappers expose raw kernel layouts and results: callers must keep rings, registered resources, and request buffers valid until operations finish. The example follows kernel-provided offsets, exercises single/separate ring mappings, and uses explicit x86-64 fences when publishing or consuming entries. It repeatedly writes and reads a registered anonymous file after closing its ordinary descriptor, checks completion cookies/results/flags and reused slots, and verifies invalid setup flags, enter flags, opcodes, and file indices. All resources are released after completion. Exact stdout comes from read buffers. Kernel io_uring support and permission are required; no skip is counted as success. See io_uring_setup(2) and the kernel ABI header. examples/linux_aio.lim exercises native io_setup, io_submit, io_getevents, io_pgetevents, io_cancel, and io_destroy without libaio. It writes and reads a memfd, checks completion cookies, the request pointer, byte counts, empty-queue behavior, and invalid requests, then prints the read payload. It also cancels a pending eventfd poll, drains its completion, rejects a second cancellation, and checks the packed signal-mask argument to io_pgetevents, including mask restoration and invalid sizes. Modern Linux returns -EINPROGRESS when cancellation is accepted and posts the completion to the queue; the legacy io_cancel output pointer is unused. An accepted cancellation does not itself permit freeing request storage; drain its completion first. This follows the kernel AIO implementation. These raw APIs require a zero-initialized context output for setup and native iocb/io_event layouts; request and data storage must remain valid until completion. See io_submit(2). examples/linux_process_control.lim exercises prctl thread-name changes and restoration, arch_prctl FS/GS queries, and capget/capset capability version negotiation and unchanged-set round trips, with exact name output; examples/linux_identity.lim exercises setuid, setgid, setreuid, setregid, setresuid, setresgid, setfsuid, and setfsgid by reapplying current IDs or using unchanged-ID sentinels. It compares all real, effective, saved, and filesystem IDs, checks invalid-ID errors, and prints U only after the checks pass. Run this example as an ordinary, non-setuid executable. These direct credential syscalls affect the calling kernel thread, unlike libc's process-wide credential synchronization. Filesystem-ID setters return the previous ID on both success and failure, so callers must query again to verify the result; see setresuid(2) and setfsuid(2). examples/linux_fifo.lim exercises mknod/mknodat FIFO creation and fchmodat2 path and AT_EMPTY_PATH permission updates, verifies metadata and errors, unlinks both FIFOs, and checks bytes through an open FIFO; examples/linux_ioctl.lim checks pipe unread-byte counts with FIONREAD, sets nonblocking mode with FIONBIO, verifies errors, and prints the exact transferred bytes. linux-ioctl takes a #u32 request and a #usize argument word, which may encode a pointer; callers must supply the request-specific buffer layout and lifetime. Request encodings are architecture-specific; see ioctl(2). examples/linux_zero_copy.lim checks sendfile, tee, and splice payloads and offsets; examples/linux_directory.lim checks both getdents64 and legacy getdents, including record boundaries, name termination, file/link names, supported type tags (allowing DT_UNKNOWN), EOF, and errors. It prints D after the legacy enumeration checks and also exercises cwd queries. Legacy x86-64 records put the name at byte 18 and the type in their final byte, unlike getdents64; see getdents(2). examples/linux_resources.lim checks usage, limits, and umask restoration; examples/linux_signals.lim checks signal action and mask querying, installation, and restoration without delivering a signal; examples/linux_signal_stack.lim installs, queries, and restores a 64-KiB alternate signal stack, checks invalid flags and undersized-stack errors, arms and cancels an alarm, and tests tkill with signal zero and an invalid signal. It prints S after these checks; it does not test execution of a handler on the alternate stack. Stack storage must remain mapped while registered; see sigaltstack(2). examples/linux_pkeys.lim requires Linux x86-64 PKU/OSPKE support. It tests pkey_alloc, pkey_mprotect, and pkey_free, checks PKRU rights, and verifies that a child's forbidden write produces SIGSEGV with core dumps disabled. The parent restores key zero before freeing the allocated key, checks invalid flags and stale-key errors, and prints K from the restored mapping. On machines without protection-key support allocation can return -ENOSPC; this hardware-specific test requires successful allocation rather than silently counting an unsupported path as coverage. See pkey_alloc(2). examples/linux_program_break.lim queries and reapplies the current personality, grows the program break by two pages, checks memory access, rejects impossible growth, and restores the original break. It prints H from the allocated region before releasing it. linux-brk returns a #usize address: the new break on success or unchanged break on failure, not a negative errno or libc's zero/-1 result. Its unsupported-target fallback is zero. Program-break ownership must be coordinated across allocators/threads; this example is standalone and single-threaded. See brk(2). examples/linux_signal_receive.lim blocks SIGUSR1, sends it to itself, consumes it with signalfd, signalfd4, and rt_sigtimedwait, checks signal records and empty-queue errors, and restores the original mask. It also sends to itself with rt_sigqueueinfo and rt_tgsigqueueinfo, verifies SI_QUEUE, sender fields, and full 64-bit payloads, and checks invalid signals and null input records. Raw siginfo_t records are 128 bytes on the supported target; sender PID/UID fields are supplied by the caller, not authenticated credentials. See rt_sigqueueinfo(2). examples/linux_timers.lim checks POSIX timer creation, arming, querying, deletion, zero overruns on a newly created timer, and invalid-handle behavior without signal delivery; examples/linux_interval_timers.lim checks arming, querying, and restoring the process's legacy interval timer state; examples/linux_inotify.lim checks create/delete event records and watch cleanup using a private working directory; examples/linux_wait4.lim forks and reaps a child and validates the kernel's encoded exit status. The paired tests/fixtures/exec_driver.lim and exec_target.lim programs exercise execve, relative execveat, and execveat with AT_EMPTY_PATH. Their Rust harness compiles the target into a private working directory, checks exact output from all three replacement images, and verifies child exit statuses and failed-execution errors. Both wrappers take explicit null-terminated arrays of string pointers for arguments and environment, and NUL-terminated path strings. Successful calls replace the process image and never return; failures return raw negative errno values. Descriptor-based execution follows the Linux-specific execveat rules. examples/linux_waitid.lim checks setsid and setpgid in isolated children, exits them through exit/exit_group, observes their exit records with WNOWAIT, and reaps them with waitid; examples/linux_affinity.lim round-trips the process's allowed-CPU mask and checks the affinity state is unchanged; examples/linux_copy_file_range.lim validates explicit-offset copying between anonymous files, including the copied bytes and updated offsets; examples/linux_scheduler_queries.lim checks scheduler parameters, policy priority bounds, invalid-policy behavior, and the current nice value; examples/linux_scheduler_updates.lim reapplies the current scheduling parameters, policy, attributes, nice value, and I/O priority through sched_setparam, sched_setscheduler, sched_setattr, setpriority, and ioprio_set, then verifies queried state and invalid-argument errors; examples/linux_renameat2.lim checks no-replace collision errors, successful renaming, and old/new path visibility in a scratch working directory; examples/linux_statx.lim checks anonymous-file metadata through AT_EMPTY_PATH, including the returned size mask and exact file size; examples/linux_openat2.lim exercises RESOLVE_BENEATH, missing-path errors, and rejection of unknown resolution flags in a scratch cwd; examples/linux_xattrs.lim exercises descriptor-based extended-attribute creation, listing, retrieval, removal, and the missing-attribute error on a fresh memfd. tests/io_examples.rs checks exact program exit/output behavior, syscall argument counts zero through six, piped IO, local socket payloads, and kernel error results.

Building and running

For the standard library's measured syscall breadth, test commands, and remaining safety/coverage gaps, see syscall coverage.

The repository contains a Nix flake with the Rust toolchain:

nix develop
nix develop --command cargo test --all-targets
nix develop --command cargo doc --no-deps --open

Compile Lim source directly to a native executable from the Nix development shell. The backend emits inspectable assembly; its x86-64 encoder and ELF writer produce the executable without external build tools. By default, the output is placed beside the input and uses the input filename without its extension. -o selects a different path:

nix develop --command cargo run -- examples/fibonacci.lim
nix develop --command cargo run -- examples/fibonacci.lim -o /tmp/fibonacci
/tmp/fibonacci
echo $? # 55 for the Fibonacci example
nix develop --command cargo run -- --check-examples examples
nix develop --command cargo run -- examples/fibonacci.lim --target x86_64-sysv
nix develop --command cargo run -- --format examples/fibonacci.lim
nix develop --command cargo run -- fmt examples/modules/main.lim

--format retains comments in their surrounding syntax, including nested forms and generator templates. Formatting is idempotent.

The formatter keeps binding names beside their explicit types and callees beside #call or #unsafe-call. Long colon argument lists put each named group on its own line; empty argument lists use (). Short unsafe expressions and single-expression cases stay compact, while multi-expression case bodies are indented as sequences. Function and generator declarations are separated with blank lines.

Formatting uses Lisp-style headers and two-space body indentation. Function signatures stay together, short nested expressions stay inline, and closing parentheses follow the final expression. A #for keeps initialization, comparison, and mutation together, followed by its indented body:

(#for (#let-mut i #u64 0) (#u64::lt (#clone i) 10) (#set i (#u64::add-wrap (#clone i) 1))
  (#assert (#u64::lt (#clone i) 10)))

Ordinary expressions exceeding a target width of 100 columns wrap between arguments. Form headers may exceed that width. Comments and parser shorthand retain their source spelling.

lim fmt INPUT formats the file and its transitive explicit file dependencies within the same library boundary. Dependencies across a boundary are skipped. The read-only --format form remains available to print one formatted file or write it to a separate output path.

Native compilation carries an explicit target description. The supported target/ABI matrix currently has one entry:

The linker reads ELF object symbol tables directly. When all objects have no unresolved symbols and no libraries were explicitly requested, it links statically without libc, pthread, or a dynamic interpreter. This includes programs importing the direct-syscall Linux library. Unused external declarations alone do not require a runtime. Inline assembly's foreign references are detected from encoded relocations. References between supplied objects are resolved before considering shared libraries. If unresolved references remain, or libraries were explicitly requested, the compiler writes the interpreter, dynamic symbol/string tables, GOT relocations, and shared-library dependencies itself. Supplied ELF64 objects may contain code, read-only data, writable data, and BSS. Source constants and object-file read-only sections occupy a separate readable, non-executable ELF segment; code is read-execute and mutable data is read-write. Unsupported #asm forms or ELF relocations are diagnosed rather than passed to an external tool. All 318 current examples build with external build tools absent from PATH. The object linker currently accepts x86-64 R_X86_64_64, PC32, PLT32, 32, 32S, GOTPCREL, GOTPCRELX, and REX_GOTPCRELX relocations. Direct unresolved PC32 references to sized data symbols in shared libraries use R_X86_64_COPY relocations. TLS data and unsupported relocation forms are rejected with a linker diagnostic. Absolute shared-library symbol addresses stored in writable object sections use dynamic R_X86_64_64 relocations. PC-relative GOT and COPY references may also originate in writable sections. An undefined weak object symbol with no linked object definition resolves to zero; it does not force a shared library dependency. ELF forms outside this supported subset are rejected. The dynamic loader path is read from the compiler's own ELF interpreter when available, with LIM_DYNAMIC_LINKER as an absolute-path override and the conventional Linux x86-64 loader path as a fallback. Shared libraries are located using the loader's directory, target library search paths, and standard Linux paths; their directories are recorded as an ELF runpath. After main returns, the entry stub calls Linux exit_group with its result, not thread-only exit, so outstanding kernel workers cannot change the process's final status. Explicit linux-exit remains thread-only. See exit_group(2).

All other target names (including other operating systems using the System V calling convention) are rejected. Host selection requires both Linux and x86-64. The Rust API exposes TargetDescription and generate_assembly_for_target; the existing generate_assembly API selects the supported host target.

--check-examples recursively parses, type-checks, borrow-checks, and lowers every .lim file under the selected directory. It reports each source file individually and returns failure if any example fails.

--emit-asm INPUT OUTPUT remains available to inspect backend output. --stack-usage INPUT compiles the project through code generation, then reports generated-code stack bounds without invoking the native linker. It accepts --target, --cfg, and --module-path options just like compilation. Every generated #generate expansion is materialized as a readable, content-addressed .lim entry under .lim/generated/, regardless of whether it uses a built-in or a user-defined generator. The digest is derived from the normalized invocation, compiler version, target, complete loaded import forms, and compiler cfg values. A neighboring key file verifies the full key before a cache hit, so a digest collision cannot return unrelated generated source. A checksum over the key and generated bytes detects edited or damaged entries; invalid entries are regenerated. Checksums detect accidental changes and are not an authenticity mechanism against someone who can edit both data and metadata. User-generator evaluation also keeps its lower-level syntax cache in the same directory with an integrity checksum. Cache records are staged under unique names and published atomically; the inspectable-source checksum is published last as a consistency marker. An interrupted or concurrent write is treated as a cache miss and regenerated. Staging files older than one hour are removed when the cache is next read; newer temporary files may belong to active compiler processes and are left alone. There are no numbered generated-source files; deleting .lim/ only causes generators to run and materialized entries to be recreated.

Compile-time configuration

#cfg-if includes only the selected top-level forms. Its condition is built from #cfg-is, #cfg-not, #cfg-and, and #cfg-or; branches contain forms directly, with an optional final #cfg-else branch:

(#cfg-if (#cfg-and (#cfg-is #platform linux) (#cfg-is #feature fast))
  (#fn selected () #u64 (#return 1u64))
  (#cfg-else
    (#fn selected () #u64 (#return 0u64))))

#platform and #os are populated automatically from the compiler host OS (linux, macos, or windows, where applicable); #arch is the target architecture (such as x86_64), and #target is its canonical target triple (currently x86_64-unknown-linux-gnu for the supported backend). Other keys must be passed with --cfg KEY=VALUE; for example, --cfg feature=fast. Command-line settings override automatic values. Configured values are literal symbols or strings in #cfg-is. Excluded forms are removed before imports, generators, name checks, and type checking are processed.

Pass --cfg repeatedly to set several keys. It works in both binary and assembly-output modes; a key supplied more than once uses its last value.

Use --collect-cfgs INPUT to print the sorted, unique cfg keys referenced by the source and its imports. Collection scans every cfg branch, including inactive branches, and follows imports found inside those branches:

nix develop --command cargo run -- --collect-cfgs examples/cfg_platform.lim
# prints: #platform

User-defined generators

(#syntax StepAwait (#u64 Step StepPoll.StepPending StepPoll.StepReady step-poll))
(#await StepAwait step)

(#generate #async-fn ((protocol WorkAwait) (waker LocalWaker)
  (function (#fn work ((offset #u64)) #u64
    (#return (#await StepAwait (Waiting offset)))))))
// In another async function:
(#await WorkAwait (#call work (($ offset))))

(#fn u64-less ((left (#ref #u64)) (right (#ref #u64))) #bool
  (#return (#u64::lt (#deref left) (#deref right))))
(#capability sortable #u64
  ((u64-less ((#ref #u64) (#ref #u64)) #bool)))
(#gn make-sortable ((element sortable))
  `((#type Sortable ,element)))
(#generate make-sortable #u64)

parameters := (parameter ...)
parameter  := name | (name capability-name ...)

(#gn aliases (pairs)
  (#gn-for-each pair pairs
    (#gn-list
      (#gn-symbol "#type")
      (#gn-first pair)
      (#gn-first (#gn-rest pair)))))

(#generate aliases ((Byte #u8) (Word #u16)))

(#gn-fn make-alias (name target)
  `(#type ,name ,target))

(#gn aliases (pairs)
  `(,@(#gn-for-each pair pairs
       (#gn-call make-alias
         (#gn-first pair)
         (#gn-first (#gn-rest pair))))))

(#require-generated Work::Frame #async-fn-pinned
  (Work::Poll Work::Poll.Pending Work::Poll.Ready Work::poll))

Imports

Distributed enums collect variants from active imports and generator outputs. Declare (#distributed-enum Error ()) once, and add individual variants with (#enum-contribute Error (Failure #u32)). After expansion, the compiler merges identical variants by name, rejects conflicts, and compiles one ordinary enum. See collections and tasks for the full rules and cooperative async generators. General distributed syntax is not supported.

Struct and enum declarations require a property list between the name and their fields or variants. Use () when no properties are needed. The supported properties are #linear and #repr-c:

(#struct FileHandle (#linear) ((descriptor #u64)))
(#enum Maybe (#repr-c) ((Maybe.Some #u64) Maybe.None))
(#struct NativeOwner (#linear #repr-c) ((handle (#ptr #u8))))

Aggregates become linear transitively when they own a linear field or, for an enum, any linear payload in any variant. References do not make their containing aggregate linear because they do not own their referents. Explicit #linear forces a struct or enum to be linear even when all fields or payloads are plain data. It does not change layout or Send/Sync. Generated task state types use this property.

File references identify declarations directly, without copying source or prepending prefixes. Aliases give those declarations explicit local spellings:

(#alias read = ./shared.lim::read)
(#alias Widget = project::compat/lib.lim::Widget)

./ paths resolve relative to the source containing the reference. project:: paths resolve from the nearest lim.project ancestor of the principal source; when there is no manifest, its directory is the project root. All dependencies use that same root. / retains filesystem-absolute meaning. Rooted paths cannot contain ..; direct references do not search module-path lists. Files are loaded once by canonical identity, and alias cycles and runtime recursion are rejected.

A directory containing lib.lim establishes a library permission boundary. Each source belongs to its nearest boundary, including a separately compiled white-box test. References within that library may name implementation files; references from outside must target lib.lim and select an exported declaration. Nested library directories establish independent boundaries. Canonical paths prevent symlink and .. privacy bypasses. #unstable explicitly bypasses the entry-point/export restrictions for a selected declaration, not its struct fields.

Only lib.lim may contain (#export Type function ...), listing the declarations available outside the library. Other declarations remain library-internal. Exporting a struct type does not export its representation: external code cannot construct, read, write, borrow, or project its fields. Exporting an enum exposes every variant for construction and matching; individual variants cannot appear in #export. Every payload type must also be publicly accessible, including in unused variants. Adding a variant changes the exhaustive matching contract. An unexported enum remains private. To hide its representation, store it inside an exported opaque struct and expose functions that operate on that struct; see examples/opaque_handle.lim and examples/opaque_handle/lib.lim. Exported function signatures and aliases cannot expose private types. All implementation declarations remain visible to whole-program borrow checking and optimization.

Generated declarations belong to their invocation's library, not the physical .lim cache directory. Each generated file has access to its producer's definition library and its invocation library, including private functions, types, and representations. A nested generator gets its own definition library and the original invocation library; it does not accumulate its ancestors' definition-library privileges. A canonical file has one declaration identity, regardless of which alias reaches it. Separate source paths can carry different library versions.

Write @name to resolve a name before generator execution. Inside a generator definition it uses that definition's file scope; in supplied arguments it uses the invocation source's file scope. Qualification produces the actual flat file-qualified identifier (for example, /project/library/helper.lim::Helper), not a hidden binding or a runtime expression. Forwarding and substitution never qualify it again. Literal strings, generator parameters, and unmarked local bindings are not interpreted by this operation. Handwritten forward declarations are collected before qualification. Exported generated targets can be qualified using their library's literal export contract; other unknown names cannot be qualified. In particular, @local cannot silently become a local reference after splicing a literal function. Pass new declaration names as literal symbols.

Invocation references are checked using caller permissions before interpreting the generator, including explicitly qualified references inside quoted syntax. A caller cannot pass @lib@secret when that declaration is private to lib. Literal strings and selectors remain data: a generator may deliberately turn them into references using #gn-symbol, #gn-symbol-append, or #gn-variant. The resulting code uses its generated file's permissions. Thus generators are privileged library APIs: their authors must validate data and executable syntax they incorporate into their output. Qualification checks are not a sandbox for an arbitrary code-splicing generator. #unsafe obligations remain unchanged.

Inspectable generated files record permissions as reader syntax, for example:

(#generated-context
  ((producer "lib@make")
   (definition-module "/project/library/lib.lim")
   (definition-file "lib")
   (invocation-module "/project/app/lib.lim")
   (invocation-file "")))

This compiler-owned header is checked against the current generator and invocation on cache reuse. It contains no serialized source IDs or per-symbol permission comments. Copying a header into source, supplying one to a generator, or manufacturing one with generator operations is rejected. A generator cannot manufacture late @ qualification either: qualification is a source operation. Files outside a lib.lim boundary share the <global> module; physical invocation locations remain in the existing generated-file origin comments and do not prevent equivalent expansions in that module from sharing a cache artifact.

For example, an exported counter-reader generator can emit a call to a private counter-value helper. The consumer still cannot invoke that helper directly:

(#alias counter-reader = ./encapsulation/lib.lim::counter-reader)
(#generate counter-reader read-generated-counter)

See examples/generator_private_helpers.lim for a complete executable example.

An expansion instance includes the invoking file's identity, generator, and literal arguments. Identical calls in one file can reuse a generated declaration; calls in different files retain separate declaration identities. Cache keys also include resolved references, dependency contents, and validated definition/caller contexts. Multiple aliases to one source share that source; separate dependency versions occupy different source paths.

An exported generator may invoke its library-private generator helpers, including nested generators. Syntax equality and argument deduplication compare values, not the way symbols were constructed. Builtin expansions also distinguish producing definition contexts. Cache keys include definition/invocation context headers as well as generator/dependency identities, and digests cover the complete generated file. Cached authority is reconstructed from the current expansion, not accepted from a file's self-asserted claims. #std remains one compiler-provided prelude. Its facade explicitly lists its declarations; parameter labels retain their original source spelling. See examples/library_boundary.lim and examples/encapsulation/test.lim.

To bound compiler resource use, a project is limited to 128 simultaneously nested source files, 4096 unique source dependencies, and 64 MiB of cumulative source text (including the root file). Dependency-limit errors identify the reference that crosses the limit; an oversized root file is rejected before import traversal.

The compiler resolves each file reference exactly: ./ is relative to its source file, project:: is relative to the compilation's project root, and / is an absolute filesystem path. There is no fallback search through module directories.

Projects may add a lim.project manifest beside the root source:

schema-version = 1
name = "example"
source-root = "src"
output-dir = "build"
module-path = "modules"
target = "x86_64-sysv"
link-lib = "m"
link-object = "native/support.o"

Manifest paths are relative to the manifest. The nearest manifest above the principal source defines the project:: root, including for dependencies outside that directory. Without a manifest, the principal source's directory defines it. The CLI defaults binary output into the output directory and applies the manifest target unless --target overrides it. Repeated link-lib and link-object entries add linker inputs. Schema version 1 validates required name/version, supported target names, existing source and module directories, duplicate module roots, and existing object files; unknown keys are errors.

Lexical syntax

Whitespace separates tokens. // starts a line comment. A line beginning with bare # is also a comment unless the # begins a keyword, operator, or character literal.

The lexer recognizes:

• ( and ) for lists;
• { and } for named pair lists;
• [ and ] for typed infix expressions;
• = for record assignments and ; for entry/form termination;
• 'form quote syntax;
• #generate as the generated-code keyword; #generate stays inside identifiers;
• symbols;
• signed and unsigned integer literals;
• floating-point literals;
• strings and character literals.

. is an ordinary character in a symbol, not a namespace or member-access operator. - is also an ordinary symbol character. Thus these are single identifiers:

Work::poll
my-value
Choice.Ready

Builtin forms are distinguished by their # prefix:

(#fn main () #u64
  (#return 42u64))

The character literal syntax is #\a, #\space, #\newline, and so on. Unicode escapes use #\u{03bb}. Strings support \n, \r, \t, \\, \", and \u{...} escapes.

Integer literals may use binary, octal, hexadecimal, and underscores:

42u32  -1i8  0b1010u16  0o77u8  0xffffu128

Floating-point literals carry an explicit width when used in canonical code: 1.5f32 and 0.25f64.

Types

The builtin scalar types are:

Fixed aggregates are written explicitly:

(#tuple #u64 #bool #char)
(#array #u32 4)

Construct a fixed-size array value with #array-of, keeping it visually distinct from the #array type form:

(#let values (#array #u32 3)
  (#array-of (#array #u32 3) 10u32 20u32 30u32))

An immutable slice type is written (#slice T). Borrow an array directly with (#borrow-slice array), or select [start, end) with (#borrow-slice array start end). These operations explicitly borrow storage; they neither move the array nor allocate. Both bounds must be #usize. (#slice-of array-reference) instead converts an existing immutable array reference into a slice without extending its backing storage's lifetime. Use (#slice-len view) for its runtime length and (#slice-idx view index) to get a shared reference to an element. Indexing checks the index against the slice length and traps if it is out of bounds. Use (#slice-range view start end) to create an immutable half-open subrange [start, end). Both bounds are #usize; the operation traps if start > end or end > (#slice-len view). Empty and end-boundary ranges are valid. A subslice retains the original borrow provenance, including across function returns; it does not extend the referent's lifetime. Slices remain immutable.

User-defined names refer to concrete structs, enums, and aliases. Generic declarations and angle-bracket applications are not part of Lim. Generators create concrete specializations explicitly, such as (#generate #vec ((element #u64) (allocator Alloc) (name VecU64))). Allocator-backed collections add their concrete operations explicitly with (#generate #vec-alloc ((element #u64) (allocator Root) (vector VecU64) (destroy destroy))); Root::State must denote Alloc, the state type passed to #generate #vec. The root provides a byte-pointer allocation enum, safe ::allocate, and unsafe ::grow / ::deallocate; grow takes :old-layout and the requested :layout. Handwritten and generated bundles follow the same ordinary naming convention, without a producer requirement. #std provides SystemAllocator::Allocator, whose empty state is constructed with (#struct-literal SystemAllocator ()). Providers promise fresh, unique, aligned, non-null successful allocations, preservation of the old allocation on growth failure, and matching deallocation. Names and type checking cannot prove these semantic promises. The generated API includes VecU64::new, ::reserve, ::push, ::get, ::get-mut, ::set, ::pop, and ::free. (#generate #vec-sort ((element #u64) (vector VecU64) (comparator compare-u64))) adds VecU64::sort; its named comparator accepts two immutable element references and returns #bool. Allocation failure and capacity overflow are returned in generated result types. See the allocator ABI for the allocator and destruction function signatures.

() is the unit value and ! is the never type. A function returning ! must not reach a normal return. A void function returns explicitly with (#return ()).

(#std)
(#fn main () #u64
  (#let text (#array #char 3) "Aé🙂")
  (#return
    (#match (#call String::from-chars ((text (#borrow-slice text))))
      (#case (StringCreateResult.StringCreated owned)
        (#block
          (#let length #usize (#call String::len ((string (#borrow owned)))))
          (#call String::free ((string owned)))
          (#if (#usize::eq length 7usize) 42u64 1u64)))
      (#case (StringCreateResult.StringCreateFailed error) 2u64))))

(#std)
(#fn main () #u64
  (#let greeting (#array #char 5) "Hello")
  (#let suffix (#array #char 9) ", world 🙂")
  (#let-mut message String
    (#match (#call String::from-chars ((text (#borrow-slice greeting))))
      (#case (StringCreateResult.StringCreated created-message) created-message)
      (#case (StringCreateResult.StringCreateFailed error) (#panic))))
  (#let tail String
    (#match (#call String::from-chars ((text (#borrow-slice suffix))))
      (#case (StringCreateResult.StringCreated created-tail) created-tail)
      (#case (StringCreateResult.StringCreateFailed error) (#panic))))
  (#assert (#match (#call String::push-string ((string (#borrow-mut message)) (text (#borrow tail))))
    (#case StringStatus.StringOk true) (#case _ false)))
  (#assert (#match (#call String::push-char ((string (#borrow-mut message)) (value #\!)))
    (#case StringStatus.StringOk true) (#case _ false)))
  (#assert (#i64::eq (#println (#borrow message)) 0i64))
  (#call String::free ((string tail)))
  (#call String::free ((string message)))
  (#return 42u64))

(#std)
(#generate #utf8-view ((name BorrowedText) (owner (#slice #u8))))
(#fn main () #u64
  (#let bytes (#array #u8 2) (#array-of (#array #u8 2) 195u8 169u8))
  (#let view BorrowedText
    (#match (#call BorrowedText::from-owner ((owner (#borrow-slice bytes))))
      (#case (BorrowedText::Result.Valid accepted) accepted)
      (#case _ (#panic))))
  (#let-mut iterator BorrowedText::Chars (#call BorrowedText::chars ((view view))))
  (#assert (#match (#call BorrowedText::Chars::next ((iterator (#borrow-mut iterator))))
    (#case (BorrowedText::CharResult.Char value) (#char::eq value #\é))
    (#case _ false)))
  (#forget iterator)
  (#return 42u64))

Top-level declarations

(#fn below-100 ((value #u64)) #bool
  (#return (#u64::lt value 100u64)))

(#fn submit ((value #u64)) ()
  (#requires (#call below-100 ((value value))))
  (#return ()))

(#fn validate-and-submit ((value #u64)) ()
  (#if-valid (#call below-100 ((value value)))
    (#call submit ((value value))))
  (#return ()))

(#fn below-100 ((value #u64)) #bool
  (#return (#u64::lt value 100u64)))
(#type Small
  (#where (value #u64) (#call below-100 ((value value)))))
(#struct Request () ((count Small) (tag #u64)))

(#fn consume-small ((value Small)) ()
  (#return ()))

(#fn under-two ((index #usize)) #bool
  (#return (#usize::lt index 2usize)))
(#fn widen ((index #usize)) ()
  (#requires (#call under-two ((index index))))
  (#ensures (#usize::lt index 4usize))
  (#return ()))
(#type Index4 (#where (index #usize) (#usize::lt index 4usize)))
(#fn read-four ((values (#ref (#array #u64 4))) (index Index4)) #u64
  (#return (#index-proven values index)))
(#fn use ((values (#ref (#array #u64 4))) (index #usize)) #u64
  (#return (#if-valid (#call under-two ((index index)))
    (#block
      (#call widen ((index index)))
      (#let checked Index4 index)
      (#call read-four ((values values) (index checked))))
    0u64)))

(#fn add ((left #u32) (right #u32)) #u32
  (#let total #u32 (#u32::add-wrap left right))
  (#return total))

(#fn add ((left #u32) (right #u32)) #u32
  (#return (#u32::add-wrap left right)))
(#fn main () #u64
  (#return (#as (#call add ((right 2u32) (left 40u32))) #u64)))

(#return : #u64::add-wrap left right)
// Equivalent to (#return (#u64::add-wrap left right)).

(a : b : c)
// Equivalent to (a (b (c))).

(#fn increment ((#mut value #u64)) #u64
  (#set value (#u64::add-wrap value 1u64))
  (#return value))

(add ((left 20u32) (right 22u32)))
add { left = 20u32; right = 22u32; }

(#fn add ((left #u32) (right #u32)) #u32
  (#return (#u32::add-wrap left right)))
(#fn main () #u64
  (#let left #u32 20u32)
  (#let right #u32 22u32)
  (#return (#as (#call add (($ left) ($ right))) #u64)))

(#extern-fn #abi-c abs ((value #i32)) #i32)
(#fn main () #u64
  (#return (#as (#unsafe (#unsafe-call abs ((value -42i32)))) #u64)))

printf 'hello from Lim\n' | ./target/debug/lim examples/echo_input.lim -o /tmp/lim-echo
printf 'hello from Lim\n' | /tmp/lim-echo

(#type UserId #u64)
(#type Pair (#tuple #u64 #bool))
(#type Matrix (#array #f32 4))

(#struct Point () ((x #u64) (y #u64)))

(#fn main () #u64
  (#let point Point (#struct-literal Point ((x 7u64) (y 9u64))))
  (#return (#get point y)))

(#struct MovePayload () ((x #i32) (y #i32)))
(#enum Message ()
  (Message.Quit
   (Message.Move MovePayload)
   (Message.Write (#array #char 8))))

(#const answer #u64 42u64)
(#static values (#array #u64 3)
  (#array (#array #u64 3) 10u64 20u64 30u64))

(#fn first-value () #u64
  (#return (#unsafe (#index values 0u64))))

(#static counter (#atomic #u64) (#atomic-init #u64 0u64))
(#fn increment-counter () #u64
  (#return (#unsafe
    (#atomic-fetch-add (#borrow counter) 1u64 #memory-relaxed))))

Variables and mutation

Local bindings always state their type:

(#let count #u32 0u32)
(#let-mut total #u64 0u64)

#let creates an immutable binding; use #let-mut for a mutable binding. Bindings may not shadow a visible parameter, local, or global; choose a distinct name instead. Names may be reused in separate sibling scopes when neither binding is visible from the other. #set assigns a mutable scalar or aggregate local:

(#set total (#u64::add-wrap total 1u64))

A whole reference-bearing local may also be assigned from another typed binding or a fieldless enum variant, for example (#set view next) or (#set view Empty). The replacement installs that binding's reference origins and releases the old binding's loans. Shared references remain Copy; exclusive references transfer without duplication. An outstanding borrow of the destination still prevents replacement, and a linear old value must already have been consumed. Arbitrary reference-bearing RHS expressions and member replacement retain their existing restrictions. examples/reference_assignment.lim releases the old owner, reads the new owner, then drops both shared handles before mutating the new owner.

Binding an exclusive reference, or storing it in an aggregate, transfers its handle: subsequent use of the source handle is rejected. Extracting an exclusive reference from an owned aggregate likewise transfers its selected slot, not the pointee or the other fields. Forgetting the remaining container does not end the transferred borrow; explicitly release the destination handle before mutating its owner. See examples/exclusive_reference_move.lim. References need no mandatory destruction at function exit, and passing a reference directly to a function is a call-duration reborrow rather than a handle transfer.

A derived field reference also suspends overlapping parent access through function calls. Moving the child into another aggregate, or moving and restoring its holder through pinned storage, does not erase that restriction. Calls may use the child's own reference; explicitly release the child holder before lending the parent again. examples/reference_parent_call.lim demonstrates that order, and tests/ui/call-suspended-parent.lim shows a rejected parent call.

The same access restriction applies when a function returns the child reference, directly or inside an aggregate. A returned call reborrow retains the referent's loan even if its temporary parent handle is released; it does not require that handle's storage to stay alive. See examples/returned_reference_parent.lim for a returned reference carried out of a labeled loop and used after parent-handle cleanup. tests/ui/call-returned-parent.lim rejects lending the parent again while its returned child is live.

Struct types are not constructors. Create a value with #struct-literal, or write a named free-standing constructor function that returns one. Every field must be supplied exactly once; fields may appear in any order, and omitted fields are not defaulted:

(#struct Point () ((x #u64) (y #u64)))
(#let point Point
  (#struct-literal Point
    ((y 22u64) (x 20u64))))

Unknown, duplicate, or missing fields are compile-time errors. A type name in call position, such as (Point 20u64 22u64), is rejected; give constructor functions distinct names such as make-point. The UI suite covers this rejection in tests/ui/type-as-constructor.lim; it also pins the diagnostic spans for positional calls, generic function declarations, and angle-bracket generic call syntax in tests/ui/positional-call.lim, tests/ui/generic-function.lim, and tests/ui/generic-angle-call.lim.

Aggregate projections can be updated with #set-index, #set-field, and #set-payload:

(#set-index values 0u64 10u64)
(#set-field point x 11u64)
(#set-field pair 1 12u64)
(#set-payload choice Move 0 5i32)

Mutable slices use a separate type and constructors: (#slice-mut #u64), #borrow-slice-mut array to borrow a full mutable array, or #borrow-slice-mut array start end to select a half-open range. #slice-mut-of converts an existing mutable array reference, #slice-mut-idx provides exclusive element access, and #slice-mut-split view at to consume a view and produce two disjoint halves. The split point is a checked #usize index; an index greater than the length traps, and the halves cover [0, at) and [at, len). Views are linear: splitting consumes the parent, and overlapping mutable loans or access through the original array are rejected while a view is live. Each half must itself be consumed (for example, passed to a function or explicitly #forget-ted). Mutable slices can be returned when their inferred provenance comes from a function argument; a view of a local array cannot escape.

(#borrow (#deref reference)) and (#borrow-mut (#deref reference)) explicitly reborrow the existing referent without loading or moving it. Exclusive reborrowing requires an exclusive parent. A pinned parent produces a pinned reborrow; this syntax cannot remove the pin guarantee. Scoped borrow forms accept the same dereferenced places.

Pinning a mutable slice holder does not pin its backing elements. An exclusive reference to that holder, including (#pin-ref-mut (#slice-mut T)), can reborrow a range through (#slice-mut-range (#deref holder) start end) without extracting or moving the holder. A shared holder reference cannot grant this exclusive access. The resulting range still borrows the original backing storage and must end before conflicting access to that storage.

(#slice-mut-range parent start end) reborrows an existing mutable slice handle: a named handle or an exclusive, variable-rooted aggregate field/tuple slot such as (#get holder view). Owned aggregate projections require a mutable owner; projections through a shared reference and temporary receiver expressions are rejected. It does not consume the parent. Parent access, transfer and destruction are suspended until the child is released. Nested views retain the original backing storage's lifetime and physical offsets. Unrelated aggregate slots remain usable while a field's child is live. All range constructors check start <= end <= length and trap on failure; empty ranges are valid. Constant disjoint regions permit independent exclusive borrows (or an exclusive and a shared borrow). Dynamic bounds are conservatively overlapping; use #slice-mut-split for two runtime-disjoint mutable regions. Direct array borrowing accepts owned array places and array fields through ordinary references; it does not silently convert an array reference or erase a pinned reference.

(#let-mut values (#array #u64 4) (#array (#array #u64 4) 1u64 2u64 3u64 4u64))
(#let whole (#slice-mut #u64) (#borrow-slice-mut values))
(#let (#tuple left right)
  (#tuple (#slice-mut #u64) (#slice-mut #u64))
  (#slice-mut-split whole 2usize))
(#deref-set (#slice-mut-idx left 0usize) 17u64)
(#deref-set (#slice-mut-idx right 0usize) 25u64)
(#forget left)
(#forget right)

(#enum Answer () ((Answer.Value #u64) Answer.Empty))
(#fn main () #u64
  (#let answer Answer (#enum-literal Answer.Value 42u64))
  (#return (#match answer
    (#case (Answer.Value value) value)
    (#case Answer.Empty 0u64))))

(#enum Outcome () ((Outcome.Success #u64) Outcome.Failure))
(#fn main () #u64
  (#let-else (Outcome.Success answer) (Outcome.Success 42u64)
    (#else
      (#return 0u64)))
  (#return answer))

(#std)
(#enum Task () ((Task.Work #u64) Task.Idle))
(#generate #enum-project ((enum Task) (variant Task.Work) (payload #u64) (mode #pin-ref-mut) (name WorkProjection)))
(#fn main () #u64
  (#let-mut task Task (Task.Work 42u64))
  (#let-else (WorkProjection.Some frame)
    (#call WorkProjection::project ((source (#pin-borrow-mut task))))
    (#else
      (#forget task)
      (#return 0u64)))
  (#let answer #u64 (#unsafe (#pin-read frame)))
  (#forget frame)
  (#forget task)
  (#return answer))

(#let count #u64 40u64)
(#let total #u64 (#u64::add-wrap (#clone count) count))

(#let-mut count #u64 0u64)
(#set count (#u64::add-wrap count 1u64))

(#struct Buffer () ((allocation Allocation)))
(#fn Buffer::destroy ((buffer Buffer)) ()
  (Allocation::release (#get buffer allocation))
  (#forget buffer)
  (#return ()))

Operators

Numeric operators are never unqualified in canonical syntax. The operand type is part of the identifier, and integer arithmetic must also specify its overflow mode:

(#u64::add-wrap left right)
(#i32::sub-saturate left right)
(#u128::mul-wrap left right)
(#u128::div-wrap dividend divisor)
(#u128::rem-wrap dividend divisor)

The available integer arithmetic operations are add, sub, mul, div, and rem. The modes are:

• -wrap: modular two's-complement or unsigned wrapping behavior;
• -saturate: clamp to the representable bounds.

There is no plain integer arithmetic spelling. #u64::add and #u128::div are rejected because they omit the overflow mode.

Floating-point arithmetic uses the type-qualified operator without an overflow mode:

(#f64::add left right)
(#f32::div numerator denominator)
(#f64::rem left right)

The remaining type-qualified operator families are bitwise operations (&, |, ^, !, <<, >>), comparisons (<, <=, >, >=, ==, !=), and boolean short-circuit operations (#bool::and, #bool::or). The operand type must match the qualifier. Shifts are checked against the width of the left operand when the count is statically known; invalid dynamic counts trap at runtime.

Unary negation is written, for example, as #i128::sub-wrap value.

All conversions are explicit with #as:

(#as value #u64)

Conversions cover integer, character, boolean, and floating-point scalar representations subject to the type checker’s range rules.

Expressions and builtin forms

Builtin forms are ordinary Lisp lists whose first symbol begins with #. The table below is a quick, categorized overview. The alphabetic reference that follows documents each reserved # form, its shape, a use in the appropriate context, and its effect.

(#fn increment ((#mut value #u64)) #u64
  (#let reference (#ref-mut #u64) (#borrow-mut value))
  (#deref-set reference (#u64::add-wrap (#deref reference) 1u64))
  (#drop reference)
  (#return value))

(#fn main () #u64
  (#return (#call increment ((value 41u64)))))

(#gn-fn alias-declaration (name)
  (#gn-if (#gn-symbol? name)
    `(#type ,name #u64)
    (#gn-error "alias name must be a symbol")))

(#gn make-alias (name)
  (#gn-list (#gn-call alias-declaration name)))

(#generate make-alias Answer)

(#fn main () Answer
  (#return 42u64))

(#return (#if (#u64::gt value 0u64)
              value
              0u64))

(#while (#u64::lt i 10u64)
  (#set i (#u64::add-wrap i 1u64)))

(#fn main () #u64
  (#let result #u64 (#loop (#break 42u64)))
  (#return result))

(#for (#let-mut i #u64 0u64)
      (#u64::lt i 10u64)
      (#set i (#u64::add-wrap i 1u64))
  (#set total (#u64::add-wrap total i)))

(#for () keep-going
      (#await () StepTask StepPoll.StepPending StepPoll.StepReady step-poll step-task)
  (#set keep-going false))

(#for () (#u64::lt index 2u64)
  (#call advance
    ((next (#await #u64 StepTask StepPoll.StepPending StepPoll.StepReady step-poll step-task))
     (counter (#borrow-mut index))))
  ())

(#for-range (i #u64) 0u64 10u64
  (#set total (#u64::add-wrap total i)))

#fn main {
  #params = {};
  #returns = #u64;
  #body:
    #let-mut total #u64 0;
    #for-range (number #u64) 1 11:
      #set total [#u64 #wrap; total + number];
    #return total;
}

(#fn main () #u64
  (#return
    (#label outer
      (#loop (#break-to outer 42u64)))))

Patterns and matching

#match requires exhaustive coverage. Enums require every variant; scalar booleans require both values. Integer literals and inclusive #range patterns are combined to check coverage of the complete scrutinee type, including #u128 and #i128. Patterns may overlap or appear in any order; the first matching arm wins. _ supplies a wildcard. Character matches still require a wildcard. Guarded arms do not contribute unconditional coverage. Every arm must be explicitly introduced with #case. Enum payloads are written as constructor patterns:

(#match value
  (#case (Some payload) payload)
  (#case None 0u64))

Tuple, struct, array, scalar, range, typed-literal, and #or patterns are supported. Guards are placed between the pattern and body, using #when:

(#match value
  (#case (Some payload) (#when (#u64::gt payload 40u64)) payload)
  (#case (Some _) 0u64)
  (#case None 0u64))

No wildcard is needed when integer patterns cover the entire domain. This example tests the inclusive boundary between two ranges:

(#fn classify ((value #u8)) #u64
  (#return (#match value
    (#case (#range 0u8 127u8) 0u64)
    (#case (#range 128u8 255u8) 42u64))))
(#fn main () #u64
  (#assert (#u64::eq (#call classify ((value 127u8))) 0u64))
  (#return (#call classify ((value 128u8)))))

Destructuring uses the same aggregate pattern shapes:

(#let (#tuple left right) (#tuple #u64 #u64) pair)

The pattern syntax is checked against the explicitly declared type; bindings are not inferred. When the matched value is a pinned enum reference, ordinary #case is reserved for the wildcard fallback (#case _ body). Every named variant uses #case-pin or #case-pin-mut, including fieldless variants such as (#case-pin Empty body). The shared form binds a #pin-ref payload, including when the input itself is mutable; the mutable form binds a #pin-ref-mut and therefore requires exclusive input. Payload arms accept only one binder or _. Guards, wildcard defaults, exhaustiveness, and duplicate checks follow the usual match rules. The payload stays in its original stack or heap slot, and returned payload references retain the matched owner’s lifetime. Existing unsafe #pin-write and checked #pin-set-field rules still apply inside an exclusive arm.

Ordinary references use #case-ref and #case-ref-mut to borrow enum payloads without pinning the owner. The shared form binds #ref Payload; the exclusive form binds #ref-mut Payload and requires mutable input. Each named variant, including fieldless variants, uses the matching form. #case _ is the fallback, and borrowed and pinned forms cannot be mixed in one match. Payload patterns accept one binder or _, without nested destructuring. examples/borrowed_cases.lim is a runnable example.

All five case forms accept a sequence of body expressions, after the optional (#when condition) guard. Multiple expressions lower to one #block in the arm's scope; the last expression supplies its value. This does not introduce implicit function returns or automatic destruction. For example:

(#case (Work::Poll.Pending pending)
  (#forget pending)
  0u64)

This is equivalent to (#case (Work::Pending pending) (#block (#forget pending) 0u64)). A body is required even after a guard.

Async lowering can still conservatively reject an exclusive match receiver returned by another function: its frame retains a conflicting parent reference handle. This is a generator limitation, not a restriction on ordinary functions; async_generator_matches_reference_returned_by_call records the pending case.

(#enum Choice () ((Choice.Full #u64) Choice.Empty Choice.Other))
(#fn main () #u64
  (#let-mut choice Choice (Choice.Full 41u64))
  (#let observed #u64 (#match (#borrow choice)
    (#case-ref (Choice.Full payload) (#deref payload))
    (#case-ref Choice.Empty 0u64)
    (#case _ 0u64)))
  (#let updated #u64 (#match (#borrow-mut choice)
    (#case-ref-mut (Choice.Full payload) (#block (#deref-set payload 42u64) (#deref payload)))
    (#case-ref-mut Choice.Empty 0u64)
    (#case _ 0u64)))
  (#assert (#u64::eq observed 41u64))
  (#return updated))

(#struct Payload () ((value #u64)))
(#enum Choice () ((Choice.Full Payload) Choice.Empty))
(#fn main () #u64
  (#let-mut choice Choice (Choice.Full (#struct-literal Payload ((value 41u64)))))
  (#let pin (#pin-ref-mut Choice) (#pin choice))
  (#let answer #u64 (#match pin
    (#case-pin-mut (Choice.Full payload)
      (#block
        (#pin-set-field payload value 42u64)
        (#get payload value)))
    (#case-pin-mut Choice.Empty 0u64)))
  (#forget pin)
  (#forget choice)
  (#return answer))

Generated declarations

#generate marks a generated declaration. Compiler-provided generators take one list of named (key value) pairs or a record of literal arguments. Keys may be written in any order, but every required key must appear exactly once. User-defined #gn generators retain their own positional literal interface. For example:

(#generate #optional ((type #u64) (name Maybe?)))
(#generate #result ((ok #u64) (error #u32) (name Result)))

(#generate #array ((element #u64) (length 4) (name Array4)))
(#fn main () #u64
  (#let values Array4 (#array-of 10 42 30 40))
  (#let index #usize 1usize)
  (#return
    (#if-valid (#call Array4::in-bounds ((index index)))
      (#block
        (#call Array4::prove-in-bounds ((index index)))
        (#call Array4::get ((values (#borrow values)) (index index))))
      0u64)))

Permanent non-goals

Lim intentionally has no closures, function-pointer values, methods or impl blocks, traits, or user-defined interfaces. Functions are named, free-standing declarations; generators create concrete declarations when specialization or operation families are needed. Thread spawning likewise names the worker at compile time rather than passing a callable value. This keeps call targets explicit, preserves whole-program recursion and ownership checks, and avoids implicit dispatch in generated code.

Direct file references and aliases

An explicit file reference has the spelling ./path/file.lim::declaration. The .lim:: delimiter separates the path from the complete declaration name, which may itself contain :: or an enum variant's dot. Paths resolve relative to the source file containing the reference. Canonical file identity and the declaration name identify the target; two files may declare the same name. No library source is copied or rewritten to add prefixes.

Bind a file-local spelling with #alias:

(#alias allocate = ./allocator/lib.lim::allocate)
(#alias Value = ./values.lim::Value)

Calls may use an alias or a direct reference. Named argument labels keep the callee's declared spelling. Aliases preserve type and function identity and cannot shadow declarations, other aliases, or local bindings. Unused aliases are checked too. Cyclic aliases and conflicting imported spellings are errors. There are no wildcard or prefixing import forms. Every dependency is an explicit file reference or alias; #std selects the compiler-provided standard prelude.

Files in the same nearest lib.lim boundary may refer to implementation files. Cross-library references must target lib.lim and select an exported name. The entry point can export aliases to declarations in its implementation files. Exporting a struct alias keeps the representation opaque; exporting an enum alias exposes its variants under the aliased type name.

For an intentional dependency on an implementation detail, wrap the target:

(#alias inspect = (#unstable ./library/internal.lim::inspect))

#unstable bypasses the entry-point and export restrictions for that exact declaration. It does not expose other declarations or struct representations. Selecting an enum type includes that enum's variants, as for an enum export. It does not remove type, borrow, linearity, or unsafe-call checks. Private functions may rely on library invariants, so this escape hatch is a deliberate dependency on an internal contract, not a promise that arbitrary calls are safe.

Generator definitions resolve their own references in their definition file. Explicit @name inputs resolve in the caller's file before interpretation; unmarked generator arguments remain literal syntax. Generated aliases contain resolved file references and retain the validated definition/invocation context. A generator may deliberately expose a declaration it can access by emitting an alias; this grants access to that declaration, never to its struct fields or unrelated private helpers. Forward generated targets are checked after expansion. Generator cache identities include resolved references and loaded dependencies. Fresh declarations belong to their source file. A resolved reference cannot be used to declare a symbol in another file; generators should receive a separate fresh local name for their outputs. See examples/file_access.lim for two same-named functions in different files.

Value representation and native backend

The established backend emits Intel-syntax x86-64 assembly and follows the explicit x86_64-sysv target description. Scalar integer and pointer-sized ABI words use general purpose registers; #f32 and #f64 values use SSE registers. #i128 and #u128 use two machine words.

An experimental aarch64-linux target (aarch64-unknown-linux-gnu) lowers checked bodies directly through a separate A64 instruction encoder and writes static Linux ELF internally. Its inspectable .inst listing contains resolved instruction words and descriptions; no external assembler or linker is used. Scalar integer arguments use AAPCS64 registers and aligned stack arguments. Aggregates use Lim's internal indirect convention, not a foreign aggregate ABI. The target deliberately rejects operations it does not yet implement; it is not equivalent in coverage to x86-64. See AArch64 testing for the supported subset, emulator execution and remaining acceptance matrix. --target selects builtin cfg defaults independently of the host; explicit --cfg values override those defaults regardless of argument order.

Tuples, arrays, structs, and enums remain value types. Small aggregates can be flattened through the native argument and result registers. Larger aggregates use compiler-generated caller storage at the ABI boundary and are copied as value data. Aggregate operations do not implicitly expose their storage addresses or permit layout reinterpretation; raw pointers remain explicit values handled by the unsafe pointer operations described above. Large struct-field and enum-payload projections copy directly into aggregate storage, so the source value does not need to fit in the native value registers. Enum payload reads check the active discriminant before copying. References to local enums retain the stack-layout tag used to distinguish their downward-growing storage from upward-growing static storage.

Zero-sized values such as () and empty structs/arrays occupy no value words. The compiler computes each function’s maximum call depth after type checking. Use lim --stack-usage INPUT to inspect a static upper bound for generated code from main and each thread entry point, including frames, stack temporaries, outgoing arguments, alignment, generated helpers, and the limiting internal call chain. The analysis follows emitted control flow and reports positive stack-growth loops as unbounded. Any reachable external or indirect callee makes the total unknown; the report shows the known generated portion and the unresolved callees. Runtime startup and external-library stack use are excluded, so finite Lim call depth alone is not a guarantee against stack overflow.

The report recognizes local assembly labels and follows both edges of each conditional branch, including early returns and generated thread error paths. It tracks frame-pointer save/restore operations and includes return-address space for external calls in the known portion. Unsupported stack-pointer updates or inconsistent frame-pointer states produce an analysis error instead of a numeric bound. This analysis describes the emitted assembly; it does not measure the operating system's available stack.

Division by zero, invalid dynamic shifts, failed assertions, #panic, and #unreachable lower to runtime traps. Intentional trap examples are kept separate by the repository’s native sweep.

Compiler pipeline

The library exposes these stages:

1. lex converts source into tokens with byte and line/column spans.
2. parse builds untyped S-expressions and preserves #generate as Expr::Generate.
3. parse_program or parse_program lowers declarations and builtin forms into the typed program representation, including generated forms and concrete generator expansions.
4. check_types validates declarations, expressions, layouts, patterns, calls, constants, mutability, and the acyclic call graph.
5. generate_assembly emits native x86-64 assembly.

Public Rust API

The crate is dependency-free. Its primary public types and functions are:

• lex(&str) -> Result<Vec<Token>, LexError>;
• parse(&str) -> Result<Vec<SpannedExpr>, String>;
• parse_program(&str) -> Result<Program, String> for Lim programs and surface notation;
• check_types(&Program) -> Result<(), String>;
• generate_assembly(&Program) -> Result<String, String>;
• wasm::check(&str) -> Result<(), Diagnostic> for self-contained browser input;
• wasm::compile(&str) -> Result<wasm::Module, Diagnostic> for the scalar WebAssembly teaching backend, with runtime contract audits enabled;
• render_diagnostic(&Diagnostic, source, filename) -> String and render_error(source, filename, error) -> String for Rust-style terminal source excerpts;
• format_source(&str) -> Result<String, String>;
• compile_source_to_assembly and link_native_binary, which return Result<_, Diagnostic> with stable phase codes for lexer, parser, generator, analysis, code generation, assembler, and linker failures;
• write_generated_sources_diagnostic for recoverable generator-materializing diagnostics;
• write_generated_sources(&str, &Path) -> Result<(), String>;
• AST and metadata types: Span, Token, TokenKind, Expr, Type, Statement, Function, Item, and Program.

Tooling can use Diagnostic and DiagnosticCode for stable high-level error categories (E1000 lexing, E2000 parsing, E3000 generators, E4000 typing, E4100 borrowing, E4200 linear ownership, E4300 unsafe checks, E4400 contracts, E5000 code generation, and E6000 linking). Diagnostics carry an optional source span and structured notes; legacy string-returning APIs remain available for compatibility.

Borrow failures include the E4100 code, function and statement context, and source locations for recognized borrow operators and the conflicting access. Function-body type errors retain parsed expression trees and generally point at the offending value or identifier; some checks still report the enclosing expression or statement. Generated forms retain source context through parsing, so generator failures remain associated with their invocation. For mismatched operands of explicitly typed builtin expressions, the diagnostic mapper uses the reported types and typed syntax to underline the incompatible operand when it can identify one; this also works for top-level initializers and typed numeric literals. Named-call and struct-literal validation retains source spans through lowering, so unknown or duplicate names and missing-argument/field forms underline the responsible identifier or argument/field list. Declaration uniqueness and unsafe-impl validation likewise underline the repeated or invalid name instead of the whole declaration. C-layout discriminant and thread-task declaration diagnostics target the invalid discriminant, worker name, result type, or aggregate field type. Thread-task handles in function signatures and type aliases underline the generated task type token. Import resolution errors underline the path string, and unknown cfg keys underline the referenced key. Thread-worker Send errors underline the failing parameter type. When #if branches have different types, the incompatible branch value is selected without confusing a similarly typed condition expression. For #match result mismatches, span selection only considers arm values, not the scrutinee or patterns. Named-call argument type errors include the parameter name internally, allowing the diagnostic to underline the responsible named value rather than the call. Struct-literal field type errors similarly underline the named field value, even when an earlier field has the same actual type. Enum constructor payload type errors identify the failing payload position and underline that argument. Unknown named types in local #let annotations underline the type token, including diagnostics formatted as expected-type mismatches. Immutable-assignment diagnostics underline the target binding. Named-type mismatches in destructuring lets underline the annotation, even when the pattern constructor has the same name. Mutable-borrow-through-immutable-reference diagnostics underline the owner. Invalid condition, array-index, and shift-count diagnostics underline the offending operand. Type errors for invalid index, slice-of, slice-len, get, get-payload, and deref-set operands underline the argument with the incompatible shape. Builtin arity errors underline the operator identifier, retaining its qualified spelling in source. Unresolved function calls underline the callee name. Non-exhaustive match diagnostics underline the #match keyword. Generator capability-contract errors underline the implicated operation name, including the second spelling in a duplicate-operation error. Generator-function recursion errors underline the recursive #gn-call target. Duplicate generator parameters underline the repeated parameter name. Unknown worker parameter types are resolved to the worker signature even when an unrelated earlier local has the same name. Call safety errors for #call and #unsafe-call underline the callee; raw-pointer operation errors underline the offending builtin name. Duplicate capability/type pairs and duplicate generator declarations underline the repeated type or generator name. Invalid array/struct assignment targets underline the named target. Missing fields and enum payload variants in get expressions underline the unresolved member name. Unknown enum variants in match arms underline the pattern token. Unknown enum variants in #let-else patterns do likewise. Repeated boolean, enum, and wildcard match patterns underline the later duplicate. Out-of-range and repeated integer match patterns underline the offending literal. Range-pattern diagnostics underline the invalid range, or its upper bound when the bounds are reversed. Duplicate character match patterns underline the later character literal. Enum match payload-arity errors underline the affected variant pattern. An explicit #return whose value does not match the function return type underlines the returned expression. Tuple and array constructor element type errors underline the specific incompatible element, even when another element has the same actual type. Aggregate constructor arity errors underline an extra value or the constructor head when an element is missing; nested tuple mismatch coverage confirms the inner expression does not steal the outer diagnostic span. Borrow conflict spans select the accessed binding rather than a same-named field selector, call callee, or named-argument label in the same expression.

The CLI renders errors with an available span or line/column as a source hunk with an underline. The parsed source tree retains recursive spans, and the type, ownership, borrow, unsafe, generator, and code-generation phases use them where their checks identify a source expression. Statement-level checks prefer their value expression over the enclosing statement when a more precise token or projection is not available. In that case the diagnostic uses the smallest retained expression or declaration span. The UI suite requires each diagnostic fixture to assert an exact source fragment and underline width, or a custom exact-alignment check, so future diagnostics keep this source-location contract. Diagnostic source hunks expand tabs at four-column stops before aligning the underline, and account for common wide and combining Unicode characters, so the displayed code and caret use the same columns. Lexer column positions count Unicode scalar values rather than UTF-8 bytes. Extremely long source lines are rendered as a bounded excerpt with ellipses; the underline stays aligned to the original source column. When a global constant expression contains a function call, its codegen diagnostic highlights the nested #call form rather than the whole initializer. Imported-source parsing retains lexer and parser spans directly, including quoted tokens with internal whitespace and escaped quotes, instead of reconstructing a one-character range from line and column. UI regression tests verify exact caret columns for unknown identifiers, recursive calls, and code-generation failures, including highlighted widths, as well as checking their lines. The UI rejection fixtures also pin type-as-constructor, positional-call, generic declaration/call, missing-#case, and aggregate-layout-overflow diagnostics (tests/ui/{type-as-constructor,positional-call,generic-function, generic-angle-call,match-missing-case,aggregate-layout-overflow}.lim). The aggregate overflow diagnostic covers the declaration and caps its underline at the renderer's documented 80-column limit. Complete positive examples in this reference are compiled through native assembly generation by tests/language_docs.rs; stack-bound examples are additionally checked by the stack-usage report tests, including the external-callee unknown-bound case. Repeated moves of linear fields and array elements identify their repeated #get or #index projections. The UI tests also verify full unterminated-string spans and zero-width EOF locations for incomplete lists. Each UI fixture must provide an exact highlighted fragment or an explicit custom caret-alignment assertion.

Span offsets are byte offsets into the original UTF-8 source. line and column are one-based. Lexer failures carry a LexError; parser failures from the lower-level parser carry source spans in ParseError when using the parser internals exposed by the AST path.

Grammar and builtin semantics

The core grammar is:

program       = { form } ;
form          = atom | list | quote | quasiquote | unquote | splice ;
list          = "(" { form } ")" ;
quote         = "'" form ;
quasiquote    = "`" form ;
unquote       = "," form ;
splice        = ",@" form ;
atom          = symbol | integer | float | character | string | "#generate" ;
symbol        = identifier ;
identifier    = { letter | digit | "_" | "-" | "." | ":" | "@" | "?" | "!" | "+" | "*" | "/" | "<" | ">" | "=" | "&" | "|" | "^" } ;

Whitespace and slash-to-end-of-line comments may occur between tokens. Builtin declaration and statement forms are the #-prefixed forms described in the tables and sections above; arithmetic and comparison forms include their type and overflow mode in the identifier. #let, #let-mut, #borrow, #borrow-mut, #return, #unsafe, #drop, #forget, and #clone define ownership and borrow behavior; #cfg-* is compile-time only; #gn-* is generator-time only; and #generate declarations expand before ordinary parsing, type checking, and borrow checking. Unknown prefixed forms are rejected rather than treated as future keywords.

Examples and verification

The examples/ directory contains programs covering arithmetic, all integer widths, floating point, constants, statics, arrays, tuples, structs, enums, patterns, loops, generated optional/result types, aggregate ABI paths, and external functions. examples/fibonacci.lim computes Fibonacci(10) and exits with 55.

Run the complete native check with:

nix develop --command ./scripts/native-sweep.sh

The sweep compiles and links every example, executes it, and reports ordinary successes, intentional traps, and compiler/linker/timeout failures separately. # Generated thread calls {#generated-thread-calls}

Spawn and join are ordinary named calls, including when the compiler derives their signatures from a short #thread-task declaration. Spawn uses the worker's parameter names; join uses task. For example, write (#call Task::join ((task handle))). Generated enum variants in #case patterns retain their constructor syntax. There is no positional-call exception for generated thread functions. # Floating-point global evaluation {#floating-point-global-evaluation}

Float constants and static aggregate fields retain their declared f32/f64 bit representation. Each arithmetic operation rounds at its operand width, including intermediate f32 results; it is not an integer conversion or a single rounding at the end of an expression. Literal tokens must be finite, but pure arithmetic can produce infinities and NaNs, as at runtime. Signed zero is preserved. NaN payload bits are not a portable equality contract. Pure float arithmetic, named constants, and supported constant conditionals may initialize globals; calls and runtime effects remain forbidden, and constant dependency cycles are errors. Reading or writing statics still requires #unsafe.

(#struct RefValue () ((value (#ref #u64))))
(#fn read-value ((words (#slice #u64))) #u64
  (#let restored RefValue (#unsafe (#word-read RefValue words)))
  (#let answer #u64 (#deref (#get restored value)))
  (#forget restored)
  (#return answer))

(#fn main () #u64
  (#let seed #u64 42u64)
  (#let-mut words (#array #u64 1) (#array-repeat 0u64))
  (#unsafe (#word-write RefValue (#borrow-slice-mut words)
    (#struct-literal RefValue ((value (#borrow seed))))))
  (#let answer #u64 (#call read-value ((words (#borrow-slice words)))))
  (#forget words)
  (#return answer))

What the compiler verifies

• A call has evidence for every declared requirement.
• Successful #if-valid branches grant facts about exactly the checked subjects.
• Joins retain facts common to every continuing path.
• Possible writes revoke facts and saved Boolean evidence that depend on them.
• Structural read/write footprints cross calls; semantic contracts require explicit annotations at every intermediary.
• Constrained bindings, fields, parameters and results require evidence.
• Fixed storage constraints must be restored when exclusive loans end. A returned/reborrowed alias carries the same obligation.
• Specifications name pure Boolean predicates or typed scalar comparisons and type-correct, pure observations. Unsupported analysis fails closed.

It does not prove #ensures, #preserves, or #assume true. These are the explicit trust boundary. Instrumented execution audits function promises over the exercised inputs; tests cannot establish their universal correctness. Requirements and restoration rules remain compiler obligations in production.

Local analysis

src/contracts replaces the former src/proof and src/theorem.rs modules:

• mod.rs collects explicit clauses and constrained types before erasure.
• summaries.rs records transitive structural reads, writes and returned reference origins. It never infers semantic contracts.
• flow.rs tracks subject identities, predicate facts, dependency versions, branch joins, mutable loans and fixed storage obligations.
• lowering.rs erases ghost forms and optionally emits native contract checks.

Facts are opaque named applications, matched by predicate and argument identity. There is no SAT solving, arithmetic implication discovery, predicate unfolding, symbolic execution of function bodies, or hidden runtime proof object. The rule checker follows ordinary control flow and declared interfaces. Checked function/type metadata is tied to its lowered AST; modifying a parsed program cannot retain contracts for a different body.

Typed scalar comparisons also form exact atomic facts. They carry their operator, scalar type and operand identities; a comparison does not imply a different bound automatically. Explicit helper calls may require one claim and promise another through #ensures, audited in instrumented execution. This is contract-directed code, not a separate proof kernel or tactic engine.

Scalar comparisons can use ordinary named calls, for example (#call #usize::lt ((left index) (right 4usize))). The compiler generates the typed intrinsic signature and lowers it to the same operation and fact identity as (#usize::lt index 4usize). This spelling change introduces no new inference.

#index-proven accepts a reference to a fixed array and a #usize index. Its implicit requirement is exactly (#usize::lt index N) for the array length. Production omits the bounds check; instrumented lowering uses ordinary checked indexing at the access. Named predicates require an explicit helper to establish the comparison claim. index_contracts.lim demonstrates the helper, a constrained index assignment and the proven access. Ordinary #index and dynamic slice operations retain their checks.

#generate #array emits concrete accessors with explicit comparison requirements, a named bounds validator and an explicit prove-in-bounds helper connecting its claim to the required comparison. Copy elements also receive a by-value getter; linear elements use shared or mutable borrows. These are inspectable ordinary functions, checked and instrumented like handwritten code. generated_array.lim demonstrates intrinsic calls, a programmer-written implication helper and a generated getter.

Ordinary functions in programs containing async code retain their original contracts across planning. The completed generated program receives normal evidence checking and instrumentation. Planning uses checked projections and cannot authorize a production proven access.

Writes to a sibling field need not invalidate a predicate that only reads the other field. Unknown aliases, raw memory and opaque effect boundaries use conservative invalidation rather than assuming disjointness. Baseline Lim ownership, initialization and borrow checking remains mandatory.

Runtime behavior

Use lim --check-contracts INPUT ... or --cfg contracts=check for test builds. contracts=test also enables assertions through CompileConfig.

An assumption never disables an independent contract assertion. A predicate failure uses Lim's normal panic path. Panic/divergent exits have no normal postcondition obligation.

Deliberate boundaries

The checker matches conjunctions of named predicates. Disjunction does not grant either operand, and an ordinary #if grants no evidence. Equal arithmetic expressions or two predicates with equivalent bodies are not interchangeable. Loops use conservative entry facts; no induction or inferred loop invariant is performed. Unknown aliasing may require explicit validation or a contract.

After an element reference ends, its owner stays unavailable for general use until the fixed invariant is restored. A base-input predicate can observe the owner for validation, or #assume can supply the closing evidence without execution. A mutable reference returned while an invariant is open transfers that pending obligation; the call does not claim the owner is already valid.

Fixed arrays are expanded up to 1024 constrained elements; type traversal has a depth limit of 64. At most 4096 facts and 200,000 local analysis steps are accepted. Individual identities are limited to 16 KiB; cumulative identity and state-snapshot work is limited to 64 MiB of logical analysis data. These work weights are not a measurement of compiler RSS. Exceeding a limit rejects the program without accepting partial evidence.

#old supports snapshot observations rather than mutable reference handles. Dynamic containers should place a named predicate on the whole collection, for example #where (value VecU64) (sorted (&value)), rather than depend on inferred elementwise relationships. Unsupported nested constraint shapes are rejected with a diagnostic; they never silently lose their requirements. Nested constraints in slices, raw pointers, pinned owners, atomic slots, enum payloads and recursive aggregates currently require a predicate on the enclosing value. Constrained global storage is rejected; construct validated values in functions. Constrained reference handles use immutable bindings; #ref-mut still permits mutation of the referent. Mutable parameter bindings cannot appear directly in postconditions; use scalar #old observations or return the value.

Reproducible pathological benchmark

The ignored unit benchmark constructs nondeterministic initialization histories at two storage widths. It asserts that bounded rejection occurs, and prints elapsed time, the state/fact budgets, and the diagnostic. It does not compare timings against a flaky CI threshold or accept a partial result.

bash scripts/limited-run.sh nix develop -c \
  env CARGO_PROFILE_TEST_DEBUG=0 CARGO_INCREMENTAL=0 \
  cargo test --lib pathological_specialization_reports_bounded_work \
  -- --ignored --nocapture --test-threads=1

For end-to-end release compilation use scripts/benchmark-compile.py with its reference/scoped/snapshot/async workload switches and a retained baseline. Use --timings on a compile or --check command to inspect stage contributions. Record build profile, target, corpus, and cold/warm cache state with results.

tests/seeded_safety.rs also contains the ignored pathological_reference_programs_report_cold_and_warm_check_codegen_times benchmark. It compiles actual balanced 8/32/128-target reference-selection programs, reports first/cached passes, and asserts identical assembly. It measures the in-process frontend and assembly generation, not process startup or linking:

bash scripts/limited-run.sh nix develop -c \
  env CARGO_PROFILE_TEST_DEBUG=0 CARGO_INCREMENTAL=0 \
  cargo test --test seeded_safety pathological_reference_programs \
  -- --ignored --nocapture --test-threads=1

One local debug-profile run under the resource limits below produced:

The initialization-history model rejected at 128 states in 0.30 ms for 16 fact columns and 23.53 ms for 4096 columns. These are diagnostic workload samples, not release performance claims or a before/after speedup measurement. Re-run the retained benchmarks on the same profile and host when comparing changes.

Development commands should run through scripts/limited-run.sh. Its current aggregate scope enforces 2 GiB RAM, no swap, two CPU equivalents, a process limit, a ten-minute timeout, one Cargo build job, and serial Rust tests. These external limits protect the host independently of the compiler's internal proof budgets.

Build and serve

The Nix shell includes the Rust WebAssembly standard library, Node and Pandoc. No npm packages, wasm-bindgen, JavaScript frameworks or Rust crates from a registry are required.

bash scripts/limited-run.sh nix develop -c bash scripts/build-playground.sh
python3 -m http.server 8000
# Open http://localhost:8000/docs/playground.html
# Read http://localhost:8000/docs/

Serve the repository root so links to examples also work. The HTML handbook can also be opened directly from disk. The playground needs HTTP because browsers restrict local module workers and fetching WebAssembly from file: URLs.

docs/lim-compiler.wasm is generated output, excluded from Git. Static hosting needs this file alongside the HTML, CSS and .mjs files. The release profile is wasm; the build script copies the resulting artifact into docs/.

docs/index.html is the website homepage: design introduction, tutorial and full reference. A static host can serve docs/ at /, with the repository's examples mounted at /examples/.

Rebuild the handbook after changing its Markdown sources or styling. The check verifies synchronization, every internal anchor, and the absence of scripts or fetched resources:

bash scripts/limited-run.sh nix develop -c python3 scripts/build-reference.py
bash scripts/limited-run.sh nix develop -c python3 scripts/build-reference.py --check

Supported browser programs

The backend emits from validated typed bodies. It runs the same type, ownership, borrow and predicate-evidence checks as native compilation. Contract runtime audits are enabled. It does not reinterpret source in JavaScript or bypass the checker when it encounters a feature it cannot emit.

#usize and #isize retain their existing 64-bit Lim scalar meaning here; they are not browser linear-memory addresses. Unsigned 64-bit results display without truncation, using JavaScript BigInt at the boundary. Unit displays as (). The native backend remains the route for the full runtime language.

The emitted example module has no memory or host imports. The first backend is intentionally a teaching subset, not a portable implementation of the native standard library, an FFI, or a WASI runtime. Unsupported code generation produces an explicit diagnostic. Check only does not require a runnable main.

Bounds, cancellation and failure

• Source input is limited to 32 KiB of UTF-8.
• Runnable output is limited to 64 reachable functions and 16,384 typed nodes per reachable function. Unused functions are checked but not emitted.
• The Rust compiler module has an 8 MiB stack and a 256 MiB linear-memory cap. Memory exhaustion, stack overflow or a compiler trap stops that worker.
• Compilation and example execution run off the page’s main thread. Each action uses a fresh worker, which is terminated when complete, cancelled, or after the 10-second total deadline. Stop can interrupt an infinite example loop.
• These limits supplement the compiler’s own analysis budgets. No result is accepted by weakening a failed proof or skipping ownership checking.

A runtime trap can come from #panic, #assert, a failed contract audit, division by zero or an invalid shift count. A compiled module is still available for download when execution traps. A compile diagnostic has the native error code, source position and excerpt. Editing the source does not change an already-running example; rerun it for a new result.

Compiler interface

lim-browser is a small cdylib wrapper over the lim crate. Its exported ABI version is 1. Only the following entry points and compiler linear memory are needed by the host:

Write UTF-8 into the input buffer, call lim_compile, then copy the output. A later call or memory growth can invalidate earlier buffer views. The wrapper never dereferences a caller-supplied pointer. Status 0 contains raw Wasm bytes; statuses 1 and 2 contain UTF-8 text. A compiler trap invalidates that worker; create a fresh one instead of resuming it.

Native Rust callers can use lim::wasm::check(source) and lim::wasm::compile(source). compile returns module bytes plus a ReturnType; both functions return regular Diagnostic errors. Neither uses a disk cache.

Verification and extending the backend

bash scripts/limited-run.sh nix develop -c \
  env CARGO_PROFILE_TEST_DEBUG=0 CARGO_INCREMENTAL=0 \
  cargo test --test wasm_backend
bash scripts/limited-run.sh nix develop -c node scripts/check-playground.mjs
# Optional UI smoke test; requires Chromium on PATH (or set CHROMIUM).
bash scripts/limited-run.sh nix develop -c node scripts/check-browser-ui.mjs

The engine tests execute emitted modules, check integer boundaries, branches, loop control, short-circuit evaluation and contract evidence, and reject unsupported features. The artifact test loads the actual Rust compiler Wasm, compiles the page’s example templates, checks diagnostics and unsigned results, and verifies runtime postcondition and shift traps. The Chromium test also checks the worker deadline, cancellation, mobile layout, browser Find and the manual’s absence of scripts or fetched resources. Its process/thread flags keep headless Chromium within the development runner’s process limit.

src/wasm.rs consumes checked typed_body nodes, rather than adding a second type checker. Extend its explicit supported cases and add execution tests before advertising another feature. Memory-backed values and aggregate layout need a separate design; silently representing references as integers would lose the language’s guarantees.

Background specifications: Rust’s browser target, WebAssembly binary instructions, instantiating a module and terminating a worker.