hraness

deterministic semantics: seeded order, atomic commits, replay

same input, same world, every time

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

A deterministic language is not one that avoids randomness; it is one where every source of variation is a declared input. Ask “what does this program do” of a Platonik experiment and the answer is a mathematical object: the same Experiment value, fed to the same interpreter, produces the same RunResult, byte for byte, on any machine that compiles the pinned toolchain. That property is what turns a run into evidence. This article walks through the three mechanisms that make it true in crates/platonik-core/src/sim.rs: a fixed tick pipeline, a seeded activation order, and atomic per-cell commits, and then the verification scheme that converts determinism into receipts.

the order of a tick

Determinism fails first at ambiguous scheduling: if two cells can act “simultaneously,” someone has to define who sees what. Platonik’s answer is a totally ordered tick. In run_through, each tick executes these phases in this exact sequence:

  1. Expire unread inbox signals. Every inbox entry still occupied from the previous tick is cleared and recorded as expired. Messages are transient by physics; persistence must be earned through take_message into a register.
  2. Apply declared events. Each Event scheduled for this tick (a link_enabled or valve_enabled toggle, a clear_memory intervention, or a v2+ edge_blocked closure) is applied to a cloned state and committed in declaration order.
  3. Deliver due signals. Pending Signal values with deliver_tick <= tick are attempted in queue order; each resolves to delivered, disabled, not_adjacent, or full, and the outcome is recorded on the frame.
  4. Activate each eligible cell once, in seeded order. This is the sweep. A cell born during construction becomes eligible no earlier than the tick after its birth: active_order filters on birth.tick < tick.
  5. Drain beacons. Each beacon whose drain_every divides the tick loses up to drain_amount charge; a drain to zero marks exhausted.
  6. Charge checking and audit invariants. The meter reserves Checking work proportional to cells, beacons, sparks, closed edges, and construction state, then check_live_invariants runs while the tick’s frame is still warm.

Every phase boundary is a semantic commitment. Because events fire before activation, a route closure scheduled at tick 27 is already true when cells choose their moves that tick. Because delivery precedes activation, a signal sent on tick 40 with delay 2 is observable on tick 42, never sooner. Because drains come last, a cell that deposits its spark on the drain tick still saves the beacon: the credit lands in phase four, the drain hits in phase five, and the ledger reconciles.

seeding the schedule

Inside the sweep, the question “which cell acts first” could leak nondeterminism through iteration order, hash maps, or pointer addresses. Platonik removes the question entirely: order_ids sorts the eligible cell ids by a keyed hash that changes every tick but derives only from declared inputs.

fn mix(mut value: u64) -> u64 {
    value = value.wrapping_add(0x9e3779b97f4a7c15);
    value = (value ^ (value >> 30)).wrapping_mul(0xbf58476d1ce4e5b9);
    value = (value ^ (value >> 27)).wrapping_mul(0x94d049bb133111eb);
    value ^ (value >> 31)
}
ids.sort_by_key(|id| (mix(experiment.seed ^ ((tick as u64) << 32) ^ *id as u64), *id));

The mix is the SplitMix64 finalizer (three multiply-xor rounds with the standard constants) applied to seed ^ (tick << 32) ^ id. Sort by the mixed value, break ties by the raw id. The schedule is therefore fair in a precise sense: each cell’s position in the order varies unpredictably across ticks (no permanent first-mover advantage), yet it is a pure function of (seed, tick, id), all immutable inputs, so the entire sequence can be recomputed by anyone holding the experiment file. The challenge generator reuses the same SplitMix64 family for its world derivation, keeping the whole system on one dependency-free, platform-stable mixing function.

Stable identity does the other half of the work. Cells are addressed by id: u16, not by position or index, so the order is over identities, and the seeded shuffle is the only randomness the scheduler has. There is no HashMap iteration in the hot path, no system RNG, no thread interleaving. The engine is single-threaded and the model is integer-only, which removes floating-point and concurrency nondeterminism by construction rather than by discipline.

atomicity is a semantic choice

policy::activate gives each cell a transaction. It snapshots the meter, clones the world State, executes the rule scan and one action into the clone, and then decides what to commit:

  • Success: the clone replaces the world; later cells in the sweep see the committed result.
  • Ordinary action failure (a blocked move, an empty-source pickup): the clone still commits (position unchanged), the attempt is recorded with its error, and the meter keeps its charges.
  • Limit fault (Stop::Fuel or Stop::Activation): the clone is discarded entirely; the world rolls back as if the cell never acted, but the meter is not part of the clone, so the spent fuel remains spent.

That last case is the subtle one. Rollback preserves integrity (a half-written signal or a mid-move cell can never be observed) while the retained charges preserve accounting, so a program cannot probe the world for free by exceeding its window halfway through. docs/engine.md compresses the contract into one line: “Each activation commits atomically and permits at most one action; later cells see the committed state. Movement never grants an extra activation.” That final clause kills a whole class of double-turn exploits: a move is the action, not a prelude to one.

Even the way a run ends is enumerated. RunStatus has exactly three values (Complete, FuelExhausted, ActivationLimit), and the outcome predicate combines status with the world’s own conservation checks, so “the program did well” and “the run finished” and “the ledger balanced” are separately recorded facts. A deterministic failure is still a deterministic result: a fuel-exhausted run replays to the identical partial trace, which is why the suite can preserve expected failures alongside successes and verify both.

replay is the semantics

Determinism is only useful if someone checks it, so the receipt format makes re-execution the definition of verification. A platonik-receipt-v1 envelope in check.rs carries {schema, protocol, experiment_hash, result_hash, experiment, result}: the complete input beside the complete output, each identified by artifact_hash, a SHA-256 over the canonical serde JSON.

verify_receipt then does the strict thing. It confirms the schema and protocol match the experiment’s declared version, recomputes both hashes, runs the independent validate_result checker (which audits conservation, beacon ledgers, delivery records, activation order, and budgets without trusting the simulator’s own predicates) and finally calls run(&receipt.experiment) again, requiring replayed == receipt.result: exact structural equality of the entire trace, every frame, every cost counter. The repository’s phrasing is blunt: “re-execution is the check; a hash alone is not evidence that a computation ran correctly.”

This is a meaning-preserving notion of equality. Whitespace and field order in the original JSON do not matter (parsing normalizes them), but every semantic value must be identical, so a receipt certifies “this input produces this output under this protocol version” and nothing weaker. The same machinery underwrites continuation: run_through accepts a checked frame prefix and resumes from its final state, which is how saved habitats advance across CLI invocations without trusting the save file: the prefix is re-verified, not believed. And it is what lets the aggregate gate double as cross-platform evidence: the same committed receipts pass recomputation on macOS and Linux CI, which is replay across architectures in the only sense that matters.

where determinism ends

The honest boundary deserves its own paragraph, because the repository draws it carefully. The checker is separate code in the same repository: check.rs audits the trace and verify re-runs the engine, but this is not an independent second implementation of every simulator rule, and the docs say so. Determinism is established for the pinned artifact (Rust 1.97.1, edition 2024, locked serde/serde_json/sha2, release overflow checks enabled), not for all hardware and all compilers forever. And determinism itself proves nothing about what a run means: an identical replay establishes that the computation is reproducible, not that it models anything outside itself.

What you can take from the design is the discipline: order every phase, derive every schedule from declared inputs, commit each step atomically with its costs retained, and define verification as re-execution rather than comparison. A deterministic language semantics is less a property you claim than a structure you build and then keep honest by checking it every single time.

sources

  • platonik: crates/platonik-core/src/sim.rs for the tick pipeline, order_ids, and run_through; crates/platonik-core/src/policy.rs for atomic activate; crates/platonik-core/src/check.rs for verify_receipt and artifact_hash
  • docs/engine.md: the tick contract and atomicity rules
  • docs/rust-bridge.md: “re-execution is the check” and the scope of the checker
  • docs/continuous-habitat.md: checked continuation of a saved world