Interrupts and ISRs

Purpose

Interrupt handling combines language semantics with target facts. The language owns the meaning of attributes such as @isr and the requirement that the full reachable call graph be safe. The platform owns facts such as interrupt identities, physical vectors, controller routing, nesting relations, entry ABI and stack domains.

This separation lets the same Sec source express an interrupt handler without baking one MCU's vector-table layout or one controller's priority encoding into the language.

Three Interrupt Contracts

Sec distinguishes three related attributes:

These are compiler-verified contracts, not documentation-only annotations.

@isr

@isr marks a function as an interrupt entrypoint without binding it to a particular platform vector. This is useful when a platform layer or generated wrapper performs the final physical binding.

@isr
fn DeviceInterruptEntry() void {
    ServiceDevice()
}

The Sec 0.1 baseline implies @noPanic, @noAlloc and @noBlock. Additional restrictions are evaluated from the concrete ISR profile for the active CompilationPlan rather than being encoded as one universal hard-coded list.

@interruptSafe

@interruptSafe is for reusable functions that may be called from ISR code. It does not make the function an interrupt entrypoint and does not bind it to target metadata.

@interruptSafe
fn ClearPendingFlag(ref mut status: DeviceStatus) void {
    status.Pending = false
}

The contract includes transitive requirements such as:

• 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 effect source that prevents proof.

@interrupt(...)

The common direct-binding form names the vector or interrupt identity in the attribute:

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

@interrupt(...) implies @isr. The compiler therefore performs both binding validation and ISR safety validation.

The handler's machine-level entry convention comes from the resolved target metadata. The compiler may generate target-specific wrappers where the physical controller or ABI requires claim, dispatch, completion or other entry/exit work.

Named Interrupt Identities

Named identities are the preferred form. They come from compiler knowledge packs, Device definitions or other canonical platform metadata.

Interrupt.Timer0
Interrupt.UART0
Interrupt.GPIOA
Interrupt.DMA1

A name is not merely an alias for a number. It can resolve to a complete interrupt description containing availability, controller route, entry/vector identity, ABI, aliases and execution relationships.

Raw Vector Numbers

Sec also permits a raw numeric vector form where target metadata allows it:

@interrupt(vector: 15)
fn CustomHandler() void {
    HandleCustomSource()
}

A raw vector does not bypass target validation. The selected platform still decides whether that vector is valid, which ABI applies and what execution properties can be proven. Prefer a named identity whenever the target already knows the interrupt.

Platform Interrupt Metadata

Interrupt metadata belongs to the resolved platform model. A concrete Device may refine or supply details that an architecture alone cannot know.

Canonical metadata may describe:

• logical interrupt source identity;
• controller and route identity;
• physical entry or vector identity;
• entry ABI and required generated wrapper;
• availability on the selected Device;
• aliases and canonical binding identity;
• priority class or controller-specific priority information;
• preemption, nesting, reentry and masking relations;
• physical stack domain and stack budget constraints;
• claim, dispatch and completion requirements where applicable.

Source semantics should not guess any of these facts from an architecture name or a raw priority integer.

Binding Resolution

Interrupt binding is resolved against the immutable active CompilationPlan. The same symbolic source identity can therefore resolve differently for different target variants while preserving one source-level meaning.

Interrupt.Timer0
        |
        v
active CompilationPlan
        |
        v
canonical source + route + physical entry + ISR profile

Cross compilation always uses target metadata. The host machine running the compiler has no authority over interrupt identities or entry conventions for the target binary.

One Active Binding Owner

One resolved interrupt binding has one active owner. Two source functions may not both claim the same canonical interrupt entry in the same concrete compilation.

Duplicate detection uses canonical resolved identity, not only source spelling. Two different aliases that resolve to the same physical binding are still a conflict.

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

@interrupt(vector: Interrupt.Timer0Alias)
fn Second() void {}    // invalid when both names resolve to one binding

Binding Is Not Controller Configuration

Declaring an interrupt handler establishes a program binding. It does not perform controller lifecycle operations.

@interrupt(...) does not by itself:

• enable the peripheral source;
• configure the interrupt controller;
• set hardware priority registers;
• unmask the source;
• clear pending state;
• start a timer or peripheral;
• acknowledge a device condition.

Those operations belong to explicit platform, device or driver behavior. This keeps binding declarative and prevents a declaration from causing hidden hardware writes.

Interrupt Lifecycle

Sec keeps interrupt lifecycle concepts distinct. They must not be collapsed into one vague “interrupt is active” state.

The platform model may distinguish:

• source configuration;
• routing;
• controller enable/mask state;
• pending state;
• active state;
• claim or dispatch;
• source servicing or acknowledgement;
• controller completion;
• return from the interrupt entry context.

Different architectures and controllers realize these stages differently. The compiler may generate canonical wrapper steps when the platform metadata requires them, but source-level binding does not pretend that every controller works alike.

Logical Source vs Physical Entry

A logical interrupt source and a physical entry/vector are not necessarily identical. One controller entry may dispatch several sources, and one logical source may be routed differently on another Device.

Sec therefore keeps at least these identities conceptually separate:

logical source
route/controller input
physical entry or vector
handler binding

This distinction is essential for generated dispatchers, shared controller entries, aliases and portable Device descriptions.

Priority Is Platform Semantics

Sec does not define interrupt semantics by comparing raw numeric priority values. Different controllers use different encodings and may invert or otherwise transform the numerical representation.

The platform resolves a canonical priority class and the execution relationships that analyses actually need. The compiler asks questions such as whether one context may preempt or nest another; it does not infer those answers by assuming that a larger integer always means a higher priority.

Preemption, Nesting and Reentry

The ExecutionEnvironment in the active plan owns resolved relations such as:

MayPreempt(A, B)
CannotPreempt(A, B)
MayNest(A, B)
CannotNest(A, B)
MayReenter(A)

ISR analysis consumes these relations directly. It does not reconstruct them from controller register values or architecture folklore.

This matters for stack composition, shared-state races, synchronization and reentrant runtime behavior. Two handlers that can never overlap have different proof obligations from two handlers that may nest or run concurrently on different cores.

Masking

Interrupt masking may change which interrupt contexts can overlap, but masking is not a universal synchronization primitive. Its effect is interpreted through the selected platform model.

In particular, local interrupt masking does not automatically exclude:

• another CPU core;
• DMA engines;
• external bus masters;
• unrelated interrupt domains;
• threads or tasks running elsewhere.

Static analysis must therefore use actual execution relations rather than assuming “interrupts disabled” means “all concurrency disabled”.

ISR Safety Baseline

Sec 0.1 uses a conservative baseline for ISR entry. @isr and @interruptSafe imply the verified no-panic, no-allocation and no-blocking guarantees. The resolved ISR profile may impose additional requirements.

An ISR is not made safe merely because its own body looks short. The compiler verifies the complete reachable behavior, including helper functions and generated cleanup.

Reachable Effects

ISR validation consumes transitive effect summaries. Relevant facts may include:

• MayPanic;
• MayAllocate;
• MayBlock;
• MaySuspend;
• spawn or scheduler requirements;
• volatile and external-state operations;
• foreign calls;
• runtime-helper requirements;
• synchronization acquisition.

Not every external effect is forbidden. A bounded device-register acknowledgement, for example, may be exactly what the interrupt handler must perform. Safety is proven against the resolved profile rather than implemented as a blanket ban on hardware access.

Cleanup and Compiler-Inserted Work

ISR validation includes work that may execute because of language semantics even when it is not written as an obvious ordinary call at the handler's final source line.

This includes applicable:

• defer bodies;
• destruction and cleanup;
• error-path cleanup;
• compiler-generated runtime helpers;
• target-generated interrupt entry or completion wrappers.

The compiler must not prove an ISR safe from the visible body and then introduce a blocking, allocating or otherwise forbidden lowering helper afterward.

FFI and Runtime Helpers

A foreign function or runtime helper is ISR-safe only when its contract and the active platform profile establish that fact. Unknown foreign behavior cannot be assumed safe.

A synchronous foreign callback entered while executing in ISR context inherits that context for safety analysis. A real context handoff may establish a new execution context, but the transition itself must be represented explicitly in compiler and platform semantics.

Ownership, References and Borrowing

ISRs use the ordinary Sec memory model. There is no separate ISR reference type. References, ownership, borrowing, moves and destruction keep their normal meanings.

What changes is the concurrency context. A reference that is valid by lifetime rules may still participate in an invalid data race when interrupt preemption makes two accesses overlap. ISR analysis therefore consumes the ordinary ownership/lifetime proof together with concurrency analysis rather than replacing it.

ISRs Are Concurrent Execution

Interrupt handlers participate in Sec's concurrency model. Shared storage accessed by an ISR and another execution context must satisfy the same data-race principles as other overlapping execution.

The compiler uses resolved preemption, nesting and reentry relations when deciding which accesses may actually overlap. Race and deadlock analyses remain their own canonical owners; ISR analysis consumes those results rather than reimplementing them.

ISR Stack Proof

Interrupt safety includes stack requirements, especially when interrupts may nest. Stack analysis owns stack-size reasoning. ISR analysis consumes the resulting proof under the resolved interrupt profile and stack domain.

Nested stack composition depends on actual MayPreempt and MayNest relations rather than simply adding every handler's maximum stack use together.

A known exact requirement that exceeds the ISR stack budget is invalid. When only an insufficient upper-bound proof is available, the result may remain unproven rather than being reported as a false definite violation.

Generated Entry Code

A platform may require compiler-generated entry code around the source handler. Such code may perform canonical controller work such as claim, dispatch and completion, or adapt the physical ABI to the Sec handler's source signature.

Generated code is part of the ISR contract. It must obey the same profile restrictions and must be included in stack/effect reasoning where relevant.

Vector Tables and Link Roots

A resolved @interrupt binding may create linker- and startup-visible requirements. The compiler may need to emit vector-table entries, dispatcher roots, retained symbols or startup metadata for the selected platform.

These are generated from canonical binding metadata. Source code should not manually reproduce vector-table structure when the platform model already owns it.

An interrupt binding is therefore also a reachability root: the handler must remain available to the final linked program even when no ordinary Sec call refers to it.

ISR Analysis

ISR analysis is a cross-analysis verifier. It combines facts from the call graph, effect analysis, stack analysis, data-race analysis, deadlock analysis, ownership and lifetime analysis, FFI contracts and the resolved CompilationPlan.

The implementation model is intentionally two-phase:

1. compute reusable transitive function requirement summaries;
2. evaluate each ISR root against its concrete resolved ISR profile.

This prevents every interrupt root from independently recomputing the same transitive function properties and allows normal functions to be analyzed once and reused across several ISR contexts.

Recursive call groups are handled through monotone fixed-point analysis over strongly connected components. Unknown requirements remain localized rather than poisoning unrelated functions or unrelated ISR roots.

Resolved ISR Profiles

Each interrupt root is evaluated under a profile derived from the active target and interrupt metadata. Conceptually, the profile contains facts such as:

ISRProfile
    ExecutionClass
    PriorityClass
    NestingModel
    Capabilities
    RequiredProofs
    StackBudget

The profile is resolved from canonical platform semantics, not reconstructed from source annotations or raw hardware numbers.

A helper may therefore be safe under one profile and unusable under another without changing its source code. Explicit guarantees such as @interruptSafe, however, remain stable promises and cannot be weakened by a concrete specialization.

Valid, Invalid and Unproven

ISR verification distinguishes proof outcomes instead of turning every incomplete proof into either success or failure.

• Valid — required safety properties are proven for the root/profile.
• Invalid — a definite profile violation is proven.
• Unproven — required safety could not be established from available facts.

A definite violation dominates uncertainty. A handler is not considered valid merely because some unrelated proof is still pending.

Incremental Analysis

ISR results depend on more than source text. They also depend on call-graph summaries, effect facts, stack proofs, race/deadlock results and the active CompilationPlan.

The compiler and LSP therefore track proof dependencies. A change to platform interrupt metadata, a helper's effect summary or a call edge invalidates only the ISR roots that depend on those facts. Stale positive proofs must not remain visible after a dependency changes.

Diagnostics

Interrupt diagnostics should explain both the root and the transitive reason for a failure.

error: interrupt handler Timer0Handler is not valid for Interrupt.Timer0

reachable call:
    Timer0Handler -> UpdateState -> GrowBuffer

requirement:
    ISR profile forbids dynamic allocation

cause:
    GrowBuffer may allocate

Useful diagnostics may also identify:

• duplicate canonical interrupt binding;
• unknown or unavailable named interrupt identity;
• invalid raw vector for the selected target;
• ABI/signature incompatibility;
• stack proof exceeding the resolved budget;
• unresolved foreign or indirect-call behavior;
• a data race created by an actual preemption relation;
• a stale or invalid platform interrupt definition.

Complete Example

type TimerStatus register[32] {
    Pending: bit
    _: bit[31]
}

@address(Platform.Timer0Status)
let mut timerStatus: TimerStatus

@interruptSafe
fn AcknowledgeTimer() void {
    timerStatus.Pending = false
}

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

fn ConfigureTimer() Result[void, TimerError] {
    // Configure the peripheral and interrupt controller explicitly.
    // The @interrupt declaration above does not enable or unmask it.
    return Ok()
}

The binding says which handler owns Interrupt.Timer0. The explicit setup code is still responsible for device/controller configuration. ISR analysis verifies the complete reachable handler path against the resolved interrupt profile.

Current Implementation Status

The interrupt and ISR design is complete through the current rulebook blocks, but the implementation status remains conservatively planned. The normative model is therefore established even though full parser, semantic, analysis, lowering, vector-table and backend integration is not yet claimed complete.

Separate ISR-analysis design work already defines the two-phase summary/profile model, Semantic IR inputs, SCC fixed-point handling, proof dependencies and incremental invalidation behavior. These are compiler design commitments, not evidence that every stage is already implemented end to end.

Best Practices

• Bind to named interrupt identities rather than raw vector numbers whenever the platform provides them.
• Use @interruptSafe for reusable helpers that are intentionally callable from ISR code.
• Keep interrupt handlers short, bounded and explicit about hardware acknowledgement.
• Do not expect @interrupt to configure or enable the underlying hardware.
• Do not infer preemption semantics from raw priority integers.
• Do not assume local interrupt masking excludes other cores, DMA or unrelated execution domains.
• Use ordinary Sec ownership and reference rules; do not invent ISR-specific pointer conventions.
• Keep unknown foreign and runtime behavior out of ISR call graphs unless a verified contract exists.
• Remember that cleanup, generated wrappers and compiler helpers also participate in the ISR proof.
• Let stack, race and deadlock analyses own their facts; ISR analysis should consume those proofs.

Summary

• @interruptSafe verifies reusable ISR-callable code but does not create an interrupt entrypoint.
• @isr declares an interrupt entry contract without binding a physical vector.
• @interrupt(...) binds resolved target interrupt metadata and implies @isr.
• Named interrupt identities are preferred over raw numeric vectors.
• Interrupt metadata is resolved through the immutable active CompilationPlan.
• One canonical interrupt binding has one active owner; duplicate aliases are still duplicates.
• Binding does not enable, unmask, configure, start, acknowledge or clear the hardware source.
• Logical source, route, physical entry, controller lifecycle and peripheral service are distinct concepts.
• Priority meaning comes from platform semantics, not raw numeric comparison.
• Preemption, nesting and reentry are canonical resolved execution relations.
• Local interrupt masking does not imply global exclusion from multicore, DMA or unrelated execution.
• The Sec 0.1 ISR baseline includes verified no-panic, no-allocation and no-blocking requirements.
• The full reachable call graph, cleanup, compiler helpers, FFI and generated wrappers participate in validation.
• ISRs use the ordinary Sec ownership, lifetime and borrowing model.
• ISR concurrency participates in ordinary race and deadlock reasoning.
• Stack analysis owns stack proofs; ISR analysis evaluates those proofs against the resolved profile.
• Platforms may generate vector-table entries, dispatchers, claim/completion wrappers and linker roots.
• ISR analysis is two-phase: reusable transitive summaries followed by per-root profile evaluation.
• Verification distinguishes Valid, Invalid and Unproven outcomes.
• The normative design is established, while current implementation status remains planned.