Effect contracts#

An effect contract describes what a function may observe or change in addition to its input and return types. Types answer which values cross a call boundary; effects answer what else can happen while the call is in progress.

This contract says that identity reads value and that its first return is the same table as value. It does not write through the table, change its shape or metatable, let it escape, allocate, yield, raise, or invoke opaque external behavior.

@effects is type-erased. It adds no runtime guard and changes no calling convention. Its consumers are the checker and optimizations that need to know whether a call can invalidate a proof.

Complete upper bounds#

An @effects contract is a complete upper bound, not a list of interesting effects and not an instruction to infer the omitted members.

@effects() means no observable effects in the effect model. Every list is empty and every boolean is false. If the body performs an omitted effect, the checker reports NUPP2112.

The contract above is rejected because the body writes through values and, conservatively, may change its shape. The corresponding complete contract is:

Declaring more than the body currently does is valid. That is what makes a contract an upper bound: an implementation may become less effectful without changing its contract. Declaring less is invalid because a caller could then make an unsound decision from the missing fact.

Where contracts are checked and trusted#

The meaning of an effect annotation depends on whether its implementation is visible.

A visible body cannot use an annotation to hide what it does. A declaration without a body necessarily crosses a trust boundary, just as an FFI type signature does: the compiler records the promise but cannot prove the foreign implementation honors it.

external = true says that the call may interact with state outside the parameter-rooted paths in the contract. Omit it only when the declaration's implementation really is contained by the other members.

For a bodyless Nupp declaration, @effects can be combined with const:

The two promises are independent. @effects describes calling the value; const says the binding continues to hold that same value. This trusted use of const belongs on bodyless declaration surfaces such as .d.nupp files. Do not apply it to an ordinary module merely to suggest that the module is stable: the promise is shallow and says nothing about mutation of its fields.

Contract members#

Every argument is named. The contract is closed: an unknown member, a repeated member, a list member that is not a literal array of strings, or a boolean member that is not literally true or false is NUPP2112.

Path-valued members#

Boolean members#

All eleven members are optional. Omission means an empty list or false, not unknown.

Paths and roots#

Paths are symbolic strings. Use these canonical roots:

Examples:

The current checker treats path entries as opaque strings after validating that their container is an array and each entry is a string. It does not yet reject a noncanonical path spelling. Consumers compare paths exactly, so use the forms documented here: "value" and "value[*]" are distinct facts, and one does not imply the other.

That exactness matters for visible bodies. Merely evaluating a parameter is a root read; a recognized operation such as rawget(value, key) may additionally produce an element read. When NUPP2112 names a missing path, add the exact fact only if it is part of the intended public contract.

self, $global, calls, and metatables are principally declaration vocabulary today. Visible-body inference is parameter-centric; where it cannot map state back to a parameter, it may report $capture or widen to unknown instead of producing one of those more specific paths.

Return aliases#

returns uses N=path, where N is a one-based result position.

This does not describe the result's type—that remains the return type annotation. It says the result and argument may be the same object, which is the fact alias analysis needs.

Multiple results name their positions independently:

Return aliases propagate through direct visible calls:

The second contract is verified from the first summary. A fresh table returned from a function is not a return alias; describe the allocation with allocates = true.

Allocation, raising, and yielding#

The non-memory flags describe behavior that cannot be located at one path.

Table expressions and nested function values are allocations in the current analysis.

Direct calls to error and assert set raises. A direct coroutine.yield sets yields. These facts also propagate from a directly resolved visible callee.

For the user-facing control-flow model, including nosuspend, cancellation, coroutine inheritance, and concurrent combinators, see suspension. Suspension handlers own the scheduling policy. This page stays focused on complete @effects contracts.

raises is an optimizer effect, not a replacement for API documentation. Public failure conditions still belong in @raises docblocks, and never still describes a function that never returns normally.

Writes, shapes, and metatables#

writes and shapes answer different questions:

• writes = {"values[*]"} says an entry may receive a different value.
• shapes = {"values"} says the set of entries or array boundary may change.

The current inference deliberately classifies an indexed parameter assignment as both. It does not try to prove that values[1] = replacement replaces an already-present slot rather than inserting or removing one. This conservative choice may reject an optimization, but it cannot authorize one from a shape fact that was too narrow.

Writes through a nonlocal table are summarized under $capture; writes to a table local to the function do not become caller-visible path effects unless that table escapes.

metatables is primarily declaration-facing today. It lets a foreign or bodyless contract say that behavior derived from a metatable can change. A consumer that depends on ordinary raw table behavior must stop when a relevant metatable effect is possible.

Escape facts#

An escape says that an argument may remain reachable somewhere the caller does not control after the call returns. Storing an argument into captured state, global state, or through another reference is conservatively an escape.

Returning the argument is represented by returns, not escapes, because the alias remains explicit in the call's results.

An escape does not itself say the value is later mutated. It says that a later proof cannot assume the caller owns the only reference.

Calls and fixed-point propagation#

The checker collects visible functions in the file, identifies direct calls by definition rather than spelling, and repeatedly joins callee effects into callers until the summaries stop changing. Recursive and mutually recursive groups therefore converge to one conservative fixed point.

Parameter-rooted paths are substituted at a call site. If a callee writes items[*] and the caller passes its own parameter values, the caller acquires writes = {"values[*]"}. Effects on local scratch values stay local. Effects that cannot be mapped safely widen toward captured or unknown state.

This propagation is currently file-local. Calls through imported modules, computed function values, unresolved methods, or other definitions without a summary are unknown. Effect summaries are not yet serialized into the cross-module incremental interface.

The calls list itself is currently carried by declared summaries and propagated into callers; inference does not enumerate every directly observed call into that list. A direct known call contributes its callee's other effects, while an unknown call widens the whole summary as described below.

Unknown calls and top#

Unknown code is pessimistic by default. An unresolved call widens the inferred summary to top, meaning no finite @effects(...) contract can verify the visible body.

The example is rejected: external = true is an ordinary declared effect, not a spelling for “accept arbitrary unknown behavior.” The checker cannot prove what callback does, so the visible implementation cannot claim a complete finite contract.

The current analysis recognizes a deliberately small set of builtins rather than treating every prelude function as unknown:

• type, tonumber, select, and rawequal;
• rawget, rawlen, ipairs, pairs, and next;
• error and assert as raising;
• coroutine.yield as yielding.

Everything else needs a directly resolved visible summary or remains unknown. A same-file function definition takes precedence over this list. The fallback recognition is otherwise spelling-based today, so do not rely on an unresolved value shadowing one of these names when writing a verified contract.

How contracts are verified#

For each visible function carrying @effects, the checker:

1. creates parameter-rooted alias classes for direct local aliases;
2. walks the body conservatively, without entering nested function bodies;
3. propagates summaries from directly resolved callees;
4. repeats propagation to a fixed point across the file;
5. checks that every inferred path, flag, and return alias is present in the declared contract.

The comparison is set containment. Order and duplicate path strings have no semantic effect after normalization, although repeating a named member such as two separate reads = ... arguments is invalid.

The first missing fact is reported as NUPP2112, for example:

@effects contract is missing shapes = "values"

An unknown call instead reports that the contract calls code with unknown effects. The annotation points at the function declaration; optimizer remarks, when applicable, point at the call or mutation that stopped a proof.

Inference without an annotation#

Visible functions do not need @effects merely so the compiler can analyze them. The checker infers a summary whether or not an annotation is present, and same-file optimizations may use that inferred summary.

Add @effects when the contract itself is valuable:

• an API boundary should make side effects reviewable;
• a visible implementation should be prevented from silently growing new effects;
• a bodyless or C declaration needs a trusted summary;
• a future implementation must preserve a stable optimization interface.

Do not mechanically annotate every private helper. An inferred private summary can change with its body; a declared complete contract becomes an obligation that every later edit must continue to satisfy.

Optimizer interaction#

The numeric ipairs pass is the first consumer. It lowers a loop only after a separate dense-entry and alias proof succeeds. Calls in the containing body are then checked pessimistically:

• top or unresolved calls stop the rewrite;
• external, yields, or a metatable effect stops it;
• a shapes effect mapped to the iterated array stops it;
• captured or unresolved shape effects stop it.

An effect contract cannot force the rewrite. The array must still be a visible dense literal with a static bound, its binding must not be exposed elsewhere, and all the pass's other proof obligations must hold. Use -O1 --remarks or -O2 --remarks to see OPT-2 explain why it rewrote or declined a loop.

See Optimization for levels, remarks, pass controls, and the benchmark behind that restriction.

Effects, stability, relaxation, and ownership#

These mechanisms answer different questions:

An effect summary does not imply stability, purity does not imply ownership, and ownership does not imply a call cannot raise or yield. State each boundary with the mechanism that actually describes it.

Current conservative limits#

The effect system is intentionally useful before it is a full program IR. Its current limits are part of the contract with users:

• propagation follows direct, definition-resolved calls in one file;
• alias classes are flow-insensitive and cover direct local assignments and declared return aliases, not arbitrary heap paths;
• there is no CFG/SSA-sensitive effect query yet;
• path strings use canonical conventions but are not yet grammar-validated;
• builtin fallback recognition is spelling-based after same-file resolution;
• imported effect summaries are not yet part of incremental interface hashes;
• unknown calls widen to top rather than accepting an optimistic annotation;
• trusted C and .d.nupp declarations are only as correct as their author.

These choices lose optimization opportunities. They are safe defaults: when the compiler cannot establish a fact, it declines the transformation instead of manufacturing a proof.

Complete member example#

This declaration demonstrates the whole surface. Real contracts should include only the effects the implementation may actually perform.

Because this is a cdef function, the compiler trusts the declaration. The same annotation on a visible Nupp function would be checked as an upper bound on its inferred body effects.

Diagnostic checklist#

When an effect contract reports NUPP2112:

1. Read the missing member or unknown-call explanation literally.
2. Decide whether the implementation should perform that effect.
3. If yes, add the exact path or boolean to the public contract.
4. If no, change the implementation or call a directly summarized helper.
5. Do not use external = true to suppress an unknown visible call; it does not mean “unchecked.”
6. Re-run nupp check before looking at optimizer remarks.

For bodyless declarations, review the implementation on the other side of the boundary: the checker cannot do that verification for you.