Vanadium

Runtime safety utilities inspired by Ada for the V programming language.

Vanadium provides a set of runtime check wrappers, memory isolation layers, and compile-time design utilities for the V programming language. It introduces ranged types, validated values, sandboxed variables, thread-safe synchronization containers, bounded arrays, secure buffers, timing attack guards, and a development-time property prover.

Operations return V Result types (!T), prompting explicit handling at runtime.

• Core Protections
• API Reference
  • Ranged Types
  • Validated Variables
  • Jail and Sandboxing
  • Memory Protected IJail
  • Seccomp Sandboxing Alternative
  • Thread-Safe Locked Variables
  • Bounded Arrays
  • Checked Arithmetic
  • Safe Type Casting
  • Compile-Time Dimensional Analysis
  • Timing Attack Mitigation
  • Secure Buffers
  • Depth Guard
  • Finite State Machines
• Development-Time Bounded Prover
• Performance and Optimizations
• Limitations
• License

Vanadium provides runtime mitigations or development-time checks for several common programming concerns:

The Ranged[T] structure constrains any ordered numeric type to a specific min..max range. Reading .val is read-only outside the module, while mutation requires calling .set().

struct Ranged[T] {
pub:
	min T
	max T
	val T
}

mut score := vanadium.ranged(0, 100, 75) or {
	eprintln(err)
	return
}
println(score)

score.set(85) or { eprintln(err) }
score.set(120) or {
	eprintln(err)
}

The Validated[T] structure wraps a value with an associated validation function. All mutations run through this validator before committing to the inner field. It compiles with automatic deep cloning for maps and arrays to avoid unsafe references.

struct Validated[T] {
pub:
	validator fn (T) bool
	val T
}

mut email := vanadium.validated('user@domain.com', fn (s string) bool {
	return s.contains('@') && s.ends_with('.com')
})!

email.set('invalid-format') or {
	eprintln(err)
}

The Jail[T] container acts as a type-level quarantine for untrusted variables (e.g. raw web or Telegram user inputs). The wrapped value is private and cannot be read directly, forcing developers to sanitize or validate the variable to release it.

mut user_jail := vanadium.jail('  untrusted_dirty_username   ')

cleaned := user_jail.map(fn (s string) string {
	return s.trim_space()
})

released := cleaned.release(fn (s string) bool {
	return s.is_alnum() && s.len < 30
}) or {
	eprintln(err)
	return
}
println(released.val)

The IJail structure isolates untrusted input strings physically in memory using OS-level system calls. It allocates a dedicated memory page surrounded by read/write disabled guard pages (PROT_NONE). Any out-of-bounds read or overflow attempt triggers an immediate hardware-level segmentation fault, halting the process before heap/stack contamination.

To prevent memory leaks or unsafe heap references, raw string exposure is restricted. Data must be processed locally inside localized callback closures.

mut raw_payload := vanadium.ijail('raw_dirty_payload')!
raw_payload.use(fn (payload string) ! {
	println(payload)
})!
raw_payload.free()

mut raw_payload := vanadium.ijail('{"id": 45}')!
user_id := raw_payload.execute(fn (payload string) !int {
	return 45
})!
raw_payload.free()

For process hardening, system call filtering, and Seccomp sandboxing in V, please check out the tailsmails/vcomp project.

The Locked[T] struct encapsulates any shared resource (such as a map or standard structures) inside an atomic synchronization container. It prevents concurrent write panics and data races. It features compile-time type branch analysis ($if T is $map / $if T is $array) to automatically duplicate reference types via deep-cloning.

mut safe_map := vanadium.locked(map[string]int{})

safe_map.update(fn (mut m map[string]int) {
	m['connections'] = 42
	m['queries'] = 0
})

println(safe_map.get()['connections'])

The BArray[T] structure represents a fixed-capacity list. This prevents unbounded allocations and bounds violations by handling failures through Result types.

struct BArray[T] {
pub:
	cap int
	data []T
}

mut arr := vanadium.barray[int](3)!
mut list := vanadium.barray_from([10, 20, 30], 5)!
list.append(40)!
list.remove(0)!

Standard arithmetic operations can silently wrap or truncate on integers. Vanadium provides runtime checked wrappers for standard types, using compiler-native overflow detection.

vanadium.c_add(a, b)!
vanadium.c_sub(a, b)!
vanadium.c_mul(a, b)!
vanadium.c_div(a, b)!

sum := vanadium.c_add(2000000000, 2000000000) or {
	eprintln(err)
	0
}

Narrowing conversions (e.g., i64 to u8) silently drop bits in V. The generic safe_cast[T, F] and helper functions check boundaries before casting.

vanadium.safe_cast[To, From](val)!
vanadium.to_u8(val)!
vanadium.to_i16(val)!
vanadium.to_i32(val)!
vanadium.to_i64(val)!

val_u8 := vanadium.to_u8(i64(128))!

vanadium.to_u8(i64(300)) or {
	eprintln(err)
}

Unlike standard primitive tagging, Vanadium uses generic phantoms to enforce unit types (e.g., Meters, Seconds) directly at compile-time with zero runtime overhead.

struct Unit[A, B] {
pub:
	val B
}

struct Meter {}
struct Second {}
struct Speed {}

dist := vanadium.unit[Meter, int](150)
time_val := vanadium.unit[Second, int](5)

speed := vanadium.div_units[Meter, Second, Speed, int](dist, time_val)!
println(speed.val)

Compares byte arrays using bitwise XOR accumulation, ensuring processing time is constant regardless of where mismatches occur.

key_a := [u8(1), 2, 3]
key_b := [u8(1), 2, 4]
is_equal := vanadium.constant_time_eq(key_a, key_b)

Pads the execution of sensitive routines to always meet a designated threshold, protecting against runtime side-channels.

tg := vanadium.time_guard(100 * time.millisecond)
do_cryptographic_work()
tg.pad()

vanadium.timed_call(50 * time.millisecond, fn () {
	verify_database_record()
})

The SecBuf structure stores sensitive data (e.g., cryptographic keys, passwords) and performs a deterministic multi-pass write barrier (zeros, 0xFF, pattern, zeros) during clear() to prevent RAM cold boot recovery.

mut buf := vanadium.sec_buf(32)!
buf.write([u8(0xAA), 0xBB, 0xCC])!
buf.clear()

Protects against recursive stack overflow by enforcing limits on nested function calls.

fn recursive_parse(mut dg vanadium.Depth) ! {
	dg.enter()!
	defer { dg.leave() }
	
	recursive_parse(mut dg)!
}

Manages secure software states and allowed transitions step-by-step.

mut sm := vanadium.fsm('door', 0)
sm.add_state(0, 'locked')
sm.add_state(1, 'unlocked')
sm.add_transition(0, 1)

sm.step(1)!

Vanadium includes a finite mathematical property testing suite (Prover). It allows running exhaustive calculations over finite bounds in development environments.

To minimize overhead, all Prover functions and heavy Fsm verification routines compile as empty inline No-ops in production builds, allowing zero runtime cost when compiling with the -prod flag.

mut p := vanadium.new_prover('Math Properties')

p.prove_for_range('multiplication is commutative', -10, 10, fn (x i64) bool {
	return x * 2 == 2 * x
})

report := p.report()
if report != '' {
	println(report)
}

Vanadium prioritizes minimal overhead:

• Inlining: Performance-critical paths use the @[inline] attribute to reduce call-stack overhead.
• Branch Prediction: Conditions checking rare error paths are marked with _unlikely_ to aid compiler and CPU branch predictor optimizations.
• No global locks: Mutex locks are excluded by default; concurrency is managed natively through V’s standard concurrent patterns and isolated containers like Locked[T].
• Compile-time pruning: Large diagnostic structures compile to empty definitions under production mode, ensuring zero performance penalty in final builds.

Vanadium provides runtime mitigations and finite development testing. It is not a replacement for formal mathematical verification systems such as SPARK. For mission-critical environments (e.g., avionics, safety-critical medical devices), Ada/SPARK remains the required standard.