Resource ownership, borrowing, and FFI safety#

Nupp gives C pointers and ordinary Lua values the same affine resource model. The checker arranges ordinary lexical cleanup and finds invalid cleanup, double consumption, use after move, dangling lexical borrows, and unproved raw-pointer use before the program runs. The model is intentionally smaller than Rust's: there are no named lifetimes, no typestate and no borrow checker for arbitrary object graphs.

The central rule is:

Safe code must either prove a resource lifetime or name the exact trusted boundary where it stops proving it.

For Nupp bodies, the compiler derives non-escape and transfer effects where it can. For C declarations and other bodyless interfaces, annotations state facts that cannot be recovered from a header. unsafe do is the explicit escape hatch for an address or invariant that the checker cannot prove.

What developers gain#

Plain LuaJIT and FFI provide no static distinction among a fresh allocation, a shared pointer, a pointer retained by C, and an already-freed pointer. Cleanup conventions live in comments and tests. Nupp turns those conventions into checked interfaces:

• a locally droppable owner is destroyed at lexical scope exit unless moved;
• a takes call moves its argument and later use is rejected;
• a derived borrow cannot outlive or be stored away from its source;
• C cannot retain Lua-managed memory without a pinned anchor and a declared release;
• a raw pointer cannot be dereferenced, indexed, or passed through an uncontracted C parameter in checked code;
• a record containing resources is itself an affine resource;
• a raw or unknown coroutine suspension cannot strand a live obligation;
• cleanup remains deterministic and does not depend on a GC finalizer.

This is useful even in small programs because failures are reported at the ownership boundary, not later as a leak, double free, stale callback, or occasional use-after-free.

Ownership syntax#

All ownership syntax is erased or lowered to direct Lua/FFI operations. It does not change the C ABI and does not install ffi.gc finalizers.

Intrinsics live under nupp#

nupp.drop, nupp.borrow, nupp.intoRaw, nupp.fromRaw, nupp.borrowFrom, and nupp.pin are compiler-provided operations on the always-available nupp global:

The old bare spellings remain aliases. They report the same diagnostics and lower to the same code, but new code and these examples use nupp.* so the operation's origin is explicit. Either spelling can be shadowed: a local nupp makes nupp.drop an ordinary field call, just as a local drop makes drop(x) an ordinary call.

Owned results and deterministic cleanup#

An explicit cleanup list is the clearest C-boundary contract:

Cleanup functions run from left to right. drop takes the owner, so it cannot run twice. Passing the value to any takes parameter discharges the same obligation without also running the recorded cleanup:

Every live owner must be discharged along every checked path. A locally droppable ordinary binding is discharged automatically at its lexical scope boundary, including raised and structured exits. A successful drop, takes call, ownership-preserving move, @owned return, or intoRaw inside unsafe transfers or ends that responsibility and suppresses automatic cleanup. Ignoring an owned call result is still an error. Transfer-only owners remain errors unless an explicit terminal consumes them.

@owned works on Nupp functions and managed Lua values too:

A bodyless API may attach the same producer contract directly to a function-valued record or interface field:

The checker verifies the body against the declared return contract, but the claim that the returned external resource is truly exclusive remains a contract. Exclusivity is not observable from a pointer value.

Free cleanup functions are resolved where @owned is declared. A private cleanup therefore crosses a module boundary with the owner contract without becoming a public module field. The declaring module registers its function object under a compiler-owned key; a consuming module resolves that key on its first discharge and then calls the cached function directly. Loading the consumer before the producer is safe because resolution is lazy, and obtaining an owner necessarily ran the producer first.

Cleanup context is owner state#

A resource cannot secretly carry its pool, allocator, arena, or parent handle: ownership annotations erase, and cleanup later needs a runtime place from which to read that context. Make the pair an explicit nominal owner and put the context in its fields. A custom @drop method can then pass every required argument without allocating a closure per owner:

The release contract consumes the connection, so Nupp can check this cleanup without unsafe. The wrapper remains visible in the API because its pool is real runtime state; Nupp does not hide it in a side table or attach a finalizer.

Transfer-only owners#

Use an opaque owner only when another API must accept the value and local code has no valid way to destroy it:

Bare @owned does not mean opaque. Opaque ownership must be conspicuous.

Default drop and Closeable-style interfaces#

@drop marks a consuming operation as the default drop operation. A bare @owned producer uses it when the result type has exactly one default:

A free function can be the default as well, but its resource parameter must be takes:

An interface can declare the contract once and subtypes inherit it:

This gives a Closeable-style abstraction without privileging the name close. The annotation, not spelling, supplies the contract. Bare @owned is rejected when the type has no default or inherits more than one, because the compiler must never guess whether close, free, stop, or another operation is correct.

Parameter effects: takes, borrows, and exclusive#

takes complements borrows: the first transfers the obligation; the second temporarily sees the value.

Shared borrowing allows mutation#

borrows is a lifetime and aliasing contract, not a const qualifier. Nupp is normally single-threaded, so mutation through a shared borrow is allowed when it does not invalidate the identity or lifetime of the resource:

There is deliberately no borrowMut intrinsic and no exclusive<T> wrapper. Exclusive access is a call effect, so the one surface is exclusive:

Use exclusive only for operations that may invalidate derived views, replace storage, reallocate, or otherwise require call-duration exclusivity. Ordinary field mutation belongs under borrows.

What is inferred#

For a Nupp body, the checker derives whether each resource-shaped parameter stays within the call. A read-only or stable-mutation helper needs no annotation:

If a parameter is returned without a borrowing-return contract, stored, captured, or sent through an untyped/indirect call, it is conservatively escaping. A borrow cannot be passed there:

Explicit borrows remains useful because it pins intent and improves error locality:

Without the annotation, adding that store changes the inferred interface and errors appear at callers that provide borrows. With it, the implementation change is rejected at the declaration.

Inference cannot originate facts outside a body. cdef declarations, .d.nupp overlays, callbacks supplied by another module, and indirect calls therefore need explicit contracts or conservative treatment. Resource exclusivity, cleanup choice, and whether C retains an address are never inferred.

Lexical borrows and result provenance#

nupp.borrow(owner) is the explicit lexical form. It is useful when a named view must keep the owner immovable for part of a scope:

Most calls do not need nupp.borrow(...): passing an owner to a borrows parameter borrows it implicitly for the call.

Borrows may be read, mutated stably, and reborrowed. They may not be returned without a result contract, stored in a table or field, assigned to an outer binding, captured by a closure, or moved into an untyped call.

A returned view names its source:

The result keeps pool borrowed until the result's scope ends. Methods may use borrowed<T> return sugar when the receiver is the only source:

Layered resources can be both owned and dependent:

The TLS session must be dropped, and the socket cannot be dropped until that happens. A result may name several roots:

For functions with bodies, the checker traces returned expressions and rejects a claimed source it cannot prove. When provenance really travels through opaque pointer manipulation, assert it at a narrow unsafe boundary:

Bodyless foreign declarations remain trusted contracts because there is no implementation to inspect.

Capability-preserving generics#

Payload type parameters do not erase the capability beside a value. A result relation names the input slot whose exact cleanup order, opacity, roots, pin, retention state, and affine identity move to the result:

Visible identity and narrowing bodies infer this relation. Bodyless interfaces state it explicitly. assert and setmetatable use it, so narrowing an optional owner does not lose its producer-specific cleanup. A generic body that duplicates, stores, or abandons its argument remains callable for plain values but rejects an affine instantiation.

Raw pointers and unsafe#

Raw pointers are allowed, but validity-dependent use requires unsafe unless the value is owned, borrowed, pinned, or passed through a declared lifetime effect. This is rejected:

The unchecked operation is explicit:

The same rule covers raw pointer indexing and passing a raw pointer to a plain C pointer parameter. Give the C parameter a truthful borrows, exclusive, takes, retains, or releases contract to use it from checked code.

Foreign calls without lifetime contracts#

When a C API lacks those annotations, the wrapper still has to retain its allocator context, but its cleanup must put the trusted boundary at the call:

This FFI-shaped pair is a struct because its C pointers have a fixed layout and need no Lua-table features. A record would also be valid when table identity, dynamic fields, or GC-managed state are useful.

unsafe grants permission for unproved pointer operations. It does not suppress affine obligations or turn off the checker. Owners still must be discharged, borrows still cannot escape, and lexical cleanup still runs:

Abandoning and reconstructing tracking#

Both directions require unsafe because each discards a proof or asserts one:

fromRaw does not discover ownership. It asserts that this exact value is now exclusive and associates the named cleanup list. A false assertion can still double-free, so small unsafe blocks are easier to audit than ambient unchecked FFI code.

C output parameters#

C APIs often return status separately from a pointer written through T **. Nupp declarations can expose that as an ordinary multiple return without changing the ABI.

Owned outputs#

The generated call allocates the output slot, passes it in its original C parameter position, calls C once, and appends the logical output to the Lua return list. On failure, a conditional output is nil.

success accepts always, zero, nonzero, or a literal number/string. Use one annotation per output; multiple outputs preserve both C argument order and Lua return order. Every owned output needs an explicit cleanup name or list.

Borrowed outputs#

A borrowed output must name the input that keeps it valid:

The from parameter must itself be a borrows input. This prevents an output annotation from inventing provenance unrelated to the call.

C retention and Lua-managed memory#

A call-duration borrow is insufficient when C stores an address after return. Create a pinned<T> handle and describe both ends of the retention:

The generated C call receives handle.pointer, not the Lua handle table. Duplicate retention, release before retention, leaving scope while retained, or passing an unpinned address is rejected. The releases annotation promises that C stops retaining the pointer before the call returns.

Callbacks are an opaque derivation and require a narrow unsafe construction, then a pin restores a checked lifetime:

Automatic lexical cleanup#

An ordinary owned local runs its recorded cleanup at its lexical boundary:

Acquisitions occur left to right and cleanup occurs right to left. Cleanup also runs for early return, loop control, and errors. The local remains movable; moving, returning, or explicitly dropping it deactivates automatic cleanup exactly once. Use drop for early release and an explicit terminal operation when successful completion has protocol meaning. If the body and cleanup both fail, Nupp preserves the body failure as the primary error and reports the cleanup failure with it.

Every cleanup function and @drop body must be non-suspending. A foreign or bodyless cleanup makes this trusted promise; a visible body is checked from its transitive effect summary.

Affine records and resource composition#

A record with owned<T> or pinned<T> fields is itself affine:

When no custom default exists, cleanup is synthesized in reverse field declaration order. Individual affine fields may move out. Their path-sensitive state becomes moved, independent fields remain accessible, whole-record methods are refused, and synthesized drop skips only fields proven moved. Assigning the same exact affine contract back reinitializes the field.

A record may define a custom @drop method. The checker requires that its body discharge every affine field, and it does that by handing each one to a takes parameter — the field's own drop operation:

nupp.drop(self.second) does not work here. drop needs a value whose static type carries a cleanup list, and a field spelled owned<File> records the obligation without recording how to discharge it; that reports NUPP2602 and names the fix. The same applies inside a function to a takes parameter: its erased payload does not carry the producer-specific cleanup witness, so an untouched takes parameter is not automatically destroyed. Its body must use an explicit matching terminal, transfer, or owning return.

Nominal records may also retain declared borrows:

Construction proves bytes derives from the sibling source; the source field cannot be replaced while the dependent field is live. Anonymous and dynamic table storage remains rejected.

Dynamic resource sets#

nupp.resource_set is the audited container for a runtime number of owners:

adopt moves the owner and returns a borrow tied to the set. The compiler reifies that producer's exact cleanup references only at this call. Set cleanup runs registrations in reverse order, attempts every cleanup step, and reports primary and suppressed failures. remove deletes one registration and returns the original capability exactly once. An opaque owner needs an explicit matching terminal consumer as the second argument.

Checked spans#

nupp.span provides ByteSpan and affine ByteWriteSpan views. They retain a root, carry a runtime element count, bounds-check every index and slice, and keep an invalidation barrier live for a write span until commit or scope exit. Direct pointer or variable-length C-array indexing has no runtime bound and is rejected even when its lifetime is rooted. A fixed C array rejects a literal index that is statically out of range and inserts a runtime check for every non-literal index. Conversion, unchecked indexing, and unknown pointer arithmetic remain inside the smallest possible unsafe block.

Coroutines#

Raw coroutines may be abandoned forever, and LuaJIT has no general static join or cancellation guarantee. Suspending with a live owner, borrow, pin, or retained handle is therefore rejected:

Yielding with no temporal obligation is valid. A checked suspension operation may cross obligations because it either blocks to completion or transfers a park to an installed handler whose cancellation must resume and unwind it. Lexically placing raw coroutine.yield inside a handled region does not bless it. Handler shutdown cancels every park before succeeding, and cleanup still cannot suspend while cancellation is discharging another obligation.

Scoped callback parameters are the synchronous analogue: an inline closure may capture a borrow only when the visible callee proves it invokes the callback without storing, returning, retaining, or forwarding it to an unknown target. Owners are never captured by ordinary copyable closures.

What is proved and what is trusted#

Indirect or untyped calls are conservative. If the checker cannot see a callee contract, an owner or borrow may not cross it. Convert through intoRaw in unsafe only when abandoning the guarantee is intentional.

Non-goals and limits#

• No typestate. The checker tracks whether a resource obligation is live, moved, borrowed, retained, or discharged, not arbitrary states such as connected/authenticated/committed.
• No prohibition on shared mutation. borrows permits stable mutation; exclusive exists only for operations requiring exclusivity.
• No automatic terminal choice for opaque or multi-terminal protocols. Ordinary locals auto-destroy only when their exact producer cleanup is known.
• No inference of ownership from names such as new, close, or free.
• No arbitrary affine table storage; dynamic ownership is confined to ResourceSet.
• No proof of C implementation behavior, allocator pairing, cleanup body correctness, or unsafe code.
• No implicit ffi.gc; safe code also rejects attaching it to owned, borrowed, pinned, or retained values because that would create a second cleanup path.

The guarantee is consequently precise: safe Nupp code follows its visible resource contracts. Incorrect foreign contracts and unsafe blocks are the auditable trusted computing base.

Choosing the smallest contract#

Use this order when binding an API:

1. Mark every fresh owning return or output with @owned.
2. Mark destruction/adoption parameters takes.
3. Mark call-duration pointer access borrows; use exclusive only if live views could be invalidated.
4. Mark pointers stored by C with matching retains and releases operations, and require callers to pin managed memory.
5. Name the source of every borrowed return or output.
6. Keep raw operations in the smallest possible unsafe do block.
7. Use ordinary locals for lexical owners and explicit operations for early release or meaningful terminals.

This surface makes the common path short while preserving annotations exactly where inference cannot originate or where a stable public contract is useful.

Run nupp ownership-audit --json [file...] to enumerate foreign pointer parameters/results, every explicit unsafe assertion region, and each recognized raw memory operation inside one. The report is an inventory of the trusted surface, not a claim that the foreign implementation was verified. Add --regions to include deterministic automatic-cleanup region identities, activation and cleanup order, and their protected lowering class.