core.math — Mathematics
The largest module in the stdlib — a 10-layer mathematical stack plus a substantial pure-mathematics branch. libm-free: every function is implemented in Verum on top of CPU intrinsics.
This page is an index of every layer and sub-module. Deep APIs (hundreds of functions per layer) are listed here in summary form; follow the source links for complete signatures.
Layer overview
Layer 9 Agents & LLM agent/ (tokenizer, KV cache, ReAct, RAG)
Layer 8 State-space models + distributed ssm/ distributed/
Layer 7 Neural networks nn/
Layer 6 Automatic differentiation autodiff/
Layer 5 GPU / accelerator gpu/
Layer 4 Tensor system tensor/
Layer 3 Numerical analysis & random calculus/ random/
Layer 2 Linear algebra (BLAS-style) linalg/
Layer 1 Scalar math constants/ elementary/ hyperbolic/ special/
Layer 0 Foundation ieee754/ integers/ bits/ checked/ libm/
Pure mathematics (parallel branch): algebra/, category/,
topology/, analysis/, logic/, hott/, cubical/,
simplicial/, infinity_category/, infinity_topos/,
kan_extension/, fibration/, model_category/, operad/,
number_theory/.
∞-topos foundations: quantum_logic/, giry/, epistemic/,
cohesive/, day_convolution/, sdg/.
Others: complex/, category_finite/, bitvec/,
observational/, examples/, internal/, simple/, advanced/,
tactics/.
Layer 0 — Foundation
math.ieee754
type FpCategory is NaN | Infinite | Zero | Subnormal | Normal;
f64_decompose(f: Float64) -> (sign: Bool, exp: Int, mantissa: UInt64)
f32_decompose(f: Float32) -> (Bool, Int, UInt32)
f64_compose(sign, exp, mantissa) -> Float64
f32_compose(sign, exp, mantissa) -> Float32
classify(f: Float64) -> FpCategory classify_f32(f: Float32) -> FpCategory
is_nan / is_infinite / is_finite / is_normal / is_subnormal
copysign(x, y) signbit(x) -> Bool
math.integers
type DivMode is Truncate | Floor | Ceiling | Euclidean;
div_floor(a, b) div_ceiling(a, b)
div_euclidean(a, b) mod_euclidean(a, b) mod_floor(a, b)
div(a, b, mode: DivMode) divmod(a, b) -> (q, r)
gcd(a, b) -> Int gcd_binary(a, b) -> Int lcm(a, b) -> Int
extended_gcd(a, b) -> (gcd, x, y) // ax + by = gcd
mod_inverse(a, m) -> Maybe<Int>
mod_pow(base, exp, m) -> Int
math.bits
clz(x) / clz32(x) ctz(x) / ctz32(x)
popcnt(x) / popcnt32(x)
ffs(x) / ffs32(x) fls(x) / fls32(x)
highest_bit(x) / lowest_bit(x)
rotl(x, n) / rotr(x, n) rotl32 / rotr32
bswap(x) / bswap32 / bswap16
bitreverse(x)
math.checked
Overflow-safe arithmetic wrappers (thin layer over intrinsics, but using refinement types to document invariants).
math.libm
Pure-Verum libm. sin, cos, exp, log, pow, etc. — all
implemented on top of the bit-level primitives above. No C library
dependency. See the callout at the top of Layer 1 — the same-named
functions one layer up are currently affected by a stdlib
name-resolution defect; this module is entangled in the same
collision (it declares some of the same bare names) and has not been
independently verified.
Layer 1 — Scalar math
A stdlib build-time bug currently causes sin, cos, exp, log,
and sqrt in core.math.elementary to resolve to a same-named
function declared in a different core/math/*.vr file instead of
their own implementation — several submodules in this stack declare
functions with the same bare names (e.g. a Tensor-typed exp
elsewhere in core.math). Effects vary: some calls crash with a
runtime type error, at least one (sin) has been observed silently
returning a value of the wrong type entirely rather than failing
loudly. This is a name-resolution defect in the compiler's stdlib
build, not a numerical one, and it is not fixed yet.
It propagates. Anything that calls one of those five names internally inherits the failure — often only for part of its input range, where an implementation switches to a Taylor-series fast path for small inputs that happens to avoid the broken call, while its general-case path does not.
- Always broken:
sin,cos,exp,log,sqrt,exp2,log2,log10,acoth. - Broken for typical (not all) inputs — the general-case path
calls one of the five above; a small-input fast path does not:
pow(non-integer exponents),hypot,log1p,expm1,asin,acos, and effectively all ofmath.hyperbolic's general case (sinh,cosh,tanh,sech,csch,coth,asinh,acosh,atanh,asech,acsch,gudermannian,inverse_gudermannian) and most ofmath.special(gamma,lgamma,digamma,beta,lbeta,erf,erfc,erfinv). - Confirmed unaffected:
tanandsincos— both were numerically wrong until 2026-07-28 (see the changelog) and are now fixed and unaffected by the defect above — plusatan,atan2,cbrt,powi, the rounding functions (floor/ceil/round/rint/trunc/fract),min/max/clamp/abs/signum,fma, and the interpolation helpers (lerp,inverse_lerp,remap,smoothstep,smootherstep).
Don't trust a result from the "typical inputs" group without checking it independently until this is fixed.
math.constants
const PI: Float const E: Float const TAU: Float
const PHI: Float const SQRT2: Float
const EPSILON: Float const INFINITY: Float const NAN: Float
// Refinement-based semantic aliases
type NonNegative is Float { self >= 0.0 };
type Positive is Float { self > 0.0 };
type UnitInterval is Float { 0.0 <= self && self <= 1.0 };
type Probability is UnitInterval;
type Angle is Float; // radians
math.elementary
// Trigonometry
sin(x) / cos(x) / tan(x) asin(x) / acos(x) / atan(x) / atan2(y, x)
sincos(x) -> (Float, Float)
// Exponentials & logs
exp(x) / exp2(x) / expm1(x) log(x) / log2(x) / log10(x) / log1p(x)
// Powers & roots
pow(x, y) / powi(x, n: Int) sqrt(x) / cbrt(x) / hypot(x, y)
// Rounding
floor / ceil / round / rint / trunc / fract
// Min/max/clamp
min(a, b) / max(a, b) / clamp(x, lo, hi)
abs(x) / signum(x)
// Fused operations
fma(a, b, c) // (a*b + c) with single rounding
lerp(a, b, t) // linear interpolation
inverse_lerp(a, b, x) -> Float // where x sits in [a, b]
remap(x, lo1, hi1, lo2, hi2) -> Float // remap x from [lo1, hi1] to [lo2, hi2]
smoothstep(edge0, edge1, x) / smootherstep(edge0, edge1, x)
// Safe variants — return Maybe<T>
sqrt_safe(x) / log_safe(x) / asin_safe(x) / acos_safe(x)
math.hyperbolic
sinh / cosh / tanh asinh / acosh / atanh
Most of this module's general-case paths are currently broken — see the callout at the top of Layer 1.
math.special
gamma(x) / lgamma(x) / digamma(x)
beta(x, y) / lbeta(x, y)
erf(x) / erfc(x) / erfinv(x)
Every function here calls into log/exp/sqrt/sin/cos — see
the callout at the top of Layer 1; treat this module as unverified
until that lands.
Layer 2 — Linear algebra
math.linalg
BLAS-style API. Types: Vector<T>, Matrix<T>, StaticVector<T, const N>,
StaticMatrix<T, const R, const C>, and the Numeric protocol.
// Level 1 (vector ops)
dot(a, b) -> T nrm2(a) -> T asum(a) -> T
iamax(a) -> Int // index of max |element|
scal(alpha, a) axpy(alpha, x, y) // y := αx + y
copy(src, dst) swap(a, b)
rotg(a, b) -> (c, s) rot(x, y, c, s)
// Level 2 (matrix-vector)
gemv(alpha, A, x, beta, y) // y := α A x + β y
trsv(upper, A, x) // triangular solve
ger(alpha, x, y, A) // A := α x yᵀ + A
syr(alpha, x, A) // symmetric rank-1
// Level 3 (matrix-matrix)
gemm(alpha, A, B, beta, C) // C := α A B + β C
trsm(upper, alpha, A, B) // triangular solve
syrk(alpha, A, beta, C) // symmetric rank-k
// Decompositions
lu(A) -> LUDecomposition<T>
qr(A) -> QRDecomposition<T>
cholesky(A) -> CholeskyDecomposition<T>
svd(A) -> SvdDecomposition<T>
// Solvers
determinant(A) -> T
inverse(A) -> Maybe<Matrix<T>>
solve(A, b) -> Maybe<Vector<T>> // Ax = b
Layer 3 — Numerical analysis & random
math.calculus
// Differentiation
forward_diff(f, x, h) -> Float
backward_diff(f, x, h) -> Float
central_diff(f, x, h) -> Float
// Integration
trapezoid(f, a, b, n) -> Float
simpson(f, a, b, n) -> Float
romberg(f, a, b, tol) -> Float
gauss_legendre(f, a, b, n) -> Float
// ODE solvers
euler(f, t0, y0, h, n) -> List<Float>
heun(f, t0, y0, h, n) -> List<Float>
midpoint(f, t0, y0, h, n) -> List<Float>
rk4(f, t0, y0, h, n) -> List<Float>
rk45(f, t0, y0, h_init, tol) -> List<(Float, Float)> // adaptive
// Root finding
bisection(f, a, b, tol) -> Maybe<Float>
newton(f, df, x0, tol, max_iter) -> Maybe<Float>
secant(f, x0, x1, tol, max_iter) -> Maybe<Float>
brent(f, a, b, tol) -> Maybe<Float>
// Optimisation
gradient_descent(f, grad, x0, lr, max_iter) -> Vector<Float>
newton_optimize(f, grad, hess, x0, tol) -> Vector<Float>
bfgs(f, grad, x0, tol, max_iter) -> Vector<Float>
math.random
type RandomKey is UInt64;
type Rng is protocol {
fn next_u64(&mut self) -> UInt64;
fn split(&self) -> (RandomKey, RandomKey);
};
type XorShift128 is { ... }; type PCG is { ... };
XorShift128.new(seed: UInt64) -> XorShift128
PCG.new(seed: UInt64, stream: UInt64) -> PCG // two words: seed and stream
rng.uniform_01() -> Float // [0.0, 1.0)
rng.uniform(lo, hi) -> Int / Float
rng.normal_01() -> Float
rng.normal(mean, std) -> Float
rng.truncated_normal(lo, hi, mean, std) -> Float
rng.exponential(lambda) -> Float
rng.bernoulli(p) -> Bool rng.poisson(lambda) -> Int
rng.gamma(shape, scale) -> Float rng.beta(alpha, beta) -> Float
rng.chi_squared(k) -> Float rng.student_t(df) -> Float
rng.categorical(probs) -> Int
rng.permutation(n) -> List<Int>
rng.shuffle_vec(&mut xs) rng.choice(&xs) -> &T
Layer 4 — Tensor system
Defines Tensor<T, const S: Shape> (statically shaped) and DynTensor<T>
(dynamic), plus all the usual operations.
Tensor operations run under the interpreter. The AOT tier lowers some of them and announces the rest: of the 107 tensor runtime helpers the compiler references, 71 are panic stubs that name themselves when reached. Measured 2026-09-02:
verum run shape ok
verum run --tier aot PANIC: verum_tensor_arange_i: no Tier-1 lowering
yet (T0193/T0179)
This is deliberate. A helper declared without a body would either break the link or silently return zero; a stub that panics with its own name fails where you can see it, and names the epic that is landing the real lowerings per operation.
What is not yet measured is WHICH operations survive Tier 1 — every
tensor spec in the conformance suite runs at tier 0, so the boundary is
known to exist and not known in detail. If you are targeting AOT, run
your kernel under --tier aot before depending on it.
// Construction
zeros<Float, shape[3, 4]>() -> Tensor<Float, shape[3, 4]>
ones<Float, shape[3, 4]>()
full<Float, shape[2, 2]>(value: 3.14)
eye<Float, 5>() // identity
arange(start, stop, step) -> DynTensor<Float>
linspace(start, stop, n) -> Tensor<Float, shape[n]>
rand<Float, shape[3, 4]>() // uniform [0, 1)
randn<Float, shape[3, 4]>() // standard normal
// Shape — these ARE methods on the tensor
t.shape() t.rank() t.ndim() t.dim(i) t.numel()
t.reshape(...) t.squeeze() t.unsqueeze(axis) t.permute(axes)
t.slice(...) t.get(...) t.set(...) t.item() t.cast(...) t.to(device)
t.contiguous() t.is_contiguous() t.clone() t.device()
// Everything else is a FREE FUNCTION taking the tensor by reference
transpose(&t) flatten(&t) cumsum(&t, axis)
matmul(&a, &b) mm(&a, &b) bmm(&a, &b)
sum(&t) mean(&t) prod(&t) argmax(&t) argmin(&t) // whole tensor
sum_axis(&t, axis) mean_axis(&t, axis) max_axis(&t, axis)
min_axis(&t, axis) argmax_axis(&t, axis) all_axis / any_axis
softmax(&t) softmax_axis(&t, axis) log_softmax(&t, axis)
// Comparison — free, and they return a Bool tensor
eq(&a, &b) ne(&a, &b) lt(&a, &b) le(&a, &b) gt(&a, &b) ge(&a, &b)
// Selection
where_tensor(&mask, &a, &b) where_scalar(&mask, a, b)
masked_select(&t, &mask) masked_sum / masked_mean / masked_min / masked_max
// Composition
cat(&tensors, axis) / stack(&tensors, axis)
split(t, sizes, axis) / chunk(t, n, axis)
hstack / vstack / dstack
The tensor API is free functions over &DynTensor<T>, not methods.
t.matmul(other) does not compile; matmul(&t, &other) does. Only the
shape and storage operations in the first block are methods.
Normalisation is likewise not a tensor method: layer_norm(shape) and
rms_norm(dim) build a module (LayerNorm, RMSNorm) that you then
apply. There is no batch_norm, no masked_fill, no logical_and, and
a tensor does not report its own dtype.
Layer 5 — GPU
type GPUBackend, DeviceId, DeviceInfo, ComputeCapability;
type DeviceSelector, DeviceRegistry;
type MemorySpace, DevicePtr<T>, GPUBuffer<T>, PinnedBuffer<T>;
type Stream, Event, LaunchConfig, CudaGraph;
GPUBackend.default() -> GPUBackend
device.allocate<T>(count) -> GPUBuffer<T>
device.launch(config, kernel, args)
device.sync()
See simd.gpu and
intrinsics → gpu for device-side
intrinsics.
Layer 6 — Automatic differentiation
type DiffMode is ReverseMode | ForwardMode | MixedMode { threshold: Float };
DiffMode.auto(input_dim, output_dim) -> DiffMode
// Picks ForwardMode when output_dim / input_dim > 1, else ReverseMode.
type Differentiable is protocol {
type Tangent; type Cotangent;
fn zero_tangent() -> Self.Tangent;
fn add_tangent(a: Self.Tangent, b: Self.Tangent) -> Self.Tangent;
fn scale_tangent(t: Self.Tangent, s: Float) -> Self.Tangent;
}
// Gradients
grad(f) -> fn(input) -> Cotangent
value_and_grad(f, x) -> (output, gradient)
grad_argnums(f, argnums) -> fn(*args) -> Tuple<Cotangent>
// Vector-Jacobian products
vjp(f, x) -> (output, vjp_fn: fn(cotangent) -> Cotangent)
jvp(f, x, tangent) -> (output, tangent_out)
// Higher-order
jacobian(f) -> fn(x) -> Tensor
hessian(f) -> fn(x) -> Tensor
hvp(f, x, v) -> Tensor // Hessian-vector product
// Control
stop_gradient(x) -> T
custom_vjp(primal, vjp_fn)
GradientScope { fn enter() / exit() }
with_no_grad(|| pure_inference())
// Memory
checkpoint(f, x) -> y // trade recompute for memory
recompute(values)
core/math/autodiff.vr declares four Differentiable
implementations — for Float, DynTensor<T: RealField>,
Vector<Float> and Matrix<Float>. There are none for Float32 or
Float64.
Two caveats, both measured on the current toolchain rather than read off the source:
-
A
<T: Differentiable>bound is satisfied byFloatas of 2026-09-03 (it was not when this page was first written). Measured with the control that makes the result mean something:probe result needs_diff(1.0)wheref: Floataccepted needs_diff(p)wherepimplements nothingerror<E405>: type \Plain` does not implement `Differentiable``The negative case is the point: a clean result on
Floatalone would equally mean "the bound is not checked at all".Float32andFloat64are still refused —core/math/autodiff.vrdeclaresimplement Differentiable for Floatand nothing for the sized spellings, so this is a missing implementation rather than a carrier defect. The underlying cause the page used to describe (a protocol impl is carried by its target type's descriptor, and built-in scalars have none) was repaired under T1068. -
@derive(Differentiable)on a user record does not generate an implementation. The compiler says so rather than pretending:warning<W0507>: `@derive(Differentiable)` on `Params` was not applied— no generator for this protocol yetWrite the implementation by hand until a generator lands.
Layer 7 — Neural networks
type Module is protocol { ... };
type Trainable is protocol { ... };
type Parameter<T> is { value: T, grad: Maybe<T> };
// Layers
Linear.new(in_dim, out_dim) -> Linear
Embedding.new(vocab, dim) -> Embedding
Conv2d.new(in_ch, out_ch, kernel_size, stride, padding)
LayerNorm.new(shape) RMSNorm.new(shape) BatchNorm.new(features)
// Activations
relu / gelu / silu / sigmoid / softmax / softplus / tanh
// Dropout
Dropout.new(p)
// Attention
MultiHeadAttention.new(embed_dim, num_heads, dropout)
FeedForward.new(embed_dim, hidden_dim, dropout)
TransformerBlock.new(embed_dim, num_heads, hidden_dim, dropout)
RoPE.new(dim, max_positions)
// Optimisers
type Optimizer is protocol { fn step(&mut self, grads: &Params); }
SGD.new(params, lr, momentum, weight_decay)
AdamW.new(params, lr, betas, weight_decay)
// Schedulers — `LRScheduler` is a protocol (`get_lr(step) -> Float`),
// so you construct a concrete one, not a factory method on the protocol.
CosineScheduler.new(initial_lr, min_lr, warmup_steps, total_steps)
LinearWarmup { target_lr, warmup_steps }
// Loss
mse_loss(pred, target) / cross_entropy(pred, target) / bce_loss(pred, target)
// Utility
clip_grad_norm(params, max_norm)
Layer 8 — SSM & distributed
math.ssm — state-space models
S4.new(dim, state_dim, kernel) / Mamba.new(dim, state_dim, conv_dim)
BiMambaBlock.new(dim, state_dim) Jamba.new(...) // hybrid SSM + attention
MoELayer.new(num_experts, dim, routing: RoutingStrategy)
RoutingStrategy is TopK(k) | Hash(buckets) | Learned;
BalanceLoss.new(num_experts)
math.distributed
DataParallel.new(module, devices)
DistributedDataParallel.new(module, process_group)
FSDP.new(module, sharding_strategy) // fully-sharded data parallel
ActorMesh.new(layout) Supervision(...)
RDMA.connect(peer) // remote direct memory access
Layer 9 — Agents, RAG, guardrails
math.agent
type Tokenizer is protocol { fn encode(text) -> List<Int>; fn decode(ids) -> Text; }
type KVCache is { ... }; PagedKVCache.new(num_pages, page_size)
type SpeculativeDecoder is { ... };
type ContinuousBatcher is { ... };
LLMAgent.new(model, tokenizer)
ReActAgent.new(llm, tool_registry, max_iterations)
MemoryStore.new(vector_store)
flash_attention(q, k, v, scale) / paged_attention(...)
sample_top_p(logits, p) / sample_temperature(logits, t) / sample_greedy(logits)
type ChatMessage is { role: Text, content: Text };
type FunctionSchema is { name: Text, parameters: Data };
type ExecutableTool is protocol { fn call(args) -> Data; }
QuantizedLinear.new(in_dim, out_dim, bits: Int) // INT4/INT8
math.guardrails
ContentClassifier.new(categories, threshold)
Guardrail.new(&classifiers)
PIIFilter.new(patterns)
TopicGuardrail.new(allowed_topics)
GuardrailChain.new(&rails)
GuardedAgent.new(agent, chain)
math.rag
Document { id, content, embedding, metadata }
VectorStore is protocol { ... };
HNSWIndex.new(dim, m, ef_construction)
TextChunker.new(chunk_size, overlap)
BM25Index.new()
HybridRetriever.new(vector_store, bm25, weight)
RAGPipeline.new(retriever, llm, prompt_template)
Pure mathematics
Self-contained formalisations, used by the verification system
and by theory_interop. Depth varies per branch; most define
the usual algebraic structures and their universal
constructions.
algebra/— groups, rings, fields, lattices, modules.category/— categories, functors, natural transformations, adjunctions, monads, limits, colimits.topology/— point-set topology, manifolds, homology.analysis/— real, functional, measure theory.logic/— propositions-as-types, proof terms, decidability.hott/— cubical HoTT:I,Path,refl,transport,hcomp,Equiv,IsContr,IsProp,ua,funext,S1,Susp,Trunc,Quotient.cubical/— interval operations,Face,comp,Glue.simplicial/—SimplicialSet,KanComplex,InfinityGroupoid.infinity_category/—QuasiCategory,InfinityFunctor,MappingSpace.infinity_topos/—Sieve,GrothendieckTopology,InfPresheaf,InfSheaf,InfinityTopos,GeometricMorphism,DescentObstruction.kan_extension/—InfLeftKanExtension,InfRightKanExtension,PointwiseKanExtension.fibration/—GrothendieckFibration,CartesianMorphism.model_category/—QuillenModelStructure,WeakEquivalence.operad/— operads,E_noperads, ∞-operads.number_theory/— Peano naturals, primes, modular arithmetic.
∞-Topos foundations
quantum_logic/—OrthomodularLattice,EpistemicHilbertSpace, measure, commutator.giry/—MeasurableSpace,ProbabilityMeasure, Giry monad,LlmOracle.epistemic/—EpistemicStatus,Theory,EpistemicTopology, theory-site.cohesive/— cohesive structure: Π ⊣ Disc ⊣ Γ ⊣ coDisc.day_convolution/—SymmetricMonoidalCategory,DayConvolution,CognitiveExtension.sdg/— synthetic differential geometry:D,TangentBundle,DifferentialForm,Connection.
Miscellaneous
complex/— complex numbers.category_finite/— finite categories (decidable equality).bitvec/— bit-vectors for cryptography.observational/— observational type theory.examples/— worked examples covering the algebra and topology layers.internal/— library internals (@internalmarked).simple//advanced/— convenience API / fine-grained API.tactics/— tactic library for proof automation.
Cross-references
- simd — SIMD vectors that
math.tensoruses under the hood. - intrinsics — raw CPU/GPU primitives.
- theory_interop — theory registry + translation + coherence audit; consumes
math.infinity_topos+math.kan_extension. - proof — proof certificates that verify math-module obligations.
- Verification → cubical & HoTT — the path types that
math.hottencodes.