Glossary

Terms that appear throughout the Verum documentation, with precise meanings.

A

Affine type — A type whose values may be used at most once; the compiler forbids duplication but allows discarding. Declared with type affine T is ....

AOT — Ahead-of-Time compilation. Verum's LLVM backend that produces native binaries. Tier 1 of the two-tier execution model.

Aliasing — Multiple references to the same value. Verum's rules: any number of immutable (&T), or exactly one mutable (&mut T).

Attribute — A compile-time annotation written with @ prefix, such as @derive(Clone) or @verify(formal).

C

Capability — (1) In the context system, a typed effect like Database or Logger. (2) In CBGR, one of eight bits indicating a reference's allowed operations (READ, WRITE, EXECUTE, DELEGATE, REVOKE, BORROWED, MUTABLE, NO_ESCAPE), subject to monotonic attenuation.

CBGR — Capability-Based Generational References. Verum's default memory safety mechanism: ~15 ns runtime check per deref.

Cog — A Verum package. Distributable archive containing VBC, metadata, and optional proof certificates.

Context — A typed capability requested via using [...] and provided via provide. Replaces globals / thread-locals.

Contract — A function specification: where requires, where ensures, loop invariant, decreases.

Cubical — Cubical type theory. Verum's foundation for path types and higher-inductive types with computational univalence.

D

Dependent type — A type that depends on a value. Π-types (function types whose return depends on an argument), Σ-types (pairs whose second depends on the first), path types.

Derive — Automatic generation of protocol implementations via @derive(P).

E

Epoch — A counter in CBGR that prevents generation wraparound. Each thread advances its epoch periodically.

Escape analysis — Compile-time inference of whether a reference can outlive the scope that produced it. Used to promote &T to &checked T.

Execution mode — Interpreter (direct VBC interpretation, instant startup) or AOT (VBC lowered through LLVM for CPU, or MLIR for @device(gpu) code). Verum does not have a JIT tier. See Runtime tiers.

Execution tier — The CBGR safety tier attached to each reference: Tier0_Full (~15 ns), Tier1_Epoch (~8 ns), Tier2_Gen (~3 ns), Tier3_Unchecked (0 ns). Independent of execution mode.

F

FatRef — 32-byte reference for unsized types (slices, dyn).

FFI — Foreign Function Interface. extern "C" blocks; C ABI only.

G

Generation — A 32-bit counter in an allocation's CBGR header, incremented on free. A reference with a stale generation is rejected.

Generic — A type or function parameterised by types, const values, lifetimes, kinds, or contexts.

H

HIT — Higher-Inductive Type. A sum type with path constructors — i.e., constructors that produce equalities, not just values.

HoTT — Homotopy Type Theory. The family of type theories in which path types and univalence are first-class. Verum implements a cubical fragment.

I

Incremental compilation — Re-compiling only the functions whose source or dependencies changed. Verum's default mode.

Invariant — A property that holds at every iteration of a loop, stated with invariant clause.

is — Reserved keyword. Used in type T is ... and as a pattern / type-test operator.

L

Linear type — A type whose values must be used exactly once. Stronger than affine.

LSP — Language Server Protocol. verum lsp implements LSP 3.17.

M

Mathesis — Verum's ∞-topos of formal theories; a research-facing stdlib module.

Meta function — meta fn — a function that runs at compile time.

MIR — Mid-level IR used during optimisation phases, between AST and VBC.

Module — A .vr file or a directory with mod.vr. Imported with mount.

N

Nursery — A structured-concurrency scope. Owns a set of tasks; does not return until they are all joined or cancelled.

O

Obligation — A proof requirement generated by the verifier, such as "prove xs[i] is in bounds" or "prove the postcondition holds."

Orphan rule — Cross-cog protocol-implementation coherence: an implement P for T is valid only if P or T is from the defining cog.

P

Path type — Path<A>(a, b) — a proof that a and b are equal in type A, treated as data that can be transported.

Portfolio (verification) — Running the SMT backend in parallel on the same obligation and cross-validating.

Protocol — A trait / interface. Declared as type P is protocol { ... }.

R

Refinement type — A type plus a predicate that every value must satisfy: Int { self > 0 }.

Refinement reflection — Extending the refinement vocabulary by making @logic functions available as SMT axioms.

S

Semantic honesty — Verum's rule that type names describe meaning, not implementation: List (not Vec), Text (not String).

SMT — Satisfiability Modulo Theories. The class of solvers Verum's verification backend dispatches to. Language-level Verum does not commit to a specific SMT solver; the current implementation bundles Z3 and CVC5 as backends behind the capability router, and a Verum-native solver is on the roadmap.

SSA — Static single assignment form. Used by CBGR analysis.

Structured concurrency — Concurrency organised into lexical scopes (nurseries) that own their tasks' lifetimes.

T

Task — A unit of async execution. Spawned with spawn; joined via a JoinHandle.

Theorem — A proved statement declared with the theorem keyword.

ThinRef — 16-byte reference for sized types.

Tier — See "Execution tier" and "Reference tier."

Transport — Moving a value along a type-level path. Key operation in cubical type theory.

U

Univalence — The axiom "type equivalence is type equality." Verum implements it computationally in its cubical fragment.

V

V-LLSI — Verum Low-Level System Interface. Zero-FFI kernel layer.

VBC — Verum ByteCode. The compiler's unified intermediate representation. Every tier runs on VBC.

VCS — Verum Conformance Suite. The comprehensive language test suite at vcs/.

Z

Z3 — One of the SMT solvers the current verification backend can dispatch to (alongside CVC5). Implementation detail, not a language commitment — see SMT.