Skip to main content

core.base — Foundational types and protocols

Everything in core.base is loaded by the prelude — you do not need to mount it. It contains the types and protocols that every other module assumes.

This page enumerates every public item.

FileWhat's in it
maybe.vrMaybe<T>, MaybeIter<T>, collect_maybe, flatten_maybe
result.vrResult<T,E>, ResultIter<T>, Error
ordering.vrOrdering
ops.vrControlFlow<B,C>, Try, FromResidual, Never, Drop
protocols.vrthe operator and capability protocols (Eq, Ord, Hash, Clone, Copy, Default, Debug, Display, Send, Sync, Add..Shr, From/Into, Deref/AsRef, Numeric, …)
iterator.vrIterator protocol + 30+ adapters
cell.vrCell, RefCell, OnceCell, LazyCell, Ref, RefMut
memory.vrHeap<T>, Shared<T>, Weak<T>, Cow<T>, Pin<P>, ManuallyDrop<T>, MaybeUninit<T>
panic.vrpanic, assert, unreachable, todo, catch_unwind, PanicInfo
env.vrargs, var, home_dir, os_name, arch, exit
data.vrData (dynamic JSON-like value), parse_json
serde.vrSerialize, Deserialize, Serializer, Deserializer
error.vrStackFrame, Backtrace, ErrorProtocol, ErrorChain
log.vrLogLevel, Logger, LogRecord, trace/debug/info/warn/error
coinductive.vrcorecursive analysis (CorecursiveCall, check_productivity, bisimilar_up_to)
primitives.vrinherent methods on Int, Float, Bool, Char, Byte

Module status

Each core.base.* module carries an explicit conformance status so you know what you can rely on today versus what is still in flight. The status is the truth-table over the module's public-API surface as exercised by core-tests/base/<module>/ under both verum test --interp (Tier 0 VBC interpreter) and verum test --aot (Tier 2 LLVM AOT). The same source file MUST pass both — interpreter/AOT divergence is itself a test failure (see core-tests/ for the discovery contract).

StatusMeaning
stableEvery public method is conformance-tested under --interp and --aot. Algebraic laws are pinned by exhaustive or large-domain property tests. Cross-stdlib integration is verified. Safe to depend on in production.
partialSubset of the public API is conformance-tested and stable. The rest is exercised in regression_test.vr via @ignored tests pinning the specific defects that block coverage. The non-ignored API surface is safe; everything else is documented per-module under "Open defects".
regression-onlyModule is gated by upstream stdlib / language-level defects (function-id remap, archive-driven default-method dispatch, CBGR generation tracking on returned &Text, …). Public-API tests do not pass yet — only @ignored regressions exist to lock the bug shapes. Avoid in production until promoted.
undocumentedDocumentation in this reference is authoritative, but the module has not yet been routed through the core-tests/ conformance suite. The current page is a best-effort snapshot of the source; it may drift from runtime behaviour.
ModuleStatusConformance suite
maybe.vrpartialcore-tests/base/maybe — 65/75 pass. Remaining 10 gated by MaybeUninit.assume_init StackOverflow via forget/ptr_read unsafe primitives + CBGR generation tracking.
result.vrpartialcore-tests/base/result — 78/90 pass. Remaining gated by variant-payload field-index drift on user error types + closure dispatch in retry_with_result_list_accumulation.
ordering.vrpartialcore-tests/base/ordering — 18/23 pass. Tier-0 dispatcher inlines Int.cmp, Float.cmp (NaN-as-Equal), Bool.cmp (false < true), Text.cmp. Remaining failures cluster on Text.cmp CBGR-ref deref path under apple.cmp(&banana) argument shape.
ops.vrpartialcore-tests/base/ops — 3/7. closure-dispatch cluster blocked.
protocols.vrstablecore-tests/base/protocols — 2/2 conformance.
iterator.vrpartialcore-tests/base/iterator — 11/19. Range.collect/map/inspect and iter().find/next blocked on transitive module loading (Iterator default-method bodies in core.base.iterator not in user wanted_module_prefixes).
cell.vrpartialcore-tests/base/cell — 15/28. Cell family stable; RefCell Ref/RefMut Deref auto-deref landed in commit 170820255 but LazyCell.force still gates on RefMut being in transitive wanted set.
memory.vrpartialcore-tests/base/memoryHeap.new / Heap.into_inner / Heap.try_new / nested-heap round-trips stable in both interpreter and AOT. CBGR introspection surface (is_valid, is_allocated, is_freed, generation, epoch, header_generation, current_epoch, header_epoch, capabilities, header_size) exposed and round-trip-tested under cbgr_test.vr — 4/18 pass in interp baseline. Remaining 14 fail on assertion failed: left != right (incl. test_heap_default, test_heap_cbgr_after_modification); root-cause hypothesis is T.default() primitive-protocol-default dispatch resolving to non-zero sentinel in interpreter. Stdlib companion fix landed in this branch: duplicate Heap.is_freed definition removed; language-level dup-method check added (see Open defects below).
panic.vrpartialcore-tests/base/panicpanic/assert/unreachable stable; catch_unwindPanicInfo.location gated by CBGR use-after-free in &Text return-refs.
env.vrstablecore-tests/base/envargs/var/home_dir/os_name/arch/exit exercised under interp + AOT.
data.vrpartialcore-tests/base/data — 27/33. Remaining gated by pattern_data_pipeline assertion drift.
serde.vrpartialcore-tests/base/serde — 16/17. Only collect_multiple_serde_errors blocked.
error.vrpartialcore-tests/base/error — 54/89. StackFrame.new / Eq / format stable; remaining failures span variant-payload drift + Display/Debug formatter dispatch via f"{...}".
log.vrpartialcore-tests/base/log — 14/19. LogLevel, LogRecord, builders, level_trace/debug/info/warn/error constructors all green. Field-iteration tests gated by archive-driven iter().find(...) default-method dispatch.
coinductive.vrundocumented
primitives.vrpartialcore-tests/base/primitivesInt.checked_add / checked_sub / wrapping_* / saturating_* / to_le_bytes etc. stable post-fix (typechecker now populates inherent_methods from the archive — see commits 4112766c1 + dc64b1142). Int.MAX, Int.BITS, Float.BITS, Float.NAN, Float.INFINITY, Float.PI, Float.MAX, Float.MIN, Float.EPSILON, Float.NEG_INFINITY constants stable post-fix (body-compiled const archive descriptor now carries is_const = true AND return_type = TypeRef::Concrete(<primitive TypeId>) — see commits d52cd695c + acbdb2f32). Per-type integer-arithmetic conformance suites (int_test.vr, float_test.vr, uint_isize_test.vr, bitmanip_test.vr, bool_byte_char_test.vr, comparison_test.vr, arithmetic_edge_test.vr, property_test.vr) now compile to typecheck; runtime green count tracked in core-tests/base/primitives/.
glob.vrpartialcore-tests/base/glob — 1/3. POSIX class + literal matching; globstar (**) cross-separator gated by str.as_bytes archive load.
coercion.vrpartialcore-tests/base/coercion — 1/2. IntCoercible / Indexable / RangeLike / TensorLike / BytewiseFfi marker protocols loaded from .vr; numeric_field_coercion blocked by field-index drift.
mod.vrpartialcore-tests/base/mod — 1/4. VERSION constants exposed; Range.inspect default method gated.
nanoid.vrregression-onlycore-tests/base/nanoid — 0/1. function-id remap.
string_distance.vrundocumented
ulid.vrregression-onlycore-tests/base/ulid — 0/6. ulid_from_parts function-id remap; sequential-ULID lex-ordering tickles StackOverflow in monotonic-counter loop.
uuid.vrpartialcore-tests/base/uuidUuid.parse/from_bytes stable; Uuid.to_text previously lenient-skipped on Text.new (one of ~400 Text.* method cascade entries at May-11 baseline). Tracked under task #16 (twice attempted reland regressed; runtime sentinel handler durably landed via commit b5f5462d4) (commits b5f5462d4 runtime sentinel handler + 5b657aa16 stage-1 + 98fced985 stage-2 + 7cdb334b2 + 86784eebf stub-overwrite discipline): caller-modules now see Text.new / List.from / AtomicInt.new / Duration.from_secs / variant constructors as stubs from compile-time-zero; producing modules' real bodies overlay the stubs via the sentinel-ID-range overwrite gate at stdlib_bootstrap.rs:1453; stuck stubs (when producing module itself fails precompile) degrade gracefully via the runtime sentinel handler with a clean [lenient] task#16 stage-N stub never resolved panic. Stage 1 targets 386 Text-method skips; combined with Stage 2's 131 variant-constructor skips, ~631 of 1333 fresh-baseline skips (≈47%) close as one architectural fix.
snowflake.vrregression-onlycore-tests/base/snowflake — 0/6. function-id remap.
semver.vrregression-onlycore-tests/base/semver — 0/2. format/format_semver aliased; tests still gated by function-id remap when the test compilation unit references a stdlib helper.
semver_constraint.vrundocumented
retry.vrregression-onlycore-tests/base/retry — 3/14. Closure receiver lowered as non-pointer at the call_closure site; RetryStrategy builder API stable, retry() itself blocked.

The status table is the runtime truth, not the file's lifecycle annotation — lifecycle: Lifecycle.Theorem("v0.1") is the spec lifecycle (what the contract promises), while the table above is the implementation lifecycle (what the runtime currently delivers). When the two diverge, the table is the source of truth for callers.

Method-dispatch surface

The runtime's method-dispatch flow combines several mechanisms — each contributes a class of behaviours that user code relies on. Knowing which mechanism fires for a given call site helps narrow runtime "method not found" diagnostics.

LayerWhat it dispatchesExample
Tier-0 inlineBuilt-in primitive methods (Int.cmp, Bool.lt, Float.partial_cmp, Text.eq, List.len, Map.get, ...) compiled into the Rust dispatcher for zero overhead.42.cmp(&43) == Less
Receiver-type qualified lookup<TypeName>.<method> against the function table; uses the receiver heap-header's TypeId to recover the type name.MyError.message(&err)
Built-in TypeId → canonical-name fallbackWhen the receiver carries a hardcoded built-in TypeId (Range/List/Map/Set/Maybe/Result/...) but no TypeDescriptor exists in self.types, the dispatcher maps the TypeId to the canonical name (Range for TypeId(517) etc.) and retries the lookup.range.collect() where range has TypeId::RANGE
Receiver-type override (qualified mismatch)When codegen emits T.method but the runtime receiver is actually a different type (alias/inference drift), the dispatcher retries with <actual>.<bare>.r.is_err() codegen'd as Text.is_err on a Result receiver
Protocol-default-method fallbackWalks the receiver's TypeDescriptor.protocols; for each impl, tries the protocol's default body (<ProtocolName>.<method>).err.message() on a user MyError that implement ErrorProtocol without overriding message
Deref-protocol auto-derefWhen method dispatch fails on a heap receiver, walks the Deref chain (bounded depth 4) calling deref() to unwrap inner values, then retries dispatch by qualified name.refmut.push(item) on RefMut<List<T>>
Target-type-aware .into() rewriteAt codegen time, let x: T = expr.into() rewrites to T::from(expr) when T.from exists in the function table.let opt: Maybe<Int> = 42.into()Some(42)
Unique bare-suffix matchLast resort when bare-name method is unique across the function table (single function ending in .<name>); skipped on ambiguity.unqualified it.next() resolving to a unique *.next

Stdlib bootstrap pre-pass architecture (task #16)

Stdlib precompile runs in two stages inside verum_compiler::pipeline::stdlib_bootstrap::compile_core:

  1. STEP 3 — global typechecker registration across ALL stdlib modules (Pass 0–5: import aliases, cross-module imports, type names, type bodies, function signatures, protocols, impl blocks). At the end, the typechecker's inherent_methods / variant_constructor_parents / inductive_constructors are populated with the entire stdlib surface.

  2. STEP 3.5 + 3.6 — global VBC-codegen registry pre-pass (introduced May-11 to close ~631 of 1333 lenient-skips):

    • 3.5 — for every implement <CanonicalType> { public fn ... } inherent-impl block where <CanonicalType> is in the closed canonical-stdlib set (Text / List / Map / Set / Deque / BTreeMap / BTreeSet / Heap / Shared / Weak / Cow / Pin / Mutex / RwLock / AtomicInt / AtomicBool / AtomicU64 / AtomicI32 / AtomicU32 / Channel / Semaphore / Duration / Instant / Maybe / Result), pre-register every public method as a stub FunctionInfo keyed under <CanonicalType>.<method> into global_function_registry. Stub FunctionId lives in the sentinel range u32::MAX - 0x40_0000...

    • 3.6 — for every type X is A | B | C(T) | D { f: F }; declaration, pre-register every variant constructor under qualified <X>.<Variant> (unconditional) and simple <Variant> (first-wins). Stub FunctionId lives in u32::MAX - 0xC0_0000.. (distinct from 3.5 range).

  3. STEP 4 — per-module VBC codegen. Each compile_core_module_from_ast calls codegen.import_functions(&self.global_function_registry) so its private codegen ctx sees EVERY canonical-stdlib stub from compile-time-zero. Function bodies that reference Text.new / AdMysql / Duration.from_secs resolve immediately via the stub's qualified name, regardless of whether the producing module has finished compiling yet.

  4. STEP 4 export-back — when each module completes, its real bodies export back to global_function_registry via the stub-overwrite gate at stdlib_bootstrap.rs:1453: entries whose existing FunctionId falls in the stage-1 or stage-2 sentinel range are OVERWRITTEN; everything else preserves the original first-wins discipline. Real bodies always replace stubs, never the other way around.

Net effect: Text.new is reachable from every stdlib body regardless of its file's compilation order vs core/text/text.vr. Same for AdMysql, Duration.from_secs, and every other canonical- type constructor + variant. Closes tasks #4 + #8 (Text.from cascade) as side-effects.

The sentinel-ID ranges are 1M slots each — single bootstrap typically registers thousands of stubs, well within range. Stubs become permanent if the producing module FAILS to compile (existing first-wins preserves whatever the export-back exposed); since stub bodies are Call { func_id = sentinel } and the archive has no function at that id, the runtime previously rejected the call with the cryptic Function N not found — strictly worse than the pre- fix clean lenient-skip panic carrying the original method name.

The runtime-side sentinel-stub handler at verum_vbc::interpreter::dispatch_table::handlers::calls::handle_call (commit b5f5462d4) closes this gap: it detects the stage-1/stage-2 sentinel ranges at the dispatch boundary BEFORE the get_function ok_or-raise and emits a clean diagnostic:

Panic: [lenient] task#16 stage-N <class> stub never resolved
(func_id=X); the producing stdlib module failed precompile —
check stderr for `[lenient] SKIP <Type>.<method>` warnings during
the build

<class> is "canonical-type static method" for stage-1 stubs and "stdlib variant constructor" for stage-2 stubs. The runtime sentinel handler is durable — it lives in tree regardless of whether stages 1+2 themselves are currently active, so future re-applications of the pre-pass don't risk the regression that forced the original revert (stuck stubs degraded catastrophically without the handler).

Commits: b5f5462d4 (runtime sentinel handler — durable safety net) + 5b657aa16 (stage-1, relanded from 471066f53) + 98fced985 (stage-2, relanded from 22f2ddebd) + 7cdb334b2 (stub-overwrite, relanded from 37fc3fdc3) + 86784eebf (corrected stub-range check, relanded from e0e759b05).

The reland sequence preserves the original architectural fix while adding the runtime safety net that prevents the catastrophic failure mode discovered during the first attempt (stuck stubs → Function N not found instead of [lenient] X stub never resolved).

The order above is the fallback order — each layer fires only when the previous one missed. Tier-0 always wins; protocol-default and Deref auto-deref are last-mile safety nets. Diagnostics like "method 'X' not found on receiver of runtime kind Y" mean every layer exhausted itself — typically the cause is either (a) the carrier module is not in the lazy-load wanted_module_prefixes (transitive load gap), (b) the receiver's TypeDescriptor genuinely lacks the protocol, or (c) the method name has drifted between source and the archive's compiled body.


Maybe<T> — optional value

type Maybe<T> is None | Some(T);

The Verum equivalent of Option. Used wherever a value may be absent.

Constructing

let a: Maybe<Int> = Maybe.Some(42);
let b: Maybe<Int> = Maybe.None;

let parsed = "42".parse_int(); // returns Maybe<Int>

Inspecting

m.is_some() -> Bool
m.is_none() -> Bool
m.contains(&value) -> Bool // requires T: Eq
m.is_some_and(f: fn(&T) -> Bool) -> Bool
m.is_none_or(f: fn(&T) -> Bool) -> Bool

Unwrapping

m.unwrap() // panics if None
m.expect("must exist") // panics with message
m.unwrap_or(default)
m.unwrap_or_else(|| compute())
m.unwrap_or_default() // requires T: Default

Transforming

m.map(|x| x + 1) // Maybe<U>
m.and_then(|x| if x > 0 { Some(x) } else { None })
m.or_else(|| compute_fallback())
m.map_or(default, |x| x + 1)
m.map_or_else(|| default(), |x| x + 1)
m.filter(|x| *x > 0)
m.flatten() // Maybe<Maybe<T>> -> Maybe<T> (T: Default)

Combining

m.and(other) // Maybe<U>: Some(_).and(x) = x; None.and(_) = None
m.or(other) // Maybe<T>: Some(x).or(_) = Some(x); None.or(y) = y
m.xor(other) // exclusive: Some/None or None/Some
m.zip(other) // Maybe<(T, U)>
m.zip_with(other, |a, b| a + b)

Result interop

m.ok_or(error) // Maybe<T> -> Result<T, E>
m.ok_or_else(|| make_error())

Mutating

m.take() // -> Maybe<T>, leaves *self = None
m.replace(value) // -> Maybe<T>, sets *self = Some(value)
m.insert(value) // -> &mut T
m.get_or_insert(value) // -> &mut T
m.get_or_insert_with(|| compute())
m.get_or_insert_default() // T: Default
m.take_if(|x| should_take(x))

Iteration

for x in m.iter() { ... } // 0 or 1 element
for x in m.iter_mut() { ... }

Module-level helpers

collect_maybe(iter) // Iterator<Maybe<T>> -> Maybe<List<T>> (all-or-nothing)
flatten_maybe(items) // &List<Maybe<T>> -> List<T> (skip None)
flatten_maybe_iter(iter) // Iterator<Maybe<T>> -> List<T>

? operator

? propagates None from a Maybe-returning function:

fn first_word(text: &Text) -> Maybe<Text> {
let space = text.find(" ")?; // returns None early
Maybe.Some(text.slice(0, space))
}

Pitfall — accidental swallowing

m.unwrap_or(default) discards the information that the value was absent. When the absence might indicate a bug, prefer expect (with a precise message) so the panic carries diagnostic value.


Result<T, E> — fallible value

type Result<T, E> is Ok(T) | Err(E);

The canonical error type. By convention E is a dedicated error enum (type ParseError is …) or, for quick code, Text.

Constructing

let r: Result<Int, Text> = Result.Ok(42);
let r: Result<Int, Text> = Result.Err("bad");

Inspecting

r.is_ok() -> Bool
r.is_err() -> Bool
r.is_ok_and(|v| *v > 0)
r.is_err_and(|e| matches(e, Error.Timeout))

Conversion

r.ok() // Result<T,E> -> Maybe<T>
r.err() // Result<T,E> -> Maybe<E>

Unwrapping

r.unwrap() // E: Debug; panics on Err
r.unwrap_err() // T: Debug; panics on Ok
r.expect("must succeed")
r.expect_err("must fail")
r.unwrap_or(default)
r.unwrap_or_else(|e| recover(e))
r.unwrap_or_default() // T: Default

Transforming

r.map(|t| t + 1) // Result<U,E>
r.map_err(|e| ApiError.wrap(e)) // Result<T,F>
r.map_or(default, |t| t + 1)
r.map_or_else(|e| handle_err(e), |t| t + 1)
r.and_then(|t| further(t)) // flatmap on Ok
r.or_else(|e| recover(e)) // flatmap on Err
r.and(other) // (Ok(_), x) -> x; (Err(e), _) -> Err(e)
r.or(other)
r.flatten() // Result<Result<T,E>,E> -> Result<T,E>

Borrowing & inspection

r.as_ref() // Result<T,E> -> Result<&T, &E>
r.as_mut() // -> Result<&mut T, &mut E>
r.inspect(|t| log(t)) // pass-through with side effect on Ok
r.inspect_err(|e| log(e)) // pass-through with side effect on Err

Iteration

for v in r.iter() { ... } // 0 elements on Err, 1 on Ok
for v in r.iter_mut() { ... }

Error (lightweight catch-all)

type Error is { message: Text };
let e = Error.new("something broke");

Implements Debug + Display + Describable + Eq + Clone. Useful when you do not yet have a typed error hierarchy. Replace with a dedicated error enum (type MyError is | NotFound | Timeout(Duration)) once the failure modes stabilise.

? operator

In a function returning Result<_, E>, the ? operator unwraps an Ok or returns the Err early — converting via From if necessary.

fn load_config() -> Result<Config, Error> {
let bytes = fs.read("config.toml")?;
let text = Text.from_utf8(&bytes)?;
toml.parse(&text)
}

Pitfall — unwrap in libraries

unwrap is fine in tests and prototypes. In library code, prefer ? and let the caller decide. expect("invariant: …") is acceptable when you can articulate why panic is the only sane response.


Ordering

type Ordering is Less | Equal | Greater;

The result of cmp. Total ordering primitives.

o.is_less() / o.is_equal() / o.is_greater()
o.is_le() / o.is_ge()
o.reverse() // Less <-> Greater
o.then(other) // lexicographic chain
o.then_with(|| compute()) // lazy chain
o.to_int() // -1 / 0 / 1
Ordering.from_int(n) // parse from -1/0/1

Lexicographic comparison idiom:

fn cmp(a: &Person, b: &Person) -> Ordering {
a.last.cmp(&b.last)
.then_with(|| a.first.cmp(&b.first))
.then_with(|| a.age.cmp(&b.age))
}

ControlFlow<B, C> and Try

type ControlFlow<B, C> is Continue(C) | Break(B);

The protocol behind ?. You rarely write it directly, but it powers custom early-return types:

type Try is protocol {
type Output;
type Residual;
fn from_output(output: Output) -> Self;
fn branch(self) -> ControlFlow<Residual, Output>;
};

type FromResidual<R> is protocol {
fn from_residual(residual: R) -> Self;
};

Maybe, Result, and any user-defined sum type can implement Try to participate in the ? operator.

Never (alias !) is the bottom type; it can be coerced to any type. Returned by panic, exit, infinite loops, etc.


Operator protocols

Implementing these makes your type work with the corresponding syntax. From protocols.vr:

ProtocolSyntaxMethods
PartialEq==, !=eq(&self, other: &Self) -> Bool
Eq(marker)extends PartialEq
PartialOrd<, <=, >, >=partial_cmp(&self, other: &Self) -> Maybe<Ordering>
Ord(sortable)cmp(&self, other: &Self) -> Ordering; min, max, clamp
Hashhashinghash<H: Hasher>(&self, h: &mut H)
Clone.clone()clone(&self) -> Self, clone_from(&mut self, other: &Self)
Copyimplicit copyextends Clone; marker only
DefaultT.default()default() -> Self
Debug{:?}fmt_debug(&self, f: &mut Formatter) -> FmtResult
Display{}fmt(&self, f: &mut Formatter) -> FmtResult
Dropscope exitdrop(&mut self)
Add<Rhs>a + badd(self, rhs: Rhs) -> Self.Output
Sub, Mul, Div, Rem, Negarithmeticanalogous
BitAnd, BitOr, BitXor, Not, Shl, Shrbitwiseanalogous
AddAssign..ShrAssigna += b etc.in-place compound
Index<Idx>xs[i]index(&self, i: Idx) -> &Self.Output
IndexMut<Idx>xs[i] = …index_mut(&mut self, i: Idx) -> &mut Self.Output
Derefauto-derefderef(&self) -> &Self.Target
DerefMutmutable auto-derefderef_mut(&mut self) -> &mut Self.Target
From<T>T.from(x)from(x: T) -> Self
Into<T>x.into()into(self) -> T
TryFrom<T> / TryInto<T>fallible variantswith Error associated type
AsRef<T>&Self -> &Tas_ref(&self) -> &T
AsMut<T>&mut Self -> &mut Tas_mut(&mut self) -> &mut T
Borrow<B> / BorrowMut<B>hash-key borrowingborrow(&self) -> &B

Numeric protocols

type Zero is protocol { fn zero() -> Self; fn is_zero(&self) -> Bool; }
type One is protocol { fn one() -> Self; fn is_one(&self) -> Bool; }
type Numeric is protocol; // implemented by all primitive numerics
type SignedNumeric is protocol extends Numeric;
type Integer is protocol extends Atomic;
type SignedInteger is protocol extends Integer;
type Atomic is protocol; // safe for atomic ops

Capability protocols

type Sized is protocol; // statically sized; auto for almost all types
type Send is protocol; // safe to move across threads
type Sync is protocol; // safe to share `&Self` across threads
type Unpin is protocol; // not structurally pinned
type Any is protocol { fn type_id(&self) -> TypeId; }

Send and Sync are auto-derived; opt out with !Send / !Sync in generic bounds (fn f<T: Send + !Sync>(x: T)).

Error protocols

type Describable is protocol { fn description(&self) -> Text; }
type ErrorSource is protocol extends Describable {
fn source(&self) -> Maybe<&dyn ErrorSource>;
}
type ErrorProtocol is protocol extends ErrorSource {
fn message(&self) -> Text;
fn backtrace(&self) -> Maybe<&Backtrace>;
}
type FromStr is protocol { fn from_str(s: &Text) -> Result<Self, ParseError>; }
type ToString is protocol { fn to_string(&self) -> Text; }

Implementations the stdlib provides

TraitFor
Numericevery primitive integer + every Float*
Integerevery primitive integer
SignedIntegerInt8..Int128, Int, ISize
Atomicevery primitive integer + Bool
HasherDefaultHasher (FxHash-based, wrapping_mul core)

The Display + Debug + Eq triple — error-type contract

Every public stdlib type whose name ends in Error (and every state-machine / status / outcome type whose values cross module boundaries) implements all three of Display, Debug, and Eq. The contract is enforced across ~280 stdlib error types covering async, base, collections, compress, database/{common,sqlite,mysql, postgres}, encoding, intrinsics, io, mem, mesh/{k8s,xds}, meta, net/{dns,h3,http,http2,http3,proxy,quic,tls,tls13,url,websocket}, runtime, security, sys/{common,linux,darwin,windows,signal}, text, time.

Why all three:

  • Display — user-facing message routed through print(...), panic(...), error-renderer, log lines, network-protocol error bodies. Lowercase / sentence-case message; no internal symbol names. e.g. "connection refused: 127.0.0.1:5432".

  • Debug — structured-log payload routed through core.base.log.{trace,debug,info,warn,error}, f"{:?}", snapshot serialisers, gdb-friendly dumps. Symbol-form repr that round-trips back to the literal source constructor. e.g. "DbError.ConnectionRefused { host: \"127.0.0.1\", port: 5432 }".

  • Eq — pattern-test discipline: assert_eq(err, ExpectedKind) in tests, if err == NetworkError.Timeout { … } in retry logic, Set<MyError> in dedup workflows.

Recipe by error-type shape (the four canonical patterns):

// Pattern 1 — All-unit variants. Tag-int helper avoids the
// path-type confusion that bites pair-form match on single-variant
// types.
fn my_err_tag(e: &MyError) -> Int {
match e {
Foo => 0,
Bar => 1,
Baz => 2,
}
}
implement Eq for MyError {
fn eq(&self, other: &MyError) -> Bool {
my_err_tag(self) == my_err_tag(other)
}
}

// Pattern 2 — Mixed unit + payload variants. Direct match-pair
// with field renaming on payload arms; cross-variant fall-through.
implement Eq for MyError {
fn eq(&self, other: &MyError) -> Bool {
match (self, other) {
(MyError.Timeout, MyError.Timeout) => true,
(MyError.Other(a), MyError.Other(b)) => a == b,
_ => false,
}
}
}

// Pattern 3 — Single-variant unit type. Trivial Eq; deliberately
// avoids `(SoleVariant, SoleVariant) => true` form that the type
// checker reads as a path-type lookup for the bare variant name.
implement Eq for MyError {
fn eq(&self, _other: &MyError) -> Bool { true }
}

// Pattern 4 — Record-form error with multiple fields. Compare
// every field; structural equality.
implement Eq for MyError {
fn eq(&self, other: &MyError) -> Bool {
self.code == other.code
&& self.message == other.message
&& self.span == other.span
}
}

When not to add Eq:

  • The error wraps a trait object (Heap<dyn Error>, List<Heap<dyn Error>>). The Error protocol is intentionally not Eq-extending — comparing two trait objects via .message() text would be an oracle leak masquerading as structural equality. Defer Eq with an inline rationale comment.

  • The error carries a payload of type Span (or any other type whose Eq impl is unstable / position-dependent) and structural span-comparison would surface false negatives across re-parses. Compare the meaningful fields only and document the elision.


Iterator and adapters

type Iterator is protocol {
type Item;
fn next(&mut self) -> Maybe<Self.Item>;
fn size_hint(&self) -> (Int, Maybe<Int>);
// ... 60+ default methods
}

Consuming methods (terminal)

.count() // -> Int
.last() // -> Maybe<Item>
.nth(n) // -> Maybe<Item>
.advance_by(n) // -> Result<(), Int>
.collect<C>() // -> any C: FromIterator<Item>
.fold(init, |acc, x| ...) // -> B
.reduce(|a, b| max(a,b)) // -> Maybe<Item>
.try_fold(init, |acc, x| ...)
.scan(state, |st, x| ...)
.all(|x| pred(x)) // -> Bool (short-circuits on false)
.any(|x| pred(x)) // -> Bool (short-circuits on true)
.find(|x| pred(x)) // -> Maybe<Item>
.find_map(|x| ...) // -> Maybe<U>
.position(|x| pred(x)) // -> Maybe<Int>
.sum() // -> Item: Add + Zero
.product() // -> Item: Mul + One
.min() / .max() // -> Maybe<Item> (Item: Ord)
.min_by_key(|x| key(x)) / .max_by_key
.min_by(|a,b| cmp) / .max_by
.min_max() // -> Maybe<(Item, Item)>

Adapter methods (lazy — return new iterators)

.map(|x| f(x)) // MappedIter
.filter(|x| pred(x)) // FilterIter
.filter_map(|x| ...) // FilterMapIter
.flat_map(|x| produce_seq(x)) // FlatMapIter
.flatten() // FlattenIter — Iter<Iter<T>> -> Iter<T>
.take(n) // TakeIter
.skip(n) // SkipIter
.take_while(|x| pred(x)) // TakeWhileIter
.skip_while(|x| pred(x)) // SkipWhileIter
.chain(other_iter) // ChainIter
.zip(other_iter) // ZipIter
.enumerate() // EnumerateIter — yields (Int, Item)
.peekable() // PeekableIter — adds .peek()
.dedup() // DedupIter — removes consecutive equals
.interleave(other_iter) // InterleaveIter
.step_by(stride) // StepByIter
.inspect(|x| log(x)) // InspectIter — pass-through with side effect
.fuse() // FuseIter — None stays None
.cycle() // CycleIter — repeats forever
.cloned() / .copied() // Iter<&T> -> Iter<T>
.chunks(n) // ChunksIter — windows of n
.windows(n) // WindowsIter — sliding window
.intersperse(separator) // IntersperseIter
.intersperse_with(|| sep()) // IntersperseWithIter
.pairwise() // PairwiseIter — yields (Item, Item)
.zip_longest(other) // ZipLongestIter
.map_while(|x| ...) // MapWhileIter — stops on None
.by_ref() // ByRef — iterate without consuming

Idiomatic chains

// sum of squares of odd numbers in 0..100
let s: Int = (0..100).filter(|x| x % 2 == 1).map(|x| x * x).sum();

// first prime > 1000
let p = (1001..).find(|n| is_prime(n));

// dedupe a sorted list and join with commas
let csv: Text = sorted.iter().dedup().map(|x| x.to_string())
.intersperse(",".to_string()).collect();

// produce a Map<Int, List<String>> grouped by length
let by_len: Map<Int, List<Text>> = words.iter()
.fold(Map.new(), |mut m, w| {
m.entry(w.len()).or_insert_with(List.new).push(w.clone());
m
});

Pitfall — re-using a consumed iterator

Iterators are single-use unless they implement Clone. Use .by_ref() when you want to consume only part of an iterator and keep iterating later.


Cells (interior mutability)

Cell<T> — copy-based, !Sync

let c = Cell.new(0);
c.set(42);
c.get(); // requires T: Clone
c.replace(100); // returns old value
c.take(); // returns value, leaves Default (T: Default)
c.update(|v| v + 1); // apply function in-place

RefCell<T> — runtime-borrow-checked, !Sync

let rc = RefCell.new(List.new());
{
let mut w = rc.borrow_mut(); // panics if any borrow active
w.push(1);
}
{
let r = rc.borrow(); // panics if mutable borrow active
print(f"{r.len()}");
}

// Non-panicking variants:
match rc.try_borrow_mut() {
Result.Ok(mut w) => { w.push(2); }
Result.Err(_) => log("contended"),
}

OnceCell<T> — write-once

let cfg: OnceCell<Config> = OnceCell.new();
cfg.set(load_config()).unwrap();
let value = cfg.get_or_init(|| load_config());

LazyCell<T> — lazy computation

let computed: LazyCell<HeavyResult> = LazyCell.new(|| compute_once());
let result = computed.force(); // computes on first call, caches

Protocol implementations

TypeEqOrdHashCloneDefaultDebugDisplay
Cell<T>T: Clone+EqT: Clone+Ord— (interior mutability)T: CloneT: Clone+DefaultT: Clone+DebugT: Clone+Display
RefCell<T>T: Eq— (interior mutability)T: CloneT: DefaultT: DebugT: Display
OnceCell<T>T: Clone+EqT: Clone+HashT: CloneyesT: Clone+DebugT: Clone+Display

Cell and RefCell deliberately omit Hash — interior mutability would let the contained value (and thus the hash) change between insertions and lookups in a Map<Cell<T>, V>, breaking the map invariant. Same policy as Rust's Cell<T>: !Hash / RefCell<T>: !Hash. OnceCell<T> is write-once: once set() succeeds, both Eq and Hash see the same value forever, so the Hash–Eq invariant holds and Map<OnceCell<T>, V> is sound.

Display for Cell / OnceCell delegates transparently to the inner value's Display; the wrapper is invisible to user-facing rendering. Display for RefCell does the same when no mutable borrow is active and falls back to the sentinel <borrowed> otherwise (because handing out a shared borrow for fmt concurrently with a mutable borrow would violate the dynamic borrow-check; printing the sentinel is preferable to panicking inside formatter machinery).

For thread-safe equivalents, see sync (AtomicCell, Mutex, RwLock, OnceLock).


Heap, Shared, Cow, Pin

TypeSemantics
Heap<T>unique heap allocation; CBGR-tracked
Shared<T>atomically ref-counted; Send + Sync if T: Send + Sync
Weak<T>non-owning ref to a Shared<T> (breaks cycles)
Cow<T>clone-on-write — borrowed &T until you call .to_mut()
Pin<P>structurally pinned (used for self-referential futures)
ManuallyDrop<T>wraps T to prevent automatic drop
MaybeUninit<T>wraps possibly-uninit memory; safe initialisation

Heap<T>

Heap<T> is the unique-ownership heap allocation. Each Heap carries a 16-byte (ptr, generation: UInt32, epoch: UInt16) triple; deref-time CBGR validation re-reads the allocation header's atomic generation and epoch and panics on mismatch — that is how use-after-free is detected at Tier 0 with ~15ns overhead. Tier 1 elides the check when the compiler proves the reference cannot outlive the allocation.

Construction

Heap.new(value: T) -> Heap<T> // panics on OOM
Heap.new_default() -> Heap<T> // T: Default
Heap.new_zeroed() -> Heap<T> // bit-pattern 0
Heap.try_new(value: T) -> Result<Heap<T>, AllocError> // non-panicking

Deref (CBGR-checked)

h.as_ref() -> &T
h.as_mut() -> &mut T
*h // implicit deref via Deref protocol — same CBGR check

Move / leak / round-trip

h.into_inner() -> T // free header, return value
h.into_raw() -> &unsafe T // intentional leak; pair with from_raw
unsafe Heap.from_raw(p: &unsafe T) -> Heap<T>
h.leak() -> &mut T // 'static-lifetime reference

CBGR introspection — read the underlying allocation header directly, skipping the cached (generation, epoch) triple stored on the Heap. Use these for diagnostics and conformance tests; in production code the implicit deref handles validation for you.

h.generation() -> UInt32 // cached value from construction
h.epoch() -> UInt16 // cached value from construction
h.is_valid() -> Bool // both gen + epoch agree with header
h.is_allocated() -> Bool // header.generation != 0
h.is_freed() -> Bool // header.generation != h.generation
h.header_generation() -> UInt32 // re-read header atomically (Acquire)
h.current_epoch() -> UInt16 // re-read epoch from header
h.header_epoch() -> UInt32 // alias of current_epoch (UInt32 shape)
h.capabilities() -> UInt16 // header capability bits
h.header_size() -> Int // CBGR header byte size — currently 32

All introspection methods use atomic loads with ORDERING_ACQUIRE, so they synchronise correctly across threads. header_size() returns the constant 32; if the allocator's AllocationHeader ever changes size, this constant must update in lockstep with verum_runtime::cbgr::HEADER_SIZE — the inline - 32 offset is repeated at six sites inside core/base/memory.vr and is tracked as a hoist-to-constant audit item.

Protocol implementations

ProtocolBoundBehaviour
Deref / DerefMutalways*h calls as_ref / as_mut (CBGR-checked)
Dropalwaysruns drop_in_place on *self.ptr, then cbgr_dealloc (header generation increment for CBGR invalidation)
CloneT: CloneHeap.new((**self).clone()) — independent allocation
DebugT: Debugwraps as Heap(<inner>)
DisplayT: Displaytransparent — delegates to T.fmt, wrapper invisible
EqT: Eq**self == **other
OrdT: Ord(**self).cmp(&**other)
HashT: Hash(**self).hash(hasher)
DefaultT: DefaultHeap.new_default()

Shared<T> and Weak<T>

Shared.new(value) Shared.clone(&s) s.weak() -> Weak<T>
weak.upgrade() -> Maybe<Shared<T>>
Shared.strong_count(&s) / weak_count

Weak<T> carries identity-based Eq and Hash — two Weak<T> compare equal iff they were produced from the same Shared<T> allocation (matching pointer + generation + epoch). This is the only sound equality for weak handles: comparing inner values would require upgrade-then-deref, but the upgrade can fail mid-comparison if another thread drops the last Shared, breaking transitivity. Identity equality lets Map<Weak<T>, V> work (cycle-breaking caches, weak-keyed observer registries). Debug on Weak<T> renders Weak { gen: N, epoch: M, alive } or … dropped } for post-mortem dumps without leaking raw pointers.

Cow<T>

let c: Cow<List<Int>> = Cow.Borrowed(&xs);
let owned: &mut List<Int> = c.to_mut(); // clones if Borrowed

Raw pointer helpers

ptr_read(p) ptr_write(p, value) // unsafe
drop_in_place(p) forget(value) // mem leaks
is_null(p) null_ptr<T>()
ptr_offset(p, n)

Protocol implementations — Display is transparent, Debug is wrapped

Smart-pointer types in core.base.memory follow a deliberate asymmetry between Display and Debug:

TypeDisplay<T>Debug<T>
Heap<T: Display>(**self).fmt(f) — invisible wrapperHeap(<inner>)
Shared<T: Display>(**self).fmt(f) — invisible wrapperShared(<inner>)
Cow<T: Clone + Display>self.as_ref().fmt(f) — invisibleBorrowed(<inner>) / Owned(<inner>)

Rationale:

  • Display is for user-facing renderingprint(x), f"…{x}…", network-protocol error bodies, log lines. Box-style pointers are conceptually invisible at this layer: print(Heap.new(42)) should produce 42, not Heap(42).

  • Debug is for structured-log payloadcore.base.log.{trace,debug,info,warn,error}, f"…{x:?}…", gdb-style dumps, snapshot serialisers. Here the wrapper IS information: knowing Heap("hello") vs the raw "hello" distinguishes "owned-on-heap" from a stack value during incident analysis.

This split mirrors Rust's Display for Box<T> / Debug for Box<T> convention and aligns with the broader Display + Debug + Eq triple contract above — every public stdlib pointer type now provides Display + Debug + Eq + Hash + Clone + Default + Ord (gated by the inner type's bounds).

For full memory primitives see mem.


panic and assertions

Panicking

panic("invariant violated") -> !
panic_at("oops", "src/foo.vr", 12, 4) -> !
abort() -> ! // immediate; no unwinding
exit(code) -> !

Assertions

Core assertions — always on, panic on failure:

assert(cond, "message")
assert_eq(left, right, "message") // T: Eq + Debug
assert_ne(left, right, "message")
assert_some(maybe, "expected Some")
assert_none(maybe, "expected None")
assert_ok(result, "expected Ok")
assert_err(result, "expected Err")

Extended assertions (added for reference-quality testing — see Tooling → Testing):

// Float comparison with tolerance — use this INSTEAD of assert_eq
// on any Float-typed value; direct IEEE-754 equality is almost never
// what you want after arithmetic.
assert_approx_eq(left: Float, right: Float, tolerance: Float = 1e-9, msg: Text)

// Inclusive-range check: fails if v < lo or v > hi.
assert_between<T: Ord>(v: T, lo: T, hi: T, msg: Text)

// Sorted-ascending check over &List<T>. O(n).
assert_is_sorted<T: Ord>(list: &List<T>, msg: Text)

// Membership check. O(n) linear scan.
assert_contains<T: Eq>(list: &List<T>, needle: &T, msg: Text)

// Expects the closure to panic. Succeeds iff it does; fails the
// assertion if the closure returns normally. Implemented via
// catch_unwind.
assert_panics<T>(f: fn() -> T, msg: Text)

Debug-only variants — stripped in release builds:

debug_assert(cond, "msg")
debug_assert_eq(a, b, "msg")
debug_assert_ne(a, b, "msg")

Markers

unreachable("dead branch") -> !
unreachable_unchecked("dead in release; UB hint") -> !
unimplemented("phase 2") -> !
todo("write me") -> !

Catch panics

catch_unwind(|| risky()) -> Result<T, PanicInfo>
resume_unwind(panic_info) -> !

Compile-time helpers

@file() @line() @column()
@function() @module()
@current_location()

PanicInfo carries message: Text, optional Location { file, line, column }. set_panic_handler(hook) installs a global hook (fn(&PanicInfo)).

dbg — print-and-pass-through

let total = dbg(items.iter().filter(|x| x.is_active()).count());
// stderr: [src/foo.vr:42] items.iter().filter(...).count() = 17

env — process environment

CLI arguments

args() -> List<Text> // all argv
arg(i) -> Maybe<Text>
args_count() -> Int
args_os() -> Args // iterator

Environment variables

var(key) -> Result<Text, VarError>
var_opt(key) -> Maybe<Text>
set_var(key, value)
remove_var(key)
vars() -> Vars // iterator over (Text, Text)
vars_list() -> List<(Text, Text)>

VarError is NotPresent | NotUnicode(List<Byte>).

Standard locations

home_dir() -> Maybe<Text> // HOME or USERPROFILE
user() -> Maybe<Text> // USER or USERNAME
path() -> Maybe<Text> // PATH
shell() -> Maybe<Text> // SHELL or COMSPEC
locale() -> Maybe<Text> // LANG / LC_*
temp_dir() -> Text // TMPDIR/TMP/TEMP or /tmp

Platform info

os_name() -> Text // "macos", "linux", "windows"
arch() -> Text // "aarch64", "x86_64", ...
os_family() -> Text // "unix" or "windows"

Exit

exit(code) -> !
exit_success() -> ! // 0
exit_failure() -> ! // 1

Path utilities

split_paths(path_str) -> List<Text> // splits PATH-style string

Data — dynamic typed value

When you genuinely don't know the schema (e.g., reading arbitrary JSON configuration), Data is the JSON-like dynamic value:

type Data is
| Null
| Bool(Bool)
| Int(Int)
| Float(Float)
| Text(Text)
| Array(List<Data>)
| Object(Map<Text, Data>);

Construction & parsing

Data.null() Data.from_int(42) Data.from_text("hi")
Data.empty_object() Data.empty_array()
parse_json(input) -> Result<Data, DataError>

Type predicates and accessors

d.is_null() d.is_bool() d.is_int() d.is_float() d.is_text()
d.is_array() d.is_object() d.is_number()
d.as_bool() d.as_int() d.as_float() d.as_text()
d.as_array() d.as_object()
d.as_array_mut() d.as_object_mut()
d.type_name() -> Text

Object / array operations

d.get(key) d.get_mut(key) d.contains_key(key)
d.set(key, value) -> Result<(), DataError>
d.remove(key) -> Maybe<Data>
d.at(index) d.at_mut(index)
d.push(value) -> Result<(), DataError>
d.pop() -> Maybe<Data>
d.len() d.is_empty()
d.keys() d.values()

Path access, merging, output

d.path("user.address.city") -> Maybe<&Data>
d.merge(&other) d.deep_merge(&other)
d.to_json() d.to_json_pretty()
d.to_string() d.to_number()

DataError

type DataError is
| TypeMismatch
| KeyNotFound(Text)
| IndexOutOfBounds(Int)
| ParseError(Text)
| InvalidCast;

For typed schemas, prefer dedicated record types with @derive(Serialize, Deserialize) — see serde.vr below.


Serialisation — Serialize / Deserialize

type Serialize is protocol {
fn serialize<S: Serializer>(&self, s: &mut S) -> Result<S.Ok, S.Error>;
}
type Deserialize is protocol {
fn deserialize<D: Deserializer>(d: &mut D) -> Result<Self, D.Error>;
}

The format is supplied by an implementation of the dual Serializer / Deserializer protocols (one per format: JSON, TOML, YAML, …). Most user types just @derive(Serialize, Deserialize) and let an external cog (e.g. toml, serde_json-equivalent) drive the format.

Helper builders:

ListSerializer.serialize_element(&value)
MapSerializer.serialize_key(&k); MapSerializer.serialize_value(&v)
RecordSerializer.serialize_field(name, &value)

SerdeError is the common error: constructors include unexpected_type(expected, found), missing_field(name), unknown_field(name).


error — backtraces and chains

type StackFrame is { function: Text, file: Text, line: Int, column: Int };
type Backtrace is { frames: List<StackFrame> };

Backtrace.capture() -> Backtrace // current stack (best-effort)
Backtrace.from_frames(frames) -> Backtrace
bt.frames() / bt.is_empty() / bt.len()

ErrorProtocol

type ErrorProtocol is protocol extends ErrorSource {
fn message(&self) -> Text;
fn backtrace(&self) -> Maybe<&Backtrace>;
}

Chain rendering

format_error_chain(&error) -> Text // walks .source() and prints all
match result {
Result.Err(e) => eprint(format_error_chain(&e)),
Result.Ok(_) => (),
}

log — structured logging protocol

type LogLevel is Trace | Debug | Info | Warn | Error;

type Logger is protocol {
fn log(&self, level: LogLevel, message: &Text);
fn is_enabled(&self, level: LogLevel) -> Bool;
}

type LogRecord is {
level: LogLevel,
message: Text,
fields: List<(Text, Text)>,
module_path: Maybe<Text>,
file: Maybe<Text>,
line: Maybe<Int>,
};

type LogRecordBuilder is { /* opaque */ };

Level constructors (free functions)

For mount import sites that prefer free-function style over LogLevel.Trace:

mount core.base.log.{
LogLevel, LogRecord, LogRecordBuilder,
level_trace, level_debug, level_info, level_warn, level_error,
};

let l: LogLevel = level_warn();

LogLevel itself implements Eq, Ord, Clone, Copy, Hash, Display, Debug, Default (defaults to Info); severity()0..4 and name()"TRACE".."ERROR" are the workhorse accessors.

LogRecord construction

LogRecord.new(level, message, fields) // 3-arg canonical
LogRecord.simple(level, message) // shortcut, fields = []

// Chainable builder methods (each returns a new record):
rec.with_field(key, value)
rec.with_module_path(path)
rec.with_file(file)
rec.with_line(line)

LogRecordBuilder — imperative builder

For sites where a record is assembled across control-flow paths (e.g. attaching fields conditionally before finalising):

let rec = LogRecordBuilder.new()
.level(level_warn())
.message("disk full".to_text())
.field("disk".to_text(), "/var".to_text())
.field("free_gb".to_text(), "0".to_text())
.module_path("daemon::disk".to_text())
.file("disk.vr".to_text())
.line(142)
.build();

Defaults: Info / empty message / no fields / no source location.

Convenience functions (require Logger in context)

fn handle(req: Request) using [Logger] {
info(&"received request");
debug(&f"path = {req.path}");
if !req.is_authenticated() {
warn(&f"unauthorised access from {req.remote_addr}");
}
error(&f"unexpected: {err}");
}

Backends

NullLogger (no-op, useful in tests). Real backends are in user code or third-party cogs (file logger, journald, syslog, …). To wire a backend, implement Logger for MyBackend { … } and provide it via provide MyBackend.new() as Logger { … } — the same context-system plumbing covered in stdlib/context.


coinductive — productivity & bisimulation analysis

For corecursive function bodies. Most users will not import this directly; it backs the cofix modifier's productivity check.

type CorecursiveCall is { callee: Text, guard_depth: Int };
type ProductivityResult is Productive | NonProductive { unguarded: List<Text> };

corec_call(callee, depth) check_productivity(calls)
is_guarded(call)
observation(label, payload) trace(steps)
trace_prefix(t, n)
observations_equal(a, b)
bisimilar_up_to(left, right, depth) // BisimulationResult

Primitive methods (primitives.vr)

Inherent methods on the built-in numeric / character types. Selected highlights — see source for full list.

Int (64-bit signed)

constants: Int.MIN Int.MAX Int.BITS
predicates: is_positive, is_negative, is_zero, is_power_of_two
arithmetic: abs, signum, pow(n), min, max, clamp
checked: checked_add, checked_sub, checked_mul, checked_div, ...
wrapping: wrapping_add, wrapping_sub, wrapping_mul, ...
saturating: saturating_add, saturating_sub, saturating_mul
overflowing: overflowing_add (-> (T, Bool)), ...
bits: leading_zeros, trailing_zeros, count_ones, count_zeros,
swap_bytes, reverse_bits, rotate_left, rotate_right
bytes: to_le_bytes, to_be_bytes, from_le_bytes, from_be_bytes
conversion: to_float, to_binary, to_hex, to_octal, to_text, parse_int
euclidean: div_euclid, rem_euclid
range: in_range, ilog2, ilog10, abs_diff

Float (64-bit)

constants: Float.MIN Float.MAX Float.MIN_POSITIVE Float.NAN
Float.INFINITY Float.NEG_INFINITY
classify: is_nan, is_infinite, is_finite, is_normal,
is_sign_positive, is_sign_negative
arithmetic: abs, signum, trunc, fract, round, ceil, floor,
sqrt, cbrt, pow(n), exp, log, log10, log2
trig: sin, cos, tan, asin, acos, atan, atan2
hyper: sinh, cosh, tanh, asinh, acosh, atanh
ops: min, max, clamp, copysign, fma, hypot
conversion: to_int, to_bits, from_bits, to_string, parse_float

Bool

.count() // count of `true` in a slice (extension idiom)
.to_int() // 0 or 1
.to_text() // "true" / "false"
parse_bool(text)

Char

classify: is_alphabetic, is_numeric, is_whitespace, is_control,
is_uppercase, is_lowercase
case: to_uppercase, to_lowercase
encoding: encode_utf8, escape_debug
constants:Char.MIN Char.MAX Char.UNICODE_LIMIT

Byte

is_ascii, is_ascii_digit, is_ascii_alphabetic, is_ascii_whitespace
to_int, to_char, to_text
Byte.from_int(n)

IDs and versioning

uuid — RFC 4122 / 9562

let v4 = Uuid.new_v4(); // 122 bits random
let v7 = Uuid.new_v7(); // 48-bit unix-ms + 74 random bits
let text: Text = v7.to_text();
let back = Uuid.parse(&text)?;

v7 is time-ordered — lexicographic sort matches chronological sort, ideal for DB primary keys (no B-tree fragmentation). The 48-bit timestamp prefix comes from core.time.system_time.SystemTime.now().timestamp_millis() (wall clock, clock_gettime(CLOCK_REALTIME) on Unix); the remaining 74 random bits come from the platform CSPRNG via core.sys.common.random_bytes.

snowflake — Twitter 64-bit IDs

let mut gen = Snowflake.new(DEFAULT_EPOCH_MS, worker_id)?;
let id: UInt64 = gen.next_id()?;

// Decompose.
let parts = snowflake.parse(id, DEFAULT_EPOCH_MS);
// { timestamp_ms, worker_id, sequence }

Bit layout: [ 0 | 41-bit unix-ms | 10-bit worker | 12-bit seq ]. Monotonically increasing within a worker; the generator surfaces two distinct clock-regression errors so non-monotone wall clocks never silently produce non-monotone IDs:

  • ClockRegressed(delta_ms) — wall clock went backwards relative to this generator's last emitted ID.
  • ClockBeforeEpoch(delta_ms) — wall clock is earlier than the configured epoch (e.g. embedded systems with an unset RTC reading 1970 against the 2010 Twitter epoch, or tests using a future epoch). Pre-fix, the underlying subtraction underflowed UInt64 silently and the resulting bit-shifted value produced corrupt non-sortable IDs with no error surfaced.

The wall-clock source is core.time.system_time.SystemTime.now() .timestamp_millis()clock_gettime(CLOCK_REALTIME) on Linux/macOS, GetSystemTimePreciseAsFileTime on Windows.

Saturates at 4 M IDs/sec per worker (12-bit sequence wraps each ms).

Pick UUID v4/v7 for cross-system interop, Snowflake for compact DB primary keys with explicit worker sharding.

nanoid — URL-safe short IDs

let id = nanoid.generate(); // 21 chars ≈ 126 bits
let short = nanoid.generate_len(10);
let hex = nanoid.generate_with_alphabet(b"0123456789abcdef", 16);

Byte-exact compatible with the nanoid JS/Go/Rust/Python libraries. Rejection sampling over the smallest power-of-two mask covering the alphabet eliminates modulo-bias. Birthday collision ≈ 1 per 2.4 × 10¹⁸ IDs at default length.

semver — Semantic Versioning 2.0.0

let v = semver.parse(&Text.from("1.0.0-beta.1+build.5"))?;
// v.major = 1, v.pre_release = ["beta", "1"], v.build_meta = ["build", "5"]

let a = semver.parse(&Text.from("1.0.0-alpha"))?;
let b = semver.parse(&Text.from("1.0.0"))?;
assert(semver.cmp(&a, &b) < 0); // release > prerelease (§11.3)

Strict §9 parser — leading zeros in numeric identifiers rejected. Full §11 total ordering: major/minor/patch → prerelease-vs-release → numeric < alphanumeric → fewer identifiers < more at common prefix equal. Build metadata ignored in precedence (§10).

glob — shell-style pattern matching

glob.matches("src/**/*.rs", "src/foo/bar.rs") // true
glob.matches("*.rs", "src/lib.rs") // false — * doesn't cross /

let pat = glob.compile("target/**")?;
pat.matches_path("target/debug/verum") // true
FormMatches
*sequence of non-separator chars
**any number of path segments
?single non-separator char
[abc] / [a-z] / [!abc]class / range / negated
\cliteral c

** follows fnmatch(FNM_PATHNAME \| FNM_LEADING_DIR) — the Bazel / Cargo / Jest / .gitignore convention.


See also

  • collectionsList, Map, Set, Deque, BinaryHeap, BTreeMap, BTreeSet.
  • textText (UTF-8 string), Char, formatter, regex, tagged literals.
  • mem — CBGR allocator and the implementation under Heap / Shared.
  • sync — thread-safe equivalents of Cell, atomics, Mutex, RwLock.
  • Language → patterns — pattern syntax used with Maybe / Result.
  • Language → error handlingResult/Maybe/?/throws/try/recover.