Attributes

Purpose

Attributes are used when a property belongs to a declaration, changes compilation or verification, is orthogonal to ordinary declaration grammar and must be understood by the compiler.

Attributes are not comments, macros, textual preprocessing or arbitrary user metadata.

static also remains separate: it describes storage duration/type association, not physical placement or target binding.

Closed Attribute Set

Only attributes known to the selected compiler version and language profile are accepted.

@audit(category: "finance")
fn PostInvoice() void {
}

The example above is invalid in Sec 0.1. Unknown attributes are not preserved as passive metadata.

Sec 0.1 Compiler-Known Attributes

@target(...)
@when(...)
@address(...)
@interrupt(...)
@isr
@interruptSafe
@noCopy
@noAlloc
@noPanic
@noBlock
@link_name("foreign-symbol")

Attribute Categories

Syntax

@isr

@address(0x40021000)

@interrupt(vector: Interrupt.Timer0)

@target(os: "linux", arch: "amd64")

@when(config.telemetry)

An individual attribute defines whether its arguments are positional, named or absent.

Attribute Arguments

Using the wrong argument form is a compile-time error.

Attribute Arguments Are Evaluated at Plan Time

Initial attribute arguments must be available while the compilation plan is constructed or validated.

They cannot depend on runtime execution, allocation, I/O, mutable runtime state, ordinary user-function calls, dynamic dispatch or foreign calls.

Compiler-known target constants and build configuration values are available only where the specific attribute permits them.

Attachment

An attribute normally applies to the next allowed top-level statement:

@noPanic
fn Calculate() int {
    return 10
}

Consecutive attributes form one attribute set for the same declaration:

@noAlloc
@noPanic
@noBlock
fn PollDevice() Result[State, DeviceError] {
    ...
}

An attribute left without an attached statement before end-of-file is invalid.

Comments and Whitespace Do Not Break Attachment

@noPanic

// Public arithmetic entrypoint.
fn Add(left: int, right: int) Result[int, ArithmeticError] {
    let result := try left + right
    return Ok(result)
}

Sec 0.1 Attributes Attach at Compilation-Unit Level

The initial attribute system does not decorate arbitrary local statements or expressions.

fn Work() void {
    @target(os: "linux")    // invalid
    PerformLinuxOperation()
}

Multiple Attributes on One Declaration

@target(device: "controller-a")
@address(Peripheral.GPIOA)
let mut GPIOA: GPIORegisters

Both attributes attach directly to GPIOA. One attribute does not create a scope for another.

Attribute Order

Initial attribute semantics are order-independent inside one attachment set.

Selection attributes are best written before binding and verification attributes because that follows the conceptual compilation order.

Duplicate Attributes and Arguments

@noCopy
@noCopy    // invalid
type Identity struct {
    Value: uint64
}

Repeat target selectors in one attribute instead:

@target(os: "linux", arch: "amd64")
fn Open() void {
}

A named argument may also appear only once.

Conflicting Attributes

The compiler rejects semantic conflicts such as two addresses, two interrupt vectors, contradictory target selectors or a verified guarantee contradicted by required behavior.

Redundant Attributes May Be Written Explicitly

@interrupt(vector: Interrupt.Timer0)
@isr
@noPanic
@noAlloc
@noBlock
fn Timer0Handler() void {
}

This is valid even though the stronger attributes imply several of the written guarantees. Tooling may report redundancy informationally, but the formatter does not delete it automatically.

@target

@target selects source according to target identity.

@target(os: "linux", arch: "amd64")
fn RawWrite(...) Result[int, WriteError] {
    ...
}

Initial selector names are:

os
arch
cpu
device
board

At least one selector is required. Omitted selectors impose no restriction, and all supplied selectors must match the active compilation plan.

@target can select an entire source file when it is the first source-bearing line, or the next top-level declaration when used later in the file.

Detailed source-selection semantics belong to chapter 38.

@when

@when conditionally includes the next top-level declaration according to typed compile-time configuration.

@when(config.telemetry)
fn SendTelemetry() Result[void, TelemetryError] {
    ...
}

It does not create runtime branching. The declaration is either part of the current compilation plan or it is not.

The initial condition language includes boolean configuration parameters, true, false, !, &&, ||, ==, != and parentheses.

Target identity belongs in @target; typed program configuration belongs in @when.

@address

@address binds one module-scope storage declaration to a compile-time address:

@address(Peripheral.GPIOA)
let mut GPIOA: GPIORegisters

Raw numeric form is also valid when the active target provides a compatible region:

@address(0x40021000)
let mut GPIO: GPIORegisters

The declaration refers to storage that already exists. It does not allocate ordinary storage, and its reads use volatile semantics.

mut determines whether writes are permitted.

The compiler validates target pointer width, address space, complete region coverage, alignment, physical access width, permissions, representation compatibility, required privilege and detectable overlap.

A numeric address by itself is never sufficient proof of a valid binding, and unsafe does not waive this validation.

@address applies to exactly one module-scope let declaration, not to locals, parameters, fields, functions or types.

Hardware placement is covered in detail in chapter 50.

@interrupt

@interrupt binds a function to a target interrupt vector:

@interrupt(vector: Interrupt.Timer0)
fn Timer0Handler() void {
}

The vector must resolve at compile time to an identity accepted by the selected target. Named target-provided vectors are preferred where available.

The compiler validates vector availability, unique binding, signature, ABI and ISR requirements.

@interrupt(...) implies @isr. The reverse is not true.

@isr

@isr declares and verifies an interrupt service routine without itself choosing a vector:

@isr
fn SharedInterruptHandler() void {
}

The verified contract includes at least:

• no panic;
• no allocation;
• no blocking;
• interrupt-safe call graph;
• target-compatible signature and entry/return behavior;
• bounded stack requirements;
• no forbidden lock acquisition;
• no ordinary scheduler suspension;
• safe shared-state access under the approved synchronization model.

A target may reject @isr when it has no defined ISR ABI.

@interruptSafe

@interruptSafe verifies that a function may be called from ISR code:

@interruptSafe
fn ReadStatus() Status {
    ...
}

It does not make the function an ISR and does not bind a vector.

The guarantee includes no panic, no allocation, no blocking, compatible synchronization, safe shared-state access, compatible callees and acceptable stack behavior under ISR policy.

@noCopy

@noCopy is a nominal type policy:

@noCopy
type SessionID struct {
    Value: uint64
}

It forbids compiler-derived implicit copy.

Implicit copy is invalid:

let second := first

Explicit ownership transfer may remain valid:

let second :<- first

Copyability is distinct from movability, relocatability and pinning.

Explicit methods named Copy, Clone, Duplicate, Snapshot or ToOwned remain ordinary APIs.

@noCopy applies to nominal user-defined types rather than individual variables, fields, parameters or functions.

A containing aggregate becomes non-copyable when it stores a non-copyable field unless another rule introduces copyable indirection.

@noAlloc

@noAlloc is a transitive compiler-verified guarantee:

@noAlloc
fn Process(
    buffer: ref byte[],
) Result[void, ProcessError] {
    ...
}

No reachable execution path may allocate.

Verification includes the body, reachable callees, generic specializations, closures, defer bodies, reachable destructors, foreign declarations and compiler-generated operations.

Unknown allocation behavior violates the guarantee.

Using try on an allocating operation does not make it compatible with @noAlloc; fallible allocation still allocates when it succeeds.

@noPanic

@noPanic is a transitive compiler-verified panic-free guarantee:

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

No reachable panic-capable operation may remain unresolved.

The compiler checks panic-capable operations and calls, unproven assertions, reachable checked unreachable, explicit panic once finalized, foreign abort/unwind behavior and panic-capable cleanup.

@noPanic does not catch panic. It requires the panic effect to be absent.

@noBlock

@noBlock verifies that no reachable execution path waits for an unbounded external event or parks the current execution domain:

@noBlock
fn PollStatus() Status {
    ...
}

Blocking includes blocking I/O, sleep, waiting on mutexes/semaphores, condition waits, thread joins, blocking task waits, scheduler parking, unbounded external waits and foreign calls declared as blocking.

Finite computation, statically bounded loops, nonblocking polling, try-lock and separately proven bounded lock-free retry are not forbidden merely by @noBlock.

Nonblocking is not the same as bounded execution time.

@link_name

@link_name selects the external symbol used by an extern declaration:

@link_name("foreign_symbol")
extern "C" fn SecName(...) C::int

It is valid only on an extern declaration and requires one non-empty string literal.

It changes only the foreign/link symbol. It does not change the Sec name, calling convention, safety, ownership, effects, dependency metadata or ABI compatibility.

Attribute Implications

@interrupt(...)
    => @isr

@isr
    => @noPanic
    => @noAlloc
    => @noBlock
    => interrupt-safe call graph

@interruptSafe
    => @noPanic
    => @noAlloc
    => @noBlock

Effective guarantees are semantic facts even when only the stronger attribute is written explicitly.

Verified Attributes on extern Declarations

For ordinary Sec functions with bodies, guarantee attributes are proven from the implementation and reachable call graph.

For an extern declaration, the compiler normally cannot inspect the foreign body. An applicable guarantee is therefore a trusted foreign contract, not proof of the foreign implementation.

The compiler preserves this trust provenance and treats unspecified foreign effects conservatively.

Attribute Validation Order

Conceptually:

1. parse files and attributes;
2. evaluate file-level target selection;
3. evaluate top-level @target and @when;
4. construct the active source/symbol set;
5. validate overlapping declaration variants;
6. perform ordinary semantic analysis on active declarations;
7. verify nominal/effect attributes;
8. validate target bindings;
9. lower active declarations.

Selection attributes therefore participate before active semantic analysis, while verification attributes depend on the resolved semantic program.

Formatter Behavior

The canonical formatter writes one attribute per line:

@target(os: "linux")
@when(config.telemetry)
@noPanic
fn SendTelemetry() Result[void, TelemetryError] {
    ...
}

Formatting preserves attachment and does not silently delete explicitly written attributes simply because another attribute implies them.

LSP and Tooling

Tooling should understand attributes semantically, including:

• completion restricted to compiler-known attributes;
• completion restricted by allowed attachment target;
• argument-name and target-selector completion;
• hover describing the attribute contract;
• display of implied guarantees;
• display of source excluded by the active compilation plan;
• cause chains for failed verified guarantees;
• navigation to target/device/interrupt knowledge;
• trusted provenance display for extern guarantees.

Diagnostics

Unknown attribute

unknown attribute `@audit`

Sec 0.1 accepts only compiler-known attributes

Wrong attachment target

`@noCopy` cannot be applied to variable `session`

`@noCopy` is a nominal type policy

help: apply it to the declared type instead

Duplicate attribute

duplicate attribute `@noPanic`

the attribute already appears in this attachment set

Duplicate argument

duplicate argument `os` in `@target`

each named argument may appear only once

Unattached attribute

`@noPanic` has no declaration to attach to

an attribute must be followed by an allowed top-level statement

Argument not available at plan time

`@when` condition is not available at compilation-plan time

attribute arguments cannot depend on runtime state or ordinary function calls

Verified guarantee violation

`PollStatus` does not satisfy `@noBlock`

call path:
    PollStatus
    -> WaitForDevice

`WaitForDevice` may block indefinitely

Guarantee diagnostics should show the semantic cause chain rather than pointing only at the attribute line.

Best Practices

• Use only compiler-known attributes with defined Sec semantics.
• Keep one attribute per line.
• Write selection attributes before binding and guarantee attributes for readability.
• Use @target for target identity and @when for typed program configuration.
• Prefer named target-provided addresses and interrupt vectors where available.
• Use @noCopy on nominal types, not individual variables.
• Treat @noAlloc, @noPanic and @noBlock as verified contracts, not documentation comments.
• Use @interruptSafe for reusable ISR-safe helpers rather than marking them as ISR entrypoints.
• Use @interrupt when the function owns a concrete vector binding.
• Use @isr without @interrupt only when vector binding is supplied elsewhere.
• Use @link_name only to map a Sec extern declaration to its actual foreign symbol.
• Keep native library dependencies in project/package/build metadata rather than inventing per-function library attributes.
• Do not depend on source order of attributes for semantics.
• Do not mechanically remove redundant attributes that intentionally document a stronger contract.

Summary

• Attributes attach compiler-understood semantics to top-level declarations.
• Sec 0.1 has a closed compiler-known attribute set.
• Unknown attributes are compile-time errors and are not retained as passive metadata.
• Attributes are not macros, textual preprocessing or arbitrary runtime reflection metadata.
• The initial set is @target, @when, @address, @interrupt, @isr, @interruptSafe, @noCopy, @noAlloc, @noPanic, @noBlock and @link_name.
• Selection attributes choose active source for one compilation plan.
• Target-binding attributes connect declarations to target storage or interrupt machinery.
• Verified guarantee attributes are compiler-proven for ordinary Sec implementations.
• @noCopy changes nominal copy policy.
• @link_name changes only the foreign symbol of an extern declaration.
• Every attribute defines its own valid attachment targets and argument form.
• Initial attribute arguments must be available at compilation-plan time.
• Runtime execution, arbitrary user-function calls, I/O, allocation and mutable runtime state cannot be required to evaluate initial attribute arguments.
• An attribute normally attaches to the next allowed top-level statement.
• Consecutive attributes form one attachment set for the same declaration.
• Whitespace and comments do not break attachment.
• Sec 0.1 attributes do not attach to arbitrary local statements or expressions.
• Initial attribute semantics are order-independent within one attachment set.
• Duplicate attributes are invalid unless repetition is explicitly defined.
• Duplicate named arguments are invalid.
• Conflicting attribute semantics are compile-time errors.
• Explicitly written redundant implied attributes are valid.
• @target selects source by target identity.
• Initial target selector names are os, arch, cpu, device and board.
• All supplied target selectors must match the active compilation plan.
• @when conditionally includes a top-level declaration using typed plan-time configuration.
• @when does not create runtime branching.
• @address binds one module-scope storage declaration to a target-validated compile-time address.
• @address does not allocate ordinary storage.
• @address implies volatile access semantics.
• A raw numeric address alone does not prove a valid target binding.
• unsafe does not waive address-space, region, privilege, alignment or representation validation.
• @interrupt binds a function to a target interrupt vector.
• @interrupt implies @isr.
• @isr verifies ISR behavior without itself selecting a vector.
• @interruptSafe verifies that a helper may be called from ISR code.
• @interruptSafe does not make the function an ISR.
• @isr and @interruptSafe imply no-panic, no-allocation and no-block requirements.
• @noCopy forbids compiler-derived implicit copy of a nominal type.
• @noCopy does not imply immovability, non-relocatability or pinning.
• Explicit named duplication APIs remain ordinary APIs even on an @noCopy type.
• @noAlloc verifies that no reachable execution path allocates.
• Fallible allocation is still allocation and remains incompatible with @noAlloc.
• @noPanic verifies absence of reachable panic behavior; it does not catch panic.
• @noBlock verifies absence of unbounded waits and scheduler parking.
• Nonblocking behavior alone does not imply bounded execution time.
• @link_name is valid only on extern declarations and requires one non-empty string literal.
• @link_name does not alter ABI, safety, ownership, effects or native dependency metadata.
• For ordinary Sec functions, verified guarantee attributes are proven by the compiler.
• For extern declarations, applicable guarantee attributes are trusted foreign contracts.
• Trust provenance from extern guarantees remains visible to compiler analysis.
• Unknown foreign effects are treated conservatively.
• The formatter writes one attribute per line and preserves explicit attributes and attachment.
• LSP and analysis should understand valid targets, arguments, implied guarantees, active/excluded source and trusted foreign provenance.