Glossary

Key terms and their precise meanings in Sector9.

A

Actor

A Sector9 language construct, inherited from Motoko, representing an Internet Computer canister. Actors encapsulate state and expose public functions. In Sector9, actors are the primary unit of verification - their invariants and method contracts are checked by the verifier.

ANF (A-Normal Form)

An intermediate representation where all subexpressions are named. Sector9 transforms effectful calls to ANF during verification preprocessing to simplify reasoning about evaluation order.

Assertion

A statement that a condition must hold at a specific program point. Sector9 supports three assertion forms: assert (verification-only), runtime:assert (verification + runtime trap), and trap (trap when condition is true).

Assert Unsat

A test outcome encoded with an _unsat filename whose failure is caused by an assertion. Older local notes may say _assert_unsat, but the runner classifies outcomes by the final supported suffix such as _sat, _unsat, _noperm, or _reject.

Async

A function modifier indicating the function returns a future. Async functions can contain await expressions and may be interleaved with other calls between awaits.

Async Star (async*)

A repeatable computation form consumed by await*. It passes control into the callee without forcing an extra interleaving point unless the callee actually reaches a suspending await.

Atomicity

Code between awaits executes without interruption. No external interference occurs within an atomic block - only at await boundaries.

Await

An expression that suspends execution until an async result is available. Await boundaries are points where other actors may modify shared state.

Await Barrier

The verification-level representation of an await expression. At an await barrier, the verifier models potential interference by havocing (invalidating) shared state that may have been modified by concurrent calls.

Await Star (await*)

Executes an async* computation. If the callee cannot suspend, verification treats it like a local atomic call. If the callee may reach a real await, the same try/catch-all and interference rules as await apply.

B

Biconditional (<==>)

Logical equivalence operator. a <==> b is true when both sides have the same truth value. Equivalent to (a ==> b) and (b ==> a).

C

Canister

The unit of deployment on the Internet Computer. In Sector9, canisters are represented as actors. The terms are often used interchangeably, though "canister" emphasizes the deployment artifact while "actor" emphasizes the programming model.

Composite Query

A query function that can call other query functions. Declared with shared composite query. Less common than regular queries.

Contract

A specification of function behavior consisting of preconditions (requires) and postconditions (ensures). Contracts express what a function expects and guarantees without specifying how.

Counterexample

A concrete set of values that demonstrates why verification failed. Use --counterexample to request the verifier to produce failing inputs.

D

Deterministic Mode

A verification flag (--deterministic) that ensures reproducible Viper output. Useful for golden file testing where byte-exact matches are required.

Decreases

A clause that would specify a termination measure for recursive functions or loops. Currently rejected in Sector9 - termination is not verified.

E

Effect

A side effect such as reading or writing state. Effects are tracked via reads and modifies clauses and inferred across the call graph.

Ensures

A postcondition clause specifying what must be true when a function returns. Multiple ensures clauses are conjoined (AND-ed together).

Ensures Unsat

A test outcome encoded with an _unsat filename whose failure is caused by an ensures clause. Use the ordinary _unsat suffix and make the test name describe the failing obligation.

Entry Requires

A runtime entry guard for public/exported actor methods. entry_requires should mirror caller-controlled logical requires clauses, but cannot mention ghost state, old(), or result because it runs at the exported runtime boundary.

Erasure

The removal of verification-only constructs from runtime output. Ghost state, assertions, and contracts are erased - they exist only for verification.

Escape Analysis

A static analysis that classifies objects by ownership: actor-rooted, fresh allocations, or unknown/external. Objects that may escape to external callers are treated as shared and invalidated across await boundaries.

Exists

Existential quantifier. exists<T>(pure func(x : T) : Bool = ...) asserts that at least one value satisfies the predicate. See also: Forall.

F

Footprint

The set of state locations a function may access. Declared via reads (for observation) and modifies (for mutation) clauses.

Forall

Universal quantifier. forall<T>(pure func(x : T) : Bool = ...) asserts that all values satisfy the predicate. Use forallWith for explicit triggers. See also: Exists.

ForallWith

Universal quantifier with explicit triggers. forallWith<T>(predicate, triggers) guides SMT instantiation with the specified trigger functions. Use when automatic trigger inference fails.

Frame Condition

The guarantee that state not listed in modifies remains unchanged. Automatically generated by the verifier.

Framing

The verification technique of proving that state outside a function's footprint is preserved. Unlisted fields are guaranteed unchanged.

Fold/Unfold

Permission management operations for predicate instances. Unfold breaks a predicate into its component permissions; fold reconstructs a predicate from those permissions. Used internally by the verifier to manage ownership predicates.

G

Ghost

Verification-only state or code. ghost var declares ghost variables, ghost { } creates ghost blocks. Ghost constructs are erased from runtime output.

Golden File

Expected verification output stored in test/viper/**/ok/. Used for regression testing - update_goldens.sh refreshes them after intentional changes.

H

Havoc

The verification technique of invalidating (making unknown) the value of state that may be modified. At await barriers, shared state is havoced to model potential interference from concurrent calls.

Heap Model

The abstract representation of program state as a collection of locations with permissions. Actor fields and arrays are modeled as heap locations requiring explicit read/write permissions.

I

Implication (==>)

Logical operator meaning "if...then". a ==> b is true when a is false or both a and b are true. Equivalent to not a or b.

Invariant

A property that must hold at specified points. Actor invariants hold before and after each public method. Loop invariants hold at each iteration.

Interference

The possibility that shared state changes between awaits. The verifier models conservative interference - any modification to shared state may occur at await boundaries.

L

Lemma

A helper function that establishes facts for other proofs. Declared with the lemma modifier. Lemma bodies are verified like methods but exist only for proof purposes.

Linearity

A historical spec-collection rule that required consuming and rebinding values on update. Current Map, Set, Seq, and Multiset values are persistent: updates return new values and do not consume the old version.

Loop Invariant

A property that must hold at the start of each loop iteration. Specified with loop:invariant. The verifier checks it holds initially and is preserved by each iteration.

Lvalue

A location that can be assigned to, represented as a base plus access path (field accesses, array indices). The verifier tracks lvalues to determine what can be read or written.

M

Map

A spec collection representing key-value associations. Operations include Map.empty, Map.get, Map.update, Map.contains, Map.domain, Map.range, and Map.card. See also: Spec Collection.

Modifies

A clause listing fields that a function may change. Grants write permission to listed fields. Unlisted fields are implicitly framed as unchanged.

Motoko

The upstream language Sector9 is derived from. Sector9 remains Motoko-like and legacy .mo files are accepted, but current verified code should be described as Sector9 source.

Multiset

A spec collection allowing duplicate elements with multiplicity tracking. Operations include Multiset.empty, Multiset.count, Multiset.union, and Multiset.card. See also: Spec Collection.

MVIR (Sector9 Verification IR)

The intermediate representation used between Sector9 source and Viper. MVIR preserves effect information and places for the permission and framing analysis passes.

N

Noperm

A test outcome suffix (_noperm) indicating a permission failure. The function accesses state not declared in its reads or modifies clauses.

O

Old Expression (old())

Captures a value at method entry for comparison in postconditions. old(counter) refers to counter's value when the method was called. Only valid in spec contexts.

Ownership Predicate

A predicate (named Owned$TypeName) representing exclusive ownership of a mutable object. When a reference is owned, the owner has full permissions to all fields. Ownership predicates are folded and unfolded automatically by the verifier.

Opaque Owner Transaction

The verifier mode used inside an opaque type's owner module while a mutator is updating payload fields. The owner carrier may stay open and dirty across intermediate writes, but it must be folded and its invariants rechecked before return, await, escaping calls, or explicit owner close points.

Orthogonal Persistence

The IC model where committed actor state persists across messages without explicit serialization. Stable actor fields also persist across compatible upgrades.

P

Partial Correctness

Proving that if a program terminates, it produces correct results. Sector9 provides partial correctness - termination is not verified.

Permission

Access rights to heap locations. The verifier tracks read and write permissions. reads grants read permission, modifies grants write permission.

Permission State

The set of access and predicate permissions available at a given program point. The verifier tracks permission state to schedule fold/unfold operations and verify access rights.

Persistent Actor

An actor declared with persistent actor { }. Ordinary fields are stable by default and survive compatible upgrades; use transient for caches or derived state that should reset.

Postcondition

A condition that must hold when a function returns successfully. Specified with ensures.

Precondition

A condition that must hold when a function is called. Specified with requires. Caller's obligation, function's assumption.

Principal

The IC's representation of identity (user, canister, or system). Used for access control and caller identification. Available via the caller parameter in shared functions.

Place

A stable reference to a heap location, represented as a root (Self, local variable, or result) plus a list of projections (field accesses, array indices). Used throughout the effect system for tracking what can be read or written.

Prelude

The built-in definitions that Sector9 provides for verification, including spec collections (Map, Set, Seq, Multiset), quantifiers (forall, exists), and domain axioms. Part of the trusted base.

Pure

A function modifier indicating no side effects. Pure functions cannot await, mutate state, or access actor fields. They may call pure or trusted helpers with known summaries and may appear in specifications.

Q

Quantifier

An expression over all values of a type. forall<T>(pure func(x : T) : Bool = ...) for universal claims, exists<T>(...) for existential claims.

Query

A shared function that skips consensus for speed and is normally used for read APIs. Declared with shared query. Current verification still requires reads/modifies declarations for any actor fields the body accesses; prefer read-only query APIs because query execution should not be treated as durable consensus state.

R

Reads

A clause listing fields that a function observes but doesn't modify. Grants read permission. Fields in reads but not modifies are framed as unchanged.

Reentrancy

The possibility that a method is interrupted by concurrent invocations from other actors. At each await, the verifier assumes the environment may modify shared actor state arbitrarily.

Reject

A test outcome where the front-end rejects the program before verification. Used for testing syntax errors and type check failures.

Requires

A precondition clause specifying what must be true when a function is called. Multiple requires clauses are conjoined.

Result

A keyword in postconditions referring to the function's return value. ensures result >= 0 constrains what the function returns.

Runtime Assert

A runtime check that traps if the condition is false. Written as runtime:assert condition. The verifier also proves the condition holds.

S

SAT (Satisfiable)

A test outcome where verification succeeds. The contracts are satisfied by the implementation.

Semantic Framing

The technique of shrinking permission bundles based on what locations are actually accessed. Instead of explicit frame assertions, the verifier gives methods permissions only for locations they may touch.

Seq

A spec collection representing ordered sequences indexed by Int. Operations include Seq.empty, Seq.get, Seq.len, Seq.concat, Seq.slice, and Seq.contains. See also: Spec Collection.

Set

A spec collection representing unordered unique elements. Operations include Set.empty, Set.singleton, Set.contains, Set.union, Set.intersect, Set.minus, and Set.subset. See also: Spec Collection.

Shared

A function modifier indicating the function can be called from other actors or clients. Shared update functions execute under consensus; query and composite query shared functions use query execution and are normally read APIs.

Shared State

Actor fields and any local variables that may alias actor state or escape to external callers. Shared state is invalidated across await boundaries to model potential interference.

Silicon

The Viper verification backend used by Sector9. Silicon translates Viper programs to SMT queries that Z3 solves. Controlled with --cores for parallelism and --verify-timeout-ms for time limits.

Signature-Only Declaration

A bodyless trusted or abstract declaration. A bodyless trusted function is a deliberate assumption; an abstract function is a verifier placeholder. Plain bodyless declarations are rejected.

SMT (Satisfiability Modulo Theories)

The underlying decision procedure used by the verifier. SMT solvers like Z3 determine if logical formulas are satisfiable.

Soundness

The property that the verifier does not accept code that violates its modeled contracts. Sector9's guarantee is conditional on the trusted base, backend solver, and the verifier's supported execution model.

Spec Collection

Mathematical collections for verification: Map, Set, Seq, Multiset. These are ghost-only, immutable, and used for abstract reasoning.

Spec-Immutable

A type restriction for spec collection elements. Elements cannot contain var fields, mutable arrays, functions, actors, or async types.

Stable Variable

Actor state that persists across upgrades. Declared with stable var.

T

Test Level

Numbered test/viper/level* directories organizing verification tests by increasing complexity. Level 1 covers basic arithmetic and contracts; higher levels cover advanced features like async, mutable records, and quantifiers. Not every number is necessarily present in the current tree.

Trap

A runtime failure that aborts execution and rolls back state. trap condition traps when the condition is true. The verifier proves trap conditions cannot occur.

Trigger

A pattern that guides SMT quantifier instantiation. Use forallWith for explicit triggers when automatic inference is insufficient.

Trusted

A function modifier indicating the body is assumed correct without verification. Contracts are still checked at call sites, but the implementation is not verified.

Trusted Base

The set of axioms, primitive operations, and user assumptions that Sector9 relies on without proof. Includes generated Viper prelude axioms, primitive spec collection operations, trusted functions, and abstract/spec stubs.

U

UNSAT (Unsatisfiable)

A test outcome where verification fails. The contracts cannot be satisfied by the implementation - there's a bug or missing specification.

Update

A state-modifying shared function that goes through consensus. Standard shared functions without the query modifier are update functions.

V

Verification

The process of mathematically proving that code satisfies its specification. Sector9 translates Sector9 source to Viper and uses SMT solving.

Viper

The intermediate verification language used by Sector9. Sector9 source is translated to Viper, which is then verified by an SMT-based backend.

W

Wildcard Permission

A weak read permission that allows observation without exclusive access. In Viper, encoded as acc(..., wildcard). Contrasts with full/write permission.

Write Permission

Full exclusive permission allowing both reading and modifying a location. In Viper, encoded as acc(..., write). Contrasts with wildcard/read permission.

Z

Z3

The SMT solver used by Silicon to discharge verification goals. Z3 determines if logical formulas encoding the program properties are satisfiable.

Summary

• Contracts: requires, ensures, modifies, reads define function specifications
• Assertions: assert (verification-only), runtime:assert (both), trap (error condition)
• Ghost: ghost var, ghost { } for verification-only state and code
• Quantifiers: forall, exists, forallWith for universal/existential claims
• Spec Collections: Map, Set, Seq, Multiset for abstract reasoning
• Permissions: Read vs write access, ownership predicates, fold/unfold operations
• Concurrency: Atomicity between awaits, interference at await barriers, escape analysis
• Test Suffixes: _sat (passes), _unsat (fails), _reject (syntax error), _noperm (permission error)
• Pipeline: Sector9 source -> MVIR -> Viper -> Silicon -> Z3 (SMT)