hraness

deterministic cores, effectful shells

pure logic in the middle, every effect behind a port

Drafted by an AI agent at Ben Guo's direct request from the Hraness source repositories, and checked against those sources before publication.

A peer-to-peer system lives or dies on two kinds of code: the code that decides, and the code that touches the world. The first kind must be replayable: given the same inputs it must produce the same outputs, byte for byte, on any machine, under a debugger or in a fuzzer. The second kind (sockets, clocks, filesystems, entropy) is none of those things. The architectural question is where you put the seam between them.

Valhalla’s answer is strict: every effect sits behind a port, and the cores hold no handle to the world at all.

the pattern

The workspace separates the system into a deterministic core and an effectful shell, and the line between them is not stylistic; it is a set of crate manifests. vhalla-core opens with #![no_std] and a doc comment that states the contract plainly: no filesystem, process, network, cryptography, model, or browser dependency. vhalla-session is no_std too, and its module doc says the same thing differently: “This crate has no network, clock, entropy, storage, policy, or host effects.” Inside vhalla-session there is a complete three-message handshake (Pending::initiate, Pending::respond, Pending::confirm, Pending::finish) and not one call that touches the outside.

How does a handshake work without a clock or a random source? The caller passes them in. initiate takes nonce: [u8; 32], now: u64, and deadline: u64 as plain values. The crate validates the nonce is not all zeros (a broken entropy source fails closed) and checks now against the deadline and the pairing’s expires_at. Freshness is a parameter, not a syscall. The session id is derived deterministically: SHA-256 over a domain string, the pairing digest, and both nonces. Two runs with the same inputs produce the same session id; that is not a bug, it is the property that makes the whole layer testable.

where the line runs

The ports are the edges of the pure crates. Time comes in as now: u64 parameters: verify_and_accept, receive, execute, check_deadline all take a clock reading instead of reading a clock. Entropy comes in as nonce: [u8; 32] parameters; the OS entropy lives in vhalla-identity’s Unix adapter, which calls getrandom::fill and passes the bytes inward. The transport keys a session binds to arrive as observed_local and observed_remote, values the adapter took from an authenticated connection, which the pure layer treats as claims to compare against the pinned Pairing, never as truth.

The shell is every crate allowed to touch the world: vhalla-identity (filesystem and entropy), vhalla-native (libp2p sockets), vhalla-journal and the three *-store crates (durable state, unix-gated), vhalla-rooms-node (a whole tokio runtime). Each is small relative to what it protects, and each translates between the world’s messy types (io::Result, Instant, file handles) and the core’s closed enums and fixed-width records.

why bother

The payoff is not purity for its own sake. Three concrete things fall out of the seam.

The core replays. crates/vhalla-ledger/tests/recovery_hegel.rs drives a stateful test (appends, checkpoints, snapshot, restore, replay attempts) with every choice drawn inside the loop from a seeded generator. Sixty-four cases run in milliseconds and shrink to minimal failures deterministically, because nothing in Ledger can reach a wall clock or a file. The same property is why vhalla-wire’s proptest round-trips are total: Envelope::decode is a pure function of its input bytes.

The boundary is auditable. When a reviewer asks “what can this code do,” the answer for vhalla-session is compute and return. Every effect is visible in the signature of the function that requests it. You do not have to grep for std::net: no_std makes it unnameable.

The shell is thin by necessity. Because the cores refuse to hold effect handles, the adapters cannot smuggle policy into themselves. vhalla-native’s job is reduced to: read bounded frames, observe transport keys, call Pending::respond with fresh nonces, write the returned bytes. The session logic, the part that can be wrong, is all in the pure crate where a test can reach it.

how the effects get in

Look at the actual injection points, because the discipline is in the details. vhalla-identity’s Identity::initiate_session is the bridge: it calls getrandom::fill(&mut nonce) itself (the only place entropy enters), then delegates to Pending::initiate(pairing, &self.key, observed_local, observed_remote, nonce, now, deadline). The signing key never leaves Identity; the session crate receives &SigningKey and returns bytes and a Pending. The adapter owns the syscall; the core owns the semantics.

The same shape appears in the journal. vhalla-journal is not no_std (it must fsync), but it still separates the decision from the effect. A Store trait names every filesystem operation the commit protocol needs: lock, read_pin, create_bundle, sync_bundle, write_height_marker, rename_pin, sync_dir. FsStore implements it against a real directory; FaultingStore wraps any Store and injects programmed faults per step (CrashBefore, CrashAfter, FailIo) while logging the attempted order. The commit protocol is pure sequencing logic; the commit operations are a port.

That port is what lets the test suite answer questions a unit test never could. crash_after_rename_recovers_committed_and_retry_is_idempotent kills the process after rename_pin but before sync_dir, reopens the journal, and asserts the pin is committed and the retry reconciles to AlreadyCommitted rather than double-applying. The fault is injected at exactly one step, through the Store boundary, without patching the filesystem.

testing what the shell owes

Once the seam exists, the tests line up by layer. In the core: proptest for round-trip laws (Envelope encode/decode), Hegel for stateful sequences (ledger restart-and-replay), compile-fail doctests for the type-state rules (VerifiedEnvelope cannot be cloned, AuthorizedEffect cannot be fabricated). At the boundary: FaultingStore schedules crash points through vhalla-journal’s Step enum (Lock, ReadPin, CreateBundle, SyncBundle, WriteHeightMarker, SyncHeightMarker, WritePinTmp, SyncPinTmp, RenamePin, SyncDir) and asserts recovery behavior per step. In the shell: real two-process subprocess tests in vhalla-cli/tests/ and vhalla-native where actual QUIC sockets carry actual frames.

The layers do not substitute for each other. A passing proptest does not qualify the socket code; a green two-process test does not prove the recovery rules. But each layer’s tests are cheap precisely because the others hold: the pure tests never wait on timeouts, and the socket tests never need to imagine corrupt state: they observe real corruption only if the OS produces it.

the honest limits

Two caveats matter, and the codebase states both.

First, determinism does not survive losing state. vhalla-crypto’s ReplayWindow is deliberately volatile: not cloneable, not resettable, not evicting. The crate doc is blunt: “Replay state is volatile; a restarted owner must retain it durably or establish a fresh session before accepting traffic.” A pure core makes the decision replayable; it does not make the history durable. That is the shell’s job, and the session crate punts it upward with a documented requirement rather than pretending otherwise.

Second, the pattern does not isolate hostile code in the same process. vhalla-host’s doc is equally blunt: “Rust ownership prevents ordinary capability duplication; it does not isolate hostile code or protect policy/clock storage in a compromised process.” A deterministic core behind ports is a way to make correct code cheap to verify and incorrect code hard to write. It is not a sandbox, and no amount of no_std changes what a malicious dependency in the same address space can do.

A third limit is that the injected clock is only as trustworthy as its source. vhalla-native implements Clock on top of SystemTime plus Instant (the wall clock for the value, the monotonic clock for elapsed time) and returns Error::Clock if the wall clock ever moves backwards. vhalla-session goes further: a now earlier than the last accepted reading calls close() on the session, permanently. A clock rollback is treated not as a bad input but as evidence that the timeline is no longer reliable: the session cannot be trusted to order events, so it ends. The pure layer’s determinism means the rollback is always detected; the shell’s job is to decide that detection means stop, not carry on.

The pattern’s real claim is narrower and more durable: every effect is a parameter, every decision is a pure function, and the seam between them is drawn by the compiler. Whatever the shell touches, the core can always be replayed.

sources

  • vhalla
  • crates/vhalla-session/src/lib.rs: the no_std handshake with injected now, nonce, deadline
  • crates/vhalla-identity/src/unix.rs: the OS-entropy adapter that feeds the core
  • crates/vhalla-journal/src/lib.rs: the Store port, FsStore, and FaultingStore
  • crates/vhalla-ledger/tests/recovery_hegel.rs: stateful deterministic testing over a pure core
  • crates/vhalla-host/src/lib.rs: the “ownership is not isolation” caveat in its own words

keep reading: free for subscribers

the rest of this lesson is free. add your email once and every subscriber lesson on this site stays unlocked.

already subscribed? enter the same email to unlock.