Skip to main content

Verified Subset Boundaries

Verified code runs under a stricter, sound subset of Sector9. Sector9 is a language derived from Motoko, but verification adds contracts, ghost state, footprints, and runtime-entry guard rules. This page summarizes the boundaries enforced by the verifier.

Trusted Boundary​

  • Verified by default: Code is verified unless marked trusted.
  • Trusted functions still need specs: At least one requires and ensures, plus reads/modifies if they touch actor state.

See Trusted Modifier.

Effects and Framing​

  • reads/modifies are required for actor state access.
  • Missing transitive effects are rejected (no auto-fix).
  • Calls with unknown effect summaries are forbidden unless pure or trusted.

See Footprints.

Expression Purity​

  • Impure calls are materialized into statement-level temporaries (ANF). Direct let x = await f() is rejected; use try { await f() } catch (_) { fallback } when an awaited result is needed.
  • Specs (requires/ensures/invariants) may call only pure functions.
  • Public actor methods with caller-controlled logical requires need matching entry_requires. The runtime guard cannot mention ghost state, old(), or result.

Async and Error Handling​

  • Every await (and any await* that may suspend) must be wrapped in try with a catch-all.
  • await? and throw are rejected in verification.
  • Error values (Error) cannot escape verified code.
  • finally can mutate state but cannot await, return, break, or throw.
  • Unawaited futures are rejected (no fire-and-forget).

See Await and Error Handling.

Aliasing and Mutability​

  • Deep mutable actor state is restricted. Keep public actor state shallow when possible; current owned/fresh local lanes cover some mutable-record and direct array cases, while nested array actor fields remain unsupported.
  • If aliasing cannot be proven disjoint, verification rejects the code.
  • Locals that may reference actor state across await are rejected.
  • Opaque/token handles are copyable identities, but their hidden payloads are still owner-controlled. Non-owner modules may store and pass handles through capability-summarized module APIs and supported containers; they cannot inspect or mutate the sealed payload directly.
  • Descriptor-backed collection snapshots can enumerate handle identities through exact BMap.entries / MBMap.entries and BSeq array/list/freeze bridges, but they do not snapshot owner payloads. Direct BMap.toArray over handle values remains unsupported.
  • Opaque owner mutators may batch several payload field writes before the invariant is rechecked. The owner must be repaired before return, await, or a call boundary that receives or writes the dirty owner.
  • Stable persistence for token/opaque handles must be compiler-owned: source code should keep handle types in stable fields and supported containers, while the compiler preserves raw same-identity state and checks owner identity. Stable upgrade is not a shared boundary and must not call toShared/fromShared.
  • Handle-bearing actor-state carriers are conservative across await: a fresh local handle may cross an await, but a handle recovered from actor-owned carriers such as records, arrays, BMap, MBMap, or BSeq may not be kept live across the suspension.

See Deep Aliasing and Local vs Shared State.

Structural Subtyping​

  • Structural subtyping of records/modules is allowed only for spec-immutable types.
  • Structural coercions involving mutable identity (arrays, mutable records, actors) are rejected.

See Verified Subtyping.

Higher-Order Function Values​

  • Function values must be pure or carry type contracts.
  • Escaping functions that touch $Self require full requires/ensures and exact reads/modifies.
  • Uncontracted callback types are treated as pure, so impure callbacks must use contract-typed parameters.

See Contract Subtyping.

Iteration​

  • for-in loops accept iterator objects whose next() method is () -> ?T with a type contract.

Integer and Spec Restrictions​

  • Verified code runs in checked-int mode.
  • Division/modulo in specs must be guarded against zero.

See Runtime Limitations.