Skip to main content

Verified Restrictions and Soundness Notes

This reference collects the current Sector9 restrictions and soundness model, including how verification models memory, effects, and async behavior.

Scope and Status​

  • Verified by default: code is verified unless explicitly trusted.
  • Trusted code still needs a spec surface (requires/ensures, and reads/modifies when impure).
  • Unknown or indirect effects are rejected in verified code unless pure, trusted, or fully contract-typed.
  • Signature-only assumption surfaces must be explicit: use abstract for VDD/proof interfaces and bodyless trusted for deliberate trusted-base assumptions. Plain bodyless declarations reject in verified code.
  • Restriction tests use _sat, _unsat, and _reject; a small legacy _noperm lane remains for known nested-permission coverage.

Core Memory and Permission Model​

  • Heap model: actor fields are the only heap roots that require explicit reads/modifies. Local or fresh heap values are tracked within a method.
  • Permissions: read vs write only (src/viper/perm_amount.ml). Read uses wildcard (and internal half-permissions for field distinctness), write uses full permission. Permission state and guards live in src/viper/perm_state.ml.
  • Invariants: actor invariants are asserted at entry, exit, and before each await. old(e) snapshots only method entry (no per-await old).
  • Await model: await is a commit point; Viper inserts an await-havoc over $Self state, computed from public method effects only. Await safety uses escape analysis in src/viper/mvir_await_locals.ml. $Self-reachable refs across await are rejected. Deep-mutable actor fields are also forbidden across await, including via helper-returned aliases (interprocedural return-field summaries).
  • Caller identity: Prim.caller_id() is modeled as ghost $Self.$caller_id (Int) with implicit permissions in method pre/post. It is treated as mutable call-context state and is havoced at await boundaries when public methods exist, so equality across await is not provable.
  • Borrow counters for async array-field arguments are tracked in src/viper/alias.ml and src/viper/lower_stmt_call_args.ml.
  • Canonical locations: place keys are normalized in src/viper/mvir_locn.ml, src/viper/mvir_place.ml, src/viper/mvir_inline_indices.ml, and src/viper/mvir_freeze_indices.ml.
  • Effects: call summaries come from src/viper/mvir_effects.ml and are used for alias filtering and permission tracking. Unknown summaries remain a hard reject (R1.3).
  • Actor-field distinctness facts are inferred in src/viper/mvir_field_distinct.ml and injected into invariants using a half-permission read access.

Verified Restrictions (Current Behavior)​

Verified vs Trusted​

  • Verified by default; only trusted bypasses restriction checks.
  • Trusted functions still require requires/ensures and, if impure, reads/modifies.

Effects and Framing​

  • Exact reads/modifies are required for actor fields; missing fields are errors.
  • Actor let fields whose types are spec-immutable are treated as implicit reads (no explicit reads clause required).
  • No auto-expanding footprints; inferred effects are used only to reject.
  • Any call with unknown effect summary is rejected unless pure, trusted, or fully contract-typed.

Purity and ANF​

  • Supported effectful executable expressions are materialized into ordered statement-level temporaries before Viper lowering. Pure/spec contexts reject statementful children fail closed.
  • Direct let x = await f()-style value binding is rejected. Use an enclosing try { await f() } catch (_) { fallback } expression when a result is needed.
  • Specs can call only pure or spec-only functions.

Contracts, Specs, and Ghost Boundaries​

  • Method/type contracts are header-only; decreases is rejected in verification (M0335).
  • Public exported methods with nontrivial logical requires need entry_requires guards in Viper mode. entry_requires is emitted as a runtime entry assertion and cannot mention old(...) or result.
  • Shared function bodies may contain standalone phase ... do { ... }; blocks in the current straight-line public async slice.
  • old() snapshots method entry only. It is allowed in postconditions and ghost/spec/lemma contexts, and is forbidden in invariants, requires clauses, and pure function bodies/contracts.
  • Contract expressions are self-framing (implicit access added). Invariants are limited to $Self-rooted heap access. Type contracts allow $Self/locals/result. Method contracts do not enforce a $Self-only heap-access check beyond framing.
  • Spec collections (Map/Set/Seq/Multiset) are pure values for verification. Element and key types must be spec-immutable (no var fields, arrays, functions, actors, async), except opaque/token handles by identity.
  • Float is modeled as an opaque value; arithmetic and ordering carry no axioms. Only equality is meaningful in proofs; use runtime asserts for Float semantics.
  • verification_only; is now an internal-only verifier sentinel rather than supported source syntax. Source uses are rejected; write proof-only helpers as ghost func or lemma instead.
  • Prelude spec collections only: Map/Set/Seq/Multiset in specs refer to the prelude types. User modules with those names are not treated as spec collections for lowering. Alias core modules (for example, import PureMap ...) to avoid name collisions.
  • Ghost code cannot mutate runtime state; ghost values cannot flow into runtime computations. Ghost fields are module-private.

Async/Await and Error Handling​

  • Every await or await* that may suspend must be in try with a single catch-all. A non-suspending await* over an async* computation is treated like a local call and does not introduce await interference.
  • try and catch use a single catch-all; refutable catch patterns are rejected.
  • await inside a catch must be wrapped in its own try/catch-all; try/finally without catch is rejected for awaits.
  • await? is rejected everywhere.
  • throw is rejected in verified code (commit semantics; not rollback).
  • Error values and types are forbidden outside a catch binder; errors cannot escape verified code.
  • trap and runtime:assert are proof obligations; disallowed in pure funcs and inside finally.
  • finally allows state mutation but forbids await, throw, return, break, and non-unit bodies.
  • Unawaited futures are rejected (no fire-and-forget).

Aliasing and Mutability Restrictions (Baseline)​

  • Deep mutable structures are disallowed by default. Current exceptions:
    • (R4.1-3) In method bodies only, a mutable field may directly contain a mutable record whose own var fields are shallow. These locals must not escape to $Self or return (checked in src/viper/mvir_escape.ml).
    • (R4.1-4) Private helper signatures may mention those deep-mutable types only when the body is translated (not trusted, bodyless, or obj-block). Public signatures still reject them. Wrappers such as ?T, tuples, and variants remain rejected.
    • (R4.1-6) Arrays are allowed as direct mutable fields under the same local-only deep-mutable rules.
    • (R4.1-8) Direct function fields are allowed for local-only deep-mutable records and remain subject to higher-order purity and contract checks.
    • Deep-mutable actor fields are allowed only for private fields that are absent from public modifies. Any method that awaits and touches those fields is rejected, including via helper-returned aliases. Return-field summaries are computed only for methods with bodies; trusted and bodyless callees do not add extra dependencies.
    • Actors in mutable fields remain rejected. Actor and module fields still require shallow payloads unless covered by the private-field rule.
  • Nested arrays (arrays of arrays) in actor fields remain unsupported in verification; nested element permissions are not generated, so a[i][j] triggers permission errors (coverage tests keep these as _noperm).
  • Opaque or token handle actor fields: private fields whose type is an opaque or token-owned handle are allowed even if they appear in public modifies. Mutators must declare modifies m explicitly; readers must declare reads m. Aliasing between distinct handle actor fields is rejected, including via locals, params, and helper calls.
  • Structural subtyping is allowed only for spec-immutable record or module types.
  • Alias checks are centralized in src/viper/mvir_alias_guard.ml, use explicit disjointness facts (requires a != b), and run at await barriers and method end. Disjointness compares full nested place paths (field and index projections), not only top-level fields. Only source-level disjointness assertions contribute facts; compiler-inserted asserts do not justify aliasing.
  • Ref returns are treated as owned-fresh only when a fixpoint summary proves the callee returns a fresh allocation that does not escape to $Self or unknown calls. trusted, bodyless, and dynamic returns remain non-fresh. This covers mutable-record refs and recognized fresh array-returning helper/library paths when the summary proves freshness; unsupported array-returning calls remain conservative.
  • Element-level contracts on arrays returned from actor fields generally fail unless the array is fresh. Return a copied array, use a BSeq.XSeq bridge, or reason through a ghost Seq model if you need result[i] facts in postconditions.
  • Mutable-record alias handling remains in src/viper/mvir_mutrec_alias.ml and src/viper/mvir_mutrec_post.ml.
  • Explicit postconditions are never rewritten. If aliasing would invalidate an explicit ensures, verification fails unless disjointness is proven.

Closures and Higher-Order Functions​

  • Captured variables are read-only in closures unless the closure has a contract. Any captured mutation requires a contract-bearing function type.
  • Escaping closures that touch $Self require full contracts (requires/ensures plus reads/modifies).
  • Uncontracted callback types are treated as pure only if the value flowing into the type is provably pure. Purity is enforced at value-flow boundaries (argument passing, let/var bind, return, store), not just call sites.
  • Inside a callee, contractless function parameters are treated as pure-like because call sites already prove purity or trust.
  • Contract subtyping: requires are contravariant, ensures covariant, and reads/modifies must be subsets. Logical implication is checked via Viper obligations.

Iteration Rules​

  • for (x in it) requires an iterator with a contracted next (Iter<T> or structural equivalent). Contracts, not AST patterns, control verification.
  • Built-in array, blob, and text iterators use contracted next thunks.
  • Iterator element types must be spec-immutable (no var, arrays, functions, actors, mutable records).
  • arr.values() lowers to index-based loops. General iterators lower to next() calls with contract checks and element-range assumptions.

Data Structures, Any, and Opaque/Token Instances​

  • No name-based data structure restrictions. Representation types remain visible. Soundness comes from contracts and effects, not hidden types.
  • Any is allowed in verified code as a dynamic escape hatch, but proof precision is intentionally weak. Ownership/escape reasoning treats it as unknown and escaping, so prefer concrete types for strong proofs.
  • opaque T is a verification-only wrapper (nominal per defining module). Outside the defining module, opaque T cannot be inspected (no field access, projections, pattern matching, or structural subtyping), but can be passed, stored, and compared. Inside, it unwraps to T.
  • token T is a shareable value-level wrapper (nominal per defining module). Outside the defining module, token T cannot be inspected. Inside, it unwraps to T. Shared signatures use the token wire wrapper described below. Mutable handle usage is further restricted; see the handle section.

Opaque/Token Handle Capability Rules​

Opaque/token handles are module-owned identities with sealed payloads. The verifier tracks them with handle-capability summaries rather than by ad hoc container names.

  • Public module APIs may mention handles when the verifier has a handle-capability summary for the callee. Public actor/shared signatures may not mention local-only opaque handles directly.
  • Public type aliases may not expose opaque or token handles from other modules.
  • Public async signatures may not mention local-only handles; handle APIs are synchronous module APIs.
  • Public handle APIs must be non-bodyless for runtime use. The narrow proof-only bodyless exception is an explicit public ghost abstract func summary over handles; trusted or non-ghost bodyless handle APIs remain rejected.
  • If a public handle API mentions deep-handle types (opaque or token with mutable payload), the owner module must expose a public proof-visible model(...) surface, usually public ghost func model(...) or a real public pure func model(...) runtime observer.
  • There is no generated public valid(handle) observer. Generic opaque validity is implicit in the owned/folded carrier predicate; public APIs preserve it and expose only domain-specific model/observer facts when callers need them.
  • Verified public mutators that write handle payloads need model/effect-relevant postconditions: observer transitions against old(...), observer preservation/final-state facts, or result/receipt facts tied to observer calls. Vacuous contracts such as ensures true and self-tautologies such as model(x) == model(x) are rejected for payload writes.
  • Handles may be passed to non-owner modules and returned from non-owner modules, including nested inside records, options, tuples, variants, arrays, BMap, MBMap, BSeq, and proof collections such as Map, Seq, Set, and Multiset.
  • Non-owner modules may use a foreign handle only by calling the owner module's public API. They may not inspect, project, pattern-match, forge, or mutate the sealed payload directly.
  • Handles may not be passed to unknown callees or functions that do not explicitly accept them. Runtime calls passing handles to bodyless callees without consumed proof-only summaries are rejected.
  • Higher-order handle APIs require a known callable descriptor with a consumed handle-capability summary. Unknown or declaration-only callable paths remain rejected.
  • Handles may not be sent to other actors directly; only shareable token wire types may cross shared boundaries via token wrappers.
  • Nested shareable tokens in shared return types are allowed. The compiler rewrites containers structurally and applies toShared and fromShared at the appropriate leaves.
  • Actor fields may store handles and handle-bearing private carriers, including BMap, MBMap, and BSeq registries, but await liveness is conservative for actor-state reachable handles.
  • Fresh local handles may cross await and later call the owner API. Handles recovered from actor-owned option, record, tuple, variant, array, BMap, MBMap, BSeq, or other actor-owned carriers may not be kept live across await.
  • Container models expose handle identity, not owner payload snapshots. Equality of Map<K,H>, Seq<H>, BMap<K,H>, or BSeq<H> models proves which handles are present; it does not prove Owner.model(h) stayed unchanged after a possible owner mutation. Exact BMap.entries / MBMap.entries snapshots and BSeq.toArray / BSeq.toList / BSeq.freeze snapshots keep that same identity-only boundary for handle elements.

Shareable Token Wrappers (Default)​

These rules apply by default for shareable token types.

  • A module may define at most one token type.
  • If a module defines public type Name = token { ... }, it must also define a public module NameShared.
  • NameShared is restricted to:
    • type Shared
    • private toShared(t : Name) : Shared
    • private fromShared(s : Shared) : Name
    • no other types or values (except a compiler-inserted proof helper)
  • toShared and fromShared must be non-async and are untrusted; their bodies are verified.
  • The compiler inserts a private proof helper inside NameShared that enforces toShared(fromShared(s)) == s (checked field-by-field for record wire types).
  • The compiler computes a module hash (CHASH) from the typed AST and tags the wire type as { __mod$<hash> : NameShared.Shared }.
  • Shared function signatures are rewritten so every shareable token position (including nested inside arrays, records, variants, options, tuples) is replaced with its wire wrapper. The compiler inserts fromShared on entry and toShared on return.
  • Shared functions that expose shareable token values must declare sr9.
  • sr9 is allowed even without shareable tokens to require proof.
  • Proof wrappers and signature verification are emitted only in IC/Ref modes. In LLVM and Elixir backends, sr9 is treated as trusted: no __proof$ wrapper or proof init args are used, and verified is set true for those entries.
  • sr9 rejects non-canister principals (anon, self-auth, derived, reserved) before proof parsing and verification.
  • Verified shared calls wrap arguments and returns as { __proof$ : Blob; __data$ : <wire> } and validate proofs before use.
  • User code cannot declare __mod$, __proof$, or __data$-prefixed fields or construct the wire wrapper manually.
  • Counterfeit tags (wrong __mod$<hash> label) are rejected at decode time with a Candid record-field mismatch, which traps the call.
  • Stable upgrade storage is not a shared boundary. Token stable compatibility is tied to the defining token module CHASH and must not call toShared or fromShared; local opaque stable compatibility follows ordinary Motoko raw stable type shape rules.
  • from_candid, to_candid, and call_raw are disabled to prevent bypassing tag checks.
  • Awaiting a shared call that moves token arguments must be enclosed in try { } catch { } (current check covers direct await of a shared call).
  • Converting token values to Any is rejected, including inside the owner module when the token is otherwise visible.
  • Runtime compilation and Viper lowering rewrite shared signatures to wire types. Viper verifies wrapper signatures (no handles in shared signatures).
  • The compiler injects controller-only __s9_set_proof and __s9_set_gate_key methods to install proof material at runtime; self-calls are rejected so in-canister code cannot overwrite proof or gate key state.

Integer Semantics​

  • Verified builds require checked-int mode; unchecked and bitvec modes are rejected for verification.
  • Division and modulo in specs must be guarded (for example, divisor non-zero).

Sector9-Specific Behavior Notes​

  • Actor init runs before invariants are established; old($Self...) is not meaningful in ActorInit, so size-preservation posts are omitted there.
  • Array size invariants are injected only when a contract explicitly mentions array access (Acc or ArrayAcc), not when relying solely on $Inv or $Perm.
  • Selective imports are global and do not allow scope shadowing. Avoid local names that clash with selective imports if you want the local binding to win.
  • Opaque and token ownership is tracked per module. Inside the owner module, these types are unwrapped for subtyping and inference. Outside, they remain sealed.

Aliasing Unrestriction Steps (Implemented)​

Only steps marked [x] in unrestrict.md are implemented.

  • Step 0: Canonical place keys and explicit disjointness facts. Alias checks use canonical Mvir_place keys and normalized indices.
  • Step 1: Read-only aliasing within an atomic segment. Multiple read-only aliases allowed; writes still reject unless later steps allow them.
  • Step 2: Read-only alias propagation through locals and aggregates (ref-formers like ArrayLocE, FldAcc on ref-typed fields).
  • Step 3: Disjoint record-field writes when projections diverge at the field boundary (place-sensitive).
  • Step 4: Disjoint array element writes only with explicit guards (i != j or proven non-overlap).
  • Step 5: Aliasing through calls with known effects, using mvir_effects summaries; unknown effects remain rejected.
  • Step 6: Loops require invariants that re-establish permissions and disjointness facts; otherwise reject.
  • Step 7: Mixed read/write aliasing only with explicit equality and a single writer; multiple writers still rejected.
  • Step 8: Fresh, non-escaping aliasing (no await crossing). Owned-fresh aliases may write through each other when equality is explicit.
  • Step 9: Controlled aliasing across await is not implemented and remains rejected.

Where the Logic Lives (For Future Changes)​

  • Canonicalization: src/viper/mvir_locn.ml, src/viper/mvir_place.ml, src/viper/mvir_inline_indices.ml, src/viper/mvir_freeze_indices.ml.
  • Alias checks: src/viper/mvir_alias_guard.ml and mutrec-specific passes.
  • Opaque and token handle aliasing: src/viper/mvir_opaque_handle_alias.ml.
  • Await safety: src/viper/mvir_await_locals.ml, src/viper/mvir_await.ml, $expire_borrows in src/viper/perm_state.ml.
  • Effects: src/viper/mvir_effects.ml and annotate_calls.
  • Permissions: src/viper/perm_state.ml, src/viper/perm_amount.ml, src/viper/mvir_perm_fold_unfold.ml, src/viper/mvir_perm_markers.ml.

Summary​

  • Sector9 enforces a strict effect, aliasing, and async model to keep Viper lowering sound.
  • Token and opaque handles are routed by capability summaries: non-owner code can store and pass handle identities, while payload access stays with the owner module and shared boundaries still use token wire wrappers.
  • The restrictions and module pointers above are the authoritative reference for verifier behavior.