Effects and Verified Guarantees

Why Effects Matter

Type correctness alone cannot answer every question needed by systems code. A function may have a perfectly valid return type and still be unsuitable for a particular execution context.

The compiler may need to know whether a call can:

• panic;
• allocate storage;
• wait synchronously;
• suspend and resume later;
• create another execution instance;
• perform file, socket or device I/O;
• read or write volatile storage;
• mutate state visible outside local computation;
• depend on time, randomness or another nondeterministic source.

These facts are useful for ordinary APIs, but they become essential for interrupt handlers, embedded targets, bounded-memory code, deterministic cleanup and concurrency analysis.

No General Effect Language

Sec 0.1 does not expose a general algebraic-effect language. There are no programmer-written effect sets, effect handlers or runtime effect objects that must accompany ordinary functions.

The compiler owns the detailed analysis. Source code uses ordinary Sec syntax and, where a stable promise matters, one of the compiler-known verified attributes.

fn ReadConfiguration() Result[Config, ConfigError] {
    ...
}

@noAlloc
fn ParseFixedHeader(input: ref byte[]) Result[Header, ParseError] {
    ...
}

The first function still receives an inferred effect summary even though it declares no effect attribute. The second additionally promises that no reachable path performs dynamic allocation.

Inferred Effects vs Declared Guarantees

Every analyzed callable receives inferred effect information.

fn AddOne(value: int) Result[int, ArithmeticError] {
    let result := try value + 1
    return Ok(result)
}

The compiler may prove that this implementation does not panic, allocate, block or suspend. Those are implementation facts.

A declared guarantee turns the relevant fact into a source-level contract:

@noPanic
fn AddOne(value: int) Result[int, ArithmeticError] {
    let result := try value + 1
    return Ok(result)
}

If a later implementation change introduces a reachable panic-capable operation, compilation fails. The compiler does not silently weaken the declared promise.

Public Contract Boundaries

The absence of an inferred effect is not automatically a public guarantee across a separate compilation boundary.

Public callers may rely on guarantees established by:

• explicit verified attributes;
• interface requirements;
• function or callback contracts once their effect syntax is defined;
• generic constraints that establish the required behavior;
• compiler-known intrinsic contracts;
• target knowledge exposed as part of a target contract.

A private implementation may be more restrictive than its public contract. That can help optimization and local verification without accidentally promising the stronger property to external callers.

Summary May-Effects

Internally, Sec records positive facts describing effects that may occur on at least one reachable execution path. The canonical summary set includes:

These names describe compiler facts. They are not additional function modifiers that ordinary Sec source must spell out.

Effects are combined conservatively. If one reachable path may allocate and another may block, the callable may have both effects even when no single path performs both.

Direct and Transitive Effects

A direct effect is introduced by an operation in the body itself:

fn ReadStatus() Result[Status, IOError] {
    return DeviceRead()
}

If DeviceRead() performs I/O, the call introduces that behavior into the containing function.

Effects are transitive. Reachable behavior includes more than obvious function calls:

• ordinary function and method calls;
• generic specializations;
• closures and indirect function values;
• interface dispatch;
• destructors and automatic cleanup;
• defer bodies;
• implicit compiler-generated operations;
• foreign functions;
• inline assembly declarations;
• target-specific intrinsics;
• task and thread operations.

Path-Sensitive Analysis

An effect contributes only when the corresponding path remains reachable after semantic analysis and required control-flow proof.

if false {
    PanicCapableOperation()
}

The unreachable branch does not make the surrounding function panic-capable.

Proof may also eliminate the failure path of an ordinary checked operation:

if divisor != 0 {
    let result := total / divisor
    Use(result)
}

When the compiler can prove the divisor is nonzero on this path, the division does not contribute a division-by-zero panic effect.

A runtime branch whose alternatives are both possible contributes effects from every reachable branch.

Call Graph and Recursion

Transitive effect verification operates on the active call graph for the selected compilation plan.

Recursive and mutually recursive call groups are analyzed to a fixed point. If one reachable member of a recursive group may allocate, callers in that group inherit the allocation effect unless path or contract proof excludes it.

fn A() void {
    B()
}

fn B() void {
    C()
}

fn C() void {
    A()
}

The compiler does not stop at one call edge. It computes a stable summary for the reachable recursive component.

Unknown indirect call targets are conservative. A strong guarantee cannot be proven by simply assuming that an unresolved call happens to be harmless.

Errors Are Not Effects

Returning Result[T, E] is ordinary typed control flow, not an effect by itself.

fn Open() Result[File, OpenError] {
    ...
}

The function may still allocate, block or perform I/O. Conversely, returning Err(...) does not mean the function panicked.

This distinction keeps expected failure explicit in the type system while allowing effect analysis to describe execution behavior independently.

Runtime Checks and try

Language-defined runtime checks contribute effects according to their control flow. Checked arithmetic is a common example.

let total := left + right

If overflow is possible and ordinary checked arithmetic would panic, the operation may contribute MayPanic.

Using try can convert that supported failure into explicit error flow:

let total := try left + right

The overflow path is then represented as an ordinary error result rather than panic. This can make the operation compatible with @noPanic.

try removes only the failure mode it explicitly handles.

let value := try allocator.New[Value]()

Allocation failure may be explicit and panic-free, but the allocation effect remains. Likewise, try network.Read() does not erase I/O or blocking behavior.

@noPanic

@noPanic is a compiler-verified transitive guarantee that MayPanic is absent from every reachable path covered by the contract.

@noPanic
fn Add(left: int, right: int) Result[int, ArithmeticError] {
    let result := try left + right
    return Ok(result)
}

The guarantee excludes reachable:

• explicit panic;
• panic-capable operations whose safety is not proven;
• panic-capable callees;
• unproven assertions;
• checked-unreachable failures;
• panic-capable cleanup;
• unknown foreign abort or unwind behavior accepted as safe.

@noPanic does not catch or suppress a panic. The compiler proves that the relevant panic path does not exist.

@noAlloc

@noAlloc requires the dynamic-allocation effect to be absent throughout reachable execution.

@noAlloc
fn Inspect(packet: ref Packet) bool {
    return packet.Valid
}

Dynamic allocation includes operations such as:

• heap allocation;
• arena allocation that consumes arena capacity;
• collection growth;
• closure-environment allocation where storage must be acquired;
• task or thread control storage allocation;
• foreign allocation;
• compiler helpers that acquire dynamic storage.

The following are not allocation merely because they exist:

• fixed stack locals;
• fixed arrays;
• static storage;
• addressed storage;
• register values;
• caller-provided storage;
• an arena view over caller-provided storage;
• reuse of already available collection capacity without growth.

Bounded arena allocation is still allocation. @noAlloc means no dynamic allocation, not merely “no heap allocation”.

@noBlock

@noBlock guarantees that reachable execution does not synchronously wait for an unbounded external event or park the current execution domain.

@noBlock
fn PollStatus() Status {
    return ReadReadyState()
}

Blocking behavior includes:

• blocking I/O;
• sleep;
• waiting for a mutex or semaphore;
• condition-variable waiting;
• thread join;
• a task wait classified as blocking;
• scheduler parking;
• waiting for external input without a proven bounded policy;
• foreign calls declared or conservatively treated as blocking.

@noBlock does not automatically forbid:

• ordinary finite computation;
• statically bounded loops;
• nonblocking polling;
• try-lock;
• bounded lock-free retry when separately proven;
• ordinary memory-mapped status reads.

Nonblocking does not mean constant-time. Worst-case latency and execution-time bounds are separate analyses.

Blocking and Suspension Are Different

Sec tracks synchronous blocking separately from asynchronous suspension. A suspending operation may yield execution so other work can proceed without synchronously blocking an execution thread.

Interrupt-safe contracts are stronger: ISR execution may not block, park, yield or resume later as an ordinary task continuation, so those contracts forbid both blocking and suspension.

Spawn, I/O and External State

Some effect facts exist because several analyses need to distinguish behaviors that would otherwise look superficially similar.

Creating concurrent work

Creating a task, thread or other execution instance contributes the spawn effect. The same operation may also allocate, suspend or mutate external scheduler state.

I/O

File, socket, terminal, device, foreign and platform services may contribute MayIO. I/O can be blocking, nonblocking, suspending or polling, so MayIO is not equivalent to MayBlock.

External mutation

Mutating globals, shared state, foreign state, device state or persistent storage may contribute MayMutateExternalState. Mutating a purely local temporary does not by itself do so.

fn Normalize(value: int) int {
    let mut local := value
    ...
    return local
}

Local mutation alone is not externally observable state mutation.

Volatile Access

Access to addressed or otherwise volatile storage is tracked separately as MayAccessVolatile.

Examples include:

• reading from a fixed hardware address;
• writing addressed storage;
• volatile register access;
• compiler-known hardware register operations.

Volatile operations are observable. The compiler may not remove, duplicate, merge or reorder them in ways that violate volatile semantics.

Volatile access is not automatically the same thing as file or socket I/O, and it is not automatically forbidden in interrupt code. Target knowledge decides whether a specific hardware operation is valid in that context.

Nondeterministic Input

A function may depend on information that can vary independently of its ordinary explicit parameters. Sec tracks this separately as nondeterministic input.

Typical sources include:

• clock values;
• random sources;
• environment state;
• process or thread identity;
• uncontrolled external device state;
• foreign nondeterministic input.

One operation may carry several effect facts. A volatile device read may also be nondeterministic, for example, without collapsing the two concepts into one flag.

Interrupt Contracts

Interrupt attributes are composite verified contracts. They combine effect analysis with stack, target, ABI and synchronization requirements.

@interruptSafe

@interruptSafe verifies that a function or method may be called from ISR code. It does not bind an interrupt vector and does not turn the function into an ISR entrypoint.

The contract requires at least:

• no reachable panic;
• no dynamic allocation;
• no synchronous blocking;
• no asynchronous suspension;
• no forbidden spawning;
• interrupt-compatible volatile and external-state behavior;
• an interrupt-safe reachable call graph;
• acceptable stack behavior;
• no unresolved unknown effect source.

@isr

@isr applies the interrupt-entry safety contract. It implies @noPanic, @noAlloc and @noBlock, together with additional ISR-specific restrictions.

@interrupt(...)

@interrupt(...) binds the function to target interrupt metadata and implies @isr. The interrupt chapter defines vector binding and the target entry model in detail.

Target knowledge matters. A bounded register acknowledgement or interrupt-flag write may be valid even though it is externally observable. Interrupt safety is not implemented as a blanket ban on every hardware effect.

Cleanup, defer and Destruction

Verified guarantees include cleanup that can execute on reachable exits. This is important because effects may occur after the last visibly written ordinary statement.

@noBlock
fn Work() void {
    defer {
        BlockingClose()
    }
}

This function violates @noBlock. The deferred operation executes during cleanup and therefore participates in the function's effective behavior.

Effect analysis includes applicable cleanup on:

• normal return;
• early return;
• explicit error propagation;
• scope exit;
• cancellation paths where cleanup is defined;
• contained panic cleanup where the panic model requires it.

Destructors may also contribute allocation, blocking, I/O, volatile access or external mutation unless another rule forbids those behaviors. A containing guarantee must account for the destructor behavior that can actually run.

Function Values and Callbacks

Effect guarantees participate in callable compatibility. A function with fewer possible effects may be used where a more permissive callable is accepted; a more-effectful function cannot satisfy a stricter requirement.

Conceptually:

stricter callable requirements
    accept an equal or stronger implementation
    reject an implementation with additional forbidden effects

The exact source syntax for effect-constrained function types is not fixed in Sec 0.1. The semantic compatibility rule is fixed even though the general type syntax is not.

A public function that invokes a callback cannot claim a guarantee such as @noPanic unless the callback contract or resolved callable target establishes the required absence of panic.

The compiler must not infer a public callback guarantee merely from the particular call sites visible in one executable build.

Interfaces

Interface methods may carry verified effect requirements. Every implementation must satisfy the interface contract.

An implementation may be stronger. For example, an interface method that permits allocation may be implemented by a method that is allocation-free.

The reverse is invalid:

interface requirement: no allocation
implementation: may allocate

// invalid

This follows the same subset principle as callback compatibility: fewer possible effects are compatible with a context that allows more; additional forbidden effects are not.

Generics and Specialization

Generic effect behavior may depend on operations available on type parameters, destruction behavior, callbacks, selected implementations and target-specific specialization.

fn Apply[T](value: T) void {
    ...
}

When effect-relevant behavior depends on T, the compiler may retain a symbolic or conservative summary until a concrete specialization is known.

A concrete specialization may prove fewer effects than the generic upper bound. This stronger inferred fact may be used internally for optimization and local verification.

The exact source syntax for generic effect constraints remains separate from the basic generic type syntax and is not invented by this chapter.

FFI and Trusted Effects

The compiler can analyze Sec source, but it cannot automatically inspect arbitrary foreign implementation behavior with the same certainty.

Unknown foreign code is therefore conservative. Unless an explicit FFI contract or compiler-known platform description establishes otherwise, foreign code may perform effects that prevent strong guarantees from being proven.

A verified-looking attribute on an extern declaration is not ordinary proof of the foreign body. Foreign guarantees cross a trust boundary and must preserve that provenance.

unsafe itself is not modeled as a general MayUnsafe effect. Instead, the compiler records that a proof depends on a trusted or unsafe boundary.

Arena Lifetime Effects

Not every effect can be represented as an unordered “may happen” flag. Arena operations change storage validity in an order-sensitive way.

The compiler tracks conceptual events such as:

ArenaCreate(A)
ArenaAllocate(A, size)
ArenaReset(A)
ArenaRelease(A)

Order matters:

let arena := Arena.FromBuffer(ref buffer)
let value := arena.New[Value]()
arena.Reset()

Use(ref value)    // invalid: backing lifetime epoch was reset

The programmer sees ordinary Arena operations and references. Sec does not expose general source-level region variables merely to support this analysis.

Branches and loops merge arena state together with ordinary flow facts. A later use is valid only when every continuing path preserves the required storage validity.

Quantitative Resource Facts

Some resource properties are numeric rather than boolean. Sec keeps those separate from the summary may-effect set.

Examples include:

• maximum live arena allocation;
• remaining arena capacity;
• unknown allocation bounds;
• maximum stack contribution;
• maximum simultaneous task creation where provable;
• path-specific resource peaks.

A function can therefore be known to allocate and, separately, have a proven maximum amount of allocation in a particular bounded storage domain.

These facts feed later static-analysis and target checks without changing the source meaning of @noAlloc.

Guarantees Do Not Depend on Optional Optimization

A declared guarantee must hold because the program semantics and required compiler analyses prove it, not because one optimization setting happens to remove an effect.

A guarantee may rely on required proofs such as:

• semantic constant evaluation;
• dead-path proof;
• mandatory escape analysis;
• required call-graph resolution;
• type and contract proof;
• compiler-known intrinsic semantics.

It must not be true only because:

• release optimization removed an allocation;
• inlining happened to erase a helper;
• one optimization level simplified a loop;
• debug and release happened to make different incidental choices.

For the same compilation plan and source semantics, debug and release builds agree on verified effect guarantees.

Compilation Plans and Targets

Effect analysis is performed for the active source graph and concrete compilation plan. Target selection can change which implementation is reachable and how certain target operations are classified.

This does not make guarantees arbitrary. The selected plan determines the reachable program; the compiler then verifies the declared contract for that plan.

Target knowledge may provide facts about:

• platform intrinsics;
• hardware register access;
• blocking versus nonblocking platform calls;
• interrupt-safe device operations;
• stack and ABI restrictions.

Unknown target behavior remains conservative. A strong guarantee is never established by guessing that an unknown platform operation is safe.

Diagnostics

Effect diagnostics should explain the cause, not merely report that a boolean flag failed.

A guarantee failure identifies:

• the failed declared guarantee;
• the operation that introduced the forbidden effect;
• the relevant call chain;
• the source location;
• whether the fact was proven, trusted or unknown;
• the active compilation plan when relevant.

error: `PollDevice` does not satisfy @noBlock

PollDevice
  -> calls ReadDevice
  -> calls OSRead
  -> operation may wait for external input

effect introduced at:
    platform/linux/device.sec:51

When several causes contribute the same effect, tooling may summarize the count and provide navigation to each cause rather than hiding the additional paths.

LSP and Tooling

Effect information is useful while reading code, not only when a build fails. The language server may expose inferred effects and declared guarantees through hover and navigation.

Useful tooling information includes:

• inferred effects;
• explicit and implied guarantees;
• direct versus transitive causes;
• call-chain navigation;
• trust provenance;
• active compilation plan;
• arena invalidation information;
• quantitative resource facts when available.

Effects:
    MayIO
    MaySuspend

Guarantees:
    noBlock

Provenance:
    Sec source

Tooling displays compiler facts; it does not introduce a second effect system with different language semantics.

No Mandatory Runtime

Effect analysis is compile-time and does not require runtime effect machinery.

Sec does not require:

• runtime effect objects;
• an effect stack;
• dynamic effect checks;
• effect dispatch;
• an exception unwinder;
• a mandatory scheduler;
• a mandatory allocation tracker.

Compiler metadata may be retained where needed for separate compilation, debugging, diagnostics or language-server features, but ordinary effect correctness is not enforced by a runtime effect engine.

Best Practices

• Declare a verified guarantee when callers need to rely on it as part of the API.
• Do not add guarantees merely as documentation; every one becomes a compiler-checked obligation.
• Use Result and try for expected failure rather than relying on panic.
• Remember that try does not remove unrelated allocation, I/O or blocking effects.
• Keep @noAlloc code free from every dynamic allocation source, including arena allocation.
• Do not treat @noBlock as a worst-case execution-time guarantee.
• Review cleanup paths when an effect guarantee unexpectedly fails.
• Give public callbacks and interfaces explicit effect contracts when callers need stable guarantees.
• Keep foreign and assembly trust boundaries narrow and documented.
• Use target knowledge for hardware behavior; do not encode ISR safety as assumptions in ordinary source.
• Let stronger inferred implementation facts remain internal unless they are intentionally part of the API contract.

Summary

• Sec performs compile-time effect analysis in addition to ordinary type, ownership and borrow analysis.
• Sec 0.1 does not expose a general programmer-written effect language.
• Every callable receives inferred effect information even without an effect attribute.
• Inferred absence of an effect is not automatically a stable public API promise.
• @noPanic, @noAlloc and @noBlock are transitive compiler-verified guarantees.
• @interruptSafe, @isr and @interrupt(...) are stronger composite contracts.
• The compiler distinguishes panic, allocation, blocking, suspension, spawning, I/O, volatile access, external mutation and nondeterministic input.
• Expected Result errors are typed control flow, not effects by themselves.
• try converts supported failure into explicit error flow but does not erase unrelated effects.
• Blocking and asynchronous suspension are separate facts.
• Effect verification includes reachable callees, cleanup, defer, destruction and compiler-generated operations.
• Effect compatibility is monotonic: a less-effectful implementation may satisfy a more permissive contract, not the reverse.
• Interfaces, callbacks and generic specializations participate in effect compatibility.
• Unknown indirect, foreign or target behavior is handled conservatively.
• Foreign and assembly guarantees retain trust provenance rather than being reported as ordinary source proof.
• Arena lifetime changes are ordered effects rather than ordinary unordered summary flags.
• Quantitative resource facts such as stack and arena peaks remain separate from boolean may-effects.
• Verified guarantees cannot depend only on optional optimization.
• Effect analysis is performed for the active compilation plan.
• No mandatory runtime effect system is required.